domain FState = {NOMINAL, LOST, ERROR} ;
domain FailureType = {Err, Loss, Ok} ;

node Function
   flow   I : FailureType : in ; O : FailureType : out ;
   state  S : FState ;
   event  fail_loss, fail_err ;
   init   S := NOMINAL ;
   trans  S != LOST    |- fail_loss -> S := LOST ;
          S =  NOMINAL |- fail_err  -> S := ERROR ;
   assert O = case { S = NOMINAL : I, S = LOST : Loss, else Err } ;
edon