sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Splitted explicit model adapter into several logical functions.

tempestpy_adaptions
dehnert 12 years ago
parent
777aa3a914
commit
db01eb92d9
5 changed files with 229 additions and 109 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 69
      examples/dtmc/crowds/crowds5_5.pm
  2. 0
      examples/dtmc/die/die.pm
  3. 254
      src/adapters/ExplicitModelAdapter.h
  4. 2
      src/ir/Program.cpp
  5. 11
      src/storm.cpp

69
examples/dtmc/crowds/crowds5_5.pm
View File

@ -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;

0
test.input → examples/dtmc/die/die.pm
View File

254
src/adapters/ExplicitModelAdapter.h
View File

@ -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));
}
uint_fast64_t targetIndex = (*stateToIndexMap.find(newState)).second;
delete newState;
ExplicitModelAdapter(std::shared_ptr<storm::ir::Program> program) : program(program), allStates(),
stateToIndexMap(), booleanVariables(), integerVariables(), booleanVariableToIndexMap(),
integerVariableToIndexMap(), numberOfTransitions(0) {
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;
}
}
}
StateType* initialState = getNewState(numberOfBooleanVariables, numberOfIntegerVariables);
void computeReachableStateSpace() {
bool nondeterministicModel = program->getModelType() == storm::ir::Program::MDP || program->getModelType() == storm::ir::Program::CTMDP;
for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) {
// Prepare some internal data structures, such as mappings from variables to indices and so on.
this->prepareAuxiliaryDatastructures();
// 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());
// 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

2
src/ir/Program.cpp
View File

@ -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;
}

11
src/storm.cpp
View File

@ -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;

Write Preview
Loading…
Cancel
Save