From 1fd89f3922a6bb5daeecd63b1dc6dda11f043b23 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 14 Nov 2016 12:08:26 +0100 Subject: [PATCH] fixes in reach expression parsing for expected reward Former-commit-id: d9f5e887d8daf12e03716bfb30dc63d6a3c839a6 [formerly 02cea9bff274de8b91fa3c5c350897044a0aeadd] Former-commit-id: dd387c2595beb5494ba055aa5c0067caee899d9e --- src/parser/JaniParser.cpp | 4 +++- src/storage/jani/JSONExporter.cpp | 34 ++++++++++++++++--------------- src/storage/jani/JSONExporter.h | 10 ++++----- 3 files changed, 26 insertions(+), 22 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a149a9e92..76d3d1e1e 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -223,7 +223,7 @@ namespace storm { } std::shared_ptr reach; if (propertyStructure.count("reach") > 0) { - reach = parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString); + reach = std::make_shared(parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString)); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported"); } @@ -425,6 +425,8 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Looking for operator for formula " << propertyStructure.dump() << ", but did not find one"); } } diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 967922622..e0c37fabc 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -139,8 +139,8 @@ namespace storm { return iDecl; } - modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) { - FormulaToJaniJson translator(continuousTime); + modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model) { + FormulaToJaniJson translator(model); return boost::any_cast(formula.accept(translator)); } @@ -334,35 +334,37 @@ namespace storm { boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { modernjson::json opDecl; std::vector accvec; - if(continuous) { - accvec.push_back("time"); - } else { + if(model.isDiscreteTimeModel()) { accvec.push_back("steps"); + } else { + accvec.push_back("time"); } if(f.hasBound()) { auto bound = f.getBound(); opDecl["op"] = comparisonTypeToJani(bound.comparisonType); if(f.hasOptimalityType()) { opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); } else { opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; - opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); } - opDecl["left"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); + opDecl["left"]["exp"] = f.getRewardModelName(); opDecl["left"]["accumulate"] = modernjson::json(accvec); opDecl["right"] = numberToJson(bound.threshold); } else { if(f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); } else { // TODO add checks opDecl["op"] = "Emin"; - opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none)); } - opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); + opDecl["exp"] = f.getRewardModelName(); opDecl["accumulate"] = modernjson::json(accvec); } return opDecl; @@ -520,7 +522,7 @@ namespace storm { } JsonExporter exporter; exporter.convertModel(janiModel); - exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel()); + exporter.convertProperties(formulas, janiModel); os << exporter.finalize().dump(4) << std::endl; } @@ -732,23 +734,23 @@ namespace storm { } } - modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { + modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model) { modernjson::json propDecl; propDecl["states"]["op"] = "initial"; propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); - propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); + propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model); return propDecl; } - void JsonExporter::convertProperties( std::vector> const& formulas, bool continuousModel) { + void JsonExporter::convertProperties( std::vector> const& formulas, storm::jani::Model const& model) { std::vector properties; uint64_t index = 0; for(auto const& f : formulas) { modernjson::json propDecl; propDecl["name"] = "prop" + std::to_string(index); - propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), continuousModel); + propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), model); ++index; properties.push_back(propDecl); } diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 67c448160..3f82984be 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -33,9 +33,9 @@ namespace storm { }; class FormulaToJaniJson : public storm::logic::FormulaVisitor { - + public: - static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime); + static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& modeln); virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; @@ -56,8 +56,8 @@ namespace storm { virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; private: - FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { } - bool continuous; + FormulaToJaniJson(storm::jani::Model const& model) : model(model) { } + storm::jani::Model const& model; }; class JsonExporter { @@ -69,7 +69,7 @@ namespace storm { private: void convertModel(storm::jani::Model const& model); - void convertProperties(std::vector> const& formulas, bool timeContinuousModel); + void convertProperties(std::vector> const& formulas, storm::jani::Model const& model); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() {