mcrl2::pbes_system::pbesinst_symbolic_algorithm¶
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
mcrl2::pbes_system::pbesinst_symbolic_algorithm::state_type¶ typedef for
propositional_variable_instantiation
Protected attributes¶
-
data::rewriter
mcrl2::pbes_system::pbesinst_symbolic_algorithm::datar¶ Data rewriter.
-
std::set<state_type>
mcrl2::pbes_system::pbesinst_symbolic_algorithm::done¶ Propositional variable instantiations that have been handled.
-
std::multimap<state_type, state_type>
mcrl2::pbes_system::pbesinst_symbolic_algorithm::edges¶ Data structure for storing the result. E[i] corresponds to the equations generated from the i-th PBES equation.
-
state_type
mcrl2::pbes_system::pbesinst_symbolic_algorithm::init¶ The initial value.
-
std::map<core::identifier_string, std::size_t>
mcrl2::pbes_system::pbesinst_symbolic_algorithm::m_equation_index¶ A lookup map for PBES equations.
-
pbes &
mcrl2::pbes_system::pbesinst_symbolic_algorithm::m_pbes¶ The PBES that is being instantiated.
-
enumerate_quantifiers_rewriter
mcrl2::pbes_system::pbesinst_symbolic_algorithm::R¶ The rewriter.
-
std::set<state_type>
mcrl2::pbes_system::pbesinst_symbolic_algorithm::todo¶ Propositional variable instantiations that need to be handled.
