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