[SAL] A question when using SAL

[harry huang]

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