Line data Source code
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 : //
9 : /// \file liblts.cpp
10 :
11 : #include "mcrl2/lts/lts_algorithm.h"
12 : #include "mcrl2/lts/lts_io.h"
13 :
14 : using namespace mcrl2::core;
15 : using namespace mcrl2::core::detail;
16 : using namespace mcrl2::log;
17 :
18 :
19 : namespace mcrl2
20 : {
21 : namespace lts
22 : {
23 : namespace detail
24 : {
25 :
26 0 : lts_type guess_format(std::string const& s, const bool be_verbose/*=true*/)
27 : {
28 0 : std::string::size_type pos = s.find_last_of('.');
29 :
30 0 : if (pos != std::string::npos)
31 : {
32 0 : std::string ext = s.substr(pos+1);
33 :
34 0 : if (ext == "aut")
35 : {
36 0 : if (be_verbose)
37 : {
38 0 : mCRL2log(verbose) << "Detected .aut extension.\n";
39 : }
40 0 : return lts_aut;
41 : }
42 0 : else if (ext == "lts")
43 : {
44 0 : if (be_verbose)
45 : {
46 0 : mCRL2log(verbose) << "Detected .lts extension.\n";
47 : }
48 0 : return lts_lts;
49 : }
50 0 : else if (ext == "fsm")
51 : {
52 0 : if (be_verbose)
53 : {
54 0 : mCRL2log(verbose) << "Detected .fsm extension.\n";
55 : }
56 0 : return lts_fsm;
57 : }
58 0 : else if (ext == "dot")
59 : {
60 0 : if (be_verbose)
61 : {
62 0 : mCRL2log(verbose) << "Detected .dot extension.\n";
63 : }
64 0 : return lts_dot;
65 : }
66 0 : }
67 :
68 0 : return lts_none;
69 : }
70 :
71 : static const std::string type_strings[] = { "unknown", "lts", "aut", "fsm", "dot" };
72 :
73 : static const std::string extension_strings[] = { "", "lts", "aut", "fsm", "dot" };
74 :
75 : static 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 :
85 : static std::string mime_type_strings[] = { "",
86 : "application/lts",
87 : "text/aut",
88 : "text/fsm",
89 : "text/dot"
90 : };
91 :
92 0 : lts_type parse_format(std::string const& s)
93 : {
94 0 : if (s == "lts")
95 : {
96 0 : return lts_lts;
97 : }
98 0 : else if (s == "aut")
99 : {
100 0 : return lts_aut;
101 : }
102 0 : else if (s == "fsm")
103 : {
104 0 : return lts_fsm;
105 : }
106 0 : else if (s == "dot")
107 : {
108 0 : return lts_dot;
109 : }
110 0 : return lts_none;
111 : }
112 :
113 0 : std::string string_for_type(const lts_type type)
114 : {
115 0 : return (type_strings[type]);
116 : }
117 :
118 0 : std::string extension_for_type(const lts_type type)
119 : {
120 0 : return (extension_strings[type]);
121 : }
122 :
123 0 : std::string mime_type_for_type(const lts_type type)
124 : {
125 0 : return (mime_type_strings[type]);
126 : }
127 :
128 0 : static const std::set<lts_type>& initialise_supported_lts_formats()
129 : {
130 0 : static std::set<lts_type> s;
131 0 : for (std::size_t i = lts_type_min; i<1+(std::size_t)lts_type_max; ++i)
132 : {
133 0 : if (lts_none != (lts_type) i)
134 : {
135 0 : s.insert((lts_type) i);
136 : }
137 : }
138 0 : return s;
139 : }
140 0 : const std::set<lts_type>& supported_lts_formats()
141 : {
142 0 : static const std::set<lts_type>& s = initialise_supported_lts_formats();
143 0 : return s;
144 : }
145 :
146 : /* Auxiliary function, used below */
147 : template<typename T>
148 0 : bool lts_named_cmp(const std::string N[], T a, T b)
149 : {
150 0 : return N[a] < N[b];
151 : }
152 :
153 0 : std::string supported_lts_formats_text(lts_type default_format, const std::set<lts_type>& supported)
154 : {
155 0 : std::vector<lts_type> types(supported.begin(), supported.end());
156 0 : std::sort(types.begin(),
157 : types.end(),
158 0 : [](const lts_type& t1, const lts_type& t2){ return lts_named_cmp<lts_type>(type_strings, t1, t2); });
159 :
160 0 : std::string r;
161 0 : for (std::vector<lts_type>::iterator i=types.begin(); i!=types.end(); ++i)
162 : {
163 0 : r += " '" + type_strings[*i] + "' for the " + type_desc_strings[*i];
164 :
165 0 : if (*i == default_format)
166 : {
167 0 : r += " (default)";
168 : }
169 :
170 : // Still unsafe if types.size() < 2
171 0 : assert(types.size() >= 2);
172 0 : if (i == types.end() - 2)
173 : {
174 0 : r += ", or\n";
175 : }
176 0 : else if (i != types.end() - 1)
177 : {
178 0 : r += ",\n";
179 : }
180 : }
181 :
182 0 : return r;
183 0 : }
184 :
185 0 : std::string supported_lts_formats_text(const std::set<lts_type>& supported)
186 : {
187 0 : return supported_lts_formats_text(lts_none,supported);
188 : }
189 :
190 0 : std::string lts_extensions_as_string(const std::string& sep, const std::set<lts_type>& supported)
191 : {
192 0 : std::vector<lts_type> types(supported.begin(), supported.end());
193 0 : std::sort(types.begin(),
194 : types.end(),
195 0 : [](const lts_type& t1, const lts_type& t2){ return lts_named_cmp<lts_type>(extension_strings, t1, t2); });
196 :
197 0 : std::string r, prev;
198 0 : bool first = true;
199 0 : for (std::vector<lts_type>::iterator i=types.begin(); i!=types.end(); i++)
200 : {
201 0 : if (extension_strings[*i] == prev) // avoid mentioning extensions more than once
202 : {
203 0 : continue;
204 : }
205 0 : if (first)
206 : {
207 0 : first = false;
208 : }
209 : else
210 : {
211 0 : r += sep;
212 : }
213 0 : r += "*." + extension_strings[*i];
214 0 : prev = extension_strings[*i];
215 : }
216 :
217 0 : return r;
218 0 : }
219 :
220 0 : std::string lts_extensions_as_string(const std::set<lts_type>& supported)
221 : {
222 0 : return lts_extensions_as_string(",",supported);
223 : }
224 :
225 : } // namespace detail
226 : } //lts
227 : } //data
|
