mcrl2::pbes_system::strong_bisimulation_algorithm

Include file:

#include "mcrl2/pbes/bisimulation.h
class mcrl2::pbes_system::strong_bisimulation_algorithm

Algorithm class for strong bisimulation.

Public member functions

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 strong bisimulation between stwo 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