#include <pbes_explorer.h>

Public Types
using	operation_type = parity_game_generator::operation_type
	The variable sequence type.

Public Member Functions
bool	get_reset_option () const
	Returns if the reset option is set.

int	get_number_of_groups () const
	Returns the number of transition groups.

const std::vector< std::string > &	get_transition_variable_names () const
	Returns the map from transition group number to the variable name of the equation to which the transition group belongs.

const std::vector< operation_type > &	get_transition_types () const
	Returns the map from transition group number to the type of the right hand side of the equation to which the transition group belongs.

const std::map< std::string, operation_type > &	get_variable_types () const
	Returns the map from variable names to the type of the right hand side of the equation for the variable.

const std::map< std::string, int > &	get_variable_priorities () const
	Returns the map from variable names to the priority of the equation for the variable.

const std::map< std::string, std::vector< std::string > > &	get_variable_parameter_signatures () const
	Returns the map from variable names to the list of parameters signatures for the variable.

const std::map< std::string, std::vector< int > > &	get_variable_parameter_indices () const
	Returns the map from variable names to the list of indices of the parameters signatures for the variable according the order in the list of parameter signatures for the system.

const std::map< std::string, std::map< int, int > > &	get_variable_parameter_index_positions () const
	Returns the map from variable names to the map from indices of parameter signatures for the variable (according to the list of parameter signatures for the system) to the index of the type of the parameter (in the list of types for the system).

const lts_type &	get_lts_type () const
	Returns the LTS Type.

const std::map< int, std::vector< bool > > &	get_dependency_matrix () const
	Returns the dependency matrix.

const std::map< int, std::vector< bool > > &	get_read_matrix () const
	Returns the read dependency matrix.

const std::map< int, std::vector< bool > > &	get_write_matrix () const
	Returns the write dependency matrix.

int	get_index (const std::string &signature)
	Returns the index for a parameter signature in the list of parameter signatures for the system.

bool	is_read_dependent_propvar (int group)
	Determines if `group` is read dependent on the propositional variable. Returns true, because the propositional variable is needed to determine if the group belongs to the variable.

bool	is_read_dependent_parameter (int group, int part)
	Determines if `group` is read dependent on part `part` of the state vector. Returns true if the parameter represented by `part` is in the set of parameters of the state variable for the group or in the set of data variables used in the expression of for the group.

bool	is_write_dependent_propvar (int group)
	Determines if `group` is write dependent on the propositional variable. Returns true if propositional variables other than the group variable occur in the group expression or the group expression may directly evaluate to `true` or `false`.

bool	is_write_dependent_parameter (int group, int part)
	Determines if `group` is read dependent on part `part` of the state vector. Returns true if the parameter represented by `part` is in the set of data variables changed by the expression for the group.

std::string	state_to_string (const ltsmin_state &state)
	Returns a string representation for state `state`.

Static Public Member Functions
static std::string	get_param_signature (const std::string &paramname, const std::string &paramtype)
	Returns a signature using name and type of a parameter.

Protected Member Functions
const std::vector< pbes_expression > &	get_transition_expressions () const
	Returns the map from transition group number to the expression of the transition group.

const std::map< std::string, propositional_variable > &	get_variables () const
	Returns the map from variable names to the variable object for the variable.

const std::map< std::string, fixpoint_symbol > &	get_variable_symbols () const
	Returns the map from variable names to the fixpoint operator of the equation for the variable.

const std::map< std::string, data::variable_list > &	get_variable_parameters () const
	Returns the map from variable names to the sequence of parameters for the variable.

std::set< std::string >	used (const pbes_expression &expr)
	Computes the free variables actually used, not only passed through, in an expression.

std::set< std::string >	used (const pbes_expression &expr, const std::set< std::string > &L)
	Computes the free variables actually used, not only passed through, in an expression.

std::set< std::string >	copied (const pbes_expression &expr)
	Computes the free variables which are copied/passed through (to a recursive variable) in an expression.

std::set< std::string >	copied (const pbes_expression &expr, const std::set< std::string > &L)
	Computes the free variables which are copied/passed through (to a recursive variable) in an expression.

