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.