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/detail/lps2pbes_e.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_LPS2PBES_E_H
13 : #define MCRL2_PBES_DETAIL_LPS2PBES_E_H
14 :
15 : #include "mcrl2/pbes/detail/lps2pbes_rhs.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace pbes_system {
20 :
21 : namespace detail {
22 :
23 : template <typename TermTraits, typename Parameters>
24 : void E(const state_formulas::state_formula& x,
25 : Parameters& parameters,
26 : std::vector<pbes_equation>& result,
27 : TermTraits tr
28 : );
29 :
30 : template <typename Derived, typename TermTraits, typename Parameters>
31 : struct e_traverser: public state_formulas::state_formula_traverser<Derived>
32 : {
33 : typedef state_formulas::state_formula_traverser<Derived> super;
34 : using super::enter;
35 : using super::leave;
36 : using super::apply;
37 :
38 : typedef std::vector<pbes_equation> result_type;
39 :
40 : Parameters& parameters;
41 : std::vector<result_type> result_stack;
42 :
43 315 : e_traverser(Parameters& parameters_, TermTraits)
44 315 : : parameters(parameters_)
45 315 : {}
46 :
47 : Derived& derived()
48 : {
49 : return static_cast<Derived&>(*this);
50 : }
51 :
52 493 : void push(const result_type& x)
53 : {
54 493 : result_stack.push_back(x);
55 493 : }
56 :
57 808 : result_type& top()
58 : {
59 808 : return result_stack.back();
60 : }
61 :
62 : const result_type& top() const
63 : {
64 : return result_stack.back();
65 : }
66 :
67 178 : result_type pop()
68 : {
69 178 : result_type result = top();
70 178 : result_stack.pop_back();
71 178 : return result;
72 : }
73 :
74 178 : bool is_timed() const
75 : {
76 178 : return parameters.T != data::undefined_real_variable();
77 : }
78 :
79 : // the empty equation list
80 226 : result_type epsilon() const
81 : {
82 226 : return result_type();
83 : }
84 :
85 16 : void leave(const data::data_expression&)
86 : {
87 16 : push(epsilon());
88 16 : }
89 :
90 62 : void leave(const state_formulas::true_&)
91 : {
92 62 : push(epsilon());
93 62 : }
94 :
95 59 : void leave(const state_formulas::false_&)
96 : {
97 59 : push(epsilon());
98 59 : }
99 :
100 0 : void apply(const state_formulas::not_&)
101 : {
102 0 : throw mcrl2::runtime_error("e_traverser: negation is not supported!");
103 : }
104 :
105 49 : void leave(const state_formulas::and_&)
106 : {
107 49 : std::vector<pbes_equation> right = pop();
108 49 : std::vector<pbes_equation> left = pop();
109 49 : push(left + right);
110 49 : }
111 :
112 40 : void leave(const state_formulas::or_&)
113 : {
114 40 : std::vector<pbes_equation> right = pop();
115 40 : std::vector<pbes_equation> left = pop();
116 40 : push(left + right);
117 40 : }
118 :
119 0 : void apply(const state_formulas::imp&)
120 : {
121 0 : throw mcrl2::runtime_error("e_traverser: implication is not supported!");
122 : }
123 :
124 11 : void leave(const state_formulas::forall&)
125 : {
126 : // skip
127 11 : }
128 :
129 4 : void leave(const state_formulas::exists&)
130 : {
131 : // skip
132 4 : }
133 :
134 111 : void leave(const state_formulas::must&)
135 : {
136 : // skip
137 111 : }
138 :
139 86 : void leave(const state_formulas::may&)
140 : {
141 : // skip
142 86 : }
143 :
144 0 : void leave(const state_formulas::yaled&)
145 : {
146 0 : push(epsilon());
147 0 : }
148 :
149 2 : void leave(const state_formulas::yaled_timed&)
150 : {
151 2 : push(epsilon());
152 2 : }
153 :
154 0 : void leave(const state_formulas::delay&)
155 : {
156 0 : push(epsilon());
157 0 : }
158 :
159 2 : void leave(const state_formulas::delay_timed&)
160 : {
161 2 : push(epsilon());
162 2 : }
163 :
164 85 : void leave(const state_formulas::variable&)
165 : {
166 85 : push(epsilon());
167 85 : }
168 :
169 : template <typename Expr>
170 178 : void apply_mu_nu(const Expr& x, const fixpoint_symbol& sigma)
171 : {
172 178 : const core::identifier_string& X = x.name();
173 178 : data::variable_list xf = detail::mu_variables(x);
174 178 : data::variable_list xp = parameters.lps.process_parameters();
175 178 : const state_formulas::state_formula& phi = x.operand();
176 356 : data::variable_list e = xf + xp + Par(X, data::variable_list(), parameters.phi0);
177 178 : if (is_timed())
178 : {
179 6 : e.push_front(parameters.T);
180 : }
181 178 : propositional_variable v(X, e);
182 178 : pbes_expression expr = detail::RHS(phi, parameters, TermTraits());
183 178 : pbes_equation eqn(sigma, v, expr);
184 534 : std::vector<pbes_equation> result = { eqn };
185 178 : E(phi, parameters, result, TermTraits());
186 178 : push(result);
187 178 : }
188 :
189 136 : void apply(const state_formulas::nu& x)
190 : {
191 136 : apply_mu_nu(x, fixpoint_symbol::nu());
192 136 : mCRL2log(log::trace) << "E(" << x << ") = " << core::detail::print_list(top()) << std::endl;
193 136 : }
194 :
195 42 : void apply(const state_formulas::mu& x)
196 : {
197 42 : apply_mu_nu(x, fixpoint_symbol::mu());
198 42 : mCRL2log(log::trace) << "E(" << x << ") = " << core::detail::print_list(top()) << std::endl;
199 42 : }
200 : };
201 :
202 : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
203 : struct apply_e_traverser: public Traverser<apply_e_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
204 : {
205 : typedef Traverser<apply_e_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
206 : using super::enter;
207 : using super::leave;
208 : using super::apply;
209 :
210 315 : apply_e_traverser(Parameters& parameters, TermTraits tr)
211 315 : : super(parameters, tr)
212 315 : {}
213 : };
214 :
215 : template <typename TermTraits, typename Parameters>
216 315 : void E(const state_formulas::state_formula& x, Parameters& parameters, std::vector<pbes_equation>& result, TermTraits tr)
217 : {
218 315 : apply_e_traverser<e_traverser, TermTraits, Parameters> f(parameters, tr);
219 315 : f.apply(x);
220 315 : assert(f.result_stack.size() == 1);
221 315 : result.insert(result.end(), f.top().begin(), f.top().end());
222 315 : }
223 :
224 : template <typename TermTraits, typename Parameters>
225 : void E_structured(const state_formulas::state_formula& x,
226 : Parameters& parameters,
227 : std::vector<pbes_equation>& result,
228 : TermTraits tr
229 : );
230 :
231 : template <typename Derived, typename TermTraits, typename Parameters>
232 : struct e_structured_traverser: public e_traverser<Derived, TermTraits, Parameters>
233 : {
234 : typedef e_traverser<Derived, TermTraits, Parameters> super;
235 : using super::enter;
236 : using super::leave;
237 : using super::apply;
238 : using super::push;
239 : using super::top;
240 : using super::pop;
241 : using super::is_timed;
242 : using super::epsilon;
243 : using super::parameters;
244 :
245 : // typedef std::vector<pbes_equation> result_type;
246 :
247 0 : e_structured_traverser(Parameters& parameters,
248 : TermTraits tr
249 : )
250 0 : : super(parameters, tr)
251 0 : {}
252 :
253 : Derived& derived()
254 : {
255 : return static_cast<Derived&>(*this);
256 : }
257 :
258 : template <typename Expr>
259 0 : void apply_mu_nu(const Expr& x, const fixpoint_symbol& sigma)
260 : {
261 0 : const core::identifier_string& X = x.name();
262 0 : data::variable_list xf = detail::mu_variables(x);
263 0 : data::variable_list xp = parameters.lps.process_parameters();
264 0 : const state_formulas::state_formula& phi = x.operand();
265 0 : data::variable_list d = xf + xp + Par(X, data::variable_list(), parameters.phi0);
266 0 : if (is_timed())
267 : {
268 0 : d.push_front(parameters.T);
269 : }
270 0 : data::data_expression_list e = data::make_data_expression_list(d);
271 0 : propositional_variable v(X, d);
272 0 : std::vector<pbes_equation> equations;
273 0 : pbes_expression expr = detail::RHS_structured(phi, parameters, d, sigma, equations, TermTraits());
274 0 : pbes_equation eqn(sigma, v, expr);
275 0 : std::vector<pbes_equation> result = { eqn };
276 0 : result.insert(result.end(), equations.begin(), equations.end());
277 0 : E_structured(phi, parameters, result, TermTraits());
278 0 : push(result);
279 0 : }
280 :
281 0 : void apply(const state_formulas::nu& x)
282 : {
283 0 : apply_mu_nu(x, fixpoint_symbol::nu());
284 0 : }
285 :
286 0 : void apply(const state_formulas::mu& x)
287 : {
288 0 : apply_mu_nu(x, fixpoint_symbol::mu());
289 0 : }
290 : };
291 :
292 : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
293 : struct apply_e_structured_traverser: public Traverser<apply_e_structured_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
294 : {
295 : typedef Traverser<apply_e_structured_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
296 : using super::enter;
297 : using super::leave;
298 : using super::apply;
299 :
300 0 : apply_e_structured_traverser(Parameters& parameters,
301 : TermTraits tr
302 : )
303 0 : : super(parameters, tr)
304 0 : {}
305 : };
306 :
307 : template <typename TermTraits, typename Parameters>
308 0 : void E_structured(const state_formulas::state_formula& x,
309 : Parameters& parameters,
310 : std::vector<pbes_equation>& result,
311 : TermTraits tr
312 : )
313 : {
314 0 : apply_e_structured_traverser<e_structured_traverser, TermTraits, Parameters> f(parameters, tr);
315 0 : f.apply(x);
316 0 : assert(f.result_stack.size() == 1);
317 0 : result.insert(result.end(), f.top().begin(), f.top().end());
318 0 : }
319 :
320 : } // namespace detail
321 :
322 : } // namespace pbes_system
323 :
324 : } // namespace mcrl2
325 :
326 : #endif // MCRL2_PBES_DETAIL_LPS2PBES_E_H
|