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/modal_formula/parse.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_MODAL_FORMULA_PARSE_H
13 : #define MCRL2_MODAL_FORMULA_PARSE_H
14 :
15 : #include "mcrl2/data/merge_data_specifications.h"
16 : #include "mcrl2/lps/parse.h"
17 : #include "mcrl2/modal_formula/has_name_clashes.h"
18 : #include "mcrl2/modal_formula/resolve_name_clashes.h"
19 : #include "mcrl2/modal_formula/translate_regular_formulas.h"
20 : #include "mcrl2/modal_formula/translate_user_notation.h"
21 : #include "mcrl2/modal_formula/typecheck.h"
22 : #include "mcrl2/process/merge_action_specifications.h"
23 :
24 : namespace mcrl2
25 : {
26 :
27 : namespace action_formulas
28 : {
29 :
30 : namespace detail {
31 :
32 : action_formula parse_action_formula(const std::string& text);
33 :
34 : } // namespace detail
35 :
36 : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
37 : action_formula parse_action_formula(const std::string& text,
38 : const data::data_specification& dataspec,
39 : const VariableContainer& variables,
40 : const ActionLabelContainer& actions
41 : )
42 : {
43 : action_formula x = detail::parse_action_formula(text);
44 : x = action_formulas::typecheck_action_formula(x, dataspec, variables, actions);
45 : x = action_formulas::translate_user_notation(x);
46 : return x;
47 : }
48 :
49 : inline
50 : action_formula parse_action_formula(const std::string& text, const lps::stochastic_specification& lpsspec)
51 : {
52 : return parse_action_formula(text, lpsspec.data(), lpsspec.global_variables(), lpsspec.action_labels());
53 : }
54 :
55 : } // namespace action_formulas
56 :
57 : namespace regular_formulas
58 : {
59 :
60 : namespace detail
61 : {
62 :
63 : regular_formula parse_regular_formula(const std::string& text);
64 :
65 : } // namespace detail
66 :
67 : template <typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable> >
68 : regular_formula parse_regular_formula(const std::string& text,
69 : const data::data_specification& dataspec,
70 : const VariableContainer& variables,
71 : const ActionLabelContainer& actions
72 : )
73 : {
74 : regular_formula x = detail::parse_regular_formula(text);
75 : x = regular_formulas::typecheck_regular_formula(x, dataspec, variables, actions);
76 : x = regular_formulas::translate_user_notation(x);
77 : return x;
78 : }
79 :
80 : inline
81 : regular_formula parse_regular_formula(const std::string& text, const lps::stochastic_specification& lpsspec)
82 : {
83 : return parse_regular_formula(text, lpsspec.data(), lpsspec.global_variables(), lpsspec.action_labels());
84 : }
85 :
86 : } // namespace regular_formulas
87 :
88 : namespace state_formulas
89 : {
90 :
91 : namespace detail {
92 :
93 : state_formula parse_state_formula(const std::string& text);
94 : state_formula_specification parse_state_formula_specification(const std::string& text);
95 :
96 : } // namespace detail
97 :
98 : struct parse_state_formula_options
99 : {
100 : bool check_monotonicity = true;
101 : bool translate_regular_formulas = true;
102 : bool type_check = true;
103 : bool translate_user_notation = true;
104 : bool resolve_name_clashes = true;
105 : };
106 :
107 : inline
108 178 : state_formula post_process_state_formula(
109 : const state_formula& formula,
110 : parse_state_formula_options options = parse_state_formula_options()
111 : )
112 : {
113 178 : state_formula x = formula;
114 178 : if (options.translate_regular_formulas)
115 : {
116 156 : mCRL2log(log::debug) << "formula before translating regular formulas: " << x << std::endl;
117 156 : x = translate_regular_formulas(x);
118 156 : mCRL2log(log::debug) << "formula after translating regular formulas: " << x << std::endl;
119 : }
120 178 : if (options.translate_user_notation)
121 : {
122 178 : x = state_formulas::translate_user_notation(x);
123 : }
124 178 : if (options.check_monotonicity && !is_monotonous(x))
125 : {
126 0 : throw mcrl2::runtime_error("state formula is not monotonic: " + state_formulas::pp(x));
127 : }
128 178 : if (options.resolve_name_clashes && has_state_variable_name_clashes(x))
129 : {
130 2 : mCRL2log(log::debug) << "formula before resolving name clashes: " << x << std::endl;
131 2 : x = state_formulas::resolve_state_variable_name_clashes(x);
132 2 : mCRL2log(log::debug) << "formula after resolving name clashes: " << x << std::endl;
133 : }
134 178 : return x;
135 0 : }
136 :
137 : /// \brief Parses a state formula from an input stream
138 : /// \param text A string.
139 : /// \param lpsspec A stochastic linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
140 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
141 : /// \param options A set of options guiding parsing.
142 : /// \return The parse result.
143 : inline
144 174 : state_formula parse_state_formula(const std::string& text,
145 : lps::stochastic_specification& lpsspec,
146 : const bool formula_is_quantitative,
147 : parse_state_formula_options options = parse_state_formula_options()
148 : )
149 : {
150 174 : state_formula x = detail::parse_state_formula(text);
151 174 : if (options.type_check)
152 : {
153 174 : x = state_formulas::typecheck_state_formula(x, lpsspec, formula_is_quantitative);
154 : }
155 173 : lpsspec.data().add_context_sorts(state_formulas::find_sort_expressions(x));
156 346 : return post_process_state_formula(x, options);
157 174 : }
158 :
159 : /// \brief Parses a state formula from an input stream
160 : /// \param text A string.
161 : /// \param lpsspec A linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
162 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
163 : /// \param options A set of options guiding parsing.
164 : /// \return The parse result.
165 : inline
166 139 : state_formula parse_state_formula(const std::string& text,
167 : lps::specification& lpsspec,
168 : const bool formula_is_quantitative,
169 : parse_state_formula_options options = parse_state_formula_options()
170 : )
171 : {
172 139 : lps::stochastic_specification stoch_lps_spec=lps::stochastic_specification(lpsspec);
173 139 : state_formula phi = parse_state_formula(text, stoch_lps_spec, formula_is_quantitative, options);
174 138 : lpsspec = remove_stochastic_operators(stoch_lps_spec);
175 276 : return phi;
176 139 : }
177 :
178 : /// \brief Parses a state formula from an input stream
179 : /// \param in A stream.
180 : /// \param lpsspec A stochastic linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
181 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
182 : /// \param options A set of options guiding parsing.
183 : /// \return The parse result.
184 : inline
185 2 : state_formula parse_state_formula(std::istream& in,
186 : lps::stochastic_specification& lpsspec,
187 : const bool formula_is_quantitative,
188 : parse_state_formula_options options = parse_state_formula_options()
189 : )
190 : {
191 2 : std::string text = utilities::read_text(in);
192 4 : return parse_state_formula(text, lpsspec, formula_is_quantitative, options);
193 2 : }
194 :
195 : /// \brief Parses a state formula from an input stream
196 : /// \param in A stream.
197 : /// \param lpsspec A linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
198 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
199 : /// \param options A set of options guiding parsing.
200 : /// \return The parse result.
201 : inline
202 : state_formula parse_state_formula(std::istream& in,
203 : lps::specification& lpsspec,
204 : const bool formula_is_quantitative,
205 : parse_state_formula_options options = parse_state_formula_options()
206 : )
207 : {
208 : lps::stochastic_specification stoch_lps_spec=lps::stochastic_specification(lpsspec);
209 : state_formula phi = parse_state_formula(in, stoch_lps_spec, formula_is_quantitative, options);
210 : lpsspec = remove_stochastic_operators(stoch_lps_spec);
211 : return phi;
212 : }
213 :
214 : /// \brief Parses a state formula specification from a string.
215 : /// \param text A string.
216 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
217 : /// \param options A set of options guiding parsing.
218 : /// \return The parse result.
219 : inline
220 5 : state_formula_specification parse_state_formula_specification(
221 : const std::string& text,
222 : const bool formula_is_quantitative,
223 : parse_state_formula_options options = parse_state_formula_options()
224 : )
225 : {
226 5 : state_formula_specification result = detail::parse_state_formula_specification(text);
227 5 : if (options.type_check)
228 : {
229 5 : result.formula() = state_formulas::typecheck_state_formula(result.formula(), formula_is_quantitative, result.data(), result.action_labels(), data::variable_list());
230 : }
231 5 : result.formula() = post_process_state_formula(result.formula(), options);
232 5 : return result;
233 0 : }
234 :
235 : /// \brief Parses a state formula specification from an input stream.
236 : /// \param in An input stream.
237 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
238 : /// \param options A set of options guiding parsing.
239 : /// \return The parse result.
240 : inline
241 0 : state_formula_specification parse_state_formula_specification(
242 : std::istream& in,
243 : const bool formula_is_quantitative,
244 : parse_state_formula_options options = parse_state_formula_options()
245 : )
246 : {
247 0 : std::string text = utilities::read_text(in);
248 0 : return parse_state_formula_specification(text, formula_is_quantitative, options);
249 0 : }
250 :
251 : /// \brief Parses a state formula specification from a string
252 : /// \param text A string
253 : /// \param lpsspec A linear process containing data and action declarations necessary to type check the state formula.
254 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
255 : /// \param options A set of options guiding parsing.
256 : /// \return The parse result
257 : inline
258 0 : state_formula_specification parse_state_formula_specification(const std::string& text,
259 : lps::stochastic_specification& lpsspec,
260 : const bool formula_is_quantitative,
261 : parse_state_formula_options options = parse_state_formula_options()
262 : )
263 : {
264 0 : state_formula_specification result = detail::parse_state_formula_specification(text);
265 : // Merge data specification checks whether the combined datatypes are well typed.
266 0 : data::data_specification dataspec = data::merge_data_specifications(lpsspec.data(), result.data());
267 0 : process::action_label_list actspec = process::merge_action_specifications(lpsspec.action_labels(), result.action_labels());
268 :
269 0 : if (options.type_check)
270 : {
271 0 : data::data_type_checker type_checker(dataspec);
272 : // The type checker below checks whether the combined action list is well typed.
273 0 : type_checker(result.data().user_defined_equations()); // This changes the data equations in result.data() to become well typed.
274 : // Note that while type checking the formula below the non type checked equations are used. This is not an issue
275 : // as the shape of equations do not influence well typedness of a modal formula.
276 0 : result.formula() = state_formulas::typecheck_state_formula(result.formula(), formula_is_quantitative, dataspec, actspec, lpsspec.global_variables());
277 0 : }
278 :
279 0 : result.formula() = post_process_state_formula(result.formula(), options);
280 0 : return result;
281 0 : }
282 :
283 :
284 : /// \brief Parses a state formula specification from a string
285 : /// \param text A string
286 : /// \param lpsspec A linear process containing data and action declarations necessary to type check the state formula.
287 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
288 : /// \param options A set of options guiding parsing.
289 : /// \return The parse result
290 : inline
291 : state_formula_specification parse_state_formula_specification(const std::string& text,
292 : lps::specification& lpsspec,
293 : const bool formula_is_quantitative,
294 : parse_state_formula_options options = parse_state_formula_options()
295 : )
296 : {
297 : lps::stochastic_specification stoch_lps_spec=lps::stochastic_specification(lpsspec);
298 : state_formula_specification sfs = parse_state_formula_specification(text, stoch_lps_spec, formula_is_quantitative, options);
299 : lpsspec = remove_stochastic_operators(stoch_lps_spec);
300 : return sfs;
301 : }
302 :
303 : /// \brief Parses a state formula specification from an input stream.
304 : /// \param in An input stream.
305 : /// \param lpsspec A stochastic linear process containing data and action declarations necessary to type check the state formula.
306 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
307 : /// \param options A set of options guiding parsing.
308 : /// \return The parse result.
309 : inline
310 0 : state_formula_specification parse_state_formula_specification(std::istream& in,
311 : lps::stochastic_specification& lpsspec,
312 : const bool formula_is_quantitative,
313 : parse_state_formula_options options = parse_state_formula_options()
314 : )
315 : {
316 0 : return parse_state_formula_specification(utilities::read_text(in), lpsspec, formula_is_quantitative, options);
317 : }
318 :
319 : /// \brief Parses a state formula specification from an input stream.
320 : /// \param in An input stream.
321 : /// \param lpsspec A linear process containing data and action declarations necessary to type check the state formula.
322 : /// \param formula_is_quantitative If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
323 : /// \param options A set of options guiding parsing.
324 : /// \return The parse result.
325 : inline
326 : state_formula_specification parse_state_formula_specification
327 : (std::istream& in,
328 : lps::specification& lpsspec,
329 : const bool formula_is_quantitative,
330 : parse_state_formula_options options = parse_state_formula_options()
331 : )
332 : {
333 : lps::stochastic_specification stoch_lps_spec=lps::stochastic_specification(lpsspec);
334 : state_formula_specification sfs = parse_state_formula_specification(in, stoch_lps_spec, formula_is_quantitative, options);
335 : lpsspec = remove_stochastic_operators(stoch_lps_spec);
336 : return sfs;
337 : }
338 : } // namespace state_formulas
339 :
340 : } // namespace mcrl2
341 :
342 : #endif // MCRL2_MODAL_FORMULA_PARSE_H
|
