token-mutex.maude

--- modified from "All about Maude," p390.

fmod NUMBER is
  sorts Number . 
  op 0 : -> Number [ctor] .
  op s : -> Number [ctor] .
  op __ : Number Number -> Number [ctor comm assoc id: 0] .
endfm


fmod TOKEN-CONF is
  protecting NUMBER .
  sorts Token Mode ModeWait .
  subsorts ModeWait < Mode .
  op {_} : Number -> Token [ctor] . 
  op crit : -> Mode [ctor] . 
  op wait : -> ModeWait [ctor] . 

  sorts Proc ProcWait .
  subsort ProcWait < Proc .
  op [_,_] : Number Mode -> Proc [ctor] . 
  op [_,_] : Number ModeWait -> ProcWait [ctor] . 

  sort Conf ConfTWait ConfWait .
  subsort Proc < Conf . 
  subsort Token < ConfTWait .
  subsorts ProcWait < ConfWait < ConfTWait < Conf .
  op none : -> ConfWait [ctor] . 
  op __ : Conf Conf -> Conf [ctor comm assoc id: none] . 
  op __ : ConfWait ConfWait -> ConfWait [ctor ditto] . 
  op __ : ConfTWait ConfTWait -> ConfTWait [ctor ditto] . 
endfm


mod TOKEN-MUTEX is 
  pr TOKEN-CONF .

  sort Top .
  op <_,_> : Number Conf -> Top .

  vars N M : Number . var CF : Conf .

  rl [enter] : <   s N M,   {M} [M, wait] CF > 
            => <   s N M,       [M, crit] CF > [narrowing] . 
  rl [exit1] : < s s N M,       [M, crit] CF >
            => < s s N M, {s M} [M, wait] CF > [narrowing] . 
  rl [exit2] : <     s M,       [M, crit] CF >
            => <     s M,   {0} [M, wait] CF > [narrowing] . 
endm


load symbolic-checker

(mod TOKEN-MUTEX-SATISFACTION is
  pr TOKEN-MUTEX .
  pr SYMBOLIC-CHECKER .

  subsort Top < State .

  op mutex : -> Prop .

  vars N M M' : Number .  
  var CF : Conf .  var WF : ConfWait . var WTF : ConfTWait .

  eq < N, WTF > |= mutex = true [variant] .
  eq < N, WTF [M,crit] > |= mutex = true [variant] .
  eq < N, CF [M,crit] [M',crit] > |= mutex = false [variant] .
endm)


--- true: one token
(lfmc < N, {M} WF > |= [] mutex .)


--- false: more than one token: 
(lfmc < N, WTF > |= [] mutex .)