Intermediate commit to switch workplace.

src/adapters/IntermediateRepresentationAdapter.h

@@ -35,6 +35,13 @@ public:
 	}
 };
 
+class StateCompare {
+public:
+	bool operator()(StateType* state1, StateType* state2) const {
+		return *state1 == *state2;
+	}
+};
+
 class IntermediateRepresentationAdapter {
 public:
 	template<class T>
@@ -72,24 +79,20 @@ public:
 			}
 		}
 
-		StateType* initialState = new StateType(std::vector<bool>(), std::vector<int_fast64_t>());
-		std::get<0>(*initialState).resize(numberOfBooleanVariables);
-		std::get<1>(*initialState).resize(numberOfIntegerVariables);
+		StateType* initialState = getNewState(numberOfBooleanVariables, numberOfIntegerVariables);
 
 		for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) {
-			bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(std::get<0>(*initialState), std::get<1>(*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(std::get<0>(*initialState), std::get<1>(*initialState));
+			int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(*initialState);
 			std::get<1>(*initialState)[i] = initialValue;
 		}
 
-		std::cout << "Initial State:" << std::get<0>(*initialState) << " / " << std::get<1>(*initialState) << std::endl;
-
 		uint_fast64_t nextIndex = 1;
-		std::unordered_map<StateType*, uint_fast64_t, StateHash> stateToIndexMap;
+		std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
 		std::vector<StateType*> allStates;
 		std::queue<StateType*> stateQueue;
 
@@ -97,6 +100,7 @@ public:
 		stateQueue.push(initialState);
 		stateToIndexMap[initialState] = 0;
 
+		uint_fast64_t totalNumberOfTransitions = 0;
 		while (!stateQueue.empty()) {
 			// Get first state in queue.
 			StateType* currentState = stateQueue.front();
@@ -111,15 +115,44 @@ public:
 					storm::ir::Command const& command = module.getCommand(j);
 
 					// Check if this command is enabled in the current state.
-					if (command.getGuard()->getValueAsBool(std::get<0>(*currentState), std::get<1>(*currentState))) {
+					if (command.getGuard()->getValueAsBool(*currentState)) {
+						std::unordered_map<StateType*, double, StateHash, StateCompare> stateToProbabilityMap;
 						for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
 							storm::ir::Update const& update = command.getUpdate(k);
 
+							StateType* newState = new StateType(*currentState);
+
 							std::map<std::string, storm::ir::Assignment> const& booleanAssignmentMap = update.getBooleanAssignments();
 							for (auto assignedVariable : booleanAssignmentMap) {
-								// Check if the variable that is being assigned is a boolean or an integer.
-								// auto boolIt =
+								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));
+							}
+
+							auto probIt = stateToProbabilityMap.find(newState);
+							if (probIt != stateToProbabilityMap.end()) {
+								stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+							} else {
+								++totalNumberOfTransitions;
+								stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+							}
 
+							auto it = stateToIndexMap.find(newState);
+							if (it != stateToIndexMap.end()) {
+								// Delete the state object directly as we have already seen that state.
+								delete newState;
+							} else {
+								// Add state to the queue of states that are still to be explored.
+								stateQueue.push(newState);
+
+								// Add state to list of all states so that we can delete it at the end.
+								allStates.push_back(newState);
+
+								// Give a unique index to the newly found state.
+								stateToIndexMap[newState] = nextIndex;
+								++nextIndex;
 							}
 						}
 					}
@@ -127,13 +160,68 @@ public:
 			}
 		}
 
+		std::cout << "Found " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions.";
+
+		storm::storage::SquareSparseMatrix<T>* resultMatrix = new storm::storage::SquareSparseMatrix<T>(allStates.size());
+		resultMatrix->initialize(totalNumberOfTransitions);
+
+		for (StateType* state : allStates) {
+			// Iterate over all modules.
+			for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+				storm::ir::Module const& module = program.getModule(i);
+
+				// Iterate over all commands.
+				for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
+					storm::ir::Command const& command = module.getCommand(j);
+
+					// Check if this command is enabled in the current state.
+					if (command.getGuard()->getValueAsBool(*currentState)) {
+						std::unordered_map<StateType*, double, StateHash, StateCompare> stateToProbabilityMap;
+						for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
+							storm::ir::Update const& update = command.getUpdate(k);
+
+							StateType* newState = new StateType(*currentState);
+
+							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));
+							}
+							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));
+							}
+
+							auto probIt = stateToProbabilityMap.find(newState);
+							if (probIt != stateToProbabilityMap.end()) {
+								stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+							} else {
+								++totalNumberOfTransitions;
+								stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState);
+							}
+		}
+
 		// Now free all the elements we allocated.
 		for (auto element : allStates) {
 			delete element;
 		}
-		return nullptr;
+		return resultMatrix;
 	}
 
+private:
+	static StateType* getNewState(uint_fast64_t numberOfBooleanVariables, uint_fast64_t numberOfIntegerVariables) {
+		StateType* result = new StateType();
+		result->first.resize(numberOfBooleanVariables);
+		result->second.resize(numberOfIntegerVariables);
+		return result;
+	}
+
+	static void setValue(StateType* state, uint_fast64_t index, bool value) {
+		std::get<0>(*state)[index] = value;
+	}
+
+	static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) {
+		std::get<1>(*state)[index] = value;
+	}
 };
 
 }

