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/pbes/normalize.h
10 : /// \brief Normalization of pbes expressions.
11 :
12 : #ifndef MCRL2_PBES_NORMALIZE_H
13 : #define MCRL2_PBES_NORMALIZE_H
14 :
15 : #include "mcrl2/data/consistency.h"
16 : #include "mcrl2/pbes/builder.h"
17 : #include "mcrl2/pbes/traverser.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace pbes_system
23 : {
24 :
25 : /// \cond INTERNAL_DOCS
26 : // \brief Visitor for checking if a pbes expression is normalized.
27 : struct is_normalized_traverser: public pbes_expression_traverser<is_normalized_traverser>
28 : {
29 : typedef pbes_expression_traverser<is_normalized_traverser> super;
30 : using super::enter;
31 : using super::leave;
32 : using super::apply;
33 :
34 : bool result;
35 :
36 137 : is_normalized_traverser()
37 137 : : result(true)
38 137 : {}
39 :
40 : /// \brief Visit not node
41 0 : void enter(const not_& /* x */)
42 : {
43 0 : result = false;
44 0 : }
45 :
46 : /// \brief Visit imp node
47 0 : void enter(const imp& /* x */)
48 : {
49 0 : result = false;
50 0 : }
51 : };
52 : /// \endcond
53 :
54 : /// \cond INTERNAL_DOCS
55 : // \brief Visitor for checking if a pbes expression is normalized.
56 : struct normalize_builder: public pbes_expression_builder<normalize_builder>
57 : {
58 : typedef pbes_expression_builder<normalize_builder> super;
59 : using super::apply;
60 :
61 : bool negated;
62 :
63 436 : normalize_builder()
64 436 : : negated(false)
65 436 : {}
66 :
67 : template <class T>
68 2532 : void apply(T& result, const data::data_expression& x)
69 : {
70 2532 : result = negated ? data::not_(x) : x;
71 2532 : }
72 :
73 : template <class T>
74 139 : void apply(T& result, const not_& x)
75 : {
76 139 : negated = !negated;
77 139 : super::apply(result, x.operand());
78 139 : negated = !negated;
79 139 : }
80 :
81 : template <class T>
82 1850 : void apply(T& result, const and_& x)
83 : {
84 1850 : pbes_expression left;
85 1850 : super::apply(left, x.left());
86 1850 : pbes_expression right;
87 1850 : super::apply(right, x.right());
88 1850 : if (negated)
89 : {
90 46 : make_or_(result, left, right);
91 : }
92 : else
93 : {
94 1804 : make_and_(result, left, right);
95 : }
96 1850 : }
97 :
98 : template <class T>
99 1067 : void apply(T& result, const or_& x)
100 : {
101 1067 : pbes_expression left;
102 1067 : super::apply(left, x.left());
103 1067 : pbes_expression right;
104 1067 : super::apply(right, x.right());
105 1067 : if (negated)
106 : {
107 36 : make_and_(result, left, right);
108 : }
109 : else
110 : {
111 1031 : make_or_(result, left, right);
112 : }
113 1067 : }
114 :
115 : template <class T>
116 586 : void apply(T& result, const imp& x)
117 : {
118 586 : negated = !negated;
119 586 : pbes_expression left;
120 586 : super::apply(left, x.left());
121 586 : negated = !negated;
122 586 : pbes_expression right;
123 586 : super::apply(right, x.right());
124 586 : if (negated)
125 : {
126 8 : make_and_(result, left, right);
127 : }
128 : else
129 : {
130 578 : make_or_(result, left, right);
131 : }
132 586 : }
133 :
134 : template <class T>
135 390 : void apply(T& result, const forall& x)
136 : {
137 390 : pbes_expression body;
138 390 : super::apply(body, x.body());
139 390 : result = negated ? make_exists_(x.variables(), body) : make_forall_(x.variables(), body);
140 390 : }
141 :
142 : template <class T>
143 438 : void apply(T& result, const exists& x)
144 : {
145 438 : pbes_expression body;
146 438 : super::apply(body, x.body());
147 438 : result = negated ? make_forall_(x.variables(), body) : make_exists_(x.variables(), body);
148 438 : }
149 :
150 : template <class T>
151 1948 : void apply(T& result, const propositional_variable_instantiation& x)
152 : {
153 1948 : if (negated)
154 : {
155 0 : throw mcrl2::runtime_error(std::string("normalize error: illegal argument ") + pp(x));
156 : }
157 1948 : result = x;
158 1948 : }
159 : };
160 : /// \endcond
161 :
162 : /// \brief Checks if a pbes expression is normalized
163 : /// \param x A PBES expression
164 : /// \return True if the pbes expression is normalized
165 : template <typename T>
166 137 : bool is_normalized(const T& x)
167 : {
168 137 : is_normalized_traverser f;
169 137 : f.apply(x);
170 137 : return f.result;
171 : }
172 :
173 : /// \brief The function normalize brings (embedded) pbes expressions into positive normal form,
174 : /// i.e. a formula without any occurrences of ! or =>.
175 : /// \param x an object containing pbes expressions
176 : template <typename T>
177 428 : void normalize(T& x,
178 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
179 : )
180 : {
181 428 : normalize_builder f;
182 428 : f.update(x);
183 428 : }
184 :
185 : /// \brief The function normalize brings (embedded) pbes expressions into positive normal form,
186 : /// i.e. a formula without any occurrences of ! or =>.
187 : /// \param x an object containing pbes expressions
188 : template <typename T>
189 8 : T normalize(const T& x,
190 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
191 : )
192 : {
193 8 : T result;
194 8 : normalize_builder f;
195 8 : f.apply(result, x);
196 16 : return result;
197 0 : }
198 :
199 : } // namespace pbes_system
200 :
201 : } // namespace mcrl2
202 :
203 : #endif // MCRL2_PBES_NORMALIZE_H
|
