Line data Source code
1 : // Author(s): Jan Friso Groote
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 : /** \file lts_lts.h
11 : *
12 : * \brief This file contains a class that contains labelled transition systems in lts (mcrl2) format.
13 : * \details A labelled transition system in lts/mcrl2 format is a transition system
14 : * with as state labels vectors of strings, and as transition labels strings.
15 : * \author Jan Friso Groote
16 : */
17 :
18 :
19 : #ifndef MCRL2_LTS_LTS_MCRL2_H
20 : #define MCRL2_LTS_LTS_MCRL2_H
21 :
22 : #include "mcrl2/lps/parse.h"
23 : #include "mcrl2/lps/print.h"
24 : #include "mcrl2/lps/state.h"
25 : #include "mcrl2/lps/probabilistic_data_expression.h"
26 : #include "mcrl2/lts/probabilistic_lts.h"
27 :
28 : namespace mcrl2
29 : {
30 : namespace lts
31 : {
32 :
33 : /** \brief This class contains state labels for an labelled transition system in .lts format.
34 : \details A state label in .lts format consists of lists of balanced tree of data expressions.
35 : These represent sets of state vectors. The reason for the sets is that states can
36 : be merged by operations on state spaces, and if so, the sets of labels can easily
37 : be joined.
38 : */
39 : class state_label_lts : public atermpp::term_list< lps::state >
40 : {
41 : public:
42 : typedef atermpp::term_list< lps::state > super;
43 :
44 : /** \brief Default constructor.
45 : */
46 1750 : state_label_lts()
47 1750 : {}
48 :
49 : /** \brief Copy constructor. */
50 1938 : state_label_lts(const state_label_lts& )=default;
51 :
52 : /** \brief Copy assignment. */
53 1296 : state_label_lts& operator=(const state_label_lts& )=default;
54 :
55 : /** \brief Construct a single state label out of the elements in a container.
56 : */
57 : template < class CONTAINER >
58 : explicit state_label_lts(const CONTAINER& l)
59 : {
60 : static_assert(std::is_same<typename CONTAINER::value_type, data::data_expression>::value,"Value type must be a data_expression");
61 : this->push_front(lps::state(l.begin(),l.size()));
62 : }
63 :
64 : /** \brief Construct a state label out of a balanced tree of data expressions, representing a state label.
65 : */
66 870 : explicit state_label_lts(const lps::state& l)
67 870 : {
68 870 : this->push_front(l);
69 870 : }
70 :
71 : /** \brief Construct a state label out of list of balanced trees of data expressions, representing a state label.
72 : */
73 : explicit state_label_lts(const super& l)
74 : : super(l)
75 : {
76 : }
77 :
78 : /** \brief An operator to concatenate two state labels.
79 : \details Is optimal whenever |l| is smaller than the left operand, i.e. |l| < |this|.
80 : */
81 0 : state_label_lts operator+(const state_label_lts& l) const
82 : {
83 : // The order of the state labels should not matter. For efficiency the elements of l are inserted in front of the aterm_list.
84 0 : state_label_lts result(*this);
85 :
86 0 : for (const lps::state& el : l)
87 : {
88 0 : result.push_front(el);
89 : }
90 :
91 0 : return result;
92 0 : }
93 : };
94 :
95 : /** \brief Pretty print a state value of this LTS.
96 : \details The label is printed as (t1,...,tn) if it consists of a single label.
97 : Otherwise the labels are printed with square brackets surrounding it.
98 : \param[in] label The state value to pretty print.
99 : \return The pretty-printed representation of value. */
100 :
101 0 : inline std::string pp(const state_label_lts& label)
102 : {
103 0 : std::string s;
104 0 : if (label.size()!=1)
105 : {
106 0 : s += "[";
107 : }
108 0 : bool first=true;
109 0 : for(const lps::state& l: label)
110 : {
111 0 : if (!first)
112 : {
113 0 : s += ", ";
114 : }
115 0 : first = false;
116 0 : s += "(";
117 0 : for (lps::state::iterator i=l.begin(); i!=l.end(); ++i)
118 : {
119 0 : if (i!=l.begin())
120 : {
121 0 : s += ",";
122 : }
123 0 : s += data::pp(*i);
124 : }
125 0 : s += ")";
126 : }
127 0 : if (label.size()!=1)
128 : {
129 0 : s += "]";
130 : }
131 0 : return s;
132 0 : }
133 :
134 : /** \brief A class containing the values for action labels for the .lts format.
135 : \details An action label is a multi_action. */
136 : class action_label_lts: public mcrl2::lps::multi_action
137 : {
138 : public:
139 :
140 : /** \brief Default constructor. */
141 1554 : action_label_lts()
142 1554 : {}
143 :
144 : /** \brief Copy constructor. */
145 2963 : action_label_lts(const action_label_lts& )=default;
146 :
147 : /** \brief Copy assignment. */
148 1535 : action_label_lts& operator=(const action_label_lts& )=default;
149 :
150 : /** \brief Constructor. */
151 1034 : explicit action_label_lts(const mcrl2::lps::multi_action& a)
152 1034 : : mcrl2::lps::multi_action(sort_multiactions(a))
153 : {
154 1034 : }
155 :
156 : /** \brief Hide the actions with labels in tau_actions.
157 : \return Returns whether the hidden action becomes empty, i.e. a tau or hidden action.
158 : */
159 : void hide_actions(const std::vector<std::string>& tau_actions)
160 : {
161 : process::action_vector new_multi_action;
162 : for (const process::action& a: this->actions())
163 : {
164 : if (std::find(tau_actions.begin(),tau_actions.end(),
165 : std::string(a.label().name()))==tau_actions.end()) // this action must not be hidden.
166 : {
167 : new_multi_action.push_back(a);
168 : }
169 : }
170 : *this= action_label_lts(lps::multi_action(process::action_list(new_multi_action.begin(), new_multi_action.end()),time()));
171 : }
172 :
173 : /* \brief The action label that represents the internal action.
174 : */
175 2486 : static const action_label_lts& tau_action()
176 : {
177 2486 : static action_label_lts tau_action=action_label_lts();
178 2486 : return tau_action;
179 : }
180 :
181 : protected:
182 : /// A function to sort a multi action to guarantee that multi-actions are compared properly.
183 1034 : static mcrl2::lps::multi_action sort_multiactions(const mcrl2::lps::multi_action& a)
184 : {
185 1034 : if (a.actions().size()<=1)
186 : {
187 1030 : return a;
188 : }
189 4 : std::multiset<process::action> sorted_actions(a.actions().begin(), a.actions().end());
190 8 : return mcrl2::lps::multi_action(process::action_list(sorted_actions.begin(),sorted_actions.end()),a.time());
191 4 : }
192 : };
193 :
194 : /** \brief Print the action label to string. */
195 508 : inline std::string pp(const action_label_lts& l)
196 : {
197 1016 : return lps::pp(mcrl2::lps::multi_action(l));
198 : }
199 :
200 : /** \brief Parse a string into an action label.
201 : \details The string is typechecked against the data specification and
202 : list of declared actions. If parsing or type checking fails, an
203 : mcrl2::runtime_error is thrown.
204 : \param[in] multi_action_string The string to be parsed.
205 : \param[in] data_spec The data specification used for parsing.
206 : \param[in] act_decls Action declarations.
207 : \return The parsed and type checked multi action. */
208 12 : inline action_label_lts parse_lts_action(
209 : const std::string& multi_action_string,
210 : const data::data_specification& data_spec,
211 : lps::multi_action_type_checker& typechecker)
212 : {
213 12 : std::string l(multi_action_string);
214 24 : lps::multi_action al;
215 : // Find an @ symbol in the action, in which case it is timed.
216 12 : size_t position_of_at=l.find_first_of('@');
217 12 : std::string time_expression_string;
218 12 : if (position_of_at!=std::string::npos)
219 : {
220 : // The at symbol is found. It is a timed action.
221 0 : time_expression_string=l.substr(position_of_at+1,l.size());
222 0 : l=l.substr(0,position_of_at-1);
223 : }
224 : try
225 : {
226 12 : al=lps::parse_multi_action(l, typechecker, data_spec);
227 : }
228 0 : catch (mcrl2::runtime_error& e)
229 : {
230 0 : throw mcrl2::runtime_error("Parse error in action label " + multi_action_string + ".\n" + e.what());
231 0 : }
232 :
233 12 : if (time_expression_string.size()>0)
234 : {
235 : try
236 : {
237 0 : data::data_expression time=parse_data_expression(time_expression_string,data::variable_list(),data_spec);
238 : // Translate the sort of time to a real.
239 0 : if (time.sort()==data::sort_pos::pos())
240 : {
241 0 : time = data::sort_nat::cnat(time);
242 : }
243 0 : if (time.sort()==data::sort_nat::nat())
244 : {
245 0 : time = data::sort_int::cint(time);
246 : }
247 0 : if (time.sort()==data::sort_int::int_())
248 : {
249 0 : time = data::sort_real::creal(time, data::sort_pos::c1());
250 : }
251 0 : if (time.sort()!=data::sort_real::real_())
252 : {
253 0 : throw mcrl2::runtime_error("The time is not of sort Pos, Nat, Int or Real\n");
254 : }
255 0 : return action_label_lts(lps::multi_action(al.actions(),time));
256 0 : }
257 0 : catch (mcrl2::runtime_error& e)
258 : {
259 0 : throw mcrl2::runtime_error("Parse error in the time expression " + multi_action_string + ".\n" + e.what());
260 0 : }
261 : }
262 12 : return action_label_lts(al);
263 12 : }
264 :
265 : namespace detail
266 : {
267 :
268 : /** \brief a base class for lts_lts_t and probabilistic_lts_t.
269 : */
270 : class lts_lts_base
271 : {
272 : protected:
273 : data::data_specification m_data_spec;
274 : data::variable_list m_parameters;
275 : process::action_label_list m_action_decls;
276 :
277 : public:
278 : /// \brief Default constructor
279 188 : lts_lts_base()
280 188 : {}
281 :
282 : /// \brief Standard equality function;
283 : bool operator==(const lts_lts_base& other) const
284 : {
285 : return m_data_spec==other.m_data_spec &&
286 : m_parameters==other.m_parameters &&
287 : m_action_decls==other.m_action_decls;
288 : }
289 :
290 : void swap(lts_lts_base& l)
291 : {
292 : const data::data_specification auxd=m_data_spec;
293 : m_data_spec=l.m_data_spec;
294 : l.m_data_spec=auxd;
295 : m_parameters.swap(l.m_parameters);
296 : m_action_decls.swap(l.m_action_decls);
297 : }
298 :
299 : /** \brief Yields the type of this lts, in this case lts_lts. */
300 58 : static lts_type type()
301 : {
302 58 : return lts_lts;
303 : }
304 :
305 : /** \brief Returns the mCRL2 data specification of this LTS.
306 : */
307 76 : const data::data_specification& data() const
308 : {
309 76 : return m_data_spec;
310 : }
311 :
312 : /** \brief Return action label declarations stored in this LTS.
313 : */
314 74 : const process::action_label_list& action_label_declarations() const
315 : {
316 74 : return m_action_decls;
317 : }
318 :
319 : /** \brief Set the action label information for this LTS.
320 : * \param[in] decls The action labels to be set in this lts.
321 : */
322 186 : void set_action_label_declarations(const process::action_label_list& decls)
323 : {
324 186 : m_action_decls=decls;
325 186 : }
326 :
327 : /** \brief Set the mCRL2 data specification of this LTS.
328 : * \param[in] spec The mCRL2 data specification for this LTS.
329 : */
330 186 : void set_data(const data::data_specification& spec)
331 : {
332 186 : m_data_spec=spec;
333 186 : }
334 :
335 : /** \brief Return the process parameters stored in this LTS.
336 : */
337 179 : const data::variable_list& process_parameters() const
338 : {
339 179 : return m_parameters;
340 : }
341 :
342 : /** \brief Returns the i-th parameter of the state vectors stored in this LTS.
343 : * \return The state parameters stored in this LTS.
344 : */
345 : const data::variable& process_parameter(std::size_t i) const
346 : {
347 : assert(i<m_parameters.size());
348 : data::variable_list::const_iterator j=m_parameters.begin();
349 : for(std::size_t c=0; c!=i; ++j, ++c)
350 : {}
351 : return *j;
352 : }
353 :
354 :
355 : /** \brief Set the state parameters for this LTS.
356 : * \param[in] params The state parameters for this lts.
357 : */
358 183 : void set_process_parameters(const data::variable_list& params)
359 : {
360 183 : m_parameters=params;
361 183 : }
362 :
363 : };
364 :
365 : } // namespace detail
366 :
367 :
368 : /** \brief This class contains labelled transition systems in .lts format.
369 : \details In this .lts format, an action label is a multi action, and a
370 : state label is an expression of the form STATE(t1,...,tn) where
371 : ti are data expressions.
372 : */
373 : class lts_lts_t : public lts< state_label_lts, action_label_lts, detail::lts_lts_base >
374 : {
375 : public:
376 : /** \brief Creates an object containing no information. */
377 176 : lts_lts_t() {}
378 :
379 : /** \brief Load the labelled transition system from file.
380 : * \details If the filename is empty, the result is read from stdout.
381 : * \param[in] filename Name of the file to which this lts is written.
382 : */
383 : void load(const std::string& filename);
384 :
385 : /** \brief Save the labelled transition system to file.
386 : * \details If the filename is empty, the result is read from stdin.
387 : * \param[in] filename Name of the file from which this lts is read.
388 : */
389 : void save(const std::string& filename) const;
390 : };
391 :
392 : /** \brief This class contains probabilistic labelled transition systems in .lts format.
393 : \details In this .lts format, an action label is a multi action, and a
394 : state label is an expression of the form STATE(t1,...,tn) where
395 : ti are data expressions.
396 : */
397 : class probabilistic_lts_lts_t :
398 : public probabilistic_lts< state_label_lts,
399 : action_label_lts,
400 : probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
401 : detail::lts_lts_base >
402 : {
403 : public:
404 : /** \brief Creates an object containing no information. */
405 12 : probabilistic_lts_lts_t() {}
406 :
407 : /** \brief Load the labelled transition system from file.
408 : * \details If the filename is empty, the result is read from stdout.
409 : * \param[in] filename Name of the file to which this lts is written.
410 : */
411 : void load(const std::string& filename);
412 :
413 : /** \brief Save the labelled transition system to file.
414 : * \details If the filename is empty, the result is read from stdin.
415 : * \param[in] filename Name of the file from which this lts is read.
416 : */
417 : void save(const std::string& filename) const;
418 : };
419 : } // namespace lts
420 : } // namespace mcrl2
421 :
422 : namespace std
423 : {
424 :
425 : /// \brief specialization of the standard std::hash function for an action_label_string.
426 : template<>
427 : struct hash< mcrl2::lts::action_label_lts >
428 : {
429 1271 : std::size_t operator()(const mcrl2::lts::action_label_lts& as) const
430 : {
431 : hash<mcrl2::lps::multi_action> hasher;
432 2542 : return hasher(as);
433 : }
434 : };
435 :
436 : } // namespace std
437 :
438 :
439 : #endif
|