src/ir/TransitionReward.h

@@ -10,6 +10,8 @@
 
 #include "expressions/BaseExpression.h"
 
+#include <memory>
+
 namespace storm {
 
 namespace ir {

src/ir/Update.cpp

@@ -79,18 +79,18 @@ std::string Update::toString() const {
 	uint_fast64_t i = 0;
 	for (auto assignment : booleanAssignments) {
 		result << assignment.second.toString();
-		++i;
 		if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) {
 			result << " & ";
 		}
+		++i;
 	}
 	i = 0;
 	for (auto assignment : integerAssignments) {
 		result << assignment.second.toString();
-		++i;
 		if (i < integerAssignments.size() - 1) {
 			result << " & ";
 		}
+		++i;
 	}
 	return result.str();
 }

src/ir/Variable.h

@@ -11,6 +11,7 @@
 #include "expressions/BaseExpression.h"
 
 #include <string>
+#include <memory>
 
 namespace storm {
 

src/ir/expressions/BaseExpression.h

@@ -37,7 +37,7 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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,9 +31,9 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
-		bool resultLeft = left->getValueAsBool(booleanVariableValues, integerVariableValues);
-		bool resultRight = right->getValueAsBool(booleanVariableValues, integerVariableValues);
+	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) {
 		case AND: return resultLeft & resultRight; break;
 		case OR: return resultLeft | resultRight; break;

src/ir/expressions/BinaryNumericalFunctionExpression.h

@@ -28,13 +28,13 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsInt(variableValues);
 		}
 
-		int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues);
-		int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues);
+		int_fast64_t resultLeft = left->getValueAsInt(variableValues);
+		int_fast64_t resultRight = right->getValueAsInt(variableValues);
 		switch(functionType) {
 		case PLUS: return resultLeft + resultRight; break;
 		case MINUS: return resultLeft - resultRight; break;
@@ -45,13 +45,13 @@ public:
 		}
 	}
 
-	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
 		if (this->getType() != double_) {
-			BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsDouble(variableValues);
 		}
 
-		double resultLeft = left->getValueAsDouble(booleanVariableValues, integerVariableValues);
-		double resultRight = right->getValueAsDouble(booleanVariableValues, integerVariableValues);
+		double resultLeft = left->getValueAsDouble(variableValues);
+		double resultRight = right->getValueAsDouble(variableValues);
 		switch(functionType) {
 		case PLUS: return resultLeft + resultRight; break;
 		case MINUS: return resultLeft - resultRight; break;

src/ir/expressions/BinaryRelationExpression.h

@@ -28,9 +28,9 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
-		int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues);
-		int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues);
+	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) {
 		case EQUAL: return resultLeft == resultRight; break;
 		case LESS: return resultLeft < resultRight; break;

src/ir/expressions/BooleanConstantExpression.h

@@ -29,7 +29,7 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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,8 +28,8 @@ public:
 
 	}
 
-	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
-		bool resultChild = child->getValueAsBool(booleanVariableValues, integerVariableValues);
+	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;
 		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "

src/ir/expressions/UnaryNumericalFunctionExpression.h

@@ -28,12 +28,12 @@ public:
 
 	}
 
-	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsInt(variableValues);
 		}
 
-		int_fast64_t resultChild = child->getValueAsInt(booleanVariableValues, integerVariableValues);
+		int_fast64_t resultChild = child->getValueAsInt(variableValues);
 		switch(functionType) {
 		case MINUS: return -resultChild; break;
 		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
@@ -41,12 +41,12 @@ public:
 		}
 	}
 
-	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
 		if (this->getType() != double_) {
-			BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsDouble(variableValues);
 		}
 
-		double resultChild = child->getValueAsDouble(booleanVariableValues, integerVariableValues);
+		double resultChild = child->getValueAsDouble(variableValues);
 		switch(functionType) {
 		case MINUS: return -resultChild; break;
 		default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "

src/ir/expressions/VariableExpression.h

@@ -32,25 +32,25 @@ public:
 		return variableName;
 	}
 
-	virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsInt(variableValues);
 		}
 
-		return integerVariableValues[index];
+		return variableValues.second[index];
 	}
 
-	virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
 		if (this->getType() != bool_) {
-			BaseExpression::getValueAsBool(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsBool(variableValues);
 		}
 
-		return booleanVariableValues[index];
+		return variableValues.first[index];
 	}
 
-	virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const& variableValues) const {
 		if (this->getType() != double_) {
-			BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+			BaseExpression::getValueAsDouble(variableValues);
 		}
 
 		throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with "

src/parser/PrismParser.cpp

@@ -459,11 +459,8 @@ std::shared_ptr<storm::ir::Program> PrismParser::parse(std::istream& inputStream
 		}
 		msg << std::endl;
 
-// On Mac OS, exception messages are not displayed in case an exception is propagated to the
-// operating system, so we need to display the message ourselves.
-#if defined(MACOSX)
-		std::cout << msg.str();
-#endif
+		std::cerr << msg.str();
+
 		// Now propagate exception.
 		throw storm::exceptions::WrongFileFormatException() << msg.str();
 	}

src/storm.cpp

@@ -244,6 +244,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::SquareSparseMatrix<double>* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix<double>(*program);
+	result->print();
+	delete result;
 
 	cleanUp();
 	return 0;