From 8b73f0a0d138cb8277501d3447e833c4c05ba8f5 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Mon, 19 Apr 2021 11:33:44 +0200 Subject: [PATCH] added util functions to shieldExpression --- src/storm/logic/ShieldExpression.cpp | 25 ++++++++++++++++++++++++- src/storm/logic/ShieldExpression.h | 7 ++++++- 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/storm/logic/ShieldExpression.cpp b/src/storm/logic/ShieldExpression.cpp index d17cc85de..a9cbeb088 100644 --- a/src/storm/logic/ShieldExpression.cpp +++ b/src/storm/logic/ShieldExpression.cpp @@ -6,7 +6,11 @@ namespace storm { namespace logic { ShieldExpression::ShieldExpression() {} - ShieldExpression::ShieldExpression(ShieldingType type, ShieldComparison comparison, double value) : type(type), comparison(comparison), value(value) { + ShieldExpression::ShieldExpression(ShieldingType type, std::string filename) : type(type), filename(filename) { + //Intentionally left empty + } + + ShieldExpression::ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value) : type(type), filename(filename), comparison(comparison), value(value) { //Intentionally left empty } @@ -49,6 +53,25 @@ namespace storm { return "<" + typeToString() + ", " + comparisonToString() + "=" + std::to_string(value) + ">"; } + std::string ShieldExpression::prettify() const { + std::string prettyString = ""; + std::string comparisonType = isRelative() ? "relative" : "absolute"; + switch(type) { + case storm::logic::ShieldingType::PostSafety: prettyString += "Post-Safety"; break; + case storm::logic::ShieldingType::PreSafety: prettyString += "Pre-Safety"; break; + case storm::logic::ShieldingType::Optimal: prettyString += "Optimal"; break; + } + prettyString += "-Shield "; + if(!(type == storm::logic::ShieldingType::Optimal)) { + prettyString += "with " + comparisonType + " comparison (" + comparisonToString() + " = " + std::to_string(value) + "):"; + } + return prettyString; + } + + std::string ShieldExpression::getFilename() const { + return filename; + } + std::ostream& operator<<(std::ostream& out, ShieldExpression const& shieldExpression) { out << shieldExpression.toString(); return out; diff --git a/src/storm/logic/ShieldExpression.h b/src/storm/logic/ShieldExpression.h index 5a7a0cd45..b214f3baa 100644 --- a/src/storm/logic/ShieldExpression.h +++ b/src/storm/logic/ShieldExpression.h @@ -17,7 +17,8 @@ namespace storm { class ShieldExpression { public: ShieldExpression(); - ShieldExpression(ShieldingType type, ShieldComparison comparison, double value); + ShieldExpression(ShieldingType type, std::string filename); + ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value); bool isRelative() const; bool isPreSafetyShield() const; @@ -29,12 +30,16 @@ namespace storm { std::string typeToString() const; std::string comparisonToString() const; std::string toString() const; + std::string prettify() const; + std::string getFilename() const; friend std::ostream& operator<<(std::ostream& stream, ShieldExpression const& shieldExpression); private: ShieldingType type; ShieldComparison comparison; double value; + + std::string filename; }; } }