[SAL] A question when using SAL

[John Rushby]

Harry,

>  But when I used "sal-smc simple1 th1", it still said proved

That's because your specification deadlocks (no action is possible
when i=100).   If you do
  sal-deadlock-checker simple1 process
this will be reported to you.   F properties only apply to infinite
traces and this specification has none (because of the deadlock).

If you add an else clause so it reads

         i<100  --> i' = i+1;
   []
         ELSE -->

then the deadlock is fixed and you'll get a counterexample to your
property.

> Second, I saw there is way to define invariant in the "DEFINITION", 
> so I define a invariant in modification (3). 

One the deadlock is fixed, this works ok:

 th2: THEOREM process |- F(high);


Good luck,
John