diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index d056f6849..1c2d9365e 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -17,6 +17,7 @@ #include #include #include +#include typedef std::pair, std::vector> StateType; @@ -52,8 +53,102 @@ public: class ExplicitModelAdapter { public: template - static storm::storage::SparseMatrix* toSparseMatrix(storm::ir::Program const& program) { + std::shared_ptr> toSparseMatrix(storm::ir::Program const& program) { LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program."); + + this->computeReachableStateSpace(program); + + + + std::shared_ptr> resultMatrix(new storm::storage::SparseMatrix(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 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 const& booleanAssignmentMap = update.getBooleanAssignments(); + for (auto assignedVariable : booleanAssignmentMap) { + setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState)); + } + std::map 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 const& booleanAssignmentMap = update.getBooleanAssignments(); for (auto assignedVariable : booleanAssignmentMap) { setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState)); } std::map 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* resultMatrix = new storm::storage::SparseMatrix(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 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 const& booleanAssignmentMap = update.getBooleanAssignments(); - for (auto assignedVariable : booleanAssignmentMap) { - setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState)); - } - std::map 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 allStates; + uint_fast64_t numberOfTransitions; + std::vector numbersOfNondeterministicChoices; }; } // namespace adapters diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index e5dfa9ce3..73bb62e9c 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -24,6 +24,10 @@ Program::Program(ModelType modelType, std::mapisSet("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 program = parser.parseFile("test.input"); - storm::adapters::SymbolicModelAdapter symbolicAdapter; - symbolicAdapter.toMTBDD(*program); + + std::shared_ptr> matrix = storm::adapters::ExplicitModelAdapter::toSparseMatrix(*program); + + //storm::adapters::SymbolicModelAdapter symbolicModelAdapter; + //symbolicAdapter.toMTBDD(*program); cleanUp(); return 0;