16#ifndef MCRL2_LTS_LTS_PREORDER_H
17#define MCRL2_LTS_LTS_PREORDER_H
67 else if (s ==
"ready-sim")
71 else if (s ==
"trace")
75 else if (s ==
"weak-trace")
79 else if (s ==
"trace-ac")
83 else if (s ==
"weak-trace-ac")
87 else if (s ==
"failures")
91 else if (s ==
"weak-failures")
95 else if (s ==
"failures-divergence")
117 is.setstate(std::ios_base::failbit);
145 return "weak-trace-ac";
149 return "weak-failures";
151 return "failures-divergence";
174 return "default void preorder";
176 return "strong simulation preorder";
178 return "strong ready simulation preorder";
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)";
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_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...