[SAL] variable declarations and renaming

Rimvydas Rukšėnas rimvydas at eecs.qmul.ac.uk
Mon Apr 18 10:29:41 PDT 2011


Hi all,

I was assuming that exactly the same behaviours are always generated by the following two modules  (device1 and device2, see attachment for the full specs):

   dev: MODULE =
   BEGIN
     LOCAL x: State
<spec1>
   END;

   device1: MODULE = WITH GLOBAL st:State RENAME x TO st IN dev;

   device2: MODULE =
   BEGIN
     GLOBAL st: State
<spec1 with st substituted for x>
   END;

However, when device1 and device2 are composed in the same way with other modules, I get different verification outcomes for the same property involving the two compositions (see attachment).

Am I missing something?

Thanks,

Rimvydas

-------------- next part --------------
example : CONTEXT = 
BEGIN

  State: TYPE = boolean;

  guard: MODULE =
  BEGIN
    INPUT start: boolean
    TRANSITION [ start --> ]
  END;

  env: MODULE =
  BEGIN
    GLOBAL st: State
    OUTPUT start: boolean
    INITIALIZATION start = FALSE
    TRANSITION
      [ NOT(start) --> start' = TRUE; st' IN { s:State | TRUE } ]
  END;


  dev: MODULE = 
  BEGIN
    LOCAL x: State
    INITIALIZATION x = FALSE
    TRANSITION
      x' = NOT(x)
  END;

  device1: MODULE = WITH GLOBAL st:State RENAME x TO st IN dev;

  system1: MODULE = (guard || device1) [] env;
  
  device2: MODULE = 
  BEGIN
    GLOBAL st: State
    INITIALIZATION st = FALSE
    TRANSITION
      st' = NOT(st)
  END;

  system2: MODULE = (guard || device2) [] env;

  
  error1: CLAIM system1 |- X (X (st));
  % sal-smc -v 3 example error1
  % proved (I think this should be false...)

  error2: CLAIM system2 |- X (X (st));
  % sal-smc -v 3 example error2
  % invalid

END


More information about the SAL mailing list