FSM: States

A state of the FSM corresponds to the current state of the solver under test. Transitions from one state to another (or the same) state either have an “action” (the execution of one or more solver API calls) associated, or are “empty”, i.e., do not execute any solver API calls. Taking a transition executes its action.

Transitions are weighted, and their weight is defined via its priority when adding transitions to a state via murxla::State::add_action(). A priority of 1 indicates highest priority, UINT32_MAX lowest priority, and 0 disables the transition.

A transition with an associated action is defined by adding a murxla::Action to a state via murxla::State::add_action() while defining its priority and next state. Similarly, empty transitions are added as instances of murxla::Transition.

Each state of the FSM may provide a pre-condition for transitioning into that state (murxla::State::f_precond). Use murxla::FSM::new_state() to create and add new states to the FSM. To add solver-specific actions to a state, retrieve the state via murxla::FSM::get_state().

State

class State

A state of the FSM.

Corresponds to a state of the solver under test.

We distinguish three configuration kinds (State::ConfigKind) of states:

  • regular states

  • decision states

  • choice states

We further identify one state as the initial state, and one state as the final state.

A decision state is a state that only serves as decision point with a single point of entrance and only specific transitions (the choices to be made) out of the state. A decision state is not to be extended with any other actions other than the transitions that represent the choices this decision state has been created for. From a decision state, we may only transition into the choice states that represent the valid choices for this decision.

A choice state is a state that represents a valid choice for a specific decision. It represents a very specific solver state that is a precondition for specific actions (solver API calls) to be executed. Choice states may only be transitioned into from their corresponding decision state.

As an example, we use a decision state DECIDE_SAT_UNSAT for handling different solver states after a satisfiability check in state CHECK_SAT. From CHECK_SAT, we transition into DECIDE_SAT_UNSAT, from where we transition into either choice state SAT (when the result is sat or unknown) or UNSAT (when the result is unsat). Each choice state configure actions to make additional queries to the solver under the specific premise that a check-sat call has been issued and the satisfiability result is either sat or unsat.

Public Types

enum ConfigKind

The configuration kind of a state.

Values:

enumerator REGULAR

Regular state.

enumerator DECISION

Decision state.

enumerator CHOICE

Choice state.

using Kind = std::string

The kind of a state.

This is used a state identifier when retrieving states that have been added to the FSM via FSM::get_state(). We use strings here to make the set of state kinds easily extensible with solver-specific states.

Public Functions

inline State()

Default constructor.

inline State(const Kind &kind, std::function<bool(void)> fun, bool ignore, bool is_final, ConfigKind config)

Constructor.

Parameters:

  • kind – The kind of the state.

  • fun – The precondition of the state.

  • ignore – True if the state should be ignored when adding actions to all states (add_action_to_all_states), or adding all configured states as next state for a transition (add_action_to_all_states_next).

  • is_final – True if state is a final state.

  • config – The configuration kind of the state.

inline const Kind &get_kind()

Get the kind of this state.

Returns:

The kind of this state.

inline ConfigKind get_config()

Get the configuration kind of this state.

Returns:

The configuration kind of this state.

inline const uint64_t get_id() const

Get the id of this state.

Returns:

The id of this state.

inline void set_id(uint64_t id)

Set the id of this state.

Parameters:

id – The unique identifier of this state.

inline bool is_final()

Determine if this state is a final state.

Returns:

True if this state is a final state.

inline void update_precondition(std::function<bool(void)> fun)

Update the function defining the precondition for entering the state.

Parameters:

fun – The new precondition.

State *run(RNGenerator &rng)

Take one of the transitions (and execute its associated action) associated with this state. Transitions with higher weight, are picked with a higher probability.

Parameters:

rng – The associated random number generator.

Returns:

The next state.

void add_action(Action *action, uint32_t priority, State *next = nullptr)

Add action to this state.

Parameters:

  • action – The action to add.

  • priority – The priority of the action, determines the weight, and thus the probability to choose running the action. The actual weight of the action is computed as sum/priority, with sum being the sum of the priorities of all actions in that state.

  • next – The state to transition into after running the action. Optional, if not set, we stay in the current state.

void disable_action(Action::Kind kind)

Disable action of given kind. This will set the priority to 0.

Parameters:

kind – The kind of the action to disable.

Public Static Attributes

static const Kind UNDEFINED = "undefined"

The undefined state.

static const Kind NEW = "new"

The state where an instance of the solver under test is created and initialized.

By default, this is configured as the initial state.

static const Kind SET_LOGIC = "set_logic"

The state where the logic of the formulas to be created is configured.

static const Kind OPT = "opt"

The state where solver options are configured.

static const Kind OPT_REQ = "opt_req"

The state where solver options that are required based on the current solver configuration are configured (see Solver::get_required_options()).

static const Kind DELETE = "delete"

The state where the instance of the solver under test is deleted (not the final state).

static const Kind FINAL = "final"

The final state.

By default, no actions are performed in this state.

static const Kind CREATE_SORTS = "create_sorts"

The state where sorts of enabled theories are created.

static const Kind CREATE_INPUTS = "create_inputs"

The state where inputs with avaible sorts are created.

static const Kind CREATE_TERMS = "create_terms"

The state where terms are created from available inputs and terms.

Precondition: At least one term (input) must already have been created.

static const Kind ASSERT = "assert"

The state where formulas (boolean terms) are asserted.

Precondition: At least one boolean term must already have been created.

static const Kind CHECK_SAT = "check_sat"

The state where satisfiability is checked, optionally under a given set of assumptions. formulas (boolean terms) are asserted.

Depending on the result of the satisfiability check, by default, from this state we always transition into the DECIDE_SAT_UNSAT decision state.

static const Kind SAT = "sat"

The choice state representing the solver state after a sat or unknown result.

This state may only be entered from the DECIDE_SAT_UNSAT decision state.

Note

If a solver disallows querying model values after an unknown result, introduce a solver-specific choice state for unknown and add a transition from DECIDE_SAT_UNSAT to this new solver-specific state accordingly.

static const Kind UNSAT = "unsat"

The choice state representing the solver state after an unsat result.

This state may only be entered from the DECIDE_SAT_UNSAT decision state.

static const Kind PUSH_POP = "push_pop"

The state where context levels are pushed and popped.

static const Kind DECIDE_SAT_UNSAT = "decide-sat_unsat"

The decision state that is reached immediately after an action is executed in state CHECK_SAT. This state is where it is decided which one of the corresponding choice states SAT and UNSAT to enter, depending on the satisfiability result.

As a decision state, it only serves as decision point for which choice state to transition into, with a single point of entrance (from state CHECK_SAT) and only specific transitions (the choices to be made) out of the state.