***
*** 1.
***

fmod M is
  sort Elt .
  ops a b c d : -> Elt .
endfm

fmod MSET is
  pr M .
  sort MSet .
  subsorts Elt < MSet .
  op empty : -> MSet .
  op _;_ : MSet MSet -> MSet [assoc comm id: empty] .
  op del : MSet Elt -> MSet .
  var S : MSet .
  vars X Y : Elt .
  eq del(X ; S,X) = del(S,X) .
  eq del(Y ; S,X) = Y ; S [owise] .
endfm

red in MSET : del(a ; b ; a ; c ; a ; d,a) .
red in MSET : del(empty,a) .

--- (a)
--- del(empty,a) does ont reduce to empty.

red in MSET : del(empty,a) .

--- (b)

fmod MSET is
  pr M .
  sort MSet .
  subsorts Elt < MSet .
  op empty : -> MSet .
  op _;_ : MSet MSet -> MSet [assoc comm id: empty] .
  op del : MSet Elt -> MSet .
  var S : MSet .
  var X : Elt .
  eq del(X ; S,X) = del(S,X) .
  eq del(S,X) = S [owise] .
endfm

red in MSET : del(a ; b ; a ; c ; a ; d,a) .
red in MSET : del(empty,a) .

--- (c)

fmod MSET is
  pr M .
  sort MSet .
  subsorts Elt < MSet .
  op empty : -> MSet .
  op _;_ : MSet MSet -> MSet [assoc comm id: empty] .
  op del : MSet Elt -> MSet .
  op enabled-del : MSet Elt -> Bool .
  vars S S' : MSet .
  vars X X' : Elt .
  eq del(X ; S,X) = del(S,X) .
  ceq del(S',X') = S if enabled-del(S',X') =/= true
                     /\ enabled-del(S,X) := enabled-del(S',X') .
  eq enabled-del(X ; S,X) = true .
endfm

red in MSET : del(a ; b ; a ; c ; a ; d,a) .
red in MSET : del(empty,a) .


***
*** 2.
***

fmod PNAT is
  sort Nat .
  op 0 : -> Nat .
  op s_ : Nat -> Nat .
  op _+_ : Nat Nat -> Nat .
  op _*_ : Nat Nat -> Nat .
  vars X Y : Nat .
  eq X + 0 = X .
  eq X + s Y = s (X + Y) .
  eq 0 + Y = Y .
  eq s X + Y = s (X + Y) .
  eq X * 0 = 0 .
  eq X * s Y = (X * Y) + X .
  eq X + (X + X) = X * s s s 0 .
endfm

--- (a) Compute all critical pairs.
---   (1) X + 0 = X
---   (2) X + s Y = s (X + Y)
---   (3) 0 + Y = Y
---   (4) s X + Y = s (X + Y)
---   (5) X * 0 = 0
---   (6) X * s Y = (X * Y) + X
---   (7) X + (X + X) = X * s s s 0
--- Every combination of ovelapping LHSs is as follows:
---   (1,4), (1,7), (2,3), (2,7), (3,7), (4,7)
--- So, there are six critical pairs, which are as follows:
---   i.   (s X,s (X + 0))
---   ii.  (0 + 0,0 * s s s 0)
---   iii. (s (0 + Y), s Y)
---   iv.  (s Y + s (s Y + Y),s Y * s s s 0)
---   v.   (0 + 0,0 * s s s 0)
---   vi.  (s Y + s (s Y + Y),s Y * s s s 0)

--- (b) Prove that PNAT is confluent assuming that PNAT is terminating.
--- Proof
--- All we have to do is to prove every ciritical pair is confluent.
--- i. s (X + 0) --> s X  by (1)
---    So, it is confluent.
--- ii. 0 + 0 --> 0  by (1)
---     0 * s s s 0 --> (0 * s s 0) + 0  by (6)
---                 --> 0 * s s 0        by (1)
---                 --> (0 * s 0) + 0    by (6)
---                 --> 0 * s 0          by (1)
---                 --> (0 * 0) + 0      by (6)
---                 --> 0 * 0            by (1)
---                 --> 0                by (5)
---     So, it is confluent.
--- iii. s (0 + Y) ---> s Y  by (3)
---      So, it is confluent.
--- iv. s Y + s (s Y + Y) --> s (s Y + (s Y + Y))              by (2)
---                       --> s (s Y + s (Y + Y))              by (4)
---                       --> s s (s Y + (Y + Y))              by (2)
---                       --> s s s (Y + (Y + Y))              by (4)
---                       --> s s s (Y * s s s 0)              by (7)
---                       --> s s s ((Y * s s 0) + Y)          by (6)
---                       --> s s s (((Y * s 0) + Y) + Y)      by (6)
---                       --> s s s ((((Y * 0) + Y) + Y) + Y)  by (6)
---                       --> s s s (((0 + Y) + Y) + Y)        by (5)
---                       --> s s s ((Y + Y) + Y)              by (3)
---     s Y * s s s 0 --> (s Y * s s 0) + s Y              by (6)
---                   --> ((s Y * s 0) + s Y) + s Y        by (6)
---                   --> (((s Y * 0) + s Y) + s Y) + s Y  by (6)
---                   --> ((0 + s Y) + s Y) + s Y          by (5)
---                   --> (s Y + s Y) + s Y                by (3)
---                   --> s ((s Y + s Y) + Y)              by (2)
---                   --> s (s (s Y + Y) + Y)              by (2)
---                   --> s s ((s Y + Y) + Y)              by (4)
---                   --> s s (s (Y + Y) + Y)              by (4)
---                   --> s s s ((Y + Y) + Y)              by (4)
---     So, it is confluent.
--- v. The same as ii.
--- vi. The same as iv.
--- Q.E.D.


***
*** 3.
***

