mcrl2::pbes_system::ltsmin_state

Include file:

#include "mcrl2/pbes/pbes_explorer.h
class mcrl2::pbes_system::ltsmin_state

Public types

type mcrl2::pbes_system::ltsmin_state::operation_type

typedef for parity_game_generator::operation_type

Friends

friend class mcrl2::pbes_system::ltsmin_state::explorer

friend class mcrl2::pbes_system::ltsmin_state::lts_info

Private attributes

std::vector<data_expression> mcrl2::pbes_system::ltsmin_state::param_values
int mcrl2::pbes_system::ltsmin_state::priority
operation_type mcrl2::pbes_system::ltsmin_state::type
std::string mcrl2::pbes_system::ltsmin_state::var

Protected member functions

void add_parameter_value(const data_expression&)

Adds a parameter value to the list of parameter values.

const std::vector<data_expression> &get_parameter_values() const

Returns the list of parameter values.

ltsmin_state(const std::string &varname, const pbes_expression &e)

Constructor.

Parameters:

  • varname the propositional variable of the state.
  • e a propositional variable instantiation.
pbes_expression to_pbes_expression() const

Returns a PBES expression representing the state.

Public member functions

std::string get_variable() const

Returns the priority for the state, which depends on the fixpoint operator of the equation of the propositional variable of the state and on the equation order.

Returns a string representation of the propositional variable of the state.

ltsmin_state(const std::string &varname)

Constructor.

Parameters:

  • varname the name of the propositional variable of the state.
bool operator<(const ltsmin_state &other) const

Compares two PBES_State objects. Uses lexicographical ordering on priority, type, variable and parameter values.

Parameters:

  • other an other PBES_State object.

Returns: true if this.priority < other.priority || (this.priority==other.priority && (this.type < other.type || (this.type==other.type && this.var < other.var || (this.var==other.var && this.param_values < other.param_values) ) ) ).

bool operator==(const ltsmin_state &other) const

Checks if two PBES_State objects are equal.

Parameters:

  • other an other PBES_State object.

Returns: true if this.priority==other.priority && this.type==other.type && this.var==other.var && param_values==param_values.

std::string state_to_string() const

Returns the player or type of the state (And/Or, Abelard/Eloise, Odd/Even).

Returns a string representation of the state.