searchpredicate

search predicates

CafeOBJ provides a whole set of search predicates, that searches the reachable states starting from a given state, optionally checking additional conditions. All of them based on the following three basic ones:

• S =(n,m)=>* SS [if Pred] search states reachable by 0 or more transitions;
• S =(n,m)=>+ SS [if Pred] search states reachable by 1 or more transitions;
• S =(n,m)=>! SS [if Pred] search states reachable by 0 or more transitions, and require that the reached state is a final state, i.e., no further transitions can be applied.

To allow for conditional transitions, a transition is only considered in the search if Pred holds.

The parameters n and m in these search predicates:

• n, a natural number or *, gives the maximal number of solutions to be searched. If * is given all solutions are searched exhaustively.
• m, a natural number but not *, gives the maximal depth up to which search is performed.

The predicates return true if there is a (chain of) transitions that fits the parameters (n,m, and *, +, !) and connects S with SS.

There are two orthogonal extension to this search predicate, one adds a suchThat clause, one adds a withStateEq clause.

S =(n,m)=>* SS [if Pred1] suchThat Pred2 ~ (and similar for ! and +) In this case not only the existence, of a transition sequence is tested, but also whether the predicate Pred2, which normally takes S and SS as arguments, holds.

S =(n,m)=>* SS [if Pred1] withStateEq Pred2 ~ (and similar for ! and +) Pred2 is used to determine whether a search continues at SS or not, by comparing SS with all states that have been traversed in the current search. If the predicate Pred2 returns true on the combination of SS as first argument, and any of the previously visited states as second argument, then the search is not continued after SS. (This is a kind of loop detection.)

These two cases can also be combined into

S =(n,m)=>* SS [if Pred1] suchThat Pred2 withStateEq Pred3