mcrl2::pbes_system::explorer

Include file:

#include "mcrl2/pbes/pbes_explorer.h

class mcrl2::pbes_system::explorer

Public types

type mcrl2::pbes_system::explorer::operation_type

typedef for parity_game_generator::operation_type

The expression type of the equation.

Private attributes

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

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

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

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

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

pbes mcrl2::pbes_system::explorer::p

Protected attributes

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

the PBES greybox interface

Protected member functions

std::string data_to_string(const data::data_expression &e)

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.

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.

Parameters:

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

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

ltsmin_state get_state(const propositional_variable_instantiation &expr) const

Returns a PBES_State object for expr.

Parameters:

• expr a propositional variable instantiation expression.

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.

Parameters:

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

Returns: the index of value in local store type_no.

data::data_expression string_to_data(const std::string &s)

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.

Public member functions

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

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.

explorer(const std::string &filename, const std::string &rewrite_strategy, bool reset_flag, bool always_split_flag)

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.

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.

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.

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.

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.

lts_info *get_info() const

Returns the PBES_Info object.

ltsmin_state get_initial_state() const

Returns the initial state.

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.

Parameters:

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

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

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.

Parameters:

• index an index.

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

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.

Parameters:

• state the source state.

Returns: a list of successor states.

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.

Parameters:

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

Returns: a list of successor states.

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.

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.

void initial_state(int *state)

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.

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:

voidoperator()(int*const&next_state,intgroup); 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

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.

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:

voidoperator()(int*const&next_state,intgroup); 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

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.

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.

~explorer()

Destructor.

Public static member functions

ltsmin_state false_state()

Returns the state representing false.

ltsmin_state true_state()

Returns the state representing true.