Model of Jackson-Zave Turnstile Example

models
1

This is my attempt at an Alloy model of the famous turnstile example from Michael Jackson and Pamela Zave’s 1995 article Deriving Specifications from Requirements: an Example (https://doi.org/10.1145/225014.225016). The example has some interesting subtleties, e.g., the turnstile does not have to lock immediately after a person has pushed or entered, but can instead permit a small delay in case another coin is entered, preventing the need to lock and unlock for every customer.

I welcome feedback and suggestions for improvement.

/* Filename : turnstile.als
 * Author   : Stephen F. Siegel
 * Created  : 2024-03-06
 * Modified : 2024-03-10
 *
 * Model of the turnstile control system described in Jackson and Zave, 
 * "Deriving Specifications from Requirements: an Example", ICSE, 1995,
 * https://doi.org/10.1145/225014.225016
 *
 * I have tried to stay true to the spirit of the original article
 * while making changes to conform to the Alloy modeling style.
 *
 * Use with theme: TurnstileTheme.thm
 */
sig Person {} -- fixed set of all people
var sig Pushed in Person {} -- people who have pushed the turnstile
var sig Entered in Person {} -- people who have entered the zoo
sig Coin {} -- fixed set of all coins
var sig Paid in Coin {} -- coins that have been dropped in the machine
enum TurnstileEnum { PE0, PE1 } -- initial state and intermediate state
var one sig Turnstile in TurnstileEnum {} -- current state of Turnstile
enum LockEnum { LOCKED, UNLOCKED, LU2 } -- locked, unlocked, undefined states
var one sig Lock in LockEnum {} -- current state of Lock
enum Time { T10, T750 } -- units of time (milliseconds)
-- the sum of members of RLTime is a lower bound on the time since ReqLock
-- became true...
var sig RLTime in Time {}
fact init { -- initial state
  no Entered+Pushed+Paid+RLTime
  Turnstile = PE0
  Lock = LOCKED
}
pred push[p: Person] { -- a "Push" event
  !(p in Pushed+Entered) and Turnstile = PE0
  Turnstile' = PE1
  Pushed' = Pushed + p
  Entered' = Entered and Paid' = Paid and Lock' = Lock
  ReqLock implies RLTime' = RLTime + T10 else no RLTime'
}
pred enter[p: Person] { -- an "Enter" event
  (p in Pushed - Entered) and Turnstile = PE1
  Turnstile' = PE0
  Entered' = Entered + p
  Pushed' = Pushed and Paid' = Paid and Lock' = Lock
  ReqLock implies RLTime' = RLTime + T750 else no RLTime'
}
pred coin[c: Coin] {  -- a "Coin" event: a coin is dropped into machine
  ! (c in Paid)
  Paid' = Paid + c
  Pushed' = Pushed and Entered' = Entered and
  Turnstile' = Turnstile and Lock' = Lock
  ReqLock implies RLTime' = RLTime else no RLTime'
}
pred lock { -- a "Lock" event
  (Lock = UNLOCKED and Lock' = LOCKED) or
    (Lock = LOCKED and Lock' = LU2) or (Lock = LU2 and Lock' = LU2)
  Pushed' = Pushed and Entered' = Entered
  Paid' = Paid and Turnstile' = Turnstile
  ReqLock implies RLTime' = RLTime else no RLTime'
}
pred unlock { -- an "Unlock" event
  (Lock = LOCKED and Lock' = UNLOCKED) or
    (Lock = UNLOCKED and Lock' = LU2) or (Lock = LU2 and Lock' = LU2)
  Pushed' = Pushed and Entered' = Entered
  Paid' = Paid and Turnstile' = Turnstile
  ReqLock implies RLTime' = RLTime else no RLTime'
}
pred stutter { -- nothing happens
  Pushed' = Pushed and Entered' = Entered and Paid' = Paid
  Turnstile' = Turnstile and Lock' = Lock
  ReqLock implies RLTime' = RLTime else no RLTime'
}
pred ReqLock { Lock = UNLOCKED and #Pushed = #Paid } -- Lock is required
pred ReqUnlock { Lock = LOCKED and #Pushed < #Paid } -- Unlock is required
-- IND1: Push and Enter alternate: embedded in definition of push
-- DEF1: definition of LU0 (LOCKED), LU1 (UNLOCKED), and LU2:
--   embedded in definitions of lock, unlock
fact IND2 { -- no push when locked
  always ( Lock = LOCKED implies no p:Person | push[p] )
}
-- IND3: this is implied by IND1 so is not needed
-- IND4: Duration[PE0]>=10 and Duration[PE1]>=750.  This is modeled
--       using the RLTime variable.
fact OPT3 { -- machine alternates Unlock, Lock
  always {
    Lock = LOCKED implies !lock
    Lock = UNLOCKED implies !unlock
  }
}
fact OPT4 { -- locked and #Push=#Coin => unlock cannot occur
  always ((Lock = LOCKED and #Pushed = #Paid) implies !unlock)
}
fact OPT5 { -- unlocked and #Push<#Coin => lock cannot occur
  always ((Lock = UNLOCKED and #Pushed < #Paid) implies !lock)
}
fact OPT6 { -- Duration[ReqUnlock] < 250.  We use the weaker:
  always ( ReqUnlock => eventually !ReqUnlock )
}
fact OPT7 { -- Duration[ReqLock] < 760.  We use the weaker:
  always !(T10 + T750 in RLTime)
}
pred move {
  (some p:Person | (push[p] or enter[p])) or
  (some c:Coin | coin[c]) or
  lock or unlock 
}
fact Transition { always (move or stutter) }
pred example1 { -- 3 people pay and enter
  #Person = 3
  #Coin = 3
  eventually #Entered = 3
}
run example1 for 3 but 20 steps
-- the following illustrates the interesting property that after the
-- first unlock, people can repeatedly pay and enter the zoo without
-- any intervening lock action occurring...
pred example2 { -- coin, unlock, push, enter, coin, push, enter
  #Person = 2
  #Coin = 2
  eventually {
    some p:Person | push[p]
    after {
      some p:Person | enter[p]
      after {
        some c:Coin | coin[c]
        after {
          some p:Person | push[p]
          after {
            some p:Person | enter[p]
          }
        }
      }
    }
  }
}
run example2 for 3 but 10 steps
-- Now what we want to check: OPT1 and OPT2. All checks pass.
assert OPT1 { always #Entered <= #Paid }
check OPT1 for 3 but 2 Person, 2 Coin, 20 steps
check OPT1 for 3 but 30 steps 
check OPT1 for 4 but 30 steps  -- over 2 minutes on Mac M1
assert OPT2 { -- if credit, machine does not block someone from entering
  always (#Entered < #Paid =>
    eventually ( Lock=UNLOCKED or some Pushed - Entered) )
}
check OPT2 for 3 but 2 Person, 2 Coin, 20 steps
check OPT2 for 3 but 30 steps
check OPT2 for 4 but 30 steps -- almost 1 minute on Mac M1

I also have created a theme which makes the examples easier to understand.

2

I have revised this model to correct an error in how time was computed and clarify it somewhat. Here is v2:

/* Filename : turnstile.als
 * Author   : Stephen F. Siegel
 * Created  : 2024-03-06
 * Modified : 2024-03-14
 *
 * Model of the turnstile control system described in Jackson and Zave, 
 * "Deriving Specifications from Requirements: an Example", ICSE, 1995,
 * https://doi.org/10.1145/225014.225016
 *
 * I have tried to stay true to the spirit of the original article
 * while making changes to conform to the Alloy modeling style.
 *
 * Use with theme: TurnstileTheme.thm
 */

sig Person {} -- fixed set of all people
var sig Pushed in Person {} -- people who have pushed the turnstile
var sig Entered in Person {} -- people who have entered the zoo

sig Coin {} -- fixed set of all coins
var sig Paid in Coin {} -- coins that have been dropped in the machine

enum TurnstileEnum { PE0, PE1 } -- initial state and intermediate state
var one sig Turnstile in TurnstileEnum {} -- current state of Turnstile

enum LockEnum { LOCKED, UNLOCKED, LU2 } -- locked, unlocked, undefined states
var one sig Lock in LockEnum {} -- current state of Lock

/* Time: variable RLTime gives a lower bound on the time since ReqLock
   last became true.  To make this precise, say 

     s0 --t1--> s1 --t2--> ... s(n-1) --tn--> sn

   is an execution.  We first define the current interval I in which
   ReqLock has been true.  There are two cases, depending on whether
   ReqLock holds at s(n-1).
  
   If ReqLock holds at s(n-1), let i be the least integer such that ReqLock
   holds in s(j) for all j:i..n-1.  Then t(i) occurs at a point in time
   that begins the interval in which ReqLock holds.  (t(n) either ends that
   interval or is also in that interval.)  Let I be the time interval that
   begins with event t(i) and ends with event t(n).  The events occurring
   in I are t(i),...,t(n).

   If ReqLock does not hold at s(n-1) but does hold at s(n) then t(n)
   begins a new interval in which ReqLock holds.  Let I be the interval
   which is the single point in time at which t(n) occurs. The only event
   occurring in I is t(n).

   If ReqLock is false at both s(n-1) and s(n) then I is empty and RLTime
   is empty, and nothing further need be said about this case.
        
   Otherwise the value R of RLTime in s(n) satisfies the following:
  
   (1) the sum of the numbers in R is less than or equal to the total
   real time (in milliseconds) of I

   Claim (1) follows from the following claims, which follow in turn
   from how RLTime is updated at each transition.
   Let E be the projection of the events of I onto {Push,Enter}.

   (2) R is empty iff E is empty.

   (3) R={T0} iff E has size 1. (I.e., either E={Push} or E={Enter}.)

   (4) T10 is in R iff E contains a substring (Enter, Push).
   In this case, the turnstyle entered and exited state PE0 within I,
   and as Duration[PE0]>=10, the duration of I is at least 10.

   (5) T750 is in R iff E contains a substring (Push, Enter).
   In this case, the turnstyle entered and exited state PE1 within I,
   and as Duration[PE1]>=750, the duration of I is at least 750.

   Note that R contains T10+T750 iff E contains a substring
   (Enter, Push, Enter) or (Push, Enter, Push), which implies the
   duration of I, and therefore Duration[ReqLock], is at least 760.
   (One of the specifications, OPT7, says this can't happen.)
 */
enum Time { T0, T10, T750 } -- units of time (milliseconds)
var sig RLTime in Time {}

fact init { -- initial state
  no Entered+Pushed+Paid+RLTime
  Turnstile = PE0
  Lock = LOCKED
}

pred push[p: Person] { -- a "Push" event
  !(p in Pushed+Entered) and Turnstile = PE0
  Turnstile' = PE1
  Pushed' = Pushed + p
  Entered' = Entered and Paid' = Paid and Lock' = Lock
  !ReqLock => (ReqLock2 implies RLTime'=T0 else no RLTime')
  ReqLock => ((no Time) implies RLTime'=T0 else RLTime'=RLTime+T10)
}

pred enter[p: Person] { -- an "Enter" event
  (p in Pushed - Entered) and Turnstile = PE1
  Turnstile' = PE0
  Entered' = Entered + p
  Pushed' = Pushed and Paid' = Paid and Lock' = Lock
  !ReqLock => (ReqLock2 implies RLTime'=T0 else no RLTime')
  ReqLock => ((no Time) implies RLTime'=T0 else RLTime'=RLTime+T750)
}

pred coin[c: Coin] {  -- a "Coin" event: a coin is dropped into machine
  ! (c in Paid)
  Paid' = Paid + c
  Pushed' = Pushed and Entered' = Entered and
  Turnstile' = Turnstile and Lock' = Lock
  ReqLock implies RLTime'=RLTime else no RLTime'
}

pred lock { -- a "Lock" event
  (Lock = UNLOCKED and Lock' = LOCKED) or
    (Lock = LOCKED and Lock' = LU2) or (Lock = LU2 and Lock' = LU2)
  Pushed' = Pushed and Entered' = Entered
  Paid' = Paid and Turnstile' = Turnstile
  ReqLock implies RLTime'=RLTime else no RLTime'
}

pred unlock { -- an "Unlock" event
  (Lock = LOCKED and Lock' = UNLOCKED) or
    (Lock = UNLOCKED and Lock' = LU2) or (Lock = LU2 and Lock' = LU2)
  Pushed' = Pushed and Entered' = Entered
  Paid' = Paid and Turnstile' = Turnstile
  ReqLock implies RLTime'=RLTime else no RLTime'
}

pred stutter { -- nothing happens
  Pushed' = Pushed and Entered' = Entered and Paid' = Paid
  Turnstile' = Turnstile and Lock' = Lock
  ReqLock implies RLTime'=RLTime else no RLTime'
}

-- Lock is required in the current state...
pred ReqLock { Lock = UNLOCKED and #Pushed = #Paid }
-- Lock is required in the next state...
pred ReqLock2 { Lock' = UNLOCKED and #Pushed' = #Paid' }
 -- Unlock is required in the current state...
pred ReqUnlock { Lock = LOCKED and #Pushed < #Paid }

-- IND1: Push and Enter alternate: embedded in definition of push
-- DEF1: definition of LU0 (LOCKED), LU1 (UNLOCKED), and LU2:
--   embedded in definitions of lock, unlock

fact IND2 { -- no push when locked
  always ( Lock = LOCKED implies no p:Person | push[p] )
}

-- IND3: this is implied by IND1 so is not needed
-- IND4: Duration[PE0]>=10 and Duration[PE1]>=750.  This is modeled
--       using the RLTime variable.

fact OPT3 { -- machine alternates Unlock, Lock
  always {
    Lock = LOCKED implies !lock
    Lock = UNLOCKED implies !unlock
  }
}

fact OPT4 { -- locked and #Push=#Coin => unlock cannot occur
  always ((Lock = LOCKED and #Pushed = #Paid) implies !unlock)
}

fact OPT5 { -- unlocked and #Push<#Coin => lock cannot occur
  always ((Lock = UNLOCKED and #Pushed < #Paid) implies !lock)
}

fact OPT6 { -- Duration[ReqUnlock] < 250.  We use the weaker:
  always ( ReqUnlock => eventually !ReqUnlock )
}

fact OPT7 { -- Duration[ReqLock] < 760.  We use the weaker:
  always !(T10 + T750 in RLTime)
}

pred move {
  (some p:Person | (push[p] or enter[p])) or
  (some c:Coin | coin[c]) or
  lock or unlock 
}

fact Transition { always (move or stutter) }

pred example1 { -- 3 people pay and enter and gate locks
  eventually (#Entered = 3 and !ReqLock)
}
run example1 for 3 but 20 steps

-- the following illustrates the interesting property that after the
-- first unlock, people can repeatedly pay and enter the zoo without
-- any intervening lock action occurring...
pred example2 { -- coin, unlock, push, enter, coin, push, enter
  eventually {
    (some p:Person | push[p]);
    (some p:Person | enter[p]);
    (some c:Coin | coin[c]);
    (some p:Person | push[p]);
    (some p:Person | enter[p])
  }
}
run example2 for 3 but 10 steps

-- Now what we want to check: OPT1 and OPT2. All checks pass.

assert OPT1 { always #Entered <= #Paid }
check OPT1 for 3 but 2 Person, 2 Coin, 20 steps
check OPT1 for 3 but 30 steps 
check OPT1 for 4 but 30 steps  -- over 2 minutes on Mac M1

assert OPT2 { -- if credit, machine does not block someone from entering
  always (#Entered < #Paid =>
    eventually ( Lock=UNLOCKED or some Pushed - Entered) )
}
check OPT2 for 3 but 2 Person, 2 Coin, 20 steps
check OPT2 for 3 but 30 steps
check OPT2 for 4 but 30 steps -- almost 1 minute on Mac M1

-- paper doesn't say this but it's also true that T10 never added
-- to RLTime...
assert noT10 { always !(T10 in RLTime) }
check noT10 for 3 but 30 steps