mCRL2
Loading...
Searching...
No Matches
lts_lts.h
Go to the documentation of this file.
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
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"
27
28namespace mcrl2
29{
30namespace lts
31{
32
39class state_label_lts : public atermpp::term_list< lps::state >
40{
41 public:
43
47 {}
48
51
54
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
66 explicit state_label_lts(const lps::state& l)
67 {
68 this->push_front(l);
69 }
70
73 explicit state_label_lts(const super& l)
74 : super(l)
75 {
76 }
77
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 state_label_lts result(*this);
85
86 for (const lps::state& el : l)
87 {
88 result.push_front(el);
89 }
90
91 return result;
92 }
93};
94
101inline std::string pp(const state_label_lts& label)
102{
103 std::string s;
104 if (label.size()!=1)
105 {
106 s += "[";
107 }
108 bool first=true;
109 for(const lps::state& l: label)
110 {
111 if (!first)
112 {
113 s += ", ";
114 }
115 first = false;
116 s += "(";
117 for (lps::state::iterator i=l.begin(); i!=l.end(); ++i)
118 {
119 if (i!=l.begin())
120 {
121 s += ",";
122 }
123 s += data::pp(*i);
124 }
125 s += ")";
126 }
127 if (label.size()!=1)
128 {
129 s += "]";
130 }
131 return s;
132}
133
137{
138 public:
139
142 {}
143
146
149
153 {
154 }
155
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 */
176 {
178 return tau_action;
179 }
180
181 protected:
184 {
185 if (a.actions().size()<=1)
186 {
187 return a;
188 }
189 std::multiset<process::action> sorted_actions(a.actions().begin(), a.actions().end());
190 return mcrl2::lps::multi_action(process::action_list(sorted_actions.begin(),sorted_actions.end()),a.time());
191 }
192};
193
195inline std::string pp(const action_label_lts& l)
196{
198}
199
209 const std::string& multi_action_string,
210 const data::data_specification& data_spec,
212{
213 std::string l(multi_action_string);
215 // Find an @ symbol in the action, in which case it is timed.
216 size_t position_of_at=l.find_first_of('@');
217 std::string time_expression_string;
218 if (position_of_at!=std::string::npos)
219 {
220 // The at symbol is found. It is a timed action.
221 time_expression_string=l.substr(position_of_at+1,l.size());
222 l=l.substr(0,position_of_at-1);
223 }
224 try
225 {
226 al=lps::parse_multi_action(l, typechecker, data_spec);
227 }
228 catch (mcrl2::runtime_error& e)
229 {
230 throw mcrl2::runtime_error("Parse error in action label " + multi_action_string + ".\n" + e.what());
231 }
232
233 if (time_expression_string.size()>0)
234 {
235 try
236 {
237 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 if (time.sort()==data::sort_pos::pos())
240 {
241 time = data::sort_nat::cnat(time);
242 }
243 if (time.sort()==data::sort_nat::nat())
244 {
245 time = data::sort_int::cint(time);
246 }
247 if (time.sort()==data::sort_int::int_())
248 {
250 }
251 if (time.sort()!=data::sort_real::real_())
252 {
253 throw mcrl2::runtime_error("The time is not of sort Pos, Nat, Int or Real\n");
254 }
255 return action_label_lts(lps::multi_action(al.actions(),time));
256 }
257 catch (mcrl2::runtime_error& e)
258 {
259 throw mcrl2::runtime_error("Parse error in the time expression " + multi_action_string + ".\n" + e.what());
260 }
261 }
262 return action_label_lts(al);
263}
264
265namespace detail
266{
267
271{
272 protected:
276
277 public:
280 {}
281
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 &&
288 }
289
291 {
294 l.m_data_spec=auxd;
297 }
298
300 static lts_type type()
301 {
302 return lts_lts;
303 }
304
308 {
309 return m_data_spec;
310 }
311
315 {
316 return m_action_decls;
317 }
318
323 {
324 m_action_decls=decls;
325 }
326
331 {
332 m_data_spec=spec;
333 }
334
338 {
339 return m_parameters;
340 }
341
345 const data::variable& process_parameter(std::size_t i) const
346 {
347 assert(i<m_parameters.size());
349 for(std::size_t c=0; c!=i; ++j, ++c)
350 {}
351 return *j;
352 }
353
354
359 {
360 m_parameters=params;
361 }
362
363};
364
365} // namespace detail
366
367
373class lts_lts_t : public lts< state_label_lts, action_label_lts, detail::lts_lts_base >
374{
375 public:
378
383 void load(const std::string& filename);
384
389 void save(const std::string& filename) const;
390};
391
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:
406
411 void load(const std::string& filename);
412
417 void save(const std::string& filename) const;
418};
419} // namespace lts
420} // namespace mcrl2
421
422namespace std
423{
424
426template<>
427struct hash< mcrl2::lts::action_label_lts >
428{
429 std::size_t operator()(const mcrl2::lts::action_label_lts& as) const
430 {
431 hash<mcrl2::lps::multi_action> hasher;
432 return hasher(as);
433 }
434};
435
436} // namespace std
437
438
439#endif
Read-only balanced binary tree of terms.
Iterator for term_list.
A list of aterm objects.
Definition aterm_list.h:23
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:255
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:281
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:274
void push_front(const lps::state &el)
Inserts a new element at the beginning of the current list.
void swap(unprotected_aterm &t) noexcept
Swaps this term with its argument.
Definition aterm.h:156
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
\brief A data variable
Definition variable.h:28
\brief A timed multi-action
const process::action_list & actions() const
const data::data_expression & time() const
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
action_label_lts & operator=(const action_label_lts &)=default
Copy assignment.
static mcrl2::lps::multi_action sort_multiactions(const mcrl2::lps::multi_action &a)
A function to sort a multi action to guarantee that multi-actions are compared properly.
Definition lts_lts.h:183
void hide_actions(const std::vector< std::string > &tau_actions)
Hide the actions with labels in tau_actions.
Definition lts_lts.h:159
action_label_lts(const action_label_lts &)=default
Copy constructor.
static const action_label_lts & tau_action()
Definition lts_lts.h:175
action_label_lts()
Default constructor.
Definition lts_lts.h:141
action_label_lts(const mcrl2::lps::multi_action &a)
Constructor.
Definition lts_lts.h:151
a base class for lts_lts_t and probabilistic_lts_t.
Definition lts_lts.h:271
static lts_type type()
Yields the type of this lts, in this case lts_lts.
Definition lts_lts.h:300
void set_process_parameters(const data::variable_list &params)
Set the state parameters for this LTS.
Definition lts_lts.h:358
const data::data_specification & data() const
Returns the mCRL2 data specification of this LTS.
Definition lts_lts.h:307
bool operator==(const lts_lts_base &other) const
Standard equality function;.
Definition lts_lts.h:283
process::action_label_list m_action_decls
Definition lts_lts.h:275
void swap(lts_lts_base &l)
Definition lts_lts.h:290
void set_action_label_declarations(const process::action_label_list &decls)
Set the action label information for this LTS.
Definition lts_lts.h:322
const data::variable & process_parameter(std::size_t i) const
Returns the i-th parameter of the state vectors stored in this LTS.
Definition lts_lts.h:345
data::data_specification m_data_spec
Definition lts_lts.h:273
const data::variable_list & process_parameters() const
Return the process parameters stored in this LTS.
Definition lts_lts.h:337
void set_data(const data::data_specification &spec)
Set the mCRL2 data specification of this LTS.
Definition lts_lts.h:330
lts_lts_base()
Default constructor.
Definition lts_lts.h:279
const process::action_label_list & action_label_declarations() const
Return action label declarations stored in this LTS.
Definition lts_lts.h:314
data::variable_list m_parameters
Definition lts_lts.h:274
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:374
lts_lts_t()
Creates an object containing no information.
Definition lts_lts.h:377
void save(const std::string &filename) const
Save the labelled transition system to file.
void load(const std::string &filename)
Load the labelled transition system from file.
A class that contains a labelled transition system.
Definition lts.h:83
This class contains probabilistic labelled transition systems in .lts format.
Definition lts_lts.h:402
void load(const std::string &filename)
Load the labelled transition system from file.
probabilistic_lts_lts_t()
Creates an object containing no information.
Definition lts_lts.h:405
void save(const std::string &filename) const
Save the labelled transition system to file.
A class that contains a labelled transition system.
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:40
state_label_lts()
Default constructor.
Definition lts_lts.h:46
state_label_lts(const state_label_lts &)=default
Copy constructor.
state_label_lts operator+(const state_label_lts &l) const
An operator to concatenate two state labels.
Definition lts_lts.h:81
state_label_lts(const super &l)
Construct a state label out of list of balanced trees of data expressions, representing a state label...
Definition lts_lts.h:73
atermpp::term_list< lps::state > super
Definition lts_lts.h:42
state_label_lts(const lps::state &l)
Construct a state label out of a balanced tree of data expressions, representing a state label.
Definition lts_lts.h:66
state_label_lts & operator=(const state_label_lts &)=default
Copy assignment.
state_label_lts(const CONTAINER &l)
Construct a single state label out of the elements in a container.
Definition lts_lts.h:58
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
add your file description here.
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int.h:80
const basic_sort & int_()
Constructor for sort expression Int.
Definition int.h:47
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat.h:140
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat.h:46
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos.h:78
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos.h:45
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real.h:107
const basic_sort & real_()
Constructor for sort expression Real.
Definition real.h:48
data_expression parse_data_expression(std::istream &in, const VariableContainer &variables, const data_specification &dataspec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
Parses and type checks a data expression.
Definition parse.h:276
std::string pp(const abstraction &x)
Definition data.cpp:39
std::string pp(const action_summand &x)
Definition lps.cpp:26
multi_action parse_multi_action(std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Parses a multi_action from an input stream.
Definition parse.h:42
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
action_label_lts parse_lts_action(const std::string &multi_action_string, const data::data_specification &data_spec, lps::multi_action_type_checker &typechecker)
Parse a string into an action label.
Definition lts_lts.h:208
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::vector< action > action_vector
\brief vector of actions
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
This file contains a class that contains labels for probabilistic transitions as a mCRL2 data express...
The file containing the core class for transition systems.
The class summand.
std::size_t operator()(const mcrl2::lts::action_label_lts &as) const
Definition lts_lts.h:429
#define hash(l, r, m)
Definition tree_set.cpp:23