Line data Source code
1 : // Author(s): anonymous, Thomas Neele
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 :
10 : #include "mcrl2/atermpp/aterm_io_binary.h"
11 : #include "mcrl2/core/load_aterm.h"
12 : #include "mcrl2/data/data_io.h"
13 : #include "mcrl2/pbes/algorithms.h"
14 : #include "mcrl2/pbes/detail/pbes_io.h"
15 : #include "mcrl2/pbes/io.h"
16 : #include "mcrl2/pbes/join.h"
17 : #include "mcrl2/pbes/parse.h"
18 : #include "mcrl2/pbes/normal_forms.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace pbes_system
24 : {
25 :
26 29 : const std::vector<utilities::file_format>& pbes_file_formats()
27 : {
28 29 : static std::vector<utilities::file_format> result;
29 29 : if (result.empty())
30 : {
31 2 : result.push_back(utilities::file_format("pbes", "PBES in internal format", false));
32 2 : result.back().add_extension("pbes");
33 2 : result.push_back(utilities::file_format("text", "PBES in textual (mCRL2) format", true));
34 2 : result.back().add_extension("txt");
35 2 : result.push_back(utilities::file_format("bes", "BES in internal format", false));
36 2 : result.back().add_extension("bes");
37 2 : result.push_back(utilities::file_format("pgsolver", "BES in PGSolver format", true));
38 2 : result.back().add_extension("gm");
39 2 : result.back().add_extension("pg");
40 : }
41 29 : return result;
42 : }
43 :
44 : /// \brief Save a PBES in the format specified.
45 : /// \param pbes The PBES to be stored
46 : /// \param stream The stream to which the output is saved.
47 : /// \param format Determines the format in which the result is written. If unspecified, or
48 : /// pbes_file_unknown is specified, then a default format is chosen.
49 4 : void save_pbes(const pbes& pbes,
50 : std::ostream& stream,
51 : utilities::file_format format)
52 : {
53 4 : if (format == utilities::file_format())
54 : {
55 1 : format = pbes_format_internal();
56 : }
57 4 : mCRL2log(log::verbose) << "Saving result in " << format.shortname() << " format..." << std::endl;
58 4 : if (format == pbes_format_internal() || (format == pbes_format_internal_bes() && pbes_system::algorithms::is_bes(pbes)))
59 : {
60 3 : atermpp::binary_aterm_ostream(stream) << pbes;
61 : }
62 1 : else if (format == pbes_format_pgsolver() && pbes_system::algorithms::is_bes(pbes))
63 : {
64 0 : save_bes_pgsolver(pbes, stream);
65 : }
66 1 : else if (format == pbes_format_text())
67 : {
68 1 : stream << pp(pbes);
69 : }
70 : else
71 : {
72 0 : throw mcrl2::runtime_error("Trying to save PBES in non-PBES format (" + format.shortname() + ")");
73 : }
74 4 : }
75 :
76 : /// \brief Load a PBES from file.
77 : /// \param pbes The PBES to which the result is loaded.
78 : /// \param stream The stream from which to load the PBES.
79 : /// \param format The format that should be assumed for the file in infilename. If unspecified, or
80 : /// pbes_file_unknown is specified, then a default format is chosen.
81 : /// \param source The source from which the stream originates. Used for error messages.
82 6 : void load_pbes(pbes& pbes, std::istream& stream, utilities::file_format format, const std::string& /*source*/)
83 : {
84 6 : if (format == utilities::file_format())
85 : {
86 2 : format = pbes_format_internal();
87 : }
88 6 : mCRL2log(log::verbose) << "Loading PBES in " << format.shortname() << " format..." << std::endl;
89 6 : if (format == pbes_format_internal() || format == pbes_format_internal_bes())
90 : {
91 5 : atermpp::binary_aterm_istream(stream) >> pbes;
92 : }
93 : else
94 1 : if (format == pbes_format_text())
95 : {
96 1 : stream >> pbes;
97 : }
98 : else
99 : {
100 0 : throw mcrl2::runtime_error("Trying to load PBES from non-PBES format (" + format.shortname() + ")");
101 : }
102 5 : }
103 :
104 : /// \brief save_pbes Saves a PBES to a file.
105 : /// \param pbes The PBES to save.
106 : /// \param filename The file to save the PBES in.
107 : /// \param format The format in which to save the PBES.
108 : /// \param welltypedness_check If set to false, skips checking whether pbes is well typed before
109 : /// saving it to file.
110 : ///
111 : /// The format of the file in infilename is guessed if format is not given or if it is equal to
112 : /// utilities::file_format().
113 4 : void save_pbes(const pbes& pbes, const std::string& filename,
114 : utilities::file_format format,
115 : bool welltypedness_check)
116 : {
117 4 : if (welltypedness_check)
118 : {
119 4 : assert(pbes.is_well_typed());
120 : }
121 4 : if (format == utilities::file_format())
122 : {
123 2 : format = guess_format(filename);
124 : }
125 :
126 4 : if (filename.empty())
127 : {
128 0 : save_pbes(pbes, std::cout, format);
129 : }
130 : else
131 : {
132 4 : std::ofstream filestream(filename,(format.text_format()?std::ios_base::out: std::ios_base::binary));
133 4 : if (!filestream.good())
134 : {
135 0 : throw mcrl2::runtime_error("Could not open file " + filename);
136 : }
137 4 : save_pbes(pbes, filestream, format);
138 4 : }
139 4 : }
140 :
141 : /// \brief Load pbes from file.
142 : /// \param pbes The pbes to which the result is loaded.
143 : /// \param filename The file from which to load the PBES.
144 : /// \param format The format in which the PBES is stored in the file.
145 : ///
146 : /// The format of the file in infilename is guessed if format is not given or if it is equal to
147 : /// utilities::file_format().
148 7 : void load_pbes(pbes& pbes,
149 : const std::string& filename,
150 : utilities::file_format format)
151 : {
152 7 : if (format == utilities::file_format())
153 : {
154 5 : format = guess_format(filename);
155 : }
156 7 : if (filename.empty())
157 : {
158 0 : load_pbes(pbes, std::cin, format);
159 : }
160 : else
161 : {
162 7 : std::ifstream filestream(filename,(format.text_format()?std::ios_base::in: std::ios_base::binary));
163 7 : if (!filestream.good())
164 : {
165 1 : throw mcrl2::runtime_error("Could not open file " + filename);
166 : }
167 8 : load_pbes(pbes, filestream, format, core::detail::file_source(filename));
168 7 : }
169 5 : }
170 :
171 : // transforms DataVarId to DataVarIdNoIndex
172 : // transforms OpId to OpIdNoIndex
173 : // transforms PropVarInst to PropVarInstNoIndex
174 352 : static atermpp::aterm_appl remove_index_impl(const atermpp::aterm_appl& x)
175 : {
176 352 : if (x.function() == core::detail::function_symbol_OpId())
177 : {
178 54 : return atermpp::aterm_appl(core::detail::function_symbol_OpIdNoIndex(), x.begin(), --x.end());
179 : }
180 325 : return x;
181 : }
182 :
183 : // transforms DataVarIdNoIndex to DataVarId (obsolete)
184 : // transforms OpIdNoIndex to OpId
185 : // transforms PropVarInstNoIndex to PropVarInst (obsolete)
186 306 : static atermpp::aterm_appl add_index_impl(const atermpp::aterm_appl& x)
187 : {
188 306 : if (x.function() == core::detail::function_symbol_DataVarIdNoIndex())
189 : {
190 0 : const data::variable& y = reinterpret_cast<const data::variable&>(x);
191 0 : return data::variable(y.name(), y.sort());
192 : }
193 306 : else if (x.function() == core::detail::function_symbol_OpIdNoIndex()) // This should be removed in due time. Say 2025.
194 : {
195 24 : const data::function_symbol& y = reinterpret_cast<const data::function_symbol&>(x);
196 24 : return data::function_symbol(y.name(), y.sort());
197 : }
198 282 : else if (x.function() == core::detail::function_symbol_PropVarInstNoIndex()) // This should be removed in due time. Say 2025.
199 : {
200 0 : const pbes_system::propositional_variable_instantiation& y = reinterpret_cast<const pbes_system::propositional_variable_instantiation&>(x);
201 0 : return pbes_system::propositional_variable_instantiation(y.name(), y.parameters());
202 : }
203 282 : return x;
204 : }
205 :
206 6 : inline atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const pbes_equation& equation)
207 : {
208 6 : stream << equation.symbol();
209 6 : stream << equation.variable();
210 6 : stream << equation.formula();
211 6 : return stream;
212 : }
213 :
214 9 : inline atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, pbes_equation& equation)
215 : {
216 9 : fixpoint_symbol symbol;
217 9 : propositional_variable var;
218 9 : pbes_expression expression;
219 :
220 9 : stream >> symbol;
221 9 : stream >> var;
222 9 : stream >> expression;
223 :
224 9 : equation = pbes_equation(symbol, var, expression);
225 :
226 9 : return stream;
227 9 : }
228 :
229 7 : atermpp::aterm pbes_marker()
230 : {
231 7 : return atermpp::aterm_appl(atermpp::function_symbol("parameterised_boolean_equation_system", 0));
232 : }
233 :
234 3 : atermpp::aterm_ostream& operator<<(atermpp::aterm_ostream& stream, const pbes& pbes)
235 : {
236 3 : atermpp::aterm_stream_state state(stream);
237 3 : stream << remove_index_impl;
238 :
239 3 : stream << pbes_marker();
240 3 : stream << pbes.data();
241 3 : stream << pbes.global_variables();
242 3 : stream << pbes.equations();
243 3 : stream << pbes.initial_state();
244 3 : return stream;
245 3 : }
246 :
247 4 : atermpp::aterm_istream& operator>>(atermpp::aterm_istream& stream, pbes& pbes)
248 : {
249 4 : atermpp::aterm_stream_state state(stream);
250 4 : stream >> add_index_impl;
251 :
252 : try
253 : {
254 4 : atermpp::aterm marker;
255 4 : stream >> marker;
256 :
257 4 : if (marker != pbes_marker())
258 : {
259 0 : throw mcrl2::runtime_error("Stream does not contain a parameterised boolean equation system (PBES).");
260 : }
261 :
262 4 : data::data_specification data;
263 4 : std::set<data::variable> global_variables;
264 4 : std::vector<pbes_equation> equations;
265 4 : propositional_variable_instantiation initial_state;
266 :
267 4 : stream >> data;
268 4 : stream >> global_variables;
269 4 : stream >> equations;
270 4 : stream >> initial_state;
271 :
272 4 : pbes = pbes_system::pbes(data, global_variables, equations, initial_state);
273 :
274 : // Add all the sorts that are used in the specification
275 : // to the data specification. This is important for those
276 : // sorts that are built in, because these are not explicitly
277 : // declared.
278 4 : complete_data_specification(pbes);
279 4 : }
280 0 : catch (std::exception& ex)
281 : {
282 0 : mCRL2log(log::error) << ex.what() << "\n";
283 0 : throw mcrl2::runtime_error(std::string("Error reading parameterised boolean equation system (PBES)."));
284 0 : }
285 :
286 4 : return stream;
287 4 : }
288 :
289 : namespace detail
290 : {
291 :
292 0 : pbes load_pbes(const std::string& filename)
293 : {
294 0 : pbes result;
295 0 : if (filename.empty())
296 : {
297 0 : atermpp::binary_aterm_istream(std::cin) >> result;
298 : }
299 : else
300 : {
301 0 : std::ifstream from(filename, std::ifstream::in | std::ifstream::binary);
302 0 : atermpp::binary_aterm_istream(from) >> result;
303 0 : }
304 0 : return result;
305 0 : }
306 :
307 0 : void save_pbes(const pbes& pbesspec, const std::string& filename)
308 : {
309 0 : if (filename.empty())
310 : {
311 0 : atermpp::binary_aterm_ostream(std::cout) << pbesspec;
312 : }
313 : else
314 : {
315 0 : std::ofstream to(filename, std::ofstream::out | std::ofstream::binary);
316 0 : if (!to.good())
317 : {
318 0 : throw mcrl2::runtime_error("Could not write to filename " + filename);
319 : }
320 0 : atermpp::binary_aterm_ostream(to) << pbesspec;
321 0 : }
322 0 : }
323 :
324 : } // namespace detail
325 :
326 : /// \brief Conversion to atermappl.
327 : /// \return The PBES converted to aterm format.
328 195 : atermpp::aterm_appl pbes_to_aterm(const pbes& p)
329 : {
330 : atermpp::aterm_appl global_variables = atermpp::aterm_appl(core::detail::function_symbol_GlobVarSpec(),
331 195 : data::variable_list(p.global_variables().begin(),
332 390 : p.global_variables().end()));
333 :
334 195 : atermpp::aterm_list eqn_list;
335 195 : const std::vector<pbes_equation>& eqn = p.equations();
336 784 : for (auto i = eqn.rbegin(); i != eqn.rend(); ++i)
337 : {
338 589 : atermpp::aterm a = pbes_equation_to_aterm(*i);
339 589 : eqn_list.push_front(a);
340 589 : }
341 195 : atermpp::aterm_appl equations = atermpp::aterm_appl(core::detail::function_symbol_PBEqnSpec(), eqn_list);
342 195 : atermpp::aterm_appl initial_state = atermpp::aterm_appl(core::detail::function_symbol_PBInit(), p.initial_state());
343 195 : atermpp::aterm_appl result;
344 :
345 390 : result = atermpp::aterm_appl(core::detail::function_symbol_PBES(),
346 390 : data::detail::data_specification_to_aterm(p.data()),
347 : global_variables,
348 : equations,
349 195 : initial_state);
350 :
351 390 : return result;
352 195 : }
353 :
354 : } // namespace pbes_system
355 :
356 : } // namespace mcrl2
|