mcrl2::pbes_system::ltsmin_state Class Reference

#include <pbes_explorer.h>

Public Types
typedef parity_game_generator::operation_type	operation_type

Public Member Functions
	ltsmin_state (const std::string &varname)
	Constructor.
bool	operator< (const ltsmin_state &other) const
	Compares two PBES_State objects. Uses lexicographical ordering on priority, type, variable and parameter values.
bool	operator== (const ltsmin_state &other) const
	Checks if two PBES_State objects are equal.
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.
std::string	state_to_string () const
	Returns the player or type of the state (And/Or, Abelard/Eloise, Odd/Even).

Protected Member Functions
	ltsmin_state (const std::string &varname, const pbes_expression &e)
	Constructor.
const std::vector< data_expression > &	get_parameter_values () const
	Returns the list of parameter values.
void	add_parameter_value (const data_expression &)
	Adds a parameter value to the list of parameter values.
pbes_expression	to_pbes_expression () const
	Returns a PBES expression representing the state.

Private Attributes
int	priority
std::string	var
operation_type	type
std::vector< data_expression >	param_values

Friends
class	lts_info
class	explorer

Detailed Description

Definition at line 116 of file pbes_explorer.h.

Member Typedef Documentation

operation_type

typedef parity_game_generator::operation_type mcrl2::pbes_system::ltsmin_state::operation_type

Definition at line 122 of file pbes_explorer.h.

Constructor & Destructor Documentation

ltsmin_state() [1/2]

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

protected

Constructor.

Parameters

varname	the propositional variable of the state.
e	a propositional variable instantiation.

Definition at line 1185 of file pbes_explorer.cpp.

ltsmin_state() [2/2]

mcrl2::pbes_system::ltsmin_state::ltsmin_state

(

const std::string &

varname

)

Constructor.

Parameters

varname

the name of the propositional variable of the state.

Definition at line 1179 of file pbes_explorer.cpp.

Member Function Documentation

add_parameter_value()

void mcrl2::pbes_system::ltsmin_state::add_parameter_value ( const data_expression &  value )

protected

Adds a parameter value to the list of parameter values.

Definition at line 1246 of file pbes_explorer.cpp.

get_parameter_values()

const std::vector< data_expression > & mcrl2::pbes_system::ltsmin_state::get_parameter_values ( ) const

protected

Returns the list of parameter values.

Definition at line 1240 of file pbes_explorer.cpp.

get_variable()

std::string mcrl2::pbes_system::ltsmin_state::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.

Definition at line 1234 of file pbes_explorer.cpp.

operator<()

bool mcrl2::pbes_system::ltsmin_state::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) ) ) ).

Definition at line 1211 of file pbes_explorer.cpp.

operator==()

bool mcrl2::pbes_system::ltsmin_state::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.

Definition at line 1226 of file pbes_explorer.cpp.

state_to_string()

std::string mcrl2::pbes_system::ltsmin_state::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.

Definition at line 1266 of file pbes_explorer.cpp.

to_pbes_expression()

pbes_expression mcrl2::pbes_system::ltsmin_state::to_pbes_expression ( ) const

protected

Returns a PBES expression representing the state.

Definition at line 1252 of file pbes_explorer.cpp.

Friends And Related Symbol Documentation

explorer

friend class explorer

friend

Definition at line 119 of file pbes_explorer.h.

lts_info

friend class lts_info

friend

Definition at line 118 of file pbes_explorer.h.

Member Data Documentation

param_values

std::vector<data_expression> mcrl2::pbes_system::ltsmin_state::param_values

private

Definition at line 128 of file pbes_explorer.h.

priority

int mcrl2::pbes_system::ltsmin_state::priority

private

Definition at line 125 of file pbes_explorer.h.

type

operation_type mcrl2::pbes_system::ltsmin_state::type

private

Definition at line 127 of file pbes_explorer.h.

var

std::string mcrl2::pbes_system::ltsmin_state::var

private

Definition at line 126 of file pbes_explorer.h.

---

The documentation for this class was generated from the following files:

• pbes/include/mcrl2/pbes/pbes_explorer.h
• pbes/source/pbes_explorer.cpp