mcrl2::pbes_system::lts_info

Include file:

#include "mcrl2/pbes/pbes_explorer.h

class mcrl2::pbes_system::lts_info

Public types

type mcrl2::pbes_system::lts_info::operation_type

typedef for parity_game_generator::operation_type

The variable sequence type.

Friends

friend class mcrl2::pbes_system::lts_info::explorer

friend class mcrl2::pbes_system::lts_info::ltsmin_state

Private attributes

bool mcrl2::pbes_system::lts_info::always_split_option

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

int mcrl2::pbes_system::lts_info::number_of_groups

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

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

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

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

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

bool mcrl2::pbes_system::lts_info::reset_option

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

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

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

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

lts_type mcrl2::pbes_system::lts_info::type

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

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

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

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

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

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

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

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

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

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

Private static attributes

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

Private member functions

void compute_dependency_matrix()

Computes dependency matrix from PBES.

void compute_lts_type()

Computes LTS Type from PBES.

void compute_transition_groups()

Computes transition groups from PBES.

int count_variables(const pbes_expression &e)

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.

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.

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.

Protected member functions

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

Computes the set of parameters changed in the expression.

Parameters:

• phi

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

Computes the set of parameters changed in the expression.

Parameters:

• phi
• L

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.

Parameters:

• expr

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.

Parameters:

• expr
• L

const data_expression &get_default_value(int index)

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.

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).

Parameters:

• params a sequence of variables.

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.

Parameters:

• params a sequence of variables.

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, data::variable_list> &get_variable_parameters() const

Returns the map from variable names to the sequence of parameters 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, propositional_variable> &get_variables() const

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

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

Constructor.

lts_info

Parameters:

• p
• pgg
• reset
• always_split

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

Computes the set of parameters reset in the expression.

Parameters:

• phi
• d

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

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

Parameters:

• expr

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.

Parameters:

• expr
• L

Protected static member functions

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

Computes the free variables read in an expression.

Parameters:

• expr

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

Converts a variable_sequence_type into a sequence of parameter signatures.

Parameters:

• params a sequence of variables.

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

Converts a variable_sequence_type into a set of parameter signatures.

Parameters:

• params a sequence of variables.

std::string get_param_signature(const variable &param)

Returns a signature for parameter param.

Parameters:

• param a parameter.

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

Computes the propositional variables used in an expression.

Parameters:

• expr

bool tf(const pbes_expression &phi)

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

Parameters:

• phi a PBES expression

Public member functions

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

Returns the 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.

Parameters:

• signature The parameter signature.

const lts_type &get_lts_type() const

Returns the LTS Type.

int get_number_of_groups() const

Returns the number of transition groups.

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

Returns the read dependency matrix.

bool get_reset_option() const

Returns if the reset option is set.

const std::vector<lts_info::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::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::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 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::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, 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, lts_info::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<int, std::vector<bool>> &get_write_matrix() const

Returns the write dependency matrix.

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.

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)) ).

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.

Parameters:

• group the number of the transition group.

Returns: true.

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.

Parameters:

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

Returns: true if param_part in changed(expr(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.

Parameters:

• group the number of the transition group.

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

std::string state_to_string(const ltsmin_state &state)

Returns a string representation for state state.

Parameters:

• state

Public static member functions

std::string get_param_signature(const std::string &paramname, const std::string &paramtype)

Returns a signature using name and type of a parameter.

Parameters:

• paramname the parameter name.
• paramtype the parameter type.