...

open util/ordering [Time] as trace
open util/integer
open util/ordering [LockRef] as queue

...

sig Time { }

abstract sig Event { pre: Time, post: Time }
sig Null extends Event { } -- null events can only be at beginning of trace
fact NullEvent { all e: Null | no s: SystemState | e.pre = s.time }

fact TemporalStructure {
all t: Time - trace/last | one e: Event | e.pre = t
all t: trace/last | no e: Event | e.pre = t
all e: Event | e.post = (e.pre).next }

...

sig LockRef { }

pred PastQueue [g: set LockRef, f: lone LockRef, -- (g, f) is older
q: set LockRef, p: lone LockRef] { -- than (q, p)
(g = q)
=> (f != p && ( (some f && some p && queue/lt [f, p])
|| (some f && no p) ) )
else ( (g in q)
&& ( (some f && some p && queue/lte [f, p])
|| (some f && no p)
|| (no f && some p && p in (q - g))
|| (no f && no p) ) ) }

pred PastPtr [f: LockRef, s: SystemState] {
f in s.trueQset && (no s.trueQptr || queue/gt [s.trueQptr, f]) }

pred CurrentOrPastPtr [f: LockRef, s: SystemState] {
f in s.trueQset && (no s.trueQptr || queue/gte [s.trueQptr, f]) }

sig Timestamp {ref: LockRef, tme: Time}

fact TimestampsAreRecords { all p0, p1: Timestamp |
(p0.ref = p1.ref && p0.tme = p1.tme) => p0 = p1 }

pred EarlierTimestamp [t0, t1: Timestamp] {-- true if t0 is earlier than t1
queue/lt [t0.ref, t1.ref] || (t0.ref = t1.ref && lt [t0.tme, t1.tme]) }

pred EarlierOrEqualTimestamp [t0, t1: Timestamp] {
queue/lt [t0.ref, t1.ref] || (t0.ref = t1.ref && lte [t0.tme, t1.tme]) }

pred PastTimestamp [t: Timestamp, s: SystemState ] {
PastPtr [t.ref, s] || (t.ref = s.trueQptr && lt [t.tme, s.time]) }

pred CurrentOrPastTimestamp [t: Timestamp, s: SystemState ] {
PastPtr [t.ref, s] || (t.ref = s.trueQptr && lte [t.tme, s.time]) }

...

abstract sig Message { stamp: Timestamp, val: Value }

abstract sig RepMsg extends Message { cli: Client }
sig RepPutMsg, RepGetMsg extends RepMsg { }

fact RepMsgsAreRecords { all m0, m1: RepMsg |
(m0.cli = m1.cli && m0.stamp = m1.stamp && m0.val = m1.val) => m0 = m1 }

abstract sig ClientMsg extends Message { rep: Replica }
abstract sig ClientPutMsg, ClientGetMsg extends ClientMsg { }
sig ClientPutAck, ClientPutNack, ClientPutNohold extends ClientPutMsg {}
sig ClientGetAck, ClientGetNack, ClientGetNohold extends ClientGetMsg {}

fact ClientMsgsAreRecords { all m0, m1: ClientMsg |
(m0.rep = m1.rep && m0.stamp = m1.stamp && m0.val = m1.val) => m0 = m1 }

SYSTEM STATE AND TRACES

...

sig Client { }

sig Value { } one sig True, False extends Value { }

