Added possibility to evaluate expressions without concrete variables. Fixed some minor things in CUDD Makefiles. Renamed IR adapter.

CMakeLists.txt

@@ -44,6 +44,12 @@ message(STATUS "EIGEN3_INCLUDE_DIR is ${EIGEN3_INCLUDE_DIR}")
 set(GMMXX_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-4.2/include)
 message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}")
 
+# Set all CUDD references to the version in the repository
+set(CUDD_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include)
+set(CUDD_LIBRARY_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/util ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/st ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj)
+message(STATUS "CUDD_INCLUDE_DIR is ${CUDD_INCLUDE_DIR}")
+message(STATUS "CUDD_LIBRARY_DIRS is ${CUDD_LIBRARY_DIRS}")
+
 # Now define all available custom options
 option(DEBUG "Sets whether the DEBUG mode is used" ON)
 option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
@@ -160,6 +166,13 @@ if (ADDITIONAL_LINK_DIRS)
 	link_directories(${ADDITIONAL_LINK_DIRS})
 endif(ADDITIONAL_LINK_DIRS)
 
+if (CUDD_INCLUDE_DIR)
+    include_directories(${CUDD_INCLUDE_DIR})
+endif(CUDD_INCLUDE_DIR)
+if (CUDD_LIBRARY_DIRS)
+    link_directories(${CUDD_LIBRARY_DIRS})
+endif(CUDD_LIBRARY_DIRS)
+
 # Add the executables
 # Must be created *after* Boost was added because of LINK_DIRECTORIES
 add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS})
@@ -211,6 +224,10 @@ if (LOG4CPLUS_INCLUDE_DIR)
     endif(UNIX AND NOT APPLE)
 endif(LOG4CPLUS_INCLUDE_DIR)
 
+if (CUDD_LIBRARY_DIRS)
+    target_link_libraries(storm "-lcudd -lmtr -lst -lutil -lepd -lobj")
+endif(CUDD_LIBRARY_DIRS)
+
 if (THREADS_FOUND)
 	include_directories(${THREADS_INCLUDE_DIRS})
     target_link_libraries (storm ${CMAKE_THREAD_LIBS_INIT})

resources/3rdparty/cudd-2.5.0/Makefile

@@ -7,15 +7,16 @@
 # be overridden from the command line.
 
 # C++ compiler
-CXX	= g++
+#CXX	= g++
 #CXX	= icpc
 #CXX	= ecpc
 #CXX	= CC
 #CXX	= /usr/local/opt/SUNWspro/bin/CC
 #CXX	= cxx
+CXX	= clang++
 
 # Specific options for compilation of C++ files.
-CXXFLAGS =
+CXXFLAGS = -std=c++11 -stdlib=libc++
 # Stricter standard conformance for g++.
 #CXXFLAGS = -std=c++98
 # For Sun CC version 5, this invokes compatibility mode.
@@ -27,12 +28,13 @@ CXXFLAGS =
 # C compiler used for all targets except optimize_dec, which always uses cc.
 #CC	= cc
 #CC	= /usr/local/opt/SUNWspro/bin/cc
-CC	= gcc
+#CC	= gcc
 #CC	= icc
 #CC	= ecc
 #CC	= /usr/ucb/cc
 #CC	= c89
 #CC	= $(CXX)
+CC	= clang
 
 # On some machines ranlib is either non-existent or redundant.
 # Use the following definition if your machine has ranlib and you think
@@ -49,7 +51,7 @@ RANLIB	= ranlib
 #ICFLAGS	=
 # These two are typical settings for optimized code with gcc.
 #ICFLAGS	= -g -O3 -Wall
-ICFLAGS	= -g -O3
+ICFLAGS	= -O3
 
 # Use XCFLAGS to specify machine-dependent compilation flags.
 # For some platforms no special flags are needed.
@@ -59,7 +61,7 @@ ICFLAGS	= -g -O3
 #  Linux
 #
 # Gcc 4.2.4 or higher on i686.
-XCFLAGS	= -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD
+XCFLAGS	= -arch x86_64 -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8
 # Gcc 3.2.2 or higher on i686.
 #XCFLAGS	= -mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD
 # Gcc 2.8.1 on i686.
@@ -198,7 +200,7 @@ DDWDIR	= .
 IDIR	= $(DDWDIR)/include
 INCLUDE = -I$(IDIR)
 
-BDIRS	= cudd dddmp mtr st util epd
+BDIRS	= cudd dddmp mtr st util epd obj
 DIRS	= $(BDIRS) nanotrav
 
 #------------------------------------------------------------------------

resources/3rdparty/cudd-2.5.0/obj/Makefile