std::set< std::string >	changed (const pbes_expression &phi)
	Computes the set of parameters changed in the expression.

std::set< std::string >	changed (const pbes_expression &phi, const std::set< std::string > &L)
	Computes the set of parameters changed in the expression.

std::set< std::string >	reset (const pbes_expression &phi, const std::set< std::string > &d)
	Computes the set of parameters reset in the expression.

std::vector< int >	get_param_indices (const data::variable_list &params)
	Converts a variable_sequence_type into a sequence of indices of parameter signatures in the list of parameter signatures for the system.

std::map< int, int >	get_param_index_positions (const data::variable_list &params)
	Converts a variable_sequence_type into a map from indices of parameter signatures (in the list of parameter signatures for the system) to the index of the type of the parameter (in the list of types for the system).

const data_expression &	get_default_value (int index)
	Returns a default value for the sort of a parameter signature.

	lts_info (pbes &p, detail::pbes_greybox_interface *pgg, bool reset, bool always_split)
	Constructor.

Static Protected Member Functions
static bool	tf (const pbes_expression &phi)
	Determines if the term phi contains a branch that directly results in `true` or `false` (not a variable).

static std::set< std::string >	occ (const pbes_expression &expr)
	Computes the propositional variables used in an expression.

static std::set< std::string >	free (const pbes_expression &expr)
	Computes the free variables read in an expression.

static std::set< std::string >	get_param_set (const data::variable_list &params)
	Converts a variable_sequence_type into a set of parameter signatures.

static std::vector< std::string >	get_param_sequence (const data::variable_list &params)
	Converts a variable_sequence_type into a sequence of parameter signatures.

static std::string	get_param_signature (const variable &param)
	Returns a signature for parameter `param`.

Private Member Functions
int	count_variables (const pbes_expression &e)
	Counts the number of propositional variables in an expression.

bool	is_pass_through_state (const propositional_variable_instantiation &propvar)
	Determines if the propositional variable instantiation is one that only copies parameters from the current state.

std::vector< pbes_expression >	split_expression_and_substitute_variables (const pbes_expression &e, int current_priority, operation_type current_type, std::set< std::string > vars_stack)
	Splits the expression into parts (disjuncts or conjuncts) and recursively tries to substitute the propositional variables with the parts of the right hand side of the equation for the variable.

void	compute_lts_type ()
	Computes LTS Type from PBES.

void	compute_transition_groups ()
	Computes transition groups from PBES.

void	compute_dependency_matrix ()
	Computes dependency matrix from PBES.

Private Attributes
pbes &	p

detail::pbes_greybox_interface *	pgg

bool	reset_option

bool	always_split_option

lts_type	type

std::map< int, std::vector< bool > >	read_matrix

std::map< int, std::vector< bool > >	write_matrix

std::map< int, std::vector< bool > >	matrix

std::map< std::string, int >	param_index

std::vector< data_expression >	param_default_values

int	number_of_groups = 0

std::vector< pbes_expression >	transition_expression

std::vector< pbes_expression >	transition_expression_plain

std::vector< std::string >	transition_variable_name

std::vector< operation_type >	transition_type

std::map< std::string, propositional_variable >	variables

std::map< std::string, operation_type >	variable_type

std::map< std::string, fixpoint_symbol >	variable_symbol

std::map< std::string, int >	variable_priority

std::map< std::string, pbes_expression >	variable_expression

std::map< std::string, data::variable_list >	variable_parameters

std::map< std::string, std::vector< std::string > >	variable_parameter_signatures

std::map< std::string, std::vector< int > >	variable_parameter_indices

std::map< std::string, std::map< int, int > >	variable_parameter_index_positions

Static Private Attributes
static std::map< variable, std::string >	variable_signatures

Friends
class	ltsmin_state

class	explorer

Detailed Description

Definition at line 171 of file pbes_explorer.h.

Member Typedef Documentation

◆ operation_type

using mcrl2::pbes_system::lts_info::operation_type = parity_game_generator::operation_type

The variable sequence type.

Definition at line 178 of file pbes_explorer.h.

Constructor & Destructor Documentation

◆ lts_info()