sig Replica { } fact { # Replica = 5 }

abstract sig ClientState { }
one sig Dead, Live, Enqueued, Critical, MustGet, MustPut, MustPut4Synch,
SynchGetting, SynchPutting, Getting, Putting extends ClientState { }

abstract sig ReplicaState { }
one sig Failed, Started extends ReplicaState { }

sig SystemState {
time: Time,
-- lock store
-- real state
Qset: Replica -> LockRef,
Qptr: Replica -> lone LockRef,
trueDataSynchFlag: True + False, -- true value in eventu.consis. data
-- history variables
trueQset: set LockRef,
trueQptr: lone LockRef,
synchFlag: True + False,
-- client state
-- real state
clientRef: Client -> lone LockRef,
clientState: Client -> one ClientState,
clientTask: Client -> lone (ClientPutAck + ClientGetAck),
-- what client is waiting for
clientInputs: Client -> ClientMsg,
-- history variables
trueTimestamp: Timestamp,
trueValue: Value,
-- music state
repState: Replica -> one ReplicaState,
repInputs: Replica -> RepMsg,
repTask: Replica -> lone RepMsg, -- what replica is working on
-- music's

-- the true data tuple is the written tuple with the highest timestamp
all t: Timestamp, v: Value |
( (t -> v) in (writePending + writeSucceeded)
&& (no t': Timestamp, v': Value |
(t' -> v') in (writePending + writeSucceeded)
&& EarlierTimestamp [t, t'] )
) => (t = trueDataTimestamp && v = trueDataValue)
}

pred DataStoreDefined [s: SystemState] {
-- the datastore is well-defined when it has a true tuple in writeSucceeded
some s.trueDataTimestamp
&& (s.trueDataTimestamp -> s.trueDataValue) in s.writeSucceeded }

fact UpdateOfDefinedSet {
all e: TraceEvent, s: e.prest, s': e.postst |
DataStoreDefined [s] => s'.defined = s.defined + s.time
else s'.defined = s.defined }

pred InitialState [s: SystemState] {
s.trueQset = queue/first && no s.trueQptr
s.Qset = (Replica -> queue/first) && no s.Qptr
Client.(s.clientState) in Dead && some s.trueValue
some s.trueTimestamp
(s.trueTimestamp).ref = queue/first && lt [(s.trueTimestamp).tme,s.time]
s.synchFlag = False && s.trueDataSynchFlag = False
no s.clientRef && no s.clientTask && no s.clientInputs
Replica.(s.repState) in Failed && no s.repInputs && no s.repTask
no s.writePending && no s.defined
s.writeSucceeded = (s.trueTimestamp -> s.trueValue) }

pred LockStoreInvariant [s: SystemState] {
-- LockRefs are ordered. A queue is represented by a set of lockRefs and
-- an optional pointer. The set contains all the lockRefs that have ever
-- been enqueued (ordered implicitly by the order on lockRefs, which is
-- also the order of use). If there is a pointer, it points to the current
-- lockHolder. If there is no pointer, all lockRefs in the set have been
-- used and released.
-- Unused lockRefs are always larger than queued ones.
all f0: s.trueQset, f1: LockRef - s.trueQset | queue/lt [f0, f1]
-- The trueQptr is in the trueQset.
s.trueQptr in s.trueQset
-- A replica's Qset must be the trueQset or a subset of it that is a
-- "prefix" of it, in the sense of the ordering on lockRefs.
all r: Replica |
( r.(s.Qset) in s.trueQset
&& all f0: r.(s.Qset), f1: s.trueQset - r.(s.Qset) | queue/lt [f0, f1] )
-- A replica's Qptr is in the replica's Qset.
all r: Replica | r.(s.Qptr) in r.(s.Qset)
-- A replica's queue must be a current or past truth.
all r: Replica |
( (r.(s.Qset) = s.trueQset && r.(s.Qptr) = s.trueQptr)
|| PastQueue [r.(s.Qset), r.(s.Qptr), s.trueQset, s.trueQptr] )
-- At least a quorum of replicas have the true queue.
let correctQueues =
{ r: Replica | r.(s.Qset) = s.trueQset && r.(s.Qptr) = s.trueQptr } |
gte [ # correctQueues, 3]
-- this is a basic safety property for the implementation of the synch flag
s.trueDataSynchFlag = False => s.synchFlag = False
}

pred ClientStateInvariant [s: SystemState] {
-- includes client's relation to music
-- A client's lockRef is found in the trueQset.
all c: Client | c.(s.clientRef) in s.trueQset
-- A client's lockRef is unique among clients, and is always in the
-- trueQset.
let repMsgRef = { c: Client, f: LockRef |
some m: Replica.(s.repInputs + s.repTask) |
(c = m.cli && f = m.stamp.ref) } |
let clientMsgRef = { c: Client, f: LockRef |
some m: c.(s.clientInputs + s.clientTask) |
f = m.stamp.ref && f = c.(s.clientRef) } |
( (all f: LockRef | lone (s.clientRef + repMsgRef + clientMsgRef).f)
&& (all f: Client.(s.clientRef + repMsgRef + clientMsgRef) |
f in s.trueQset )
)
-- properties of client states
all c: Client | c.(s.clientState) in (Dead + Live)
=> ( no c.(s.clientRef)
&& no c.(s.clientTask) )
all c: Client | c.(s.clientState) in Enqueued
=> ( some c.(s.clientRef)
&& ! PastPtr [c.(s.clientRef), s]
&& no c.(s.clientTask) )
all c: Client | c.(s.clientState) in Critical + MustGet
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef), s]
&& no c.(s.clientTask) )
all c: Client | c.(s.clientState) in MustPut + MustPut4Synch
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef),s]
&& some c.(s.clientTask) -- only the task value is significant
&& c.(s.clientTask) in ClientPutAck )
all c: Client | c.(s.clientState) in SynchGetting + Getting
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef), s]
&& some c.(s.clientTask) -- only replica and stamp are significant
&& c.(s.clientTask) in ClientGetAck )
all c: Client | c.(s.clientState) in SynchPutting + Putting
=> ( some c.(s.clientRef)
&& CurrentOrPastPtr [c.(s.clientRef), s]
&& some c.(s.clientTask) && c.(s.clientTask) in ClientPutAck )
-- the client task must be in the client's current epoch
all c: Client, m: ClientMsg |
m in c.(s.clientTask) => m.stamp.ref = c.(s.clientRef)
}

pred MusicStateInvariant [s: SystemState] {
-- includes Music's relation to datastore
-- If a replica has a task, it is started.
all r: Replica | some r.(s.repTask) => r.(s.repState) = Started
-- writes being waited for are writes pending or succeeded
all r: Replica, m: RepPutMsg |
(r -> m) in s.repTask
=> (m.stamp -> m.val) in s.writePending + s.writeSucceeded
}

