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/normal_forms.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_NORMAL_FORMS_H
13 : #define MCRL2_PBES_NORMAL_FORMS_H
14 :
15 : #include "mcrl2/pbes/traverser.h"
16 :
17 : namespace mcrl2
18 : {
19 :
20 : namespace pbes_system
21 : {
22 :
23 : namespace detail
24 : {
25 :
26 : enum standard_form_type
27 : {
28 : standard_form_both,
29 : standard_form_and,
30 : standard_form_or
31 : };
32 :
33 : typedef std::pair<pbes_expression, standard_form_type> standard_form_pair;
34 :
35 : /// \brief Traverser that implements the standard form normalization.
36 : class standard_form_traverser: public pbes_system::pbes_expression_traverser<standard_form_traverser>
37 : {
38 : public:
39 : typedef pbes_system::pbes_expression_traverser<standard_form_traverser> super;
40 :
41 : using super::apply;
42 : using super::enter;
43 : using super::leave;
44 :
45 : /// \brief If true, the result will be in standard recursive normal form, otherwise in standard form.
46 : bool m_recursive_form;
47 :
48 : /// \brief The fixpoint symbol of the current equation.
49 : fixpoint_symbol m_symbol;
50 :
51 : /// \brief The name of the variable of the current equation, with a trailing underscore added.
52 : std::string m_name;
53 :
54 : /// \brief Is set to true if the value true is encountered in the PBES.
55 : bool m_has_true;
56 :
57 : /// \brief Is set to true if the value false is encountered in the PBES.
58 : bool m_has_false;
59 :
60 : /// \brief For generating fresh variables.
61 : utilities::number_postfix_generator m_generator;
62 :
63 : /// \brief A stack containing sub-terms.
64 : std::vector<standard_form_pair> m_expression_stack;
65 :
66 : /// \brief A vector containing generated equations.
67 : std::vector<pbes_equation> m_equations;
68 :
69 : /// \brief A vector containing generated equations with new variables.
70 : std::vector<pbes_equation> m_equations2;
71 :
72 : /// \brief Maps right hand sides of equations to their corresponding left hand side.
73 : std::map<pbes_expression, propositional_variable_instantiation> m_table;
74 :
75 : /// \brief The expression corresponding to true.
76 : pbes_expression m_true;
77 :
78 : /// \brief The expression corresponding to false.
79 : pbes_expression m_false;
80 :
81 : /// \brief Pops the stack and returns the popped element
82 41 : standard_form_pair pop()
83 : {
84 41 : standard_form_pair result = m_expression_stack.back();
85 41 : m_expression_stack.pop_back();
86 41 : return result;
87 : }
88 :
89 : /// \brief Pushes (first, second) on the stack.
90 41 : void push(const pbes_expression& first, standard_form_type second)
91 : {
92 41 : m_expression_stack.push_back(standard_form_pair(first, second));
93 41 : }
94 :
95 : /// \brief Generates a fresh pbes variable.
96 12 : propositional_variable fresh_variable(const std::string& hint)
97 : {
98 24 : core::identifier_string s = m_generator(hint);
99 36 : return propositional_variable(s, data::variable_list());
100 12 : }
101 :
102 : /// \brief Generates an equation var=expr for the expression expr (if it does not exist).
103 : /// \return The variable var.
104 2 : propositional_variable_instantiation create_variable(const pbes_expression& expr, standard_form_type type, const std::string& hint)
105 : {
106 2 : std::map<pbes_expression, propositional_variable_instantiation>::iterator i = m_table.find(expr);
107 2 : if (i != m_table.end())
108 : {
109 0 : return i->second;
110 : }
111 2 : propositional_variable var=fresh_variable(hint);
112 2 : propositional_variable_instantiation varinst(var.name(), data::data_expression_list());;
113 2 : m_table[expr] = varinst;
114 2 : if (type == standard_form_and)
115 : {
116 2 : m_equations2.push_back(pbes_equation(m_symbol, var, expr));
117 : }
118 : else
119 : {
120 0 : m_equations2.push_back(pbes_equation(m_symbol, var, expr));
121 : }
122 2 : return varinst;
123 2 : }
124 :
125 : /// \brief Constructor.
126 : /// \param recursive_form Determines whether or not the result will be in standard recursive normal form.
127 7 : standard_form_traverser(bool recursive_form = false)
128 7 : : m_recursive_form(recursive_form),
129 7 : m_has_true(false),
130 7 : m_has_false(false)
131 : {
132 7 : if (m_recursive_form)
133 : {
134 5 : m_true = propositional_variable_instantiation(fresh_variable("True").name(), data::data_expression_list());
135 5 : m_false = propositional_variable_instantiation(fresh_variable("False").name(), data::data_expression_list());
136 : }
137 : else
138 : {
139 2 : m_true = true_();
140 2 : m_false = false_();
141 : }
142 7 : }
143 :
144 : /// \brief Returns the top element of the expression stack, which is the result of the normalization.
145 : pbes_expression result() const
146 : {
147 : return m_expression_stack.back().first;
148 : }
149 :
150 : /// \brief Returns the generated equations.
151 : const std::vector<pbes_equation>& equations() const
152 : {
153 : return m_equations;
154 : }
155 :
156 : /* /// \brief Enter true node.
157 : /// \param x A term.
158 : void enter(const true_& x)
159 : {
160 : (void)x; // Suppress a non used variable warning.
161 : m_has_true = true;
162 : push(m_true, standard_form_both);
163 : }
164 :
165 : /// \brief Enter false node
166 : /// \param x A term
167 : void enter(const false_& x)
168 : {
169 : (void)x; // Suppress a non used variable warning.
170 : m_has_false = true;
171 : push(m_false, standard_form_both);
172 : } */
173 :
174 : /// \brief Enter a data_expression that must be either true or false.
175 : /// \param x A term
176 2 : void enter(const data::data_expression& x)
177 : {
178 2 : if (is_false(x))
179 : {
180 0 : m_has_false = true;
181 0 : push(m_false, standard_form_both);
182 : }
183 : else
184 : {
185 2 : assert(is_true(x));
186 2 : m_has_true = true;
187 2 : push(m_true, standard_form_both);
188 : }
189 2 : }
190 :
191 : /// \brief Enter propositional_variable node.
192 : /// \param x A pbes variable.
193 26 : void enter(const propositional_variable_instantiation& x)
194 : {
195 26 : push(x, standard_form_both);
196 26 : }
197 :
198 : /// \brief Leave not node.
199 0 : void leave(const not_& /* x */)
200 : {
201 0 : throw mcrl2::runtime_error("negation is not supported in standard recursive form algorithm");
202 : }
203 :
204 : /// \brief Leave and node
205 7 : void leave(const and_& /* x */)
206 : {
207 7 : standard_form_pair right = pop();
208 7 : standard_form_pair left = pop();
209 7 : if (left.second == standard_form_or)
210 : {
211 0 : left.first = create_variable(left.first, standard_form_or, m_name);
212 : }
213 7 : if (right.second == standard_form_or)
214 : {
215 0 : right.first = create_variable(right.first, standard_form_or, m_name);
216 : }
217 7 : push(and_(left.first, right.first), standard_form_and);
218 7 : }
219 :
220 : /// \brief Leave or node
221 6 : void leave(const or_& /* x */)
222 : {
223 6 : standard_form_pair right = pop();
224 6 : standard_form_pair left = pop();
225 6 : if (left.second == standard_form_and)
226 : {
227 0 : left.first = create_variable(left.first, standard_form_and, m_name);
228 : }
229 6 : if (right.second == standard_form_and)
230 : {
231 2 : right.first = create_variable(right.first, standard_form_and, m_name);
232 : }
233 6 : push(or_(left.first, right.first), standard_form_or);
234 6 : }
235 :
236 : /// \brief Leave imp node
237 0 : void leave(const imp& /* x */)
238 : {
239 0 : throw mcrl2::runtime_error("implication is not supported in standard recursive form algorithm");
240 : }
241 :
242 : /// \brief Enter an equation
243 15 : void enter(const pbes_equation& eq)
244 : {
245 15 : m_symbol = eq.symbol();
246 15 : m_name = std::string(eq.variable().name()) + '_';
247 15 : }
248 :
249 : /// \brief Leave an equation
250 15 : void leave(const pbes_equation& eq)
251 : {
252 15 : standard_form_pair p = pop();
253 15 : m_equations.push_back(pbes_equation(eq.symbol(), eq.variable(), p.first));
254 : // m_table[p.first] = eq.variable();
255 15 : }
256 :
257 : /// \brief Enter a pbes equation system.
258 7 : void enter(const pbes& x)
259 : {
260 7 : assert(!x.equations().empty());
261 22 : for (const pbes_equation& eqn: x.equations())
262 : {
263 15 : m_generator.add_identifier(std::string(eqn.variable().name()));
264 : }
265 7 : }
266 :
267 : /// \brief Leave a pbes equation system.
268 7 : void leave(const pbes&)
269 : {
270 : // set the fixpoint symbol for the added equations m_equations2, and move them to m_equations
271 7 : assert(!m_equations.empty());
272 7 : fixpoint_symbol sigma = m_equations.back().symbol();
273 9 : for (pbes_equation& eqn: m_equations2)
274 : {
275 2 : eqn.symbol() = sigma;
276 : }
277 7 : std::copy(m_equations2.begin(), m_equations2.end(), std::back_inserter(m_equations));
278 :
279 : // add equations for true and false if needed
280 7 : if (m_recursive_form)
281 : {
282 5 : if (m_has_true)
283 : {
284 1 : m_equations.push_back(pbes_equation(fixpoint_symbol::nu(),
285 2 : propositional_variable(atermpp::down_cast<propositional_variable_instantiation>(m_true).name()),
286 1 : m_true));
287 : }
288 5 : if (m_has_false)
289 : {
290 0 : m_equations.push_back(pbes_equation(fixpoint_symbol::mu(),
291 0 : propositional_variable(atermpp::down_cast<propositional_variable_instantiation>(m_false).name()),
292 0 : m_false));
293 : }
294 : }
295 7 : }
296 :
297 : };
298 :
299 : } // namespace detail
300 :
301 : /// \brief Transforms a PBES into standard form.
302 : /// \param eqn A pbes equation system
303 : /// \param recursive_form Determines whether or not the result will be in standard recursive normal form
304 : inline
305 7 : void make_standard_form(pbes& eqn, bool recursive_form = false)
306 : {
307 7 : detail::standard_form_traverser t(recursive_form);
308 7 : t.apply(eqn);
309 7 : assert(!is_propositional_variable(eqn.initial_state()) || eqn.equations().begin()->variable() == propositional_variable(eqn.initial_state()));
310 7 : assert(!is_propositional_variable(eqn.initial_state()) || t.m_equations.begin()->variable() == propositional_variable(eqn.initial_state()));
311 7 : eqn.equations() = t.m_equations;
312 7 : }
313 :
314 : } // namespace pbes_system
315 :
316 : } // namespace mcrl2
317 :
318 : #endif // MCRL2_PBES_NORMAL_FORMS_H
|
