From db01eb92d97e0e0fb4530865fda5d60e613f93d4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 6 Feb 2013 19:51:58 +0100
Subject: [PATCH] Splitted explicit model adapter into several logical
functions.
---
examples/dtmc/crowds/crowds5_5.pm | 69 +++++++
test.input => examples/dtmc/die/die.pm | 0
src/adapters/ExplicitModelAdapter.h | 256 +++++++++++++++----------
src/ir/Program.cpp | 2 +-
src/storm.cpp | 11 +-
5 files changed, 229 insertions(+), 109 deletions(-)
create mode 100644 examples/dtmc/crowds/crowds5_5.pm
rename test.input => examples/dtmc/die/die.pm (100%)
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<TotalRuns -> 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<class T>
- 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));
- }
+ ExplicitModelAdapter(std::shared_ptr<storm::ir::Program> 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<class T>
+ std::shared_ptr<storm::storage::SparseMatrix<T>> toSparseMatrix() {
+ LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program.");
- resultMatrix->finalize();
+ this->computeReachableStateSpace();
+ std::shared_ptr<storm::storage::SparseMatrix<T>> resultMatrix = this->buildMatrix<T>();
- 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<storm::ir::BooleanVariable> booleanVariables;
- std::vector<storm::ir::IntegerVariable> integerVariables;
booleanVariables.resize(numberOfBooleanVariables);
integerVariables.resize(numberOfIntegerVariables);
- std::unordered_map<std::string, uint_fast64_t> booleanVariableToIndexMap;
- std::unordered_map<std::string, uint_fast64_t> 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<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
- std::vector<StateType*> allStates;
+ allStates.clear();
+ stateToIndexMap.clear();
std::queue<StateType*> 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<StateType*, double, StateHash, StateCompare> 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<StateType*> 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<std::string, storm::ir::Assignment> 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<class T>
+ std::shared_ptr<storm::storage::SparseMatrix<T>> buildMatrix() {
+ std::shared_ptr<storm::storage::SparseMatrix<T>> resultMatrix(new storm::storage::SparseMatrix<T>(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<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 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<storm::ir::Program> program;
std::vector<StateType*> allStates;
+ std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
+ std::vector<storm::ir::BooleanVariable> booleanVariables;
+ std::vector<storm::ir::IntegerVariable> integerVariables;
+ std::unordered_map<std::string, uint_fast64_t> booleanVariableToIndexMap;
+ std::unordered_map<std::string, uint_fast64_t> integerVariableToIndexMap;
uint_fast64_t numberOfTransitions;
- std::vector<uint_fast64_t> 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<std::string, std::shared_ptr<stor
// Nothing to do here.
}
-ModelType Program::getModelType() const {
+Program::ModelType Program::getModelType() const {
return modelType;
}
diff --git a/src/storm.cpp b/src/storm.cpp
index d02cee982..55819560b 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -241,12 +241,13 @@ int main(const int argc, const char* argv[]) {
// testChecking();
storm::parser::PrismParser parser;
- std::shared_ptr<storm::ir::Program> program = parser.parseFile("test.input");
+ std::shared_ptr<storm::ir::Program> program = parser.parseFile("examples/dtmc/die/die.pm");
+ storm::adapters::ExplicitModelAdapter explicitModelAdapter(program);
+ std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = explicitModelAdapter.toSparseMatrix<double>();
- std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = storm::adapters::ExplicitModelAdapter::toSparseMatrix<double>(*program);
-
- //storm::adapters::SymbolicModelAdapter symbolicModelAdapter;
- //symbolicAdapter.toMTBDD(*program);
+ std::shared_ptr<storm::ir::Program> secondProgram = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm");
+ storm::adapters::ExplicitModelAdapter secondExplicitModelAdapter(secondProgram);
+ std::shared_ptr<storm::storage::SparseMatrix<double>> secondMatrix = secondExplicitModelAdapter.toSparseMatrix<double>();
cleanUp();
return 0;