Exploration algorithm

Jon Jacky, University of Washington

The exploration algorithm treats program state as first class.

// Types
type Value;      // values, type of method arguments and return values
type State;      // concrete model state, something like Map<Name, Value>
type Action;     // name of method in model, maybe just string 
type Args;       // method argument list, something like Seq<Value>
type Transition; // state transition, like <State,Action,Args,Value,State>

// Exploration state, transitions stores the generated FSM
Seq<State> frontier = Seq{ S0 };      // states to be explored
Set<Transition> transitions = Set{};  // generated FSM

// From the model, acts like configuration
State S0 = ...;                         // initial state
bool IsEnabled(Action a, Args args, State current);
     // action is enabled in current state according to precondition in model

// Configuration
Seq<Action> Actions;         // actions from model used to generate FSM
Seq<Args> Domain(Action a, State current); // argument lists for action a 

// Utility methods called by Explore
// Invoke executes action+args in the current state, returns next state
// Also returns return value, only used here to label transition
// No nondeterminism for now, only one next state
// If Invoked invocation throws exception, Invoke returns current state 
<State,Value> State Invoke(Action a, Args args, State current); 

This simplified algorithm performs exhaustive exploration.

// Exhaustive exploration, concrete states only, no nondeterminism
// Domains are the only explicit limits to exploration here
// No explicit arguments but depends on exploration state and configuration
// Updates exploration state: transitions, frontier
void Explore() {
  while (!frontier.IsEmpty) {
      State current = frontier.Head;
      foreach (Action action in Actions) {
        foreach (Args args in Domain(action, current)) {
          if (IsEnabled(action, args, current)) {
            (next, result) = Invoke(action, args, current); 
            let states = Set{ t in transition; ... };
            if !(next in states) frontier += Seq{next}; // append next state
            transitions += Set{(current, action, args, result, next)};
          } // end if invocation is enabled
        } // end foreach args in Domain
      } // end foreach action
      frontier = fronter.Tail;  // remove current state from frontier
  } // end explore while frontier is not empty and stop condition not reached
} // end Explore method       

Appending next state to end of frontier results in breadth-first exploration (shown here, Spec Explorer default). Pushing next state on front of frontier results in depth-first exploration (optional).

For efficiency, store "state deltas" and compare hash functions on states.

Limiting exploration

Stopping rules and filters on states and can limit exploration.

bool Stop();           // stopping condition has been reached
bool Filter(State s);  // s should be added to generated FSM

void Explore() {
            (next, result) = Invoke(action, args, current); 
            if (Filter(next)) { // true if next state passes Filter
              if !(next in states) frontier += Seq{next}; 
              transitions += Set{(current, action, args, result, next)};
            } // end if next state passes Filter
            if (Stop()) return; // return immediately if stopping condition
} // end Explore method       

Exploring with state groupings

State groupings provide a way to sample the state space.

Grouping expressions calculate a value for each state.

Example: the size of a collection. All states where the collection has the same size have the same grouping expression value.

Exploration builds an FSM with a single representative state for each grouping expression value. (Actually, N of representatives is configurable).

Example: one state where the collection has each size 0, 1, 2, ..., regardless of collection contents. (Use a filter to set the maximum size of the collection).

When there are multiple grouping expressions, exploration builds an FSM which contains the union (not the Cartesian product) of all the grouping expression values.

// FOR GROUPINGS: special case for exposition, two groupings
Value Grouping1(State s);     // Value of grouping expression 1 in state s
Value Grouping2(State s);     // Value of grouping expression 2 in state s

void Explore() {
              (next, result) = Invoke(action, args, current); 
              Set<Value> group1 = Set{ s in states; Grouping1(s) };
              Set<Value> group2 = Set{ s in states; Grouping2(s) };
              if (!(Grouping1(next) in group1)
                  || !(Grouping2(next) in group2)){
                frontier += Set{next};
                transitions += Set{(current, action, args, result, next)};
              } // end if next state is new representative in group1 or group2
} // end Explore method       

Exercise: What if you want to explore the Cartesian product of properties?

Controlling exploration order

When you are only sampling the state space, exploration order matters.

The "frontier" actually contains all the transitions from all the frontier states, not just the states themselves.

You can control the order in which frontier transitions are searched.

"Partial exploration" may discard some frontier transitions without exploring them.