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

Made DD-based model construction work for all DTMC benchmarks we have. Included tests for both DD-based and excplicit model generation from PRISM models. 

Former-commit-id: e4af6d9f8a
main
dehnert 11 years ago
parent
b3d18c2367
commit
0f0baf61a4
4 changed files with 162 additions and 59 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. 70
      src/builder/DdPrismModelBuilder.cpp
  2. 82
      src/builder/DdPrismModelBuilder.h
  3. 36
      test/functional/builder/DdPrismModelBuilderTest.cpp
  4. 33
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp

70
src/builder/DdPrismModelBuilder.cpp
View File

@ -52,6 +52,8 @@ namespace storm {
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Update const& update) {
storm::dd::Dd<Type> updateDd = generationInfo.manager->getOne();
STORM_LOG_TRACE("Translating update " << update);
// Iterate over all assignments (boolean and integer) and build the DD for it.
std::vector<storm::prism::Assignment> assignments = update.getAssignments();
std::set<storm::expressions::Variable> assignedVariables;
@ -122,7 +124,7 @@ namespace storm {
template <storm::dd::DdType Type>
typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) {
STORM_LOG_TRACE("Translating guard " << command.getGuardExpression());
storm::dd::Dd<Type> guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression());
storm::dd::Dd<Type> guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()];
STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable.");
if (!guardDd.isZero()) {
@ -138,9 +140,6 @@ namespace storm {
commandDd += updateDd;
}
guardDd.exportToDot(module.getName() + "_cmd_" + std::to_string(command.getGlobalIndex()) + "_grd.dot");
commandDd.exportToDot(module.getName() + "_cmd_" + std::to_string(command.getGlobalIndex()) + ".dot");
return ActionDecisionDiagram(guardDd, guardDd * commandDd);
} else {
return ActionDecisionDiagram(*generationInfo.manager);
@ -428,18 +427,20 @@ namespace storm {
}
return result;
} else {
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
// Simply add all actions.
storm::dd::Dd<Type> result = module.independentAction.transitionsDd;
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
result += synchronizingAction.second.transitionsDd;
}
return result;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
}
}
template <storm::dd::DdType Type>
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
std::pair<storm::dd::Dd<Type>, typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram> DdPrismModelBuilder<Type>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
// Create the initial offset mapping.
std::map<uint_fast64_t, uint_fast64_t> synchronizingActionToOffsetMap;
for (auto const& actionIndex : generationInfo.program.getActionIndices()) {
@ -467,9 +468,15 @@ namespace storm {
// Combine the non-synchronizing action.
system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, nextModule.independentAction, system.identity, nextModule.identity);
// For all synchronizing actions that the next module does not have, we need to multiply the identity of the next module.
for (auto& action : system.synchronizingActionToDecisionDiagramMap) {
if (!nextModule.hasSynchronizingAction(action.first)) {
action.second = combineUnsynchronizedActions(generationInfo, action.second, ActionDecisionDiagram(*generationInfo.manager), system.identity, nextModule.identity);
}
}
// Combine synchronizing actions.
for (auto const& actionIndex : currentModule.getActionIndices()) {
std::cout << "treating action index " << actionIndex << std::endl;
if (system.hasSynchronizingAction(actionIndex)) {
system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]);
} else {
@ -488,11 +495,11 @@ namespace storm {
result = result / result.sumAbstract(generationInfo.columnMetaVariables);
}
return result;
return std::make_pair(result, system);
}
template <storm::dd::DdType Type>
void DdPrismModelBuilder<Type>::translateProgram(storm::prism::Program const& program, Options const& options) {
std::pair<storm::dd::Dd<Type>, storm::dd::Dd<Type>> DdPrismModelBuilder<Type>::translateProgram(storm::prism::Program const& program, Options const& options) {
// There might be nondeterministic variables. In that case the program must be prepared before translating.
storm::prism::Program preparedProgram;
if (options.constantDefinitions) {
@ -503,24 +510,42 @@ namespace storm {
preparedProgram = preparedProgram.substituteConstants();
std::cout << "translated prog: " << preparedProgram << std::endl;
// std::cout << "translated prog: " << preparedProgram << std::endl;
// Start by initializing the structure used for storing all information needed during the model generation.
// In particular, this creates the meta variables used to encode the model.
GenerationInformation generationInfo(preparedProgram);
auto clock = std::chrono::high_resolution_clock::now();
storm::dd::Dd<Type> transitionMatrix = createSystemDecisionDiagram(generationInfo);
std::cout << "Built transition matrix in " << std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl;
transitionMatrix.exportToDot("trans.dot");
std::cout << "num transitions: " << transitionMatrix.getNonZeroCount() << std::endl;
std::pair<storm::dd::Dd<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
storm::dd::Dd<Type> transitionMatrix = transitionMatrixModulePair.first;
ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
storm::dd::Dd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo);
std::cout << "initial states: " << initialStates.getNonZeroCount() << std::endl;
// Cut the transition matrix to the reachable fragment of the state space.
storm::dd::Dd<Type> reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix);
transitionMatrix *= reachableStates;
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Dd<Type> statesWithTransition = transitionMatrix.notZero();
if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
}
statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables);
storm::dd::Dd<Type> deadlockStates = reachableStates * !statesWithTransition;
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states.");
// FIXME: For MDPs, we need to use an action encoding if we do not want to attach a lot of self-loops.
transitionMatrix += deadlockStates * globalModule.identity;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
}
}
storm::dd::Dd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrix);
std::cout << "reachable states: " << reachableStates.getNonZeroCount() << std::endl;
exit(-1);
return std::make_pair(reachableStates, transitionMatrix * reachableStates);
}
template <storm::dd::DdType Type>
@ -541,14 +566,9 @@ namespace storm {
// If the model is an MDP, we can abstract from the variables encoding the nondeterminism in the model.
storm::dd::Dd<Type> transitionBdd = transitions.notZero();
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
std::set<storm::expressions::Variable> abstractVariables;
abstractVariables.insert(generationInfo.synchronizationMetaVariables.begin(), generationInfo.synchronizationMetaVariables.end());
abstractVariables.insert(generationInfo.nondeterminismMetaVariables.begin(), generationInfo.nondeterminismMetaVariables.end());
transitionBdd = transitionBdd.existsAbstract(abstractVariables);
transitionBdd = transitionBdd.existsAbstract(generationInfo.allNondeterminismVariables);
}
transitionBdd.exportToDot("trans.dot");
reachableStatesBdd.exportToDot("reach.dot");
// Perform the BFS to discover all reachable states.
bool changed = true;

