mCRL2
Loading...
Searching...
No Matches
lts_probabilistic_equivalence.h
Go to the documentation of this file.
1// Author(s): Hector Joao Rivera Veruzco
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_PROBABILISTIC_EQUIVALENCE_H
17#define MCRL2_LTS_LTS_PROBABILISTIC_EQUIVALENCE_H
18
19#include <string>
21
22namespace mcrl2
23{
24namespace lts
25{
26
32{
36};
37
46inline
48{
49 if (s == "none")
50 {
52 }
53 else if (s == "pbisim-bem")
54 {
56 }
57 else if (s == "pbisim")
58 {
60 }
61 else
62 {
63 throw mcrl2::runtime_error("Unknown equivalence " + s + ".");
64 }
65}
66
67// \overload
68inline
69std::istream& operator>>(std::istream& is, lts_probabilistic_equivalence& eq)
70{
71 try
72 {
73 std::string s;
74 is >> s;
76 }
78 {
79 is.setstate(std::ios_base::failbit);
80 }
81 return is;
82}
83
90{
91 switch (eq)
92 {
94 return "none";
96 return "pbisim-bem";
98 return "pbisim";
99 default:
100 throw mcrl2::runtime_error("Unknown equivalence.");
101 }
102}
103
104// \overload
105inline
106std::ostream& operator<<(std::ostream& os, const lts_probabilistic_equivalence& eq)
107{
109 return os;
110}
111
116inline std::string description(const lts_probabilistic_equivalence& eq)
117{
118 switch(eq)
119 {
121 return "identity equivalence";
123 return "probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm by Baier, Engelen and Majster-Cederbaum, 2000";
125 return "probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera-Verduzco and de Vink, 2017";
126 default:
127 throw mcrl2::runtime_error("Unknown equivalence.");
128 }
129}
130
131
137{
139};
140
148inline
150{
151 if (s == "none")
152 {
154 }
155 else
156 {
157 throw mcrl2::runtime_error("Unknown preorder " + s + ".");
158 }
159}
160
161// \overload
162inline
163std::istream& operator>>(std::istream& is, lts_probabilistic_preorder& eq)
164{
165 try
166 {
167 std::string s;
168 is >> s;
170 }
172 {
173 is.setstate(std::ios_base::failbit);
174 }
175 return is;
176}
177
184{
185 switch (pre)
186 {
188 return "none";
189 default:
190 throw mcrl2::runtime_error("Unknown preorder.");
191 }
192}
193
194// \overload
195inline
196std::ostream& operator<<(std::ostream& os, const lts_probabilistic_preorder& pre)
197{
199 return os;
200}
201
206inline std::string description(const lts_probabilistic_preorder& pre)
207{
208 switch (pre)
209 {
211 return "identity preorder";
212 default:
213 throw mcrl2::runtime_error("Unknown preorder.");
214 }
215}
216
217} // namespace lts
218} // namespace mcrl2
219
220#endif // MCRL2_LTS_LTS_PROBABILISTIC_EQUIVALENCE_H
221
222
223
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_probabilistic_preorder parse_probabilistic_preorder(std::string const &s)
Determines the probabilistic preorder from a string.
lts_probabilistic_equivalence
LTS equivalence relations.
std::string print_probabilistic_equivalence(const lts_probabilistic_equivalence &eq)
Gives the short name of an equivalence.
lts_probabilistic_equivalence parse_probabilistic_equivalence(const std::string &s)
Determines the equivalence from a string.
lts_probabilistic_preorder
LTS preorder relations.
std::string print_probabilistic_preorder(const lts_probabilistic_preorder &pre)
Gives the short name of an preorder.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72