[SAL] A question when using SAL

[harry huang]

Hi John,

Thanks for the information, I tried the suggestions in below and it works. 
Two more questions, does "ELSE --> (without nothing)" mean break the loop ? 
What is "[]" ? Is it means two process asynchronously executing "i' = i+1" 
and "ELSE" parts ? (I do not think I have two processes, but only 1 
process). Thanks.

Harry


>From: John Rushby <rushby at csl.sri.com>
>To: "harry huang" <harryh23 at hotmail.com>
>CC: tiwari at csl.sri.com, sal at csl.sri.com
>Subject: Re: [SAL] A question when using SAL
>Date: Sun, 18 Jun 2006 14:14:23 PDT
>
>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
>