mod NID is
  pr CONFIGURATION .
  ops n0 n1 n2 n3 n4 n5 : -> Oid [ctor] .
  op goal? : Oid -> Bool .
  var NI : Oid .
  eq goal?(n3) = true .
  eq goal?(NI) = false [owise] .
endm

mod NNPAIR is
  pr NID .
  pr NAT .
  sort NNPair .
  op <_,_> : Oid Nat -> NNPair [ctor] .
endm

mod GSTATUS is
  sort GStat .
  ops nFin fin : -> GStat [ctor] .
endm

mod SOUP {D :: TRIV} is
  sort Soup{D} .
  subsort D$Elt < Soup{D} .
  op empty : -> Soup{D} [ctor] .
  op _ _ : Soup{D} Soup{D} -> Soup{D} [ctor assoc comm id: empty] .
  op _\in_ : D$Elt Soup{D} -> Bool .
  var E : D$Elt .
  var S : Soup{D} .
  eq E \in empty = false .
  eq E \in E S = true .
  eq E \in S = false [owise] .
endm

view NNPair from TRIV to NNPAIR is
  sort Elt to NNPair .
endv

mod SOUP-NNPAIR is
  pr SOUP{NNPair} .
  op _\in_ : Oid Soup{NNPair} -> Bool .
  var NI : Oid .
  var W : Nat .
  var NNPs : Soup{NNPair} .
  eq NI \in < NI,W > NNPs = true .
  eq NI \in NNPs = false [owise] .
endm

mod OCOMP is
  pr SOUP-NNPAIR .
  pr GSTATUS .
  sort OComp .
  op Node : -> Cid [ctor] .
  op nnps1 :_ : Soup{NNPair} -> Attribute [ctor gather (&)] .
  op nnps2 :_ : Soup{NNPair} -> Attribute [ctor gather (&)] .
  op Gstat : -> Cid [ctor] .
  op status :_ : GStat -> Attribute [ctor gather (&)] .
endm

view OComp from TRIV to OCOMP is
  sort Elt to OComp .
endv

mod OCOMP-SOUP is
  pr SOUP{OComp} .
endm

mod CONFIG is
  pr OCOMP-SOUP .
  sorts Config .
  --- op {_} : Soup{OComp} -> Config [ctor] .
  --- op {_} : Configuration -> Config [ctor] .
  op gs : -> Oid [ctor] .
  --- op init : -> Config .
  op init : -> Configuration .
  vars NNPs1 NNPs2 : Soup{NNPair} .
  var OCs : Soup{OComp} .
  eq init = < gs : Gstat | status : nFin >
                   < n0 : Node | nnps1 : (< n1,4 > < n2,1 > < n3,6 >), nnps2 : empty >
                   < n2 : Node | nnps1 : (< n1,2 > < n5,1 >), nnps2 : empty >
                   < n3 : Node | nnps1 : empty, nnps2 : empty >
                   < n4 : Node | nnps1 : (< n3,1 >), nnps2 : empty >
                   < n5 : Node | nnps1 : (< n1,1 > < n3,3 >), nnps2 : empty > .
endm

mod EX is
  inc CONFIG .
  vars NI NI' : Oid .
  var W : Nat .
  vars NNPs1 NNPs2 NNPs3 NNPs1' NNPs2' : Soup{NNPair} .
  var OCs : Configuration .

  rl [ex-stutter] : < gs : Gstat | status : fin > => < gs : Gstat | status : fin > .

  rl [ex-done] : < gs : Gstat | status : nFin > => < gs : Gstat | status : fin > .

  rl [ex-change] : 
  < gs : Gstat | status : nFin > < NI : Node |  nnps1 : (< NI',W > NNPs1), nnps2 : NNPs2 >
   => 
  < gs : Gstat | status : nFin > < NI : Node |  nnps1 : NNPs1, nnps2 : (< NI',(if W == 1 then 1 else W + 1 fi) > NNPs2) > .

  crl [ex-del] : 
  < gs : Gstat | status : nFin > < NI : Node | nnps1 : NNPs1, nnps2 : NNPs2 > 
   => 
  < gs : Gstat | status : nFin > < NI : Node | nnps1 : empty, nnps2 : NNPs3 > 
  if < NI', W > NNPs3 := NNPs1 NNPs2 /\ W > 1 .
endm

***(
search [1] in EX : init =>* 
< n2 : Node | nnps1 : NNPs1, nnps2 : NNPs2 > OCs
such that not (n5 \in NNPs1 NNPs2) .

search [1] in EX : init =>* 
< n5 : Node | nnps1 : NNPs1, nnps2 : NNPs2 > OCs
such that not (n3 \in NNPs1 NNPs2) .
)***

in model-checker .

mod EX-PREDS is
  pr EX .
  inc SATISFACTION .
  --- subsort Config < State .
  subsort Configuration < State .
  op fin : -> Prop .
  op n2->n5 : -> Prop .
  op n3->n5 : -> Prop .
  var OCs : Configuration .
  vars NNPs1 NNPs2 : Soup{NNPair} .
  var PROP : Prop .
  eq < gs : Gstat | status : fin > OCs |= fin = true .
  eq < n2 : Node | nnps1 : NNPs1, nnps2 : NNPs2 > OCs |= n2->n5 = (n5 \in NNPs1 NNPs2) .
  eq < n3 : Node | nnps1 : NNPs1, nnps2 : NNPs2 > OCs |= n3->n5 = (n3 \in NNPs1 NNPs2) .
  eq OCs |= PROP = false [owise] .
endm

mod EX-CHECK is
  inc EX-PREDS .
  inc MODEL-CHECKER .
  inc LTL-SIMPLIFIER .
endm

***(
red in EX-CHECK : modelCheck(init,[] n2->n5) .
red in EX-CHECK : modelCheck(init,[] n3->n5) .
red in EX-CHECK : modelCheck(init,<> fin) .
)***