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 tools.cpp
10 :
11 : #include "mcrl2/lps/binary.h"
12 : #include "mcrl2/lps/constelm.h"
13 : #include "mcrl2/lps/detail/specification_property_map.h"
14 : #include "mcrl2/lps/invelm_algorithm.h"
15 : #include "mcrl2/lps/io.h"
16 : #include "mcrl2/lps/parelm.h"
17 : #include "mcrl2/lps/parse.h"
18 : #include "mcrl2/lps/sumelm.h"
19 : #include "mcrl2/lps/suminst.h"
20 : #include "mcrl2/lps/tools.h"
21 : #include "mcrl2/lps/untime.h"
22 : #include "mcrl2/lps/one_point_rule_rewrite.h"
23 : #include "mcrl2/lps/rewriters/one_point_condition_rewrite.h"
24 :
25 : namespace mcrl2
26 : {
27 :
28 : namespace lps
29 : {
30 :
31 0 : void lpsbinary(const std::string& input_filename,
32 : const std::string& output_filename,
33 : const std::string& parameter_selection)
34 : {
35 0 : lps::stochastic_specification spec;
36 0 : load_lps(spec, input_filename);
37 0 : data::rewriter r(spec.data());
38 :
39 0 : lps::binary_algorithm<data::rewriter, stochastic_specification>(spec, r, parameter_selection).run();
40 0 : save_lps(spec, output_filename);
41 0 : }
42 :
43 0 : void lpsconstelm(const std::string& input_filename,
44 : const std::string& output_filename,
45 : data::rewriter::strategy rewrite_strategy,
46 : bool instantiate_free_variables,
47 : bool ignore_conditions,
48 : bool remove_trivial_summands,
49 : bool remove_singleton_sorts
50 : )
51 : {
52 0 : lps::stochastic_specification spec;
53 0 : load_lps(spec, input_filename);
54 0 : mcrl2::data::rewriter R(spec.data(), rewrite_strategy);
55 0 : lps::constelm_algorithm<data::rewriter, stochastic_specification> algorithm(spec, R);
56 :
57 : // preprocess: remove single element sorts
58 0 : if (remove_singleton_sorts)
59 : {
60 0 : algorithm.remove_singleton_sorts();
61 : }
62 :
63 : // apply constelm
64 0 : algorithm.run(instantiate_free_variables, ignore_conditions);
65 :
66 : // postprocess: remove trivial summands
67 0 : if (remove_trivial_summands)
68 : {
69 0 : algorithm.remove_trivial_summands();
70 : }
71 :
72 0 : save_lps(spec, output_filename);
73 0 : }
74 :
75 0 : void lpsinfo(const std::string& input_filename,
76 : const std::string& input_file_message
77 : )
78 : {
79 0 : stochastic_specification spec;
80 0 : load_lps(spec, input_filename);
81 0 : lps::detail::specification_property_map<stochastic_specification> info(spec);
82 0 : std::cout << input_file_message << "\n\n";
83 0 : std::cout << info.info();
84 0 : }
85 :
86 0 : bool lpsinvelm(const std::string& input_filename,
87 : const std::string& output_filename,
88 : const std::string& invariant_filename,
89 : const std::string& dot_file_name,
90 : data::rewriter::strategy rewrite_strategy,
91 : data::detail::smt_solver_type solver_type,
92 : const bool no_check,
93 : const bool no_elimination,
94 : const bool simplify_all,
95 : const bool all_violations,
96 : const bool counter_example,
97 : const bool path_eliminator,
98 : const bool apply_induction,
99 : const int time_limit)
100 : {
101 0 : stochastic_specification spec;
102 0 : data::data_expression invariant;
103 :
104 0 : load_lps(spec, input_filename);
105 :
106 0 : if (!invariant_filename.empty())
107 : {
108 0 : std::ifstream instream(invariant_filename.c_str());
109 :
110 0 : if (!instream.is_open())
111 : {
112 0 : throw mcrl2::runtime_error("cannot open input file '" + invariant_filename + "'");
113 : }
114 :
115 0 : mCRL2log(log::verbose) << "parsing input file '" << invariant_filename << "'..." << std::endl;
116 :
117 0 : data::variable_list& parameters=spec.process().process_parameters();
118 0 : invariant = data::parse_data_expression(instream, parameters, spec.data());
119 :
120 0 : instream.close();
121 0 : }
122 : else
123 : {
124 0 : throw mcrl2::runtime_error("A file containing an invariant must be specified using the option --invariant=INVFILE.");
125 : }
126 :
127 0 : if (no_check)
128 : {
129 0 : mCRL2log(log::warning) << "The invariant is not checked; it may not hold for this LPS." << std::endl;
130 : }
131 : else
132 : {
133 : detail::Invariant_Checker<stochastic_specification> v_invariant_checker(spec,
134 : rewrite_strategy,
135 : time_limit,
136 : path_eliminator,
137 : solver_type,
138 : apply_induction,
139 : counter_example,
140 : all_violations,
141 0 : dot_file_name);
142 :
143 0 : if (!v_invariant_checker.check_invariant(invariant))
144 : {
145 0 : return false; // The invariant was checked and found invalid.
146 : }
147 0 : }
148 :
149 : invelm_algorithm<stochastic_specification> algorithm(spec,
150 : rewrite_strategy,
151 : time_limit,
152 : path_eliminator,
153 : solver_type,
154 : apply_induction,
155 0 : simplify_all);
156 0 : algorithm.run(invariant, !no_elimination);
157 0 : save_lps(spec, output_filename);
158 0 : return true;
159 0 : }
160 :
161 0 : void lpsparelm(const std::string& input_filename,
162 : const std::string& output_filename
163 : )
164 : {
165 0 : lps::stochastic_specification spec;
166 0 : load_lps(spec, input_filename);
167 0 : lps::parelm(spec, true);
168 0 : save_lps(spec, output_filename);
169 0 : }
170 :
171 0 : void lpspp(const std::string& input_filename,
172 : const std::string& output_filename,
173 : bool print_summand_numbers,
174 : core::print_format_type format
175 : )
176 : {
177 0 : lps::stochastic_specification spec;
178 0 : load_lps(spec, input_filename);
179 :
180 0 : mCRL2log(log::verbose) << "printing LPS from "
181 0 : << (input_filename.empty()?"standard input":input_filename)
182 0 : << " to " << (output_filename.empty()?"standard output":output_filename)
183 0 : << " in the " << core::pp_format_to_string(format) << " format" << std::endl;
184 :
185 0 : std::string text;
186 0 : if (format == core::print_internal)
187 : {
188 0 : text = pp(specification_to_aterm(spec));
189 : }
190 : else
191 : {
192 0 : text = print_summand_numbers ? lps::pp_with_summand_numbers(spec) : lps::pp(spec);
193 : }
194 0 : if (output_filename.empty())
195 : {
196 0 : std::cout << text;
197 : }
198 : else
199 : {
200 0 : std::ofstream output_stream(output_filename.c_str());
201 0 : if (output_stream)
202 : {
203 0 : output_stream << text;
204 0 : output_stream.close();
205 : }
206 : else
207 : {
208 0 : throw mcrl2::runtime_error("could not open output file " + output_filename + " for writing");
209 : }
210 0 : }
211 0 : }
212 :
213 0 : void lpsrewr(const std::string& input_filename,
214 : const std::string& output_filename,
215 : const data::rewriter::strategy rewrite_strategy,
216 : const lps_rewriter_type rewriter_type
217 : )
218 : {
219 0 : stochastic_specification spec;
220 0 : load_lps(spec, input_filename);
221 0 : switch (rewriter_type)
222 : {
223 0 : case simplify:
224 : {
225 0 : mcrl2::data::rewriter R(spec.data(), rewrite_strategy);
226 0 : lps::rewrite(spec, R);
227 0 : break;
228 0 : }
229 0 : case quantifier_one_point:
230 : {
231 0 : one_point_rule_rewrite(spec);
232 0 : break;
233 : }
234 0 : case condition_one_point:
235 : {
236 0 : mcrl2::data::rewriter R(spec.data(), rewrite_strategy);
237 0 : lps::one_point_condition_rewrite(spec, R);
238 0 : break;
239 0 : }
240 : }
241 0 : lps::remove_trivial_summands(spec);
242 0 : lps::remove_redundant_assignments(spec);
243 0 : save_lps(spec, output_filename);
244 0 : }
245 :
246 0 : void lpssumelm(const std::string& input_filename,
247 : const std::string& output_filename,
248 : const bool decluster)
249 : {
250 0 : stochastic_specification spec;
251 0 : load_lps(spec, input_filename);
252 :
253 0 : sumelm_algorithm<stochastic_specification>(spec, decluster).run();
254 :
255 0 : mCRL2log(log::debug) << "Sum elimination completed, saving to " << output_filename << std::endl;
256 0 : save_lps(spec, output_filename);
257 0 : }
258 :
259 0 : void lpssuminst(const std::string& input_filename,
260 : const std::string& output_filename,
261 : const data::rewriter::strategy rewrite_strategy,
262 : const std::string& sorts_string,
263 : const bool finite_sorts_only,
264 : const bool tau_summands_only)
265 : {
266 0 : stochastic_specification spec;
267 0 : load_lps(spec, input_filename);
268 0 : std::set<data::sort_expression> sorts;
269 :
270 : // Determine set of sorts to be expanded
271 0 : if(!sorts_string.empty())
272 : {
273 0 : std::vector<std::string> parts = utilities::split(utilities::remove_whitespace(sorts_string), ",");
274 0 : for (const std::string& part : parts)
275 : {
276 0 : sorts.insert(data::parse_sort_expression(part, spec.data()));
277 : }
278 0 : }
279 0 : else if (finite_sorts_only)
280 : {
281 0 : sorts = lps::finite_sorts(spec.data());
282 : }
283 : else
284 : {
285 0 : const std::set<data::sort_expression>& sort_set=spec.data().sorts();
286 0 : sorts = std::set<data::sort_expression>(sort_set.begin(),sort_set.end());
287 : }
288 :
289 0 : mCRL2log(log::verbose) << "expanding summation variables of sorts: " << data::pp(sorts) << std::endl;
290 :
291 0 : mcrl2::data::rewriter r(spec.data(), rewrite_strategy);
292 0 : lps::suminst_algorithm<data::rewriter, stochastic_specification>(spec, r, sorts, tau_summands_only).run();
293 0 : save_lps(spec, output_filename);
294 0 : }
295 :
296 0 : void lpsuntime(const std::string& input_filename,
297 : const std::string& output_filename,
298 : const bool add_invariants,
299 : const bool apply_fourier_motzkin,
300 : const data::rewriter::strategy rewrite_strategy
301 : )
302 : {
303 0 : stochastic_specification spec;
304 0 : load_lps(spec, input_filename);
305 0 : data::rewriter rewr(spec.data(),rewrite_strategy);
306 0 : untime_algorithm<stochastic_specification>(spec, add_invariants, apply_fourier_motzkin, rewr).run();
307 0 : save_lps(spec, output_filename);
308 0 : }
309 :
310 0 : void txt2lps(const std::string& input_filename,
311 : const std::string& output_filename
312 : )
313 : {
314 0 : lps::stochastic_specification spec;
315 0 : std::ifstream ifs(input_filename);
316 0 : if (!ifs.good())
317 : {
318 0 : throw mcrl2::runtime_error("Could not open file " + input_filename + ".");
319 : }
320 0 : parse_lps(ifs, spec);
321 0 : save_lps(spec, output_filename);
322 0 : }
323 :
324 : } // namespace lps
325 :
326 : } // namespace mcrl2
|
