mCRL2
Loading...
Searching...
No Matches
lts_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_BUILDER_H
13#define MCRL2_LTS_BUILDER_H
14
15#include "mcrl2/lps/explorer.h"
17#include "mcrl2/lts/lts_io.h"
18
19namespace mcrl2 {
20
21namespace lts {
22
24inline
26{
27 return lps::state(s.begin(), s.size() - 1);
28}
29
31{
33 // All LTS classes use integers to represent actions in transitions. A mapping from actions to integers
34 // is needed to avoid duplicates.
36
38 {
40 m_actions.emplace(std::make_pair(tau, m_actions.size()));
41 }
42
43 std::size_t add_action(const lps::multi_action& a)
44 {
45 lps::multi_action sorted_multi_action(a.sort_actions());
46 auto i = m_actions.find(sorted_multi_action);
47 if (i == m_actions.end())
48 {
49 i = m_actions.emplace(std::make_pair(sorted_multi_action, m_actions.size())).first;
50 }
51 return i->second;
52 }
53
54 // Add a transition to the LTS
55 virtual void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads = 0) = 0;
56
57 // Add actions and states to the LTS
58 virtual void finalize(const indexed_set_for_states_type& state_map, bool timed) = 0;
59
60 // Save the LTS to a file
61 virtual void save(const std::string& filename) = 0;
62
63 virtual ~lts_builder() = default;
64};
65
67{
68 public:
69 void add_transition(std::size_t /* from */, const lps::multi_action& /* a */, std::size_t /* to */, const std::size_t /* number_of_threads */) override
70 {}
71
72 void finalize(const indexed_set_for_states_type& /* state_map */, bool /* timed */) override
73 {}
74
75 void save(const std::string& /* filename */) override
76 {}
77};
78
80{
81 protected:
84
85 public:
86 lts_aut_builder() = default;
87
88 void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
89 {
91 std::size_t label = add_action(a);
94 }
95
96 // Add actions and states to the LTS
97 void finalize(const indexed_set_for_states_type& state_map, bool /* timed */) override
98 {
99 // add actions
101 for (const auto& p: m_actions)
102 {
104 }
105
106 m_lts.set_num_states(state_map.size());
107 }
108
109 void save(const std::string& filename) override
110 {
111 m_lts.save(filename);
112 }
113};
114
115// Write transitions immediately to disk, and add the AUT header later.
117{
118 protected:
119 std::ofstream out;
120 std::size_t m_transition_count = 0;
122
123 public:
124 explicit lts_aut_disk_builder(const std::string& filename)
125 {
126 mCRL2log(log::verbose) << "writing state space in AUT format to '" << filename << "'." << std::endl;
127 out.open(filename.c_str());
128 if (!out.is_open())
129 {
130 throw mcrl2::runtime_error("cannot open '" + filename + "' for writing");
131 }
132 out << "des \n"; // write a dummy header that will be overwritten
133 }
134
135 void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
136 {
139 out << "(" << from << ",\"" << lps::pp(a) << "\"," << to << ")\n";
141 }
142
143 // Add actions and states to the LTS
144 void finalize(const indexed_set_for_states_type& state_map, bool /* timed */) override
145 {
146 assert(!out.fail());
147 out.flush();
148 out.seekp(0);
149 if (out.fail())
150 {
151 throw mcrl2::runtime_error("seeking is not supported by the output stream");
152 }
153 out << "des (0," << m_transition_count << "," << state_map.size() << ")";
154 out.close();
155 }
156
157 void save(const std::string& /* filename */) override
158 { }
159};
160
162{
163 protected:
167
168 public:
170 const data::data_specification& dataspec,
171 const process::action_label_list& action_labels,
172 const data::variable_list& process_parameters,
173 bool discard_state_labels = false
174 )
175 : m_discard_state_labels(discard_state_labels)
176 {
177 m_lts.set_data(dataspec);
178 m_lts.set_process_parameters(process_parameters);
180 }
181
182 void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
183 {
185 std::size_t label = add_action(a);
188 }
189
190 // Add actions and states to the LTS
191 void finalize(const indexed_set_for_states_type& state_map, bool timed) override
192 {
193 // add actions
195 for (const auto& p: m_actions)
196 {
197 m_lts.set_action_label(p.second, action_label_lts(lps::multi_action(p.first.actions(), p.first.time())));
198 }
199
200 // add state labels
202 {
203 std::size_t n = state_map.size();
204 std::vector<state_label_lts> state_labels(n);
205 for (std::size_t i = 0; i < n; i++)
206 {
207 if (timed)
208 {
209 state_labels[i] = state_label_lts(remove_time_stamp(state_map[i]));
210 }
211 else
212 {
213 state_labels[i] = state_label_lts(state_map[i]);
214 }
215 }
216 m_lts.state_labels() = std::move(state_labels);
217 }
218
219 m_lts.set_num_states(state_map.size(), true);
221 }
222
223 void save(const std::string& filename) override
224 {
225 m_lts.save(filename);
226 }
227};
228
230{
231 protected:
232 std::fstream fstream;
233 std::unique_ptr<atermpp::binary_aterm_ostream> stream;
236
237 public:
239 const std::string& filename,
240 const data::data_specification& dataspec,
241 const process::action_label_list& action_labels,
242 const data::variable_list& process_parameters,
243 bool discard_state_labels = false
244 )
245 : m_discard_state_labels(discard_state_labels)
246 {
247 bool to_stdout = filename.empty() || filename == "-";
248 if (!to_stdout)
249 {
250 fstream.open(filename, std::ofstream::out | std::ofstream::binary);
251 if (fstream.fail())
252 {
253 throw mcrl2::runtime_error("Fail to open file " + filename + " for writing.");
254 }
255
256 mCRL2log(log::verbose) << "writing state space in LTS format to '" << filename << "'." << std::endl;
257 }
258 stream = std::make_unique<atermpp::binary_aterm_ostream>(to_stdout ? std::cout : fstream);
259
260 mcrl2::lts::write_lts_header(*stream, dataspec, process_parameters, action_labels);
261 }
262
263 void add_transition(std::size_t from, const lps::multi_action& a, std::size_t to, const std::size_t number_of_threads) override
264 {
268 }
269
270 // Add actions and states to the LTS
271 void finalize(const indexed_set_for_states_type& state_map, bool timed) override
272 {
274 {
275 // Write the state labels in the order of their indices.
276 for (std::size_t i = 0; i < state_map.size(); i++)
277 {
278 if (is_aterm_balanced_tree(state_map[i])) // in a parallel context not all positions may be filled.
279 {
280 if (timed)
281 {
283 }
284 else
285 {
287 }
288 }
289 }
290 }
291
292 // Write the initial state.
294 }
295
296 void save(const std::string&) override {}
297};
298
300{
301 public:
303 lts_dot_builder(const data::data_specification& dataspec, const process::action_label_list& action_labels, const data::variable_list& process_parameters)
304 : super(dataspec, action_labels, process_parameters)
305 { }
306
307 void save(const std::string& filename) override
308 {
309 lts_dot_t dot;
311 dot.save(filename);
312 }
313};
314
316{
317 public:
319 lts_fsm_builder(const data::data_specification& dataspec, const process::action_label_list& action_labels, const data::variable_list& process_parameters)
320 : super(dataspec, action_labels, process_parameters)
321 { }
322
323 void save(const std::string& filename) override
324 {
325 lts_fsm_t fsm;
327 fsm.save(filename);
328 }
329};
330
331inline
332std::unique_ptr<lts_builder> create_lts_builder(const lps::specification& lpsspec, const lps::explorer_options& options, lts_type output_format, const std::string& output_filename = "")
333{
334 switch (output_format)
335 {
336 case lts_aut:
337 {
338 if (options.save_at_end)
339 {
340 return std::make_unique<lts_aut_builder>();
341 }
342 else
343 {
344 return std::make_unique<lts_aut_disk_builder>(output_filename);
345 }
346 }
347 case lts_dot: return std::make_unique<lts_dot_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters());
348 case lts_fsm: return std::make_unique<lts_fsm_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters());
349 case lts_lts:
350 {
351 if (options.save_at_end)
352 {
353 return std::make_unique<lts_lts_builder>(lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters(), options.discard_lts_state_labels);
354 }
355 else
356 {
357 return std::make_unique<lts_lts_disk_builder>(output_filename, lpsspec.data(), lpsspec.action_labels(), lpsspec.process().process_parameters(), options.discard_lts_state_labels);
358 }
359 }
360 default: return std::make_unique<lts_none_builder>();
361 }
362}
363
364} // namespace lts
365
366} // namespace mcrl2
367
368#endif // MCRL2_LTS_BUILDER_H
A set that assigns each element an unique index, and protects its internal terms en masse.
Definition indexed_set.h:30
Read-only balanced binary tree of terms.
size_type size() const
Returns the size of the term_balanced_tree.
iterator begin() const
Returns an iterator pointing to the beginning of the term_balanced_tree.
A list of aterm objects.
Definition aterm_list.h:23
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
multi_action sort_actions() const
Returns the multiaction in which the list of actions is sorted.
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const LinearProcess & process() const
Returns the linear process of the specification.
const data::data_specification & data() const
Returns the data specification.
Linear process specification.
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
This class contains strings to be used as values for action labels in lts's.
void set_process_parameters(const data::variable_list &params)
Set the state parameters for this LTS.
Definition lts_lts.h:358
void set_action_label_declarations(const process::action_label_list &decls)
Set the action label information for this LTS.
Definition lts_lts.h:322
void set_data(const data::data_specification &spec)
Set the mCRL2 data specification of this LTS.
Definition lts_lts.h:330
void save(const std::string &filename) override
std::mutex m_exclusive_transition_access
Definition lts_builder.h:83
void add_transition(std::size_t from, const lps::multi_action &a, std::size_t to, const std::size_t number_of_threads) override
Definition lts_builder.h:88
void finalize(const indexed_set_for_states_type &state_map, bool) override
Definition lts_builder.h:97
void finalize(const indexed_set_for_states_type &state_map, bool) override
void save(const std::string &) override
void add_transition(std::size_t from, const lps::multi_action &a, std::size_t to, const std::size_t number_of_threads) override
lts_aut_disk_builder(const std::string &filename)
A simple labelled transition format with only strings as action labels.
Definition lts_aut.h:70
void save(const std::string &filename) const
Save the labelled transition system to file.
void save(const std::string &filename) override
lts_dot_builder(const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters)
A class to contain labelled transition systems in graphviz format.
Definition lts_dot.h:137
void save(std::ostream &os) const
Save the labelled transition system to a stream.
void save(const std::string &filename) override
lts_fsm_builder(const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters)
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:248
void save(const std::string &filename) const
Save the labelled transition system to file.
lts_lts_builder(const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters, bool discard_state_labels=false)
void add_transition(std::size_t from, const lps::multi_action &a, std::size_t to, const std::size_t number_of_threads) override
void save(const std::string &filename) override
void finalize(const indexed_set_for_states_type &state_map, bool timed) override
std::mutex m_exclusive_transition_access
void add_transition(std::size_t from, const lps::multi_action &a, std::size_t to, const std::size_t number_of_threads) override
std::unique_ptr< atermpp::binary_aterm_ostream > stream
lts_lts_disk_builder(const std::string &filename, const data::data_specification &dataspec, const process::action_label_list &action_labels, const data::variable_list &process_parameters, bool discard_state_labels=false)
void finalize(const indexed_set_for_states_type &state_map, bool timed) override
void save(const std::string &) override
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:374
void save(const std::string &filename) const
Save the labelled transition system to file.
void finalize(const indexed_set_for_states_type &, bool) override
Definition lts_builder.h:72
void add_transition(std::size_t, const lps::multi_action &, std::size_t, const std::size_t) override
Definition lts_builder.h:69
void save(const std::string &) override
Definition lts_builder.h:75
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
void set_num_action_labels(const labels_size_type n)
Sets the number of action labels of this LTS.
Definition lts.h:310
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
std::vector< STATE_LABEL_T > & state_labels()
Provides the state labels of an LTS.
Definition lts.h:253
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
Definition lts.h:334
void set_action_label(const labels_size_type action, const ACTION_LABEL_T &label)
Sets the label of an action.
Definition lts.h:402
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:40
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
size_type size(std::size_t thread_index=0) const
The number of elements in the indexed set.
A class for a map of keys to values in T based using the simple hash table set implementation.
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains lts_convert routines that translate different lts formats into each other.
This include file contains routines to read and write labelled transitions from and to files and from...
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:62
@ verbose
Definition logger.h:35
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
std::string pp(const action_summand &x)
Definition lps.cpp:26
void lts_convert(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
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 to(const outgoing_pair_t &p)
Target state of a label state pair.
void write_lts_header(atermpp::aterm_ostream &stream, const data::data_specification &data, const data::variable_list &parameters, const process::action_label_list &action_labels)
Writes the start of an LTS stream.
void write_initial_state(atermpp::aterm_ostream &stream, std::size_t index)
Write the initial state to the LTS stream.
void write_state_label(atermpp::aterm_ostream &stream, const state_label_lts &label)
Write a state label to the LTS stream.
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
void write_transition(atermpp::aterm_ostream &stream, std::size_t from, const lps::multi_action &label, std::size_t to)
Write a transition to the LTS stream.
lps::state remove_time_stamp(const lps::state &s)
Removes the last element from state s.
Definition lts_builder.h:25
std::unique_ptr< lts_builder > create_lts_builder(const lps::specification &lpsspec, const lps::explorer_options &options, lts_type output_format, const std::string &output_filename="")
static constexpr bool GlobalThreadSafe
Enables thread safety for the whole toolset.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
virtual ~lts_builder()=default
virtual void add_transition(std::size_t from, const lps::multi_action &a, std::size_t to, const std::size_t number_of_threads=0)=0
atermpp::indexed_set< lps::state, mcrl2::utilities::detail::GlobalThreadSafe > indexed_set_for_states_type
Definition lts_builder.h:32
virtual void finalize(const indexed_set_for_states_type &state_map, bool timed)=0
utilities::unordered_map_large< lps::multi_action, std::size_t > m_actions
Definition lts_builder.h:35
virtual void save(const std::string &filename)=0
std::size_t add_action(const lps::multi_action &a)
Definition lts_builder.h:43