[SAL-HELP] transitive closure definition in SAL

[Natarajan Shankar]

Lee: I thought I sent a response to your transitive closure question,
but since I didn't see it myself, here's another try.
I'm attaching a module that computes the transitive closure of a
relation and goes from a not_ready to ready state.  In my earlier email,
I used iterative squaring to compute the transitive closure, but
on Bruno's advice, I tried the linear recursion and that works out
a lot better.  If you send us the exact SAL expression that you're
working with, we can perhaps find a way to improve the performance.

Cheers,
Shankar

tc: CONTEXT =
BEGIN

  n : NATURAL = 10;
  index: TYPE = [0..n];

  P: [[index, index] -> bool] = 
    (LAMBDA (i, j: index): i = j+1);


  PC: TYPE = {not_ready, ready};

  tc: MODULE =
   BEGIN
    OUTPUT
     pc: PC,
     oldR, R: [[index, index] -> bool]

     INITIALIZATION
     pc = not_ready;
     oldR = (LAMBDA (i, j: index): FALSE);
     R = P;

     TRANSITION

     [pc = not_ready AND oldR /= R
      --> oldR' = R;
         R' = (LAMBDA (i, j: index): R(i, j) OR 
	       (EXISTS (k: index): P(i, k) AND R(k, j)))
      []
      pc = not_ready AND oldR = R
       --> pc' = ready
      []
      pc = ready -->
      ]

   END;

%sal-smc -v 10 tc ready --disable-traceability   
   ready: THEOREM tc |- F(pc = ready AND R(5, 0)); 

END