mcrl2::pbes_system::branching_bisimulation_algorithm

Include file:

#include "mcrl2/pbes/bisimulation.h

class mcrl2::pbes_system::branching_bisimulation_algorithm

Algorithm class for branching bisimulation.

Public member functions

pbes_expression close(const lps::linear_process &p, const lps::linear_process &q, my_iterator i) const

The close function.

Parameters:

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

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)

Returns a pbes that expresses branching bisimulation between two specifications.

Parameters:

• model A linear process specification
• spec A linear process specification

Returns: A pbes that expresses branching bisimulation between the 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