Merge branch 'master' into MinimalCommandCounterexample

Former-commit-id: 3a30ef5f18

src/adapters/ExplicitModelAdapter.h

@@ -287,7 +287,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.

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 {

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -17,10 +17,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"
 

src/storage/LabeledValues.h

@@ -9,6 +9,7 @@
 #define STORM_STORAGE_LABELEDVALUES_H
 
 #include <list>
+#include <set>
 
 namespace storm {
     namespace utility {

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"