[SAL-HELP] transitive closure definition in SAL

[Lee Pike]

Hello,

I have defined a binary relation R over a small finite set S of  
constants.  I am trying to compute the transitive closure of R, and  
I'm running into problems.  My approach was to use a recursive  
function that builds the transitive closure, the bound on recursion  
being the order of S.  For even small sets S (say, order < 10), SAL  
is taking an inordinately long time to determine whether some ordered  
pair is a member of the transitive closure of R (I'm using sal-inf- 
bmc -i -d 0 with a trivial stateless module---S, R, and the closure  
are all constants).

(1) I'm assuming that even in trivial cases (e.g., for some pair  
already in R, I ask whether it's in the transitive closure of R), the  
recursive function still must get completely unrolled first.  Is that  
correct?

(2) Is there a better way?  Perhaps by encoding the computation of  
the closure as a transition system?

I hope this gives the basic idea, but if anyone needs the code, I can  
post it.

Thanks,
Lee

--
Galois <http://www.galois.com/>

Phone: +1 503.626.6616 ext. 135
Fax: +1 503.350.0833