[SAL] A question when using SAL

[Leonardo de Moura]

Hi Harry,

sal-smc assumes the transition relation is total, that is, there are  
no deadlocks.
The module "process" deadlocks when i = 100.
You can find deadlocks using the tool sal-deadlock-checker.
You can avoid the deadlock with a ELSE transition:

      [
         i<100  --> i' = i+1;
            ELSE -->
      ]

Cheers,
Leonardo


On Jun 18, 2006, at 2:02 PM, harry huang wrote:

> Hi,
>
> Thanks for information. I modified the program and it is on below:
>
> ====
> simple1: CONTEXT =
> BEGIN
>
>  process: MODULE =
>    BEGIN
>      OUTPUT i: [0..100]                    -- modified (1)
>      LOCAL high: BOOLEAN                -- modified (2)
>      DEFINITION high = i > 100          -- modified (3)
>      INITIALIZATION
>        i = 1
>      TRANSITION
>      [
>         i<100  --> i' = i+1;
>      ]
>    END;
>
>  th1: THEOREM process |- F(i=110);    -- modified (4)
> END
> ====
>
> (1), (2), (3), (4) are the modified code. This code passed the  
> compiler. But I have some two issues do not understand. First, for  
> the modification (4), it should not hold because in the transition,  
> the loop stops incrementing i by 1 if i reach 100. But when I used  
> "sal-smc simple1 th1", it still said proved. Second, I saw there is  
> way to define invariant in the "DEFINITION", so I define a  
> invariant in modification (3). But why the using of "sal-smc  
> simple1 th1" still said it is proved ?
>
> Can someone gives me hints ? Thanks.
>
> harry
>
>
>> From: Ashish Tiwari <tiwari at csl.sri.com>
>> To: harry huang <harryh23 at hotmail.com>
>> CC: sal at csl.sri.com
>> Subject: Re: [SAL] A question when using SAL
>> Date: Sat, 17 Jun 2006 16:51:55 -0700 (PDT)
>>
>>
>> The type "INTEGER" is not bounded; it has infinitely
>> many elements.
>> You will have to replace it by a finite subrange type
>> (e.g. [0..100]) for sal-smc to work on this example.
>>
>> Hope this helps,
>> -Ashish
>>
>> On Sat, 17 Jun 2006, harry huang wrote:
>>
>>> Hi,
>>>
>>> I have a question when using SAL.
>>>
>>> I want to express a process doing in below after try to verify  
>>> that eventually that i == 100
>>> ===
>>> int i;
>>> for (i = 1; i<100; i++);
>>> ===
>>>
>>> So , I made a SAL program in below
>>>
>>> ====
>>> simple1: CONTEXT =
>>> BEGIN
>>>
>>> process: MODULE =
>>>   BEGIN
>>>     OUTPUT i: INTEGER
>>>     INITIALIZATION
>>>       i = 1
>>>     TRANSITION
>>>     [
>>>        increment:
>>>        i<100  --> i' = i+1;
>>>     ]
>>>   END;
>>>
>>> th1: THEOREM process |- F(i=100);
>>> END
>>> =====
>>>
>>> But when I used the command "sal-smc simple1 th1", it gave me the  
>>> error
>>> "
>>> Error: [Context: simple1, line(6), column(16)]: Finite type  
>>> representation cannot be generated, type is not finite.
>>> Reason: [Context: prelude, line(189), column(20)]: Type is not a  
>>> bounded subtype of integer, or it was not possible to determine  
>>> the bound.
>>>
>>> "
>>>
>>> Can someone give me some hints ? Thanks.
>>>
>>> Harry
>>>
>>>
>>
>