diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 53f3ba6c8..afb21561b 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -180,7 +180,7 @@ namespace storm { constantDefinition.name("constant definition"); // Shielding properties - shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + shieldExpression = (qi::lit("<") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_1, qi::_2)]; shieldExpression.name("shield expression"); @@ -645,12 +645,12 @@ namespace storm { return std::make_pair(comparisonType, value); } - std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { + std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, boost::optional> comparisonStruct) { if(comparisonStruct.is_initialized()) { - return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); + return std::shared_ptr(new storm::logic::ShieldExpression(type, comparisonStruct.get().first, comparisonStruct.get().second)); } else { STORM_LOG_INFO("Construction of shield without a comparison parameter (lambda or gamma) will default to 'lambda=0'"); - return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); + return std::shared_ptr(new storm::logic::ShieldExpression(type)); } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 97089658e..c4916ffbb 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -249,7 +249,7 @@ namespace storm { std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); - std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); + std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, boost::optional> comparisonStruct); bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); diff --git a/src/storm/logic/ShieldExpression.cpp b/src/storm/logic/ShieldExpression.cpp index 841d1a400..9902f625a 100644 --- a/src/storm/logic/ShieldExpression.cpp +++ b/src/storm/logic/ShieldExpression.cpp @@ -6,11 +6,11 @@ namespace storm { namespace logic { ShieldExpression::ShieldExpression() {} - ShieldExpression::ShieldExpression(ShieldingType type, std::string filename) : type(type), filename(filename) { + ShieldExpression::ShieldExpression(ShieldingType type) : type(type) { //Intentionally left empty } - ShieldExpression::ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value) : type(type), filename(filename), comparison(comparison), value(value) { + ShieldExpression::ShieldExpression(ShieldingType type, ShieldComparison comparison, double value) : type(type), comparison(comparison), value(value) { //Intentionally left empty } @@ -74,11 +74,7 @@ namespace storm { prettyString += "-Shield "; 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(); diff --git a/src/storm/logic/ShieldExpression.h b/src/storm/logic/ShieldExpression.h index 808ebddf9..eddf0becb 100644 --- a/src/storm/logic/ShieldExpression.h +++ b/src/storm/logic/ShieldExpression.h @@ -18,8 +18,8 @@ namespace storm { class ShieldExpression { public: ShieldExpression(); - ShieldExpression(ShieldingType type, std::string filename); - ShieldExpression(ShieldingType type, std::string filename, ShieldComparison comparison, double value); + ShieldExpression(ShieldingType type); + ShieldExpression(ShieldingType type, ShieldComparison comparison, double value); bool isRelative() const; bool isPreSafetyShield() const; @@ -34,15 +34,12 @@ namespace storm { 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 = ShieldComparison::Relative; double value = 0; - - std::string filename; }; } } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 68951bf1b..c1d0071e2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -695,6 +695,7 @@ namespace storm { std::vector choiceValues = std::vector(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero()); auto choice_it = maybeStateChoiceValues.begin(); + // TODO THIS IS BUGGY!! for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) { uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state); if (qualitativeStateSets.maybeStates.get(state)) { diff --git a/src/storm/shields/AbstractShield.cpp b/src/storm/shields/AbstractShield.cpp index abb57f57e..82f27bdc9 100644 --- a/src/storm/shields/AbstractShield.cpp +++ b/src/storm/shields/AbstractShield.cpp @@ -33,12 +33,6 @@ namespace tempest { std::string AbstractShield::getClassName() const { return std::string(boost::core::demangled_name(BOOST_CORE_TYPEID(*this))); } - - template - std::string AbstractShield::getShieldFileName() const { - return shieldingExpression->getFilename() + ".shield"; - } - // Explicitly instantiate appropriate template class AbstractShield::index_type>; diff --git a/src/storm/shields/AbstractShield.h b/src/storm/shields/AbstractShield.h index 8ca8d9117..9ef54775e 100644 --- a/src/storm/shields/AbstractShield.h +++ b/src/storm/shields/AbstractShield.h @@ -49,8 +49,7 @@ namespace tempest { storm::OptimizationDirection getOptimizationDirection(); std::string getClassName() const; - std::string getShieldFileName() const; - + virtual void printToStream(std::ostream& out, std::shared_ptr> const& model) = 0; virtual void printJsonToStream(std::ostream& out, std::shared_ptr> const& model) = 0; diff --git a/src/storm/shields/ShieldHandling.cpp b/src/storm/shields/ShieldHandling.cpp index fc5d48bfc..bcef9332c 100644 --- a/src/storm/shields/ShieldHandling.cpp +++ b/src/storm/shields/ShieldHandling.cpp @@ -2,10 +2,6 @@ namespace tempest { namespace shields { - std::string shieldFilename(std::shared_ptr const& shieldingExpression) { - return shieldingExpression->getFilename() + ".shield"; - } - template std::unique_ptr> createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates) { if(coalitionStates.is_initialized()) coalitionStates.get().complement(); diff --git a/src/storm/shields/ShieldHandling.h b/src/storm/shields/ShieldHandling.h index e50d3e860..1fff9a6a0 100644 --- a/src/storm/shields/ShieldHandling.h +++ b/src/storm/shields/ShieldHandling.h @@ -20,9 +20,7 @@ #include "storm/exceptions/InvalidArgumentException.h" namespace tempest { - namespace shields { - std::string shieldFilename(std::shared_ptr const& shieldingExpression); - + namespace shields { template std::unique_ptr> createShield(std::shared_ptr> model, std::vector const& choiceValues, std::shared_ptr const& shieldingExpression, storm::OptimizationDirection optimizationDirection, storm::storage::BitVector relevantStates, boost::optional coalitionStates);