Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
RegionResult.cpp
Go to the documentation of this file.
2
5
6namespace storm {
7namespace modelchecker {
8std::ostream& operator<<(std::ostream& os, RegionResult const& regionResult) {
9 switch (regionResult) {
11 os << "Unknown";
12 break;
14 os << "ExistsSat";
15 break;
17 os << "ExistsViolated";
18 break;
20 os << "CenterSat";
21 break;
23 os << "CenterViolated";
24 break;
26 os << "ExistsBoth";
27 break;
29 os << "AllSat";
30 break;
32 os << "AllViolated";
33 break;
34 default:
35 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException,
36 "Could not get a string from the region check result. The case has not been implemented");
37 }
38 return os;
39}
40} // namespace modelchecker
41} // namespace storm
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::ostream & operator<<(std::ostream &os, RegionCheckEngine const &e)
RegionResult
The results for a single Parameter Region.
@ CenterSat
the formula is satisfied for the parameter Valuation that corresponds to the center point of the regi...
@ AllSat
the formula is satisfied for all parameters in the given region
@ AllViolated
the formula is violated for all parameters in the given region
@ Unknown
the result is unknown
@ ExistsBoth
the formula is satisfied for some parameters but also violated for others
@ CenterViolated
the formula is violated for the parameter Valuation that corresponds to the center point of the regio...
@ ExistsSat
the formula is satisfied for at least one parameter evaluation that lies in the given region
@ ExistsViolated
the formula is violated for at least one parameter evaluation that lies in the given region
LabParser.cpp.
Definition cli.cpp:18