tla-example-with-functor.dl

.type ServerId <: symbol
.type ClientId <: symbol
.functor hashsum(i1:number, i2:number):number stateful

/*
 * Ordering predicates (scaffolding)
 */
.decl IsServer(id: ServerId)
.decl ServerLT(s1: ServerId, s2: ServerId)
ServerLT(s1, s2) :-
  IsServer(s1),
  IsServer(s2),
  ord(s1) < ord(s2).

.decl ServerIndex(s: ServerId, index: number)
ServerIndex(s, i) :-
  IsServer(s),
  i = count : ServerLT(_, s).

.decl FirstServer(s: ServerId)
FirstServer(s) :-
  IsServer(s),
  !ServerLT(_, s).

.decl LastServer(s: ServerId)
LastServer(s) :-
  IsServer(s),
  !ServerLT(s, _).

.decl LastServerIndex(s: ServerId, index: number)
LastServerIndex(s, index) :-
  LastServer(s),
  ServerIndex(s, index).

.decl NextServer(p: ServerId, n: ServerId)
NextServer(p, n) :-
  ServerIndex(p, i),
  ServerIndex(n, i+1).

.decl NumServers(n: number)
NumServers(n+1) :-
  LastServerIndex(_, n).


.decl IsClient(id: ClientId)
.decl ClientLT(c1: ClientId, c2: ClientId)
ClientLT(c1, c2) :-
  IsClient(c1),
  IsClient(c2),
  ord(c1) < ord(c2).

.decl ClientIndex(c: ClientId, index: number)
ClientIndex(c, i) :-
  IsClient(c),
  i = count : ClientLT(_, c).

.decl FirstClient(c: ClientId)
FirstClient(c) :-
  IsClient(c),
  !ClientLT(_, c).

.decl LastClient(c: ClientId)
LastClient(c) :-
  IsClient(c),
  !ClientLT(c, _).

.decl LastClientIndex(c: ClientId, index: number)
LastClientIndex(c, index) :-
  LastClient(c),
  ClientIndex(c, index).

.decl NextClient(p: ClientId, n: ClientId)
NextClient(p, n) :-
  ClientIndex(p, i),
  ClientIndex(n, i+1).

.decl NumClients(n: number)
NumClients(n+1) :-
  LastClientIndex(_, n).


// Similar ordering for client-server pairs
.decl ClientServerIndex(c: ClientId, s: ServerId, i: number)
ClientServerIndex(c, s, ci*ns + si) :-
  ClientIndex(c, ci),
  ServerIndex(s, si),
  NumServers(ns).


/*
 * Types
 */

.type Action = [
  kind : symbol, // "connect" or "disconnect"
  clientId : ClientId,
  serverId : ServerId
]

.type LockedState = [
  serverIndex: number,
  rest: LockedState
]

.type HeldState = [
  clientServerIndex: number,
  rest: HeldState
]

.type State = [
  locked: LockedState,
  held: HeldState
]


.decl DecomposeAction(a: Action, k: symbol, c: ClientId, s: ServerId)
DecomposeAction(a, k, c, s) :-
  IsClient(c),
  IsServer(s),
  (k = "connect"; k = "disconnect"),
  a = [k, c, s].



