mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm

Include file:

#include "mcrl2/pbes/pbesinst_alternative_lazy_algorithm.h

class mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm

An alternative lazy algorithm for instantiating a PBES, ported from bes_deprecated.h.

Public types

type mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::pbes_expression_pair

typedef for std::pair< pbes_expression, pbes_expression >

Protected attributes

std::unordered_map<propositional_variable_instantiation, pbes_expression> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::equation

Map a variable instantiation to its right hand side.

std::unordered_map<core::identifier_string, std::size_t> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::equation_index

A lookup map for PBES equations.

propositional_variable_instantiation mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::init

The initial value.

std::vector<std::vector<propositional_variable_instantiation>> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::instantiations

instantiations[i] contains all instantiations of the variable of the i-th equation in the PBES.

const bool mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_approximate_true

The variable m_approximimate_true indicates whether boolean variables that cannot be dealt with as the todo buffer would otherwise exceeds m_maximum_todo_size are set to true or to false

const data::data_specification &mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_data_spec

const data::rewriter &mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_datar

Data rewriter.

std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_elements_not_stored_in_todo_buffer

When the todo buffer is limited, due to m_maximum_todo_size, then the variable below counts how many elements are dropped out of the todo buffer.

const mcrl2::bes::remove_level mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_erase_unused_bes_variables

Indicate to which extent explored bes equations that turn out not to reachable can be thrown away. Values are: none, some or all.

const std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_maximum_todo_size

The maximum size that the todo buffer is allowed to have.

search_strategy mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_search_strategy

The search strategy to use when exploring the state space.

transformation_strategy mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_transformation_strategy

Transformation strategy.

std::unordered_map<propositional_variable_instantiation, std::unordered_set<propositional_variable_instantiation>> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::occurrence

Map a variable instantiation to a set of other variable instantiations on whose right hand sides it appears.

enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::R

The rewriter.

std::vector<std::size_t> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::ranks

ranks[i] contains the rank of the i-th equation in the PBES.

std::vector<fixpoint_symbol> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::symbols

symbols[i] contains the fixedpoint symbol of the i-th equation in the PBES.

std::deque<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::todo

Propositional variable instantiations that need to be handled.

std::unordered_set<propositional_variable_instantiation> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::todo_set

The content of todo as a set.

std::unordered_map<propositional_variable_instantiation, pbes_expression> mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::trivial

Map a variable instantiations to its right hand side when the latter is trivial (either true or false).

Protected static attributes

const std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::regeneration_count_init

Initial value for regeneration_period.

Protected member functions

void print_equation_count(const std::size_t nr_of_processed_variables, const std::size_t nr_of_generated_variables, const std::size_t todo_size) const

Prints a log message for every 1000-th equation.

Public member functions

void add_todo(const propositional_variable_instantiation &X)

bool find_loop(pbes_expression expr, propositional_variable_instantiation X)

bool find_loop_rec(const pbes_expression &expr, propositional_variable_instantiation X, std::size_t rank, std::unordered_map<propositional_variable_instantiation, bool> &visited)

std::size_t get_rank(const propositional_variable_instantiation &X)

pbes get_result(bool short_rename_scheme = true)

Returns the computed bes in pbes format.

Returns: The computed bes in pbes format

propositional_variable_instantiation next_todo()

pbesinst_alternative_lazy_algorithm(const data::data_specification &data_spec, const data::rewriter &datar, search_strategy search_strategy = breadth_first, transformation_strategy transformation_strategy = lazy, const mcrl2::bes::remove_level erase_unused_bes_variables = mcrl2::bes::none, const std::size_t maximum_todo_size = std::numeric_limits<std::size_t>::max(), const bool approximate_true = true)

Constructor.

Parameters:

• data_spec A data specification.
• datar A data rewriter.
• search_strategy A search strategy (e.g. breadth_first).
• transformation_strategy A strategy to transform the PBES into a BES.
• erase_unused_bes_variables An indicator how often unreachable variables must be garbage collected.
• maximum_todo_size An indication of the maximal size of the stack with explorable BES variables. If the stack exceeds this size, the ignored variable is set to true or false, depending on the parameter approximate_true.
• approximate_true If true BES variables that are not investigated are set to false. If false these variables are set to true.

void regenerate_states()

enumerate_quantifiers_rewriter &rewriter()

void run(pbes &p)

Runs the algorithm. The result is obtained by calling the function get_result.

Parameters:

• p A PBES

pbes_expression_pair simplify_pbes_expression(const pbes_expression &p, const std::unordered_map<propositional_variable_instantiation, pbes_expression> &trivial)