Include file:
#include "mcrl2/pbes/pbesinst_lazy.h
mcrl2::pbes_system::
pbesinst_lazy_algorithm
¶A PBES instantiation algorithm that uses a lazy strategy.
mcrl2::pbes_system::pbesinst_lazy_algorithm::
datar
¶Data rewriter.
mcrl2::pbes_system::pbesinst_lazy_algorithm::
discovered
¶The propositional variable instantiations that have been discovered (not necessarily handled).
mcrl2::pbes_system::pbesinst_lazy_algorithm::
init
¶The initial value (after rewriting).
mcrl2::pbes_system::pbesinst_lazy_algorithm::
m_equation_index
¶A lookup map for PBES equations.
mcrl2::pbes_system::pbesinst_lazy_algorithm::
m_iteration_count
¶mcrl2::pbes_system::pbesinst_lazy_algorithm::
m_options
¶Algorithm options.
mcrl2::pbes_system::pbesinst_lazy_algorithm::
m_pbes
¶A PBES.
mcrl2::pbes_system::pbesinst_lazy_algorithm::
R
¶The rewriter.
mcrl2::pbes_system::pbesinst_lazy_algorithm::
todo
¶The propositional variable instantiations that need to be handled.
rewrite_true_false
(const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)¶equation_index
() const¶next_todo
()on_discovered_elements
(const std::set<propositional_variable_instantiation>&)¶This function is called when new elements are added to discovered.
on_end_while_loop
()¶This function is called right after the while loop is finished.
on_report_equation
(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.
pbesinst_lazy_algorithm
(const pbessolve_options &options, const pbes &p)¶Constructor.
Parameters:
p The pbes used in the exploration algorithm.
rewrite_strategy A strategy for the data rewriter.
search_strategy The search strategy used to explore the pbes, typically depth or breadth first.
optimization An indication of the optimisation level.
rewrite_psi
(const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)¶rewriter
()run
()Runs the algorithm. The result is obtained by calling the function get_result.
solution_found
(const propositional_variable_instantiation&) const¶symbol
(std::size_t i) const¶~pbesinst_lazy_algorithm
() = default¶