12#ifndef MCRL2_PBES_PBESINST_STRUCTURE_GRAPH_H
13#define MCRL2_PBES_PBESINST_STRUCTURE_GRAPH_H
24namespace pbes_system {
53 auto vertex_psi_i =
SG1(psi_i);
61 auto vertex_psi_i =
SG1(psi_i);
86 auto vertex_psi_i =
SG1(psi_i);
94 auto vertex_psi_i =
SG1(psi_i);
103 if (equation_count > 0 && equation_count % 1000 == 0)
105 std::ostringstream out;
106 out <<
"Generated " << equation_count <<
" BES equations (" << std::fixed << std::setprecision(2) <<
parameterized boolean equation system
A PBES instantiation algorithm that uses a lazy strategy.
virtual void run()
Runs the algorithm. The result is obtained by calling the function get_result.
Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the str...
detail::structure_graph_builder m_graph_builder
void run() override
Runs the algorithm. The result is obtained by calling the function get_result.
structure_graph::index_type SG1(const pbes_expression &psi)
void on_report_equation(const std::size_t, const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) override
Reports BES equations that are produced by the algorithm. This function is called for every BES equat...
std::string status_message(std::size_t equation_count) override
void SG0(const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k)
pbesinst_structure_graph_algorithm(const pbessolve_options &options, const pbes &p, structure_graph &G)
\brief A propositional variable instantiation
const data::data_expression & undefined_data_expression()
Returns a data expression that corresponds to 'undefined'.
std::set< pbes_expression > split_and(const pbes_expression &expr, bool split_data_expressions=false)
Splits a conjunction into a sequence of operands Given a pbes expression of the form p1 && p2 && ....
bool is_or(const atermpp::aterm &x)
bool is_false(const pbes_expression &t)
Test for the value false.
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
std::set< pbes_expression > split_or(const pbes_expression &expr, bool split_data_expressions=false)
Splits a disjunction into a sequence of operands Given a pbes expression of the form p1 || p2 || ....
bool is_true(const pbes_expression &t)
Test for the value true.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.
add your file description here.
index_type insert_variable(const pbes_expression &x, const pbes_expression &psi, std::size_t k)
void insert_edge(index_type ui, index_type vi)
void set_initial_state(const propositional_variable_instantiation &x)
pbes_expression m_initial_state
index_type insert_vertex(const pbes_expression &x)
std::size_t extent() const
add your file description here.