Line data Source code
1 : // Author(s): Aad Mathijssen
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 regfrmtrans.cpp
10 :
11 : #include "mcrl2/data/xyz_identifier_generator.h"
12 : #include "mcrl2/modal_formula/translate_regular_formulas.h"
13 :
14 : using namespace mcrl2::core;
15 : using namespace mcrl2::core::detail;
16 : using namespace mcrl2::data;
17 : using namespace mcrl2::state_formulas;
18 : using namespace mcrl2::regular_formulas;
19 :
20 : namespace mcrl2
21 : {
22 : namespace regular_formulas
23 : {
24 : namespace detail
25 : {
26 :
27 : //local declarations
28 : //------------------
29 :
30 : inline state_formula translate_reg_frms_appl(state_formula part, xyz_identifier_generator &xyz_generator);
31 : /*Pre: part represents a part of a state formula
32 : * after the data implementation phase
33 : *Ret: part in which all regular formulas are translated in terms of state and
34 : * action formulas
35 : */
36 :
37 : //implementation
38 : //--------------
39 :
40 151 : state_formula translate_reg_frms(const state_formula &state_frm)
41 : {
42 151 : xyz_identifier_generator xyz_generator(find_identifiers(state_frm));
43 302 : return translate_reg_frms_appl(state_frm, xyz_generator);
44 151 : }
45 :
46 807 : inline state_formula translate_reg_frms_appl(state_formula part, xyz_identifier_generator& xyz_generator)
47 : {
48 807 : if (data::is_data_expression(part) ||
49 787 : lps::is_multi_action(part) ||
50 787 : state_formulas::is_variable(part) ||
51 644 : data::is_assignment(part) ||
52 644 : state_formulas::is_true(part) ||
53 560 : state_formulas::is_false(part) ||
54 527 : state_formulas::is_yaled(part) ||
55 527 : state_formulas::is_yaled_timed(part) ||
56 2120 : state_formulas::is_delay(part) ||
57 526 : state_formulas::is_delay_timed(part)
58 : )
59 : {
60 : //part is a data expression, a multiaction, a state variable or a data
61 : //variable declaration (with or without initialisation); return part
62 : }
63 525 : else if (state_formulas::is_must(part))
64 : {
65 : //part is the must operator; return equivalent non-regular formula
66 138 : const regular_formula reg_frm = must(part).formula();
67 138 : const state_formula phi = must(part).operand();
68 138 : if (regular_formulas::is_seq(reg_frm))
69 : {
70 3 : const regular_formula R1 = seq(reg_frm).left();
71 3 : const regular_formula R2 = seq(reg_frm).right();
72 : //red([R1.R2]phi) -> red([R1][R2]phi)
73 3 : part = translate_reg_frms_appl(must(R1, must(R2, phi)),xyz_generator);
74 3 : }
75 135 : else if (regular_formulas::is_alt(reg_frm))
76 : {
77 0 : const regular_formula R1 = alt(reg_frm).left();
78 0 : const regular_formula R2 = alt(reg_frm).right();
79 : //red([R1+R2]phi) -> red([R1]phi) && red([R2]phi)
80 0 : part = state_formulas::and_(
81 0 : translate_reg_frms_appl(must(R1,phi),xyz_generator),
82 0 : translate_reg_frms_appl(must(R2,phi),xyz_generator)
83 0 : );
84 0 : }
85 135 : else if (regular_formulas::is_trans(reg_frm))
86 : {
87 0 : const regular_formula R = trans(atermpp::aterm_appl(reg_frm)).operand();
88 : //red([R+]phi) -> red([R.R*]phi)
89 0 : part = translate_reg_frms_appl(must(seq(R,trans_or_nil(R)),phi),xyz_generator);
90 0 : }
91 135 : else if (regular_formulas::is_trans_or_nil(reg_frm))
92 : {
93 28 : const regular_formula R = trans_or_nil(atermpp::aterm_appl(reg_frm)).operand();
94 : //red([R*]phi) -> nu X. red(phi) && red([R]X),
95 : //where X does not occur free in phi and R
96 28 : const identifier_string X = xyz_generator("X");
97 28 : part = nu(X, assignment_list(), state_formulas::and_(
98 28 : translate_reg_frms_appl(phi,xyz_generator),
99 28 : translate_reg_frms_appl(must(R,mcrl2::state_formulas::variable(X, data_expression_list())),xyz_generator)
100 14 : ));
101 14 : }
102 : else
103 : {
104 : //reg_frm is an action formula; reduce phi
105 121 : part = must(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
106 : }
107 138 : }
108 387 : else if (state_formulas::is_may(part))
109 : {
110 : //part is the may operator; return equivalent non-regular formula
111 78 : regular_formula reg_frm = may(part).formula();
112 78 : state_formula phi = may(part).operand();
113 78 : if (regular_formulas::is_seq(reg_frm))
114 : {
115 0 : const regular_formula R1 = seq(reg_frm).left();
116 0 : const regular_formula R2 = seq(reg_frm).right();
117 : //red(<R1.R2>phi) -> red(<R1><R2>phi)
118 0 : part = translate_reg_frms_appl(may(R1, may(R2, phi)),xyz_generator);
119 0 : }
120 78 : else if (regular_formulas::is_alt(reg_frm))
121 : {
122 0 : const regular_formula R1 = alt(reg_frm).left();
123 0 : const regular_formula R2 = alt(reg_frm).right();
124 : //red(<R1+R2>phi) -> red(<R1>phi) || red(<R2>phi)
125 0 : part = state_formulas::or_(
126 0 : translate_reg_frms_appl(may(R1,phi),xyz_generator),
127 0 : translate_reg_frms_appl(may(R2,phi),xyz_generator)
128 0 : );
129 0 : }
130 78 : else if (regular_formulas::is_trans(reg_frm))
131 : {
132 0 : const regular_formula R = trans(atermpp::aterm_appl(reg_frm)).operand();
133 : //red(<R+>phi) -> red(<R.R*>phi)
134 0 : part = translate_reg_frms_appl(may(seq(R,trans_or_nil(R)),phi),xyz_generator);
135 0 : }
136 78 : else if (regular_formulas::is_trans_or_nil(reg_frm))
137 : {
138 14 : const regular_formula R = trans_or_nil(atermpp::aterm_appl(reg_frm)).operand();
139 : //red(<R*>phi) -> mu X. red(phi) || red(<R>X),
140 : //where X does not occur free in phi and R
141 14 : const identifier_string X =xyz_generator("X");
142 14 : part = mu(X, assignment_list(), state_formulas::or_(
143 14 : translate_reg_frms_appl(phi,xyz_generator),
144 14 : translate_reg_frms_appl(may(R,mcrl2::state_formulas::variable(X, data_expression_list())),xyz_generator)
145 7 : ));
146 7 : }
147 : else
148 : {
149 : //reg_frm is an action formula; reduce phi
150 71 : part = may(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
151 : }
152 78 : }
153 309 : else if (state_formulas::is_not(part))
154 : {
155 29 : const state_formulas::not_& not_part = atermpp::down_cast<state_formulas::not_>(part);
156 29 : part = state_formulas::not_(translate_reg_frms_appl(not_part.operand(),xyz_generator));
157 : }
158 280 : else if (state_formulas::is_minus(part))
159 : {
160 0 : const state_formulas::minus& minus_part = atermpp::down_cast<state_formulas::minus>(part);
161 0 : part = state_formulas::minus(translate_reg_frms_appl(minus_part.operand(),xyz_generator));
162 : }
163 280 : else if (state_formulas::is_and(part))
164 : {
165 134 : part = state_formulas::and_(translate_reg_frms_appl(state_formulas::and_(part).left(),xyz_generator),
166 201 : translate_reg_frms_appl(state_formulas::and_(part).right(),xyz_generator));
167 : }
168 213 : else if (state_formulas::is_or(part))
169 : {
170 40 : part = state_formulas::or_(translate_reg_frms_appl(state_formulas::or_(part).left(),xyz_generator),
171 60 : translate_reg_frms_appl(state_formulas::or_(part).right(),xyz_generator));
172 : }
173 193 : else if (state_formulas::is_imp(part))
174 : {
175 46 : part = state_formulas::imp(translate_reg_frms_appl(state_formulas::imp(part).left(),xyz_generator),
176 69 : translate_reg_frms_appl(state_formulas::imp(part).right(),xyz_generator));
177 : }
178 170 : else if (state_formulas::is_plus(part))
179 : {
180 0 : part = state_formulas::plus(translate_reg_frms_appl(state_formulas::plus(part).left(),xyz_generator),
181 0 : translate_reg_frms_appl(state_formulas::plus(part).right(),xyz_generator));
182 : }
183 170 : else if (state_formulas::is_const_multiply(part))
184 : {
185 0 : part = state_formulas::const_multiply(state_formulas::const_multiply(part).left(),
186 0 : translate_reg_frms_appl(state_formulas::const_multiply(part).right(),xyz_generator));
187 : }
188 170 : else if (state_formulas::is_const_multiply_alt(part))
189 : {
190 0 : part = state_formulas::const_multiply_alt(translate_reg_frms_appl(state_formulas::const_multiply_alt(part).left(),xyz_generator),
191 0 : state_formulas::const_multiply_alt(part).right());
192 : }
193 170 : else if (state_formulas::is_forall(part))
194 : {
195 30 : part = mcrl2::state_formulas::forall(mcrl2::state_formulas::forall(part).variables(),
196 45 : translate_reg_frms_appl(mcrl2::state_formulas::forall(part).body(),xyz_generator));
197 : }
198 155 : else if (state_formulas::is_exists(part))
199 : {
200 12 : part = mcrl2::state_formulas::exists(mcrl2::state_formulas::exists(part).variables(),
201 18 : translate_reg_frms_appl(mcrl2::state_formulas::exists(part).body(),xyz_generator));
202 : }
203 149 : else if (state_formulas::is_infimum(part))
204 : {
205 2 : part = mcrl2::state_formulas::infimum(mcrl2::state_formulas::infimum(part).variables(),
206 3 : translate_reg_frms_appl(mcrl2::state_formulas::infimum(part).body(),xyz_generator));
207 : }
208 148 : else if (state_formulas::is_supremum(part))
209 : {
210 2 : part = mcrl2::state_formulas::supremum(mcrl2::state_formulas::supremum(part).variables(),
211 3 : translate_reg_frms_appl(mcrl2::state_formulas::supremum(part).body(),xyz_generator));
212 : }
213 147 : else if (state_formulas::is_nu(part))
214 : {
215 59 : const nu nu_part(part);
216 118 : part = nu(nu_part.name(),nu_part.assignments(),
217 177 : translate_reg_frms_appl(nu_part.operand(),xyz_generator));
218 59 : }
219 88 : else if (state_formulas::is_mu(part))
220 : {
221 88 : const mu mu_part(part);
222 176 : part = mu(mu_part.name(),mu_part.assignments(),
223 264 : translate_reg_frms_appl(mu_part.operand(),xyz_generator));
224 88 : }
225 : else
226 : {
227 0 : assert(0); //Unexpected state_formula.
228 : }
229 :
230 807 : return part;
231 : }
232 :
233 : } // namespace detail
234 : } // namespace regular_formulas
235 : } // namespace mcrl2
|