12#ifndef MCRL2_PBES_PBESINST_STRUCTURE_GRAPH2_H
13#define MCRL2_PBES_PBESINST_STRUCTURE_GRAPH2_H
26namespace pbes_system {
76 std::array<vertex_set, 2>
S;
77 std::array<strategy_vector, 2>
tau;
78 std::array<detail::computation_guard, 2>
S_guard;
123 std::array<vertex_set, 2>&
S;
135 stack.push_back(elem);
140 auto result =
stack.back();
183 else if (
S[0].contains(u))
187 else if (
S[1].contains(u))
202 auto& f1_prime = elem1.
f;
203 auto& g0_1 = elem1.
g0;
204 auto& g1_1 = elem1.
g1;
206 auto& f2_prime = elem2.
f;
207 auto& g0_2 = elem2.
g0;
208 auto& g1_2 = elem2.
g1;
214 f1_prime =
and_(f1_prime, f2_prime);
215 g0_1 =
and_(g0_1, g0_2);
234 if (
less(f1_prime, f2_prime))
252 f1_prime =
and_(f1_prime, f2_prime);
263 auto& f1_prime = elem1.
f;
264 auto& g0_1 = elem1.
g0;
265 auto& g1_1 = elem1.
g1;
267 auto& f2_prime = elem2.
f;
268 auto& g0_2 = elem2.
g0;
269 auto& g1_2 = elem2.
g1;
275 f1_prime =
or_(f1_prime, f2_prime);
277 g1_1 =
or_(g1_1, g1_2);
295 if (
less(f1_prime, f2_prime))
313 f1_prime =
or_(f1_prime, f2_prime);
360 return S[0].contains(u) ||
S[1].contains(u);
399 std::size_t regeneration_period
415 while (!todo1.empty())
428 new_todo.
insert(atermpp::down_cast<propositional_variable_instantiation>(u_.formula()));
432 if (!
S[0].contains(u) && !
S[1].contains(u))
439 if (contains(done1, Y))
455 if (contains(new_todo, X))
462 if (contains(new_todo, X))
479 mCRL2log(
log::debug) <<
"Error: no strategy has been set for disjunctive node " << u <<
" in S0." << std::endl;
491 mCRL2log(
log::debug) <<
"Error: no strategy has been set for conjunctive node " << u <<
" in S1." << std::endl;
522 auto rplus_result =
Rplus(result);
523 b[thread_index] = rplus_result.b;
526 result = rplus_result.g0;
531 result = rplus_result.g1;
534 result = rplus_result.f;
622 mCRL2log(
log::verbose) <<
"found solution for" << std::setw(12) <<
S[0].size() +
S[1].size() <<
" BES equations" << std::endl;
649 for (std::size_t v = 0; v < n; v++)
A deque class in which aterms can be stored.
void push_back(const T &value)
Base class that should not be used.
A set that assigns each element an unique index, and protects its internal terms en masse.
std::pair< size_type, bool > insert(const Key &key, std::size_t thread_index=0)
A vector class in which aterms can be stored.
\brief The and operator for pbes expressions
computation_guard(std::size_t initial_count=64)
bool operator()(std::size_t count)
std::size_t regeneration_period
bool operator()(std::size_t period)
\brief The existential quantification operator for pbes expressions
\brief The universal quantification operator for pbes expressions
\brief The implication operator for pbes expressions
\brief The or operator for pbes expressions
parameterized boolean equation system
const pbessolve_options & m_options
Algorithm options.
virtual void rewrite_psi(const std::size_t, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)
pbesinst_lazy_todo todo
The propositional variable instantiations that need to be handled.
propositional_variable_instantiation init
The initial value (after rewriting).
std::size_t m_iteration_count
const fixpoint_symbol & symbol(std::size_t i) const
atermpp::indexed_set< propositional_variable_instantiation, true > discovered
The propositional variable instantiations that have been discovered (not necessarily handled).
const atermpp::deque< propositional_variable_instantiation > & elements() const
void set_todo(atermpp::deque< propositional_variable_instantiation > &new_todo)
const std::unordered_set< propositional_variable_instantiation > & irrelevant_elements() const
Adds an optimization to pbesinst_structure_graph.
void on_discovered_elements(const std::set< propositional_variable_instantiation > &elements) override
This function is called when new elements are added to discovered.
detail::computation_guard fatal_attractors_guard
void rewrite_psi(const std::size_t thread_index, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) override
Rplus_traverser::stack_element Rplus(const pbes_expression &x)
bool todo_has_only_undefined_nodes() const
pbesinst_structure_graph_algorithm2(const pbessolve_options &options, const pbes &p, structure_graph &G)
void prune_todo_list(const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t regeneration_period)
detail::computation_guard find_loops_guard
std::array< strategy_vector, 2 > tau
atermpp::vector< pbes_expression > b
std::array< vertex_set, 2 > S
detail::periodic_guard reset_guard
bool strategies_are_set_in_solved_nodes() const
pbes_expression expr(const T &x) const
pbesinst_structure_graph_algorithm super
bool solution_found(const propositional_variable_instantiation &init) const override
void on_report_equation(const std::size_t thread_index, 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...
void on_end_while_loop() override
This function is called right after the while loop is finished.
std::array< detail::computation_guard, 2 > S_guard
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 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...
\brief A propositional variable instantiation
const std::vector< index_type > & successors(index_type u) const
decoration_type decoration(index_type u) const
Standard exception class for reporting runtime errors.
Implements a simple stopwatch that starts on construction.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
std::stack< std::reference_wrapper< detail::_aterm > > term_mark_stack
const data::data_expression & undefined_data_expression()
Returns a data expression that corresponds to 'undefined'.
void fatal_attractors_original(const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
void partial_solve(structure_graph &G, const pbesinst_lazy_todo &todo, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count, const detail::structure_graph_builder &graph_builder)
void find_loops2(const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
void find_loops(const simple_structure_graph &G, const Container &discovered, const pbesinst_lazy_todo &todo, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t iteration_count, const detail::structure_graph_builder &graph_builder)
void fatal_attractors(const simple_structure_graph &G, std::array< vertex_set, 2 > &S, std::array< strategy_vector, 2 > &tau, std::size_t equation_count)
constexpr unsigned int undefined_vertex()
const pbes_expression & true_()
bool is_false(const pbes_expression &t)
Test for the value false.
std::set< structure_graph::index_type > extract_minimal_structure_graph(StructureGraph &G, typename StructureGraph::index_type init, const vertex_set &S0, const vertex_set &S1)
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
std::string pp(const fixpoint_symbol &x)
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
vertex_set attr_default_with_tau(const StructureGraph &G, vertex_set A, std::size_t alpha, std::array< strategy_vector, 2 > &tau)
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
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.
add your file description here.
A variant of the lazy algorithm for instantiating a PBES, that produces a structure_graph.
void apply(const pbes_system::pbes_equation &x)
void erase_vertices(const vertex_set &U)
structure_graph::vertex & vertex(index_type u)
structure_graph & m_graph
index_type find_vertex(const pbes_expression &x) const
std::size_t extent() const
structure_graph::vertex_vector & vertices()
atermpp::detail::reference_aterm< pbes_expression > f
stack_element(pbes_expression b_, pbes_expression f_, pbes_expression g0_, pbes_expression g1_)
atermpp::detail::reference_aterm< pbes_expression > g1
void mark(atermpp::term_mark_stack &todo) const
atermpp::detail::reference_aterm< pbes_expression > g0
atermpp::detail::reference_aterm< pbes_expression > b
void enter(const forall &x)
atermpp::vector< stack_element > stack
void leave(const exists &x)
detail::structure_graph_builder & graph_builder
const stack_element & top() const
void push(const stack_element &elem)
void leave(const data::data_expression &x)
pbes_expression_traverser< Rplus_traverser > super
std::array< vertex_set, 2 > & S
void enter(const exists &x)
static bool less(const pbes_expression &, const pbes_expression &)
Rplus_traverser(std::array< vertex_set, 2 > &S_, detail::structure_graph_builder &graph_builder_)
void leave(const forall &x)
void leave(const propositional_variable_instantiation &x)
const pbes_expression & formula() const
void insert(structure_graph::index_type u)