load model-checker.maude set include BOOL off . fmod IMP-SYNTAX is pr TRUTH . --- here we use the built-in booleans because they can go in conditional equations sort Id NzNat Nat . subsort NzNat < Nat . ops a b c d e f g i j k l m n o p q r s t u v w x y z : -> Id [ctor] . op _, : Id -> Id [ctor] . --- op true : -> Bool [ctor] . --- op false : -> Bool [ctor] . op 0 : -> Nat [ctor] . op 1 : -> NzNat [ctor] . op _+_ : Nat Nat -> Nat [ctor assoc comm id: 0] . op _+_ : NzNat Nat -> NzNat [ctor ditto] . op _*_ : Nat Nat -> Nat [ctor assoc comm] . sorts BoolExp BoolRedex . sorts NatExp NatRedex . subsort Id < NatRedex . subsort Nat NatRedex < NatExp . subsort Bool BoolRedex < BoolExp . op (_&&_) : BoolExp BoolExp -> BoolRedex [ctor] . op (_||_) : BoolExp BoolExp -> BoolRedex [ctor] . op ~_ : BoolExp -> BoolRedex [ctor] . op (_<_) : NatExp NatExp -> BoolRedex [ctor] . op (_<=_) : NatExp NatExp -> BoolRedex [ctor] . op (_=_) : NatExp NatExp -> BoolRedex [ctor] . op _-_ : NatExp NatExp -> NatRedex [ctor] . op _+_ : NatRedex NatExp -> NatRedex [ditto] . op _+_ : NatExp NatExp -> NatExp [ditto] . op _*_ : NatExp NatExp -> NatExp [ditto] . sort BasicStmt Stmt . subsort BasicStmt < Stmt . --- stmts have id: skip; leading to a simpler semantics --- but not suitable for symbolic reasoning with unification op _;_ : Stmt Stmt -> Stmt [ctor assoc id: skip prec 60] . op skip : -> BasicStmt [ctor] . op _:=_ : Id NatExp -> BasicStmt [ctor] . op if_then_fi : BoolExp Stmt -> BasicStmt [ctor] . op while_do_od : BoolExp Stmt -> BasicStmt [ctor] . endfm fmod IMP-DATA is pr IMP-SYNTAX . op ~Bool_ : Bool -> Bool . ops (_/\Bool_) (_\/Bool_) : Bool Bool -> Bool . op _-Nat_ : Nat Nat -> Nat . ops (_ Bool . op (_=Nat_) : Nat Nat -> Bool [comm] . op (_*Nat_) : Nat Nat -> Nat [assoc comm] . var N M : Nat . var P R Q : NzNat . var B : Bool . eq ~Bool true = false [variant] . eq ~Bool false = true [variant] . eq true /\Bool B = B [variant] . eq false /\Bool B = false [variant] . eq true \/Bool B = true [variant] . eq false \/Bool B = B [variant] . eq N -Nat (N + M) = 0 [variant] . eq (N + P) -Nat N = P [variant] . eq N PreMemory [ctor] . op none : -> PreMemory [ctor] . op __ : PreMemory PreMemory -> PreMemory [ctor assoc comm id: none] . op {_} : PreMemory -> Memory [ctor] . op err : -> [Memory] [ctor] . var I : Id . var J K : Nat . var M : PreMemory . eq {[I,J] [I,K] M} = err . endfm fmod IMP-EVAL is pr IMP-MEM + IMP-DATA . op eval : Memory NatExp -> [Nat] . op eval : Memory BoolExp -> [Bool] . var NE1 NE2 : NatExp . var B : Bool . var NR1 NR2 : NatRedex . var P : NzNat . var BE1 BE2 : BoolExp . var N : Nat . var M : Memory . var PM : PreMemory . var I : Id . --- recursive case eq eval(M,NR1 + P ) = eval(M,NR1) + P [variant] . eq eval(M,NR1 + NR2) = eval(M,NR1) + eval(M,NR2) [variant] . eq eval(M,NE1 - NE2) = eval(M,NE1) -Nat eval(M,NE2) [variant] . eq eval(M,NE1 * NE2) = eval(M,NE1) *Nat eval(M,NE2) [variant] . eq eval(M,BE1 && BE2) = eval(M,BE1) /\Bool eval(M,BE2) [variant] . eq eval(M,BE1 || BE2) = eval(M,BE1) \/Bool eval(M,BE2) [variant] . eq eval(M,NE1 < NE2) = eval(M,NE1) NzNat . eq 2 = 1 + 1 . eq 3 = 1 + 1 + 1 . eq 4 = 1 + 1 + 1 + 1 . eq 5 = 1 + 1 + 1 + 1 + 1 . eq 6 = 1 + 1 + 1 + 1 + 1 + 1 . eq 7 = 1 + 1 + 1 + 1 + 1 + 1 + 1 . eq 8 = 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 . eq 9 = 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 . eq 10 = 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 . endm mod IMP-SEMANTICS is pr IMP-EVAL + IMP-SYNTAX + IMP-NUMBERS . sort ImpState . op _|_ : Stmt [Memory] -> ImpState [ctor prec 61] . var P : PreMemory . var NE : NatExp . var S S' : Stmt . var I : Id . var M : Memory . var N : Nat . var BR : BoolRedex . var BE : BoolExp . rl I := NE ; S' | {[I,N] P} => S' | {[I,eval({[I,N] P},NE)] P} . rl if BR then S fi ; S' | M => if eval(M,BR) then S fi ; S' | M . rl if true then S fi ; S' | M => S ; S' | M . rl if false then S fi ; S' | M => S' | M . rl while BE do S od ; S' | M => if BE then S ; while BE do S od fi ; S' | M . endm mod THREADED-IMP-SEMANTICS is pr IMP-EVAL + IMP-SYNTAX + IMP-NUMBERS . sort ThreadedImpState Thread ThreadSet . subsort Thread < ThreadSet . op __ : ThreadSet ThreadSet -> ThreadSet [ctor prec 61 assoc comm id: none] . op none : -> ThreadSet . op {_|_} : Stmt Nat -> Thread [ctor] . op _|_|_ : ThreadSet Memory Nat -> ThreadedImpState [ctor prec 62] . sort TermStmt . subsort TermStmt < Stmt . var NE : NatExp . var S S' : Stmt . var I : Id . var TS : ThreadSet . var M : Memory . var N J K : Nat . var BR : BoolRedex . var B : Bool . var BE : BoolExp . var PM : PreMemory . rl {T:TermStmt ; S' | J} TS | M | K => {S' | J} TS | M | J . rl {I := NE ; S' | J} TS | {[I,N] PM} | K => {S' | J} TS | {[I,eval({[I,N] PM},NE)] PM} | J . rl {if BR then S fi ; S' | J} TS | M | K => {if eval(M,BR) then S fi ; S' | J} TS | M | J . rl {if true then S fi ; S' | J} TS | M | K => {S ; S' | J} TS | M | J . rl {if false then S fi ; S' | J} TS | M | K => {S' | J} TS | M | J . rl {while BE do S od ; S' | J} TS | M | K => {if BE then S ; while BE do S od fi ; S' | J} TS | M | J . endm mod PETERSON is pr THREADED-IMP-SEMANTICS . ops crit rest : -> TermStmt [ctor] . ops p0 p1 : -> Thread . op init-mem : -> Memory . eq init-mem = {[a,0] [b,0] [t,0]} . eq p0 = {while true do a := 1 ; while b = 1 do if t = 1 then a := 0 ; while t = 1 do skip od ; a := 1 fi od ; crit ; t := 1 ; a := 0 ; rest od | 0} . eq p1 = {while true do b := 1 ; while a = 1 do if t = 0 then b := 0 ; while t = 0 do skip od ; b := 1 fi od ; crit ; t := 0 ; b := 0 ; rest od | 1} . endm mod THREADED-IMP-CHECK is inc PETERSON . inc (MODEL-CHECKER + LTL-SIMPLIFIER) * (sort Nat to Nat*,sort NzNat to NzNat*, op _+_ to _.+_, op _*_ to _.*_, op _<_ to _.<_, op _<=_ to _.<=_) . subsort ThreadedImpState < State . ops exec crit : Nat -> Prop . var M : Memory . vars S S' : Stmt . vars J K L : Nat . eq ({S | J} {S' | L} | M | J) |= exec(J) = true . eq ({S | J} {S' | L} | M | K) |= exec(J) = false [owise] . eq ({crit ; S | J} {S' | L} | M | K) |= crit(J) = true . eq ({S | J} {S' | L} | M | K) |= crit(J) = false [owise] . endm --- give your solutions to the two problems below as Maude commands