[SAL-HELP] Finding nearest states

[John Rushby]

Robin,

> Is there a neat way using one of the SAL tools to find all the states  
> reachable within k transitions given some constraint?

SAL is basically a collection of scripts on top of an API for
manipulating state machines.

Existing SAL scripts do not do exactly what you want, but it's
feasible to write one to do it (for finite state): basically invoke
the BDD-based forward image computation k times.  You'll be left with
a BDD that represents the set of k-reachable states.  Intepreting that
BDD is then the big challenge.  Something similar was done in a PVS
extension called InVeST that used SMV to calculate reachable states.

However, do you really want to know the set of reachable states, or do
you just want to query that set for some property?  If the latter,
then you may be able to write a SAL formula to do it.

For example, the following is valid SAL:

  posnat: TYPE = {x: natural | x>0};

  Xn(a: boolean, n: posnat): boolean = 
    IF n = 1 THEN X(a) ELSE Xn(X(a), n-1) ENDIF;

  X24(a: boolean): boolean = Xn(a, 23);

  finish_24: THEOREM VSystem |- Xn(fini, 24)

The final formula asserts that the state predicate fini is true in
VSystem after exactly 24 steps.

Several variations and extensions on this are possible.  For example

  finish_24_foo: THEOREM VSystem |- foo IMPLIES Xn(fini, 24)

says fini is true ater 24 steps from initial states satisfying foo.  


Another approach is to write a synchronous observer: a module that observes
the system (including counting steps) and raises a flag when it sees
what you are looking for.  Then you model check for the raising of the flag.

I hope this suggests some useful directions to explore.   You may get
more concrete help if you can specify more exactly what you are aiming
to do.

John