#include <pbes_explorer.h>

Public Types
using	operation_type = parity_game_generator::operation_type
	The expression type of the equation.

Public Member Functions
	explorer (const std::string &filename, const std::string &rewrite_strategy, bool reset_flag, bool always_split_flag)
	Constructor.

	explorer (const pbes &p_, const std::string &rewrite_strategy, bool reset_flag, bool always_split_flag)
	Constructor.

	~explorer ()
	Destructor.

lts_info *	get_info () const
	Returns the PBES_Info object.

ltsmin_state	get_initial_state () const
	Returns the initial state.

void	initial_state (int *state)

int	get_index (int type_no, const std::string &s)
	Returns the index of `value` in the local store for the data type with number `type_no`. Type 0 is reserved for the string representations of variable names. The value is added to the store if it is not already present.

int	get_string_index (const std::string &s)
	Returns the index of `s` in the local store for string values. This store is reserved for the string representations of variable names. The value is added to the store if it is not already present.

void	to_state_vector (const ltsmin_state &dst_state, int dst, const ltsmin_state &src_state, int const &src)
	Transforms a PBES state to a state vector, represented by an array of integers.

std::string	get_value (int type_no, int index)
	Returns the value at position `index` in the local store for the data type with number `type_no`. Type 0 is reserved for the string representations of variable names. An exception is thrown if the index does not exist in the store.

const std::string &	get_string_value (int index)
	Returns the string at position `index` in the local store for string values. An exception is thrown if the index does not exist in the store.

ltsmin_state	from_state_vector (int *const &src)
	Transforms a state vector `src` into a PBES_State object object containing the variable and parameter values that are represented by the indices in `src`.

std::vector< ltsmin_state >	get_successors (const ltsmin_state &state)
	Computes successor states for a state. Serves as a wrapper around the get_successors function of the pbes_greybox_interface.

template<typename callback >
void	next_state_all (int *const &src, callback &cb)
	Iterates over the successors of a state and invokes a callback function for each successor state.

std::vector< ltsmin_state >	get_successors (const ltsmin_state &state, int group)
	Computes successor states for a state as defined in transition group `group`. Serves as a wrapper around the get_successors function of the pbes_greybox_interface.

template<typename callback >
void	next_state_long (int *const &src, int group, callback &cb)
	Iterates over the successors of a state for a certain transition group and invokes a callback function for each successor state.

Static Public Member Functions
static ltsmin_state	true_state ()
	Returns the state representing `true`.

static ltsmin_state	false_state ()
	Returns the state representing `false`.

Protected Member Functions
ltsmin_state	get_state (const propositional_variable_instantiation &expr) const
	Returns a PBES_State object for `expr`.

std::string	data_to_string (const data::data_expression &e)
	Returns a string representation for the data expression `e`.

data::data_expression	string_to_data (const std::string &s)
	Returns a data expression for the string representation `s`.

int	get_value_index (int type_no, const data_expression &value)
	Returns the index of `value` in the local store for the data type with number `type_no`. The value is added to the store if it is not already present.

const data_expression &	get_data_value (int type_no, int index)
	Returns the value at position `index` in the local store for the data type with number `type_no`. An exception is thrown if the index does not exist in the store.

Protected Attributes
detail::pbes_greybox_interface *	pgg
	the PBES greybox interface

Private Attributes
pbes	p

lts_info *	info

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

std::vector< std::string >	localmap_int2string

std::vector< std::map< data_expression, int > >	localmaps_data2int

std::vector< std::vector< data_expression > >	localmaps_int2data

Detailed Description

Definition at line 424 of file pbes_explorer.h.

Member Typedef Documentation

◆ operation_type

using mcrl2::pbes_system::explorer::operation_type = parity_game_generator::operation_type

The expression type of the equation.

Definition at line 428 of file pbes_explorer.h.

Constructor & Destructor Documentation

◆ explorer() [1/2]

mcrl2::pbes_system::explorer::explorer	(	const std::string &	filename,
		const std::string &	rewrite_strategy = `"jittyc"`,
		bool	reset_flag = `false`,
		bool	always_split_flag = `false`
	)

Constructor.

explorer

Parameters

filename	the name of a PBES file.
rewrite_strategy	the name of the data rewrite strategy to use.
reset_flag	if set, irrelevant parts of the state vector will be reset to a default value
always_split_flag	if set, equations will always be split into conjuncts or disjuncts to form transition groups, if not set (default) the explorer assumes the pbes to be generated with lps2pbes -p and splits accordingly.

Definition at line 1300 of file pbes_explorer.cpp.

◆ explorer() [2/2]

mcrl2::pbes_system::explorer::explorer	(	const pbes &	p_,
		const std::string &	rewrite_strategy = `"jittyc"`,
		bool	reset_flag = `false`,
		bool	always_split_flag = `false`
	)

Constructor.

Parameters