mcrl2::pbes_system::lts_info::lts_info	(	pbes &	p,
		detail::pbes_greybox_interface *	pgg,
		bool	reset = `false`,
		bool	always_split = `false`
	)

protected

Constructor.

lts_info

Parameters

p
pgg
reset
always_split

Definition at line 159 of file pbes_explorer.cpp.

Member Function Documentation

◆ changed() [1/2]

std::set< std::string > mcrl2::pbes_system::lts_info::changed ( const pbes_expression & phi )

protected

Computes the set of parameters changed in the expression.

Parameters

phi

Definition at line 782 of file pbes_explorer.cpp.

◆ changed() [2/2]

std::set< std::string > mcrl2::pbes_system::lts_info::changed	(	const pbes_expression &	phi,
		const std::set< std::string > &	L
	)

protected

Computes the set of parameters changed in the expression.

Parameters

phi
L

Definition at line 789 of file pbes_explorer.cpp.

◆ compute_dependency_matrix()

void mcrl2::pbes_system::lts_info::compute_dependency_matrix ( )

private

Computes dependency matrix from PBES.

Definition at line 537 of file pbes_explorer.cpp.

◆ compute_lts_type()

void mcrl2::pbes_system::lts_info::compute_lts_type ( )

private

Computes LTS Type from PBES.

Definition at line 176 of file pbes_explorer.cpp.

◆ compute_transition_groups()

void mcrl2::pbes_system::lts_info::compute_transition_groups ( )

private

Computes transition groups from PBES.

Definition at line 405 of file pbes_explorer.cpp.

◆ copied() [1/2]

std::set< std::string > mcrl2::pbes_system::lts_info::copied ( const pbes_expression & expr )

protected

Computes the free variables which are copied/passed through (to a recursive variable) in an expression.

Parameters

expr

Definition at line 1009 of file pbes_explorer.cpp.

◆ copied() [2/2]

std::set< std::string > mcrl2::pbes_system::lts_info::copied	(	const pbes_expression &	expr,
		const std::set< std::string > &	L
	)

protected

Computes the free variables which are copied/passed through (to a recursive variable) in an expression.

Parameters

expr
L

Definition at line 1016 of file pbes_explorer.cpp.

◆ count_variables()

int mcrl2::pbes_system::lts_info::count_variables ( const pbes_expression & e )

inlineprivate

Counts the number of propositional variables in an expression.

Returns: the number of variable occurences or INT_MAX if a variable occurs within the scope of a quantifier.

Definition at line 268 of file pbes_explorer.cpp.

◆ free()

std::set< std::string > mcrl2::pbes_system::lts_info::free ( const pbes_expression & expr )

staticprotected

Computes the free variables read in an expression.

Parameters

expr

Definition at line 926 of file pbes_explorer.cpp.

◆ get_default_value()

const data_expression & mcrl2::pbes_system::lts_info::get_default_value ( int index )

protected

Returns a default value for the sort of a parameter signature.

Parameters

index the index of the parameter signature.

Returns: a default value for the sort of the parameter.

Definition at line 675 of file pbes_explorer.cpp.

◆ get_dependency_matrix()

const std::map< int, std::vector< bool > > & mcrl2::pbes_system::lts_info::get_dependency_matrix ( ) const

Returns the dependency matrix.

Definition at line 651 of file pbes_explorer.cpp.

◆ get_index()

int mcrl2::pbes_system::lts_info::get_index ( const std::string & signature )

Returns the index for a parameter signature in the list of parameter signatures for the system.

Parameters

signature The parameter signature.

Definition at line 669 of file pbes_explorer.cpp.

◆ get_lts_type()

const lts_type & mcrl2::pbes_system::lts_info::get_lts_type ( ) const

Returns the LTS Type.

Definition at line 645 of file pbes_explorer.cpp.

◆ get_number_of_groups()

int mcrl2::pbes_system::lts_info::get_number_of_groups ( ) const

Returns the number of transition groups.

Definition at line 574 of file pbes_explorer.cpp.

◆ get_param_index_positions()

std::map< int, int > mcrl2::pbes_system::lts_info::get_param_index_positions ( const data::variable_list & params )

protected

Converts a variable_sequence_type into a map from indices of parameter signatures (in the list of parameter signatures for the system) to the index of the type of the parameter (in the list of types for the system).

