mCRL2
Loading...
Searching...
No Matches
regfrmtrans.cpp
Go to the documentation of this file.
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//
10
13
14using namespace mcrl2::core;
15using namespace mcrl2::core::detail;
16using namespace mcrl2::data;
17using namespace mcrl2::state_formulas;
18using namespace mcrl2::regular_formulas;
19
20namespace mcrl2
21{
22namespace regular_formulas
23{
24namespace detail
25{
26
27//local declarations
28//------------------
29
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
41{
42 xyz_identifier_generator xyz_generator(find_identifiers(state_frm));
43 return translate_reg_frms_appl(state_frm, xyz_generator);
44}
45
47{
48 if (data::is_data_expression(part) ||
51 data::is_assignment(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 else if (state_formulas::is_must(part))
64 {
65 //part is the must operator; return equivalent non-regular formula
66 const regular_formula reg_frm = must(part).formula();
67 const state_formula phi = must(part).operand();
68 if (regular_formulas::is_seq(reg_frm))
69 {
70 const regular_formula R1 = seq(reg_frm).left();
71 const regular_formula R2 = seq(reg_frm).right();
72 //red([R1.R2]phi) -> red([R1][R2]phi)
73 part = translate_reg_frms_appl(must(R1, must(R2, phi)),xyz_generator);
74 }
75 else if (regular_formulas::is_alt(reg_frm))
76 {
77 const regular_formula R1 = alt(reg_frm).left();
78 const regular_formula R2 = alt(reg_frm).right();
79 //red([R1+R2]phi) -> red([R1]phi) && red([R2]phi)
81 translate_reg_frms_appl(must(R1,phi),xyz_generator),
82 translate_reg_frms_appl(must(R2,phi),xyz_generator)
83 );
84 }
85 else if (regular_formulas::is_trans(reg_frm))
86 {
87 const regular_formula R = trans(atermpp::aterm(reg_frm)).operand();
88 //red([R+]phi) -> red([R.R*]phi)
89 part = translate_reg_frms_appl(must(seq(R,trans_or_nil(R)),phi),xyz_generator);
90 }
91 else if (regular_formulas::is_trans_or_nil(reg_frm))
92 {
94 //red([R*]phi) -> nu X. red(phi) && red([R]X),
95 //where X does not occur free in phi and R
96 const identifier_string X = xyz_generator("X");
98 translate_reg_frms_appl(phi,xyz_generator),
100 ));
101 }
102 else
103 {
104 //reg_frm is an action formula; reduce phi
105 part = must(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
106 }
107 }
108 else if (state_formulas::is_may(part))
109 {
110 //part is the may operator; return equivalent non-regular formula
111 regular_formula reg_frm = may(part).formula();
112 state_formula phi = may(part).operand();
113 if (regular_formulas::is_seq(reg_frm))
114 {
115 const regular_formula R1 = seq(reg_frm).left();
116 const regular_formula R2 = seq(reg_frm).right();
117 //red(<R1.R2>phi) -> red(<R1><R2>phi)
118 part = translate_reg_frms_appl(may(R1, may(R2, phi)),xyz_generator);
119 }
120 else if (regular_formulas::is_alt(reg_frm))
121 {
122 const regular_formula R1 = alt(reg_frm).left();
123 const regular_formula R2 = alt(reg_frm).right();
124 //red(<R1+R2>phi) -> red(<R1>phi) || red(<R2>phi)
125 part = state_formulas::or_(
126 translate_reg_frms_appl(may(R1,phi),xyz_generator),
127 translate_reg_frms_appl(may(R2,phi),xyz_generator)
128 );
129 }
130 else if (regular_formulas::is_trans(reg_frm))
131 {
132 const regular_formula R = trans(atermpp::aterm(reg_frm)).operand();
133 //red(<R+>phi) -> red(<R.R*>phi)
134 part = translate_reg_frms_appl(may(seq(R,trans_or_nil(R)),phi),xyz_generator);
135 }
136 else if (regular_formulas::is_trans_or_nil(reg_frm))
137 {
139 //red(<R*>phi) -> mu X. red(phi) || red(<R>X),
140 //where X does not occur free in phi and R
141 const identifier_string X =xyz_generator("X");
143 translate_reg_frms_appl(phi,xyz_generator),
145 ));
146 }
147 else
148 {
149 //reg_frm is an action formula; reduce phi
150 part = may(reg_frm, translate_reg_frms_appl(phi,xyz_generator));
151 }
152 }
153 else if (state_formulas::is_not(part))
154 {
155 const state_formulas::not_& not_part = atermpp::down_cast<state_formulas::not_>(part);
156 part = state_formulas::not_(translate_reg_frms_appl(not_part.operand(),xyz_generator));
157 }
158 else if (state_formulas::is_minus(part))
159 {
160 const state_formulas::minus& minus_part = atermpp::down_cast<state_formulas::minus>(part);
161 part = state_formulas::minus(translate_reg_frms_appl(minus_part.operand(),xyz_generator));
162 }
163 else if (state_formulas::is_and(part))
164 {
165 part = state_formulas::and_(translate_reg_frms_appl(state_formulas::and_(part).left(),xyz_generator),
166 translate_reg_frms_appl(state_formulas::and_(part).right(),xyz_generator));
167 }
168 else if (state_formulas::is_or(part))
169 {
170 part = state_formulas::or_(translate_reg_frms_appl(state_formulas::or_(part).left(),xyz_generator),
171 translate_reg_frms_appl(state_formulas::or_(part).right(),xyz_generator));
172 }
173 else if (state_formulas::is_imp(part))
174 {
175 part = state_formulas::imp(translate_reg_frms_appl(state_formulas::imp(part).left(),xyz_generator),
176 translate_reg_frms_appl(state_formulas::imp(part).right(),xyz_generator));
177 }
178 else if (state_formulas::is_plus(part))
179 {
180 part = state_formulas::plus(translate_reg_frms_appl(state_formulas::plus(part).left(),xyz_generator),
181 translate_reg_frms_appl(state_formulas::plus(part).right(),xyz_generator));
182 }
184 {
186 translate_reg_frms_appl(state_formulas::const_multiply(part).right(),xyz_generator));
187 }
189 {
192 }
193 else if (state_formulas::is_forall(part))
194 {
196 translate_reg_frms_appl(mcrl2::state_formulas::forall(part).body(),xyz_generator));
197 }
198 else if (state_formulas::is_exists(part))
199 {
201 translate_reg_frms_appl(mcrl2::state_formulas::exists(part).body(),xyz_generator));
202 }
203 else if (state_formulas::is_infimum(part))
204 {
206 translate_reg_frms_appl(mcrl2::state_formulas::infimum(part).body(),xyz_generator));
207 }
208 else if (state_formulas::is_supremum(part))
209 {
211 translate_reg_frms_appl(mcrl2::state_formulas::supremum(part).body(),xyz_generator));
212 }
213 else if (state_formulas::is_sum(part))
214 {
216 translate_reg_frms_appl(mcrl2::state_formulas::sum(part).body(),xyz_generator));
217 }
218 else if (state_formulas::is_nu(part))
219 {
220 const nu nu_part(part);
221 part = nu(nu_part.name(),nu_part.assignments(),
222 translate_reg_frms_appl(nu_part.operand(),xyz_generator));
223 }
224 else if (state_formulas::is_mu(part))
225 {
226 const mu mu_part(part);
227 part = mu(mu_part.name(),mu_part.assignments(),
228 translate_reg_frms_appl(mu_part.operand(),xyz_generator));
229 }
230 else
231 {
232 assert(0); //Unexpected state_formula.
233 }
234
235 return part;
236}
237
238} // namespace detail
239} // namespace regular_formulas
240} // namespace mcrl2
Term containing a string.
Identifier generator that generates names from the range X, Y, Z, X0, Y0, Z0, X1, ....
\brief The alt operator for regular formulas
const regular_formula & right() const
const regular_formula & left() const
\brief The seq operator for regular formulas
const regular_formula & right() const
const regular_formula & left() const
\brief The 'trans or nil' operator for regular formulas
const regular_formula & operand() const
\brief The trans operator for regular formulas
const regular_formula & operand() const
\brief The and operator for state formulas
\brief The multiply operator for state formulas with values
\brief The multiply operator for state formulas with values
\brief The existential quantification operator for state formulas
\brief The universal quantification operator for state formulas
\brief The implication operator for state formulas
\brief The infimum over a data type for state formulas
\brief The may operator for state formulas
const state_formula & operand() const
const regular_formulas::regular_formula & formula() const
\brief The minus operator for state formulas
const state_formula & operand() const
\brief The mu operator for state formulas
const core::identifier_string & name() const
const data::assignment_list & assignments() const
const state_formula & operand() const
\brief The must operator for state formulas
const regular_formulas::regular_formula & formula() const
const state_formula & operand() const
\brief The not operator for state formulas
const state_formula & operand() const
\brief The nu operator for state formulas
const core::identifier_string & name() const
const state_formula & operand() const
const data::assignment_list & assignments() const
\brief The or operator for state formulas
\brief The plus operator for state formulas with values
\brief The sum over a data type for state formulas
\brief The supremum over a data type for state formulas
\brief The state formula variable
Namespace for all data library functionality.
Definition abstraction.h:22
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:155
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
bool is_multi_action(const atermpp::aterm &x)
mcrl2::state_formulas::state_formula translate_reg_frms(const mcrl2::state_formulas::state_formula &state_frm)
Translate regular formulas in terms of state and action formulas.
state_formula translate_reg_frms_appl(state_formula part, xyz_identifier_generator &xyz_generator)
bool is_alt(const atermpp::aterm &x)
bool is_trans(const atermpp::aterm &x)
bool is_trans_or_nil(const atermpp::aterm &x)
bool is_seq(const atermpp::aterm &x)
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:231
bool is_infimum(const atermpp::aterm &x)
bool is_and(const atermpp::aterm &x)
bool is_delay_timed(const atermpp::aterm &x)
bool is_const_multiply(const atermpp::aterm &x)
bool is_minus(const atermpp::aterm &x)
bool is_exists(const atermpp::aterm &x)
bool is_not(const atermpp::aterm &x)
bool is_supremum(const atermpp::aterm &x)
bool is_must(const atermpp::aterm &x)
bool is_yaled(const atermpp::aterm &x)
bool is_true(const atermpp::aterm &x)
bool is_variable(const atermpp::aterm &x)
bool is_may(const atermpp::aterm &x)
bool is_yaled_timed(const atermpp::aterm &x)
bool is_imp(const atermpp::aterm &x)
bool is_sum(const atermpp::aterm &x)
bool is_nu(const atermpp::aterm &x)
bool is_delay(const atermpp::aterm &x)
bool is_false(const atermpp::aterm &x)
bool is_plus(const atermpp::aterm &x)
bool is_mu(const atermpp::aterm &x)
bool is_forall(const atermpp::aterm &x)
bool is_const_multiply_alt(const atermpp::aterm &x)
bool is_or(const atermpp::aterm &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Translate regular formulas in terms of state and action formulas.
Class that generates identifiers in the range X, Y, Z, X0, Y0, Z0, X1, ...