mcrl2::pbes_system::pbesinst_structure_graph_algorithm2

Include file:

#include "mcrl2/pbes/pbesinst_structure_graph2.h
class mcrl2::pbes_system::pbesinst_structure_graph_algorithm2

Adds an optimization to pbesinst_structure_graph.

Public types

type super

typedef for pbesinst_structure_graph_algorithm

Protected attributes

pbes_expression b
detail::computation_guard fatal_attractors_guard
detail::computation_guard find_loops_guard
detail::periodic_guard reset_guard
vertex_set S0
detail::computation_guard S0_guard
vertex_set S1
detail::computation_guard S1_guard

Protected member functions

void compute_attractor_set_S0(const simple_structure_graph &G)
void compute_attractor_set_S1(const simple_structure_graph &G)
pbes_expression expr(const T &x) const
bool has_successor_not_in(const simple_structure_graph &G, const structure_graph::index_type u, const vertex_set &S0, const vertex_set &S1, const std::unordered_set<pbes_expression> &done) const
void prune_todo_list(const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t regeneration_period)
std::pair<pbes_expression, pbes_expression> Rplus(const pbes_expression &x)
bool solution_found(const propositional_variable_instantiation &init) const override
bool successors_disjoint(const simple_structure_graph &G, const structure_graph::index_type u, const vertex_set &S) const

Public member functions

void on_discovered_elements(const std::set<propositional_variable_instantiation> &elements) override

This function is called when new elements are added to discovered.

void on_end_while_loop() override

This function is called right after the while loop is finished.

void on_report_equation(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_algorithm2(const pbessolve_options &options, const pbes &p, structure_graph &G)
pbes_expression rewrite_psi(const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) override