From aee1956950574f7eec41df0c4fde4ce6fa11b9ee Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 15:03:57 +0200 Subject: [PATCH] progress towards JANI formula support, fix for gcc Former-commit-id: 66d87dbe8c40c58166f90e538fd647ac33955a12 [formerly ac7ce466a1c796d6356af6ba0bcdb03672a721c7] Former-commit-id: ec11ee9831b08c93c45f758ac62d4803b2b0545c --- src/storage/jani/JSONExporter.cpp | 197 ++++++++++++++++++++++++++++++ src/storage/jani/JSONExporter.h | 27 ++++ src/storage/jani/Property.cpp | 15 +-- src/storage/jani/Property.h | 32 +++-- src/storage/ppg/defines.h | 2 + 5 files changed, 257 insertions(+), 16 deletions(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 3493affe4..be30b82b8 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -6,6 +6,7 @@ #include "src/utility/macros.h" #include "src/exceptions/FileIoException.h" +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidJaniException.h" @@ -20,6 +21,8 @@ #include "src/storage/expressions/BinaryRelationExpression.h" #include "src/storage/expressions/VariableExpression.h" +#include "src/logic/Formulas.h" + #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" @@ -85,6 +88,200 @@ namespace storm { bool allowRecursion; }; + std::string comparisonTypeToJani(storm::logic::ComparisonType ct) { + switch(ct) { + case storm::logic::ComparisonType::Less: + return "<"; + case storm::logic::ComparisonType::LessEqual: + return "≤"; + case storm::logic::ComparisonType::Greater: + return ">"; + case storm::logic::ComparisonType::GreaterEqual: + return "≥"; + } + } + + modernjson::json numberToJson(storm::RationalNumber rn) { + modernjson::json numDecl; + if(carl::isOne(carl::getDenom(rn))) { + numDecl = modernjson::json(carl::toString(carl::getNum(rn))); + } else { + numDecl["op"] = "/"; + numDecl["left"] = carl::toString(carl::getNum(rn)); + numDecl["right"] = carl::toString(carl::getDenom(rn)); + } + return numDecl; + } + + + modernjson::json constructPropertyInterval(uint64_t lower, uint64_t upper) { + modernjson::json iDecl; + iDecl["lower"] = lower; + iDecl["upper"] = upper; + return iDecl; + } + + modernjson::json constructPropertyInterval(double lower, double upper) { + modernjson::json iDecl; + iDecl["lower"] = lower; + iDecl["upper"] = upper; + return iDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { + return ExpressionToJson::translate(f.getExpression()); + } + + boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { + modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ + modernjson::json opDecl; + storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator(); + opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { + modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + if(f.hasDiscreteTimeBound()) { + opDecl["step-bounds"] = constructPropertyInterval(0, f.getDiscreteTimeBound()); + } else { + opDecl["time-bounds"] = constructPropertyInterval(f.getIntervalBounds().first, f.getIntervalBounds().second); + } + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + return opDecl; + } + + 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"); + + } + + 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"); + } + + 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"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + if(f.hasBound()) { + 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::LongRunAverageRewardFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getTrueFormula()->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + opDecl["step-bounds"] = constructPropertyInterval((uint64_t)1, (uint64_t)1); + return opDecl; + } + + + + + boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; + 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) ? "Pmax" : "Pmin"; + 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 ? "Pmin" : "Pmax"; + 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::RewardOperatorFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator(); + assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not); + opDecl["op"] = "¬"; + opDecl["exp"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast(f.getRightSubformula().accept(*this, boost::none)); + return opDecl; + } std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) { diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 604a27a47..ff54de5e8 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -2,6 +2,7 @@ #include "src/storage/expressions/ExpressionVisitor.h" +#include "src/logic/FormulaVisitor.h" #include "Model.h" // JSON parser #include "json.hpp" @@ -28,6 +29,31 @@ namespace storm { }; + class FormulaToJaniJson : public storm::logic::FormulaVisitor { + public: + static modernjson::json translate(storm::logic::Formula const& formula); + 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; + virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::GloballyFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::NextFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const; + 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; + + + }; + class JsonExporter { JsonExporter() = default; @@ -37,6 +63,7 @@ namespace storm { private: void convertModel(storm::jani::Model const& model); + void convertProperty(storm::logic::Formula const& formula); 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 9b097757d..195aec571 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::shared_ptr const& formula, std::string const& comment) - : name(name), formula(formula), comment(comment) - { - - } +// Property::Property(std::string const& name, std::string const& comment) +// : name(name), formula(formula), comment(comment) +// { +// +// } std::string const& Property::getName() const { return this->name; @@ -14,10 +14,7 @@ namespace storm { std::string const& Property::getComment() const { return this->comment; } - - std::shared_ptr const& Property::getFormula() const { - return this->formula; - } + } } \ No newline at end of file diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index 30bddac60..c0f08bc56 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -4,6 +4,27 @@ namespace storm { namespace jani { + + 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 PathExpression : public PropertyExpression { + std::shared_ptr leftStateExpression; + std::shared_ptr rightStateExpression; + }; + + + class Property { /** * Constructs the property @@ -22,16 +43,13 @@ namespace storm { * @return the comment */ std::string const& getComment() const; - /** - * Get the formula - * @return the formula - */ - std::shared_ptr const& getFormula() const; - + + + private: std::string name; - std::shared_ptr formula; std::string comment; + PropertyExpression propertyExpression; }; } } diff --git a/src/storage/ppg/defines.h b/src/storage/ppg/defines.h index 548160ba9..d993e633e 100644 --- a/src/storage/ppg/defines.h +++ b/src/storage/ppg/defines.h @@ -1,6 +1,8 @@ #pragma once #include #include +#include + namespace storm { namespace ppg { class ProgramGraph;