@@ -0,0 +1,113 @@
+# $Id: Makefile,v 1.3 2001/03/19 07:34:37 fabio Exp fabio $
+#
+# obj: CUDD's C++ interface
+#---------------------------------------------------------------------------
+.SUFFIXES: .o .cc .u
+
+#CXX	= g++
+CXX	= clang++
+RANLIB	= ranlib
+# Define EXE as .exe for MS-DOS and derivatives.
+PURE	=
+EXE	=
+#EXE	= .exe
+
+MFLAG	=
+#ICFLAGS = -g
+ICFLAGS = 
+XCFLAGS =
+#CXXFLAGS = 
+CXXFLAGS = -O3 -std=c++11 -stdlib=libc++
+CFLAGS	= $(ICFLAGS) $(MFLAG) $(XCFLAGS) $(CXXFLAGS)
+DDDEBUG =
+
+LINTFLAGS = -u -n -DDD_STATS -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_DEBUG -DDD_UNIQUE_PROFILE
+
+# this is to create the lint library
+LINTSWITCH = -o
+
+WHERE	= ..
+
+INCLUDE = $(WHERE)/include
+
+LIBS	= ./libobj.a $(WHERE)/cudd/libcudd.a $(WHERE)/mtr/libmtr.a \
+	$(WHERE)/st/libst.a $(WHERE)/util/libutil.a $(WHERE)/epd/libepd.a
+
+MNEMLIB =
+
+BLIBS	= -kL. -klobj -kL$(WHERE)/cudd -klcudd -kL$(WHERE)/mtr -klmtr \
+	-kL$(WHERE)/st -klst -kL$(WHERE)/util -klutil -kL$(WHERE)/epd -klepd
+
+LINTLIBS = ./llib-lobj.ln $(WHERE)/cudd/llib-lcudd.ln \
+	$(WHERE)/mtr/llib-lmtr.ln $(WHERE)/st/llib-lst.ln \
+	$(WHERE)/util/llib-lutil.ln $(WHERE)/epd/llib-lepd.ln
+
+LDFLAGS =
+
+# files for the package
+P	= obj
+PSRC	= cuddObj.cc
+PHDR	= cuddObj.hh $(INCLUDE)/cudd.h
+POBJ	= $(PSRC:.cc=.o)
+PUBJ	= $(PSRC:.cc=.u)
+TARGET	= test$(P)$(EXE)
+TARGETu = test$(P)-u
+
+# files for the test program
+SRC	= test$(P).cc
+OBJ	= $(SRC:.cc=.o)
+UBJ	= $(SRC:.cc=.u)
+
+#------------------------------------------------------
+
+lib$(P).a: $(POBJ)
+	ar rv $@ $?
+	$(RANLIB) $@
+
+.cc.o: $(PHDR)
+	$(CXX) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG)
+
+optimize_dec: lib$(P).b
+
+lib$(P).b: $(PUBJ)
+	ar rv $@ $?
+	$(RANLIB) $@
+
+.cc.u: $(PHDR)
+	cxx -j $< -I$(INCLUDE) $(CFLAGS)
+
+# if the header files change, recompile
+$(POBJ): $(PHDR)
+$(PUBJ): $(PHDR)
+$(OBJ): $(PHDR)
+$(UBJ): $(PHDR)
+
+$(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB)
+	$(PURE) $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm
+
+# optimize (DECstations and Alphas only: uses u-code)
+$(TARGETu): $(SRC) $(UBJ) $(HDR) $(LIBS:.a=.b)
+	cxx -O3 -Olimit 1000 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm
+
+lint: llib-l$(P).ln
+
+llib-l$(P).ln: $(PSRC) $(PHDR)
+	lint $(LINTFLAGS) $(LINTSWITCH)$(P) -I$(INCLUDE) $(PSRC)
+
+lintpgm: lint
+	lint $(LINTFLAGS) -I$(INCLUDE) $(SRC) $(LINTLIBS)
+
+tags: $(PSRC) $(PHDR)
+	ctags $(PSRC) $(PHDR)
+
+all: lib$(P).a lib$(P).b llib-l$(P).ln tags
+
+programs: $(TARGET) $(TARGETu) lintpgm
+
+clean:
+	rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \
+	.pure core *.warnings
+
+distclean: clean
+	rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \
+	*.bak *~ tags .gdb_history *.qv *.qx

src/adapters/IntermediateRepresentationAdapter.h → src/adapters/ExplicitModelAdapter.h

@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_
-#define STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_
+#ifndef STORM_IR_EXPLICITMODELADAPTER_H_
+#define STORM_IR_EXPLICITMODELADAPTER_H_
 
 #include "src/storage/SparseMatrix.h"
 #include "src/utility/Settings.h"
@@ -49,7 +49,7 @@ public:
 	}
 };
 
