mCRL2
Loading...
Searching...
No Matches
fsm_builder.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_LTS_DETAIL_FSM_BUILDER_H
13#define MCRL2_LTS_DETAIL_FSM_BUILDER_H
14
15#include <map>
16#include "mcrl2/lts/lts_fsm.h"
18
19namespace mcrl2::lts::detail {
20
21// Read a numeric value before a symbol c1 or c2, and remove it from s, including the symbol.
22inline std::string split_string_until(std::string& s, const std::string& c1, const std::string& c2="")
23{
24 std::size_t n=s.find(c1);
25 if (!c2.empty())
26 {
27 n=std::min(n,s.find(c2));
28 }
29 if (n==std::string::npos)
30 {
31 if (c2.empty())
32 {
33 throw mcrl2::runtime_error("Expect '" + c1 + "' in distribution " + s + ".");
34 }
35 else
36 {
37 throw mcrl2::runtime_error("Expect either '" + c1 + "' or '" + c2 + " in distribution " + s + ".");
38 }
39 }
40 std::string result=s.substr(0,n);
41 s=s.substr(n+1);
42 return result;
43}
44
45inline lts_fsm_base::probabilistic_state parse_distribution(const std::string& distribution)
46{
47 if (distribution.find('[')==std::string::npos) // So the distribution must consist of a state index.
48 {
49 std::size_t state_number=utilities::parse_natural_number(distribution);
50 if (state_number==0)
51 {
52 throw mcrl2::runtime_error("Transition has a zero as target state number.");
53 }
54 return lts_fsm_base::probabilistic_state(state_number-1);
55 }
56
57 // Otherwise the distribution has the shape [state1 enumerator1/denominator1 ... staten enumeratorn/denominatorn]
58 std::vector<lts_fsm_base::state_probability_pair> result;
59 std::string s = utilities::trim_copy(distribution);
60 if (s.substr(0,1) != "[")
61 {
62 throw mcrl2::runtime_error("Distribution does not start with ']': " + distribution + ".");
63 }
64 s = s.substr(1); // Remove initial "[";
65 for(; s.size() > 1; s = utilities::trim_copy(s))
66 {
67 std::size_t state_number = utilities::parse_natural_number(split_string_until(s," "));
68 if (state_number == 0)
69 {
70 throw mcrl2::runtime_error("Transition has a zero as target state number.");
71 }
72 std::string enumerator = split_string_until(s,"/");
73 std::string denominator = split_string_until(s," ","]");
74 result.emplace_back(state_number - 1, utilities::probabilistic_arbitrary_precision_fraction(enumerator,denominator));
75 }
76 return lts_fsm_base::probabilistic_state(result.begin(), result.end());
77}
78
80{
81 protected:
82 std::string m_name;
83 std::size_t m_cardinality;
84 std::string m_sort;
85 std::vector<std::string> m_values;
86
87 public:
88 fsm_parameter(const std::string& name, const std::string& cardinality, const std::string& sort, const std::vector<std::string>& values)
89 : m_name(name),
91 m_sort(sort),
93 {}
94
95 const std::string& name() const
96 {
97 return m_name;
98 }
99
100 std::string& name()
101 {
102 return m_name;
103 }
104
105 const std::string& sort() const
106 {
107 return m_sort;
108 }
109
110 std::string& sort()
111 {
112 return m_sort;
113 }
114
115 // If the cardinality is zero, the sort and the values are ignored in the FSM.
116 std::size_t cardinality() const
117 {
118 return m_cardinality;
119 }
120
121 std::size_t& cardinality()
122 {
123 return m_cardinality;
124 }
125
126 const std::vector<std::string>& values() const
127 {
128 return m_values;
129 }
130
131 std::vector<std::string>& values()
132 {
133 return m_values;
134 }
135};
136
141{
142 protected:
143 std::size_t m_source;
145 std::string m_label;
146
147 public:
148 fsm_transition(std::size_t source, std::size_t target, const std::string& label)
149 : m_source(source - 1),
152 {
153 if (source == 0 || target == 0)
154 {
155 throw mcrl2::runtime_error("A transition contains a state with state number 0.");
156 }
157 }
158
159 fsm_transition(const std::string& source_text, const std::string& target_text, const std::string& label)
160 : m_label(label)
161 {
162 std::size_t source = utilities::parse_natural_number(source_text);
163 if (source == 0)
164 {
165 throw mcrl2::runtime_error("A transition constains a source state with number 0.");
166 }
167 m_source = source - 1;
168 m_target = parse_distribution(target_text);
169 }
170
171 std::size_t source() const
172 {
173 return m_source;
174 }
175
176 std::size_t& source()
177 {
178 return m_source;
179 }
180
182 {
183 return m_target;
184 }
185
187 {
188 return m_target;
189 }
190
191 const std::string& label() const
192 {
193 return m_label;
194 }
195
196 std::string& label()
197 {
198 return m_label;
199 }
200};
201
203{
205 : fsm(fsm_),
207 {}
208
209 // Contains the result
211
212 // The parameters of the FSM
213 std::vector<fsm_parameter> parameters;
214
215 // Maps labels of the FSM to numbers
216 std::map<std::string, std::size_t> labels;
217
218 // This variable records if the initial state is set explicitly.
219 // If not it needs to be done while finishing the fsm.
221
222 void start()
223 {
224 parameters.clear();
225 labels.clear();
226 labels[action_label_string::tau_action()] = 0; // The label 0 is the tau action by default.
227 fsm.clear();
228 }
229
231 {
232 std::size_t max = 0;
233 if (distribution.size()>1)
234 {
235 for (const detail::lts_fsm_base::state_probability_pair& p: distribution)
236 {
237 max = std::max(max, p.state());
238 }
239 }
240 else
241 {
242 max=distribution.get();
243 }
244 return max;
245 }
246
247 void add_transition(const std::string& source, const std::string& target, const std::string& label)
248 {
249 fsm_transition t(source, target, label);
250
251 // Apply a correction with +1 for the mismatch between numbering in lts_fsm and the fsm file format
252 std::size_t max = std::max(t.source(),find_maximal_state_index(t.target()))+1;
253
254 if (fsm.num_states() <= max)
255 {
257 }
258 auto i = labels.find(t.label());
259 lts_fsm_t::labels_size_type label_index = 0;
260 if (i == labels.end())
261 {
262 assert(t.label() != action_label_string::tau_action());
263 label_index = fsm.add_action(action_label_string(t.label()));
264 labels[t.label()] = label_index;
265 }
266 else
267 {
268 label_index = i->second;
269 }
270
271 const std::size_t probabilistic_state_index = fsm.add_probabilistic_state(detail::lts_fsm_base::probabilistic_state(t.target()));
272 fsm.add_transition(transition(t.source(), label_index, probabilistic_state_index));
273 }
274
275 void add_state(const std::vector<std::size_t>& values)
276 {
278 }
279
280 void add_parameter(const std::string& name, const std::string& cardinality, const std::string& sort, const std::vector<std::string>& domain_values)
281 {
282 parameters.emplace_back(name, cardinality, sort, domain_values);
283 }
284
285 void add_initial_distribution(const std::string& distribution)
286 {
288 std::size_t max=find_maximal_state_index(d)+1; // Add one as state numbers are subtracted by one when parsing.
289
290 if (fsm.num_states() <= max)
291 {
293 }
295
298 }
299
301 {
302 std::size_t index = 0;
303 for (const fsm_parameter& param: parameters)
304 {
305 if (param.cardinality() > 0)
306 {
307 fsm.add_process_parameter(param.name(), param.sort());
308 for (const std::string& value: param.values())
309 {
310 fsm.add_state_element_value(index, value);
311 }
312 }
313 index++;
314 }
315 }
316
317 void finish()
318 {
319 // guarantee that the LTS has at least one state
320 if (fsm.num_states() == 0)
321 {
322 fsm.add_state();
323 }
325 {
327 }
328 }
329};
330
331} // namespace mcrl2::lts::detail
332
333#endif // MCRL2_LTS_DETAIL_FSM_BUILDER_H
This class contains strings to be used as values for action labels in lts's.
static const action_label_string & tau_action()
std::vector< std::string > m_values
Definition fsm_builder.h:85
const std::vector< std::string > & values() const
std::size_t cardinality() const
const std::string & name() const
Definition fsm_builder.h:95
fsm_parameter(const std::string &name, const std::string &cardinality, const std::string &sort, const std::vector< std::string > &values)
Definition fsm_builder.h:88
std::vector< std::string > & values()
const std::string & sort() const
const std::string & label() const
const lts_fsm_base::probabilistic_state & target() const
lts_fsm_base::probabilistic_state & target()
fsm_transition(std::size_t source, std::size_t target, const std::string &label)
fsm_transition(const std::string &source_text, const std::string &target_text, const std::string &label)
detail::lts_fsm_base::probabilistic_state m_target
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
states_size_type num_states() const
Gets the number of states of this LTS.
Definition lts.h:245
void set_num_states(const states_size_type n, const bool has_state_labels=true)
Sets the number of states of this LTS.
Definition lts.h:280
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
Definition lts.h:636
std::vector< action_label_string >::size_type labels_size_type
The sort that represents the indices of labels.
Definition lts.h:104
states_size_type add_state(const STATE_LABEL_T &label=STATE_LABEL_T())
Adds a state to this LTS.
Definition lts.h:347
labels_size_type add_action(const ACTION_LABEL_T &label)
Adds an action with a label to this LTS.
Definition lts.h:361
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:276
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
void clear()
Clear the transitions system.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
std::size_t size() const
Gets the number of probabilistic states in the vector representation of this state....
STATE get() const
Get a probabilistic state if is is simple, i.e., consists of a single state.
This class contains state labels for the fsm format.
Definition lts_fsm.h:38
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
This class contains labels for probabilistic transistions, consisting of a numerator and a denominato...
This file contains a class that contains labelled transition systems in fsm format.
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter &)
A base class for the lts_dot labelled transition system.
std::string split_string_until(std::string &s, const std::string &c1, const std::string &c2="")
Definition fsm_builder.h:22
lts_fsm_base::probabilistic_state parse_distribution(const std::string &distribution)
Definition fsm_builder.h:45
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t parse_natural_number(const std::string &text)
Parses a natural number from a string.
std::string trim_copy(const std::string &text)
Remove all trailing and leading spaces from the input.
add your file description here.
fsm_builder(probabilistic_lts_fsm_t &fsm_)
std::map< std::string, std::size_t > labels
void add_initial_distribution(const std::string &distribution)
void add_state(const std::vector< std::size_t > &values)
probabilistic_lts_fsm_t & fsm
void add_parameter(const std::string &name, const std::string &cardinality, const std::string &sort, const std::vector< std::string > &domain_values)
void add_transition(const std::string &source, const std::string &target, const std::string &label)
std::vector< fsm_parameter > parameters
std::size_t find_maximal_state_index(const lts_fsm_base::probabilistic_state &distribution)