// Single transition component
.comp Transition {
  /*
   * Main state predicates
   */
  .decl Locked(state: State, server: ServerId)
  .decl Locked_Prime(prevState: State, action: Action, server: ServerId)
  .decl Locked_Prime_Index(prevState: State, action: Action, si: number)

  // client holds server
  .decl Held(state: State, client: ClientId, server: ServerId)
  .decl Held_Prime(prevState: State, action: Action, client: ClientId, server: ServerId)
  .decl Held_Prime_Index(prevState: State, action: Action, csi: number)
  
  .decl IsState(state: State)
  IsState(state) :-
    (Locked(state, _);
     Held(state, _, _)),
    state != nil.
    
  Locked_Prime_Index(prevState, action, si) :-
    Locked_Prime(prevState, action, server),
    ServerIndex(server, si).
    
  Held_Prime_Index(prevState, action, csi) :-
    Held_Prime(prevState, action, client, server),
    ClientServerIndex(client, server, csi).


  /*
   * Forall iterations, in order to finalize the state. Scaffolding, not essential logic.
   */

  .decl PossibleAction(prevState: State, action: Action)
  PossibleAction(prevState, action) :-
    ConnectPossibleAction(prevState, action);
    DisconnectPossibleAction(prevState, action).

  .decl HeldStateUpTo(prevState: State, action: Action, clientServerIndex: number, partialState: HeldState)
  HeldStateUpTo(prevState, action, index, [index, nil]) :-
    PossibleAction(prevState, action),
    index = @@hashsum i: 0, {Held_Prime_Index(prevState, action, i)}.

//   HeldStateUpTo(prevState, action, nextIndex, [nextIndex, prevPartialState]) :-
//     HeldStateUpTo(prevState, action, prevIndex, prevPartialState),
//     nextIndex = min(i): {
//       Held_Prime_Index(prevState, action, i),
//       i > prevIndex
//     }.
      
  .decl LockedStateUpTo(prevState: State, action: Action, si: number, partialState: LockedState)
  LockedStateUpTo(prevState, action, index, [index, nil]) :-
    PossibleAction(prevState, action),
    index = @@hashsum i: 0, {Locked_Prime_Index(prevState, action, i)}.

//   LockedStateUpTo(prevState, action, nextIndex, [nextIndex, prevPartialState]) :-
//     LockedStateUpTo(prevState, action, prevIndex, prevPartialState),
//     nextIndex = min(i): {
//       Locked_Prime_Index(prevState, action, i),
//       i > prevIndex
//     }.    
  
  .decl HeldStateFinalized(prevState: State, action: Action, hstate: HeldState)
  HeldStateFinalized(prevState, action, state) :-
    HeldStateUpTo(prevState, action, maxIndex, state),
    maxIndex = @@hashsum i: 0, {Held_Prime_Index(prevState, action, i)}.

  HeldStateFinalized(prevState, action, nil) :-
    PossibleAction(prevState, action),
    !Held_Prime_Index(prevState, action, _).

  .decl LockedStateFinalized(prevState: State, action: Action, lstate: LockedState)
  LockedStateFinalized(prevState, action, state) :-
    LockedStateUpTo(prevState, action, maxIndex, state),
    maxIndex = @@hashsum i: 0, {Locked_Prime_Index(prevState, action, i)}.

  LockedStateFinalized(prevState, action, nil) :-
    PossibleAction(prevState, action),
    !Locked_Prime_Index(prevState, action, _).

  .decl TotalStateFinalized(state: State, prevState: State, action: Action)
  TotalStateFinalized([ls, hs], prevState, action) :-
    HeldStateFinalized(prevState, action, hs),
    LockedStateFinalized(prevState, action, ls).


  /*
   * Optimization predicates capturing just the "not equals" relation
   */

  .decl NotSameServer(s1: ServerId, s2: ServerId)
  NotSameServer(s1, s2) :-
    IsServer(s1),
    IsServer(s2),
    s1 != s2.

  .decl NotSameClient(c1: ClientId, c2: ClientId)
  NotSameClient(c1, c2) :-
    IsClient(c1),
    IsClient(c2),
    c1 != c2.


  /*
   * Transition rules for next state
   */

  // Auxiliary predicates, both for optimization and used elsewhere
  .decl ConnectPossible(prevState: State, c: ClientId, s: ServerId, action: Action)
  ConnectPossible(prevState, c, s, action) :-
    Locked(prevState, s),
    DecomposeAction(action, "connect", c, s).

  .decl ConnectPossibleAction(prevState: State, action: Action)
  ConnectPossibleAction(prevState, action) :-
    ConnectPossible(prevState, _, _, action).
  
  // What happens to Held, upon a connect
  Held_Prime(prevState, action, c2, s2) :-
    ConnectPossibleAction(prevState, action),
    Held(prevState, c2, s2).

  Held_Prime(prevState, action, c, s) :-
    ConnectPossible(prevState, c, s, action).

  // Locked, upon a connect
  Locked_Prime(prevState, action, s2) :-
    ConnectPossible(prevState, _, s, action),
    Locked(prevState, s2),
    NotSameServer(s, s2).


  // Optimization predicates
  .decl DisconnectPossible(prevState: State, c: ClientId, s: ServerId, action: Action)
  DisconnectPossible(prevState, c, s, action) :-
    Held(prevState, c, s),
    DecomposeAction(action, "disconnect", c, s).

  .decl DisconnectPossibleAction(prevState: State, action: Action)
  DisconnectPossibleAction(prevState, action) :-
    DisconnectPossible(prevState, _, _, action).

  // What happens to Held, upon a disconnect
  Held_Prime(prevState, action, c2, s2) :-
    DisconnectPossible(prevState, c, s, action),
    Held(prevState, c2, s2),
    (NotSameClient(c, c2);
     NotSameServer(s, s2)).

  // Locked, upon a disconnect
  Locked_Prime(prevState, action, s2) :-
    DisconnectPossibleAction(prevState, action),
    Locked(prevState, s2).

  Locked_Prime(prevState, action, s) :-
    DisconnectPossible(prevState, _, s, action).

  .output IsState
} // end of Transition component


