16#define BRANCH_BIS_EXPERIMENT_JFG
18#ifndef MCRL2_LTS_LTS_EQUIVALENCE_H
19#define MCRL2_LTS_LTS_EQUIVALENCE_H
39#ifdef BRANCH_BIS_EXPERIMENT_JFG
46#ifdef BRANCH_BIS_EXPERIMENT_JFG
53#ifdef BRANCH_BIS_EXPERIMENT_JFG
106 else if (s ==
"bisim")
110 else if (s ==
"bisim-gv")
114 else if (s ==
"bisim-gjkw")
118#ifdef BRANCH_BIS_EXPERIMENT_JFG
119 else if (s ==
"bisim-gj")
124 else if (s ==
"bisim-sig")
128 else if (s ==
"branching-bisim")
132 else if (s ==
"branching-bisim-gv")
136 else if (s ==
"branching-bisim-gjkw")
140#ifdef BRANCH_BIS_EXPERIMENT_JFG
141 else if (s ==
"branching-bisim-gj")
146 else if (s ==
"branching-bisim-sig")
150 else if (s ==
"dpbranching-bisim")
154 else if (s ==
"dpbranching-bisim-gv")
158 else if (s ==
"dpbranching-bisim-gjkw")
162#ifdef BRANCH_BIS_EXPERIMENT_JFG
163 else if (s ==
"dpbranching-bisim-gj")
168 else if (s ==
"dpbranching-bisim-sig")
172 else if (s ==
"weak-bisim")
176 else if (s ==
"dpweak-bisim")
184 else if (s ==
"ready-sim")
188 else if (s ==
"trace")
192 else if (s ==
"weak-trace")
196 else if (s ==
"coupled-sim")
200 else if (s ==
"tau-star")
204 else if (s ==
"determinisation")
226 is.setstate(std::ios_base::failbit);
248#ifdef BRANCH_BIS_EXPERIMENT_JFG
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";
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";
277 return "dpbranching-bisim-sig";
281 return "dpweak-bisim";
291 return "coupled-sim";
295 return "determinisation";
318 return "identity equivalence";
320 return "strong bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]";
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
327 return "strong bisimilarity using the O(m log n) experimental algorithm [Groote/Jansen 2024]";
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]";
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]";
354 return "divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003]";
356 return "weak bisimilarity";
358 return "divergence-preserving weak bisimilarity";
360 return "strong simulation equivalence";
362 return "strong ready simulation equivalence";
364 return "strong trace equivalence";
366 return "weak trace equivalence";
368 return "coupled simulation equivalence";
370 return "tau star reduction";
372 return "determinisation reduction";
Standard exception class for reporting runtime errors.
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.
std::ostream & operator<<(std::ostream &out, const abstraction &x)
lts_equivalence
LTS equivalence relations.
@ lts_eq_branching_bisim_sigref
@ lts_eq_divergence_preserving_weak_bisim
@ lts_eq_branching_bisim_gjkw
@ lts_red_determinisation
@ 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...