mCRL2
Loading...
Searching...
No Matches
lts_preorder.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_PREORDER_H
17#define MCRL2_LTS_LTS_PREORDER_H
18
19#include <string>
21
22namespace mcrl2
23{
24namespace lts
25{
26
32{
45};
46
56inline
57lts_preorder parse_preorder(std::string const& s)
58{
59 if (s == "unknown")
60 {
61 return lts_pre_none;
62 }
63 else if (s == "sim")
64 {
65 return lts_pre_sim;
66 }
67 else if (s == "ready-sim")
68 {
69 return lts_pre_ready_sim;
70 }
71 else if (s == "trace")
72 {
73 return lts_pre_trace;
74 }
75 else if (s == "weak-trace")
76 {
77 return lts_pre_weak_trace;
78 }
79 else if (s == "trace-ac")
80 {
82 }
83 else if (s == "weak-trace-ac")
84 {
86 }
87 else if (s == "failures")
88 {
90 }
91 else if (s == "weak-failures")
92 {
94 }
95 else if (s == "failures-divergence")
96 {
98 }
99 else
100 {
101 throw mcrl2::runtime_error("unknown preorder " + s);
102 }
103}
104
105// \overload
106inline
107std::istream& operator>>(std::istream& is, lts_preorder& eq)
108{
109 try
110 {
111 std::string s;
112 is >> s;
113 eq = parse_preorder(s);
114 }
115 catch (mcrl2::runtime_error&)
116 {
117 is.setstate(std::ios_base::failbit);
118 }
119 return is;
120}
121
127inline
128std::string print_preorder(const lts_preorder pre)
129{
130 switch(pre)
131 {
132 case lts_pre_none:
133 return "unknown";
134 case lts_pre_sim:
135 return "sim";
137 return "ready-sim";
138 case lts_pre_trace:
139 return "trace";
141 return "weak-trace";
143 return "trace-ac";
145 return "weak-trace-ac";
147 return "failures";
149 return "weak-failures";
151 return "failures-divergence";
152 default:
153 throw mcrl2::runtime_error("unknown preorder");
154 }
155}
156
157inline
158std::ostream& operator<<(std::ostream& os, const lts_preorder pre)
159{
160 os << print_preorder(pre);
161 return os;
162}
163
168inline
169std::string description(const lts_preorder pre)
170{
171 switch(pre)
172 {
173 case lts_pre_none:
174 return "default void preorder";
175 case lts_pre_sim:
176 return "strong simulation preorder";
178 return "strong ready simulation preorder";
179 case lts_pre_trace:
180 return "strong trace preorder";
182 return "weak trace preorder";
184 return "trace preorder based on an anti chain algorithm";
186 return "weak trace preorder based on an anti chain algorithm";
188 return "failures refinement";
190 return "weak failures refinement";
192 return "failures divergence refinement (automatically weak)";
193 default:
194 throw mcrl2::runtime_error("unknown preorder");
195 }
196}
197
198} // namespace lts
199} // namespace mcrl2
200
201#endif // MCRL2_LTS_LTS_PREORDER_H
202
203
204
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_preorder
LTS preorder relations.
@ lts_pre_failures_refinement
@ lts_pre_failures_divergence_refinement
@ lts_pre_weak_trace_anti_chain
@ lts_pre_weak_failures_refinement
@ lts_pre_trace_anti_chain
std::string print_preorder(const lts_preorder pre)
Gives the short name of a preorder.
lts_preorder parse_preorder(std::string const &s)
Determines the preorder 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