.init T1 = Transition
.init T2 = Transition
.init T3 = Transition
.init T4 = Transition
.init T5 = Transition
.init T6 = Transition
.init T7 = Transition
.init TFinal = Transition

/*
 * Initial state (successor of nil)
 */ 

// Initial state is nil
T1.Locked(nil, s) :-
  IsServer(s).


/*
 * Connecting transitions
 */ 

#define CopyRelations(tNew, tOld) \
  tNew.Held(state, client, server) :- tOld.Held(state, client, server). \
  tNew.Locked(state, server) :- tOld.Locked(state, server). \
  tNew.Held(state, client, server) :- tOld.TotalStateFinalized(state, prevState, action), tOld.Held_Prime(prevState, action, client, server). \
  tNew.Locked(state, server) :- tOld.TotalStateFinalized(state, prevState, action),  tOld.Locked_Prime(prevState, action, server).

  // tNew.Held_Prime(state, action, client, server) :- tOld.Held_Prime(state, action, client, server). \
  // tNew.Held_Prime_Index(state, action, csi) :- tOld.Held_Prime_Index(state, action, csi). \
  // tNew.Locked_Prime(state, action, server) :- tOld.Locked_Prime(state, action, server). \
  // tNew.Locked_Prime_Index(state, action, si) :- tOld.Locked_Prime_Index(state, action, si). \
  // tNew.HeldStateUpTo(prevState, action, clientServerIndex, partialState) :- tOld.HeldStateUpTo(prevState, action, clientServerIndex, partialState). \
  // tNew.LockedStateUpTo(prevState, action, si, partialState) :- tOld.LockedStateUpTo(prevState, action, si, partialState). \

CopyRelations(T2, T1)
CopyRelations(T3, T2)
CopyRelations(T4, T3)
CopyRelations(T5, T4)
CopyRelations(T6, T5)
CopyRelations(T7, T6)
CopyRelations(TFinal, T7)


.decl Unsafe(state: State, c1: ClientId, c2: ClientId)
Unsafe(state, c1, c2) :-
  TFinal.Held(state, c1, s),
  TFinal.Held(state, c2, s),
  c1 != c2.


/*
 * Setup of problem instance
 */

IsServer("a").
IsServer("b").
IsServer("c").
IsServer("d").
IsServer("e").
IsServer("f").
IsServer("g").
IsClient("1").
IsClient("2").
IsClient("3").
IsClient("4").
IsClient("5").
IsClient("6").
IsClient("7").

// .printsize Locked
// .printsize Held


.printsize TFinal.IsState

// .output IsState
.output Unsafe