Parameters

params a sequence of variables.

Definition at line 1140 of file pbes_explorer.cpp.

◆ get_param_indices()

std::vector< int > mcrl2::pbes_system::lts_info::get_param_indices ( const data::variable_list & params )

protected

Converts a variable_sequence_type into a sequence of indices of parameter signatures in the list of parameter signatures for the system.

Parameters

params a sequence of variables.

Definition at line 1128 of file pbes_explorer.cpp.

◆ get_param_sequence()

std::vector< std::string > mcrl2::pbes_system::lts_info::get_param_sequence ( const data::variable_list & params )

staticprotected

Converts a variable_sequence_type into a sequence of parameter signatures.

Parameters

params a sequence of variables.

Definition at line 1117 of file pbes_explorer.cpp.

◆ get_param_set()

std::set< std::string > mcrl2::pbes_system::lts_info::get_param_set ( const data::variable_list & params )

staticprotected

Converts a variable_sequence_type into a set of parameter signatures.

Parameters

params a sequence of variables.

Definition at line 1106 of file pbes_explorer.cpp.

◆ get_param_signature() [1/2]

std::string mcrl2::pbes_system::lts_info::get_param_signature	(	const std::string &	paramname,
		const std::string &	paramtype
	)

inlinestatic

Returns a signature using name and type of a parameter.

Parameters

paramname	the parameter name.
paramtype	the parameter type.

Definition at line 1172 of file pbes_explorer.cpp.

◆ get_param_signature() [2/2]

std::string mcrl2::pbes_system::lts_info::get_param_signature ( const variable & param )

inlinestaticprotected

Returns a signature for parameter param.

Parameters

param a parameter.

Definition at line 1157 of file pbes_explorer.cpp.

◆ get_read_matrix()

const std::map< int, std::vector< bool > > & mcrl2::pbes_system::lts_info::get_read_matrix ( ) const

Returns the read dependency matrix.

Definition at line 657 of file pbes_explorer.cpp.

◆ get_reset_option()

bool mcrl2::pbes_system::lts_info::get_reset_option ( ) const

Returns if the reset option is set.

Definition at line 568 of file pbes_explorer.cpp.

◆ get_transition_expressions()

const std::vector< pbes_expression > & mcrl2::pbes_system::lts_info::get_transition_expressions ( ) const

protected

Returns the map from transition group number to the expression of the transition group.

Definition at line 580 of file pbes_explorer.cpp.

◆ get_transition_types()

const std::vector< lts_info::operation_type > & mcrl2::pbes_system::lts_info::get_transition_types ( ) const

Returns the map from transition group number to the type of the right hand side of the equation to which the transition group belongs.

Definition at line 592 of file pbes_explorer.cpp.

◆ get_transition_variable_names()

const std::vector< std::string > & mcrl2::pbes_system::lts_info::get_transition_variable_names ( ) const

Returns the map from transition group number to the variable name of the equation to which the transition group belongs.

Definition at line 586 of file pbes_explorer.cpp.

◆ get_variable_parameter_index_positions()

const std::map< std::string, std::map< int, int > > & mcrl2::pbes_system::lts_info::get_variable_parameter_index_positions ( ) const

Returns the map from variable names to the map from indices of parameter signatures for the variable (according to the list of parameter signatures for the system) to the index of the type of the parameter (in the list of types for the system).

Definition at line 639 of file pbes_explorer.cpp.

◆ get_variable_parameter_indices()

const std::map< std::string, std::vector< int > > & mcrl2::pbes_system::lts_info::get_variable_parameter_indices ( ) const

Returns the map from variable names to the list of indices of the parameters signatures for the variable according the order in the list of parameter signatures for the system.

Definition at line 633 of file pbes_explorer.cpp.

◆ get_variable_parameter_signatures()

const std::map< std::string, std::vector< std::string > > & mcrl2::pbes_system::lts_info::get_variable_parameter_signatures ( ) const

Returns the map from variable names to the list of parameters signatures for the variable.

Definition at line 627 of file pbes_explorer.cpp.

◆ get_variable_parameters()

