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< data::data_expression >

Protected attributes

std::vector<summand_set> mcrl2::pbes_system::partial_order_reduction_algorithm::m_dependency_nes

data::enumerator_algorithm 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

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) const

bool depends(std::size_t i, std::size_t k, std::size_t j) 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

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

summand_set &NES(std::size_t k)

const summand_set &NES(std::size_t k) const

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()