-class IntermediateRepresentationAdapter {
+class ExplicitModelAdapter {
 public:
 	template<class T>
 	static storm::storage::SparseMatrix<T>* toSparseMatrix(storm::ir::Program const& program) {
@@ -89,12 +89,12 @@ public:
 		StateType* initialState = getNewState(numberOfBooleanVariables, numberOfIntegerVariables);
 
 		for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) {
-			bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(*initialState);
+			bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(initialState);
 			std::get<0>(*initialState)[i] = initialValue;
 		}
 
 		for (uint_fast64_t i = 0; i < numberOfIntegerVariables; ++i) {
-			int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(*initialState);
+			int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(initialState);
 			std::get<1>(*initialState)[i] = initialValue;
 		}
 
@@ -124,7 +124,7 @@ public:
 					storm::ir::Command const& command = module.getCommand(j);
 
 					// Check if this command is enabled in the current state.
-					if (command.getGuard()->getValueAsBool(*currentState)) {
+					if (command.getGuard()->getValueAsBool(currentState)) {
 						hasTransition = true;
 						std::unordered_map<StateType*, double, StateHash, StateCompare> stateToProbabilityMap;
 						std::queue<StateType*> statesToDelete;
@@ -135,12 +135,12 @@ public:
 							// std::cout << "took state: " << newState->first << "/" << newState->second << std::endl;
 							std::map<std::string, storm::ir::Assignment> const& booleanAssignmentMap = update.getBooleanAssignments();
 							for (auto assignedVariable : booleanAssignmentMap) {
-								setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState));
+								setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState));
 							}
 							std::map<std::string, storm::ir::Assignment> const& integerAssignmentMap = update.getIntegerAssignments();
 							for (auto assignedVariable : integerAssignmentMap) {
 								// std::cout << "evaluting " << assignedVariable.second.getExpression()->toString() << " as " << assignedVariable.second.getExpression()->getValueAsInt(*currentState) << std::endl;
-								setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState));
+								setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(currentState));
 							}
 
 							// std::cout << "applied: " << update.toString() << std::endl;
@@ -148,10 +148,10 @@ public:
 
 							auto probIt = stateToProbabilityMap.find(newState);
 							if (probIt != stateToProbabilityMap.end()) {
-								stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+								stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(currentState);
 							} else {
 								++totalNumberOfTransitions;
-								stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+								stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(currentState);
 							}
 
 							auto it = stateToIndexMap.find(newState);
@@ -204,7 +204,7 @@ public:
 					storm::ir::Command const& command = module.getCommand(j);
 
 					// Check if this command is enabled in the current state.
-					if (command.getGuard()->getValueAsBool(*currentState)) {
+					if (command.getGuard()->getValueAsBool(currentState)) {
 						hasTransition = true;
 						std::map<uint_fast64_t, double> stateIndexToProbabilityMap;
 						for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
@@ -214,11 +214,11 @@ public:
 
 							std::map<std::string, storm::ir::Assignment> const& booleanAssignmentMap = update.getBooleanAssignments();
 							for (auto assignedVariable : booleanAssignmentMap) {
-								setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState));
+								setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState));
 							}
 							std::map<std::string, storm::ir::Assignment> const& integerAssignmentMap = update.getIntegerAssignments();
 							for (auto assignedVariable : integerAssignmentMap) {
-								setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState));
+								setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(currentState));
 							}
 
 							uint_fast64_t targetIndex = (*stateToIndexMap.find(newState)).second;
@@ -226,9 +226,9 @@ public:
 
 							auto probIt = stateIndexToProbabilityMap.find(targetIndex);
 							if (probIt != stateIndexToProbabilityMap.end()) {
-								stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+								stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(currentState);
 							} else {
-								stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+								stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(currentState);
 							}
 						}
 
@@ -275,9 +275,8 @@ private:
 	}
 };
 
-}
+} // namespace adapters
 
-}
+} // namespace storm
 
-
-#endif /* STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ */
+#endif /* STORM_IR_EXPLICITMODELADAPTER_H_ */

src/ir/IntegerVariable.cpp

@@ -27,6 +27,17 @@ IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName,
 	}
 }
 
