[SAL] state predicates INIT_PRED and TRANS_PRED

Rimvydas Rukšėnas rimvydas at eecs.qmul.ac.uk
Mon Apr 18 15:50:13 PDT 2011


Hi all,

Is there any way to use the state predicates INIT_PRED and TRANS_PRED in SAL? I didn't succeed in that...

Trying something (see attachment) like

   State: TYPE = STATE_TYPE(system1);
   init: [ State -> boolean ] = INIT_PRED(system1);
   trans: [ [State, State] -> boolean ] = TRANS_PRED(system1);

   system2 : MODULE =
   BEGIN
     GLOBAL st: State
     INITIALIZATION [ init(st) --> ]
     TRANSITION
       st' IN { s:State | trans(st,s) }
   END;

produces an error message saying "Failed to convert expression to boolean finite representation, this kind of expression is not supported by the translator."

Any ideas?

Thanks,

Rimvydas

-------------- next part --------------
predicates : CONTEXT = 
BEGIN

  system1: MODULE = 
  BEGIN
    GLOBAL x: [0..5]
    INITIALIZATION x = 0;
    TRANSITION
      [ x < 5 --> x' = x + 1 [] x > 0 --> x' = x - 1 ]
  END;

  State: TYPE = STATE_TYPE(system1);
  init: [ State -> boolean ] = INIT_PRED(system1);
  trans: [ [State, State] -> boolean ] = TRANS_PRED(system1);

  system2 : MODULE = 
  BEGIN
    GLOBAL st: State
    INITIALIZATION [ init(st) --> ]
    TRANSITION
      st' IN { s:State | trans(st,s) }
  END;

  % sal-deadlock-checker -v 3 predicates system2

END


More information about the SAL mailing list