const std::map< std::string, data::variable_list > & mcrl2::pbes_system::lts_info::get_variable_parameters ( ) const

protected

Returns the map from variable names to the sequence of parameters for the variable.

Definition at line 621 of file pbes_explorer.cpp.

◆ get_variable_priorities()

const std::map< std::string, int > & mcrl2::pbes_system::lts_info::get_variable_priorities ( ) const

Returns the map from variable names to the priority of the equation for the variable.

Definition at line 615 of file pbes_explorer.cpp.

◆ get_variable_symbols()

const std::map< std::string, fixpoint_symbol > & mcrl2::pbes_system::lts_info::get_variable_symbols ( ) const

protected

Returns the map from variable names to the fixpoint operator of the equation for the variable.

Definition at line 609 of file pbes_explorer.cpp.

◆ get_variable_types()

const std::map< std::string, lts_info::operation_type > & mcrl2::pbes_system::lts_info::get_variable_types ( ) const

Returns the map from variable names to the type of the right hand side of the equation for the variable.

Definition at line 604 of file pbes_explorer.cpp.

◆ get_variables()

const std::map< std::string, propositional_variable > & mcrl2::pbes_system::lts_info::get_variables ( ) const

protected

Returns the map from variable names to the variable object for the variable.

Definition at line 598 of file pbes_explorer.cpp.

◆ get_write_matrix()

const std::map< int, std::vector< bool > > & mcrl2::pbes_system::lts_info::get_write_matrix ( ) const

Returns the write dependency matrix.

Definition at line 663 of file pbes_explorer.cpp.

◆ is_pass_through_state()

bool mcrl2::pbes_system::lts_info::is_pass_through_state ( const propositional_variable_instantiation & propvar )

inlineprivate

Determines if the propositional variable instantiation is one that only copies parameters from the current state.

Definition at line 227 of file pbes_explorer.cpp.

◆ is_read_dependent_parameter()

bool mcrl2::pbes_system::lts_info::is_read_dependent_parameter	(	int	group,
		int	part
	)

Determines if group is read dependent on part part of the state vector. Returns true if the parameter represented by part is in the set of parameters of the state variable for the group or in the set of data variables used in the expression of for the group.

Parameters

group	the number of the transition group.
part	the number of the state part.

Returns: true if param_part in ( params(var(group)) union used(expr(group)) ).

Definition at line 687 of file pbes_explorer.cpp.

◆ is_read_dependent_propvar()

bool mcrl2::pbes_system::lts_info::is_read_dependent_propvar ( int group )

Determines if group is read dependent on the propositional variable. Returns true, because the propositional variable is needed to determine if the group belongs to the variable.

Parameters

group the number of the transition group.

Returns: true.

Definition at line 681 of file pbes_explorer.cpp.

◆ is_write_dependent_parameter()

bool mcrl2::pbes_system::lts_info::is_write_dependent_parameter	(	int	group,
		int	part
	)

Determines if group is read dependent on part part of the state vector. Returns true if the parameter represented by part is in the set of data variables changed by the expression for the group.

Parameters

group	the number of the transition group.
part	the number of the state part.

Returns: true if param_part in changed(expr(group)).

Definition at line 754 of file pbes_explorer.cpp.

◆ is_write_dependent_propvar()

bool mcrl2::pbes_system::lts_info::is_write_dependent_propvar ( int group )

Determines if group is write dependent on the propositional variable. Returns true if propositional variables other than the group variable occur in the group expression or the group expression may directly evaluate to true or false.

Parameters

group the number of the transition group.

Returns: true if ( occ(expr(group)) - {var(group)} ) is not empty or tf(expr(group)).

Definition at line 725 of file pbes_explorer.cpp.

◆ occ()

std::set< std::string > mcrl2::pbes_system::lts_info::occ ( const pbes_expression & expr )

staticprotected

Computes the propositional variables used in an expression.

Parameters

expr

Definition at line 904 of file pbes_explorer.cpp.

◆ reset()

std::set< std::string > mcrl2::pbes_system::lts_info::reset	(	const pbes_expression &	phi,
		const std::set< std::string > &	d
	)

protected

Computes the set of parameters reset in the expression.

Parameters

phi
d

