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#define BRANCH_BIS_EXPERIMENT_JFG
17
18#ifndef MCRL2_LTS_LTS_EQUIVALENCE_H
19#define MCRL2_LTS_LTS_EQUIVALENCE_H
20
21#include <string>
23
24namespace mcrl2
25{
26namespace lts
27{
28
34{
39#ifdef BRANCH_BIS_EXPERIMENT_JFG
41#endif
46#ifdef BRANCH_BIS_EXPERIMENT_JFG
48#endif
53#ifdef BRANCH_BIS_EXPERIMENT_JFG
55#endif
66};
67
99inline
101{
102 if (s == "none")
103 {
104 return lts_eq_none;
105 }
106 else if (s == "bisim")
107 {
108 return lts_eq_bisim;
109 }
110 else if (s == "bisim-gv")
111 {
112 return lts_eq_bisim_gv;
113 }
114 else if (s == "bisim-gjkw")
115 {
116 return lts_eq_bisim_gjkw;
117 }
118#ifdef BRANCH_BIS_EXPERIMENT_JFG
119 else if (s == "bisim-gj")
120 {
121 return lts_eq_bisim_gj;
122 }
123#endif
124 else if (s == "bisim-sig")
125 {
126 return lts_eq_bisim_sigref;
127 }
128 else if (s == "branching-bisim")
129 {
131 }
132 else if (s == "branching-bisim-gv")
133 {
135 }
136 else if (s == "branching-bisim-gjkw")
137 {
139 }
140#ifdef BRANCH_BIS_EXPERIMENT_JFG
141 else if (s == "branching-bisim-gj")
142 {
144 }
145#endif
146 else if (s == "branching-bisim-sig")
147 {
149 }
150 else if (s == "dpbranching-bisim")
151 {
153 }
154 else if (s == "dpbranching-bisim-gv")
155 {
157 }
158 else if (s == "dpbranching-bisim-gjkw")
159 {
161 }
162#ifdef BRANCH_BIS_EXPERIMENT_JFG
163 else if (s == "dpbranching-bisim-gj")
164 {
166 }
167#endif
168 else if (s == "dpbranching-bisim-sig")
169 {
171 }
172 else if (s == "weak-bisim")
173 {
174 return lts_eq_weak_bisim;
175 }
176 else if (s == "dpweak-bisim")
177 {
179 }
180 else if (s == "sim")
181 {
182 return lts_eq_sim;
183 }
184 else if (s == "ready-sim")
185 {
186 return lts_eq_ready_sim;
187 }
188 else if (s == "trace")
189 {
190 return lts_eq_trace;
191 }
192 else if (s == "weak-trace")
193 {
194 return lts_eq_weak_trace;
195 }
196 else if (s == "coupled-sim")
197 {
198 return lts_eq_coupled_sim;
199 }
200 else if (s == "tau-star")
201 {
202 return lts_red_tau_star;
203 }
204 else if (s == "determinisation")
205 {
207 }
208 else
209 {
210 throw mcrl2::runtime_error("Unknown equivalence " + s + ".");
211 }
212}
213
214// \overload
215inline
216std::istream& operator>>(std::istream& is, lts_equivalence& eq)
217{
218 try
219 {
220 std::string s;
221 is >> s;
222 eq = parse_equivalence(s);
223 }
225 {
226 is.setstate(std::ios_base::failbit);
227 }
228 return is;
229}
230
236inline std::string print_equivalence(const lts_equivalence eq)
237{
238 switch(eq)
239 {
240 case lts_eq_none:
241 return "none";
242 case lts_eq_bisim:
243 return "bisim";
244 case lts_eq_bisim_gv:
245 return "bisim-gv";
247 return "bisim-gjkw";
248#ifdef BRANCH_BIS_EXPERIMENT_JFG
249 case lts_eq_bisim_gj:
250 return "bisim-gj";
251#endif
253 return "bisim-sig";
255 return "branching-bisim";
257 return "branching-bisim-gv";
259 return "branching-bisim-gjkw";
260#ifdef BRANCH_BIS_EXPERIMENT_JFG
262 return "branching-bisim-gj";
263#endif
265 return "branching-bisim-sig";
267 return "dpbranching-bisim";
269 return "dpbranching-bisim-gv";
271 return "dpbranching-bisim-gjkw";
272#ifdef BRANCH_BIS_EXPERIMENT_JFG
274 return "dpbranching-bisim-gj";
275#endif
277 return "dpbranching-bisim-sig";
279 return "weak-bisim";
281 return "dpweak-bisim";
282 case lts_eq_sim:
283 return "sim";
284 case lts_eq_ready_sim:
285 return "ready-sim";
286 case lts_eq_trace:
287 return "trace";
289 return "weak-trace";
291 return "coupled-sim";
292 case lts_red_tau_star:
293 return "tau-star";
295 return "determinisation";
296 default:
297 throw mcrl2::runtime_error("Unknown equivalence.");
298 }
299}
300
301// \overload
302inline
303std::ostream& operator<<(std::ostream& os, const lts_equivalence eq)
304{
305 os << print_equivalence(eq);
306 return os;
307}
308
313inline std::string description(const lts_equivalence eq)
314{
315 switch(eq)
316 {
317 case lts_eq_none:
318 return "identity equivalence";
319 case lts_eq_bisim:
320 return "strong bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
321 case lts_eq_bisim_gv:
322 return "strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]";
324 return "strong bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]";
325#ifdef BRANCH_BIS_EXPERIMENT_JFG
326 case lts_eq_bisim_gj:
327 return "strong bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]";
328#endif
330 return "strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
332 return "branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
334 return "branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]";
336 return "branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]";
337#ifdef BRANCH_BIS_EXPERIMENT_JFG
339 return "branching bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]";
340#endif
342 return "branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
344 return "divergence-preserving branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
346 return "divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]";
348 return "divergence-preserving branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]";
349#ifdef BRANCH_BIS_EXPERIMENT_JFG
351 return "divergence-preserving branching bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]";
352#endif
354 return "divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
356 return "weak bisimilarity";
358 return "divergence-preserving weak bisimilarity";
359 case lts_eq_sim:
360 return "strong simulation equivalence";
361 case lts_eq_ready_sim:
362 return "strong ready simulation equivalence";
363 case lts_eq_trace:
364 return "strong trace equivalence";
366 return "weak trace equivalence";
368 return "coupled simulation equivalence";
369 case lts_red_tau_star:
370 return "tau star reduction";
372 return "determinisation reduction";
373 default:
374 throw mcrl2::runtime_error("Unknown equivalence.");
375 }
376}
377
378} // namespace lts
379} // namespace mcrl2
380
381#endif // MCRL2_LTS_LTS_EQUIVALENCE_H
382
383
384
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_branching_bisim_gj
@ lts_eq_divergence_preserving_branching_bisim_gjkw
@ lts_eq_divergence_preserving_branching_bisim_gv
@ lts_eq_divergence_preserving_branching_bisim_gj
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