mCRL2
Loading...
Searching...
No Matches
lts_equivalence.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, Jan Friso Groote
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
16#ifndef MCRL2_LTS_LTS_EQUIVALENCE_H
17#define MCRL2_LTS_LTS_EQUIVALENCE_H
18
19#include <string>
21
22namespace mcrl2
23{
24namespace lts
25{
26
32{
55};
56
88inline
90{
91 if (s == "none")
92 {
93 return lts_eq_none;
94 }
95 else if (s == "bisim")
96 {
97 return lts_eq_bisim;
98 }
99 else if (s == "bisim-gv")
100 {
101 return lts_eq_bisim_gv;
102 }
103 else if (s == "bisim-gjkw")
104 {
105 return lts_eq_bisim_gjkw;
106 }
107 else if (s == "bisim-sig")
108 {
109 return lts_eq_bisim_sigref;
110 }
111 else if (s == "branching-bisim")
112 {
114 }
115 else if (s == "branching-bisim-gv")
116 {
118 }
119 else if (s == "branching-bisim-gjkw")
120 {
122 }
123 else if (s == "branching-bisim-sig")
124 {
126 }
127 else if (s == "dpbranching-bisim")
128 {
130 }
131 else if (s == "dpbranching-bisim-gv")
132 {
134 }
135 else if (s == "dpbranching-bisim-gjkw")
136 {
138 }
139 else if (s == "dpbranching-bisim-sig")
140 {
142 }
143 else if (s == "weak-bisim")
144 {
145 return lts_eq_weak_bisim;
146 }
147 else if (s == "dpweak-bisim")
148 {
150 }
151 else if (s == "sim")
152 {
153 return lts_eq_sim;
154 }
155 else if (s == "ready-sim")
156 {
157 return lts_eq_ready_sim;
158 }
159 else if (s == "trace")
160 {
161 return lts_eq_trace;
162 }
163 else if (s == "weak-trace")
164 {
165 return lts_eq_weak_trace;
166 }
167 else if (s == "coupled-sim")
168 {
169 return lts_eq_coupled_sim;
170 }
171 else if (s == "tau-star")
172 {
173 return lts_red_tau_star;
174 }
175 else if (s == "determinisation")
176 {
178 }
179 else
180 {
181 throw mcrl2::runtime_error("Unknown equivalence " + s + ".");
182 }
183}
184
185// \overload
186inline
187std::istream& operator>>(std::istream& is, lts_equivalence& eq)
188{
189 try
190 {
191 std::string s;
192 is >> s;
193 eq = parse_equivalence(s);
194 }
196 {
197 is.setstate(std::ios_base::failbit);
198 }
199 return is;
200}
201
207inline std::string print_equivalence(const lts_equivalence eq)
208{
209 switch(eq)
210 {
211 case lts_eq_none:
212 return "none";
213 case lts_eq_bisim:
214 return "bisim";
215 case lts_eq_bisim_gv:
216 return "bisim-gv";
218 return "bisim-gjkw";
220 return "bisim-sig";
222 return "branching-bisim";
224 return "branching-bisim-gv";
226 return "branching-bisim-gjkw";
228 return "branching-bisim-sig";
230 return "dpbranching-bisim";
232 return "dpbranching-bisim-gv";
234 return "dpbranching-bisim-gjkw";
236 return "dpbranching-bisim-sig";
238 return "weak-bisim";
240 return "dpweak-bisim";
241 case lts_eq_sim:
242 return "sim";
243 case lts_eq_ready_sim:
244 return "ready-sim";
245 case lts_eq_trace:
246 return "trace";
248 return "weak-trace";
250 return "coupled-sim";
251 case lts_red_tau_star:
252 return "tau-star";
254 return "determinisation";
255 default:
256 throw mcrl2::runtime_error("Unknown equivalence.");
257 }
258}
259
260// \overload
261inline
262std::ostream& operator<<(std::ostream& os, const lts_equivalence eq)
263{
264 os << print_equivalence(eq);
265 return os;
266}
267
272inline std::string description(const lts_equivalence eq)
273{
274 switch(eq)
275 {
276 case lts_eq_none:
277 return "identity equivalence";
278 case lts_eq_bisim:
279 return "strong bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
280 case lts_eq_bisim_gv:
281 return "strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]";
283 return "strong bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]";
285 return "strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
287 return "branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
289 return "branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]";
291 return "branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]";
293 return "branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
295 return "divergence-preserving branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
297 return "divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]";
299 return "divergence-preserving branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]";
301 return "divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
303 return "weak bisimilarity";
305 return "divergence-preserving weak bisimilarity";
306 case lts_eq_sim:
307 return "strong simulation equivalence";
308 case lts_eq_ready_sim:
309 return "strong ready simulation equivalence";
310 case lts_eq_trace:
311 return "strong trace equivalence";
313 return "weak trace equivalence";
315 return "coupled simulation equivalence";
316 case lts_red_tau_star:
317 return "tau star reduction";
319 return "determinisation reduction";
320 default:
321 throw mcrl2::runtime_error("Unknown equivalence.");
322 }
323}
324
325} // namespace lts
326} // namespace mcrl2
327
328#endif // MCRL2_LTS_LTS_EQUIVALENCE_H
329
330
331
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
std::string description(const rewrite_strategy s)
standard descriptions for rewrite strategies
atermpp::aterm_istream & operator>>(atermpp::aterm_istream &stream, data_specification &spec)
Reads a data specification from a stream.
Definition data_io.cpp:66
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
lts_equivalence
LTS equivalence relations.
@ lts_eq_branching_bisim_sigref
@ lts_eq_divergence_preserving_weak_bisim
@ lts_eq_branching_bisim_gjkw
@ lts_eq_branching_bisim_gv
@ lts_eq_divergence_preserving_branching_bisim_sigref
@ lts_eq_divergence_preserving_branching_bisim
@ lts_eq_divergence_preserving_branching_bisim_gjkw
@ lts_eq_divergence_preserving_branching_bisim_gv
std::string print_equivalence(const lts_equivalence eq)
Gives the short name of an equivalence.
lts_equivalence parse_equivalence(std::string const &s)
Determines the equivalence from a string.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72