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/modal_formula/normalize.h
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_NORMALIZE_H
13 : #define MCRL2_MODAL_FORMULA_NORMALIZE_H
14 :
15 : #include "mcrl2/modal_formula/negate_variables.h"
16 : #include "mcrl2/modal_formula/traverser.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace state_formulas
22 : {
23 :
24 : /// \cond INTERNAL_DOCS
25 : // \brief Visitor for checking if a state formula is normalized.
26 : struct is_normalized_traverser: public state_formula_traverser<is_normalized_traverser>
27 : {
28 : typedef state_formula_traverser<is_normalized_traverser> super;
29 : using super::enter;
30 : using super::leave;
31 : using super::apply;
32 :
33 : bool result;
34 :
35 198 : is_normalized_traverser()
36 198 : : result(true)
37 198 : {}
38 :
39 : /// \brief Visit not node
40 61 : void enter(const not_& /* x */)
41 : {
42 61 : result = false;
43 61 : }
44 :
45 : /// \brief Visit minus node
46 0 : void enter(const minus& /* x */)
47 : {
48 0 : result = false;
49 0 : }
50 :
51 : /// \brief Visit imp node
52 14 : void enter(const imp& /* x */)
53 : {
54 14 : result = false;
55 14 : }
56 : };
57 : /// \endcond
58 :
59 : /// \cond INTERNAL_DOCS
60 :
61 : // \brief Visitor for normalizing a state formula.
62 : struct normalize_builder: public state_formula_builder<normalize_builder>
63 : {
64 : typedef state_formula_builder<normalize_builder> super;
65 : using super::enter;
66 : using super::leave;
67 : using super::update;
68 : using super::apply;
69 :
70 : bool m_quantitative;
71 : bool m_negated;
72 :
73 : // negated indicates that the formulas is under a negation.
74 : // quantitative indicates that the formula yields a real value,
75 : // in which case forall, exists and not are replaced by supremum, infimum and minus.
76 63 : normalize_builder(bool quantitative, bool negated)
77 63 : : m_quantitative(quantitative),
78 63 : m_negated(negated)
79 63 : {}
80 :
81 : template <class T>
82 14 : void apply(T& result, const data::data_expression& x)
83 : {
84 14 : if (m_quantitative)
85 : {
86 0 : if (m_negated)
87 : {
88 0 : if (x.sort()==data::sort_bool::bool_())
89 : {
90 0 : result = data::sort_bool::not_(x);
91 : }
92 : else
93 : {
94 0 : result = data::sort_real::negate(x);
95 : }
96 : }
97 : else
98 : {
99 0 : result = x;
100 : }
101 : }
102 : else // x is an ordinary modal formula.
103 : {
104 14 : assert(x.sort()==data::sort_bool::bool_());
105 14 : result = m_negated ? data::sort_bool::not_(x) : x;
106 : }
107 14 : }
108 :
109 : template <class T>
110 37 : void apply(T& result, const true_& /*x*/)
111 : {
112 37 : if (m_negated)
113 : {
114 31 : result = false_();
115 : }
116 : else
117 : {
118 6 : result = true_();
119 : }
120 37 : }
121 :
122 : template <class T>
123 19 : void apply(T& result, const false_& /*x*/)
124 : {
125 19 : if (m_negated)
126 : {
127 18 : result = true_();
128 : }
129 : else
130 : {
131 1 : result = false_();
132 : }
133 19 : }
134 :
135 : template <class T>
136 103 : void apply(T& result, const not_& x)
137 : {
138 103 : assert(!m_quantitative);
139 103 : m_negated=!m_negated;
140 103 : apply(result, x.operand());
141 103 : m_negated=!m_negated;
142 103 : }
143 :
144 : template <class T>
145 0 : void apply(T& result, const minus& x)
146 : {
147 0 : assert(m_quantitative);
148 0 : m_negated=!m_negated;
149 0 : apply(result, x.operand());
150 0 : m_negated=!m_negated;
151 0 : }
152 :
153 : template <class T>
154 30 : void apply(T& result, const and_& x)
155 : {
156 30 : state_formula left, right;
157 30 : apply(left, x.left());
158 30 : apply(right, x.right());
159 30 : if (m_negated)
160 : {
161 22 : make_or_(result, left, right);
162 : }
163 : else
164 : {
165 8 : make_and_(result, left, right);
166 : }
167 30 : }
168 :
169 : template <class T>
170 20 : void apply(T& result, const or_& x)
171 : {
172 20 : state_formula left, right;
173 20 : apply(left, x.left());
174 20 : apply(right, x.right());
175 20 : if (m_negated)
176 : {
177 10 : make_and_(result, left, right);
178 : }
179 : else
180 : {
181 10 : make_or_(result, left, right);
182 : }
183 20 : }
184 :
185 : template <class T>
186 0 : void apply(T& result, const plus& x)
187 : {
188 0 : state_formula left, right;
189 0 : apply(left, x.left());
190 0 : apply(right, x.right());
191 0 : if (m_negated)
192 : {
193 : // The plus operator can be inverted if for instance the operator eq_mininf(x) is present, being equal to -infinity
194 : // if x is minus infinity, and being plus infinity otherwise.
195 : // The dual plus then is: e1 dual+ e2 = eq_mininf(e1) && eq_mininf(e2) && (e1+e2).
196 0 : throw mcrl2::runtime_error("Cannot negate the plus operator in quantitative modal formulas: " + pp(x) + ".");
197 : }
198 : else
199 : {
200 0 : make_plus(result, left, right);
201 : }
202 0 : }
203 :
204 : template <class T>
205 15 : void apply(T& result, const imp& x)
206 : {
207 30 : state_formula y = m_quantitative ?
208 0 : or_(minus(x.left()), x.right()) :
209 45 : or_(not_(x.left()), x.right());
210 15 : apply(result, y);
211 15 : }
212 :
213 : template <class T>
214 3 : void apply(T& result, const forall& x)
215 : {
216 3 : state_formula body;
217 3 : apply(body, x.body());
218 3 : if (m_negated)
219 : {
220 1 : make_exists(result, x.variables(), body);
221 : }
222 : else
223 : {
224 2 : make_forall(result, x.variables(), body);
225 : }
226 3 : }
227 :
228 : template <class T>
229 3 : void apply(T& result, const exists& x)
230 : {
231 3 : state_formula body;
232 3 : apply(body, x.body());
233 3 : if (m_negated)
234 : {
235 3 : make_forall(result, x.variables(), body);
236 : }
237 : else
238 : {
239 0 : make_exists(result, x.variables(), body);
240 : }
241 3 : }
242 :
243 : template <class T>
244 0 : void apply(T& result, const supremum& x)
245 : {
246 0 : state_formula body;
247 0 : apply(body, x.body());
248 0 : if (m_negated)
249 : {
250 0 : make_infimum(result, x.variables(), body);
251 : }
252 : else
253 : {
254 0 : make_supremum(result, x.variables(), body);
255 : }
256 0 : }
257 :
258 : template <class T>
259 0 : void apply(T& result, const infimum& x)
260 : {
261 0 : state_formula body;
262 0 : apply(body, x.body());
263 0 : if (m_negated)
264 : {
265 0 : make_supremum(result, x.variables(), body);
266 : }
267 : else
268 : {
269 0 : make_infimum(result, x.variables(), body);
270 : }
271 0 : }
272 :
273 : template <class T>
274 41 : void apply(T& result, const variable& x)
275 : {
276 41 : if (m_negated)
277 : {
278 0 : throw mcrl2::runtime_error(std::string("normalize error: illegal argument ") + pp(x));
279 : }
280 41 : result = x;
281 41 : }
282 :
283 : template <class T>
284 46 : void apply(T& result, const must& x)
285 : {
286 46 : state_formula operand;
287 46 : apply(operand, x.operand());
288 46 : if (m_negated)
289 : {
290 36 : make_may(result, x.formula(), operand);
291 : }
292 : else
293 : {
294 10 : make_must(result, x.formula(), operand);
295 : }
296 46 : }
297 :
298 : template <class T>
299 40 : void apply(T& result, const may& x)
300 : {
301 40 : state_formula operand;
302 40 : apply(operand, x.operand());
303 40 : if (m_negated)
304 : {
305 35 : make_must(result, x.formula(), operand);
306 : }
307 : else
308 : {
309 5 : make_may(result, x.formula(), operand);
310 : }
311 40 : }
312 :
313 : template <class T>
314 20 : void apply(T& result, const mu& x)
315 : {
316 20 : state_formula operand;
317 20 : if (m_negated)
318 : {
319 14 : apply(operand, negate_variables(x.name(), m_quantitative, x.operand()));
320 14 : make_nu(result, x.name(), x.assignments(), operand);
321 : }
322 : else
323 : {
324 6 : apply(operand, x.operand());
325 6 : make_mu(result, x.name(), x.assignments(), operand);
326 : }
327 20 : }
328 :
329 : template <class T>
330 21 : void apply(T& result, const nu& x)
331 : {
332 21 : state_formula operand;
333 21 : if (m_negated)
334 : {
335 13 : apply(operand, negate_variables(x.name(), m_quantitative, x.operand()));
336 13 : make_mu(result, x.name(), x.assignments(), operand);
337 : }
338 : else
339 : {
340 8 : apply(operand, x.operand());
341 8 : make_nu(result, x.name(), x.assignments(), operand);
342 : }
343 21 : }
344 :
345 : template <class T>
346 0 : void apply(T& result, const delay& x)
347 : {
348 0 : if (m_negated)
349 : {
350 0 : result=yaled();
351 : }
352 : else
353 : {
354 0 : result=x;
355 : }
356 0 : }
357 :
358 : template <class T>
359 1 : void apply(T& result, const delay_timed& x)
360 : {
361 1 : if (m_negated)
362 : {
363 1 : make_yaled_timed(result, x.time_stamp());
364 : }
365 : else
366 : {
367 0 : result=x;
368 : }
369 1 : }
370 :
371 : template <class T>
372 0 : void apply(T& result, const yaled& x)
373 : {
374 0 : if (m_negated)
375 : {
376 0 : result=delay();
377 : }
378 : else
379 : {
380 0 : result=x;
381 : }
382 0 : }
383 :
384 : template <class T>
385 1 : void apply(T& result, const yaled_timed& x)
386 : {
387 1 : if (m_negated)
388 : {
389 1 : make_delay_timed(result, x.time_stamp());
390 : }
391 : else
392 : {
393 0 : result=x;
394 : }
395 1 : }
396 : };
397 : /// \endcond
398 :
399 : /// \brief Checks if a state formula is normalized.
400 : /// \param x A PBES expression.
401 : /// \return True if the state formula is normalized.
402 : template <typename T>
403 198 : bool is_normalized(const T& x)
404 : {
405 198 : is_normalized_traverser f;
406 198 : f.apply(x);
407 198 : return f.result;
408 : }
409 :
410 : /// \brief The function normalize brings (embedded) state formulas into positive normal form,
411 : /// i.e. a formula without any occurrences of ! or =>.
412 : /// \param x an object containing state formulas.
413 : /// \param quantitative Indication whether the formula is a quantitative boolean formula.
414 : /// \param negated Indication whether the formula must be interpreted as being negated.
415 : template <typename T>
416 : void normalize(T& x, bool quantitative = false, bool negated = false, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
417 : {
418 : normalize_builder f(quantitative, negated);
419 : f.update(x);
420 : }
421 :
422 : /// \brief The function normalize brings (embedded) state formulas into positive normal form,
423 : /// i.e. a formula without any occurrences of ! or =>.
424 : /// \param x an object containing state formulas
425 : /// \param quantitative Indication whether the formula is a quantitative boolean formula.
426 : /// \param negated Indication whether the formula must be interpreted as being negated.
427 : template <typename T>
428 63 : T normalize(const T& x, bool quantitative = false, bool negated = false, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
429 : {
430 63 : T result;
431 63 : normalize_builder f(quantitative, negated);
432 63 : f.apply(result, x);
433 126 : return result;
434 0 : }
435 :
436 : } // namespace state_formulas
437 :
438 : } // namespace mcrl2
439 :
440 : #endif // MCRL2_MODAL_FORMULA_NORMALIZE_H
|