[SAL] A question when using SAL

[harry huang]

Hi Ashish,

Thanks for the clarification. That make sense. As I was wondering the 
keyword "ELSE" usually appears with "IF" statement, but there is no "IF" in 
the program although I tried to implicitly express this idea. But "[]" 
looked like to be used asynchronously in the concurrent environment. So the 
explaination of "asynchronous composition" of several "guarded transitions" 
in one process cleans my confusion.

In addition, the process jumps out transition  after executing "ELSE -->" ?

Anyway, is there more substantial notes to introduce the semantics of SAL. I 
just read the tutoral and language manual. But I feel it is not sufficient 
enough to understand some basic language semantics  because SAL actually is 
somewhat different with other popular language such as java, C. Promela, 
etc. The language manual presents a good language parser tree, but how to 
use even basic parts such as "IF... ELSE", "For", etc have not explicatly 
stated.  Thanks.

Thanks.

Harry

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