[SAL] A question when using SAL

[Ashish Tiwari]

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