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/lts2pbes_rhs.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_LTS2PBES_RHS_H
13 : #define MCRL2_PBES_DETAIL_LTS2PBES_RHS_H
14 :
15 : #include "mcrl2/pbes/replace.h"
16 : #include "mcrl2/pbes/detail/lps2pbes_par.h"
17 : #include "mcrl2/pbes/detail/lps2pbes_sat.h"
18 : #include "mcrl2/pbes/detail/lts2pbes_lts.h"
19 : #include "mcrl2/utilities/progress_meter.h"
20 :
21 : namespace mcrl2 {
22 :
23 : namespace pbes_system {
24 :
25 : namespace detail {
26 :
27 : typedef lts::lts_lts_t::states_size_type lts2pbes_state_type;
28 :
29 : inline
30 385 : core::identifier_string make_identifier(const core::identifier_string& name, lts2pbes_state_type s)
31 : {
32 770 : return core::identifier_string(std::string(name) + "'" + std::to_string(s));
33 : }
34 :
35 : struct lts2pbes_parameters
36 : {
37 : const state_formulas::state_formula& phi0; // the original formula
38 : const lts::lts_lts_t& lts0;
39 : const lts2pbes_lts& lts1;
40 : data::set_identifier_generator& id_generator;
41 : utilities::progress_meter& pm;
42 :
43 4 : lts2pbes_parameters(const state_formulas::state_formula& phi0_,
44 : const lts::lts_lts_t& lts0_,
45 : const lts2pbes_lts& lts1_,
46 : data::set_identifier_generator& id_generator_,
47 : utilities::progress_meter& pm_
48 : )
49 4 : : phi0(phi0_), lts0(lts0_), lts1(lts1_), id_generator(id_generator_), pm(pm_)
50 4 : {}
51 :
52 : template <typename TermTraits>
53 283 : pbes_expression rhs_may_must(bool is_must,
54 : const pbes_expression& left, // Sat(a(x), alpha)
55 : const pbes_expression& right, // RHS(phi, t)
56 : std::size_t, /* i */
57 : const lps::multi_action& /* a */,
58 : lts2pbes_state_type /* s */,
59 : lts2pbes_state_type /* t */,
60 : TermTraits
61 : )
62 : {
63 : typedef TermTraits tr;
64 283 : if (is_must)
65 : {
66 172 : return tr::imp(left, right);
67 : }
68 : else
69 : {
70 111 : return tr::and_(left, right);
71 : }
72 : }
73 : };
74 :
75 : // TODO: reuse code from lps2pbes_counter_example_parameters
76 : struct lts2pbes_counter_example_parameters: public lts2pbes_parameters
77 : {
78 : std::vector<propositional_variable> Zpos; // represents the additional equations { nu Zpos_i(s, a(i), s) = true }
79 : std::vector<propositional_variable> Zneg; // represents the additional equations { nu Zneg_i(s, a(i), t) = false }
80 : data::variable_list s_list; // contains the process parameter s: Nat
81 : data::variable_list t_list; // contains the process parameter t: Nat
82 :
83 : // creates variables corresponding to the action label sorts in actions
84 0 : data::variable_list action_variables(const process::action_list& actions) const
85 : {
86 0 : std::vector<data::variable> result;
87 0 : for (const process::action& a: actions)
88 : {
89 0 : for (const data::sort_expression& s: a.label().sorts())
90 : {
91 0 : data::variable v(id_generator("v"), s);
92 0 : result.push_back(v);
93 0 : }
94 : }
95 0 : return data::variable_list(result.begin(), result.end());
96 0 : }
97 :
98 : // returns the concatenation of the arguments of the list of actions
99 0 : data::data_expression_list action_expressions(const process::action_list& actions) const
100 : {
101 0 : std::vector<data::data_expression> result;
102 0 : for (const process::action& a: actions)
103 : {
104 0 : auto const& args = a.arguments();
105 0 : result.insert(result.end(), args.begin(), args.end());
106 : }
107 0 : return data::data_expression_list(result.begin(), result.end());
108 0 : }
109 :
110 : // returns the equations needed for counter example generation
111 0 : std::vector<pbes_equation> equations() const
112 : {
113 0 : std::vector<pbes_equation> result;
114 0 : for (auto const& p: Zneg)
115 : {
116 0 : pbes_equation eqn(fixpoint_symbol::nu(), p, false_());
117 0 : result.push_back(eqn);
118 0 : }
119 0 : for (auto const& p: Zpos)
120 : {
121 0 : pbes_equation eqn(fixpoint_symbol::nu(), p, true_());
122 0 : result.push_back(eqn);
123 0 : }
124 0 : return result;
125 0 : }
126 :
127 0 : std::string multi_action_name(const lps::multi_action& a) const
128 : {
129 0 : std::vector<std::string> v;
130 0 : for (const process::action& ai: a.actions())
131 : {
132 0 : v.emplace_back(ai.label().name());
133 : }
134 0 : return utilities::string_join(v, "_");
135 0 : }
136 :
137 0 : lts2pbes_counter_example_parameters(const state_formulas::state_formula& phi0,
138 : const lts::lts_lts_t& lts0,
139 : const lts2pbes_lts& lts1,
140 : data::set_identifier_generator& id_generator,
141 : utilities::progress_meter& pm
142 : )
143 0 : : lts2pbes_parameters(phi0, lts0, lts1, id_generator, pm),
144 0 : s_list { data::variable(id_generator("s"), data::sort_nat::nat()) },
145 0 : t_list { data::variable(id_generator("t"), data::sort_nat::nat()) }
146 : {
147 0 : std::size_t n = lts0.get_transitions().size();
148 0 : Zpos = std::vector<propositional_variable>(n);
149 0 : Zneg = std::vector<propositional_variable>(n);
150 0 : for (const auto& p: lts1.state_map())
151 : {
152 0 : for (const lts2pbes_lts::edge& e: p.second)
153 : {
154 0 : const lps::multi_action& ai = lts1.action_labels()[e.label];
155 0 : data::variable_list actvars = action_variables(ai.actions());
156 0 : std::string suffix = utilities::number2string(e.index) + "_" + multi_action_name(ai);
157 0 : core::identifier_string pos = id_generator("Zpos_" + suffix);
158 0 : core::identifier_string neg = id_generator("Zneg_" + suffix);
159 0 : Zpos[e.index] = propositional_variable(pos, s_list + actvars + t_list);
160 0 : Zneg[e.index] = propositional_variable(neg, s_list + actvars + t_list);
161 0 : }
162 : }
163 0 : }
164 :
165 : data::data_expression equal_to(const data::variable_list& d, const data::data_expression_list& e) const
166 : {
167 : std::vector<data::data_expression> v;
168 : auto i = d.begin();
169 : auto j = e.begin();
170 : for (; i != d.end(); ++i, ++j)
171 : {
172 : v.push_back(data::equal_to(*i, *j));
173 : }
174 : return data::lazy::join_and(v.begin(), v.end());
175 : }
176 :
177 : template <typename TermTraits>
178 0 : pbes_expression rhs_may_must(bool is_must,
179 : const pbes_expression& left, // Sat(a(x), alpha)
180 : const pbes_expression& right, // RHS(phi, t)
181 : std::size_t i, // The index of the transition s --a--> t
182 : const lps::multi_action& a,
183 : lts2pbes_state_type s,
184 : lts2pbes_state_type t,
185 : TermTraits
186 : )
187 : {
188 : typedef TermTraits tr;
189 0 : auto f = action_expressions(a.actions());
190 0 : data::data_expression_list dx = data::data_expression_list({ data::sort_nat::nat(s) }) + f + data::data_expression_list({ data::sort_nat::nat(t) });
191 0 : propositional_variable_instantiation Pos(Zpos[i].name(), dx);
192 0 : propositional_variable_instantiation Neg(Zneg[i].name(), dx);
193 0 : auto right1 = right;
194 :
195 0 : if (is_must)
196 : {
197 0 : right1 = tr::or_(tr::and_(right, Pos), Neg);
198 0 : return tr::imp(left, right1);
199 : }
200 : else
201 : {
202 0 : right1 = tr::and_(tr::or_(right, Neg), Pos);
203 0 : return tr::and_(left, right1);
204 : }
205 0 : }
206 : };
207 :
208 : template <typename TermTraits, typename Parameters>
209 : pbes_expression RHS(const state_formulas::state_formula& x,
210 : lts2pbes_state_type s,
211 : Parameters& parameters,
212 : TermTraits tr);
213 :
214 : template <typename Derived, typename TermTraits, typename Parameters>
215 : struct rhs_lts2pbes_traverser: public state_formulas::state_formula_traverser<Derived>
216 : {
217 : typedef state_formulas::state_formula_traverser<Derived> super;
218 : typedef TermTraits tr;
219 :
220 : using super::enter;
221 : using super::leave;
222 : using super::apply;
223 :
224 : lts2pbes_state_type s;
225 : Parameters& parameters;
226 : std::vector<pbes_expression> result_stack;
227 :
228 401 : rhs_lts2pbes_traverser(lts2pbes_state_type s_,
229 : Parameters& parameters_,
230 : TermTraits
231 : )
232 401 : : s(s_), parameters(parameters_)
233 401 : {}
234 :
235 0 : Derived& derived()
236 : {
237 0 : return static_cast<Derived&>(*this);
238 : }
239 :
240 767 : void push(const pbes_expression& x)
241 : {
242 767 : result_stack.push_back(x);
243 767 : }
244 :
245 767 : pbes_expression& top()
246 : {
247 767 : return result_stack.back();
248 : }
249 :
250 : const pbes_expression& top() const
251 : {
252 : return result_stack.back();
253 : }
254 :
255 366 : pbes_expression pop()
256 : {
257 366 : pbes_expression result = top();
258 366 : result_stack.pop_back();
259 366 : return result;
260 : }
261 :
262 0 : void leave(const data::data_expression& x)
263 : {
264 0 : push(x);
265 0 : }
266 :
267 18 : void leave(const state_formulas::true_&)
268 : {
269 18 : push(true_());
270 18 : }
271 :
272 86 : void leave(const state_formulas::false_&)
273 : {
274 86 : push(false_());
275 86 : }
276 :
277 0 : void apply(const state_formulas::not_&)
278 : {
279 0 : throw mcrl2::runtime_error("rhs_lts2pbes_traverser: negation is not supported!");
280 : }
281 :
282 112 : void leave(const state_formulas::and_&)
283 : {
284 112 : pbes_expression right = pop();
285 112 : pbes_expression left = pop();
286 112 : push(tr::and_(left, right));
287 112 : }
288 :
289 71 : void leave(const state_formulas::or_&)
290 : {
291 71 : pbes_expression right = pop();
292 71 : pbes_expression left = pop();
293 71 : push(tr::or_(left, right));
294 71 : }
295 :
296 0 : void apply(const state_formulas::imp&)
297 : {
298 0 : throw mcrl2::runtime_error("rhs_lts2pbes_traverser: implication is not supported!");
299 : }
300 :
301 0 : void apply(const state_formulas::forall& x)
302 : {
303 0 : derived().apply(x.body());
304 0 : top() = forall(x.variables(), top());
305 0 : }
306 :
307 0 : void apply(const state_formulas::exists& x)
308 : {
309 0 : derived().apply(x.body());
310 0 : top() = exists(x.variables(), top());
311 0 : }
312 :
313 132 : void apply(const state_formulas::must& x)
314 : {
315 132 : const auto& lts1 = parameters.lts1;
316 132 : std::vector<pbes_expression> v;
317 132 : assert(action_formulas::is_action_formula(x.formula()));
318 132 : const auto& alpha = atermpp::down_cast<const action_formulas::action_formula>(x.formula());
319 132 : const state_formulas::state_formula& phi = x.operand();
320 :
321 : // traverse all transitions s --a--> t
322 304 : for (const lts2pbes_lts::edge& e: lts1.edges(s))
323 : {
324 172 : lts2pbes_state_type t = e.state;
325 172 : const lps::multi_action& a = lts1.action_labels()[e.label];
326 172 : pbes_expression left = detail::Sat(a, alpha, parameters.id_generator, TermTraits());
327 172 : pbes_expression right = RHS(phi, t, parameters, TermTraits());
328 172 : pbes_expression p = parameters.rhs_may_must(true, left, right, e.index, a, s, t, TermTraits());
329 172 : v.push_back(p);
330 : }
331 132 : push(tr::join_and(v.begin(), v.end()));
332 132 : }
333 :
334 85 : void apply(const state_formulas::may& x)
335 : {
336 85 : const auto& lts1 = parameters.lts1;
337 85 : std::vector<pbes_expression> v;
338 85 : assert(action_formulas::is_action_formula(x.formula()));
339 85 : const auto& alpha = atermpp::down_cast<const action_formulas::action_formula>(x.formula());
340 85 : const state_formulas::state_formula& phi = x.operand();
341 :
342 : // traverse all transitions s --a--> t
343 196 : for (const lts2pbes_lts::edge& e: lts1.edges(s))
344 : {
345 111 : lts2pbes_state_type t = e.state;
346 111 : const lps::multi_action& a = lts1.action_labels()[e.label];
347 111 : pbes_expression left = detail::Sat(a, alpha, parameters.id_generator, TermTraits());
348 111 : pbes_expression right = RHS(phi, t, parameters, TermTraits());
349 111 : pbes_expression p = parameters.rhs_may_must(false, left, right, e.index, a, s, t, TermTraits());
350 111 : v.push_back(p);
351 : }
352 85 : push(tr::join_or(v.begin(), v.end()));
353 85 : }
354 :
355 0 : void leave(const state_formulas::yaled&)
356 : {
357 0 : throw mcrl2::runtime_error("rhs_lts2pbes_traverser: yaled is not supported!");
358 : }
359 :
360 0 : void leave(const state_formulas::yaled_timed&)
361 : {
362 0 : throw mcrl2::runtime_error("rhs_lts2pbes_traverser: yaled_timed is not supported!");
363 : }
364 :
365 0 : void leave(const state_formulas::delay&)
366 : {
367 0 : throw mcrl2::runtime_error("rhs_lts2pbes_traverser: yaled is not supported!");
368 : }
369 :
370 0 : void leave(const state_formulas::delay_timed&)
371 : {
372 0 : throw mcrl2::runtime_error("rhs_lts2pbes_traverser: delay_timed is not supported!");
373 : }
374 :
375 154 : void leave(const state_formulas::variable& x)
376 : {
377 154 : const core::identifier_string& X = x.name();
378 154 : core::identifier_string X_s = make_identifier(X, s);
379 154 : const data::data_expression_list& e = x.arguments();
380 154 : push(propositional_variable_instantiation(X_s, e + detail::Par(X, data::variable_list(), parameters.phi0)));
381 154 : }
382 :
383 76 : void apply(const state_formulas::nu& x)
384 : {
385 76 : const core::identifier_string& X = x.name();
386 76 : core::identifier_string X_s = make_identifier(X, s);
387 76 : data::data_expression_list e = detail::mu_expressions(x);
388 76 : push(propositional_variable_instantiation(X_s, e + detail::Par(X, data::variable_list(), parameters.phi0)));
389 76 : }
390 :
391 33 : void apply(const state_formulas::mu& x)
392 : {
393 33 : const core::identifier_string& X = x.name();
394 33 : core::identifier_string X_s = make_identifier(X, s);
395 33 : data::data_expression_list e = detail::mu_expressions(x);
396 33 : push(propositional_variable_instantiation(X_s, e + detail::Par(X, data::variable_list(), parameters.phi0)));
397 33 : }
398 : };
399 :
400 : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
401 : struct apply_rhs_lts2pbes_traverser: public Traverser<apply_rhs_lts2pbes_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
402 : {
403 : typedef Traverser<apply_rhs_lts2pbes_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
404 : using super::enter;
405 : using super::leave;
406 : using super::apply;
407 :
408 401 : apply_rhs_lts2pbes_traverser(lts2pbes_state_type s, Parameters& parameters, TermTraits tr)
409 401 : : super(s, parameters, tr)
410 401 : {}
411 : };
412 :
413 : template <typename TermTraits, typename Parameters>
414 401 : pbes_expression RHS(const state_formulas::state_formula& x,
415 : lts2pbes_state_type s,
416 : Parameters& parameters,
417 : TermTraits tr)
418 : {
419 401 : apply_rhs_lts2pbes_traverser<rhs_lts2pbes_traverser, TermTraits, Parameters> f(s, parameters, tr);
420 401 : f.apply(x);
421 802 : return f.top();
422 401 : }
423 :
424 : } // namespace detail
425 :
426 : } // namespace pbes_system
427 :
428 : } // namespace mcrl2
429 :
430 : #endif // MCRL2_PBES_DETAIL_LTS2PBES_RHS_H
|