fmod M1 is
  sort S .
  op a : -> S .
  op c_ : S -> S .
  op f : S -> S .
  op g : S -> S .
  vars X Y : S .
  eq f(X) = c c X .
  ceq g(X) = Y if f(Y) := c c c X .
endfm

--- 1. Is M1 addmissible?
--- No.
--- This is because f(t) is not a canonical form even if
--- t is a canonical form.

mod M2 is
  sort Sys .
  ops a a1 b b1 c c1 : -> Sys .
  eq a1 = a .
  eq b1 = b .
  eq c1 = c .
  rl a => b .
  rl b => c1 .
  rl c1 => a .
endm

--- 2. Is M2 addmissible?
--- No.
--- This is because the rules are not coherent w.r.t. the equations.
--- There is one-step rewrite of c1 to a, but no one-step rewrite of
--- c that is a canonical form of c1 to any "a" state.

mod M3 is
  sorts Sys1 Sys2 .
  ops a1 b1 b1' : -> Sys1 .
  ops a2 b2 : -> Sys2 .
  eq b1' = b1 .
  rl a1 => b1' .
  rl b1 => a1 .
  crl a2 => b2 if a1 => b1' .
  crl b2 => a2 if b1' => a1 .
endm

--- 3. Is M3 addmissible?
--- No.
--- This is because b1' used in the condition a1 => b1' is not
--- a canonical form.


***
*** 4.
***

mod MUTEX is
  sorts Pid Label Obs Sys .
  subsort Obs < Sys .
  ops p1 p2 : -> Pid .
  ops rs cs : -> Label .
  op void : -> Sys .
  op _ _ : Sys Sys -> Sys [assoc comm id: void] .
  op pc[_]:_ : Pid Label -> Obs .  
  op locked:_ : Bool -> Obs .
  var I : Pid .  var B : Bool .
  rl [enter] : (pc[I]: rs) (locked: false) => (pc[I]: cs) (locked: true) .
  rl [leave] : (pc[I]: cs) (locked: B) => (pc[I]: rs) (locked: false) .
endm

in model-checker

mod MUTEX-PREDS is
  pr MUTEX .
  inc SATISFACTION .
  subsort Sys < State .
  ops (_@rs) (_@cs) : Pid -> Prop .
  var I : Pid .  var S : Sys .  var P : Prop .
  eq (pc[I]: rs) S |= (I @rs) = true .
  eq (pc[I]: cs) S |= (I @cs) = true .
  eq S |= P = false [owise] .
endm

mod MUTEX-CHECK is
  pr MUTEX-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
  op init : -> Sys .
  eq init = (pc[p1]: rs) (pc[p2]: rs) (locked: false) .
  ops mutex lofree : -> Formula .
  eq mutex = [] ~((p1 @cs) /\ (p2 @cs)) .
  eq lofree = ((p1 @rs) |-> (p1 @cs)) /\ ((p2 @rs) |-> (p2 @cs)) .
endm  

red in MUTEX-CHECK : modelCheck(init,mutex) .
red in MUTEX-CHECK : modelCheck(init,lofree) .

---
--- some modification to express strong fairness given to enter
---

mod MUTEX is
  sorts Pid Label Obs Sys .
  subsort Obs < Sys .
  ops p1 p2 : -> Pid .
  ops rs cs : -> Label .
  op void : -> Sys .
  op _ _ : Sys Sys -> Sys [assoc comm id: void] .
  op pc[_]:_ : Pid Label -> Obs .  
  op locked:_ : Bool -> Obs .
  op prg[_]:_ : Pid Bool -> Obs .
  var I : Pid .  var B X : Bool .
  rl [enter] : (pc[I]: rs) (locked: false) (prg[I]: X)
    => (pc[I]: cs) (locked: true) (prg[I]: (not X)) .
  rl [leave] : (pc[I]: cs) (locked: B) => (pc[I]: rs) (locked: false) .
endm

in model-checker

mod MUTEX-PREDS is
  pr MUTEX .
  inc SATISFACTION .
  subsort Sys < State .
  ops (_@rs) (_@cs) : Pid -> Prop .
  ops enabled-enter applied-enter : Pid Bool -> Prop .
  var I : Pid .  var S : Sys .  var P : Prop . var X : Bool .
  eq (pc[I]: rs) S |= (I @rs) = true .
  eq (pc[I]: cs) S |= (I @cs) = true .
  eq (pc[I]: rs) (locked: false) (prg[I]: X) S |= enabled-enter(I,X) = true .
  eq (prg[I]: X) S |= applied-enter(I,X) = true .
  eq S |= P = false [owise] .
endm

mod MUTEX-CHECK is
  pr MUTEX-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
  op init : -> Sys .
  eq init = (pc[p1]: rs) (pc[p2]: rs) (locked: false) (prg[p1]: true) (prg[p2]: true) .
  ops mutex lofree sf1 sf2 fair : -> Formula .
  eq mutex = [] ~((p1 @cs) /\ (p2 @cs)) .
  eq lofree = ((p1 @rs) |-> (p1 @cs)) /\ ((p2 @rs) |-> (p2 @cs)) .
  eq sf1 = (([] <> enabled-enter(p1,true)) -> ([] <> applied-enter(p1,false))) /\
           (([] <> enabled-enter(p1,false)) -> ([] <> applied-enter(p1,true))) .
  eq sf2 = (([] <> enabled-enter(p2,true)) -> ([] <> applied-enter(p2,false))) /\
           (([] <> enabled-enter(p2,false)) -> ([] <> applied-enter(p2,true))) .
  eq fair = sf1 /\ sf2 .
endm  

red in MUTEX-CHECK : modelCheck(init,mutex) .
red in MUTEX-CHECK : modelCheck(init,fair -> lofree) .