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 mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::super

typedef for pbesinst_structure_graph_algorithm

Protected attributes

pbes_expression mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::b
detail::computation_guard mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::fatal_attractors_guard
detail::computation_guard mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::find_loops_guard
detail::periodic_guard mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::reset_guard
std::array<vertex_set, 2> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::S
std::array<detail::computation_guard, 2> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::S_guard
std::array<strategy_vector, 2> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::tau

Protected member functions

pbes_expression expr(const T &x) const
void prune_todo_list(const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t regeneration_period)
Rplus_traverser::stack_element Rplus(const pbes_expression &x)
bool solution_found(const propositional_variable_instantiation &init) const override
bool strategies_are_set_in_solved_nodes() const
bool todo_has_only_undefined_nodes() 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