diff --git a/examples/dtmc/crowds/crowds5_5.pm b/examples/dtmc/crowds/crowds5_5.pm new file mode 100644 index 000000000..5ce2bab9c --- /dev/null +++ b/examples/dtmc/crowds/crowds5_5.pm @@ -0,0 +1,69 @@ +dtmc + +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 5; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> 1: (phase'=0); + +endmodule + +label "observe0Greater1" = observe0>1; +label "observe1Greater1" = observe1>1; +label "observe2Greater1" = observe2>1; +label "observe3Greater1" = observe3>1; +label "observe4Greater1" = observe4>1; +label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; \ No newline at end of file diff --git a/test.input b/examples/dtmc/die/die.pm similarity index 100% rename from test.input rename to examples/dtmc/die/die.pm diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 1c2d9365e..40e0fc056 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -52,92 +52,27 @@ public: class ExplicitModelAdapter { public: - template - 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)); - } + ExplicitModelAdapter(std::shared_ptr program) : program(program), allStates(), + stateToIndexMap(), booleanVariables(), integerVariables(), booleanVariableToIndexMap(), + integerVariableToIndexMap(), numberOfTransitions(0) { - 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; - } + template + std::shared_ptr> toSparseMatrix() { + LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program."); - resultMatrix->finalize(); + this->computeReachableStateSpace(); + std::shared_ptr> resultMatrix = this->buildMatrix(); - LOG4CPLUS_INFO(logger, "Created sparse matrix with " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions."); + LOG4CPLUS_INFO(logger, "Created sparse matrix with " << resultMatrix->getRowCount() << " reachable states and " << resultMatrix->getNonZeroEntryCount() << " transitions."); - // Now free all the elements we allocated. - for (auto element : allStates) { - delete element; - } + this->clearReachableStateSpace(); 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; } @@ -146,28 +81,21 @@ private: 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; - + void prepareAuxiliaryDatastructures() { uint_fast64_t numberOfIntegerVariables = 0; uint_fast64_t numberOfBooleanVariables = 0; - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); - numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); + for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { + numberOfIntegerVariables += program->getModule(i).getNumberOfIntegerVariables(); + numberOfBooleanVariables += program->getModule(i).getNumberOfBooleanVariables(); } - std::vector booleanVariables; - std::vector integerVariables; booleanVariables.resize(numberOfBooleanVariables); integerVariables.resize(numberOfIntegerVariables); - std::unordered_map booleanVariableToIndexMap; - std::unordered_map integerVariableToIndexMap; - uint_fast64_t nextBooleanVariableIndex = 0; uint_fast64_t nextIntegerVariableIndex = 0; - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - storm::ir::Module const& module = program.getModule(i); + for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { + storm::ir::Module const& module = program->getModule(i); for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { booleanVariables[nextBooleanVariableIndex] = module.getBooleanVariable(j); @@ -180,39 +108,53 @@ private: ++nextIntegerVariableIndex; } } + } + + void computeReachableStateSpace() { + bool nondeterministicModel = program->getModelType() == storm::ir::Program::MDP || program->getModelType() == storm::ir::Program::CTMDP; + + // Prepare some internal data structures, such as mappings from variables to indices and so on. + this->prepareAuxiliaryDatastructures(); - StateType* initialState = getNewState(numberOfBooleanVariables, numberOfIntegerVariables); + // Create a fresh state which can hold as many boolean and integer variables as there are. + StateType* initialState = new StateType(); + initialState->first.resize(booleanVariables.size()); + initialState->second.resize(integerVariables.size()); - for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) { + // Now initialize all fields in the value vectors of the state according to the initial + // values provided by the input program. + for (uint_fast64_t i = 0; i < booleanVariables.size(); ++i) { bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(initialState); std::get<0>(*initialState)[i] = initialValue; } - - for (uint_fast64_t i = 0; i < numberOfIntegerVariables; ++i) { + for (uint_fast64_t i = 0; i < integerVariables.size(); ++i) { int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(initialState); std::get<1>(*initialState)[i] = initialValue; } + // Now set up the environment for a breadth-first search starting from the initial state. uint_fast64_t nextIndex = 1; - std::unordered_map stateToIndexMap; - std::vector allStates; + allStates.clear(); + stateToIndexMap.clear(); std::queue stateQueue; allStates.push_back(initialState); stateQueue.push(initialState); stateToIndexMap[initialState] = 0; - uint_fast64_t totalNumberOfTransitions = 0; + numberOfTransitions = 0; while (!stateQueue.empty()) { // Get first state in queue. StateType* currentState = stateQueue.front(); stateQueue.pop(); + // Remember whether the state has at least one transition such that transitions can be + // inserted upon detection of a deadlock state. 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); + 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) { @@ -221,11 +163,26 @@ private: // Check if this command is enabled in the current state. if (command.getGuard()->getValueAsBool(currentState)) { hasTransition = true; + + // Remember what states are targeted by an update of the current command + // in order to be able to sum those probabilities and not increase the + // transition count. std::unordered_map stateToProbabilityMap; + + // Keep a queue of states to delete after the current command. When one + // command is processed and states are encountered which were already found + // before, we can only delete them after the command has been processed, + // because the stateToProbabilityMap will contain illegal values otherwise. std::queue statesToDelete; + + // Now iterate over all updates to see where the updates take the current + // state. for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { storm::ir::Update const& update = command.getUpdate(k); + // Now copy the current state and only overwrite the entries in the + // vectors if there is an assignment to that variable in the current + // update. StateType* newState = new StateType(*currentState); std::map const& booleanAssignmentMap = update.getBooleanAssignments(); for (auto assignedVariable : booleanAssignmentMap) { @@ -236,23 +193,29 @@ private: setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(currentState)); } + // If we have already found the target state of the update, we must not + // increase the transition count. auto probIt = stateToProbabilityMap.find(newState); if (probIt != stateToProbabilityMap.end()) { stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(currentState); } else { - ++totalNumberOfTransitions; + ++numberOfTransitions; stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(currentState); } + // Depending on whether the state was found previously, we mark it for + // deletion or add it to the reachable state space and mark it for + // further exploration. auto it = stateToIndexMap.find(newState); if (it != stateToIndexMap.end()) { - // Delete the state object directly as we have already seen that state. + // Queue the state object for deletion as we have already seen that + // state. statesToDelete.push(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. + // Add state to list of all reachable states. allStates.push_back(newState); // Give a unique index to the newly found state. @@ -260,6 +223,8 @@ private: ++nextIndex; } } + + // Now delete all states queued for deletion. while (!statesToDelete.empty()) { delete statesToDelete.front(); statesToDelete.pop(); @@ -268,9 +233,12 @@ private: } } + // If the state is a deadlock state, and the corresponding flag is set, we tolerate that + // and increase the number of transitions by one, because a self-loop is going to be + // inserted in the next step. If the flag is not set, an exception is thrown. if (!hasTransition) { if (storm::settings::instance()->isSet("fix-deadlocks")) { - ++totalNumberOfTransitions; + ++numberOfTransitions; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; @@ -279,9 +247,91 @@ private: } } + template + std::shared_ptr> buildMatrix() { + std::shared_ptr> resultMatrix(new storm::storage::SparseMatrix(allStates.size())); + resultMatrix->initialize(numberOfTransitions); + + // Keep track of the running index to insert values into correct matrix row. + uint_fast64_t currentIndex = 0; + + // Determine the matrix content for every row (i.e. reachable state). + 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 the state is a deadlock state, a self-loop is inserted. Note that we do not have + // to check whether --fix-deadlocks is set, because if this was not the case an + // exception would have been thrown earlier. + if (!hasTransition) { + resultMatrix->addNextValue(currentIndex, currentIndex, 1); + } + + ++currentIndex; + } + + // Finalize matrix and return it. + resultMatrix->finalize(); + return resultMatrix; + } + + void clearReachableStateSpace() { + allStates.clear(); + stateToIndexMap.clear(); + } + + std::shared_ptr program; std::vector allStates; + std::unordered_map stateToIndexMap; + std::vector booleanVariables; + std::vector integerVariables; + std::unordered_map booleanVariableToIndexMap; + std::unordered_map integerVariableToIndexMap; uint_fast64_t numberOfTransitions; - std::vector numbersOfNondeterministicChoices; }; } // namespace adapters diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 73bb62e9c..9792451d4 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -24,7 +24,7 @@ Program::Program(ModelType modelType, std::map program = parser.parseFile("test.input"); + std::shared_ptr program = parser.parseFile("examples/dtmc/die/die.pm"); + storm::adapters::ExplicitModelAdapter explicitModelAdapter(program); + std::shared_ptr> matrix = explicitModelAdapter.toSparseMatrix(); - std::shared_ptr> matrix = storm::adapters::ExplicitModelAdapter::toSparseMatrix(*program); - - //storm::adapters::SymbolicModelAdapter symbolicModelAdapter; - //symbolicAdapter.toMTBDD(*program); + std::shared_ptr secondProgram = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm"); + storm::adapters::ExplicitModelAdapter secondExplicitModelAdapter(secondProgram); + std::shared_ptr> secondMatrix = secondExplicitModelAdapter.toSparseMatrix(); cleanUp(); return 0;