Jon Jacky, University of Washington
jon@u.washington.edu
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.
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
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?
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.