From 1716c45ec549fd41f4e8e9d989547038fe8688e7 Mon Sep 17 00:00:00 2001
From: masawei <manuel.sascha.weiand@rwth-aachen.de>
Date: Fri, 11 Oct 2013 16:01:29 +0200
Subject: [PATCH 1/2] Fixed compile errors concerning the handling of the
 STORM_HAVE_Z3 flag and a missing include in IRUtility.h Should now compile
 again.

Former-commit-id: a72c906fb0724eff334dc903c9d33aaf4bf46c8d
---
 src/counterexamples/SMTMinimalCommandSetGenerator.h | 2 +-
 src/utility/IRUtility.h                             | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index f2b0ead6e..16cfe7f72 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -16,10 +16,10 @@
 // If we have Z3 available, we have to include the C++ header.
 #ifdef STORM_HAVE_Z3
 #include "z3++.h"
+#include "src/adapters/Z3ExpressionAdapter.h"
 #endif
 
 #include "src/adapters/ExplicitModelAdapter.h"
-#include "src/adapters/Z3ExpressionAdapter.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 
diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h
index 63cf9519e..7ee230450 100644
--- a/src/utility/IRUtility.h
+++ b/src/utility/IRUtility.h
@@ -12,6 +12,7 @@
 
 #include "src/storage/LabeledValues.h"
 #include "src/ir/IR.h"
+#include "src/exceptions/InvalidArgumentException.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"

From 641c09dcfaade8676ce605db1e76b6cd0cb12acc Mon Sep 17 00:00:00 2001
From: David_Korzeniewski <david.korzeniewski@rwth-aachen.de>
Date: Tue, 15 Oct 2013 20:44:08 +0200
Subject: [PATCH 2/2] Fixed compile errors on windows caused by missing
 includes and use of initializer lists (not supported by vs11)

Former-commit-id: 294c26cd64596013e56d3bea16d30bc02474992e
---
 src/adapters/ExplicitModelAdapter.h | 5 ++++-
 src/adapters/Z3ExpressionAdapter.h  | 1 +
 src/storage/LabeledValues.h         | 1 +
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index 9696d9a33..7c41ee0c6 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -309,7 +309,10 @@ namespace storm {
                             // Update the choice by adding the probability/target state to it.
                             double probabilityToAdd = update.getLikelihoodExpression()->getValueAsDouble(currentState);
                             probabilitySum += probabilityToAdd;
-                            addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, {update.getGlobalIndex()});
+							std::set<uint_fast64_t> lables;
+							lables.insert(update.getGlobalIndex());
+                            //addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, {update.getGlobalIndex()});
+							addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, lables);
                         }
                         
                         // Check that the resulting distribution is in fact a distribution.
diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index 211baa2f1..3b15fd007 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -11,6 +11,7 @@
 #include <stack>
 
 #include "src/ir/expressions/ExpressionVisitor.h"
+#include "src/ir/expressions/Expressions.h"
 
 namespace storm {
     namespace adapters {
diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h
index 25f39d9b5..8ebb5ec45 100644
--- a/src/storage/LabeledValues.h
+++ b/src/storage/LabeledValues.h
@@ -9,6 +9,7 @@
 #define STORM_STORAGE_LABELEDVALUES_H
 
 #include <list>
+#include <set>
 
 namespace storm {
     namespace utility {