mcrl2::pbes_system::weak_bisimulation_algorithm¶
Include file:
#include "mcrl2/pbes/bisimulation.h
-
class
mcrl2::pbes_system::weak_bisimulation_algorithm¶ Algorithm class for weak bisimulation.
Protected attributes¶
-
data::set_identifier_generator
mcrl2::pbes_system::weak_bisimulation_algorithm::m_generator¶
Public member functions¶
-
pbes_expression
close1(const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const¶ The close1 function.
Parameters:
- p A linear process
- q A linear process
- i A summand iterator
Returns: The function result
-
pbes_expression
close2(const lps::linear_process &p, const lps::linear_process &q, my_iterator i, const data::data_expression_list &d, const data::data_expression_list &d1) const¶ The close function.
Parameters:
- p A linear process
- q A linear process
- i A summand iterator
- d A sequence of data expressions
- d1 A sequence of data expressions
Returns: The function result
-
pbes_expression
match(const lps::linear_process &p, const lps::linear_process &q) const The match function.
Parameters:
- p A linear process
- q A linear process
Returns: The function result
-
pbes
run(const lps::specification &model, const lps::specification &spec) Runs the algorithm.
Parameters:
- model A linear process specification
- spec A linear process specification
Returns: A pbes that expresses weak bisimulation between two specifications.
-
pbes_expression
step(const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const The step function.
Parameters:
- p A linear process
- q A linear process
- i A summand iterator
Returns: The function result
