mcrl2::pbes_system::partial_order_reduction_algorithm

Include file:

#include "mcrl2/pbes/partial_order_reduction.h
class mcrl2::pbes_system::partial_order_reduction_algorithm

Protected types

type mcrl2::pbes_system::partial_order_reduction_algorithm::enumerator_element

typedef for data::enumerator_list_element_with_substitution< pbes_expression >

Protected attributes

std::vector<summand_set> mcrl2::pbes_system::partial_order_reduction_algorithm::m_dependency_nes
data::enumerator_algorithm<enumerate_quantifiers_rewriter, data::rewriter> mcrl2::pbes_system::partial_order_reduction_algorithm::m_enumerator
pbes_equation_index mcrl2::pbes_system::partial_order_reduction_algorithm::m_equation_index
std::chrono::high_resolution_clock::duration mcrl2::pbes_system::partial_order_reduction_algorithm::m_exploration_duration
data::enumerator_identifier_generator mcrl2::pbes_system::partial_order_reduction_algorithm::m_id_generator
summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::m_invis
std::size_t mcrl2::pbes_system::partial_order_reduction_algorithm::m_largest_equation_size
pbespor_options mcrl2::pbes_system::partial_order_reduction_algorithm::m_options
std::map<data::variable, std::size_t> mcrl2::pbes_system::partial_order_reduction_algorithm::m_parameter_positions
std::vector<data::variable> mcrl2::pbes_system::partial_order_reduction_algorithm::m_parameters
srf_pbes mcrl2::pbes_system::partial_order_reduction_algorithm::m_pbes
enumerate_quantifiers_rewriter mcrl2::pbes_system::partial_order_reduction_algorithm::m_pbes_rewr
data::rewriter mcrl2::pbes_system::partial_order_reduction_algorithm::m_rewr
data::mutable_indexed_substitution mcrl2::pbes_system::partial_order_reduction_algorithm::m_sigma
smt::smt_solver *mcrl2::pbes_system::partial_order_reduction_algorithm::m_solver
std::chrono::high_resolution_clock::duration mcrl2::pbes_system::partial_order_reduction_algorithm::m_static_analysis_duration
std::vector<summand_class> mcrl2::pbes_system::partial_order_reduction_algorithm::m_summand_classes
std::unordered_map<summand_equivalence_key, std::size_t> mcrl2::pbes_system::partial_order_reduction_algorithm::m_summand_index
summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::m_vis

Protected member functions

const summand_set &choose_minimal_NES(std::size_t k, const propositional_variable_instantiation &X_e) const
void compute_dependency_NES()
void compute_deterministic()
bool compute_deterministic_data(std::size_t k)
bool compute_deterministic_equations(std::size_t k)
void compute_DNA_DNL_NES(const std::vector<parameter_info> &info)
void compute_NES_DNA_DNL()
void compute_nxt()
void compute_summand_classes()
void compute_vis_invis()
bool dependency_permanently_disables(const std::size_t k, const std::size_t k1) const

Return true iff k1 can never happen after k happens, as deduced from predicate dependencies.

bool depends(std::size_t i, std::size_t k, std::size_t j) const
bool depends(std::size_t i, std::size_t k) const
const summand_set &DNA(std::size_t k) const
summand_set &DNA(std::size_t k)
const summand_set &DNL(std::size_t k) const
summand_set &DNL(std::size_t k)
const summand_set &DNS(std::size_t k) const
summand_set &DNS(std::size_t k)
const summand_set &DNX(std::size_t k, const summand_set &Twork, const summand_set &Ts, const summand_set &en_X_e) const
summand_set en(const propositional_variable_instantiation &X_e)
std::set<std::size_t> FV(const pbes_expression &x) const
summand_set invis(const summand_set &K)
bool is_true(data::data_expression expr)
tribool left_accords_equations(std::size_t k, std::size_t k1) const
const summand_set &NES(std::size_t k) const
summand_set &NES(std::size_t k)
std::size_t parameter_position(const data::variable &v) const
void print_pbes() const
void print_summand(const srf_summand &summand, bool is_conjunctive) const
void print_summand_classes() const
std::string print_variables(const data::variable_list &v) const
tribool square_accords_equations(std::size_t k, std::size_t k1) const
summand_set stubborn_set(const propositional_variable_instantiation &X_e, const summand_set &en_X_e)
std::set<propositional_variable_instantiation> succ(const propositional_variable_instantiation &X_e, const summand_set &K)
std::size_t summand_index(const srf_summand &summand) const
tribool triangle_accords_equations(std::size_t k, std::size_t k1) const

Protected static member functions

static summand_equivalence_key rename_duplicate_variables(data::set_identifier_generator &id_gen, const summand_equivalence_key &summ)

Public member functions

void explore(const propositional_variable_instantiation &X_init, EmitNode emit_node = EmitNode(), EmitEdge emit_edge = EmitEdge())
void explore_full(const propositional_variable_instantiation &X_init, EmitNode emit_node = EmitNode(), EmitEdge emit_edge = EmitEdge())
const propositional_variable_instantiation &initial_state() const
const std::vector<data::variable> &parameters() const
partial_order_reduction_algorithm(const pbes &p, pbespor_options options)
void print() const
const fixpoint_symbol &symbol(const core::identifier_string &X) const
~partial_order_reduction_algorithm()