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.

atermpp::indexed_set<propositional_variable_instantiation, true> 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.

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

std::shared_mutex mcrl2::pbes_system::pbesinst_lazy_algorithm::m_graph_access¶

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

bool mcrl2::pbes_system::pbesinst_lazy_algorithm::m_must_abort¶

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

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

std::mutex mcrl2::pbes_system::pbesinst_lazy_algorithm::m_todo_access¶

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 void rewrite_true_false(pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)¶

Public member functions¶

const pbes_equation_index &equation_index() const¶

void next_todo(propositional_variable_instantiation &result)¶

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 std::size_t, std::shared_mutex&, 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 void rewrite_psi(const std::size_t, pbes_expression &result, 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 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 bool solution_found(const propositional_variable_instantiation&) const¶

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

virtual ~pbesinst_lazy_algorithm() = default¶