p_	a PBES.
rewrite_strategy	String representing the rewrite strategy to use for the data rewriter.
reset_flag	if set, irrelevant parts of the state vector will be reset to a default value
always_split_flag	if set, equations will always be split into conjuncts or disjuncts to form transition groups, if not set (default) the explorer assumes the pbes to be generated with lps2pbes -p and splits accordingly.

Definition at line 1321 of file pbes_explorer.cpp.

◆ ~explorer()

mcrl2::pbes_system::explorer::~explorer ( )

Destructor.

Definition at line 1335 of file pbes_explorer.cpp.

Member Function Documentation

◆ data_to_string()

std::string mcrl2::pbes_system::explorer::data_to_string ( const data::data_expression & e )

protected

Returns a string representation for the data expression e.

Parameters

e	a PBES expression that may be in internal format.

Returns: a string representation without internal rewriter quirks.

◆ false_state()

ltsmin_state mcrl2::pbes_system::explorer::false_state ( )

inlinestatic

Returns the state representing false.

Definition at line 1379 of file pbes_explorer.cpp.

◆ from_state_vector()

ltsmin_state mcrl2::pbes_system::explorer::from_state_vector ( int *const & src )

Transforms a state vector src into a PBES_State object object containing the variable and parameter values that are represented by the indices in src.

Parameters

src	an int array containg the indices of the state values.

Returns: a PBES_State object containing the variable and parameter values that are represented by the indices in src.

Definition at line 1565 of file pbes_explorer.cpp.

◆ get_data_value()

const data_expression & mcrl2::pbes_system::explorer::get_data_value	(	int	type_no,
		int	index
	)

protected

Returns the value at position index in the local store for the data type with number type_no. An exception is thrown if the index does not exist in the store.

Parameters

type_no	the number of the value type.
index	an index.

Returns: the value at position index in local store type_no.

Definition at line 1553 of file pbes_explorer.cpp.

◆ get_index()

int mcrl2::pbes_system::explorer::get_index	(	int	type_no,
		const std::string &	s
	)

Returns the index of value in the local store for the data type with number type_no. Type 0 is reserved for the string representations of variable names. The value is added to the store if it is not already present.

Parameters

type_no	The number of the value type.
s	A string representation of the data value.

Returns: The index of value in local store type_no.

Definition at line 1392 of file pbes_explorer.cpp.

◆ get_info()

lts_info * mcrl2::pbes_system::explorer::get_info ( ) const

Returns the PBES_Info object.

Definition at line 1342 of file pbes_explorer.cpp.

◆ get_initial_state()

ltsmin_state mcrl2::pbes_system::explorer::get_initial_state ( ) const

Returns the initial state.

Definition at line 1348 of file pbes_explorer.cpp.

◆ get_state()

ltsmin_state mcrl2::pbes_system::explorer::get_state ( const propositional_variable_instantiation & expr ) const

protected

Returns a PBES_State object for expr.

Parameters

expr	a propositional variable instantiation expression.

Definition at line 1363 of file pbes_explorer.cpp.

◆ get_string_index()

int mcrl2::pbes_system::explorer::get_string_index ( const std::string & s )

Returns the index of s in the local store for string values. This store is reserved for the string representations of variable names. The value is added to the store if it is not already present.

Parameters

s	The string for which the index needs to be retrieved.

Returns: the index of s in the local store for string values.

Definition at line 1406 of file pbes_explorer.cpp.

◆ get_string_value()

const std::string & mcrl2::pbes_system::explorer::get_string_value ( int index )

Returns the string at position index in the local store for string values. An exception is thrown if the index does not exist in the store.

Parameters

index an index.

Returns: the string value at position index in the local store for string values.

Definition at line 1543 of file pbes_explorer.cpp.

◆ get_successors() [1/2]

std::vector< ltsmin_state > mcrl2::pbes_system::explorer::get_successors ( const ltsmin_state & state )

Computes successor states for a state. Serves as a wrapper around the get_successors function of the pbes_greybox_interface.

Parameters

state the source state.

Returns: a list of successor states.

Definition at line 1603 of file pbes_explorer.cpp.

◆ get_successors() [2/2]

std::vector< ltsmin_state > mcrl2::pbes_system::explorer::get_successors	(	const ltsmin_state &	state,
		int	group
	)

Computes successor states for a state as defined in transition group group. Serves as a wrapper around the get_successors function of the pbes_greybox_interface.

Parameters

state	the source state.
group	the group for which the successor states are computed.

Returns: a list of successor states.

Definition at line 1646 of file pbes_explorer.cpp.

◆ get_value()

std::string mcrl2::pbes_system::explorer::get_value	(	int	type_no,
		int	index
	)

Returns the value at position index in the local store for the data type with number type_no. Type 0 is reserved for the string representations of variable names. An exception is thrown if the index does not exist in the store.

Parameters

type_no	the number of the value type.
index	an index.

Returns: a string representation of the value at position index in local store type_no.

