|
| 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 |
|
void | on_report_equation (const std::size_t thread_index, 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 | 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.
|
|
| 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 () |
|
Adds an optimization to pbesinst_structure_graph.
Definition at line 73 of file pbesinst_structure_graph2.h.