82
src/builder/DdPrismModelBuilder.h
View File

@ -59,7 +59,7 @@ namespace storm {
*
* @param program The program to translate.
*/
static void translateProgram(storm::prism::Program const& program, Options const& options = Options());
static std::pair<storm::dd::Dd<Type>, storm::dd::Dd<Type>> translateProgram(storm::prism::Program const& program, Options const& options = Options());
private:
// This structure can store the decision diagrams representing a particular action.
@ -158,12 +158,19 @@ namespace storm {
// The meta variables used to encode the synchronization.
std::vector<storm::expressions::Variable> synchronizationMetaVariables;
// A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization
// variables). This is handy to abstract from this variable set.
std::set<storm::expressions::Variable> allNondeterminismVariables;
// DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Dd<Type>> variableToIdentityMap;
// DDs representing the identity for each module (index).
// DDs representing the identity for each module.
std::map<std::string, storm::dd::Dd<Type>> moduleToIdentityMap;
// DDs representing the valid ranges of the variables of each module.
std::map<std::string, storm::dd::Dd<Type>> moduleToRangeMap;
private:
/*!
* Creates the required meta variables and variable/module identities.
@ -173,6 +180,7 @@ namespace storm {
for (uint_fast64_t i = 0; i < program.getActionIndices().size(); ++i) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable("sync" + std::to_string(i));
synchronizationMetaVariables.push_back(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
// Add nondeterminism variables (number of modules + number of commands).
@ -183,23 +191,10 @@ namespace storm {
for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable("nondet" + std::to_string(i));
nondeterminismMetaVariables.push_back(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
// Create meta variables for global program variables.
for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
rowMetaVariables.insert(variablePair.first);
variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second));
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
}
for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) {
int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
@ -210,31 +205,30 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
} for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
rowMetaVariables.insert(variablePair.first);
variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second));
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
}
// Create meta variables for each of the modules' variables.
for (storm::prism::Module const& module : program.getModules()) {
storm::dd::Dd<Type> moduleIdentity = manager->getOne();
for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
rowMetaVariables.insert(variablePair.first);
variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
moduleIdentity *= variableIdentity;
rowColumnMetaVariablePairs.push_back(variablePair);
}
storm::dd::Dd<Type> moduleRange = manager->getOne();
for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) {
int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
@ -248,12 +242,32 @@ namespace storm {
variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
variableIdentity.exportToDot(variablePair.first.getName() + "_ident.dot");
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
moduleIdentity *= variableIdentity;
moduleRange *= manager->getRange(variablePair.first);
rowColumnMetaVariablePairs.push_back(variablePair);
}
for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
rowMetaVariables.insert(variablePair.first);
variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
moduleIdentity *= variableIdentity;
moduleRange *= manager->getRange(variablePair.first);
rowColumnMetaVariablePairs.push_back(variablePair);
}
moduleToIdentityMap[module.getName()] = moduleIdentity;
moduleToRangeMap[module.getName()] = moduleRange;
}
}
};
@ -280,7 +294,7 @@ namespace storm {
static storm::dd::Dd<Type> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
static storm::dd::Dd<Type> createSystemDecisionDiagram(GenerationInformation& generationInfo);
static std::pair<storm::dd::Dd<Type>, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo);
static storm::dd::Dd<Type> createInitialStatesDecisionDiagram(GenerationInformation& generationInfo);

36
test/functional/builder/DdPrismModelBuilderTest.cpp
View File

@ -0,0 +1,36 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include <utility>
#include "src/storage/dd/CuddDd.h"
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
TEST(DdPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::pair<storm::dd::Dd<storm::dd::DdType::CUDD>, storm::dd::Dd<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(13, model.first.getNonZeroCount());
EXPECT_EQ(20, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(677, model.first.getNonZeroCount());
EXPECT_EQ(867, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(8607, model.first.getNonZeroCount());
EXPECT_EQ(15113, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(273, model.first.getNonZeroCount());
EXPECT_EQ(397, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(1728, model.first.getNonZeroCount());
EXPECT_EQ(2505, model.second.getNonZeroCount());
}

33
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -0,0 +1,33 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/PrismParser.h"
#include "src/builder/ExplicitPrismModelBuilder.h"
TEST(ExplicitPrismModelBuilderTest, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::unique_ptr<storm::models::AbstractModel<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(13, model->getNumberOfStates());
EXPECT_EQ(20, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(677, model->getNumberOfStates());
EXPECT_EQ(867, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(8607, model->getNumberOfStates());
EXPECT_EQ(15113, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(273, model->getNumberOfStates());
EXPECT_EQ(397, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(1728, model->getNumberOfStates());
EXPECT_EQ(2505, model->getNumberOfTransitions());
}
Write Preview
Loading…
Cancel
Save