[SAL] A question when using SAL
harryh23 at hotmail.com
Sun Jun 18 14:29:30 PDT 2006
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
>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
> > 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
> > 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);
More information about the SAL