rw.maude

--- The readers-writers problem in Maude
--- From: All About Maude - A High-Performance Logical Framework.
mod READERS-WRITERS is 
  sort Natural . 
  op 0 : -> Natural [ctor] . 
  op s : Natural -> Natural [ctor] .  
  sort Config . 
  op <_,_> : Natural Natural -> Config [ctor] .

  vars R W : Natural .

  rl [enter-w] : < 0, 0 > => < 0, s(0) > [narrowing] . 
  rl [leave-w] : < R, s(W) > => < R, W > [narrowing] . 
  rl [enter-r] : < R, 0 > => < s(R), 0 > [narrowing] . 
  rl [leave-r] : < s(R), W > => < R, W > [narrowing] .
endm

load symbolic-checker

(mod READERS-WRITERS-PROPS is
  pr READERS-WRITERS .
  pr SYMBOLIC-CHECKER .

  subsort Config < State .

  vars N M : Natural .

  op reads : -> Prop .
  eq < s(N), M > |= reads = true [variant] .
  eq < 0,    M > |= reads = false [variant] .

  op writes : -> Prop .
  eq < M, s(N) > |= writes = true [variant] .
  eq < M,    0 > |= writes = false [variant] .

  op writers>1 : -> Prop .
  eq < M, s(s(N)) > |= writers>1 = true [variant] .
   eq < M, s(0)   > |= writers>1 = false [variant] .
  eq < M,     0   > |= writers>1 = false [variant] . 
endm)

--- result: no counterexample
(lmc [10] < N, 0 > |= [] ~ writers>1 .)

--- result: no counterexample
(lmc [10] < N, 0 > |= [] ~ (reads /\ writes) .)

--- result: true
(lfmc < N, 0 > |= [] ~ writers>1 .)

--- result: true
(lfmc < N, 0 > |= [] ~ (reads /\ writes) .)

--- result: true
(lfmc < N, 0 > \/ < 0, s(0) > |= [] ~ writers>1 .)

--- result: true
(lfmc < N, 0 >  \/ < 0, s(0) > |= [] ~ (reads /\ writes) .)

--- result: false
(lmc < N, 0 > |= ([]<> reads) /\ ([]<> writes) .)

--- result: true
(lfmc < N, 0 > |= []<> (reads \/ writes) .)