[SAL-HELP] strange counter-example from sal-smc

[Bruno Dutertre]

Graeme Smith wrote:
> Hi,
> 
> When I try to check the attached SAL file with sal-smc, I get the 
> attached counter-example. Why does the skip transition happen when the 
> cop transition is obviously enabled?
> 
> Graeme

Hi Graeme,

The else transition in a module is taken when the guards of all
the other transitions are false. If the guards do not contain
primed variables, that's the same thing as saying that the
else transition is enabled when all the other transitions are
disabled. But when you have primed variables in the guards, that's
not so obvious.

In your example,

   opa: ev=Init AND (s'=s+1 OR s'=s+2) AND ev'=AOp -->
      s' IN {n:NAT|true}; ev' =AOp
   []
   opc: ev=AOp AND t'=t+1 AND ev'=COp -->
      t' IN {n:NAT|true}; ev'=COp

the else transition is equivalent to

   [] not (ev=Init AND  (s'=s+1 OR s'=s+2) AND ev'=AOp)
      AMD not (ev=AOp AND t'=t+1 AND ev'=COp) --> ev'=skip

The counterexample you get is consistent with this.

Avoid putting primed variables in the guards unless you are
forced to. There's usually no reason to put X' in a guard if
X is a local or output variable of the module.

Bruno