From 6e6463183957e7eee565198458ce622ad0ee44f4 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 10 Aug 2016 11:56:49 +0200
Subject: [PATCH] initial value support for booleans, some extra error
messages)
Former-commit-id: bb857b09232918f1521550da26a5ad3958937878 [formerly 80b90ed08e351f9fbfc20afeba92e5812573712b]
Former-commit-id: d529e6b9d27ee62f084a4cedc3cc33e329553b5d
---
src/parser/JaniParser.cpp | 15 ++++++++++++++-
src/parser/JaniParser.h | 3 +++
src/storage/jani/BooleanVariable.cpp | 5 +++++
src/storage/jani/BooleanVariable.h | 8 +++++++-
4 files changed, 29 insertions(+), 2 deletions(-)
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index 10f530e9e..e0fbd338a 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -20,6 +20,8 @@ namespace storm {
// Defaults
////////////
const bool JaniParser::defaultVariableTransient = false;
+ const bool JaniParser::defaultBooleanInitialValue = false;
+ const int64_t JaniParser::defaultIntegerInitialValue = 0;
const std::set<std::string> JaniParser::unsupportedOpstrings({"sin", "cos", "tan", "cot", "sec", "csc", "asin", "acos", "atan", "acot", "asec", "acsc",
"sinh", "cosh", "tanh", "coth", "sech", "csch", "asinh", "acosh", "atanh", "asinh", "acosh"});
@@ -221,7 +223,7 @@ namespace storm {
if(kind == "bounded") {
// First do the bounds, that makes the code a bit more streamlined
STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given");
- storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable "+ name + " (scope: " + scopeDescription + ")");
+ storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")");
assert(lowerboundExpr.isInitialized());
STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given");
storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")");
@@ -237,6 +239,9 @@ namespace storm {
}
std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") ");
if(basictype == "int") {
+ if(initVal) {
+ STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
+ }
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 storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr);
@@ -252,6 +257,14 @@ namespace storm {
// expressionManager->declareRationalVariable(name);
// TODO something.
} else if(variableStructure.at("type") == "bool") {
+ if(initvalcount == 1) {
+ if(variableStructure.at("initial-value").is_null()) {
+ initVal = expressionManager->boolean(defaultBooleanInitialValue);
+ } else {
+ initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+ }
+ return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar);
+ }
return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar);
} else if(variableStructure.at("type") == "int") {
return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar);
diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h
index f86085b49..82165b5ef 100644
--- a/src/parser/JaniParser.h
+++ b/src/parser/JaniParser.h
@@ -71,6 +71,9 @@ namespace storm {
// Default values -- assumptions from JANI.
//////////
static const bool defaultVariableTransient;
+
+ static const bool defaultBooleanInitialValue;
+ static const int64_t defaultIntegerInitialValue;
static const std::set<std::string> unsupportedOpstrings;
diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp
index 56cdf88bd..b7a4c4e19 100644
--- a/src/storage/jani/BooleanVariable.cpp
+++ b/src/storage/jani/BooleanVariable.cpp
@@ -7,6 +7,11 @@ namespace storm {
// Intentionally left empty.
}
+ BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient) {
+ // Intentionally left empty.
+ }
+
+
bool BooleanVariable::isBooleanVariable() const {
return true;
}
diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h
index 5f7292cbf..7a8fe8b21 100644
--- a/src/storage/jani/BooleanVariable.h
+++ b/src/storage/jani/BooleanVariable.h
@@ -7,11 +7,17 @@ namespace storm {
class BooleanVariable : public Variable {
public:
+
/*!
- * Creates a boolean variable.
+ * Creates a Boolean variable with initial value
*/
BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false);
+ /*!
+ * Creates a Boolean variable with initial value
+ */
+ BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue, bool transient=false);
+
virtual bool isBooleanVariable() const override;
};