[SAL] A question when using SAL

[harry huang]

Hi Ashish,

Thanks. But what is semantics in SAL stating jumping out the transition ?  
As "ELSE -->" means  the process remains in the state i=100 and keeps 
looping in that state, so if I uses "ELSE --> A", does that mean the process 
jumps out the "for" loop  and comes to state A ?

Harry



>From: Ashish Tiwari <tiwari at csl.sri.com>
>To: harry huang <harryh23 at hotmail.com>
>CC: sal at csl.sri.com, rushby at csl.sri.com
>Subject: Re: [SAL] A question when using SAL
>Date: Mon, 19 Jun 2006 10:20:31 -0700 (PDT)
>
>>
>>In addition, the process jumps out transition  after executing "ELSE -->" 
>>?
>
>In your example, once the counter i reaches 100,
>the "ELSE --> " transition is taken infinitely many
>times, that is, the process remains in the state
>i=100 and keeps looping in that state. (It does not
>deadlock).
>
>-Ashish
>
>>>>>If you add an else clause so it reads
>>>>>
>>>>>          i<100  --> i' = i+1;
>>>>>    []
>>>>>          ELSE -->
>>>>>
>