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¶

atermpp::vector<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 std::size_t thread_index, 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_algorithm2(const pbessolve_options &options, const pbes &p, structure_graph &G)¶

void rewrite_psi(const std::size_t thread_index, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) override