Definition at line 844 of file pbes_explorer.cpp.

◆ split_expression_and_substitute_variables()

std::vector< pbes_expression > mcrl2::pbes_system::lts_info::split_expression_and_substitute_variables	(	const pbes_expression &	e,
		int	current_priority,
		operation_type	current_type,
		std::set< std::string >	vars_stack
	)

private

Splits the expression into parts (disjuncts or conjuncts) and recursively tries to substitute the propositional variables with the parts of the right hand side of the equation for the variable.

Parameters

e	the expression
current_priority	the priority of the current equation for which the parts are computed
current_type	the operation type (AND/OR) of the current equation for which the parts are computed
vars_stack	used for detection of infinite recursion. Please, initialise to the empty set.

Definition at line 313 of file pbes_explorer.cpp.

◆ state_to_string()

std::string mcrl2::pbes_system::lts_info::state_to_string ( const ltsmin_state & state )

Returns a string representation for state state.

Parameters

state

Definition at line 1074 of file pbes_explorer.cpp.

◆ tf()

bool mcrl2::pbes_system::lts_info::tf ( const pbes_expression & phi )

staticprotected

Determines if the term phi contains a branch that directly results in true or false (not a variable).

Parameters

phi	a PBES expression

Definition at line 882 of file pbes_explorer.cpp.

◆ used() [1/2]

std::set< std::string > mcrl2::pbes_system::lts_info::used ( const pbes_expression & expr )

protected

Computes the free variables actually used, not only passed through, in an expression.

Parameters

expr

Definition at line 937 of file pbes_explorer.cpp.

◆ used() [2/2]

std::set< std::string > mcrl2::pbes_system::lts_info::used	(	const pbes_expression &	expr,
		const std::set< std::string > &	L
	)

protected

Computes the free variables actually used, not only passed through, in an expression.

Parameters

expr
L

Definition at line 944 of file pbes_explorer.cpp.

Friends And Related Symbol Documentation

◆ explorer

friend class explorer

friend

Definition at line 174 of file pbes_explorer.h.

◆ ltsmin_state

friend class ltsmin_state

friend

Definition at line 173 of file pbes_explorer.h.

Member Data Documentation

◆ always_split_option

bool mcrl2::pbes_system::lts_info::always_split_option

private

Definition at line 183 of file pbes_explorer.h.

◆ matrix

std::map<int,std::vector<bool> > mcrl2::pbes_system::lts_info::matrix

private

Definition at line 187 of file pbes_explorer.h.

◆ number_of_groups

int mcrl2::pbes_system::lts_info::number_of_groups = 0

private

Definition at line 190 of file pbes_explorer.h.

◆ p

pbes& mcrl2::pbes_system::lts_info::p

private

Definition at line 180 of file pbes_explorer.h.

◆ param_default_values

std::vector<data_expression> mcrl2::pbes_system::lts_info::param_default_values

private

Definition at line 189 of file pbes_explorer.h.

◆ param_index

std::map<std::string,int> mcrl2::pbes_system::lts_info::param_index

private

Definition at line 188 of file pbes_explorer.h.

◆ pgg

detail::pbes_greybox_interface* mcrl2::pbes_system::lts_info::pgg

private

Definition at line 181 of file pbes_explorer.h.

◆ read_matrix

std::map<int,std::vector<bool> > mcrl2::pbes_system::lts_info::read_matrix

private

Definition at line 185 of file pbes_explorer.h.

◆ reset_option

bool mcrl2::pbes_system::lts_info::reset_option

private

Definition at line 182 of file pbes_explorer.h.

◆ transition_expression

std::vector<pbes_expression> mcrl2::pbes_system::lts_info::transition_expression

private

Definition at line 191 of file pbes_explorer.h.

◆ transition_expression_plain

std::vector<pbes_expression> mcrl2::pbes_system::lts_info::transition_expression_plain

private

Definition at line 192 of file pbes_explorer.h.

◆ transition_type

std::vector<operation_type> mcrl2::pbes_system::lts_info::transition_type

private

Definition at line 194 of file pbes_explorer.h.

◆ transition_variable_name

std::vector<std::string> mcrl2::pbes_system::lts_info::transition_variable_name

private

