From 0a1cbb57f0b441a09a0db5558a4c3ca69ac7e520 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Mon, 8 Aug 2016 11:24:03 +0200
Subject: [PATCH] towards initial value support

Former-commit-id: 32e31b7834dc80a44b38e3e3d6aee7a8f9b9a246 [formerly dced3cef8b0d30e38ffd1d6a1d46bc133ffbbc13]
Former-commit-id: f7570bff749ab0828136016e51fed309ef9347da
---
 src/parser/JaniParser.cpp     |  9 +++++++++
 src/storage/jani/Variable.cpp | 19 ++++++++++++++++---
 src/storage/jani/Variable.h   | 25 ++++++++++++++++++++++++-
 3 files changed, 49 insertions(+), 4 deletions(-)

diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index d6481618e..0afe7b147 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -207,7 +207,16 @@ namespace storm {
             if(tvarcount == 1) {
                 transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name  + "' (scope: " + scopeDescription + ")  ");
             }
+            size_t initvalcount = variableStructure.count("initial-value");
+            if(transientVar) {
+                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<storm::expressions::Expression> initValue;
+            if(initvalcount == 1) {
 
+            }
             STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration.");
 
             if(variableStructure.at("type").is_object()) {
diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp
index e2d5facb4..ad7a1de51 100644
--- a/src/storage/jani/Variable.cpp
+++ b/src/storage/jani/Variable.cpp
@@ -6,11 +6,16 @@
 
 namespace storm {
     namespace jani {
-        
-        Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient) {
+
+        Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& init, bool transient) : name(name), variable(variable),  transient(transient), init(init) {
             // Intentionally left empty.
         }
-        
+
+        Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient), init() {
+            // Intentionally left empty.
+        }
+
+
         storm::expressions::Variable const& Variable::getExpressionVariable() const {
             return variable;
         }
@@ -34,6 +39,14 @@ namespace storm {
         bool Variable::isTransientVariable() const {
             return transient;
         }
+
+        bool Variable::hasInitExpression() const {
+            return static_cast<bool>(init);
+        }
+
+        storm::expressions::Expression const& Variable::getInitExpression() const {
+            return this->init.get();
+        }
         
         BooleanVariable& Variable::asBooleanVariable() {
             return dynamic_cast<BooleanVariable&>(*this);
diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h
index 197cfff65..884bf8d9b 100644
--- a/src/storage/jani/Variable.h
+++ b/src/storage/jani/Variable.h
@@ -2,6 +2,7 @@
 
 #include <cstdint>
 #include <string>
+#include <boost/optional.hpp>
 
 #include "src/storage/expressions/Variable.h"
 #include "src/storage/expressions/Expression.h"
@@ -16,7 +17,12 @@ namespace storm {
         class Variable {
         public:
             /*!
-             * Creates a new variable.
+             * Creates a new variable with initial value construct
+             */
+            Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& init, bool transient = false);
+
+            /*!
+             * Creates a new variable without initial value construct.
              */
             Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false);
             
@@ -29,6 +35,20 @@ namespace storm {
              * Retrieves the name of the variable.
              */
             std::string const& getName() const;
+
+            /*!
+             * Retrieves whether an initial expression is set.
+             */
+            bool hasInitExpression() const;
+
+            /*!
+             * Retrieves the initial expression
+             * Should only be called if an initial expression is set for this variable.
+             *
+             * @see hasInitExpression()
+             */
+            storm::expressions::Expression const& getInitExpression() const;
+
                         
             // Methods to determine the type of the variable.
             virtual bool isBooleanVariable() const;
@@ -54,6 +74,9 @@ namespace storm {
 
             /// Whether this is a transient variable.
             bool transient;
+
+            /// Expression for initial values
+            boost::optional<storm::expressions::Expression> init;
         };
         
     }