+// Return lower bound for variable.
+std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
+	return this->lowerBound;
+}
+
+// Return upper bound for variable.
+std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getUpperBound() const {
+	return this->upperBound;
+}
+
+
 // Build a string representation of the variable.
 std::string IntegerVariable::toString() const {
 	std::stringstream result;

src/ir/IntegerVariable.h

@@ -37,6 +37,18 @@ public:
 	 */
 	IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
 
+	/*!
+	 * Retrieves the lower bound for this integer variable.
+	 * @returns the lower bound for this integer variable.
+	 */
+	std::shared_ptr<storm::ir::expressions::BaseExpression> getLowerBound() const;
+
+	/*!
+	 * Retrieves the upper bound for this integer variable.
+	 * @returns the upper bound for this integer variable.
+	 */
+	std::shared_ptr<storm::ir::expressions::BaseExpression> getUpperBound() const;
+
 	/*!
 	 * Retrieves a string representation of this variable.
 	 * @returns a string representation of this variable.

src/ir/expressions/BaseExpression.h

@@ -37,7 +37,7 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (type != int_) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
 					<< this->getTypeName() << "' as 'int'.";
@@ -46,7 +46,7 @@ public:
 					<< this->getTypeName() << " because evaluation implementation is missing.";
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (type != bool_) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
 					<< this->getTypeName() << "' as 'bool'.";
@@ -55,7 +55,7 @@ public:
 					<< this->getTypeName() << " because evaluation implementation is missing.";
 	}
 
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (type != bool_) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
 					<< this->getTypeName() << "' as 'double'.";

src/ir/expressions/BinaryBooleanFunctionExpression.h

@@ -31,7 +31,7 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		bool resultLeft = left->getValueAsBool(variableValues);
 		bool resultRight = right->getValueAsBool(variableValues);
 		switch(functionType) {

src/ir/expressions/BinaryNumericalFunctionExpression.h

@@ -28,7 +28,7 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != int_) {
 			BaseExpression::getValueAsInt(variableValues);
 		}
@@ -45,7 +45,7 @@ public:
 		}
 	}
 
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != double_) {
 			BaseExpression::getValueAsDouble(variableValues);
 		}

src/ir/expressions/BinaryRelationExpression.h

@@ -28,7 +28,7 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		int_fast64_t resultLeft = left->getValueAsInt(variableValues);
 		int_fast64_t resultRight = right->getValueAsInt(variableValues);
 		switch(relationType) {

src/ir/expressions/BooleanConstantExpression.h

@@ -29,7 +29,7 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
 					<< "Boolean constant '" << this->getConstantName() << "' is undefined.";

src/ir/expressions/BooleanLiteral.h

@@ -28,7 +28,7 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
 

src/ir/expressions/DoubleConstantExpression.h

@@ -26,7 +26,7 @@ public:
 
 	}
 
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
 					<< "Double constant '" << this->getConstantName() << "' is undefined.";

src/ir/expressions/DoubleLiteral.h

@@ -30,7 +30,7 @@ public:
 
 	}
 
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
 

src/ir/expressions/IntegerConstantExpression.h

@@ -26,7 +26,7 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
 					<< "Integer constant '" << this->getConstantName() << "' is undefined.";

src/ir/expressions/IntegerLiteral.h

@@ -28,7 +28,7 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
 

src/ir/expressions/UnaryBooleanFunctionExpression.h

@@ -28,7 +28,7 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		bool resultChild = child->getValueAsBool(variableValues);
 		switch(functionType) {
 		case NOT: return !resultChild; break;

src/ir/expressions/UnaryNumericalFunctionExpression.h

@@ -28,7 +28,7 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != int_) {
 			BaseExpression::getValueAsInt(variableValues);
 		}
@@ -41,7 +41,7 @@ public:
 		}
 	}
 
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != double_) {
 			BaseExpression::getValueAsDouble(variableValues);
 		}

src/ir/expressions/VariableExpression.h

@@ -32,23 +32,33 @@ public:
 		return variableName;
 	}
 
-	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != int_) {
 			BaseExpression::getValueAsInt(variableValues);
 		}
 
-		return variableValues.second[index];
+		if (variableValues != nullptr) {
+			return variableValues->second[index];
+		} else {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression"
+					<< " involving variables without variable values.";
+		}
 	}
 
-	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != bool_) {
 			BaseExpression::getValueAsBool(variableValues);
 		}
 
-		return variableValues.first[index];
+		if (variableValues != nullptr) {
+			return variableValues->first[index];
+		} else {
+			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression"
+					<< " involving variables without variable values.";
+		}
 	}
 
-	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != double_) {
 			BaseExpression::getValueAsDouble(variableValues);
 		}

src/storm.cpp

@@ -36,7 +36,8 @@
 #include "log4cplus/fileappender.h"
 
 #include "src/parser/PrismParser.h"
-#include "src/adapters/IntermediateRepresentationAdapter.h"
+#include "src/adapters/ExplicitModelAdapter.h"
+#include "src/adapters/SymbolicModelAdapter.h"
 
 #include "src/exceptions/InvalidSettingsException.h"
 
@@ -245,9 +246,8 @@ int main(const int argc, const char* argv[]) {
 
 	storm::parser::PrismParser parser;
 	std::shared_ptr<storm::ir::Program> program = parser.parseFile("test.input");
-	storm::storage::SparseMatrix<double>* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix<double>(*program);
-	// result->print();
-	delete result;
+	storm::adapters::SymbolicModelAdapter symbolicAdapter;
+	symbolicAdapter.toMTBDD(*program);
 
 	cleanUp();
 	return 0;