mcrl2::pbes_system::lts_info

Include file:

#include "mcrl2/pbes/pbes_explorer.h
class mcrl2::pbes_system::lts_info

Public types

type operation_type

typedef for parity_game_generator::operation_type

The variable sequence type.

Friends

friend class explorer

friend class ltsmin_state

Private attributes

bool always_split_option
std::map<int, std::vector<bool>> matrix
int number_of_groups
pbes &p
std::vector<data_expression> param_default_values
std::map<std::string, int> param_index
detail::pbes_greybox_interface *pgg
std::map<int, std::vector<bool>> read_matrix
bool reset_option
std::vector<pbes_expression> transition_expression
std::vector<pbes_expression> transition_expression_plain
std::vector<operation_type> transition_type
std::vector<std::string> transition_variable_name
lts_type type
std::map<std::string, pbes_expression> variable_expression
std::map<std::string, std::map<int, int>> variable_parameter_index_positions
std::map<std::string, std::vector<int>> variable_parameter_indices
std::map<std::string, std::vector<std::string>> variable_parameter_signatures
std::map<std::string, data::variable_list> variable_parameters
std::map<std::string, int> variable_priority
std::map<std::string, fixpoint_symbol> variable_symbol
std::map<std::string, operation_type> variable_type
std::map<std::string, propositional_variable> variables
std::map<int, std::vector<bool>> write_matrix

Private static attributes

std::map<variable, std::string> 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.