mcrl2::pbes_system::pbesinst_lazy_algorithm¶

Include file:

#include "mcrl2/pbes/pbesinst_lazy.h

class mcrl2::pbes_system::pbesinst_lazy_algorithm¶: A PBES instantiation algorithm that uses a lazy strategy.

Protected attributes¶

data::rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::datar¶: Data rewriter.

std::unordered_set<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_lazy_algorithm::discovered¶: The propositional variable instantiations that have been discovered (not necessarily handled).

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_lazy_algorithm::init¶: The initial value (after rewriting).

pbes_equation_index mcrl2::pbes_system::pbesinst_lazy_algorithm::m_equation_index¶: A lookup map for PBES equations.

std::size_t mcrl2::pbes_system::pbesinst_lazy_algorithm::m_iteration_count¶

const pbessolve_options &mcrl2::pbes_system::pbesinst_lazy_algorithm::m_options¶: Algorithm options.

pbes mcrl2::pbes_system::pbesinst_lazy_algorithm::m_pbes¶: A PBES.

enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::R¶: The rewriter.

pbesinst_lazy_todo mcrl2::pbes_system::pbesinst_lazy_algorithm::todo¶: The propositional variable instantiations that need to be handled.

Protected member functions¶

data::rewriter construct_rewriter(const pbes &pbesspec)¶

pbes preprocess(const pbes &x) const¶

virtual std::string status_message(std::size_t equation_count)¶

Protected static member functions¶

static pbes_expression rewrite_true_false(const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)¶

Public member functions¶

const pbes_equation_index &equation_index() const¶

propositional_variable_instantiation next_todo()

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.

virtual void 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.

virtual pbes_expression rewrite_psi(const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)¶

enumerate_quantifiers_rewriter &rewriter()

virtual void run(): Runs the algorithm. The result is obtained by calling the function get_result.

virtual bool solution_found(const propositional_variable_instantiation&) const¶

const fixpoint_symbol &symbol(std::size_t i) const¶

virtual ~pbesinst_lazy_algorithm() = default¶