mcrl2::pbes_system::ltsmin_state Class Reference

#include <pbes_explorer.h>

Public Types
using	operation_type = parity_game_generator::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 a string representation of the propositional variable of the state.
std::string	state_to_string () const
	Returns a string representation of the state.

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 = 0
std::string	var
operation_type	type
std::vector< data_expression >	param_values

Friends
class	lts_info
class	explorer

Detailed Description

Definition at line 113 of file pbes_explorer.h.

Member Typedef Documentation

operation_type

using mcrl2::pbes_system::ltsmin_state::operation_type = parity_game_generator::operation_type

Definition at line 119 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 1189 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 1183 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 1255 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 1249 of file pbes_explorer.cpp.

get_variable()

std::string mcrl2::pbes_system::ltsmin_state::get_variable

(

)

const

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

Definition at line 1243 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 1235 of file pbes_explorer.cpp.

state_to_string()

std::string mcrl2::pbes_system::ltsmin_state::state_to_string

(

)

const

Returns a string representation of the state.

Definition at line 1275 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 1261 of file pbes_explorer.cpp.

Friends And Related Symbol Documentation

explorer

friend class explorer

friend

Definition at line 116 of file pbes_explorer.h.

lts_info

friend class lts_info

friend

Definition at line 115 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 125 of file pbes_explorer.h.

priority

int mcrl2::pbes_system::ltsmin_state::priority = 0

private

Definition at line 122 of file pbes_explorer.h.

type

operation_type mcrl2::pbes_system::ltsmin_state::type

private

Definition at line 124 of file pbes_explorer.h.

var

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

private

Definition at line 123 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