[SAL] A question when using SAL

[Ashish Tiwari]

Hi Harry,

[] means that the process can nondeterministically choose 
either of the alternatives (depending on the guards of
the guarded transitions).
The ELSE guard has a special semantics which means that it
is chosen only when all other guards fail.
So, there is just one process, but is composed of
"asynchronous composition" of several "guarded transitions".

--Ashish

On Sun, 18 Jun 2006, harry huang wrote:

> 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
>> 
>
>