From 744216d5d2c2ae77a681dca3b5df23e0196888fd Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 18:39:28 +0200 Subject: [PATCH] export formulae Former-commit-id: 4932938e383e1c8d2b09dd46591f070a43651380 [formerly 95b3269c755ac84aede16254a514be7d26a2aa24] Former-commit-id: 974a891cb6adfef1b39f9d94f1abdd63950dd7de --- src/cli/cli.cpp | 24 ++--- src/parser/JaniParser.cpp | 7 ++ src/storage/jani/JSONExporter.cpp | 158 ++++++++++++++++++++++++++++-- src/storage/jani/JSONExporter.h | 15 +-- src/storage/jani/Property.cpp | 10 +- src/storage/jani/Property.h | 29 +++--- 6 files changed, 200 insertions(+), 43 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 2c5104123..db9829084 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -222,13 +222,23 @@ namespace storm { model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; } + // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. + std::vector> formulas; + if (storm::settings::getModule().isPropertySet()) { + if (model.isJaniModel()) { + formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); + } else { + formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); + } + } + if(model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { if (storm::settings::getModule().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule().getJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule().getJaniFilename()); } } @@ -236,15 +246,7 @@ namespace storm { std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); - // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. - std::vector> formulas; - if (storm::settings::getModule().isPropertySet()) { - if (model.isJaniModel()) { - formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); - } else { - formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); - } - } + if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a49ab5548..97fc467e5 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -110,6 +110,13 @@ namespace storm { for (auto const& automataEntry : parsedStructure.at("automata")) { model.addAutomaton(parseAutomaton(automataEntry, model)); } + STORM_LOG_THROW(parsedStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Model has multiple initial value restrictions"); + storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); + if(parsedStructure.count("restrict-initial") > 0) { + STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Model needs an expression inside the initial restricion"); + initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name); + } + model.setInitialStatesRestriction(initialValueRestriction); STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index be30b82b8..e6c1e9d60 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -9,6 +9,7 @@ #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidJaniException.h" +#include "src/exceptions/NotImplementedException.h" #include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" @@ -25,6 +26,7 @@ #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" +#include "src/storage/jani/Property.h" namespace storm { namespace jani { @@ -128,6 +130,11 @@ namespace storm { return iDecl; } + modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) { + FormulaToJaniJson translator(continuousTime); + return boost::any_cast(formula.accept(translator)); + } + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { return ExpressionToJson::translate(f.getExpression()); } @@ -178,16 +185,44 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); - + modernjson::json opDecl; + std::vector tvec; + tvec.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)); + } 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"]["exp"] = modernjson::json(1); + opDecl["left"]["accumulate"] = modernjson::json(tvec); + 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)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["exp"] = modernjson::json(1); + opDecl["accumulate"] = modernjson::json(tvec); + } + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula"); } boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { @@ -219,7 +254,30 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const { - +// modernjson::json opDecl; +// if(f.()) { +// auto bound = f.getBound(); +// opDecl["op"] = comparisonTypeToJani(bound.comparisonType); +// if(f.hasOptimalityType()) { +// opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; +// opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// } else { +// opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin"; +// opDecl["left"]["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// } +// opDecl["right"] = numberToJson(bound.threshold); +// } else { +// if(f.hasOptimalityType()) { +// opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; +// opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// +// } else { +// // TODO add checks +// opDecl["op"] = "Pmin"; +// opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); +// } +// } +// return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { @@ -263,7 +321,40 @@ 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 { + accvec.push_back("steps"); + } + 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)); + } 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"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + 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)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + } + opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + opDecl["accumulate"] = modernjson::json(accvec); + } + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { @@ -402,22 +493,23 @@ namespace storm { - void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) { + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector> const& formulas, std::string const& filepath, bool checkValid) { std::ofstream ofs; ofs.open (filepath, std::ofstream::out ); if(ofs.is_open()) { - toStream(janiModel, ofs, checkValid); + toStream(janiModel, formulas, ofs, checkValid); } else { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); } } - void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) { + void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector> const& formulas, std::ostream& os, bool checkValid) { if(checkValid) { janiModel.checkValid(); } JsonExporter exporter; exporter.convertModel(janiModel); + exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel()); os << exporter.finalize().dump(4) << std::endl; } @@ -597,6 +689,54 @@ namespace storm { } + std::string janiFilterTypeString(storm::jani::FilterType const& ft) { + switch(ft) { + case storm::jani::FilterType::MIN: + return "min"; + case storm::jani::FilterType::MAX: + return "max"; + case storm::jani::FilterType::SUM: + return "sum"; + case storm::jani::FilterType::AVG: + return "avg"; + case storm::jani::FilterType::COUNT: + return "count"; + case storm::jani::FilterType::EXISTS: + return "∃"; + case storm::jani::FilterType::FORALL: + return "∀"; + case storm::jani::FilterType::ARGMIN: + return "argmin"; + case storm::jani::FilterType::ARGMAX: + return "argmax"; + case storm::jani::FilterType::VALUES: + return "values"; + + } + } + + modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { + modernjson::json propDecl; + propDecl["states"] = "initial"; + propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); + propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); + return propDecl; + } + + + void JsonExporter::convertProperties( std::vector> const& formulas, bool continuousModel) { + 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); + ++index; + properties.push_back(propDecl); + } + jsonStruct["properties"] = properties; + } + } } diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index ff54de5e8..55895364d 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -30,8 +30,9 @@ namespace storm { }; class FormulaToJaniJson : public storm::logic::FormulaVisitor { - public: - static modernjson::json translate(storm::logic::Formula const& formula); + + public: + static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime); 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; @@ -51,19 +52,21 @@ namespace storm { virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; - + private: + FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { } + bool continuous; }; class JsonExporter { JsonExporter() = default; public: - static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true); - static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false); + static void toFile(storm::jani::Model const& janiModel, std::vector> const& formulas, std::string const& filepath, bool checkValid = true); + static void toStream(storm::jani::Model const& janiModel, std::vector> const& formulas, std::ostream& ostream, bool checkValid = false); private: void convertModel(storm::jani::Model const& model); - void convertProperty(storm::logic::Formula const& formula); + void convertProperties(std::vector> const& formulas, bool timeContinuousModel); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 195aec571..28981f313 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,11 +1,11 @@ #include "Property.h" namespace storm { namespace jani { -// Property::Property(std::string const& name, std::string const& comment) -// : name(name), formula(formula), comment(comment) -// { -// -// } + Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) + : name(name), filterExpression(FilterExpression(formula)), comment(comment) + { + + } std::string const& Property::getName() const { return this->name; diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index c0f08bc56..bde51865e 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -8,20 +8,25 @@ namespace storm { enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; - class PropertyExpression { - - }; - class FilterExpression : public PropertyExpression { - std::shared_ptr states; - std::shared_ptr values; - FilterType ft; + class FilterExpression { + public: + explicit FilterExpression(std::shared_ptr formula) : values(formula) {} + + std::shared_ptr const& getFormula() const { + return values; + } + + FilterType getFilterType() const { + return ft; + } + private: + // For now, we assume that the states are always the initial states. + + std::shared_ptr values; + FilterType ft = FilterType::VALUES; }; - class PathExpression : public PropertyExpression { - std::shared_ptr leftStateExpression; - std::shared_ptr rightStateExpression; - }; @@ -49,7 +54,7 @@ namespace storm { private: std::string name; std::string comment; - PropertyExpression propertyExpression; + FilterExpression filterExpression; }; } }