mCRL2
Loading...
Searching...
No Matches
pbesinst_structure_graph.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_PBES_PBESINST_STRUCTURE_GRAPH_H
13#define MCRL2_PBES_PBESINST_STRUCTURE_GRAPH_H
14
15#include <iomanip>
16
18#include "mcrl2/pbes/join.h"
21
22namespace mcrl2 {
23
24namespace pbes_system {
25
29{
30 protected:
32
33 void SG0(const propositional_variable_instantiation& X, const pbes_expression& psi, std::size_t k)
34 {
35 auto vertex_phi = m_graph_builder.insert_variable(X, psi, k);
36 if (is_true(psi))
37 {
38 // skip
39 }
40 else if (is_false(psi))
41 {
42 // skip
43 }
45 {
46 auto vertex_psi = m_graph_builder.insert_variable(psi);
47 m_graph_builder.insert_edge(vertex_phi, vertex_psi);
48 }
49 else if (is_and(psi))
50 {
51 for (const pbes_expression& psi_i: split_and(psi))
52 {
53 auto vertex_psi_i = SG1(psi_i);
54 m_graph_builder.insert_edge(vertex_phi, vertex_psi_i);
55 }
56 }
57 else if (is_or(psi))
58 {
59 for (const pbes_expression& psi_i: split_or(psi))
60 {
61 auto vertex_psi_i = SG1(psi_i);
62 m_graph_builder.insert_edge(vertex_phi, vertex_psi_i);
63 }
64 }
65 }
66
68 {
69 auto vertex_psi = m_graph_builder.insert_vertex(psi);
70 if (is_true(psi))
71 {
72 // skip
73 }
74 else if (is_false(psi))
75 {
76 // skip
77 }
79 {
80 // skip
81 }
82 else if (is_and(psi))
83 {
84 for (const pbes_expression& psi_i: split_and(psi))
85 {
86 auto vertex_psi_i = SG1(psi_i);
87 m_graph_builder.insert_edge(vertex_psi, vertex_psi_i);
88 }
89 }
90 else if (is_or(psi))
91 {
92 for (const pbes_expression& psi_i: split_or(psi))
93 {
94 auto vertex_psi_i = SG1(psi_i);
95 m_graph_builder.insert_edge(vertex_psi, vertex_psi_i);
96 }
97 }
98 return vertex_psi;
99 }
100
101 std::string status_message(std::size_t equation_count) override
102 {
103 if (equation_count > 0 && equation_count % 1000 == 0)
104 {
105 std::ostringstream out;
106 out << "Generated " << equation_count << " BES equations (" << std::fixed << std::setprecision(2) <<
107 ((100.0 * equation_count) / m_graph_builder.extent()) << "% explored)" << std::endl;
108 return out.str();
109 }
110 return "";
111 }
112
113 public:
115 const pbessolve_options& options,
116 const pbes& p,
118 )
119 : pbesinst_lazy_algorithm(options, p),
121 {}
122
123 void on_report_equation(const std::size_t /* thread_index */,
125 const pbes_expression& psi,
126 std::size_t k
127 ) override
128 {
129 // the body of this if statement will only be executed for the first equation
131 {
133 }
134 SG0(X, psi, k);
135 }
136
137 void run() override
138 {
141 }
142};
143
144} // namespace pbes_system
145
146} // namespace mcrl2
147
148#endif // MCRL2_PBES_PBESINST_STRUCTURE_GRAPH_H
parameterized boolean equation system
Definition pbes.h:58
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...
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'.
Definition undefined.h:58
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 && ....
Definition join.h:76
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 || ....
Definition join.h:50
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...
Definition indexed_set.h:72
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 set_initial_state(const propositional_variable_instantiation &x)
add your file description here.