Intermediate commit to switch workplace.

src/adapters/ExplicitModelAdapter.h

@@ -17,6 +17,7 @@
 #include <map>
 #include <queue>
 #include <iostream>
+#include <memory>
 
 typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType;
 
@@ -52,8 +53,102 @@ public:
 class ExplicitModelAdapter {
 public:
 	template<class T>
-	static storm::storage::SparseMatrix<T>* toSparseMatrix(storm::ir::Program const& program) {
+	std::shared_ptr<storm::storage::SparseMatrix<T>> toSparseMatrix(storm::ir::Program const& program) {
 		LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program.");
+
+		this->computeReachableStateSpace(program);
+
+
+
+		std::shared_ptr<storm::storage::SparseMatrix<T>> resultMatrix(new storm::storage::SparseMatrix<T>(allStates.size()));
+		resultMatrix->initialize(totalNumberOfTransitions);
+
+		uint_fast64_t currentIndex = 0;
+		for (StateType* currentState : allStates) {
+			bool hasTransition = false;
+
+			// 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)) {
+						hasTransition = true;
+						std::map<uint_fast64_t, double> stateIndexToProbabilityMap;
+						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));
+							}
+
+							uint_fast64_t targetIndex = (*stateToIndexMap.find(newState)).second;
+							delete newState;
+
+							auto probIt = stateIndexToProbabilityMap.find(targetIndex);
+							if (probIt != stateIndexToProbabilityMap.end()) {
+								stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(currentState);
+							} else {
+								stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(currentState);
+							}
+						}
+
+						// Now insert the actual values into the matrix.
+						for (auto targetIndex : stateIndexToProbabilityMap) {
+							resultMatrix->addNextValue(currentIndex, targetIndex.first, targetIndex.second);
+						}
+					}
+				}
+			}
+			if (!hasTransition) {
+				resultMatrix->addNextValue(currentIndex, currentIndex, 1);
+			}
+
+			++currentIndex;
+		}
+
+		resultMatrix->finalize();
+
+		LOG4CPLUS_INFO(logger, "Created sparse matrix with " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions.");
+
+		// Now free all the elements we allocated.
+		for (auto element : allStates) {
+			delete element;
+		}
+
+		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;
+	}
+
+	void computeReachableStateSpace(storm::ir::Program const& program) {
+		bool nondeterministicModel = program.getModelType() == storm::ir::Program::MDP || program.getModelType() == storm::ir::Program::CTMDP;
+
 		uint_fast64_t numberOfIntegerVariables = 0;
 		uint_fast64_t numberOfBooleanVariables = 0;
 		for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
@@ -132,20 +227,15 @@ public:
 							storm::ir::Update const& update = command.getUpdate(k);
 
 							StateType* newState = new StateType(*currentState);
-							// 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));
 							}
 							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));
 							}
 
-							// std::cout << "applied: " << update.toString() << std::endl;
-							// std::cout << "got: " << newState->first << "/" << newState->second << std::endl;
-
 							auto probIt = stateToProbabilityMap.find(newState);
 							if (probIt != stateToProbabilityMap.end()) {
 								stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(currentState);
@@ -187,92 +277,11 @@ public:
 				}
 			}
 		}
-
-		storm::storage::SparseMatrix<T>* resultMatrix = new storm::storage::SparseMatrix<T>(allStates.size());
-		resultMatrix->initialize(totalNumberOfTransitions);
-
-		uint_fast64_t currentIndex = 0;
-		for (StateType* currentState : allStates) {
-			bool hasTransition = false;
-
-			// 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)) {
-						hasTransition = true;
-						std::map<uint_fast64_t, double> stateIndexToProbabilityMap;
-						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));
-							}
-
-							uint_fast64_t targetIndex = (*stateToIndexMap.find(newState)).second;
-							delete newState;
-
-							auto probIt = stateIndexToProbabilityMap.find(targetIndex);
-							if (probIt != stateIndexToProbabilityMap.end()) {
-								stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(currentState);
-							} else {
-								stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(currentState);
-							}
-						}
-
-						// Now insert the actual values into the matrix.
-						for (auto targetIndex : stateIndexToProbabilityMap) {
-							resultMatrix->addNextValue(currentIndex, targetIndex.first, targetIndex.second);
-						}
-					}
-				}
-			}
-			if (!hasTransition) {
-				resultMatrix->addNextValue(currentIndex, currentIndex, 1);
-			}
-
-			++currentIndex;
-		}
-
-		resultMatrix->finalize();
-
-		LOG4CPLUS_INFO(logger, "Created sparse matrix with " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions.");
-
-		// Now free all the elements we allocated.
-		for (auto element : allStates) {
-			delete element;
-		}
-
-		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;
-	}
+	std::vector<StateType*> allStates;
+	uint_fast64_t numberOfTransitions;
+	std::vector<uint_fast64_t> numbersOfNondeterministicChoices;
 };
 
 } // namespace adapters

src/ir/Program.cpp

@@ -24,6 +24,10 @@ Program::Program(ModelType modelType, std::map<std::string, std::shared_ptr<stor
 	// Nothing to do here.
 }
 
+ModelType Program::getModelType() const {
+	return modelType;
+}
+
 // Build a string representation of the program.
 std::string Program::toString() const {
 	std::stringstream result;

src/ir/Program.h

@@ -66,6 +66,12 @@ public:
 	 */
 	storm::ir::Module const& getModule(uint_fast64_t index) const;
 
+	/*!
+	 * Retrieves the model type of the model.
+	 * @returns the type of the model.
+	 */
+	ModelType getModelType() const;
+
 	/*!
 	 * Retrieves a string representation of this program.
 	 * @returns a string representation of this program.

src/ir/Variable.cpp

@@ -28,7 +28,7 @@ std::string const& Variable::getName() const {
 	return variableName;
 }
 
-uint_fast64_t getIndex() const {
+uint_fast64_t Variable::getIndex() const {
 	return index;
 }
 

src/storm.cpp

@@ -112,7 +112,6 @@ bool parseOptions(const int argc, const char* argv[]) {
 	}
 	if (s->isSet("test-prctl")) {
 		// storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
-		delete s;
 		return false;
 	}
 	
@@ -243,8 +242,11 @@ int main(const int argc, const char* argv[]) {
 
 	storm::parser::PrismParser parser;
 	std::shared_ptr<storm::ir::Program> program = parser.parseFile("test.input");
-	storm::adapters::SymbolicModelAdapter symbolicAdapter;
-	symbolicAdapter.toMTBDD(*program);
+
+	std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = storm::adapters::ExplicitModelAdapter::toSparseMatrix<double>(*program);
+
+	//storm::adapters::SymbolicModelAdapter symbolicModelAdapter;
+	//symbolicAdapter.toMTBDD(*program);
 
 	cleanUp();
 	return 0;