Include file:

#include "mcrl2/pbes/pbesinst_symbolic.h
class mcrl2::pbes_system::pbesinst_symbolic_algorithm

Algorithm class for the symbolic_exploration instantiation algorithm.

Public types

type state_type

typedef for propositional_variable_instantiation

Protected attributes

data::rewriter datar

Data rewriter.

std::set<state_type> done

Propositional variable instantiations that have been handled.

std::multimap<state_type, state_type> edges

Data structure for storing the result. E[i] corresponds to the equations generated from the i-th PBES equation.

state_type init

The initial value.

std::map<core::identifier_string, std::size_t> m_equation_index

A lookup map for PBES equations.

pbes &m_pbes

The PBES that is being instantiated.

enumerate_quantifiers_rewriter R

The rewriter.

std::set<state_type> todo

Propositional variable instantiations that need to be handled.

Public member functions

pbesinst_symbolic_algorithm(pbes &p, data::rewriter::strategy rewrite_strategy = data::jitty)
void run()

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