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_e.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_LTS2PBES_E_H
13 : #define MCRL2_PBES_DETAIL_LTS2PBES_E_H
14 :
15 : #include "mcrl2/pbes/detail/lts2pbes_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_lts2pbes(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_lts2pbes_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 26 : e_lts2pbes_traverser(Parameters& parameters_, TermTraits)
44 26 : : parameters(parameters_)
45 26 : {}
46 :
47 : Derived& derived()
48 : {
49 : return static_cast<Derived&>(*this);
50 : }
51 :
52 90 : void push(const result_type& x)
53 : {
54 90 : result_stack.push_back(x);
55 90 : }
56 :
57 116 : result_type& top()
58 : {
59 116 : return result_stack.back();
60 : }
61 :
62 : const result_type& top() const
63 : {
64 : return result_stack.back();
65 : }
66 :
67 64 : result_type pop()
68 : {
69 64 : result_type result = top();
70 64 : result_stack.pop_back();
71 64 : return result;
72 : }
73 :
74 : // the empty equation list
75 36 : result_type epsilon() const
76 : {
77 36 : return result_type();
78 : }
79 :
80 0 : void leave(const data::data_expression&)
81 : {
82 0 : push(epsilon());
83 0 : }
84 :
85 2 : void leave(const state_formulas::true_&)
86 : {
87 2 : push(epsilon());
88 2 : }
89 :
90 12 : void leave(const state_formulas::false_&)
91 : {
92 12 : push(epsilon());
93 12 : }
94 :
95 0 : void apply(const state_formulas::not_&)
96 : {
97 0 : throw mcrl2::runtime_error("e_lts2pbes_traverser: negation is not supported!");
98 : }
99 :
100 18 : void leave(const state_formulas::and_&)
101 : {
102 18 : std::vector<pbes_equation> right = pop();
103 18 : std::vector<pbes_equation> left = pop();
104 18 : push(left + right);
105 18 : }
106 :
107 14 : void leave(const state_formulas::or_&)
108 : {
109 14 : std::vector<pbes_equation> right = pop();
110 14 : std::vector<pbes_equation> left = pop();
111 14 : push(left + right);
112 14 : }
113 :
114 0 : void apply(const state_formulas::imp&)
115 : {
116 0 : throw mcrl2::runtime_error("e_lts2pbes_traverser: implication is not supported!");
117 : }
118 :
119 0 : void leave(const state_formulas::forall&)
120 : {
121 : // skip
122 0 : }
123 :
124 0 : void leave(const state_formulas::exists&)
125 : {
126 : // skip
127 0 : }
128 :
129 24 : void leave(const state_formulas::must&)
130 : {
131 : // skip
132 24 : }
133 :
134 16 : void leave(const state_formulas::may&)
135 : {
136 : // skip
137 16 : }
138 :
139 0 : void leave(const state_formulas::yaled&)
140 : {
141 0 : push(epsilon());
142 0 : }
143 :
144 0 : void leave(const state_formulas::yaled_timed&)
145 : {
146 0 : push(epsilon());
147 0 : }
148 :
149 0 : void leave(const state_formulas::delay&)
150 : {
151 0 : push(epsilon());
152 0 : }
153 :
154 0 : void leave(const state_formulas::delay_timed&)
155 : {
156 0 : push(epsilon());
157 0 : }
158 :
159 22 : void leave(const state_formulas::variable&)
160 : {
161 22 : push(epsilon());
162 22 : }
163 :
164 : template <typename Expr>
165 22 : void handle_mu_nu(const Expr& x, const fixpoint_symbol& sigma)
166 : {
167 22 : const core::identifier_string& X = x.name();
168 22 : data::variable_list d = detail::mu_variables(x);
169 :
170 22 : std::vector<pbes_equation> v;
171 :
172 : // traverse all states of the LTS
173 140 : for (lts2pbes_state_type s = 0; s < parameters.lts1.state_count(); s++)
174 : {
175 118 : core::identifier_string X_s = make_identifier(X, s);
176 236 : propositional_variable Xs(X_s, d + Par(X, data::variable_list(), parameters.phi0));
177 118 : v.push_back(pbes_equation(sigma, Xs, RHS(x.operand(), s, parameters, TermTraits())));
178 118 : parameters.pm.step();
179 : }
180 :
181 22 : E_lts2pbes(x.operand(), parameters, v, TermTraits());
182 22 : push(v);
183 22 : }
184 :
185 12 : void apply(const state_formulas::nu& x)
186 : {
187 12 : handle_mu_nu(x, fixpoint_symbol::nu());
188 12 : }
189 :
190 10 : void apply(const state_formulas::mu& x)
191 : {
192 10 : handle_mu_nu(x, fixpoint_symbol::mu());
193 10 : }
194 : };
195 :
196 : template <template <class, class, class> class Traverser, typename TermTraits, typename Parameters>
197 : struct apply_e_lts2pbes_traverser: public Traverser<apply_e_lts2pbes_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters>
198 : {
199 : typedef Traverser<apply_e_lts2pbes_traverser<Traverser, TermTraits, Parameters>, TermTraits, Parameters> super;
200 : using super::enter;
201 : using super::leave;
202 : using super::apply;
203 :
204 26 : apply_e_lts2pbes_traverser(Parameters& parameters, TermTraits tr)
205 26 : : super(parameters, tr)
206 26 : {}
207 : };
208 :
209 : template <typename TermTraits, typename Parameters>
210 26 : void E_lts2pbes(const state_formulas::state_formula& x,
211 : Parameters& parameters,
212 : std::vector<pbes_equation>& result,
213 : TermTraits tr
214 : )
215 : {
216 26 : apply_e_lts2pbes_traverser<e_lts2pbes_traverser, TermTraits, Parameters> f(parameters, tr);
217 26 : f.apply(x);
218 26 : assert(f.result_stack.size() == 1);
219 26 : result.insert(result.end(), f.top().begin(), f.top().end());
220 26 : }
221 :
222 : } // namespace detail
223 :
224 : } // namespace pbes_system
225 :
226 : } // namespace mcrl2
227 :
228 : #endif // MCRL2_PBES_DETAIL_LTS2PBES_E_H
|
