mod CONTROLLER is

protecting NAT .
protecting STATE .

sort Controller .

op PERFORM : Action -> Controller .
op WAITFOR : Action -> Controller .

op eController : -> Controller .
op _;_ : Controller Controller -> Controller [ assoc id: eController ] .
op _||_ : Controller Controller -> Controller [ assoc comm id: eController ] .
op _+_ : Controller Controller -> Controller [ assoc comm id: eController ] .
op *_ : Controller -> Controller .
op +_ : Controller -> Controller .

var act : Action .
var ctrl ctrl' ctrl'' ctrl''' : Controller .
var ctrl0 ctrl1 ctrl2 ctrl3 : Controller .
var waiting : Bool .

op CONTROLLER : Controller -> State .

var limit depth : Nat .

rl  CONTROLLER((PERFORM(act) || ctrl1) ; ctrl2) 
    =>
    ENABLED(act)
    CONTROLLER((WAITFOR(act) || ctrl1) ; ctrl2) .

rl  CONTROLLER((WAITFOR(act) || ctrl1) ; ctrl2)
    PERFORMED(act) 
    =>
    CONTROLLER((ctrl1 ; ctrl2)) .

crl CONTROLLER((ctrl || ctrl1) ; ctrl2) 
    =>
    CONTROLLER((ctrl' || ctrl1) ; ctrl2)
    if (ctrl' + ctrl'') := ctrl /\
       ctrl' =/= eController /\ ctrl'' =/= eController .

crl CONTROLLER((ctrl || ctrl1) ; ctrl2) 
    =>
    CONTROLLER((ctrl' || ctrl1) ; ctrl2)
    if (ctrl' + ctrl'') := ctrl /\
       ctrl' =/= eController /\ ctrl'' =/= eController .

rl  CONTROLLER((+(ctrl) || ctrl1) ; ctrl2)
     =>
    CONTROLLER(((ctrl ; *(ctrl)) || ctrl1) ; ctrl2) .

rl  CONTROLLER((*(ctrl) || ctrl1) ; ctrl2) 
    =>
    CONTROLLER((ctrl1 ; ctrl2)) .

crl CONTROLLER((*(ctrl) || ctrl1) ; ctrl2) 
    => 
    ENABLED(act)
    CONTROLLER((ctrl''' ; *(ctrl) || ctrl1) ; ctrl2)
    if ((PERFORM(act) || ctrl') ; ctrl'') := ctrl /\
       ctrl''' := ((WAITFOR(act) || ctrl') ; ctrl'') .

endm