tla-example-with-fold.dl

.type ServerId <: symbol
.type ClientId <: symbol
.functor list_fold(a: HeldOrLockedState, elem: number):HeldOrLockedState 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 NumServers(n: number)
NumServers(n+1) :-
  n = max i: ServerIndex(_, i).


.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).

// 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 HeldOrLockedState = [
  index: number,
  rest: HeldOrLockedState
]

.type State = [
  locked: HeldOrLockedState,
  held: HeldOrLockedState
]


.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, si: number)
  .decl Locked_Prime(prevState: State, action: Action, si: number)

  // client holds server
  .decl Held(state: State, csi: number)
  .decl Held_Prime(prevState: State, action: Action, csi: number)
  
  .decl IsState(state: State)
  IsState(state) :-
    (Locked(state, _);
     Held(state, _)).

  .decl ExaminedState(state: State)  // Grows monotonically. Means "will have been examined *after* the current stage".
  ExaminedState(state) :-
    IsState(state).

  /*
   * 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 HeldStateFinalized(prevState: State, action: Action, hstate: HeldOrLockedState)
  HeldStateFinalized(prevState, action, id_list) :-
    PossibleAction(prevState, action),
    id_list = @@list_fold i: nil, {Held_Prime(prevState, action, i)}.

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

  .decl LockedStateFinalized(prevState: State, action: Action, lstate: HeldOrLockedState)
  LockedStateFinalized(prevState, action, id_list) :-
    PossibleAction(prevState, action),
    id_list = @@list_fold i: nil, {Locked_Prime(prevState, action, i)}.

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

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

  /*
   * 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, action: Action, c: ClientId, s: ServerId)
  ConnectPossible(prevState, action, c, s) :-
    Locked(prevState, si),
    ServerIndex(s, si),
    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, csi) :-
    ConnectPossibleAction(prevState, action),
    Held(prevState, csi).
 
  Held_Prime(prevState, action, csi) :-
    ConnectPossible(prevState, action, c, s),
    ClientServerIndex(c, s, csi).

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


  // Optimization predicates
  .decl DisconnectPossible(prevState: State, c: ClientId, s: ServerId, action: Action)
  DisconnectPossible(prevState, c, s, action) :-
    Held(prevState, csi),
    ClientServerIndex(c, s, csi),
    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, csi) :-
    DisconnectPossible(prevState, c, s, action),
    Held(prevState, csi),
    ClientServerIndex(c2, s2, csi),
    (NotSameClient(c, c2);
     NotSameServer(s, s2)).

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

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

  .decl Unsound(state: State)
  Unsound(state) :-
    TotalStateFinalized(state, prevState, action),
    TotalStateFinalized(state, prevState2, action2),
    Held_Prime(prevState, action, i),
    !Held_Prime(prevState2, action2, i).

  .printsize Unsound    
  .output Unsound

} // 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 T8 = Transition
// .init T9 = Transition
// .init T10 = Transition
// .init T11 = Transition
// .init T12 = Transition
// .init T13 = Transition
.init TFinal = Transition

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

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


/*
 * Connecting transitions
 */ 

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

CopyRelations(T2, T1)
CopyRelations(T3, T2)
CopyRelations(T4, T3)
CopyRelations(T5, T4)
CopyRelations(T6, T5)
CopyRelations(T7, T6)
CopyRelations(TFinal, T7)
// CopyRelations(T8, T7)
// CopyRelations(T9, T8)
// CopyRelations(T10, T9)
// CopyRelations(T11, T10)
// CopyRelations(T12, T11)
// CopyRelations(T13, T12)
// CopyRelations(TFinal, T13)

.decl TotalHeld(state: State, clientServerIndex: number)
TotalHeld(state, csi) :-
  T1.Held(state, csi);
  T2.Held(state, csi);
  T3.Held(state, csi);
  T4.Held(state, csi);
  T5.Held(state, csi);
  T6.Held(state, csi);
  T7.Held(state, csi);
  // T8.Held(state, csi);
  // T9.Held(state, csi);
  // T10.Held(state, csi);
  // T11.Held(state, csi);
  // T12.Held(state, csi);
  // T13.Held(state, csi);
  TFinal.Held(state, csi).

.decl TotalLocked(state: State, serverIndex: number)
TotalLocked(state, si) :-
  T1.Locked(state, si);
  T2.Locked(state, si);
  T3.Locked(state, si);
  T4.Locked(state, si);
  T5.Locked(state, si);
  T6.Locked(state, si);
  T7.Locked(state, si);
  // T8.Locked(state, si);
  // T9.Locked(state, si);
  // T10.Locked(state, si);
  // T11.Locked(state, si);
  // T12.Locked(state, si);
  // T13.Locked(state, si);
  TFinal.Locked(state, si).

.decl TotalIsState(state: State)
TotalIsState(state) :-
  (TotalLocked(state, _);
   TotalHeld(state, _)),
  state != nil.

// .output TotalIsState

.decl Unsafe(state: State, c1: ClientId, c2: ClientId)
Unsafe(state, c1, c2) :-
  TotalHeld(state, csi1),
  ClientServerIndex(c1, s, csi1),
  ClientServerIndex(c2, s, csi2),
  TotalHeld(state, csi2),
  c1 != c2.


/*
 * Setup of problem instance
 */

IsServer("a").
IsServer("b").
IsServer("c").
IsServer("d").
IsServer("e").
IsServer("f").
IsServer("g").
// IsServer("h").
// IsServer("i").

IsClient("1").
IsClient("2").
IsClient("3").
IsClient("4").
IsClient("5").
IsClient("6").
IsClient("7").
// IsClient("8").
// IsClient("9").


// .printsize Locked
// .printsize Held


.printsize TotalIsState

.output Unsafe