Definition at line 1528 of file pbes_explorer.cpp.

◆ get_value_index()

int mcrl2::pbes_system::explorer::get_value_index	(	int	type_no,
		const data_expression &	value
	)

protected

Returns the index of value in the local store for the data type with number type_no. The value is added to the store if it is not already present.

Parameters

type_no	the number of the value type.
value	the data value.

Returns: the index of value in local store type_no.

Definition at line 1421 of file pbes_explorer.cpp.

◆ initial_state()

void mcrl2::pbes_system::explorer::initial_state ( int * state )

Definition at line 1355 of file pbes_explorer.cpp.

◆ next_state_all()

template<typename callback >

void mcrl2::pbes_system::explorer::next_state_all	(	int *const &	src,
		callback &	cb
	)

inline

Iterates over the successors of a state and invokes a callback function for each successor state.

Parameters

src	an int array containg the indices of the state values.
cb	a callback function that must provide the function operator() with the following interface:

void operator()(int* const& next_state, int group);

where

next_state is the target state of the transition
group is the number of the transition group, or -1 if it is unknown which group

Definition at line 571 of file pbes_explorer.h.

◆ next_state_long()

template<typename callback >

void mcrl2::pbes_system::explorer::next_state_long	(	int *const &	src,
		int	group,
		callback &	cb
	)

inline

Iterates over the successors of a state for a certain transition group and invokes a callback function for each successor state.

Parameters

src	an int array containg the indices of the state values.
group	the transition group
cb	a callback function that must provide the function operator() with the following interface:

void operator()(int* const& next_state, int group);

where

next_state is the target state of the transition
group is the number of the transition group, or -1 if it is unknown which group

Definition at line 605 of file pbes_explorer.h.

◆ string_to_data()

data::data_expression mcrl2::pbes_system::explorer::string_to_data ( const std::string & s )

protected

Returns a data expression for the string representation s.

Parameters

s	a string representation of a data expression.

Returns: the data expression (possibly in internal format) that s represents.

Definition at line 1385 of file pbes_explorer.cpp.

◆ to_state_vector()

void mcrl2::pbes_system::explorer::to_state_vector	(	const ltsmin_state &	dst_state,
		int *	dst,
		const ltsmin_state &	src_state,
		int *const &	src
	)

Transforms a PBES state to a state vector, represented by an array of integers.

Parameters

dst_state	the new PBES state object
dst	the int array to which the state vector is written
src_state	the source PBES state object, used to check which fields have been changed.
src	an array which is used for default values, to prevent unused variables for being reset. the non-resetting behaviour can be turned off by the –reset option.

Definition at line 1437 of file pbes_explorer.cpp.

◆ true_state()

ltsmin_state mcrl2::pbes_system::explorer::true_state ( )

inlinestatic

Returns the state representing true.

Definition at line 1373 of file pbes_explorer.cpp.

Member Data Documentation

◆ info

lts_info* mcrl2::pbes_system::explorer::info

private

Definition at line 432 of file pbes_explorer.h.

◆ localmap_int2string

std::vector<std::string> mcrl2::pbes_system::explorer::localmap_int2string

private

Definition at line 434 of file pbes_explorer.h.

◆ localmap_string2int

std::map<std::string,int> mcrl2::pbes_system::explorer::localmap_string2int

private

Definition at line 433 of file pbes_explorer.h.

◆ localmaps_data2int

std::vector<std::map<data_expression,int> > mcrl2::pbes_system::explorer::localmaps_data2int

private

Definition at line 435 of file pbes_explorer.h.

◆ localmaps_int2data

std::vector<std::vector<data_expression> > mcrl2::pbes_system::explorer::localmaps_int2data

private

Definition at line 436 of file pbes_explorer.h.

◆ p

pbes mcrl2::pbes_system::explorer::p

private

Definition at line 431 of file pbes_explorer.h.

◆ pgg

detail::pbes_greybox_interface* mcrl2::pbes_system::explorer::pgg

protected

the PBES greybox interface

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

Protected Attributes

Private Attributes

Detailed Description

Member Typedef Documentation

◆ operation_type

Constructor & Destructor Documentation

◆ explorer() [1/2]

◆ explorer() [2/2]

◆ ~explorer()

Member Function Documentation

◆ data_to_string()

◆ false_state()

◆ from_state_vector()

◆ get_data_value()

◆ get_index()

◆ get_info()

◆ get_initial_state()

◆ get_state()

◆ get_string_index()

◆ get_string_value()

◆ get_successors() [1/2]

◆ get_successors() [2/2]

◆ get_value()

◆ get_value_index()

◆ initial_state()

◆ next_state_all()

◆ next_state_long()

◆ string_to_data()

◆ to_state_vector()

◆ true_state()

Member Data Documentation

◆ info

◆ localmap_int2string

◆ localmap_string2int

◆ localmaps_data2int

◆ localmaps_int2data

◆ p

◆ pgg