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 murxla::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.
-
enumerator REGULAR
-
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 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, withsumbeing 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.
Public Static Attributes
-
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_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 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.