SIGNATURE ComState[state]

-- having an implicite state in commands

IMPORT  Void            ONLY void
        Com[void]       ONLY com
        Com[state]      ONLY com
        Com[stateId]    ONLY com

SORT state      -- sort of state

SORT stateId    -- identifier of state

FUN stateId     : state                         -> com[stateId]
        -- create a new implicite state 

FUN with        : stateId ** (state -> state)   -> com[void] 
FUN =>          : stateId ** (state -> state)   -> com[void] 
        -- perform a state transition

FUN get         : stateId                       -> com[state]
FUN ?           : stateId                       -> com[state]
        -- get the current value of an implicite state

FUN delete      : stateId                       -> com[void]
        -- delete implicite state