mCRL2
Loading...
Searching...
No Matches
liblts_fsm.cpp
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg
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//
10
11#include "mcrl2/lts/lts_io.h"
12#include "mcrl2/lts/parse.h"
14
15namespace mcrl2 {
16
17namespace lts {
18
20{
21 std::ostream& out;
24
25 fsm_writer(std::ostream& out_, const probabilistic_lts_fsm_t& fsm_)
26 : out(out_),
27 number_of_initial_state(fsm_.initial_probabilistic_state().size()<=1?
28 fsm_.initial_probabilistic_state().get():
29 fsm_.initial_probabilistic_state().begin()->state()),
30 fsm(fsm_)
31 {
32 }
33
34 // This functions swaps 0 with the number number_of_initial_state of the initial state.
35 std::size_t swap_initial_state(const std::size_t i)
36 {
38 {
39 return 0;
40 }
41 if (i==0)
42 {
44 }
45 return i;
46 }
47
49 {
50 // print parameters with used values
51 mCRL2log(log::verbose) << "writing parameter table..." << std::endl;
52 for (std::size_t i = 0; i < fsm.process_parameters().size(); i++)
53 {
54 const std::vector<std::string>& values = fsm.state_element_values(i);
55 out << fsm.process_parameter(i).first << "(" << values.size() << ") " << fsm.process_parameter(i).second << " ";
56 for (const std::string& s: values)
57 {
58 out << " \"" << s << "\"";
59 }
60 out << std::endl;
61 }
62 }
63
65 {
66 mCRL2log(log::verbose) << "writing states..." << std::endl;
67 for (std::size_t i = 0; i < fsm.num_states(); i++)
68 {
69 if (fsm.has_state_info())
70 {
71 const state_label_fsm& state_parameters = fsm.state_label(swap_initial_state(i));
72 for (std::size_t j = 0; j < state_parameters.size(); j++)
73 {
74 if (j > 0)
75 {
76 out << " ";
77 }
78 out << state_parameters[j];
79 }
80 out << std::endl;
81 }
82 }
83 }
84
85 // If there is only a single state with probility 1, write a single state, otherwise
86 // write "[state1 probability1, state2 probability2, ..., state_n probability_n]".
88 {
90 {
92 }
93 else
94 {
95 assert(probabilistic_state.size()>1);
96 out << "[";
97 bool first=true;
99 {
100 if (first)
101 {
102 first=false;
103 }
104 else
105 {
106 out << ' ';
107 }
108 out << swap_initial_state(p.state()) + 1 << " " << p.probability();
109 }
110 out << "]";
111 }
112 }
113
115 {
116 mCRL2log(log::verbose) << "writing transitions..." << std::endl;
117 for (const transition& t: fsm.get_transitions())
118 {
119 // correct state numbering, by adding 1.
120 out << swap_initial_state(t.from()) + 1 << " ";
122 out << " \"" << mcrl2::lts::pp(fsm.action_label(fsm.apply_hidden_label_map(t.label()))) << "\"" << std::endl;
123 }
124 }
125
126 void write()
127 {
129 out << "---" << std::endl;
130 write_states();
131 out << "---" << std::endl;
133 // If there is a initial distribution with more than one state, write the initial distribution.
135 {
136 out << "---" << std::endl;
138 out << "\n" << std::endl;
139 }
140 }
141};
142
143void probabilistic_lts_fsm_t::load(const std::string& filename)
144{
145 if (filename.empty() || filename=="-")
146 {
147 try
148 {
149 parse_fsm_specification(std::cin, *this);
150 }
151 catch (mcrl2::runtime_error& e)
152 {
153 throw mcrl2::runtime_error(std::string("Error parsing .fsm file from standard input.\n") + e.what());
154 }
155 }
156 else
157 {
158 std::ifstream is(filename.c_str());
159
160 if (!is.is_open())
161 {
162 throw mcrl2::runtime_error("Cannot open .fsm file " + filename + ".");
163 }
164 try
165 {
166 parse_fsm_specification(is, *this);
167 }
168 catch (mcrl2::runtime_error& e)
169 {
170 throw mcrl2::runtime_error(std::string("Error parsing .fsm file.\n") + e.what());
171 }
172 is.close();
173 }
174}
175
176void probabilistic_lts_fsm_t::save(const std::string& filename) const
177{
178 if (filename.empty() || filename=="-")
179 {
180 fsm_writer(std::cout, *this).write();
181 }
182 else
183 {
184 std::ofstream os(filename.c_str());
185
186 if (!os.is_open())
187 {
188 throw mcrl2::runtime_error("Cannot create .fsm file '" + filename + ".");
189 return;
190 }
191
192 fsm_writer(os, *this).write();
193 os.close();
194 }
195}
196
197void lts_fsm_t::load(const std::string& filename)
198{
200 l.load(filename);
205 detail::lts_fsm_base>(l,*this);
206}
207
208void lts_fsm_t::save(const std::string& filename) const
209{
215 detail::lts_fsm_base>(*this,l);
216 l.save(filename);
217}
218
219
220} // namespace lts
221
222} // namespace mcrl2
Read-only balanced binary tree of terms.
This class contains strings to be used as values for action labels in lts's.
mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > probabilistic_state
Definition lts_fsm.h:86
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.
states_size_type num_states() const
Gets the number of states of this LTS.
Definition lts.h:245
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
Definition lts.h:636
labels_size_type apply_hidden_label_map(const labels_size_type action) const
If the action label is registered hidden, it returns tau, otherwise the original label.
Definition lts.h:438
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
Definition lts.h:450
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
Definition lts.h:526
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:276
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.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
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
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
A simple straighforward parser for .fsm files.
This include file contains routines to read and write labelled transitions from and to files and from...
std::string pp(const abstraction &x)
Definition data.cpp:39
@ verbose
Definition logger.h:35
void translate_to_probabilistic_lts(const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &l_plain, probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &l_probabilistic)
void swap_to_non_probabilistic_lts(probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &l_probabilistic, lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &l_plain)
void parse_fsm_specification(std::istream &from, probabilistic_lts_fsm_t &result)
Definition parse.h:169
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
std::size_t swap_initial_state(const std::size_t i)
std::size_t number_of_initial_state
const probabilistic_lts_fsm_t & fsm
void write_probabilistic_state(const detail::lts_fsm_base::probabilistic_state &probabilistic_state)
fsm_writer(std::ostream &out_, const probabilistic_lts_fsm_t &fsm_)