mCRL2
Loading...
Searching...
No Matches
liblts_dot.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
15using namespace mcrl2::core;
16
17namespace mcrl2
18{
19namespace lts
20{
21
22void probabilistic_lts_dot_t::save(std::ostream& os) const
23{
24 // Language definition seems to suggest that the name is optional, but tools seem to think otherwise
25 os << "digraph G {" << std::endl;
26 // os << "size=\"7,10.5\";" << std::endl;
27 os << "center = TRUE;" << std::endl;
28 os << "mclimit = 10.0;" << std::endl;
29 os << "nodesep = 0.05;" << std::endl;
30 os << "node [ width=0.25, height=0.25, label=\"\" ];" << std::endl;
31 if (num_states() > 0)
32 {
33 if (initial_probabilistic_state().size()<=1)
34 {
35 const std::size_t initial_state=initial_probabilistic_state().get();
36 if (has_state_info())
37 {
38 os << state_label(initial_state).name();
39 }
40 else
41 {
42 os << "S" << initial_state;
43 }
44 }
45 else
46 {
47 throw mcrl2::runtime_error("Cannnot save a probabilistic transition system in .dot format.");
48 }
49
50 os << " [ peripheries=2 ];" << std::endl;
51 for (std::size_t i=0; i<num_states(); i++)
52 {
53 if (has_state_info())
54 {
55 const std::string& label = state_label(i).label();
56 if (!label.empty())
57 {
58 os << state_label(i).name() << " [label=\"" << label << "\"];" << std::endl;
59 }
60 }
61 else
62 {
63 os << "S" << i << std::endl;
64 }
65 }
66 }
67
68 for (const transition& t: get_transitions())
69 {
70 if (has_state_info())
71 {
72 if (probabilistic_state(t.to()).size()>1)
73 {
74 throw mcrl2::runtime_error("Cannot save probabilistic states in .dot format.");
75 }
76 os << state_label(t.from()).name() << "->" << state_label(probabilistic_state(t.to()).get()).name() << "[label=\"" <<
77 mcrl2::lts::pp(action_label(t.label())) << "\"];" << std::endl;
78 }
79 else
80 {
81 os << "S" << t.from() << " -> " << "S" << t.to() << "[label=\"" <<
82 mcrl2::lts::pp(action_label(apply_hidden_label_map(t.label()))) << "\"];" << std::endl;
83 }
84 }
85
86 os << "}" << std::endl;
87}
88
89void probabilistic_lts_dot_t::save(const std::string& filename) const
90{
91 std::ofstream os(filename.c_str());
92 if (!os.is_open())
93 {
94 throw mcrl2::runtime_error("cannot open DOT file '" + filename + "' for writing.");
95 }
96 save(os);
97 os.close();
98}
99
100void lts_dot_t::save(std::ostream& os) const
101{
107 detail::lts_dot_base>(*this,l);
108 l.save(os);
109}
110
111void lts_dot_t::save(const std::string& filename) const
112{
113 if (filename.empty() || filename=="-")
114 {
115 save(std::cout);
116 }
117 else
118 {
119 std::ofstream os(filename.c_str());
120 if (!os.is_open())
121 {
122 throw mcrl2::runtime_error("cannot open DOT file '" + filename + "' for writing.");
123 }
124 save(os);
125 os.close();
126 }
127}
128
129}
130}
This class contains strings to be used as values for action labels in lts's.
void save(std::ostream &os) const
Save the labelled transition system to a stream.
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
A class to contain labelled transition systems in graphviz format.
Definition lts_dot.h:163
void save(std::ostream &os) const
Save the labelled transition system to a stream.
const probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > & initial_probabilistic_state() const
Gets the initial state number of this LTS.
A class that contains a probabilistic state.
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 labels for states in dot format.
Definition lts_dot.h:37
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
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
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)
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