Line data Source code
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 : //
9 : /// \file mcrl2/lps/print.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_LPS_PRINT_H
13 : #define MCRL2_LPS_PRINT_H
14 :
15 : #include "mcrl2/data/parse.h"
16 : #include "mcrl2/lps/traverser.h"
17 : #include "mcrl2/process/print.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace lps
23 : {
24 :
25 : namespace detail
26 : {
27 :
28 : template <typename Derived>
29 : struct printer: public lps::add_traverser_sort_expressions<process::detail::printer, Derived>
30 : {
31 : typedef lps::add_traverser_sort_expressions<process::detail::printer, Derived> super;
32 :
33 : using super::enter;
34 : using super::leave;
35 : using super::apply;
36 : using super::derived;
37 : using super::print_action_declarations;
38 : using super::print_assignments;
39 : using super::print_condition;
40 : using super::print_expression;
41 : using super::print_list;
42 : using super::print_variables;
43 :
44 : bool m_print_summand_numbers;
45 :
46 1401 : printer()
47 1401 : : m_print_summand_numbers(false)
48 1401 : {}
49 :
50 0 : bool& print_summand_numbers()
51 : {
52 0 : return m_print_summand_numbers;
53 : }
54 :
55 : template <typename Container>
56 0 : void print_numbered_list(const Container& container,
57 : const std::string& separator = ", ",
58 : const std::string& number_separator = "",
59 : std::size_t index = 0,
60 : bool print_start_separator = false,
61 : bool print_empty_container = false
62 : )
63 : {
64 0 : if (container.empty() && !print_empty_container)
65 : {
66 0 : return;
67 : }
68 0 : for (auto i = container.begin(); i != container.end(); ++i)
69 : {
70 0 : derived().print("\n");
71 0 : derived().print(number_separator);
72 0 : derived().print("%");
73 0 : derived().print(utilities::number2string(index++));
74 :
75 0 : derived().print("\n");
76 0 : if (i == container.begin() && !print_start_separator)
77 : {
78 0 : derived().print(number_separator);
79 : }
80 : else
81 : {
82 0 : derived().print(separator);
83 : }
84 0 : derived().apply(*i);
85 : }
86 : }
87 :
88 23 : void apply(const lps::deadlock& x)
89 : {
90 23 : derived().enter(x);
91 23 : derived().print("delta");
92 23 : if (x.has_time())
93 : {
94 1 : derived().print(" @ ");
95 1 : print_expression(x.time(), precedence(x.time()) < core::detail::max_precedence);
96 : }
97 23 : derived().leave(x);
98 23 : }
99 :
100 1247 : void apply(const lps::multi_action& x)
101 : {
102 1247 : derived().enter(x);
103 1247 : if (x.actions().empty())
104 : {
105 129 : derived().print("tau");
106 : }
107 : else
108 : {
109 1118 : print_list(x.actions(), "", "", "|");
110 : }
111 1247 : if (x.has_time())
112 : {
113 8 : derived().print(" @ ");
114 8 : print_expression(x.time(), precedence(x.time()) < core::detail::max_precedence);
115 : }
116 1247 : derived().leave(x);
117 1247 : }
118 :
119 19 : void apply(const lps::deadlock_summand& x)
120 : {
121 19 : derived().enter(x);
122 19 : print_variables(x.summation_variables(), true, true, false, "sum ", ".\n ", ",");
123 19 : print_condition(x.condition(), " ->\n ");
124 19 : derived().apply(x.deadlock());
125 19 : derived().leave(x);
126 19 : }
127 :
128 9 : void apply(const lps::stochastic_distribution& x)
129 : {
130 9 : derived().enter(x);
131 9 : if (x.variables().empty()) // do not print the empty distribution
132 : {
133 1 : return;
134 : }
135 8 : derived().print("dist ");
136 8 : print_variables(x.variables(), true, true, false, "", "");
137 8 : derived().print("[");
138 8 : derived().apply(x.distribution());
139 8 : derived().print("]");
140 8 : derived().leave(x);
141 : }
142 :
143 80 : void print_distribution(const lps::action_summand&)
144 80 : { }
145 :
146 7 : void print_distribution(const lps::stochastic_action_summand& x)
147 : {
148 7 : if (x.distribution().is_defined())
149 : {
150 4 : derived().apply(x.distribution());
151 4 : derived().print(" .\n ");
152 : }
153 7 : }
154 :
155 : template <typename ActionSummand>
156 87 : void print_action_summand(const ActionSummand& x)
157 : {
158 87 : derived().enter(x);
159 87 : print_variables(x.summation_variables(), true, true, false, "sum ", ".\n ", ",");
160 87 : print_condition(x.condition(), " ->\n ");
161 87 : derived().apply(x.multi_action());
162 87 : derived().print(" .\n ");
163 87 : print_distribution(x);
164 87 : derived().print("P(");
165 87 : print_assignments(x.assignments(), true, "", "", ", ");
166 87 : derived().print(")");
167 87 : derived().leave(x);
168 87 : }
169 :
170 80 : void apply(const lps::action_summand& x)
171 : {
172 80 : print_action_summand(x);
173 80 : }
174 :
175 7 : void apply(const lps::stochastic_action_summand& x)
176 : {
177 7 : print_action_summand(x);
178 7 : }
179 :
180 34 : void apply(const lps::process_initializer& x)
181 : {
182 34 : derived().enter(x);
183 34 : derived().print("init P");
184 34 : print_variables(x.expressions(), false);
185 34 : derived().print(";");
186 34 : derived().leave(x);
187 34 : }
188 :
189 6 : void apply(const lps::stochastic_process_initializer& x)
190 : {
191 6 : derived().enter(x);
192 6 : derived().print("init ");
193 6 : if (x.distribution().is_defined())
194 : {
195 4 : derived().apply(x.distribution());
196 4 : derived().print(" . ");
197 : }
198 6 : derived().print("P");
199 6 : print_variables(x.expressions(), false);
200 6 : derived().print(";");
201 6 : derived().leave(x);
202 6 : }
203 :
204 : // this overload is enabled for linear_process and stochastic_linear_process
205 : template <typename LinearProcess>
206 44 : void print_linear_process(const LinearProcess& x)
207 : {
208 44 : derived().enter(x);
209 44 : derived().print("proc P");
210 44 : print_variables(x.process_parameters(), true, true, false, "(", ")", ", ");
211 :
212 44 : if (m_print_summand_numbers)
213 : {
214 0 : derived().print(" =");
215 :
216 0 : std::string separator = " + ";
217 0 : std::string number_separator = " ";
218 :
219 : // print action summands
220 0 : print_numbered_list(x.action_summands(), separator, number_separator, 1, false);
221 :
222 : // print deadlock summands
223 0 : print_numbered_list(x.deadlock_summands(), separator, number_separator, x.action_summands().size() + 1, true);
224 :
225 : // print delta if there are no summands
226 0 : if (x.action_summands().empty() && (x.deadlock_summands().empty()))
227 : {
228 0 : deadlock_summand_vector v;
229 0 : v.push_back(deadlock_summand(data::variable_list(), data::sort_bool::true_(), lps::deadlock(data::parse_data_expression("0"))));
230 0 : print_numbered_list(v, separator, number_separator, 1, true);
231 0 : }
232 0 : }
233 : else
234 : {
235 44 : derived().print(" =\n ");
236 :
237 : // print action summands
238 44 : std::string opener = "";
239 44 : std::string closer = "";
240 44 : std::string separator = "\n + ";
241 44 : print_list(x.action_summands(), opener, closer, separator);
242 :
243 : // print deadlock summands
244 44 : if (!x.action_summands().empty())
245 : {
246 43 : opener = separator;
247 : }
248 44 : print_list(x.deadlock_summands(), opener, closer, separator);
249 :
250 : // print delta if there are no summands
251 44 : if (x.action_summands().empty() && (x.deadlock_summands().empty()))
252 : {
253 1 : deadlock_summand_vector v;
254 1 : v.push_back(deadlock_summand(data::variable_list(), data::sort_bool::true_(), lps::deadlock(data::parse_data_expression("0"))));
255 1 : print_list(v, opener, closer, separator);
256 1 : }
257 44 : }
258 :
259 44 : derived().print(";\n");
260 44 : derived().leave(x);
261 44 : }
262 :
263 38 : void apply(const linear_process& x)
264 : {
265 38 : print_linear_process(x);
266 38 : }
267 :
268 6 : void apply(const stochastic_linear_process& x)
269 : {
270 6 : print_linear_process(x);
271 6 : }
272 :
273 : template <typename Specification>
274 40 : void print_specification(const Specification& x)
275 : {
276 40 : derived().enter(x);
277 40 : derived().apply(x.data());
278 40 : print_action_declarations(x.action_labels(), "act ",";\n\n", ";\n ");
279 40 : print_variables(x.global_variables(), true, true, true, "glob ", ";\n\n", ";\n ");
280 40 : derived().apply(x.process());
281 40 : derived().print("\n");
282 40 : derived().apply(x.initial_process());
283 40 : derived().print("\n");
284 40 : derived().leave(x);
285 40 : }
286 :
287 34 : void apply(const specification& x)
288 : {
289 34 : print_specification(x);
290 34 : }
291 :
292 6 : void apply(const stochastic_specification& x)
293 : {
294 6 : print_specification(x);
295 6 : }
296 :
297 : /* void apply(const lps::state &x)
298 : {
299 : derived().enter(x);
300 : derived().print("state(");
301 : bool first = true;
302 : for (lps::state::const_iterator i = x.begin(); i != x.end(); i++)
303 : {
304 : if (!first)
305 : {
306 : derived().print(", ");
307 : }
308 : first = false;
309 : print_expression(*i);
310 : }
311 : derived().print(")");
312 : derived().leave(x);
313 : } */
314 : };
315 :
316 : } // namespace detail
317 :
318 : /// \brief Prints the object x to a stream.
319 : struct stream_printer
320 : {
321 : template <typename T>
322 1253 : void operator()(const T& x, std::ostream& out)
323 : {
324 1253 : core::detail::apply_printer<lps::detail::printer> printer(out);
325 1253 : printer.apply(x);
326 1253 : }
327 : };
328 :
329 : /// \brief Returns a string representation of the object x.
330 : template <typename T>
331 1253 : std::string pp(const T& x)
332 : {
333 1253 : std::ostringstream out;
334 1253 : stream_printer()(x, out);
335 2506 : return out.str();
336 1253 : }
337 :
338 : } // namespace lps
339 :
340 : } // namespace mcrl2
341 :
342 : #endif // MCRL2_LPS_PRINT_H
|
