From 13d45118af216ddc5eaf061667ca38c10cf8d7b4 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 10 Aug 2016 13:24:26 +0200
Subject: [PATCH] initial value support unbounded integers, some extra error
messages)
Former-commit-id: 72a35269f30b290b73412bedc29bd6c110fd7235 [formerly 243d50b5af5b92d8f475b5afd93bc0e73a33c0cc]
Former-commit-id: 9c7e2bd9ebec26fee371c40dd1691b3a48b8ddea
---
src/parser/JaniParser.cpp | 14 ++++++++++++--
src/storage/jani/UnboundedIntegerVariable.cpp | 4 ++++
src/storage/jani/UnboundedIntegerVariable.h | 7 ++++++-
3 files changed, 22 insertions(+), 3 deletions(-)
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index e0fbd338a..25e3d8a1b 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -262,19 +262,29 @@ namespace storm {
initVal = expressionManager->boolean(defaultBooleanInitialValue);
} else {
initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+ STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
}
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") {
+ if(initvalcount == 1) {
+ if(variableStructure.at("initial-value").is_null()) {
+ initVal = expressionManager->integer(defaultIntegerInitialValue);
+ } else {
+ initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+ STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
+ }
+ return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
+ }
return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar);
} else {
// TODO clocks.
- STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")");
}
}
- STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")");
+ STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")");
}
/**
diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp
index 686d6debe..c646b09b1 100644
--- a/src/storage/jani/UnboundedIntegerVariable.cpp
+++ b/src/storage/jani/UnboundedIntegerVariable.cpp
@@ -3,6 +3,10 @@
namespace storm {
namespace jani {
+ UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient) {
+ // Intentionally left empty.
+ }
+
UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) {
// Intentionally left empty.
}
diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h
index 38255591b..d3d3daa01 100644
--- a/src/storage/jani/UnboundedIntegerVariable.h
+++ b/src/storage/jani/UnboundedIntegerVariable.h
@@ -8,9 +8,14 @@ namespace storm {
class UnboundedIntegerVariable : public Variable {
public:
/*!
- * Creates an unbounded integer variable.
+ * Creates an unbounded integer variable without initial value.
*/
UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false);
+ /*!
+ * Creates an unbounded integer variable with initial value.
+ */
+ UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const&, bool transient=false);
+
virtual bool isUnboundedIntegerVariable() const override;
};