--- Token ring mutex protocol. --- Each process loops. Basically, the local states --- beforeCS and afterCS have been replaced with a single state --- outsideCS. load model-checker load full-maude (omod MESSAGE-WRAPPER is sort MsgContent . --- message content, application-specific op msg_from_to_ : MsgContent Oid Oid -> Msg [ctor] . endom) (omod TOKEN-RING-MUTEX is including MESSAGE-WRAPPER . class Node | state : MutexState, next : Oid . sort MutexState . ops outsideCS enteringCS insideCS : -> MutexState [ctor] . *** change --- message types: ops token : -> MsgContent [ctor] . vars O O' O'' : Oid . --- Try to enter into critical section: rl [wantToEnterCS] : < O : Node | state : outsideCS > => < O : Node | state : enteringCS > . rl [getToken1] : (msg token from O to O') < O' : Node | state : outsideCS, next : O'' > => < O' : Node | > (msg token from O' to O'') . rl [getToken2] : (msg token from O to O') < O' : Node | state : enteringCS > => < O' : Node | state : insideCS > . --- Exit critical section and pass on token: rl [exitCS] : < O : Node | state : insideCS, next : O' > => < O : Node | state : outsideCS > (msg token from O to O') . endom) --- Initial state: (omod TOKEN-RING-MUTEX-INITIAL-STATE is including TOKEN-RING-MUTEX . --- node names n1 n2 n3 n4 n5 ops n1 n2 n3 n4 n5 : -> Oid [ctor] . op init : -> Configuration . eq init = (msg token from n5 to n1) *** don't forget intial token! < n1 : Node | state : outsideCS, next : n2 > < n2 : Node | state : outsideCS, next : n3 > < n3 : Node | state : outsideCS, next : n4 > < n4 : Node | state : outsideCS, next : n5 > < n5 : Node | state : outsideCS, next : n1 > . endom) (rew [100] init .) (search [1] init =>* REST:Configuration < O1:Oid : Node | state : insideCS > < O2:Oid : Node | state : insideCS > .) --- Deadlock: (search [1] init =>! C:Configuration .) --- test: three in different stages: (search [1] init =>* REST:Configuration < O1:Oid : Node | state : insideCS > < O3:Oid : Node | state : outsideCS > < O2:Oid : Node | state : enteringCS > .) (omod MODEL-CHECK-TOKEN-RING-MUTEX is including MODEL-CHECKER . including TOKEN-RING-MUTEX-INITIAL-STATE . subsort Configuration < State . op _inState_ : Oid MutexState -> Prop [ctor] . var O : Oid . var REST : Configuration . var MS : MutexState . eq REST < O : Node | state : MS > |= O inState MS = true . --- justice fairness w.r.t. first rule needed: op justiceRule1 : Oid -> Formula . eq justiceRule1(O) = (<> [] (O inState outsideCS)) -> ([] <> (O inState enteringCS)) . op justiceRule1 : -> Formula . eq justiceRule1 = justiceRule1(n1) /\ justiceRule1(n2) /\ justiceRule1(n3) /\ justiceRule1(n4) /\ justiceRule1(n5) . endom) (red modelCheck(init, justiceRule1 -> ([] <> (n1 inState insideCS) /\ [] <> (n2 inState insideCS) /\ [] <> (n3 inState insideCS) /\ [] <> (n4 inState insideCS) /\ [] <> (n5 inState insideCS))) .)