Definition at line 193 of file pbes_explorer.h.

◆ type

lts_type mcrl2::pbes_system::lts_info::type

private

Definition at line 184 of file pbes_explorer.h.

◆ variable_expression

std::map<std::string, pbes_expression> mcrl2::pbes_system::lts_info::variable_expression

private

Definition at line 199 of file pbes_explorer.h.

◆ variable_parameter_index_positions

std::map<std::string, std::map<int,int> > mcrl2::pbes_system::lts_info::variable_parameter_index_positions

private

Definition at line 203 of file pbes_explorer.h.

◆ variable_parameter_indices

std::map<std::string, std::vector<int> > mcrl2::pbes_system::lts_info::variable_parameter_indices

private

Definition at line 202 of file pbes_explorer.h.

◆ variable_parameter_signatures

std::map<std::string, std::vector<std::string> > mcrl2::pbes_system::lts_info::variable_parameter_signatures

private

Definition at line 201 of file pbes_explorer.h.

◆ variable_parameters

std::map<std::string, data::variable_list> mcrl2::pbes_system::lts_info::variable_parameters

private

Definition at line 200 of file pbes_explorer.h.

◆ variable_priority

std::map<std::string, int> mcrl2::pbes_system::lts_info::variable_priority

private

Definition at line 198 of file pbes_explorer.h.

◆ variable_signatures

std::map< variable, std::string > mcrl2::pbes_system::lts_info::variable_signatures

staticprivate

Definition at line 205 of file pbes_explorer.h.

◆ variable_symbol

std::map<std::string, fixpoint_symbol> mcrl2::pbes_system::lts_info::variable_symbol

private

Definition at line 197 of file pbes_explorer.h.

◆ variable_type

std::map<std::string, operation_type> mcrl2::pbes_system::lts_info::variable_type

private

Definition at line 196 of file pbes_explorer.h.

◆ variables

std::map<std::string, propositional_variable> mcrl2::pbes_system::lts_info::variables

private

Definition at line 195 of file pbes_explorer.h.

◆ write_matrix

std::map<int,std::vector<bool> > mcrl2::pbes_system::lts_info::write_matrix

private

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

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Static Protected Member Functions

Private Member Functions

Private Attributes

Static Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ operation_type

Constructor & Destructor Documentation

◆ lts_info()

Member Function Documentation

◆ changed() [1/2]

◆ changed() [2/2]

◆ compute_dependency_matrix()

◆ compute_lts_type()

◆ compute_transition_groups()

◆ copied() [1/2]

◆ copied() [2/2]

◆ count_variables()

◆ free()

◆ get_default_value()

◆ get_dependency_matrix()

◆ get_index()

◆ get_lts_type()

◆ get_number_of_groups()

◆ get_param_index_positions()

◆ get_param_indices()

◆ get_param_sequence()

◆ get_param_set()

◆ get_param_signature() [1/2]

◆ get_param_signature() [2/2]

◆ get_read_matrix()

◆ get_reset_option()

◆ get_transition_expressions()

◆ get_transition_types()

◆ get_transition_variable_names()

◆ get_variable_parameter_index_positions()

◆ get_variable_parameter_indices()

◆ get_variable_parameter_signatures()

◆ get_variable_parameters()

◆ get_variable_priorities()

◆ get_variable_symbols()

◆ get_variable_types()

◆ get_variables()

◆ get_write_matrix()

◆ is_pass_through_state()

◆ is_read_dependent_parameter()

◆ is_read_dependent_propvar()

◆ is_write_dependent_parameter()

◆ is_write_dependent_propvar()

◆ occ()

◆ reset()

◆ split_expression_and_substitute_variables()

◆ state_to_string()

◆ tf()

◆ used() [1/2]

◆ used() [2/2]

Friends And Related Symbol Documentation

◆ explorer

◆ ltsmin_state

Member Data Documentation

◆ always_split_option

◆ matrix

◆ number_of_groups

◆ p

◆ param_default_values

◆ param_index

◆ pgg

◆ read_matrix

◆ reset_option

◆ transition_expression

◆ transition_expression_plain

◆ transition_type

◆ transition_variable_name

◆ type

◆ variable_expression