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/lps2pbes.h
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_PBES_LPS2PBES_H
13 : #define MCRL2_PBES_LPS2PBES_H
14 :
15 : #include "mcrl2/data/merge_data_specifications.h"
16 : #include "mcrl2/lps/detail/make_timed_lps.h"
17 : #include "mcrl2/lps/linearise.h"
18 : #include "mcrl2/modal_formula/algorithms.h"
19 : #include "mcrl2/modal_formula/preprocess_state_formula.h"
20 : #include "mcrl2/pbes/algorithms.h"
21 : #include "mcrl2/pbes/detail/lps2pbes_e.h"
22 : #include "mcrl2/pbes/detail/term_traits_optimized.h"
23 : #include "mcrl2/pbes/is_monotonous.h"
24 : #include "mcrl2/process/merge_action_specifications.h"
25 :
26 : namespace mcrl2
27 : {
28 :
29 : namespace pbes_system
30 : {
31 :
32 : /// \brief Algorithm for translating a state formula and a timed specification to a pbes.
33 : class lps2pbes_algorithm
34 : {
35 : protected:
36 : data::set_identifier_generator m_generator;
37 : bool m_check_only = false;
38 :
39 : template <typename Parameters>
40 137 : void run(const state_formulas::state_formula& f, bool structured, bool unoptimized, std::vector<pbes_equation>& equations, Parameters& parameters)
41 : {
42 137 : if (structured)
43 : {
44 0 : if (unoptimized)
45 : {
46 0 : detail::E_structured(f, parameters, equations, core::term_traits<pbes_expression>());
47 : }
48 : else
49 : {
50 0 : detail::E_structured(f, parameters, equations, core::term_traits_optimized<pbes_expression>());
51 : }
52 : }
53 : else
54 : {
55 137 : if (unoptimized)
56 : {
57 0 : detail::E(f, parameters, equations, core::term_traits<pbes_expression>());
58 : }
59 : else
60 : {
61 137 : detail::E(f, parameters, equations, core::term_traits_optimized<pbes_expression>());
62 : }
63 : }
64 137 : }
65 :
66 : public:
67 : /// \brief Constructor
68 137 : explicit lps2pbes_algorithm(bool check_only = false)
69 137 : : m_check_only(check_only)
70 137 : {}
71 :
72 : /// \brief Runs the translation algorithm
73 : /// \param formula A modal formula that represents a property about the system modeled by the given specification
74 : /// \param lpsspec A linear process specification
75 : /// \param structured use the 'structured' approach of generating equations
76 : /// \param unoptimized do not optimize the resulting PBES.
77 : /// \param preprocess_modal_operators insert dummy fixpoints in modal operators, which may lead to smaller PBESs
78 : /// \param generate_counter_example If true, then the PBES is enhanced with additional equations that are used to extract a counter example.
79 : /// \param T The time parameter. If T == data::variable() the untimed version of lps2pbes is applied.
80 : /// \return A PBES that encodes the property applied to the given specification
81 137 : pbes run(const state_formulas::state_formula& formula,
82 : const lps::stochastic_specification& lpsspec,
83 : bool structured = false,
84 : bool unoptimized = false,
85 : bool preprocess_modal_operators = false,
86 : bool generate_counter_example = false,
87 : const data::variable& T = data::undefined_real_variable()
88 : )
89 : {
90 137 : state_formulas::state_formula f = formula;
91 :
92 137 : std::set<core::identifier_string> lps_ids = lps::find_identifiers(lpsspec);
93 137 : std::set<core::identifier_string> dataspec_ids = data::function_and_mapping_identifiers(lpsspec.data());
94 137 : lps_ids.insert(dataspec_ids.begin(), dataspec_ids.end());
95 137 : f = state_formulas::preprocess_state_formula(f, lps_ids, preprocess_modal_operators);
96 :
97 137 : if (m_check_only)
98 : {
99 0 : return pbes();
100 : }
101 :
102 137 : m_generator.clear_context();
103 137 : m_generator.add_identifiers(lps::find_identifiers(lpsspec));
104 137 : m_generator.add_identifiers(data::function_and_mapping_identifiers(lpsspec.data()));
105 137 : m_generator.add_identifiers(state_formulas::find_identifiers(f));
106 :
107 137 : std::vector<pbes_equation> equations;
108 137 : if (generate_counter_example)
109 : {
110 1 : detail::lps2pbes_counter_example_parameters parameters(f, lpsspec.process(), m_generator, T);
111 1 : run(f, structured, unoptimized, equations, parameters);
112 1 : equations = equations + parameters.equations();
113 1 : }
114 : else
115 : {
116 136 : detail::lps2pbes_parameters parameters(f, lpsspec.process(), m_generator, T);
117 136 : run(f, structured, unoptimized, equations, parameters);
118 : }
119 :
120 : // compute the initial state
121 137 : assert(!equations.empty());
122 137 : pbes_equation e1 = equations.front();
123 137 : core::identifier_string Xe(e1.variable().name());
124 137 : assert(state_formulas::is_mu(f) || state_formulas::is_nu(f));
125 137 : const core::identifier_string& Xf = detail::mu_name(f);
126 137 : data::data_expression_list fi = detail::mu_expressions(f);
127 137 : data::data_expression_list pi = lpsspec.initial_process().expressions();
128 274 : data::data_expression_list e = fi + pi + detail::Par(Xf, data::variable_list(), f);
129 137 : if (T != data::undefined_real_variable())
130 : {
131 5 : e.push_front(data::sort_real::real_(0));
132 : }
133 137 : propositional_variable_instantiation init(Xe, e);
134 :
135 137 : pbes result(lpsspec.data(), lpsspec.global_variables(), equations, init);
136 137 : assert(is_monotonous(result));
137 137 : pbes_system::algorithms::normalize(result);
138 137 : assert(pbes_system::algorithms::is_normalized(result));
139 137 : assert(result.is_closed());
140 137 : complete_data_specification(result);
141 137 : return result;
142 137 : }
143 : };
144 :
145 : /// \brief Translates a linear process specification and a state formula to a PBES. If the solution of the PBES
146 : /// is true, the formula holds for the specification.
147 : /// \param lpsspec A stochastic linear process specification.
148 : /// \param formula A modal formula.
149 : /// \param timed determines whether the timed or untimed variant of the algorithm is chosen.
150 : /// \param structured use the 'structured' approach of generating equations.
151 : /// \param unoptimized if true, the resulting PBES is not simplified, if false (default),
152 : /// the PBES is simplified.
153 : /// \param preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to
154 : /// obtain a more compact PBES.
155 : /// \param generate_counter_example A boolean indicating that a counter example must be generated.
156 : /// \return The resulting pbes.
157 : inline
158 137 : pbes lps2pbes(const lps::stochastic_specification& lpsspec,
159 : const state_formulas::state_formula& formula,
160 : bool timed = false,
161 : bool structured = false,
162 : bool unoptimized = false,
163 : bool preprocess_modal_operators = false,
164 : bool generate_counter_example = false,
165 : bool check_only = false
166 : )
167 : {
168 137 : if ((formula.has_time() || lpsspec.process().has_time()) && !timed)
169 : {
170 10 : mCRL2log(log::warning) << "Switch to timed translation because formula has "
171 10 : << (formula.has_time()?"":"no ") << "time, and process has "
172 5 : << (lpsspec.process().has_time()?"":"no ") << "time" << std::endl;
173 5 : timed = true;
174 : }
175 :
176 137 : if (timed)
177 : {
178 5 : lps::stochastic_specification lpsspec_timed = lpsspec;
179 5 : data::set_identifier_generator generator;
180 5 : generator.add_identifiers(lps::find_identifiers(lpsspec));
181 5 : generator.add_identifiers(state_formulas::find_identifiers(formula));
182 5 : generator.add_identifiers(data::function_and_mapping_identifiers(lpsspec.data()));
183 10 : data::variable T(generator("T"), data::sort_real::real_());
184 5 : lps::detail::make_timed_lps(lpsspec_timed.process(), generator.context());
185 10 : return lps2pbes_algorithm(check_only).run(formula, lpsspec_timed, structured, unoptimized, preprocess_modal_operators, generate_counter_example, T);
186 5 : }
187 : else
188 : {
189 264 : return lps2pbes_algorithm(check_only).run(formula, lpsspec, structured, unoptimized, preprocess_modal_operators, generate_counter_example);
190 : }
191 : }
192 :
193 : /// \brief Translates a linear process specification and a state formula to a PBES. If the solution of the PBES
194 : /// is true, the formula holds for the specification.
195 : /// \param lpsspec A linear process specification.
196 : /// \param formula A modal formula.
197 : /// \param timed determines whether the timed or untimed variant of the algorithm is chosen.
198 : /// \param structured use the 'structured' approach of generating equations.
199 : /// \param unoptimized if true, the resulting PBES is not simplified, if false (default),
200 : /// the PBES is simplified.
201 : /// \param preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to
202 : /// obtain a more compact PBES.
203 : /// \param generate_counter_example A boolean indicating that a counter example must be generated.
204 : /// \return The resulting pbes.
205 : inline
206 106 : pbes lps2pbes(const lps::specification& lpsspec,
207 : const state_formulas::state_formula& formula,
208 : bool timed = false,
209 : bool structured = false,
210 : bool unoptimized = false,
211 : bool preprocess_modal_operators = false,
212 : bool generate_counter_example = false,
213 : bool check_only = false
214 : )
215 : {
216 106 : return lps2pbes(lps::stochastic_specification(lpsspec),
217 : formula,
218 : timed,
219 : structured,
220 : unoptimized,
221 : preprocess_modal_operators,
222 : generate_counter_example,
223 212 : check_only);
224 :
225 : }
226 :
227 : /// \brief Translates a linear process specification and a state formula to a PBES. If the solution of the PBES
228 : /// is true, the formula holds for the specification.
229 : /// \param lpsspec A linear process specification.
230 : /// \param formspec A modal formula specification.
231 : /// \param timed determines whether the timed or untimed variant of the algorithm is chosen.
232 : /// \param structured use the 'structured' approach of generating equations.
233 : /// \param unoptimized if true, the resulting PBES is not simplified, if false (default),
234 : /// the PBES is simplified.
235 : /// \param preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to
236 : /// obtain a more compact PBES.
237 : /// \param generate_counter_example A boolean indicating that a counter example must be generated.
238 : /// \param check_only If check_only is true, only the formula will be checked, but no PBES is generated
239 : /// \return The resulting pbes.
240 : inline
241 0 : pbes lps2pbes(const lps::stochastic_specification& lpsspec,
242 : const state_formulas::state_formula_specification& formspec,
243 : bool timed = false,
244 : bool structured = false,
245 : bool unoptimized = false,
246 : bool preprocess_modal_operators = false,
247 : bool generate_counter_example = false,
248 : bool check_only = false
249 : )
250 : {
251 0 : lps::stochastic_specification lpsspec1 = lpsspec;
252 0 : lpsspec1.data() = data::merge_data_specifications(lpsspec1.data(), formspec.data());
253 0 : lps::normalize_sorts(lpsspec1, lpsspec1.data());
254 0 : lpsspec1.action_labels() = process::merge_action_specifications(lpsspec1.action_labels(), formspec.action_labels());
255 0 : return lps2pbes(lpsspec1, formspec.formula(), timed, structured, unoptimized, preprocess_modal_operators, generate_counter_example, check_only);
256 0 : }
257 :
258 : /// \brief Applies the lps2pbes algorithm.
259 : /// \param spec_text A string.
260 : /// \param formula_text A string.
261 : /// \param timed Determines whether the timed or untimed version of the translation algorithm is used.
262 : /// \param structured use the 'structured' approach of generating equations.
263 : /// \param unoptimized if true, the resulting PBES is not simplified, if false (default),
264 : /// the PBES is simplified.
265 : /// \param preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to
266 : /// obtain a more compact PBES.
267 : /// \param generate_counter_example A boolean indicating that a counter example must be generated.
268 : /// \param check_only If check_only is true, only the formula will be checked, but no PBES is generated
269 : /// \return The result of the algorithm
270 : inline
271 1 : pbes lps2pbes(const std::string& spec_text,
272 : const std::string& formula_text,
273 : bool timed = false,
274 : bool structured = false,
275 : bool unoptimized = false,
276 : bool preprocess_modal_operators = false,
277 : bool generate_counter_example = false,
278 : bool check_only = false
279 : )
280 : {
281 1 : pbes result;
282 1 : lps::stochastic_specification lpsspec = lps::linearise(spec_text);
283 1 : lps::specification temp_lpsspec = remove_stochastic_operators(lpsspec); // Just to check that there are no stochastic operators.
284 :
285 1 : const bool formula_is_quantitative = false;
286 1 : state_formulas::state_formula f = state_formulas::algorithms::parse_state_formula(formula_text, lpsspec, formula_is_quantitative);
287 2 : return lps2pbes(lpsspec, f, timed, structured, unoptimized, preprocess_modal_operators, generate_counter_example, check_only);
288 1 : }
289 :
290 : } // namespace pbes_system
291 :
292 : } // namespace mcrl2
293 :
294 : #endif // MCRL2_PBES_LPS2PBES_H
|
