From 890634ba77ca0df0257c513f2180ea1430b62f42 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 10 Aug 2016 10:52:20 +0200 Subject: [PATCH] initial value support (bounded integers only) Former-commit-id: 8930f3233eecc4e1d1a9e27c6cf8a29b7f1543a5 [formerly 1a0222dc3c4db59ae7548f9633ce6c869b6389c4] Former-commit-id: 9ccfff2190862e940fa975f3e6bb0150360f3de7 --- src/parser/JaniParser.cpp | 16 ++++++++++------ src/storage/expressions/Expression.cpp | 16 ++++++++++++++++ src/storage/expressions/Expression.h | 8 ++++++++ src/storage/jani/BoundedIntegerVariable.cpp | 20 ++++++++++++++++++++ src/storage/jani/BoundedIntegerVariable.h | 16 ++++++++++++++-- 5 files changed, 68 insertions(+), 8 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 8b261026e..10f530e9e 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -212,13 +212,9 @@ namespace storm { STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scopeDescription + ") "+ name + "' (scope: " + scopeDescription + ") "); } else { STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scopeDescription + ")"); - } - boost::optional initValue; - if(initvalcount == 1) { - } STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); - + boost::optional initVal; if(variableStructure.at("type").is_object()) { STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ") kind must be given"); std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scopeDescription + ") "); @@ -231,11 +227,19 @@ namespace storm { storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")"); assert(upperboundExpr.isInitialized()); STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given"); + if(initvalcount == 1) { + if(variableStructure.at("initial-value").is_null()) { + initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr); + // TODO as soon as we support half-open intervals, we have to change this. + } else { + initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + } + } std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); if(basictype == "int") { STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar, lowerboundExpr, upperboundExpr); + return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); } diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index d3121032c..4836ea670 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -256,6 +256,22 @@ namespace storm { assertSameManager(first.getBaseExpression(), second.getBaseExpression()); return Expression(std::shared_ptr(new BinaryRelationExpression(first.getBaseExpression().getManager(), first.getType().numericalComparison(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryRelationExpression::RelationType::LessOrEqual))); } + + Expression operator<(Expression const& first, int64_t second) { + return first < Expression(std::shared_ptr(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second))); + } + + Expression operator>(Expression const& first, int64_t second) { + return first > Expression(std::shared_ptr(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second))); + } + + Expression operator<=(Expression const& first, int64_t second) { + return first <= Expression(std::shared_ptr(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second))); + } + + Expression operator>=(Expression const& first, int64_t second) { + return first >= Expression(std::shared_ptr(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second))); + } Expression minimum(Expression const& first, Expression const& second) { assertSameManager(first.getBaseExpression(), second.getBaseExpression()); diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 11cfb2350..40fcaa572 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -37,6 +37,10 @@ namespace storm { friend Expression operator>=(Expression const& first, Expression const& second); friend Expression operator<(Expression const& first, Expression const& second); friend Expression operator<=(Expression const& first, Expression const& second); + friend Expression operator>(Expression const& first, int64_t second); + friend Expression operator>=(Expression const& first, int64_t second); + friend Expression operator<(Expression const& first, int64_t second); + friend Expression operator<=(Expression const& first, int64_t second); friend Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression); friend Expression implies(Expression const& first, Expression const& second); friend Expression iff(Expression const& first, Expression const& second); @@ -338,6 +342,10 @@ namespace storm { Expression operator>=(Expression const& first, Expression const& second); Expression operator<(Expression const& first, Expression const& second); Expression operator<=(Expression const& first, Expression const& second); + Expression operator>(Expression const& first, int64_t second); + Expression operator>=(Expression const& first, int64_t second); + Expression operator<(Expression const& first, int64_t second); + Expression operator<=(Expression const& first, int64_t second); Expression ite(Expression const& condition, Expression const& thenExpression, Expression const& elseExpression); Expression implies(Expression const& first, Expression const& second); Expression iff(Expression const& first, Expression const& second); diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index def815616..f0872a500 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -1,8 +1,18 @@ #include "src/storage/jani/BoundedIntegerVariable.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/utility/macros.h" namespace storm { namespace jani { + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable, initValue, transient), lowerBound(lowerBound), upperBound(upperBound) { + // Intentionally left empty. + } + + BoundedIntegerVariable::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) : Variable(name, variable, initValue), lowerBound(lowerBound), upperBound(upperBound) { + // 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. } @@ -36,5 +46,15 @@ namespace storm { return true; } + std::shared_ptr makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient, boost::optional lowerBound, boost::optional upperBound) { + if(!lowerBound || !upperBound) { + STORM_LOG_THROW(lowerBound && upperBound, storm::exceptions::NotImplementedException, "Jani Bounded Integer variables (for now) have to be bounded from both sides"); + } + 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()); + } + } } } \ No newline at end of file diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 2fa515dec..c9a42b177 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -9,11 +9,19 @@ namespace storm { class BoundedIntegerVariable : public Variable { public: /*! - * Creates a bounded integer variable. + * Creates a bounded integer variable with initial value. + */ + BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); + /*! + * 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. + * Creates a bounded integer variable with transient set to false and no initial value. */ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); @@ -52,5 +60,9 @@ namespace storm { storm::expressions::Expression upperBound; }; + /** + * Convenience function to call the appropriate constructor and retur a shared pointer to the variable. + */ + std::shared_ptr makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient, boost::optional lowerBound, boost::optional upperBound); } } \ No newline at end of file