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 datar

Data rewriter.

std::unordered_set<propositional_variable_instantiation> discovered

The propositional variable instantiations that have been discovered (not necessarily handled).

propositional_variable_instantiation init

The initial value (after rewriting).

pbes_equation_index m_equation_index

A lookup map for PBES equations.

std::size_t m_iteration_count

const pbessolve_options &m_options

Algorithm options.

pbes m_pbes

A PBES.

enumerate_quantifiers_rewriter R

The rewriter.

pbesinst_lazy_todo todo

The propositional variable instantiations that need to be handled.

Protected member functions

void add_assignments(const data::variable_list &v, const data::data_expression_list &e, data::mutable_indexed_substitution<> &sigma)

Adds the assignments [v := e] to sigma.

Parameters:

• v A sequence of data variables
• e A sequence of data expressions
• sigma The substitution that maps the i-th element of v to the i-th element of e

pbes preprocess(const pbes &x) const

std::string print_equation_count(std::size_t size) const

Prints a log message for every 1000-th equation.

void remove_assignments(const data::variable_list &v, data::mutable_indexed_substitution<> &sigma)

Removes assignments to variables in v from sigma.

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

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