From 011e3fbaa65c06f67a9ca1258bfc444848bd62a4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 13:54:29 +0200 Subject: [PATCH 1/9] fixed bug that introduced transient variables in the state space Former-commit-id: b335cf0c0dae3be17160ec6ca44a29c72996b6f9 [formerly 84339f7943cc25252bd8ccd6addc84401e643d2c] Former-commit-id: 6f64020873265b23e9af9cc6c816045ec13d2ce8 --- src/generator/JaniNextStateGenerator.cpp | 4 ++- src/generator/VariableInformation.cpp | 36 +++++++++++++++--------- 2 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index bc166cba3..10053d777 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,17 +178,19 @@ namespace storm { std::shared_ptr model = solver->getModel(); for (auto const& booleanVariable : this->variableInformation.booleanVariables) { bool variableValue = model->getBooleanValue(booleanVariable.variable); + std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.set(booleanVariable.bitOffset, variableValue); } for (auto const& integerVariable : this->variableInformation.integerVariables) { int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); + std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); } - + // Gather iterators to the initial locations of all the automata. std::vector::const_iterator> initialLocationsIterators; uint64_t currentLocationVariable = 0; diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index c1a00e4e6..3545f1e49 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -63,15 +63,19 @@ namespace storm { } for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); + ++totalBitOffset; + } } for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); + totalBitOffset += bitwidth; + } } for (auto const& automaton : model.getAutomata()) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); @@ -79,15 +83,19 @@ namespace storm { totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; + } } for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + } } } From 91e6bb299923773a89fcb9ea649465f7a9283c7c Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 15:14:47 +0200 Subject: [PATCH 2/9] fixed bug in DD-based JANI model generation related to transient edge assignments Former-commit-id: b2cf168189706f22201bf54c00cd0f822acbbd14 [formerly 0c50ca2d16cc56b2c1a12db38b6736d79e6780c7] Former-commit-id: 05686fd6f1b6198355e31940b5b764998047810a --- src/builder/DdJaniModelBuilder.cpp | 8 +++++--- src/generator/JaniNextStateGenerator.cpp | 2 -- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 8b54e0eba..1b759cfc5 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -895,7 +895,6 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second); - actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot"); } else { transitions *= action.transitions; } @@ -1107,7 +1106,8 @@ namespace storm { } // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; + storm::dd::Add sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard; + transitions *= sourceLocationAndGuard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeDestination.empty()) { @@ -1124,7 +1124,9 @@ namespace storm { // Finally treat the transient assignments. std::map> transientEdgeAssignments; if (!this->transientVariables.empty()) { - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } ); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) { + transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + } ); } return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 10053d777..b2c786b77 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,14 +178,12 @@ namespace storm { std::shared_ptr model = solver->getModel(); for (auto const& booleanVariable : this->variableInformation.booleanVariables) { bool variableValue = model->getBooleanValue(booleanVariable.variable); - std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.set(booleanVariable.bitOffset, variableValue); } for (auto const& integerVariable : this->variableInformation.integerVariables) { int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); - std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(variableValue - integerVariable.lowerBound)); From ba0d81ca52172d4bd68fbf10c7a60a3714dc29d2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 12 Oct 2016 21:13:09 +0200 Subject: [PATCH 3/9] bugfix for PRISM program: only check initial values of variables if they have one Former-commit-id: c5c548bd62f28b1d2cdc70bb75f7c84d12233c62 [formerly c27c72bd59e9f07a05cb8e9c5f56b65906ff7a2f] Former-commit-id: 97acb66693b15d0464a7dbc15c70a13c73f60f10 --- src/storage/prism/Module.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 095ac3e11..0a4347396 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -196,12 +196,12 @@ namespace storm { bool Module::containsVariablesOnlyInUpdateProbabilities(std::set const& undefinedConstantVariables) const { for (auto const& booleanVariable : this->getBooleanVariables()) { - if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } } for (auto const& integerVariable : this->getIntegerVariables()) { - if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { From aee1956950574f7eec41df0c4fde4ce6fa11b9ee Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 15:03:57 +0200 Subject: [PATCH 4/9] 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; From 6a80319c183a9825cb89960ca2bf8603e029de3f Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 15:32:32 +0200 Subject: [PATCH 5/9] another Hwloc script Former-commit-id: cc5efdeb857264fd4c3351dd09063b763e36b623 [formerly 295c0c994ed500e72c1471c288fc22c4ca660ac4] Former-commit-id: fcaf78b967628407d13274a689861d02200259e9 --- resources/cmake/find_modules/FindHwloc.cmake | 206 ++++--------------- 1 file changed, 41 insertions(+), 165 deletions(-) diff --git a/resources/cmake/find_modules/FindHwloc.cmake b/resources/cmake/find_modules/FindHwloc.cmake index d1b5b488e..1db759375 100644 --- a/resources/cmake/find_modules/FindHwloc.cmake +++ b/resources/cmake/find_modules/FindHwloc.cmake @@ -1,179 +1,55 @@ -# FindHwloc -# ---------- +# Try to find hwloc libraries and headers. # -# Try to find Portable Hardware Locality (hwloc) libraries. -# http://www.open-mpi.org/software/hwloc +# Usage of this module: # -# You may declare HWLOC_ROOT environment variable to tell where -# your hwloc library is installed. +# find_package(hwloc) # -# Once done this will define:: +# Variables defined by this module: # -# Hwloc_FOUND - True if hwloc was found -# Hwloc_INCLUDE_DIRS - include directories for hwloc -# Hwloc_LIBRARIES - link against these libraries to use hwloc -# Hwloc_VERSION - version -# Hwloc_CFLAGS - include directories as compiler flags -# Hwloc_LDLFAGS - link paths and libs as compiler flags -# - -#============================================================================= -# Copyright 2014 Mikael Lepistö -# -# Distributed under the OSI-approved BSD License (the "License"); -# -# This software is distributed WITHOUT ANY WARRANTY; without even the -# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. -# See the License for more information. -#============================================================================= - -if(WIN32) - find_path(Hwloc_INCLUDE_DIR - NAMES - hwloc.h - PATHS - ENV "PROGRAMFILES(X86)" - ENV HWLOC_ROOT - PATH_SUFFIXES - include - ) - - find_library(Hwloc_LIBRARY - NAMES - libhwloc.lib - PATHS - ENV "PROGRAMFILES(X86)" - ENV HWLOC_ROOT - PATH_SUFFIXES - lib - ) - - # - # Check if the found library can be used to linking - # - SET (_TEST_SOURCE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/linktest.c") - FILE (WRITE "${_TEST_SOURCE}" - " - #include - int main() - { - hwloc_topology_t topology; - int nbcores; - hwloc_topology_init(&topology); - hwloc_topology_load(topology); - nbcores = hwloc_get_nbobjs_by_type(topology, HWLOC_OBJ_CORE); - hwloc_topology_destroy(topology); - return 0; - } - " - ) - - TRY_COMPILE(_LINK_SUCCESS ${CMAKE_BINARY_DIR} "${_TEST_SOURCE}" - CMAKE_FLAGS - "-DINCLUDE_DIRECTORIES:STRING=${Hwloc_INCLUDE_DIR}" - CMAKE_FLAGS - "-DLINK_LIBRARIES:STRING=${Hwloc_LIBRARY}" - ) - - IF(NOT _LINK_SUCCESS) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - message(STATUS "You are building 64bit target.") - ELSE() - message(STATUS "You are building 32bit code. If you like to build x64 use e.g. -G 'Visual Studio 12 Win64' generator." ) - ENDIF() - message(FATAL_ERROR "Library found, but linking test program failed.") - ENDIF() - - # - # Resolve version if some compiled binary found... - # - find_program(HWLOC_INFO_EXECUTABLE - NAMES - hwloc-info - PATHS - ENV HWLOC_ROOT - PATH_SUFFIXES - bin - ) - - if(HWLOC_INFO_EXECUTABLE) - execute_process( - COMMAND ${HWLOC_INFO_EXECUTABLE} "--version" - OUTPUT_VARIABLE HWLOC_VERSION_LINE - OUTPUT_STRIP_TRAILING_WHITESPACE - ) - string(REGEX MATCH "([0-9]+.[0-9]+)$" - Hwloc_VERSION "${HWLOC_VERSION_LINE}") - unset(HWLOC_VERSION_LINE) - endif() - - # - # All good - # - - set(Hwloc_LIBRARIES ${Hwloc_LIBRARY}) - set(Hwloc_INCLUDE_DIRS ${Hwloc_INCLUDE_DIR}) - - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args( - Hwloc - FOUND_VAR Hwloc_FOUND - REQUIRED_VARS Hwloc_LIBRARY Hwloc_INCLUDE_DIR - VERSION_VAR Hwloc_VERSION) - - mark_as_advanced( - Hwloc_INCLUDE_DIR - Hwloc_LIBRARY) - - foreach(arg ${Hwloc_INCLUDE_DIRS}) - set(Hwloc_CFLAGS "${Hwloc_CFLAGS} /I${arg}") - endforeach() +# HWLOC_FOUND System has hwloc libraries and headers +# HWLOC_LIBRARIES The hwloc library +# HWLOC_INCLUDE_DIRS The location of HWLOC headers - set(Hwloc_LDFLAGS "${Hwloc_LIBRARY}") +find_path( + HWLOC_PREFIX + NAMES include/hwloc.h +) -else() +if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "") + set(HWLOC_PREFIX $ENV{HWLOC_BASE}) +endif() - # Find with pkgconfig - find_package(PkgConfig) +message(STATUS "Searching for hwloc library in path " ${HWLOC_PREFIX}) - if(HWLOC_ROOT) - set(ENV{PKG_CONFIG_PATH} "${HWLOC_ROOT}/lib/pkgconfig") - else() - foreach(PREFIX ${CMAKE_PREFIX_PATH}) - set(PKG_CONFIG_PATH "${PKG_CONFIG_PATH}:${PREFIX}/lib/pkgconfig") - endforeach() - set(ENV{PKG_CONFIG_PATH} "${PKG_CONFIG_PATH}:$ENV{PKG_CONFIG_PATH}") - endif() +find_library( + HWLOC_LIBRARIES + NAMES hwloc + HINTS ${HWLOC_PREFIX}/lib +) - if(hwloc_FIND_REQUIRED) - set(_hwloc_OPTS "REQUIRED") - elseif(hwloc_FIND_QUIETLY) - set(_hwloc_OPTS "QUIET") - else() - set(_hwloc_output 1) - endif() +find_path( + HWLOC_INCLUDE_DIRS + NAMES hwloc.h + HINTS ${HWLOC_PREFIX}/include +) - if(hwloc_FIND_VERSION) - if(hwloc_FIND_VERSION_EXACT) - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc=${hwloc_FIND_VERSION}) - else() - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc>=${hwloc_FIND_VERSION}) - endif() - else() - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc) - endif() +include(FindPackageHandleStandardArgs) - if(Hwloc_FOUND) - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(Hwloc DEFAULT_MSG Hwloc_LIBRARIES) +find_package_handle_standard_args( + HWLOC DEFAULT_MSG + HWLOC_LIBRARIES + HWLOC_INCLUDE_DIRS +) - if(NOT ${Hwloc_VERSION} VERSION_LESS 1.7.0) - set(Hwloc_GL_FOUND 1) - endif() +mark_as_advanced( + HWLOC_LIBRARIES + HWLOC_INCLUDE_DIRS +) - if(_hwloc_output) - message(STATUS - "Found hwloc ${Hwloc_VERSION} in ${Hwloc_INCLUDE_DIRS}:${Hwloc_LIBRARIES}") - endif() +if (HWLOC_FOUND) + if (NOT $ENV{HWLOC_LIB} STREQUAL "") +# set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}") endif() -endif() + message(STATUS "hwloc includes: " ${HWLOC_INCLUDE_DIRS}) + message(STATUS "hwloc libraries: " ${HWLOC_LIBRARIES}) +endif() \ No newline at end of file From ccfcbc0c69fc1349d2940e956d62039f698897e9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Oct 2016 15:37:26 +0200 Subject: [PATCH 6/9] fixed hwloc issue even harder Former-commit-id: 5768663ab4880968d5562114aedea295ea2ec8a9 [formerly 47af70ccf358cd6c066f89ddb3229b1528963c8e] Former-commit-id: ef788dbb6af6a7f6855d5798d964ef13cdec1752 --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 244e24057..dcc98e937 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -330,7 +330,7 @@ add_dependencies(resources sylvan) if(${OPERATING_SYSTEM} MATCHES "Linux") find_package(Hwloc QUIET REQUIRED) - if(Hwloc_FOUND) + if(HWLOC_FOUND) message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) else() From 744216d5d2c2ae77a681dca3b5df23e0196888fd Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 13 Oct 2016 18:39:28 +0200 Subject: [PATCH 7/9] 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; }; } } From 3626c044d39dabc5953e9a0a8e0291693fa18a3d Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 15 Oct 2016 00:50:11 +0200 Subject: [PATCH 8/9] several improvements towards jani-property support Former-commit-id: 3d56f22d99f3e051cc68dd08159761bea257e576 [formerly 1f527643abbb4e0bad9b609dc0f9835e7db51035] Former-commit-id: 75e40a9b69709b86cfe88a61c2c03554f4664718 --- src/parser/JaniParser.cpp | 173 ++++++++++++++++-- src/parser/JaniParser.h | 20 +- src/storage/jani/BooleanVariable.cpp | 5 +- src/storage/jani/BooleanVariable.h | 2 +- src/storage/jani/BoundedIntegerVariable.cpp | 9 +- src/storage/jani/BoundedIntegerVariable.h | 4 - src/storage/jani/JSONExporter.cpp | 7 +- src/storage/jani/Property.h | 1 + src/storage/jani/RealVariable.cpp | 2 +- src/storage/jani/RealVariable.h | 2 +- src/storage/jani/UnboundedIntegerVariable.cpp | 2 +- src/storage/jani/Variable.cpp | 2 +- src/storage/jani/Variable.h | 2 +- src/storage/prism/ToJaniConverter.cpp | 6 +- src/utility/storm.cpp | 4 +- src/utility/storm.h | 2 +- 16 files changed, 189 insertions(+), 54 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 97fc467e5..bc094f197 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -5,6 +5,8 @@ #include "src/storage/jani/ParallelComposition.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/InvalidJaniException.h" + +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/NotImplementedException.h" #include "src/storage/jani/ModelType.h" @@ -49,7 +51,7 @@ namespace storm { } - std::pair> JaniParser::parse(std::string const& path) { + std::pair> JaniParser::parse(std::string const& path) { JaniParser parser; parser.readFile(path); return parser.parseModel(); @@ -75,7 +77,7 @@ namespace storm { file.close(); } - std::pair> JaniParser::parseModel(bool parseProperties) { + std::pair> JaniParser::parseModel(bool parseProperties) { //jani-version STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version"); @@ -121,17 +123,87 @@ namespace storm { std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); - PropertyVector properties; + std::map properties; if (parseProperties && parsedStructure.count("properties") == 1) { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { - properties.push_back(this->parseProperty(propertyEntry)); + try { + auto prop = this->parseProperty(propertyEntry); + properties.emplace(prop.getName(), prop); + } catch (storm::exceptions::NotSupportedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } catch (storm::exceptions::NotImplementedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } } } return {model, properties}; } + + std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("exp"), "Operand of operator " + opstring) }; + } + + + std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); + STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; + } + + + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, std::string const& context) { + storm::expressions::Expression expr = parseExpression(propertyStructure, "Expression in property", {}, true); + if(expr.isInitialized()) { + return std::make_shared(expr); + } else if(propertyStructure.count("op") == 1) { + std::string opString = getString(propertyStructure.at("op"), "Operation description"); + + if(opString == "Pmin" || opString == "Pmax") { + std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + assert(args.size() == 1); + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + return std::make_shared(args[0], opInfo); + + } else if (opString == "∀" || opString == "∃") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); + } else if (opString == "Emin" || opString == "Emax") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Emin and Emax are currently not supported"); + } else if (opString == "Smin" || opString == "Smax") { + std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); + } else if (opString == "U") { + std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + if (propertyStructure.count("step-bounds") > 0) { + + } else if (propertyStructure.count("time-bounds") > 0) { + + } else if (propertyStructure.count("reward-bounds") > 0 ) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); + } + return std::make_shared(args[0], args[1]); + } else if (opString == "W") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); + } else if (opString == "∧" || opString == "∨") { + std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + assert(args.size() == 2); + storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; + return std::make_shared(oper, args[0], args[1]); + } else if (opString == "¬") { + std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + assert(args.size() == 1); + return std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + + } + + } + + } + storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); // TODO check unique name @@ -140,8 +212,46 @@ namespace storm { if (propertyStructure.count("comment") > 0) { comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'."); } + STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression"); + // Parse filter expression. + json const& expressionStructure = propertyStructure.at("expression"); - + STORM_LOG_THROW(expressionStructure.count("op") == 1, storm::exceptions::InvalidJaniException, "Expression in property must have an operation description"); + STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); + STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); + std::string funDescr = getString(expressionStructure.at("fun"), "Filter function in property named " + name); + storm::jani::FilterType ft; + if (funDescr == "min") { + ft = storm::jani::FilterType::MIN; + } else if (funDescr == "max") { + ft = storm::jani::FilterType::MAX; + } else if (funDescr == "sum") { + ft = storm::jani::FilterType::SUM; + } else if (funDescr == "avg") { + ft = storm::jani::FilterType::AVG; + } else if (funDescr == "count") { + ft = storm::jani::FilterType::COUNT; + } else if (funDescr == "∀") { + ft = storm::jani::FilterType::FORALL; + } else if (funDescr == "∃") { + ft = storm::jani::FilterType::EXISTS; + } else if (funDescr == "argmin") { + ft = storm::jani::FilterType::ARGMIN; + } else if (funDescr == "argmax") { + ft = storm::jani::FilterType::ARGMAX; + } else if (funDescr == "values") { + ft = storm::jani::FilterType::VALUES; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); + } + + STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); + STORM_LOG_THROW(expressionStructure.at("states").is_string(), storm::exceptions::NotImplementedException, "We only support properties where the filter has a non-complex description of the states"); + std::string statesDescr = getString(expressionStructure.at("states"), "Filtered states in property named " + name); + STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); + STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); + auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); + return storm::jani::Property(name, formula, comment); } std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { @@ -236,7 +346,6 @@ namespace storm { boost::optional initVal; if(variableStructure.at("type").is_string()) { if(variableStructure.at("type") == "real") { - expressionManager->declareRationalVariable(name); if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->rational(defaultRationalInitialValue); @@ -247,7 +356,8 @@ namespace storm { return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName)); } else if(variableStructure.at("type") == "bool") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -258,7 +368,8 @@ namespace storm { } return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName)); } else if(variableStructure.at("type") == "int") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -323,14 +434,14 @@ namespace storm { STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << "."); } - std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator); return {left}; } - std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); return {left, right}; } /** @@ -366,7 +477,7 @@ namespace storm { } } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { if(expressionStructure.is_boolean()) { if(expressionStructure.get()) { return expressionManager->boolean(true); @@ -389,31 +500,50 @@ namespace storm { if(expressionStructure.count("op") == 1) { std::string opstring = getString(expressionStructure.at("op"), scopeDescription); std::vector arguments = {}; - if(opstring == "?:") { + if(opstring == "ite") { + STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required"); + STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription)); ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription); assert(arguments.size() == 3); + ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[0], opstring, 1, scopeDescription); + ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); + if(!arguments[0].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return !arguments[0]; } else if (opstring == "=") { @@ -558,6 +688,9 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm"); } else { + if(returnNoneInitializedOnUnknownOperator) { + return storm::expressions::Expression(); + } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scopeDescription << "."); } } diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 8fa4e8277..1e87efe04 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -33,16 +33,16 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); - static std::pair parse(std::string const& path); + static std::pair> parse(std::string const& path); protected: void readFile(std::string const& path); - std::pair parseModel(bool parseProperties = true); + std::pair> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel); std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>()); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); private: std::shared_ptr parseConstant(json const& constantStructure, std::string const& scopeDescription = "global"); @@ -51,13 +51,19 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); - std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); - + std::shared_ptr parseFormula(json const& propertyStructure, std::string const& context); + std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + + std::vector> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); + std::vector> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); + + + std::shared_ptr parseComposition(json const& compositionStructure); storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); - + /** * The overall structure currently under inspection. */ diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp index 3eb63780b..ca2934f93 100644 --- a/src/storage/jani/BooleanVariable.cpp +++ b/src/storage/jani/BooleanVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { // Intentionally left empty. } @@ -19,7 +19,8 @@ namespace storm { if (initValue) { return std::make_shared(name, variable, initValue.get(), transient); } else { - return std::make_shared(name, variable, transient); + assert(!transient); + return std::make_shared(name, variable); } } diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 7fe9603e0..7eeea85fd 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -11,7 +11,7 @@ namespace storm { /*! * Creates a Boolean variable with initial value */ - BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a Boolean variable with initial value diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index 37b458ba4..1d04c8166 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -13,11 +13,7 @@ namespace storm { // Intentionally left empty. } - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable, transient), lowerBound(lowerBound), upperBound(upperBound) { - // Intentionally left empty. - } - - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { // Intentionally left empty. } @@ -56,7 +52,8 @@ namespace storm { if (initValue) { return std::make_shared(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get()); } else { - return std::make_shared(name, variable, transient, lowerBound.get(), upperBound.get()); + assert(!transient); + return std::make_shared(name, variable, lowerBound.get(), upperBound.get()); } } } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 733024b3d..9b5350d0e 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -16,10 +16,6 @@ namespace storm { * Creates a bounded integer variable with transient set to false and an initial value. */ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); - /*! - * Creates a bounded integer variable without initial value. - */ - BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); /*! * Creates a bounded integer variable with transient set to false and no initial value. */ diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index e6c1e9d60..2eefbb774 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -140,7 +140,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { - modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + modernjson::json opDecl(f.getLabel()); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ @@ -152,7 +152,7 @@ namespace storm { return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { - modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + modernjson::json opDecl(f.isTrueFormula() ? true : false); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { @@ -173,7 +173,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { - + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { @@ -718,6 +718,7 @@ namespace storm { modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { modernjson::json propDecl; propDecl["states"] = "initial"; + propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); return propDecl; diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index bde51865e..be35820a4 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -31,6 +31,7 @@ namespace storm { class Property { + public: /** * Constructs the property * @param name the name diff --git a/src/storage/jani/RealVariable.cpp b/src/storage/jani/RealVariable.cpp index 8880a9a0a..f06e87a5c 100644 --- a/src/storage/jani/RealVariable.cpp +++ b/src/storage/jani/RealVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : storm::jani::Variable(name, variable, transient) { + RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable) : storm::jani::Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/RealVariable.h b/src/storage/jani/RealVariable.h index 74c337ed9..1783b6fbf 100644 --- a/src/storage/jani/RealVariable.h +++ b/src/storage/jani/RealVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates a real variable without initial value. */ - RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + RealVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a real variable with initial value. diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp index c646b09b1..6b541054e 100644 --- a/src/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storage/jani/UnboundedIntegerVariable.cpp @@ -7,7 +7,7 @@ namespace storm { // Intentionally left empty. } - UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 8551f14df..f2c7217ff 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -12,7 +12,7 @@ namespace storm { // Intentionally left empty. } - Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient), init() { + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable), transient(false), init() { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index cbbe4aa69..2eea79679 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -25,7 +25,7 @@ namespace storm { /*! * Creates a new variable without initial value construct. */ - Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false); + Variable(std::string const& name, storm::expressions::Variable const& variable); virtual ~Variable(); diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 65289382a..e3bc3c569 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -47,7 +47,7 @@ namespace storm { storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -56,7 +56,7 @@ namespace storm { storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false)); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false)); + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -100,7 +100,7 @@ namespace storm { std::vector transientLocationAssignments; for (auto const& rewardModel : program.getRewardModels()) { auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName()); - storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName(), newExpressionVariable, true)); + storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "defaultReward" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true)); if (rewardModel.hasStateRewards()) { storm::expressions::Expression transientLocationExpression; diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index d4fb44290..5e1b8104e 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -15,8 +15,8 @@ namespace storm { return program; } - std::pair> parseJaniModel(std::string const& path) { - std::pair> modelAndFormulae = storm::parser::JaniParser::parse(path); + std::pair> parseJaniModel(std::string const& path) { + std::pair> modelAndFormulae = storm::parser::JaniParser::parse(path); modelAndFormulae.first.checkValid(); return modelAndFormulae; } diff --git a/src/utility/storm.h b/src/utility/storm.h index c5df89d64..336d6e399 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -100,7 +100,7 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } - std::pair> parseJaniModel(std::string const& path); + std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program); From ed970d78b1f6cd0005a2e758446e5975c949e054 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 16 Oct 2016 12:32:30 +0200 Subject: [PATCH 9/9] property support for jani -- several changes throughout code, parser currently only supports probability properties Former-commit-id: d5db0cda02b446032ba8e5f0ee883e5b4b80fbc7 [formerly 66d55d7e43ac62517e897f3bac4e8d9c51a471e5] Former-commit-id: 1672b21b127acf4a5f70fa4793d4bfa6776a8784 --- src/cli/cli.cpp | 45 ++++-- src/cli/entrypoints.h | 144 ++++++++++++----- .../ExplicitQualitativeCheckResult.cpp | 41 +++++ .../results/ExplicitQualitativeCheckResult.h | 6 + .../ExplicitQuantitativeCheckResult.cpp | 59 +++++++ .../results/ExplicitQuantitativeCheckResult.h | 6 + src/modelchecker/results/FilterType.cpp | 32 ++++ src/modelchecker/results/FilterType.h | 14 ++ .../results/HybridQuantitativeCheckResult.cpp | 14 ++ .../results/HybridQuantitativeCheckResult.h | 9 +- .../results/QualitativeCheckResult.h | 4 + .../results/QuantitativeCheckResult.h | 12 +- .../SymbolicQualitativeCheckResult.cpp | 17 ++ .../results/SymbolicQualitativeCheckResult.h | 6 + .../SymbolicQuantitativeCheckResult.cpp | 12 ++ .../results/SymbolicQuantitativeCheckResult.h | 7 +- src/parser/CSVParser.cpp | 23 +++ src/parser/CSVParser.h | 12 ++ src/parser/JaniParser.cpp | 148 +++++++++++++++--- src/parser/JaniParser.h | 9 +- src/parser/KeyValueParser.cpp | 26 +++ src/parser/KeyValueParser.h | 7 + src/settings/modules/IOSettings.cpp | 14 ++ src/settings/modules/IOSettings.h | 6 + src/storage/jani/JSONExporter.cpp | 42 ++--- src/storage/jani/JSONExporter.h | 5 +- src/storage/jani/Property.cpp | 23 ++- src/storage/jani/Property.h | 44 +++++- src/utility/constants.cpp | 95 +++++++++++ src/utility/constants.h | 15 ++ src/utility/storm.cpp | 11 +- src/utility/storm.h | 1 + 32 files changed, 792 insertions(+), 117 deletions(-) create mode 100644 src/modelchecker/results/FilterType.cpp create mode 100644 src/modelchecker/results/FilterType.h create mode 100644 src/parser/CSVParser.cpp create mode 100644 src/parser/CSVParser.h create mode 100644 src/parser/KeyValueParser.cpp create mode 100644 src/parser/KeyValueParser.h diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index db9829084..a1b20b546 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -213,22 +213,38 @@ namespace storm { auto ioSettings = storm::settings::getModule(); if (ioSettings.isPrismOrJaniInputSet()) { storm::storage::SymbolicModelDescription model; + std::vector properties; + if (ioSettings.isPrismInputSet()) { model = storm::parseProgram(ioSettings.getPrismInputFilename()); if (ioSettings.isPrismToJaniSet()) { model = model.toJani(true); } } else if (ioSettings.isJaniInputSet()) { - model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; + auto input = storm::parseJaniModel(ioSettings.getJaniInputFilename()); + model = input.first; + if (ioSettings.isJaniPropertiesSet()) { + for (auto const& propName : ioSettings.getJaniProperties()) { + STORM_LOG_THROW( input.second.count(propName) == 1, storm::exceptions::InvalidArgumentException, "No property with name " << propName << " known."); + properties.push_back(input.second.at(propName)); + } + } + } // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. - std::vector> formulas; + uint64_t i = 0; if (storm::settings::getModule().isPropertySet()) { if (model.isJaniModel()) { - formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); + for(auto const& formula : storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } } else { - formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); + for(auto const& formula :storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } } } @@ -236,9 +252,9 @@ namespace storm { if (storm::settings::getModule().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), storm::settings::getModule().getJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(model.asJaniModel(), formulasInProperties(properties), storm::settings::getModule().getJaniFilename()); } } @@ -250,30 +266,35 @@ namespace storm { if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel(model, formulas, true); + buildAndCheckSymbolicModel(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); #endif } else if (storm::settings::getModule().isExactSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel(model, formulas, true); + buildAndCheckSymbolicModel(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif } else { - buildAndCheckSymbolicModel(model, formulas, true); + buildAndCheckSymbolicModel(model, properties, true); } } else if (storm::settings::getModule().isExplicitSet()) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input."); // If the model is given in an explicit format, we parse the properties without allowing expressions // in formulas. - std::vector> formulas; + std::vector properties; if (storm::settings::getModule().isPropertySet()) { - formulas = storm::parseFormulasForExplicit(storm::settings::getModule().getProperty()); + uint64_t i = 0; + for(auto const& formula : storm::parseFormulasForExplicit(storm::settings::getModule().getProperty())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + + } } - buildAndCheckExplicitModel(formulas, true); + buildAndCheckExplicitModel(properties, true); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f4b009b7e..3d933038a 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -12,15 +12,72 @@ namespace storm { namespace cli { template - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + void applyFilterFunctionAndOutput(std::unique_ptr const& result, storm::modelchecker::FilterType ft) { + + if(result->isQuantitative()) { + switch(ft) { + case storm::modelchecker::FilterType::VALUES: + std::cout << *result << std::endl; + return; + case storm::modelchecker::FilterType::SUM: + std::cout << result->asQuantitativeCheckResult().sum(); + return; + case storm::modelchecker::FilterType::AVG: + std::cout << result->asQuantitativeCheckResult().average(); + return; + case storm::modelchecker::FilterType::MIN: + std::cout << result->asQuantitativeCheckResult().getMin(); + return; + case storm::modelchecker::FilterType::MAX: + std::cout << result->asQuantitativeCheckResult().getMax(); + return; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Outputting states is not supported"); + case storm::modelchecker::FilterType::EXISTS: + case storm::modelchecker::FilterType::FORALL: + case storm::modelchecker::FilterType::COUNT: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for qualitative results"); + } + } else { + switch(ft) { + case storm::modelchecker::FilterType::VALUES: + std::cout << *result << std::endl; + return; + case storm::modelchecker::FilterType::EXISTS: + std::cout << result->asQualitativeCheckResult().existsTrue(); + return; + case storm::modelchecker::FilterType::FORALL: + std::cout << result->asQualitativeCheckResult().forallTrue(); + return; + case storm::modelchecker::FilterType::COUNT: + std::cout << result->asQualitativeCheckResult().count(); + return; + + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Outputting states is not supported"); + case storm::modelchecker::FilterType::SUM: + case storm::modelchecker::FilterType::AVG: + case storm::modelchecker::FilterType::MIN: + case storm::modelchecker::FilterType::MAX: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for quantitative results"); + } + + } + } + + template + void verifySparseModel(std::shared_ptr> model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { + for (auto const& property : properties) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -29,17 +86,18 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + inline void verifySparseModel(std::shared_ptr> model, std::vector const& properties, bool onlyInitialStatesRelevant) { - for (auto const& formula : formulas) { + for (auto const& property : properties) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs."); - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -52,24 +110,24 @@ namespace storm { #endif template - void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template - void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidSettingsException, "Exploration engine is currently only applicable to PRISM models."); storm::prism::Program const& program = model.asPrismProgram(); STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs."); - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; bool supportFormula; std::unique_ptr result; if(program.getModelType() == storm::prism::Program::ModelType::DTMC) { storm::modelchecker::SparseExplorationModelChecker> checker(program); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); supportFormula = checker.canHandle(task); if (supportFormula) { @@ -77,7 +135,7 @@ namespace storm { } } else if(program.getModelType() == storm::prism::Program::ModelType::MDP) { storm::modelchecker::SparseExplorationModelChecker> checker(program); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); supportFormula = checker.canHandle(task); if (supportFormula) { @@ -94,7 +152,8 @@ namespace storm { if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -103,22 +162,23 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -126,15 +186,16 @@ namespace storm { } template - void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -182,23 +243,24 @@ namespace storm { } template - void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { // Start by building the model. - auto markovModel = buildSymbolicModel(model, formulas); + auto markovModel = buildSymbolicModel(model, formulasInProperties(properties)); // Print some information about the model. markovModel->printModelInformationToStream(std::cout); // Then select the correct engine. if (hybrid) { - verifySymbolicModelWithHybridEngine(markovModel, formulas, onlyInitialStatesRelevant); + verifySymbolicModelWithHybridEngine(markovModel, properties, onlyInitialStatesRelevant); } else { - verifySymbolicModelWithDdEngine(markovModel, formulas, onlyInitialStatesRelevant); + verifySymbolicModelWithDdEngine(markovModel, properties, onlyInitialStatesRelevant); } } template - void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { + auto formulas = formulasInProperties(properties); // Start by building the model. std::shared_ptr markovModel = buildSparseModel(model, formulas); @@ -214,12 +276,12 @@ namespace storm { if (storm::settings::getModule().isCounterexampleSet()) { generateCounterexamples(model, sparseModel, formulas); } else { - verifySparseModel(sparseModel, formulas, onlyInitialStatesRelevant); + verifySparseModel(sparseModel, properties, onlyInitialStatesRelevant); } } template - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { auto ddlib = storm::settings::getModule().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { @@ -247,35 +309,35 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); } template<> - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); } #endif template - void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); + BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulasInProperties(properties)); // Print some information about the model. model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. - if (!formulas.empty()) { + if (!properties.empty()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel(model->as>(), formulas, onlyInitialStatesRelevant); + verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); } } } diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp index aa86846fa..f5488122c 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -70,6 +70,47 @@ namespace storm { return *this; } + + bool ExplicitQualitativeCheckResult::existsTrue() const { + if (this->isResultForAllStates()) { + return !boost::get(truthValues).empty(); + } else { + for (auto& element : boost::get(truthValues)) { + if(element.second) { + return true; + } + } + return false; + } + } + bool ExplicitQualitativeCheckResult::forallTrue() const { + if (this->isResultForAllStates()) { + return boost::get(truthValues).full(); + } else { + for (auto& element : boost::get(truthValues)) { + if(!element.second) { + return false; + } + } + return true; + } + } + + uint64_t ExplicitQualitativeCheckResult::count() const { + if (this->isResultForAllStates()) { + return boost::get(truthValues).getNumberOfSetBits(); + } else { + uint64_t result = 0; + for (auto& element : boost::get(truthValues)) { + if(element.second) { + ++result; + } + } + return result; + } + } + + bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const { if (this->isResultForAllStates()) { return boost::get(truthValues).get(state); diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h index 665675cfd..afb54b4be 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -47,6 +47,12 @@ namespace storm { vector_type const& getTruthValuesVector() const; map_type const& getTruthValuesVectorMap() const; + + virtual bool existsTrue() const override; + virtual bool forallTrue() const override; + virtual uint64_t count() const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 6233216d9..87ba9e0fa 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -3,6 +3,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/storage/BitVector.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/utility/vector.h" #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidAccessException.h" @@ -81,6 +82,64 @@ namespace storm { } } + template + ValueType ExplicitQuantitativeCheckResult::getMin() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + if (this->isResultForAllStates()) { + return storm::utility::minimum(boost::get(values)); + } else { + return storm::utility::minimum(boost::get(values)); + } + } + + + template + ValueType ExplicitQuantitativeCheckResult::getMax() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + if (this->isResultForAllStates()) { + return storm::utility::maximum(boost::get(values)); + } else { + return storm::utility::maximum(boost::get(values)); + } + } + + template + ValueType ExplicitQuantitativeCheckResult::sum() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get(values)) { + sum += element; + } + } else { + for (auto& element : boost::get(values)) { + sum += element.second; + } + } + return sum; + } + + template + ValueType ExplicitQuantitativeCheckResult::average() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get(values)) { + sum += element; + } + return sum / boost::get(values).size(); + } else { + for (auto& element : boost::get(values)) { + sum += element.second; + } + return sum / boost::get(values).size(); + } + } + template bool ExplicitQuantitativeCheckResult::hasScheduler() const { return static_cast(scheduler); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 639da4fa7..d2bb9f711 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -53,6 +53,12 @@ namespace storm { virtual void oneMinus() override; + + virtual ValueType getMin() const override; + virtual ValueType getMax() const override; + virtual ValueType average() const override; + virtual ValueType sum() const override; + bool hasScheduler() const; void setScheduler(std::unique_ptr&& scheduler); storm::storage::Scheduler const& getScheduler() const; diff --git a/src/modelchecker/results/FilterType.cpp b/src/modelchecker/results/FilterType.cpp new file mode 100644 index 000000000..3a15c8169 --- /dev/null +++ b/src/modelchecker/results/FilterType.cpp @@ -0,0 +1,32 @@ +#include "FilterType.h" + + +namespace storm { + namespace modelchecker { + + std::string toString(FilterType ft) { + switch(ft) { + case FilterType::ARGMAX: + return "the argmax"; + case FilterType::ARGMIN: + return "the argmin"; + case FilterType::AVG: + return "the average"; + case FilterType::COUNT: + return "the number of"; + case FilterType::EXISTS: + return "whether there exists a state in"; + case FilterType::FORALL: + return "whether for all states in"; + case FilterType::MAX: + return "the maximum"; + case FilterType::MIN: + return "the minumum"; + case FilterType::SUM: + return "the sum"; + case FilterType::VALUES: + return "the values"; + } + } + } +} \ No newline at end of file diff --git a/src/modelchecker/results/FilterType.h b/src/modelchecker/results/FilterType.h new file mode 100644 index 000000000..040b09084 --- /dev/null +++ b/src/modelchecker/results/FilterType.h @@ -0,0 +1,14 @@ +#pragma once +#include + +namespace storm { + namespace modelchecker { + + enum class StateFilter { ARGMIN, ARGMAX }; + + enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; + + std::string toString(FilterType); + bool isStateFilter(FilterType); + } +} \ No newline at end of file diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index a32095e40..62fe2c1dd 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -5,9 +5,12 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/exceptions/InvalidOperationException.h" + +#include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" #include "src/utility/constants.h" + namespace storm { namespace modelchecker { template @@ -164,6 +167,16 @@ namespace storm { return max; } + template + ValueType HybridQuantitativeCheckResult::sum() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for hybrid results"); + } + + template + ValueType HybridQuantitativeCheckResult::average() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for hybrid results"); + } + template void HybridQuantitativeCheckResult::oneMinus() { storm::dd::Add one = symbolicValues.getDdManager().template getAddOne(); @@ -175,6 +188,7 @@ namespace storm { } } + // Explicitly instantiate the class. template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 8b7db1cea..16a802331 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -46,9 +46,14 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; - virtual ValueType getMin() const; + virtual ValueType getMin() const override; - virtual ValueType getMax() const; + virtual ValueType getMax() const override; + + virtual ValueType sum() const override; + + virtual ValueType average() const override; + virtual void oneMinus() override; diff --git a/src/modelchecker/results/QualitativeCheckResult.h b/src/modelchecker/results/QualitativeCheckResult.h index 608e2c0d1..f4a89665b 100644 --- a/src/modelchecker/results/QualitativeCheckResult.h +++ b/src/modelchecker/results/QualitativeCheckResult.h @@ -12,6 +12,10 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other); virtual void complement(); + virtual bool existsTrue() const = 0; + virtual bool forallTrue() const = 0; + virtual uint64_t count() const = 0; + virtual bool isQualitative() const override; }; } diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index bb268ae3f..2e9abe6a9 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -1,5 +1,4 @@ -#ifndef STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ -#define STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ +#pragma once #include "src/modelchecker/results/CheckResult.h" @@ -14,9 +13,16 @@ namespace storm { virtual void oneMinus() = 0; + + virtual ValueType getMin() const = 0; + + virtual ValueType getMax() const = 0; + + virtual ValueType average() const = 0; + virtual ValueType sum() const = 0; + virtual bool isQuantitative() const override; }; } } -#endif /* STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 2275b942f..3468a13c9 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -3,6 +3,8 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/exceptions/NotImplementedException.h" + namespace storm { namespace modelchecker { template @@ -49,6 +51,21 @@ namespace storm { return truthValues; } + template + bool SymbolicQualitativeCheckResult::existsTrue() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Exists not implemented for symbolic results"); + } + + template + bool SymbolicQualitativeCheckResult::forallTrue() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall not implemented for symbolic results"); + } + + template + uint64_t SymbolicQualitativeCheckResult::count() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Count not implemented for symbolic results"); + } + template std::ostream& SymbolicQualitativeCheckResult::writeToStream(std::ostream& out) const { if (this->truthValues.isZero()) { diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 3e94f5ee8..775b8c467 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -30,6 +30,12 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override; virtual void complement() override; + + virtual bool existsTrue() const override; + virtual bool forallTrue() const override; + virtual uint64_t count() const override; + + storm::dd::Bdd const& getTruthValuesVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 57f68bdf1..bde1407a4 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -5,6 +5,8 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/exceptions/InvalidOperationException.h" + +#include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" #include "src/utility/constants.h" @@ -89,6 +91,16 @@ namespace storm { return this->values.getMax(); } + template + ValueType SymbolicQuantitativeCheckResult::average() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for symbolic results"); + } + + template + ValueType SymbolicQuantitativeCheckResult::sum() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for symbolic results"); + } + template void SymbolicQuantitativeCheckResult::oneMinus() { storm::dd::Add one = values.getDdManager().template getAddOne(); diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index fd03da786..36b0c4cce 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -35,9 +35,12 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; - virtual ValueType getMin() const; + virtual ValueType getMin() const override; - virtual ValueType getMax() const; + virtual ValueType getMax() const override; + + virtual ValueType average() const override; + virtual ValueType sum() const override; virtual void oneMinus() override; diff --git a/src/parser/CSVParser.cpp b/src/parser/CSVParser.cpp new file mode 100644 index 000000000..04e26a3fa --- /dev/null +++ b/src/parser/CSVParser.cpp @@ -0,0 +1,23 @@ +#include "src/parser/CSVParser.h" +#include + +#include +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace parser { + + std::vector parseCommaSeperatedValues(std::string const& input) { + std::vector values; + std::vector definitions; + boost::split(definitions, input, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + values.push_back(definition); + } + return values; + } + } +} \ No newline at end of file diff --git a/src/parser/CSVParser.h b/src/parser/CSVParser.h new file mode 100644 index 000000000..ec21f2e80 --- /dev/null +++ b/src/parser/CSVParser.h @@ -0,0 +1,12 @@ +#include +#include + +namespace storm { + namespace parser { + /** + * Given a string seperated by commas, returns the values. + */ + std::vector parseCommaSeperatedValues(std::string const& input); + + } +} \ No newline at end of file diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index bc094f197..b6fe64bc6 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -10,6 +10,7 @@ #include "src/exceptions/NotImplementedException.h" #include "src/storage/jani/ModelType.h" +#include "src/modelchecker/results/FilterType.h" #include #include @@ -153,11 +154,41 @@ namespace storm { return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; } - + storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure) { + storm::jani::PropertyInterval pi; + if (piStructure.count("lower") > 0) { + pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval"); + // TODO substitute constants. + STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds"); + + + } + if (piStructure.count("lower-exclusive") > 0) { + STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.lowerBoundStrict = piStructure.at("lower-exclusive"); + + } + if (piStructure.count("upper") > 0) { + pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval"); + // TODO substitute constants. + STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds"); + + } + if (piStructure.count("upper-exclusive") > 0) { + STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.lowerBoundStrict = piStructure.at("upper-exclusive"); + } + STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded"); + return pi; + + + } - std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, std::string const& context) { - storm::expressions::Expression expr = parseExpression(propertyStructure, "Expression in property", {}, true); + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, std::string const& context, boost::optional> bound) { + + storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); if(expr.isInitialized()) { + assert(bound == boost::none); return std::make_shared(expr); } else if(propertyStructure.count("op") == 1) { std::string opString = getString(propertyStructure.at("op"), "Operation description"); @@ -167,9 +198,11 @@ namespace storm { assert(args.size() == 1); storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + opInfo.bound = bound; return std::make_shared(args[0], opInfo); } else if (opString == "∀" || opString == "∃") { + assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); } else if (opString == "Emin" || opString == "Emax") { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Emin and Emax are currently not supported"); @@ -177,29 +210,84 @@ namespace storm { std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); } else if (opString == "U") { + assert(bound == boost::none); std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); if (propertyStructure.count("step-bounds") > 0) { - + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound"); + if(pi.hasLowerBound()) { + STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound"); + } + int64_t upperBound = pi.upperBound.evaluateAsInt(); + if(pi.upperBoundStrict) { + upperBound--; + } + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); + return std::make_shared(args[0], args[1], upperBound); } else if (propertyStructure.count("time-bounds") > 0) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + double upperBound = pi.upperBound.evaluateAsDouble(); + STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); + return std::make_shared(args[0], args[1], upperBound); } else if (propertyStructure.count("reward-bounds") > 0 ) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); } - return std::make_shared(args[0], args[1]); + if (args[0]->isTrueFormula()) { + return std::make_shared(args[1]); + } else { + return std::make_shared(args[0], args[1]); + } } else if (opString == "W") { + assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); } else if (opString == "∧" || opString == "∨") { + assert(bound == boost::none); std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared(oper, args[0], args[1]); } else if (opString == "¬") { + assert(bound == boost::none); std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); assert(args.size() == 1); return std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + } else if (opString == "≥" || opString == "≤" || opString == "<" || opString == ">") { + assert(bound == boost::none); + storm::logic::ComparisonType ct; + if(opString == "≥") { + ct = storm::logic::ComparisonType::GreaterEqual; + } else if (opString == "≤") { + ct = storm::logic::ComparisonType::LessEqual; + } else if (opString == "<") { + ct = storm::logic::ComparisonType::Less; + } else if (opString == ">") { + ct = storm::logic::ComparisonType::Greater; + } + if (propertyStructure.at("left").count("op") > 0 && (propertyStructure.at("left").at("op") == "Pmin" || propertyStructure.at("left").at("op") == "Pmax" || propertyStructure.at("left").at("op") == "Emin" || propertyStructure.at("left").at("op") == "Emax" || propertyStructure.at("left").at("op") == "Smin" || propertyStructure.at("left").at("op") == "Smax")) { + auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get()); + STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); + // TODO evaluate this expression directly as rational number + return parseFormula(propertyStructure.at("left"), "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); + } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { + auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get()); + STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); + // TODO evaluate this expression directly as rational number + return parseFormula(propertyStructure.at("right"), "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); + + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); } - } } @@ -220,38 +308,38 @@ namespace storm { STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); std::string funDescr = getString(expressionStructure.at("fun"), "Filter function in property named " + name); - storm::jani::FilterType ft; + storm::modelchecker::FilterType ft; if (funDescr == "min") { - ft = storm::jani::FilterType::MIN; + ft = storm::modelchecker::FilterType::MIN; } else if (funDescr == "max") { - ft = storm::jani::FilterType::MAX; + ft = storm::modelchecker::FilterType::MAX; } else if (funDescr == "sum") { - ft = storm::jani::FilterType::SUM; + ft = storm::modelchecker::FilterType::SUM; } else if (funDescr == "avg") { - ft = storm::jani::FilterType::AVG; + ft = storm::modelchecker::FilterType::AVG; } else if (funDescr == "count") { - ft = storm::jani::FilterType::COUNT; + ft = storm::modelchecker::FilterType::COUNT; } else if (funDescr == "∀") { - ft = storm::jani::FilterType::FORALL; + ft = storm::modelchecker::FilterType::FORALL; } else if (funDescr == "∃") { - ft = storm::jani::FilterType::EXISTS; + ft = storm::modelchecker::FilterType::EXISTS; } else if (funDescr == "argmin") { - ft = storm::jani::FilterType::ARGMIN; + ft = storm::modelchecker::FilterType::ARGMIN; } else if (funDescr == "argmax") { - ft = storm::jani::FilterType::ARGMAX; + ft = storm::modelchecker::FilterType::ARGMAX; } else if (funDescr == "values") { - ft = storm::jani::FilterType::VALUES; + ft = storm::modelchecker::FilterType::VALUES; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); } STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); - STORM_LOG_THROW(expressionStructure.at("states").is_string(), storm::exceptions::NotImplementedException, "We only support properties where the filter has a non-complex description of the states"); - std::string statesDescr = getString(expressionStructure.at("states"), "Filtered states in property named " + name); + STORM_LOG_THROW(expressionStructure.at("states").count("op") > 0, storm::exceptions::NotImplementedException, "We only support properties where the filter has initial states"); + std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); - return storm::jani::Property(name, formula, comment); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); } std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { @@ -567,26 +655,38 @@ namespace storm { return arguments[0] != arguments[1]; } } else if (opstring == "<") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] < arguments[1]; } else if (opstring == "≤") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] <= arguments[1]; } else if (opstring == ">") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] > arguments[1]; } else if (opstring == "≥") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] >= arguments[1]; diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 1e87efe04..df36cd43c 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -1,9 +1,11 @@ #pragma once #include -#include +#include "src/logic/Formula.h" +#include "src/logic/Bound.h" #include "src/exceptions/FileIoException.h" #include "src/storage/expressions/ExpressionManager.h" + // JSON parser #include "json.hpp" @@ -16,6 +18,7 @@ namespace storm { class Variable; class Composition; class Property; + class PropertyInterval; } @@ -51,13 +54,13 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::shared_ptr parseFormula(json const& propertyStructure, std::string const& context); + std::shared_ptr parseFormula(json const& propertyStructure, std::string const& context, boost::optional> bound = boost::none); std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); std::vector> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); - + storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure); std::shared_ptr parseComposition(json const& compositionStructure); diff --git a/src/parser/KeyValueParser.cpp b/src/parser/KeyValueParser.cpp new file mode 100644 index 000000000..a9ea96612 --- /dev/null +++ b/src/parser/KeyValueParser.cpp @@ -0,0 +1,26 @@ +#include "KeyValueParser.h" + +namespace storm { + namespace parser { + + std::unordered_map parseKeyValueString(std::string const& keyValueString) { + std::unordered_map keyValueMap; + std::vector definitions; + boost::split(definitions, keyValueString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + std::size_t positionOfAssignmentOperator = definition.find('='); + STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::InvalidArgumentException, "Illegal key value string: syntax error."); + + // Now extract the variable name and the value from the string. + std::string key = definition.substr(0, positionOfAssignmentOperator); + boost::trim(key); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + keyValueMap.emplace(key, value); + } + } + } +} \ No newline at end of file diff --git a/src/parser/KeyValueParser.h b/src/parser/KeyValueParser.h new file mode 100644 index 000000000..3e32bd3ed --- /dev/null +++ b/src/parser/KeyValueParser.h @@ -0,0 +1,7 @@ +#pragma once + +namespace storm { + namespace parser { + std::unordered_map parseKeyValueString(std::string const& keyValueString); + } +} \ No newline at end of file diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c174f1f51..b6cf57dd3 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" #include "src/exceptions/InvalidSettingsException.h" +#include "src/parser/CSVParser.h" namespace storm { namespace settings { @@ -29,6 +30,8 @@ namespace storm { const std::string IOSettings::constantsOptionShortName = "const"; const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + const std::string IOSettings::janiPropertyOptionName = "janiproperty"; + const std::string IOSettings::janiPropertyOptionShortName = "jprop"; IOSettings::IOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); @@ -57,6 +60,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); } bool IOSettings::isExportDotSet() const { @@ -153,6 +158,15 @@ namespace storm { return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); } + bool IOSettings::isJaniPropertiesSet() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); + } + + std::vector IOSettings::getJaniProperties() const { + return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); + } + + bool IOSettings::isPrismCompatibilityEnabled() const { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index ae6ce6831..5514af716 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -183,6 +183,10 @@ namespace storm { * @return The string that defines the constants of a symbolic model. */ std::string getConstantDefinitionString() const; + + bool isJaniPropertiesSet() const; + + std::vector getJaniProperties() const; /*! * Retrieves whether the PRISM compatibility mode was enabled. @@ -215,6 +219,8 @@ namespace storm { static const std::string constantsOptionShortName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; + static const std::string janiPropertyOptionName; + static const std::string janiPropertyOptionShortName; }; } // namespace modules diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 2eefbb774..f70a76c62 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -105,13 +105,17 @@ namespace storm { 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)); - } + numDecl = storm::utility::convertNumber(rn); +// if(carl::isOne(carl::getDenom(rn))) { +// numDecl = modernjson::json(carl::toString(carl::getNum(rn))); +// } else { +// numDecl["op"] = "/"; +// // TODO set json lib to work with arbitrary precision ints. +// assert(carl::toInt(carl::getNum(rn)) == carl::getNum(rn)); +// assert(carl::toInt(carl::getDenom(rn)) == carl::getDenom(rn)); +// numDecl["left"] = carl::toInt(carl::getNum(rn)); +// numDecl["right"] = carl::toInt(carl::getDenom(rn)); +// } return numDecl; } @@ -689,27 +693,27 @@ namespace storm { } - std::string janiFilterTypeString(storm::jani::FilterType const& ft) { + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { - case storm::jani::FilterType::MIN: + case storm::modelchecker::FilterType::MIN: return "min"; - case storm::jani::FilterType::MAX: + case storm::modelchecker::FilterType::MAX: return "max"; - case storm::jani::FilterType::SUM: + case storm::modelchecker::FilterType::SUM: return "sum"; - case storm::jani::FilterType::AVG: + case storm::modelchecker::FilterType::AVG: return "avg"; - case storm::jani::FilterType::COUNT: + case storm::modelchecker::FilterType::COUNT: return "count"; - case storm::jani::FilterType::EXISTS: + case storm::modelchecker::FilterType::EXISTS: return "∃"; - case storm::jani::FilterType::FORALL: + case storm::modelchecker::FilterType::FORALL: return "∀"; - case storm::jani::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMIN: return "argmin"; - case storm::jani::FilterType::ARGMAX: + case storm::modelchecker::FilterType::ARGMAX: return "argmax"; - case storm::jani::FilterType::VALUES: + case storm::modelchecker::FilterType::VALUES: return "values"; } @@ -717,7 +721,7 @@ namespace storm { modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { modernjson::json propDecl; - propDecl["states"] = "initial"; + propDecl["states"]["op"] = "initial"; propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 55895364d..2159c26c5 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -4,9 +4,12 @@ #include "src/storage/expressions/ExpressionVisitor.h" #include "src/logic/FormulaVisitor.h" #include "Model.h" +#include "src/adapters/NumberAdapter.h" // JSON parser #include "json.hpp" -namespace modernjson = nlohmann; +namespace modernjson { + using json = nlohmann::basic_json; +}; namespace storm { namespace jani { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 28981f313..3e4243a3d 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,10 +1,23 @@ #include "Property.h" namespace storm { namespace jani { + + + + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { + return os << "Obtain " << toString(fe.getFilterType()) << " the 'initial'-states with values described by '" << *fe.getFormula() << "'"; + } + Property::Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment) - : name(name), filterExpression(FilterExpression(formula)), comment(comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)) { + } + + Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment) + : name(name), comment(comment), filterExpression(fe) + { + } std::string const& Property::getName() const { @@ -15,6 +28,14 @@ namespace storm { return this->comment; } + FilterExpression const& Property::getFilter() const { + return this->filterExpression; + } + + std::ostream& operator<<(std::ostream& os, Property const& p) { + return os << "(" << p.getName() << ") : " << p.getFilter(); + } + } } \ No newline at end of file diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index be35820a4..95ae41092 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -1,33 +1,52 @@ #pragma once #include "src/logic/formulas.h" +#include "src/modelchecker/results/FilterType.h" namespace storm { namespace jani { - enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; - + /** + * Property intervals as per Jani Specification. + * Currently mainly used to help parsing. + */ + struct PropertyInterval { + storm::expressions::Expression lowerBound; + bool lowerBoundStrict = false; + storm::expressions::Expression upperBound; + bool upperBoundStrict = false; + + bool hasLowerBound() { + return lowerBound.isInitialized(); + } + + bool hasUpperBound() { + return upperBound.isInitialized(); + } + }; class FilterExpression { public: - explicit FilterExpression(std::shared_ptr formula) : values(formula) {} + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : values(formula), ft(ft) {} + std::shared_ptr const& getFormula() const { return values; } - FilterType getFilterType() const { + storm::modelchecker::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; + storm::modelchecker::FilterType ft; }; + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe); + class Property { @@ -39,6 +58,13 @@ namespace storm { * @param comment An optional comment */ Property(std::string const& name, std::shared_ptr const& formula, std::string const& comment = ""); + /** + * Constructs the property + * @param name the name + * @param formula the formula representation + * @param comment An optional comment + */ + Property(std::string const& name, FilterExpression const& fe, std::string const& comment = ""); /** * Get the provided name * @return the name @@ -50,13 +76,15 @@ namespace storm { */ std::string const& getComment() const; - - + FilterExpression const& getFilter() const; private: std::string name; std::string comment; FilterExpression filterExpression; }; + + + std::ostream& operator<<(std::ostream& os, Property const& p); } } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 6d954722a..d2542a2c2 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -5,7 +5,10 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/exceptions/InvalidArgumentException.h" + #include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" namespace storm { namespace utility { @@ -143,6 +146,80 @@ namespace storm { return std::fabs(number); } + template<> + storm::RationalFunction minimum(std::vector const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template + ValueType minimum(std::vector const& values) { + assert(!values.empty()); + ValueType min = values.front(); + for (auto const& vt : values) { + if (vt < min) { + min = vt; + } + } + return min; + } + + template<> + storm::RationalFunction maximum(std::vector const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template + ValueType maximum(std::vector const& values) { + assert(!values.empty()); + ValueType max = values.front(); + for (auto const& vt : values) { + if (vt > max) { + max = vt; + } + } + return max; + } + + template<> + storm::RationalFunction minimum(std::map const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template< typename K, typename ValueType> + ValueType minimum(std::map const& values) { + assert(!values.empty()); + ValueType min = values.begin()->second; + for (auto const& vt : values) { + if (vt.second < min) { + min = vt.second; + } + } + return min; + } + + template<> + storm::RationalFunction maximum(std::map const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template + ValueType maximum(std::map const& values) { + assert(!values.empty()); + ValueType max = values.begin()->second; + for (auto const& vt : values) { + if (vt.second > max) { + max = vt.second; + } + } + return max; + } + #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -317,6 +394,24 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + template double minimum(std::vector const&); + template double maximum(std::vector const&); + + template storm::RationalNumber minimum(std::vector const&); + template storm::RationalNumber maximum(std::vector const&); + + template storm::RationalFunction minimum(std::vector const&); + template storm::RationalFunction maximum(std::vector const&); + + template double minimum(std::map const&); + template double maximum(std::map const&); + + template storm::RationalNumber minimum(std::map const&); + template storm::RationalNumber maximum(std::map const&); + + template storm::RationalFunction minimum(std::map const&); + template storm::RationalFunction maximum(std::map const&); #ifdef STORM_HAVE_CARL // Instantiations for rational number. template bool isOne(storm::RationalNumber const& value); diff --git a/src/utility/constants.h b/src/utility/constants.h index 66edb9f46..04fdf71c1 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,6 +11,8 @@ #include #include +#include +#include namespace storm { @@ -45,6 +47,19 @@ namespace storm { template ValueType simplify(ValueType value); + template + ValueType minimum(std::vector const& values); + + template + ValueType maximum(std::vector const& values); + + template< typename K, typename ValueType> + ValueType minimum(std::map const& values); + + template + ValueType maximum(std::map const& values); + + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 5e1b8104e..700fe049e 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -7,7 +7,16 @@ #include "src/utility/macros.h" #include "src/storage/jani/Property.h" -namespace storm { +namespace storm{ + + std::vector> formulasInProperties(std::vector const& properties) { + + std::vector> formulas; + for (auto const& prop : properties) { + formulas.push_back(prop.getFilter().getFormula()); + } + return formulas; + } storm::prism::Program parseProgram(std::string const& path) { storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify(); diff --git a/src/utility/storm.h b/src/utility/storm.h index 336d6e399..c20f0661d 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -100,6 +100,7 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } + std::vector> formulasInProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector> parseFormulasForExplicit(std::string const& inputString);