mCRL2
Loading...
Searching...
No Matches
liblts.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
12#include "mcrl2/lts/lts_io.h"
13
14using namespace mcrl2::core;
15using namespace mcrl2::core::detail;
16using namespace mcrl2::log;
17
18
19namespace mcrl2
20{
21namespace lts
22{
23namespace detail
24{
25
26lts_type guess_format(std::string const& s, const bool be_verbose/*=true*/)
27{
28 std::string::size_type pos = s.find_last_of('.');
29
30 if (pos != std::string::npos)
31 {
32 std::string ext = s.substr(pos+1);
33
34 if (ext == "aut")
35 {
36 if (be_verbose)
37 {
38 mCRL2log(verbose) << "Detected .aut extension.\n";
39 }
40 return lts_aut;
41 }
42 else if (ext == "lts")
43 {
44 if (be_verbose)
45 {
46 mCRL2log(verbose) << "Detected .lts extension.\n";
47 }
48 return lts_lts;
49 }
50 else if (ext == "fsm")
51 {
52 if (be_verbose)
53 {
54 mCRL2log(verbose) << "Detected .fsm extension.\n";
55 }
56 return lts_fsm;
57 }
58 else if (ext == "dot")
59 {
60 if (be_verbose)
61 {
62 mCRL2log(verbose) << "Detected .dot extension.\n";
63 }
64 return lts_dot;
65 }
66 }
67
68 return lts_none;
69}
70
71static const std::string type_strings[] = { "unknown", "lts", "aut", "fsm", "dot" };
72
73static const std::string extension_strings[] = { "", "lts", "aut", "fsm", "dot" };
74
75static std::string type_desc_strings[] = {
76 "unknown LTS format",
77 "mCRL2 LTS format",
78 "Aldebaran format (CADP)",
79 "Finite State Machine format",
80 "GraphViz format (no longer supported as input format)",
81 "SVC format"
82 };
83
84
85static std::string mime_type_strings[] = { "",
86 "application/lts",
87 "text/aut",
88 "text/fsm",
89 "text/dot"
90 };
91
92lts_type parse_format(std::string const& s)
93{
94 if (s == "lts")
95 {
96 return lts_lts;
97 }
98 else if (s == "aut")
99 {
100 return lts_aut;
101 }
102 else if (s == "fsm")
103 {
104 return lts_fsm;
105 }
106 else if (s == "dot")
107 {
108 return lts_dot;
109 }
110 return lts_none;
111}
112
113std::string string_for_type(const lts_type type)
114{
115 return (type_strings[type]);
116}
117
118std::string extension_for_type(const lts_type type)
119{
120 return (extension_strings[type]);
121}
122
123std::string mime_type_for_type(const lts_type type)
124{
125 return (mime_type_strings[type]);
126}
127
128static const std::set<lts_type>& initialise_supported_lts_formats()
129{
130 static std::set<lts_type> s;
131 for (std::size_t i = lts_type_min; i<1+(std::size_t)lts_type_max; ++i)
132 {
133 if (lts_none != (lts_type) i)
134 {
135 s.insert((lts_type) i);
136 }
137 }
138 return s;
139}
140const std::set<lts_type>& supported_lts_formats()
141{
142 static const std::set<lts_type>& s = initialise_supported_lts_formats();
143 return s;
144}
145
146/* Auxiliary function, used below */
147template<typename T>
148bool lts_named_cmp(const std::string N[], T a, T b)
149{
150 return N[a] < N[b];
151}
152
153std::string supported_lts_formats_text(lts_type default_format, const std::set<lts_type>& supported)
154{
155 std::vector<lts_type> types(supported.begin(), supported.end());
156 std::sort(types.begin(),
157 types.end(),
158 [](const lts_type& t1, const lts_type& t2){ return lts_named_cmp<lts_type>(type_strings, t1, t2); });
159
160 std::string r;
161 for (std::vector<lts_type>::iterator i=types.begin(); i!=types.end(); ++i)
162 {
163 r += " '" + type_strings[*i] + "' for the " + type_desc_strings[*i];
164
165 if (*i == default_format)
166 {
167 r += " (default)";
168 }
169
170 // Still unsafe if types.size() < 2
171 assert(types.size() >= 2);
172 if (i == types.end() - 2)
173 {
174 r += ", or\n";
175 }
176 else if (i != types.end() - 1)
177 {
178 r += ",\n";
179 }
180 }
181
182 return r;
183}
184
185std::string supported_lts_formats_text(const std::set<lts_type>& supported)
186{
187 return supported_lts_formats_text(lts_none,supported);
188}
189
190std::string lts_extensions_as_string(const std::string& sep, const std::set<lts_type>& supported)
191{
192 std::vector<lts_type> types(supported.begin(), supported.end());
193 std::sort(types.begin(),
194 types.end(),
195 [](const lts_type& t1, const lts_type& t2){ return lts_named_cmp<lts_type>(extension_strings, t1, t2); });
196
197 std::string r, prev;
198 bool first = true;
199 for (std::vector<lts_type>::iterator i=types.begin(); i!=types.end(); i++)
200 {
201 if (extension_strings[*i] == prev) // avoid mentioning extensions more than once
202 {
203 continue;
204 }
205 if (first)
206 {
207 first = false;
208 }
209 else
210 {
211 r += sep;
212 }
213 r += "*." + extension_strings[*i];
214 prev = extension_strings[*i];
215 }
216
217 return r;
218}
219
220std::string lts_extensions_as_string(const std::set<lts_type>& supported)
221{
222 return lts_extensions_as_string(",",supported);
223}
224
225} // namespace detail
226} //lts
227} //data
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
Algorithms for LTS, such as equivalence reductions, determinisation, etc.
This include file contains routines to read and write labelled transitions from and to files and from...
normalizer< Function > N(const Function &f)
@ verbose
Definition logger.h:35
std::string supported_lts_formats_text(lts_type default_format=lts_none, const std::set< lts_type > &supported=supported_lts_formats())
Gives a textual list describing supported LTS formats.
Definition liblts.cpp:153
static std::string type_desc_strings[]
Definition liblts.cpp:75
std::string extension_for_type(const lts_type type)
Gives the filename extension associated with an LTS format.
Definition liblts.cpp:118
std::string string_for_type(const lts_type type)
Gives a string representation of an LTS format.
Definition liblts.cpp:113
static const std::string type_strings[]
Definition liblts.cpp:71
const std::set< lts_type > & supported_lts_formats()
Gives the set of all supported LTS formats.
Definition liblts.cpp:140
bool lts_named_cmp(const std::string N[], T a, T b)
Definition liblts.cpp:148
std::string lts_extensions_as_string(const std::string &sep=",", const std::set< lts_type > &supported=supported_lts_formats())
Gives a list of extensions for supported LTS formats.
Definition liblts.cpp:190
lts_type parse_format(std::string const &s)
Determines the LTS format from a format specification string.
Definition liblts.cpp:92
lts_type guess_format(std::string const &s, const bool be_verbose=true)
Determines the LTS format from a filename by its extension.
Definition liblts.cpp:26
static const std::string extension_strings[]
Definition liblts.cpp:73
std::string mime_type_for_type(const lts_type type)
Gives the MIME type associated with an LTS format.
Definition liblts.cpp:123
static const std::set< lts_type > & initialise_supported_lts_formats()
Definition liblts.cpp:128
static std::string mime_type_strings[]
Definition liblts.cpp:85
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
@ lts_type_min
Definition lts_type.h:46
@ lts_type_max
Definition lts_type.h:47
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72