mcrl2::pbes_system::pbesinst_structure_graph_algorithm¶

Include file:

#include "mcrl2/pbes/pbesinst_structure_graph.h

class mcrl2::pbes_system::pbesinst_structure_graph_algorithm¶: Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the structure graph that is passed in the constructor.

Protected attributes¶

detail::structure_graph_builder mcrl2::pbes_system::pbesinst_structure_graph_algorithm::m_graph_builder¶

Protected member functions¶

void SG0(const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k, std::shared_mutex &realloc_mutex)¶

structure_graph::index_type SG1(const pbes_expression &psi, std::shared_mutex &realloc_mutex)¶

std::string status_message(std::size_t equation_count) override

Public member functions¶

void on_report_equation(const std::size_t, std::shared_mutex &realloc_mutex, const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) override: Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.

pbesinst_structure_graph_algorithm(const pbessolve_options &options, const pbes &p, structure_graph &G)¶

void run() override: Runs the algorithm. The result is obtained by calling the function get_result.