mCRL2
Loading...
Searching...
No Matches
lts_fsm.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_FSM_H
20#define MCRL2_LTS_LTS_FSM_H
21
25
26namespace mcrl2
27{
28namespace lts
29{
30
37class state_label_fsm: public std::vector < std::size_t >
38{
39 public:
43 {}
44
47
50
53 explicit state_label_fsm(const std::vector < std::size_t >& v):
54 std::vector < std::size_t >(v)
55 {}
56
60 {
61 if ((*this).empty())
62 {
63 return l;
64 }
65 return (*this);
66 }
67};
68
71inline std::string pp(const state_label_fsm& label)
72{
73 std::string s;
74 for(const std::size_t& l: label)
75 {
76 s += std::to_string(l) + " ";
77 }
78 return s;
79}
80
81namespace detail
82{
84{
85 public:
88
89 protected:
90
93 std::vector < std::vector < std::string > > m_state_element_values;
94
98 std::vector < std::pair < std::string, std::string > > m_parameters;
99
100 public:
101
102 bool operator==(const lts_fsm_base& other) const
103 {
106 }
107
112 {
113 return lts_fsm;
114 }
115
117 void swap(lts_fsm_base& other)
118 {
120 m_parameters.swap(other.m_parameters);
121 }
122
127 void
129 {
131 m_parameters.clear();
132 }
133
140 const std::vector < std::string >& state_element_values(std::size_t idx) const
141 {
142 assert(idx<m_state_element_values.size());
143 return m_state_element_values[idx];
144 }
145
150 inline std::string state_label_to_string(const state_label_fsm& l) const
151 {
152 std::string s;
153 s = "(";
154 for (std::size_t i=0; i<l.size(); ++i)
155 {
156 s += state_element_value(i,l[i]);
157 if (i+1<l.size())
158 {
159 s += ",";
160 }
161 }
162 s += ")";
163 return s;
164 }
165
172 std::size_t add_state_element_value(std::size_t idx, const std::string& s)
173 {
174 assert(idx<m_state_element_values.size());
175 m_state_element_values[idx].push_back(s);
176 return m_state_element_values[idx].size();
177 }
178
187 std::string state_element_value(std::size_t parameter_index, std::size_t element_index) const
188 {
189 assert(parameter_index<m_state_element_values.size());
190 if (m_state_element_values[parameter_index].size()==0)
191 {
192 // The domain for this parameter has no string; return the string "i"
193 return std::to_string(element_index);
194 }
195 assert(element_index<m_state_element_values[parameter_index].size());
196 return m_state_element_values[parameter_index][element_index];
197 }
198
202 std::vector < std::pair < std::string, std::string > > process_parameters() const
203 {
204 return m_parameters;
205 }
206
211 std::pair < std::string, std::string > process_parameter(std::size_t i) const
212 {
213 assert(i<m_parameters.size());
214 return m_parameters[i];
215 }
216
220 {
221 m_parameters.clear();
223 }
224
229 void add_process_parameter(const std::string& name, const std::string& sort)
230 {
231 assert(m_parameters.size()==m_state_element_values.size());
232 m_parameters.push_back(std::pair<std::string,std::string>(name,sort));
233 m_state_element_values.push_back(std::vector < std::string >());
234 }
235
236
237};
238
239} // end namespace detail
240
247class lts_fsm_t : public lts< state_label_fsm, action_label_string, detail::lts_fsm_base >
248{
249 public:
251
256 void load(const std::string& filename);
257
262 void save(const std::string& filename) const;
263};
264
272 public probabilistic_lts< state_label_fsm,
273 action_label_string,
274 probabilistic_state< std::size_t, probabilistic_arbitrary_precision_fraction >,
275 detail::lts_fsm_base >
276{
277 public:
278
280
285 void load(const std::string& filename);
286
291 void save(const std::string& filename) const;
292};
293
294} // namespace lts
295} // namespace mcrl2
296
297#endif
This file contains a class that contains labelled transition systems in aut format.
void clear()
Clear the transitions system.
Definition lts_fsm.h:128
const std::vector< std::string > & state_element_values(std::size_t idx) const
Provides the vector of strings that correspond to the values of the number at position idx in a vecto...
Definition lts_fsm.h:140
std::size_t add_state_element_value(std::size_t idx, const std::string &s)
Adds a string to the state element values for the idx-th position in a state vector....
Definition lts_fsm.h:172
mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > probabilistic_state
Definition lts_fsm.h:86
bool operator==(const lts_fsm_base &other) const
Definition lts_fsm.h:102
void clear_process_parameters()
Clear the state parameters for this LTS.
Definition lts_fsm.h:219
std::vector< std::vector< std::string > > m_state_element_values
state_element_values contain the values that can occur at the i-th position of a state label
Definition lts_fsm.h:93
lts_type type() const
The lts_type of this labelled transition system. In this case lts_fsm.
Definition lts_fsm.h:111
std::string state_element_value(std::size_t parameter_index, std::size_t element_index) const
Returns the element_index'th element for the parameter with index parameter_index.
Definition lts_fsm.h:187
std::pair< std::string, std::string > process_parameter(std::size_t i) const
Returns the i-th parameter of the state vectors stored in this LTS.
Definition lts_fsm.h:211
std::vector< std::pair< std::string, std::string > > m_parameters
m_parameters contain the parameters corresponding to the consecutive elements of a state vector....
Definition lts_fsm.h:98
std::vector< std::pair< std::string, std::string > > process_parameters() const
Return the parameters of the state vectors stored in this LTS.
Definition lts_fsm.h:202
void add_process_parameter(const std::string &name, const std::string &sort)
Set the state parameters for this LTS.
Definition lts_fsm.h:229
mcrl2::lps::state_probability_pair< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > state_probability_pair
Definition lts_fsm.h:87
std::string state_label_to_string(const state_label_fsm &l) const
Pretty print a state value of this FSM.
Definition lts_fsm.h:150
void swap(lts_fsm_base &other)
Standard swap function.
Definition lts_fsm.h:117
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:248
lts< state_label_fsm, action_label_string, detail::lts_fsm_base > super
Definition lts_fsm.h:250
void load(const std::string &filename)
Save the labelled transition system to file.
void save(const std::string &filename) const
Save the labelled transition system to file.
A class that contains a labelled transition system.
Definition lts.h:83
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:276
probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state_t, detail::lts_fsm_base > super
Definition lts_fsm.h:279
void save(const std::string &filename) const
Save the labelled transition system to file.
void load(const std::string &filename)
Save the labelled transition system to file.
A class that contains a labelled transition system.
A class that contains a probabilistic state.
This class contains state labels for the fsm format.
Definition lts_fsm.h:38
state_label_fsm(const state_label_fsm &)=default
Copy constructor.
state_label_fsm & operator=(const state_label_fsm &)=default
Copy assignment.
state_label_fsm()
Default constructor. The label becomes an empty vector.
Definition lts_fsm.h:42
state_label_fsm(const std::vector< std::size_t > &v)
Default constructor. The label is set to the vector v.
Definition lts_fsm.h:53
state_label_fsm operator+(const state_label_fsm &l) const
An operator to concatenate two state labels. Fsm labels cannot be concatenated. Therefore,...
Definition lts_fsm.h:59
std::string pp(const abstraction &x)
Definition data.cpp:39
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
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. These consist of a 64 ...
The file containing the core class for transition systems.