mCRL2
|
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. More...
#include <pbesinst_structure_graph.h>
Public Member Functions | |
pbesinst_structure_graph_algorithm (const pbessolve_options &options, const pbes &p, structure_graph &G) | |
void | on_report_equation (const std::size_t, 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. | |
void | run () override |
Runs the algorithm. The result is obtained by calling the function get_result . | |
![]() | |
pbesinst_lazy_algorithm (const pbessolve_options &options, const pbes &p) | |
Constructor. | |
virtual | ~pbesinst_lazy_algorithm ()=default |
virtual void | on_report_equation (const std::size_t, const propositional_variable_instantiation &, const pbes_expression &, std::size_t) |
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. | |
virtual void | on_discovered_elements (const std::set< propositional_variable_instantiation > &) |
This function is called when new elements are added to discovered. | |
virtual void | on_end_while_loop () |
This function is called right after the while loop is finished. | |
void | next_todo (propositional_variable_instantiation &result) |
const fixpoint_symbol & | symbol (std::size_t i) const |
virtual void | rewrite_psi (const std::size_t, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) |
virtual bool | solution_found (const propositional_variable_instantiation &) const |
virtual void | run_thread (const std::size_t thread_index, pbesinst_lazy_todo &todo, std::atomic< std::size_t > &number_of_active_processes, data::mutable_indexed_substitution<> sigma, enumerate_quantifiers_rewriter R) |
virtual void | run () |
Runs the algorithm. The result is obtained by calling the function get_result . | |
const pbes_equation_index & | equation_index () const |
enumerate_quantifiers_rewriter & | rewriter () |
Protected Member Functions | |
void | SG0 (const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) |
structure_graph::index_type | SG1 (const pbes_expression &psi) |
std::string | status_message (std::size_t equation_count) override |
![]() | |
virtual std::string | status_message (std::size_t equation_count) |
pbes | preprocess (const pbes &x) const |
data::rewriter | construct_rewriter (const pbes &pbesspec) |
Protected Attributes | |
detail::structure_graph_builder | m_graph_builder |
![]() | |
const pbessolve_options & | m_options |
Algorithm options. | |
data::rewriter | datar |
Data rewriter. | |
pbes | m_pbes |
A PBES. | |
pbes_equation_index | m_equation_index |
A lookup map for PBES equations. | |
pbesinst_lazy_todo | todo |
The propositional variable instantiations that need to be handled. | |
atermpp::indexed_set< propositional_variable_instantiation, true > | discovered |
The propositional variable instantiations that have been discovered (not necessarily handled). | |
propositional_variable_instantiation | init |
The initial value (after rewriting). | |
std::size_t | m_iteration_count = 0 |
enumerate_quantifiers_rewriter | m_global_R |
The rewriter. | |
utilities::mutex | m_todo_access |
volatile bool | m_must_abort = false |
Additional Inherited Members | |
![]() | |
static void | rewrite_true_false (pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) |
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.
Definition at line 28 of file pbesinst_structure_graph.h.
|
inline |
Definition at line 114 of file pbesinst_structure_graph.h.
|
inlineoverridevirtual |
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.
Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.
Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.
Definition at line 123 of file pbesinst_structure_graph.h.
|
inlineoverridevirtual |
Runs the algorithm. The result is obtained by calling the function get_result
.
Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.
Definition at line 137 of file pbesinst_structure_graph.h.
|
inlineprotected |
Definition at line 33 of file pbesinst_structure_graph.h.
|
inlineprotected |
Definition at line 67 of file pbesinst_structure_graph.h.
|
inlineoverrideprotectedvirtual |
Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.
Definition at line 101 of file pbesinst_structure_graph.h.
|
protected |
Definition at line 31 of file pbesinst_structure_graph.h.