mcrl2::pbes_system::bisimulation_algorithm

Include file:

#include "mcrl2/pbes/bisimulation.h

class mcrl2::pbes_system::bisimulation_algorithm

Base class for bisimulation algorithms.

Public types

type mcrl2::pbes_system::bisimulation_algorithm::my_iterator

typedef for lps::action_summand_vector::const_iterator

The iterator type for non-delta summands.

Protected types

type mcrl2::pbes_system::bisimulation_algorithm::name_map

typedef for std::map< const lps::action_summand *, std::string >

A map type for mapping summands to strings.

Protected attributes

const lps::linear_process *mcrl2::pbes_system::bisimulation_algorithm::model_ptr

Store the address of the model.

name_map mcrl2::pbes_system::bisimulation_algorithm::summand_names

Maps summands to strings.

Protected member functions

std::string action_list_name(const process::action_list &l) const

Generates a name for an action_list.

Parameters:

• l A sequence of actions

Returns: A string representation of the list l

bool is_from_model(const lps::linear_process &p) const

Returns true if p is the linear process of the model.

Parameters:

• p A linear process

Returns: True if p is the linear process of the model.

void make_substitution(const data::variable_list &v, const data::data_expression_list &e, data::mutable_map_substitution<> &result) const

std::string process_name(const lps::linear_process &p) const

Returns a name of a linear process.

Parameters:

• p A linear process

Returns: The name of the linear process.

void set_summand_names(const lps::linear_process &p)

Used for initializing summand names.

Parameters:

• p A linear process

std::string summand_name(my_iterator i) const

Returns the name of a summand.

Parameters:

• i A summand iterator

Returns: The name of the summand referred to by i

Public member functions

pbes build_pbes(const std::vector<pbes_equation> &equations, const lps::specification &M, const lps::specification &S)

Builds a pbes from the given equations.

Parameters:

• equations A sequence of pbes equations
• M A specification
• S A specification

Returns: The constructed pbes

data::mutable_map_substitution compute_process_parameter_name_clashes(const lps::specification &p, const lps::specification &q) const

Returns a substitution of variables in q such that there are no name clashes between p and q.

Parameters:

• p A linear process specification
• q A linear process specification

Returns: A substitution that should be applied to q to remove name clashes between p and q.

After this substitution the following holds: [ ((param(p)cup glob(p))cap ((param(q)cup glob(q))=emptyset ] where param(p) denotes p.process().process_parameters() and glob(p) denotes p.global_variables().

data::mutable_map_substitution compute_summand_variable_name_clashes(const lps::specification &p, const lps::specification &q) const

Returns a substitution of variables in q such that there are no name clashes between the summation variables of p and q.

Parameters:

• p A linear process specification
• q A linear process specification

Returns: A substitution that should be applied to q to remove name clashes between p and q.

pbes_expression equals(const lps::multi_action &a, const lps::multi_action &b) const

Returns a pbes expression that expresses equality of the multi-actions a and b.

Parameters:

• a A sequence of actions
• b A sequence of actions

Returns: Necessary conditions for the equality of a and b

void init(const lps::linear_process &model, const lps::linear_process &spec)

Initializes the name lookup table.

Parameters:

• model A linear process
• spec A linear process

Pre: model and spec must have the same data specification

fixpoint_symbol mu() const

Returns the fixpoint symbol mu.

Returns: The fixpoint symbol mu.

fixpoint_symbol nu() const

Returns the fixpoint symbol nu.

Returns: The fixpoint symbol nu.

void resolve_name_clashes(const lps::specification &model, lps::specification &spec, bool include_summand_variables = false)

Resolves name clashes between model and spec.

propositional_variable_instantiation var(const core::identifier_string &name, const data::data_expression_list &parameters) const

Creates a propositional variable.

Parameters:

• name A
• parameters A sequence of data expressions

Returns: The created propositional variable

propositional_variable_instantiation var(const core::identifier_string &name, const data::variable_list &parameters) const

Creates a propositional variable.

Parameters:

• name A
• parameters A sequence of data variables

Returns: The created propositional variable

core::identifier_string X(const lps::linear_process &p, const lps::linear_process &q) const

Creates a name for the propositional variable Xpq.

Parameters:

• p A linear process
• q A linear process

Returns: The name for the propositional variable Xpq

core::identifier_string Y(const lps::linear_process &p, const lps::linear_process &q) const

Creates a name for the propositional variable Ypq.

Parameters:

• p A linear process
• q A linear process

Returns: The name for the propositional variable Ypq

core::identifier_string Y(const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const

Creates a name for the propositional variable Ypqi.

Pre: The iterator i must be in p.action_summands().

Parameters:

• p A linear process
• q A linear process
• i A summand iterator

Returns: The name for the propositional variable Ypqi

core::identifier_string Y1(const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const

Creates a name for the propositional variable Y1pqi.

Pre: The iterator i must be in p.action_summands().

Parameters:

• p A linear process
• q A linear process
• i A summand iterator

Returns: The name for the propositional variable Y1pqi

core::identifier_string Y2(const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const

Creates a name for the propositional variable Y2pqi.

Pre: The iterator i must be in p.action_summands().

Parameters:

• p A linear process
• q A linear process
• i A summand iterator

Returns: The name for the propositional variable Y2pqi