fmod STATE is

sort State . --- distributed system state

op eState : -> State .
op __ : State State -> State 
        [assoc comm id: eState format (d ni d)] .

sort Action . --- actions for the interaction between
              --- environment (controller) and system model

op ENABLED : Action -> State . --- enable action
op PERFORMED : Action -> State . --- action performed

endfm