pred DataStoreInvariant [s: SystemState] {
-- datastore writes are in the past
all t: (s.writeSucceeded).Value | PastTimestamp [t, s]
-- writes pending are in the past or present
all t: (s.writePending).Value | CurrentOrPastTimestamp [t, s]
-- if the "write sets" have a timestamp overlap, then the values are
-- consistent
all t: Timestamp, v, v': Value |
( (t -> v) in s.writePending && (t -> v') in s.writeSucceeded )
=> v = v'
-- all times in the defined set are in the past
all t: s.defined | lt [t, s.time]
}

pred GlobalConsistencyInvariant [s: SystemState] {
-- in general, these constraints cover all clients and all lockRefs, not
-- just the lockholding client and trueQptr
-- no current or future true timestamps
PastTimestamp [s.trueTimestamp, s]
-- no future messages or tasks
all m:
Client.(s.clientTask+s.clientInputs) + Replica.(s.repInputs+s.repTask) |
CurrentOrPastTimestamp [m.stamp, s]
-- no current or future data store writes
all t: (s.writePending + s.writeSucceeded).Value |
CurrentOrPastTimestamp [t, s]
-- if a client has a lockRef, and the true timestamp is in the same epoch,
-- then the true timestamp is in the past with respect to this epoch;
-- NOTE this is a subtle constraint, implying that whatever local clock is
-- being used, it can distinguish well enough between sequential actions
-- of the same client
all c: Client |
( some c.(s.clientRef) && s.trueTimestamp.ref = c.(s.clientRef) )
=> lt [s.trueTimestamp.tme, s.time]
-- same as above for datastore writes
all c: Client, t: (s.writePending + s.writeSucceeded).Value |
( some c.(s.clientRef) && t.ref = c.(s.clientRef) )
=> lt [t.tme, s.time]
-- if a client has a task, it is in the present or past with respect to
-- the client's epoch
all c: Client, m: c.(s.clientTask) | lte [m.stamp.tme, s.time]
-- if a client has a task, then all repInputs and repTasks with the same
-- lockRef have the same time or an earlier one
all c: Client, m: c.(s.clientTask),
m': Replica.(s.repInputs + s.repTask) |
m'.stamp.ref = m.stamp.ref => trace/lte [m'.stamp.tme, m.stamp.tme]
-- same as above for datastore writes
all c: Client, m: c.(s.clientTask), t: Timestamp |
( t in (s.writePending + s.writeSucceeded).Value
&& t.ref = m.stamp.ref )
=> lte [t.tme, m.stamp.tme]
-- if a client has a lockRef but no task, then all repInputs and repTasks
-- with the same lockRef are in the present or past
all c: Client, m: Replica.(s.repInputs + s.repTask) |
( some c.(s.clientRef) && no c.(s.clientTask)
&& m.stamp.ref = c.(s.clientRef) )
=> trace/lte [m.stamp.tme, s.time]
-- same as above for datastore writes
all c: Client, t: (s.writePending + s.writeSucceeded).Value |
( some c.(s.clientRef) && no c.(s.clientTask)
&& t.ref = c.(s.clientRef) )
=> trace/lte [t.tme, s.time]
-- across the global state, consistent pairings of timestamps and values
let msgPairings = { t: Timestamp, v: Value |
some m: ClientPutMsg + RepPutMsg |
( m in Client.(s.clientTask) + Replica.(s.repInputs + s.repTask)
&& t = m.stamp && v = m.val ) }|
all t: Timestamp |
lone t.( msgPairings + s.writePending + s.writeSucceeded
+ (s.trueTimestamp -> s.trueValue) )
-- all messages associated with a client have the client's lockref or one
-- earlier than the client's lockref, or the client has no lockref
all c: Client, m: Message |
( m in Replica.(s.repInputs + s.repTask) && m.cli = c )
=> ( m.stamp.ref = c.(s.clientRef)
|| queue/lt [m.stamp.ref, c.(s.clientRef)] || no c.(s.clientRef) )
-- if a client has a valid Nohold message in its input queue, then the
-- client is a past lockholder.
all c: Client, f: LockRef, m: ClientPutNohold + ClientGetNohold |
(f = c.(s.clientRef) && m in c.(s.clientInputs) && m.stamp.ref = f)
=> PastPtr [f, s]
}

pred SynchingInvariant [s: SystemState] {
-- if a client is in a pre-synching state, there should be no put messages
-- within the same epoch
all c: Client |
c.(s.clientState) in Enqueued + MustGet + SynchGetting
=> (all m: RepPutMsg | m in Replica.(s.repInputs + s.repTask)
=> m.stamp.ref != c.(s.clientRef) )
-- same as above for data store writes
all c: Client, t: (s.writePending + s.writeSucceeded).Value |
c.(s.clientState) in Enqueued + MustGet + SynchGetting
=> t.ref != c.(s.clientRef)
-- synch flag NEEDED if there is an active client with a past lockRef later
-- than or equal to that of the true timestamp
(some c: Client, f: LockRef | c.(s.clientRef) = f && PastPtr [f, s]
&& queue/lte [s.trueTimestamp.ref, f] )
=> s.synchFlag = True
-- synch flag NEEDED if there are old tasks in the system that could change
-- the key value
(some m: RepPutMsg |
m in Replica.(s.repInputs + s.repTask) && PastPtr [m.stamp.ref, s]
&& EarlierTimestamp [s.trueTimestamp, m.stamp] )
=> s.synchFlag = True
-- synch flag NEEDED if there is a true data timestamp later than the true
-- timestamp and not in the current epoch
( EarlierTimestamp [s.trueTimestamp, s.trueDataTimestamp]
&& s.trueDataTimestamp.ref != s.trueQptr )
=> s.synchFlag = True
-- if the synch flag is on and there is a lockholding client, it must be
-- synching
( s.synchFlag = True
&& (some c: Client | some s.trueQptr && c.(s.clientRef) = s.trueQptr) )
=> (all c: Client |
c.(s.clientRef) = s.trueQptr
=> c.(s.clientState) in
Enqueued+MustGet+SynchGetting+MustPut4Synch+SynchPutting )
-- if the synch flag is off, then the datastore is synched or the
-- lockholding client is putting or the lockholder has just failed and
-- there has been no forced release yet
s.synchFlag = False
=> ( ( DataStoreDefined [s]
&& s.trueDataTimestamp = s.trueTimestamp
&& s.trueDataValue = s.trueValue )
|| (some c: Client |
c.(s.clientRef) = s.trueQptr
&& c.(s.clientState) in MustPut+MustPut4Synch+SynchPutting+Putting
)
|| (some s.trueQptr && (no c: Client | c.(s.clientRef) = s.trueQptr))
)

}

pred LockHolderInvariant [s: SystemState] {
-- when the lockholder is pre-synching, the true timestamp is not in
-- current epoch
all c: Client |
( c.(s.clientRef) = s.trueQptr
&& c.(s.clientState) in
Enqueued+MustGet+SynchGetting+MustPut4Synch+SynchPutting )
=> queue/lt[(s.trueTimestamp).ref, s.trueQptr]
-- if lockholding client is in a non-putting state, there should be no put
-- messages more recent than the trueTimestamp
all c: Client, m: RepPutMsg & Replica.(s.repInputs + s.repTask) |
( c.(s.clientRef) = s.trueQptr
&& c.(s.clientState) in Critical + Getting
&& m.stamp.ref = c.(s.clientRef) )
=> EarlierOrEqualTimestamp [m.stamp, s.trueTimestamp]
-- same as above for data store writes
all c: Client, t: (s.writePending + s.writeSucceeded).Value |
( c.(s.clientRef) = s.trueQptr && t.ref = c.(s.clientRef)
&& c.(s.clientState) in Critical + Getting )
=> EarlierOrEqualTimestamp [t, s.trueTimestamp]
-- critical put correctness
all c: Client |
-- precondition of lockholder's AcceptPut
( c.(s.clientState) in SynchPutting + Putting
&& c.(s.clientRef) = s.trueQptr
&& c.(s.clientTask) in c.(s.clientInputs) )
-- data store is well-defined and correct
=> ( DataStoreDefined [s]
&& s.trueDataTimestamp = (c.(s.clientTask)).stamp
&& s.trueDataValue = (c.(s.clientTask)).val )
-- during getting, the datastore is continually defined
all c: Client |
( c.(s.clientRef) = s.trueQptr
&& c.(s.clientState) in Getting )
=> ( DataStoreDefined [s]
&& (all t: Time |
lte [(c.(s.clientTask)).stamp.tme, t] && lt [t, s.time]
=> t in s.defined ) )
-- critical get correctness
all c: Client, m: ClientGetAck |
-- precondition of lockholder's AcceptGet
( c.(s.clientState) in Getting
&& c.(s.clientRef) = s.trueQptr
&& m in c.(s.clientInputs) && m.rep = (c.(s.clientTask)).rep
&& m.stamp = (c.(s.clientTask)).stamp )
-- returned value is the true one
=> m.val = s.trueValue
-- synch getting correctness
all c: Client, m: ClientGetAck |
-- precondition of lockholder's AcceptGet
( c.(s.clientState) in SynchGetting
&& c.(s.clientRef) = s.trueQptr
&& m in c.(s.clientInputs) && m.rep = (c.(s.clientTask)).rep
&& m.stamp = (c.(s.clientTask)).stamp )
-- returned value is the true one, or a proper exceptional value
=> ( m.val = s.trueValue
|| ( s.synchFlag = True
&& ( some t: Timestamp |
EarlierTimestamp [s.trueTimestamp, t]
&& t.ref != s.trueQptr
&& t in (s.writePending + s.writeSucceeded).(m.val) ) )
)
}

pred SystemStateInvariant [s: SystemState] {
LockStoreInvariant [s]
ClientStateInvariant [s]
MusicStateInvariant [s]
DataStoreInvariant [s]
GlobalConsistencyInvariant [s]
SynchingInvariant [s]
LockHolderInvariant [s]
}
pred SystemStateInvariant2 [s: SystemState] {
LockStoreInvariant [s]
ClientStateInvariant [s]
MusicStateInvariant [s]
DataStoreInvariant [s]
GlobalConsistencyInvariant [s]
SynchingInvariant [s]
LockHolderInvariant [s]
}

fact SystemStateVariant { all disj s, s': SystemState | s.time != s'.time }

...

abstract sig TraceEvent extends Event { prest, postst: SystemState }

abstract sig LockstoreEvent extends TraceEvent {
disj rep0, rep1, rep2: Replica }

abstract sig ClientEvent extends TraceEvent { client: Client }

abstract sig MusicEvent extends TraceEvent { replica: Replica }

...

pred LockstoreClientFrame [s, s': SystemState] {
s'.clientTask = s.clientTask
s'.trueTimestamp = s.trueTimestamp && s'.trueValue = s.trueValue
s'.repState = s.repState && s'.repTask = s.repTask
s'.repInputs = s.repInputs
s'.writePending = s.writePending && s'.writeSucceeded = s.writeSucceeded
}

pred LockstoreOnlyFrame [s, s': SystemState] {
LockstoreClientFrame [s, s']
s'.clientInputs = s.clientInputs
s'.clientRef = s.clientRef && s'.clientState = s.clientState }

sig EnqueueClient extends LockstoreEvent {liveClient:Client,newRef:LockRef}
fact EnqueueClientEvent {
all e: EnqueueClient, s: e.prest, s': e.postst,
r0: e.rep0, r1: e.rep1, r2: e.rep2, c: e.liveClient, f: e.newRef | {
s.time = e.pre && s'.time = e.post
-- preconditions
c.(s.clientState) = Live
-- there is an unused lockRef; constraint in model only
f ! in s.trueQset
-- postconditions
-- change queue store
f = queue/min [LockRef - s.trueQset]
s'.trueQset = s.trueQset + f
s'.Qset = (Replica - (r0 + r1 + r2)) <: (s.Qset)
+ (r0 -> s'.trueQset) + (r1 -> s'.trueQset) + (r2 -> s'.trueQset)
(no s.trueQptr => s'.trueQptr = f else s'.trueQptr = s.trueQptr)
s'.Qptr = (Replica - (r0 + r1 + r2)) <: (s.Qptr)
+ (r0 -> s'.trueQptr) + (r1 -> s'.trueQptr) + (r2 -> s'.trueQptr)
s'.synchFlag = s.synchFlag
s'.trueDataSynchFlag = s.trueDataSynchFlag
-- client update
s'.clientState = s.clientState ++ (c -> Enqueued)
s'.clientRef = s.clientRef ++ (c -> f)
s'.clientInputs = s.clientInputs
LockstoreClientFrame [s, s']
} }
/* The possibility that the client requests EnqueueClient then dies before
receiving the lockRef is not modeled. It is exactly the same as if the
client received the lockRef and then died immediately after. */

sig ReleaseLock extends LockstoreEvent { lockClient: Client }
fact ReleaseLockEvent {
all e: ReleaseLock, s: e.prest, s': e.postst,
r0: e.rep0, r1: e.rep1, r2: e.rep2, c: e.lockClient | {
s.time = e.pre && s'.time = e.post
-- preconditions
c.(s.clientState) = Critical
-- postconditions
-- change queue store
let lockRef = c.(s.clientRef) |
( s'.trueQset = s.trueQset
&& s'.Qset = (Replica - (r0 + r1 + r2)) <: (s.Qset)
+ (r0 -> s'.trueQset) + (r1 -> s'.trueQset) + (r2 -> s'.trueQset)
&& (s.trueQptr = lockRef
=> s'.trueQptr = (queue/next [s.trueQptr] & s.trueQset)
else s'.trueQptr = s.trueQptr )
&& s'.Qptr = (Replica - (r0 + r1 + r2)) <: (s.Qptr)
+ (r0 -> s'.trueQptr) + (r1 -> s'.trueQptr) + (r2 -> s'.trueQptr)
&& s'.synchFlag = s.synchFlag -- if client is the lockholder
-- and client has already synched, flag will already be false
)
s'.trueDataSynchFlag = s.trueDataSynchFlag
-- client update
s'.clientState = s.clientState ++ (c -> Live)
s'.clientRef = (Client - c) <: s.clientRef
s'.clientInputs = (Client - c) <: s.clientInputs
LockstoreClientFrame [s, s']
} }

sig ForcedRelease extends LockstoreEvent { releaseRef: LockRef }
fact ForcedReleaseEvent {
all e:ForcedRelease, s:e.prest, s':e.postst,
r0: e.rep0, r1: e.rep1, r2: e.rep2, f:e.releaseRef | {
s.time = e.pre && s'.time = e.post
-- preconditions
r0.(s.repState) = Started && no r0.(s.repTask)
r0.(s.Qptr) = f
-- postconditions, lockRef may be current or past holder
s.trueQptr = f
-- case 1: preempting the lockHolder
=> s'.trueQptr = (queue/next [s.trueQptr] & s.trueQset)
-- case 2: not preempting the lockHolder
else s'.trueQptr = s.trueQptr
-- lockstore update, both cases
s'.Qset = (Replica - (r0 + r1 + r2)) <: s.Qset
+ (r0 -> s'.trueQset) + (r1 -> s'.trueQset) + (r2 -> s'.trueQset)
s'.Qptr = (Replica - (r0 + r1 + r2)) <: (s.Qptr)
+ (r0 -> s'.trueQptr) + (r1 -> s'.trueQptr) + (r2 -> s'.trueQptr)
s'.trueQset = s.trueQset
-- setting the synch flag
f = s.trueQptr
=> s'.synchFlag = True else s'.synchFlag = s.synchFlag
-- flag may already be true, if lockholder never synched
-- f may be current or past lockholder, but regardless, MUSIC replica
-- will attempt to set synch flag using lockRef + delta
f = s.trueQptr -- f is current lockholder; this will
=> s'.trueDataSynchFlag = True -- over-ride any concurrent synch
else -- f is past lockholder
(s.synchFlag = True
=> -- there was a previous forced release, no real change
s'.trueDataSynchFlag = True
else -- there was a previous release when synched,
s'.trueDataSynchFlag = True -- but false gets over-written
-- by true anyway
)
LockstoreOnlyFrame [s, s']
} }

sig PropagateLockstore extends LockstoreEvent { }
fact PropagateLockstoreEvent {
all e:PropagateLockstore, s:e.prest,s':e.postst, r0:e.rep0,r1:e.rep1 | {
s.time = e.pre && s'.time = e.post
-- precondition
PastQueue [r0.(s.Qset), r0.(s.Qptr), r1.(s.Qset), r1.(s.Qptr)]
-- postconditions
(Replica - r0) <: s'.Qptr = (Replica - r0) <: s.Qptr
r0.(s'.Qptr) = r1.(s.Qptr)
(Replica - r0) <: s'.Qset = (Replica - r0) <: s.Qset
r0.(s'.Qset) = r1.(s.Qset)
s'.trueQset = s.trueQset && s'.trueQptr = s.trueQptr
s'.synchFlag = s.synchFlag
s'.trueDataSynchFlag = s.trueDataSynchFlag
LockstoreOnlyFrame [s, s']
} }

...

pred ClientMusicFrame [s, s': SystemState] {
s'.Qset = s.Qset && s'.Qptr = s.Qptr
s'.trueQset = s.trueQset && s'.trueQptr = s.trueQptr
s'.synchFlag = s.synchFlag
s'.trueDataSynchFlag = s.trueDataSynchFlag
s'.repState = s.repState && s'.repTask = s.repTask
s'.writePending = s.writePending && s'.writeSucceeded = s.writeSucceeded
}

pred ClientLockstoreFrame [s, s': SystemState] {
s'.Qset = s.Qset && s'.Qptr = s.Qptr
s'.trueQset = s.trueQset && s'.trueQptr = s.trueQptr
s'.repInputs = s.repInputs
s'.repState = s.repState && s'.repTask = s.repTask
s'.writePending = s.writePending && s'.writeSucceeded = s.writeSucceeded
}

pred ClientOnlyFrame [s, s': SystemState] {
ClientMusicFrame [s, s'] && s'.repInputs = s.repInputs }

sig AcquireLock extends ClientEvent { helperRep: Replica }
fact AcquireLockEvent {
all e:AcquireLock, s:e.prest, s':e.postst, c:e.client, r: e.helperRep |{
s.time = e.pre && s'.time = e.post
-- preconditions
c.(s.clientState) = Enqueued -- "you're not lockholder" reply omitted
no r.(s.repTask)
r.(s.Qptr) = c.(s.clientRef)
-- decision whether to synch the data store -- see footnote
( ( s.trueDataSynchFlag = False
&& s'.clientState = s.clientState ++ (c -> Critical) )
|| s'.clientState = s.clientState ++ (c -> MustGet)
)
-- other postconditions
s'.clientRef = s.clientRef
s'.clientTask = s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs -- trash cleanup
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }
/* This event is atomic because it is only a model of the part of the real
operation that checks the local lock store. If necessary,
synchronization begins with the MustGet state.
For this code to be valid, it must be the case that:
"quorum read of dataSynchFlag = False" => trueDataSynchFlag = False,
because the implementation is doing the quorum read.
For the implication above to be valid, any "quorum write true" since
the previous "quorum write false" must have been completed (is not still
ongoing). Note that "quorum write true" is performed by ForcedRelease,
while "quorum write false" is performed by AcceptPut.
In the implementation, the ForcedReleaser completes the quorum write
before changing the lockstore. So the quorum write must be complete
before the lock is release, if it is in fact released (the
ForcedReleaser might fail before completing the step). */

sig RequestPut extends ClientEvent { requestRep: Replica,
msg: RepPutMsg, msg': ClientPutAck, ts: Timestamp, value: Value }
-- if client is the lock holder, sets true timestamp but not true value
fact RequestPutEvent {
all e:RequestPut, s:e.prest, s':e.postst, c:e.client, r:e.requestRep,
m: e.msg, m': e.msg', t: e.ts, v: e.value | {
s.time = e.pre && s'.time = e.post
-- preconditions, these are constraints on client's behavior
c.(s.clientState) in Critical + MustPut + MustPut4Synch
-- postconditions
s'.clientRef = s.clientRef
c.(s.clientState) = MustPut4Synch
=> s'.clientState = s.clientState ++ (c -> SynchPutting)
else s'.clientState = s.clientState ++ (c -> Putting)
s'.clientInputs = (Client - c) <: s.clientInputs -- trash cleanup
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
m.cli = c && m'.rep = r
t.ref = c.(s.clientRef) && t.tme = s'.time
m.stamp = t && m'.stamp = t
c.(s.clientState) in Critical
=> (m.val = v && m'.val = m.val)
else (m.val = (c.(s.clientTask)).val && m'.val = m.val)
s'.clientTask = s.clientTask ++ (c -> m')
( s'.repInputs = s.repInputs + (r -> m)
|| s'.repInputs = s.repInputs ) -- if message lost
ClientMusicFrame [s, s']
} }

sig AcceptPut extends ClientEvent { }
fact AcceptPutEvent {
all e:AcceptPut, s:e.prest, s':e.postst, c:e.client | {
s.time = e.pre && s'.time = e.post
-- preconditions, these are constraints on client's behavior
c.(s.clientState) in SynchPutting + Putting
c.(s.clientTask) in c.(s.clientInputs)
-- postconditions
s'.clientRef = s.clientRef
s'.clientState = s.clientState ++ (c -> Critical)
s'.clientTask = (Client - c) <: s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs
c.(s.clientRef) = s.trueQptr
=> ( s'.trueTimestamp = (c.(s.clientTask)).stamp
&& s'.trueValue = (c.(s.clientTask)).val )
else ( s'.trueTimestamp = s.trueTimestamp
&& s'.trueValue = s.trueValue )
(c.(s.clientRef) = s.trueQptr && c.(s.clientState) = SynchPutting)
=> s'.synchFlag = False
else s'.synchFlag = s.synchFlag
c.(s.clientState) = SynchPutting
=> (c.(s.clientRef) = s.trueQptr
=> s'.trueDataSynchFlag = False
else-- client will do a reset, but if it is not actually the
-- lockholder, the flag's timestamp will already be later
s'.trueDataSynchFlag = s.trueDataSynchFlag
)
else s'.trueDataSynchFlag = s.trueDataSynchFlag
ClientLockstoreFrame [s, s']
} }

sig PutAborts extends ClientEvent { }
fact PutAbortsEvent {
all e:PutAborts, s:e.prest, s':e.postst, c: e.client | {
s.time = e.pre && s'.time = e.post
-- preconditions
c.(s.clientState) in Putting + SynchPutting
-- postconditions
s'.clientRef = s.clientRef
c.(s.clientState) = SynchPutting
=> s'.clientState = s.clientState ++ (c -> MustPut4Synch)
else s'.clientState = s.clientState ++ (c -> MustPut)
s'.clientTask = s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs
-- there could have been a proper nack in here;
-- there could have been an ack or nack that was lost in transit!
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }

sig PutRevealsNotHolder extends ClientEvent { msg: ClientPutNohold }
fact PutRevealsNotHolderEvent {
all e:PutRevealsNotHolder,s:e.prest,s':e.postst,c:e.client,m:e.msg | {
s.time = e.pre && s'.time = e.post
-- preconditions, these are constraints on client's behavior
c.(s.clientState) in Putting + SynchPutting
m in c.(s.clientInputs)
m.stamp = (c.(s.clientTask)).stamp
-- postconditions
s'.clientRef = (Client - c) <: s.clientRef
s'.clientState = s.clientState ++ (c -> Live)
s'.clientTask = (Client - c) <: s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }

sig RequestGet extends ClientEvent { requestRep: Replica,
msg: RepGetMsg, msg': ClientGetAck, ts: Timestamp }
fact RequestGetEvent {
all e:RequestGet, s:e.prest, s':e.postst, c:e.client, r:e.requestRep,
m: e.msg, m': e.msg', t: e.ts | {
s.time = e.pre && s'.time = e.post
-- preconditions, these are constraints on client's behavior
c.(s.clientState) in Critical + MustGet
-- postconditions
s'.clientRef = s.clientRef
( c.(s.clientState) in MustGet
=> s'.clientState = s.clientState ++ (c -> SynchGetting)
else s'.clientState = s.clientState ++ (c -> Getting) )
s'.clientInputs = (Client - c) <: s.clientInputs -- trash cleanup
s'.trueValue = s.trueValue
s'.trueTimestamp = s.trueTimestamp
m.cli = c && m'.rep = r
t.ref = c.(s.clientRef) && t.tme = s'.time
m.stamp = t && m'.stamp = t
s'.clientTask = s.clientTask ++ (c -> m')
( s'.repInputs = s.repInputs + (r -> m)
|| s'.repInputs = s.repInputs ) -- if message lost
ClientMusicFrame [s, s']
} }

sig AcceptGet extends ClientEvent {
msg: ClientGetAck, msg': ClientPutAck, ts: Timestamp }
fact AcceptGetEvent {
all e: AcceptGet, s: e.prest, s': e.postst, c: e.client,
m: e.msg, m': e.msg', t: e.ts | {
s.time = e.pre && s'.time = e.post
-- preconditions, these are constraints on client's behavior
c.(s.clientState) in SynchGetting + Getting
m in c.(s.clientInputs)
m.rep = (c.(s.clientTask)).rep && m.stamp = (c.(s.clientTask)).stamp
-- postconditions
s'.clientRef = s.clientRef
( c.(s.clientState) in SynchGetting
=> s'.clientState = s.clientState ++ (c -> MustPut4Synch)
else s'.clientState = s.clientState ++ (c -> Critical) )
( c.(s.clientState) in SynchGetting
=> ( t.ref = c.(s.clientRef) && t.tme = s'.time
&& m'.stamp = t && m'.val = m.val
&& s'.clientTask = s.clientTask ++ (c -> m') )
else s'.clientTask = (Client - c) <: s.clientTask )
s'.clientInputs = (Client - c) <: s.clientInputs
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }

sig GetAborts extends ClientEvent { }
fact GetAbortsEvent {
all e:GetAborts, s:e.prest, s':e.postst, c: e.client | {
s.time = e.pre && s'.time = e.post
-- preconditions
c.(s.clientState) in SynchGetting + Getting
-- postconditions
s'.clientRef = s.clientRef
( c.(s.clientState) in SynchGetting
=> s'.clientState = s.clientState ++ (c -> MustGet)
else s'.clientState = s.clientState ++ (c -> Critical) )
s'.clientTask = (Client - c) <: s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs
-- there could have been a proper nack in here;
-- there could have been an ack or nack that was lost in transit!
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }

sig GetRevealsNotHolder extends ClientEvent { msg: ClientGetNohold }
fact GetRevealsNotHolderEvent {
all e:GetRevealsNotHolder, s:e.prest,s':e.postst,c:e.client,m:e.msg | {
s.time = e.pre && s'.time = e.post
-- preconditions, these are constraints on client's behavior
c.(s.clientState) in SynchGetting + Getting
m in c.(s.clientInputs)
m.stamp = (c.(s.clientTask)).stamp
-- postconditions
s'.clientRef = (Client - c) <: s.clientRef
s'.clientState = s.clientState ++ (c -> Live)
s'.clientTask = (Client - c) <: s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }

sig ClientFailsOrRestarts extends ClientEvent { }
fact ClientFailsOrRestartsEvent {
all e:ClientFailsOrRestarts, s:e.prest, s':e.postst, c: e.client | {
s.time = e.pre && s'.time = e.post
-- preconditions
-- postconditions
s'.clientRef = (Client - c) <: s.clientRef
c.(s.clientState) != Dead
=> s'.clientState = s.clientState ++ (c -> Dead)
else s'.clientState = s.clientState ++ (c -> Live)
s'.clientTask = (Client - c) <: s.clientTask
s'.clientInputs = (Client - c) <: s.clientInputs
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
ClientOnlyFrame [s, s']
} }

MUSIC OPERATIONS

...

pred MusicClientFrame [s, s': SystemState] {
s'.Qset = s.Qset && s'.Qptr = s.Qptr
s'.trueQset = s.trueQset && s'.trueQptr = s.trueQptr
s'.clientRef = s.clientRef && s'.clientState = s.clientState
s'.clientTask = s.clientTask
s'.trueTimestamp = s.trueTimestamp
s'.trueValue = s.trueValue
s'.synchFlag = s.synchFlag
s'.trueDataSynchFlag = s.trueDataSynchFlag }

pred MusicOnlyFrame [s, s': SystemState] {
MusicClientFrame [s, s'] && s'.clientInputs = s.clientInputs }

sig RequestWrite extends MusicEvent {msg: RepPutMsg, msg': ClientPutNohold}
fact RequestWriteEvent {
all e: RequestWrite, s: e.prest, s': e.postst, r: e.replica,
m: e.msg, m': e.msg' | {
s.time = e.pre && s'.time = e.post
-- preconditions
r.(s.repState) = Started
no r.(s.repTask)
m in r.(s.repInputs)
-- postconditions
queue/lt [m.stamp.ref, r.(s.Qptr)] => -- past lockholder
( s'.repTask = s.repTask
&& s'.writePending = s.writePending
&& m'.rep = r && m'.stamp = m.stamp
&& s'.clientInputs = s.clientInputs + (m.cli -> m') )
else -- normal case
( s'.repTask = s.repTask + (r -> m)
&& s'.writePending = s.writePending + (m.stamp -> m.val)
&& s'.clientInputs = s.clientInputs )
s'.repState = s.repState
s'.repInputs = s.repInputs - (r -> m)
s'.writeSucceeded = s.writeSucceeded
MusicClientFrame [s, s']
} }

sig AcceptWrite extends MusicEvent { msg: ClientPutAck }
fact AcceptWriteEvent {
all e: AcceptWrite, r: e.replica, s: e.prest, s':e.postst, m: e.msg | {
s.time = e.pre && s'.time = e.post
-- precondition, invariant says there is a matching writePending
some (RepPutMsg & r.(s.repTask))
-- postconditions, based on datastore specification
s'.repInputs = s.repInputs
s'.repState = s.repState
s'.repTask = (Replica - r) <: s.repTask
let t = (r.(s.repTask)).stamp | let v = t.(s.writePending) |
( s'.writePending = s.writePending - (t -> v)
&& s'.writeSucceeded = s.writeSucceeded + (t -> v)
&& m.rep = r && m.stamp = t && m.val = v
&& s'.clientInputs = s.clientInputs + ((r.(s.repTask)).cli -> m) )
MusicClientFrame [s, s']
} }

sig WriteFails extends MusicEvent { msg: ClientPutNack }
fact WriteFailsEvent {
all e: WriteFails, r: e.replica, s: e.prest, s':e.postst, m: e.msg | {
s.time = e.pre && s'.time = e.post
-- precondition, invariant says there is a matching writePending
some (RepPutMsg & r.(s.repTask))
-- postconditions
s'.repInputs = s.repInputs
s'.repState = s.repState
s'.repTask = (Replica - r) <: s.repTask
let t = (r.(s.repTask)).stamp | let v = t.(s.writePending) |
( m.rep = r && m.stamp = t && m.val = v
&& s'.clientInputs = s.clientInputs + ((r.(s.repTask)).cli -> m) )
s'.writePending = s.writePending
s'.writeSucceeded = s.writeSucceeded
MusicClientFrame [s, s']
} }

sig RequestRead extends MusicEvent { msg: RepGetMsg, msg': ClientGetNohold}
fact RequestReadEvent {
all e:RequestRead,r:e.replica,s:e.prest,s':e.postst,m:e.msg,m':e.msg'| {
s.time = e.pre && s'.time = e.post
-- preconditions
r.(s.repState) = Started
no r.(s.repTask)
m in r.(s.repInputs)
-- postconditions
queue/lt [m.stamp.ref, r.(s.Qptr)] => -- past lockholder
( s'.repTask = s.repTask
&& m'.rep = r && m'.stamp = m.stamp
&& s'.clientInputs = s.clientInputs + (m.cli -> m') )
else -- normal case
( s'.repTask = s.repTask + (r -> m)
&& s'.clientInputs = s.clientInputs )
s'.repState = s.repState
s'.repInputs = s.repInputs - (r -> m)
s'.writePending = s.writePending
s'.writeSucceeded = s.writeSucceeded
MusicClientFrame [s, s']
} }

sig AcceptRead extends MusicEvent { msg: ClientGetAck, ts: Timestamp }
fact AcceptReadEvent {
all e:AcceptRead,s:e.prest,s':e.postst, r:e.replica, m:e.msg, t:e.ts | {
s.time = e.pre && s'.time = e.post
-- preconditions
some (RepGetMsg & r.(s.repTask))
-- postconditions, based on datastore specification
s'.repInputs = s.repInputs
s'.repState = s.repState
s'.repTask = (Replica - r) <: s.repTask
m.rep = r && m.stamp = (r.(s.repTask)).stamp
-- specification of read value
-- if the datastore has been defined continually in the past since the
-- read request
( ( all tw: Time |
lte [(r.(s.repTask)).stamp.tme, tw]
&& lt [tw, s.time] => tw in s.defined )
-- and if the datastore is defined now
&& DataStoreDefined [s] )
-- then the read value is the true data value
=> m.val = s.trueDataValue
-- in all cases the read value is in the datastore, and its timestamp
-- is no earlier than the trueTimestamp!
(t -> m.val) in (s.writePending + s.writeSucceeded)
! EarlierTimestamp [t, s.trueTimestamp]
s'.clientInputs = s.clientInputs + ((r.(s.repTask)).cli -> m)
s'.writePending = s.writePending
s'.writeSucceeded = s.writeSucceeded
MusicClientFrame [s, s']
} }
-- Note: The true value of the data store cannot change without going
-- through at least one state in which the data store is not defined;
-- this is the state in which the newest write is pending but not
-- succeeded. So there is no possibility that, in the specified case, the
-- true value changed during the reading period.

sig ReadFails extends MusicEvent { msg: ClientGetNack }
-- In this event, data store reports failure to the waiting Music replica,
-- or the waiting replica times out the request (correctly or not); if the
-- data store replies subsequently, the reply is ignored
fact ReadFailsEvent {
all e: ReadFails, r: e.replica, s: e.prest, s':e.postst, m: e.msg| {
s.time = e.pre && s'.time = e.post
-- preconditions
some (RepGetMsg & r.(s.repTask))
-- postconditions
s'.repInputs = s.repInputs
s'.repState = s.repState
s'.repTask = (Replica - r) <: s.repTask
m.rep = r && m.stamp = (r.(s.repTask)).stamp
s'.clientInputs = s.clientInputs + ((r.(s.repTask)).cli -> m)
s'.writePending = s.writePending
s'.writeSucceeded = s.writeSucceeded
MusicClientFrame [s, s']
} }

sig MusicFailsOrRestarts extends MusicEvent { }
fact MusicFailsOrRestartsEvent {
all e:MusicFailsOrRestarts, r:e.replica, s:e.prest, s':e.postst | {
s.time = e.pre && s'.time = e.post
-- preconditions
-- postconditions
s'.repInputs = (Replica - r) <: s.repInputs
r.(s.repState) = Started
=> s'.repState = s.repState ++ (r -> Failed)
else s'.repState = s.repState ++ (r -> Started)
s'.repTask = (Replica - r) <: s.repTask
s'.writePending = s.writePending
s'.writeSucceeded = s.writeSucceeded
MusicOnlyFrame [s, s']
} }

VALIDATION AND VERIFICATION

[x SystemState, x+2 Time, x+1 Event]

good exploratory scope, used for debugging:
default scope allows 2 SystemStates but
4 Time, 3 Event, 2 Client, 5 Replica, 5 Message, 5 Timestamp, 4 LockRef,
2 Value, 11 ClientState, 2 ReplicaState
also checked this expanded scope:
default scope allows 2 SystemStates but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState
Note that once the exploratory scope checked out, expanding the scope
revealed no new bugs.
======================================================================== */

pred IsInitialState [s: SystemState] { InitialState [s] }
run IsInitialState for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert InitialStateSatisfiesInvariant { all s: SystemState |
InitialState [s] => SystemStateInvariant2 [s] }
check InitialStateSatisfiesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsEnqueueClient [e: EnqueueClient] { SystemStateInvariant [e.prest] }
run IsEnqueueClient for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert EnqueueClientPreservesInvariant { all e: EnqueueClient |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check EnqueueClientPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsReleaseLock [e: ReleaseLock] { SystemStateInvariant [e.prest] }
run IsReleaseLock for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert ReleaseLockPreservesInvariant { all e: ReleaseLock |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check ReleaseLockPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsForcedRelease [e: ForcedRelease] { SystemStateInvariant [e.prest] }
run IsForcedRelease for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert ForcedReleasePreservesInvariant { all e: ReleaseLock |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check ForcedReleasePreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsPropagateLockstore [e: PropagateLockstore] {
SystemStateInvariant [e.prest] }
run IsPropagateLockstore for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert PropagateLockstorePreservesInvariant { all e: PropagateLockstore |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check PropagateLockstorePreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsAcquireLock [e: AcquireLock] { SystemStateInvariant [e.prest] }
run IsAcquireLock for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert AcquireLockPreservesInvariant { all e: AcquireLock |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check AcquireLockPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsRequestPut [e: RequestPut] { SystemStateInvariant [e.prest] }
run IsRequestPut for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert RequestPutPreservesInvariant { all e: RequestPut |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check RequestPutPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsAcceptPut [e: AcceptPut] { SystemStateInvariant [e.prest] }
run IsAcceptPut for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert AcceptPutPreservesInvariant { all e: AcceptPut |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check AcceptPutPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsPutAborts [e: PutAborts] { SystemStateInvariant [e.prest] }
run IsPutAborts for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert PutAbortsPreservesInvariant { all e: PutAborts |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check PutAbortsPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsPutRevealsNotHolder [e: PutRevealsNotHolder]
{ SystemStateInvariant [e.prest] }
run IsPutRevealsNotHolder for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert PutRevealsNotHolderPreservesInvariant { all e: PutRevealsNotHolder |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check PutRevealsNotHolderPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsRequestGet [e: RequestGet] { SystemStateInvariant [e.prest] }
run IsRequestGet for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert RequestGetPreservesInvariant { all e: RequestGet |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check RequestGetPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsAcceptGet [e: AcceptGet] { SystemStateInvariant [e.prest] }
run IsAcceptGet for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert AcceptGetPreservesInvariant { all e: AcceptGet |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check AcceptGetPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsGetAborts [e: GetAborts] { SystemStateInvariant[e.prest] }
run IsGetAborts for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert GetAbortsPreservesInvariant { all e: GetAborts |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check GetAbortsPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsGetRevealsNotHolder [e: GetRevealsNotHolder]
{ SystemStateInvariant [e.prest] }
run IsGetRevealsNotHolder for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert GetRevealsNotHolderPreservesInvariant { all e: GetRevealsNotHolder |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check GetRevealsNotHolderPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsClientFailsOrRestarts [e: ClientFailsOrRestarts]
{ SystemStateInvariant [e.prest] }
run IsClientFailsOrRestarts for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert ClientFailsOrRestartsPreservesInvariant {
all e: ClientFailsOrRestarts |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check ClientFailsOrRestartsPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsRequestWrite [e: RequestWrite]
{ SystemStateInvariant [e.prest] }
run IsRequestWrite for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert RequestWritePreservesInvariant { all e: RequestWrite |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check RequestWritePreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsAcceptWrite [e: AcceptWrite] { SystemStateInvariant [e.prest] }
run IsAcceptWrite for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert AcceptWritePreservesInvariant { all e: AcceptWrite |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check AcceptWritePreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsWriteFails [e: WriteFails] { SystemStateInvariant [e.prest] }
run IsWriteFails for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert WriteFailsPreservesInvariant { all e: WriteFails |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check WriteFailsPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsRequestRead [e: RequestRead]
{ SystemStateInvariant [e.prest] }
run IsRequestRead for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert RequestReadPreservesInvariant { all e: RequestRead |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check RequestReadPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsAcceptRead [e: AcceptRead] { SystemStateInvariant [e.prest] }
run IsAcceptRead for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert AcceptReadPreservesInvariant { all e: AcceptRead |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check AcceptReadPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsReadFails [e: ReadFails] { SystemStateInvariant [e.prest] }
run IsReadFails for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert ReadFailsPreservesInvariant { all e: ReadFails |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check ReadFailsPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

pred IsMusicFailsOrRestarts [e: MusicFailsOrRestarts]
{ SystemStateInvariant [e.prest] }
run IsMusicFailsOrRestarts for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState

assert MusicFailsOrRestartsPreservesInvariant {
all e: MusicFailsOrRestarts |
SystemStateInvariant [e.prest] => SystemStateInvariant2 [e.postst] }
check MusicFailsOrRestartsPreservesInvariant for 2 but
4 Time, 3 Event, 3 Client, 5 Replica, 6 Message, 7 Timestamp, 5 LockRef,
3 Value, 11 ClientState, 2 ReplicaState