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

started debugging JANI MDP building 

Former-commit-id: b122d605be
main
dehnert 10 years ago
parent
a4ef3cf778
commit
3919f90712
5 changed files with 224 additions and 41 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 102
      src/builder/DdJaniModelBuilder.cpp
  2. 5
      src/builder/DdPrismModelBuilder.cpp
  3. 4
      src/storage/prism/Program.cpp
  4. 150
      test/functional/builder/DdJaniModelBuilderTest.cpp
  5. 2
      test/functional/builder/DdPrismModelBuilderTest.cpp

102
src/builder/DdJaniModelBuilder.cpp
View File

@ -169,8 +169,10 @@ namespace storm {
std::map<uint64_t, storm::expressions::Variable> actionVariablesMap; std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
// The meta variables used to encode the remaining nondeterminism. // The meta variables used to encode the remaining nondeterminism.
std::vector<storm::expressions::Variable> orderedNondeterminismVariables;
std::set<storm::expressions::Variable> nondeterminismVariables;
std::vector<storm::expressions::Variable> localNondeterminismVariables;
// The meta variables used to encode the actions and nondeterminism.
std::set<storm::expressions::Variable> allNondeterminismVariables;
// DDs representing the identity for each variable. // DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap; std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap;
@ -234,10 +236,21 @@ namespace storm {
CompositionVariables<Type, ValueType> createVariables() { CompositionVariables<Type, ValueType> createVariables() {
CompositionVariables<Type, ValueType> result; CompositionVariables<Type, ValueType> result;
for (auto const& automaton : this->model.getAutomata()) {
// Start by creating a meta variable for the location of the automaton.
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
// Add the location variable to the row/column variables.
result.rowMetaVariables.insert(variablePair.first);
result.columnMetaVariables.insert(variablePair.second);
}
for (auto const& action : this->model.getActions()) { for (auto const& action : this->model.getActions()) {
if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) { if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName()); std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first; result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first;
result.allNondeterminismVariables.insert(variablePair.first);
} }
} }
@ -248,18 +261,8 @@ namespace storm {
} }
for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i)); std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i));
result.orderedNondeterminismVariables.push_back(variablePair.first);
result.nondeterminismVariables.insert(variablePair.first);
}
for (auto const& automaton : this->model.getAutomata()) {
// Start by creating a meta variable for the location of the automaton.
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
// Add the location variable to the row/column variables.
result.rowMetaVariables.insert(variablePair.first);
result.columnMetaVariables.insert(variablePair.second);
result.localNondeterminismVariables.push_back(variablePair.first);
result.allNondeterminismVariables.insert(variablePair.first);
} }
// Create global variables. // Create global variables.
@ -652,11 +655,16 @@ namespace storm {
// Add the source location and the guard. // Add the source location and the guard.
transitionsDd *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard; transitionsDd *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd<ValueType>() * guard;
// If we Multiply the ranges of global variables if we wrote at least one to make sure everything stays within its bounds.
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeUpdate.empty()) { if (!globalVariablesInSomeUpdate.empty()) {
transitionsDd *= variables.globalVariableRanges; transitionsDd *= variables.globalVariableRanges;
} }
// If the edge has a rate, we multiply it to the DD.
if (edge.hasRate()) {
transitionsDd *= variables.rowExpressionAdapter->translateExpression(edge.getRate());
}
return EdgeDd<Type, ValueType>(guard, transitionsDd, globalVariablesInSomeUpdate); return EdgeDd<Type, ValueType>(guard, transitionsDd, globalVariablesInSomeUpdate);
} else { } else {
return EdgeDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>()); return EdgeDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>());
@ -689,13 +697,15 @@ namespace storm {
}; };
template <storm::dd::DdType Type, typename ValueType> template <storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> encodeAction(uint64_t trueIndex, std::vector<storm::expressions::Variable> const& actionVariables, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> encoding = variables.manager->template getAddZero<ValueType>();
storm::dd::Add<Type, ValueType> encodeAction(boost::optional<uint64_t> trueIndex, std::vector<storm::expressions::Variable> const& actionVariables, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> encoding = variables.manager->template getAddOne<ValueType>();
trueIndex = actionVariables.size() - (trueIndex + 1);
if (trueIndex) {
*trueIndex = actionVariables.size() - (*trueIndex + 1);
}
uint64_t index = 0; uint64_t index = 0;
for (auto it = actionVariables.rbegin(), ite = actionVariables.rend(); it != ite; ++it, ++index) { for (auto it = actionVariables.rbegin(), ite = actionVariables.rend(); it != ite; ++it, ++index) {
if (index == trueIndex) {
if (trueIndex && index == trueIndex) {
encoding *= variables.manager->getEncoding(*it, 1).template toAdd<ValueType>(); encoding *= variables.manager->getEncoding(*it, 1).template toAdd<ValueType>();
} else { } else {
encoding *= variables.manager->getEncoding(*it, 0).template toAdd<ValueType>(); encoding *= variables.manager->getEncoding(*it, 0).template toAdd<ValueType>();
@ -717,17 +727,17 @@ namespace storm {
} }
template <storm::dd::DdType Type, typename ValueType> template <storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, std::vector<storm::expressions::Variable> const& orderedNondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, std::vector<storm::expressions::Variable> const& localNondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>(); storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
STORM_LOG_TRACE("Encoding " << index << " with " << orderedNondeterminismVariables.size() << " binary variable(s).");
STORM_LOG_TRACE("Encoding " << index << " with " << localNondeterminismVariables.size() << " binary variable(s).");
std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap; std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap;
for (uint_fast64_t i = 0; i < orderedNondeterminismVariables.size(); ++i) {
if (index & (1ull << (orderedNondeterminismVariables.size() - i - 1))) {
metaVariableNameToValueMap.emplace(orderedNondeterminismVariables[i], 1);
for (uint_fast64_t i = 0; i < localNondeterminismVariables.size(); ++i) {
if (index & (1ull << (localNondeterminismVariables.size() - i - 1))) {
metaVariableNameToValueMap.emplace(localNondeterminismVariables[i], 1);
} else { } else {
metaVariableNameToValueMap.emplace(orderedNondeterminismVariables[i], 0);
metaVariableNameToValueMap.emplace(localNondeterminismVariables[i], 0);
} }
} }
@ -753,17 +763,28 @@ namespace storm {
// Determine how many nondeterminism variables we need. // Determine how many nondeterminism variables we need.
std::vector<storm::expressions::Variable> orderedActionVariables; std::vector<storm::expressions::Variable> orderedActionVariables;
std::set<storm::expressions::Variable> actionVariables; std::set<storm::expressions::Variable> actionVariables;
std::map<uint64_t, uint64_t> actionIndexToVariableIndex;
std::map<uint64_t, boost::optional<uint64_t>> actionIndexToVariableIndex;
uint64_t maximalNumberOfEdgesPerAction = 0; uint64_t maximalNumberOfEdgesPerAction = 0;
for (auto const& action : automatonDd.actionIndexToEdges) { for (auto const& action : automatonDd.actionIndexToEdges) {
orderedActionVariables.push_back(variables.actionVariablesMap.at(action.first));
actionVariables.insert(orderedActionVariables.back());
actionIndexToVariableIndex[action.first] = orderedActionVariables.size() - 1;
if (action.first != model.getSilentActionIndex()) {
orderedActionVariables.push_back(variables.actionVariablesMap.at(action.first));
actionVariables.insert(orderedActionVariables.back());
actionIndexToVariableIndex[action.first] = orderedActionVariables.size() - 1;
} else {
actionIndexToVariableIndex[action.first] = boost::none;
}
maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast<uint64_t>(action.second.size())); maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast<uint64_t>(action.second.size()));
} }
// If the maximal number of edges per action is zero, which can happen if the model only has unsatisfiable guards,
// then we must not compute the number of variables.
if (maximalNumberOfEdgesPerAction == 0) {
return SystemDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>(), 0);
}
uint64_t numberOfNondeterminismVariables = static_cast<uint64_t>(std::ceil(std::log2(maximalNumberOfEdgesPerAction))); uint64_t numberOfNondeterminismVariables = static_cast<uint64_t>(std::ceil(std::log2(maximalNumberOfEdgesPerAction)));
std::vector<storm::expressions::Variable> orderedNondeterminismVariables(numberOfNondeterminismVariables);
std::copy(variables.orderedNondeterminismVariables.begin(), variables.orderedNondeterminismVariables.begin() + numberOfNondeterminismVariables, orderedNondeterminismVariables.begin());
std::vector<storm::expressions::Variable> localNondeterminismVariables(numberOfNondeterminismVariables);
std::copy(variables.localNondeterminismVariables.begin(), variables.localNondeterminismVariables.begin() + numberOfNondeterminismVariables, localNondeterminismVariables.begin());
// Prepare result. // Prepare result.
storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>(); storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
@ -774,7 +795,9 @@ namespace storm {
uint64_t edgeIndex = 0; uint64_t edgeIndex = 0;
for (auto const& edge : action.second) { for (auto const& edge : action.second) {
edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, orderedNondeterminismVariables, variables);
storm::dd::Add<Type, ValueType> dd = edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, localNondeterminismVariables, variables);
dd.exportToDot("add" + std::to_string(edgeIndex) + ".dot");
edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, localNondeterminismVariables, variables);
++edgeIndex; ++edgeIndex;
} }
@ -812,7 +835,7 @@ namespace storm {
} else if (modelType == storm::jani::ModelType::CTMC) { } else if (modelType == storm::jani::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels)); return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::MDP) { } else if (modelType == storm::jani::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.nondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
} }
@ -822,10 +845,10 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType> template <storm::dd::DdType Type, typename ValueType>
void postprocessSystemAndVariables(storm::jani::Model const& model, SystemDd<Type, ValueType>& system, CompositionVariables<Type, ValueType>& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) { void postprocessSystemAndVariables(storm::jani::Model const& model, SystemDd<Type, ValueType>& system, CompositionVariables<Type, ValueType>& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
// Get rid of the nondeterminism variables that were not used. // Get rid of the nondeterminism variables that were not used.
for (uint64_t index = system.numberOfNondeterminismVariables; index < variables.orderedNondeterminismVariables.size(); ++index) {
variables.nondeterminismVariables.erase(variables.orderedNondeterminismVariables[index]);
for (uint64_t index = system.numberOfNondeterminismVariables; index < variables.localNondeterminismVariables.size(); ++index) {
variables.allNondeterminismVariables.erase(variables.localNondeterminismVariables[index]);
} }
variables.orderedNondeterminismVariables.resize(system.numberOfNondeterminismVariables);
variables.localNondeterminismVariables.resize(system.numberOfNondeterminismVariables);
// For DTMCs, we normalize each row to 1 (to account for non-determinism). // For DTMCs, we normalize each row to 1 (to account for non-determinism).
if (model.getModelType() == storm::jani::ModelType::DTMC) { if (model.getModelType() == storm::jani::ModelType::DTMC) {
@ -899,7 +922,7 @@ namespace storm {
for (auto const& variable : variables.actionVariablesMap) { for (auto const& variable : variables.actionVariablesMap) {
action *= variables.manager->template getIdentity<ValueType>(variable.second); action *= variables.manager->template getIdentity<ValueType>(variable.second);
} }
for (auto const& variable : variables.orderedNondeterminismVariables) {
for (auto const& variable : variables.localNondeterminismVariables) {
action *= variables.manager->template getIdentity<ValueType>(variable); action *= variables.manager->template getIdentity<ValueType>(variable);
} }
transitionMatrix += deadlockStates * globalIdentity * action; transitionMatrix += deadlockStates * globalIdentity * action;
@ -933,9 +956,12 @@ namespace storm {
modelComponents.initialStates = computeInitialStates(*this->model, variables); modelComponents.initialStates = computeInitialStates(*this->model, variables);
// Perform reachability analysis to obtain reachable states. // Perform reachability analysis to obtain reachable states.
system.transitionsDd.exportToDot("trans.dot");
std::cout << "nnz: " << system.transitionsDd.getNonZeroCount() << std::endl;
std::cout << "size: " << system.transitionsDd.getNodeCount() << std::endl;
storm::dd::Bdd<Type> transitionMatrixBdd = system.transitionsDd.notZero(); storm::dd::Bdd<Type> transitionMatrixBdd = system.transitionsDd.notZero();
if (this->model->getModelType() == storm::jani::ModelType::MDP) { if (this->model->getModelType() == storm::jani::ModelType::MDP) {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.nondeterminismVariables);
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables);
} }
modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables);

5
src/builder/DdPrismModelBuilder.cpp
View File

@ -1324,6 +1324,11 @@ namespace storm {
// Cut the transitions and rewards to the reachable fragment of the state space. // Cut the transitions and rewards to the reachable fragment of the state space.
storm::dd::Bdd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo); storm::dd::Bdd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo);
transitionMatrix.exportToDot("trans_prism.dot");
std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl;
std::cout << "size: " << transitionMatrix.getNodeCount() << std::endl;
storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero(); storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
if (program.getModelType() == storm::prism::Program::ModelType::MDP) { if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables);

4
src/storage/prism/Program.cpp
View File

@ -1560,7 +1560,7 @@ namespace storm {
automaton.addBoundedIntegerVariable(newIntegerVariable); automaton.addBoundedIntegerVariable(newIntegerVariable);
storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
} else if (!accessingModuleIndices.empty()) {
} else { //if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global. // Otherwise, we need to make it global.
janiModel.addBoundedIntegerVariable(newIntegerVariable); janiModel.addBoundedIntegerVariable(newIntegerVariable);
storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
@ -1575,7 +1575,7 @@ namespace storm {
automaton.addBooleanVariable(newBooleanVariable); automaton.addBooleanVariable(newBooleanVariable);
storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
} else if (!accessingModuleIndices.empty()) {
} else { //if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global. // Otherwise, we need to make it global.
janiModel.addBooleanVariable(newBooleanVariable); janiModel.addBooleanVariable(newBooleanVariable);
storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());

150
test/functional/builder/DdJaniModelBuilderTest.cpp
View File

@ -171,3 +171,153 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions()); EXPECT_EQ(189ul, model->getNumberOfTransitions());
} }
TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
EXPECT_EQ(169ul, mdp->getNumberOfStates());
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
EXPECT_EQ(364ul, mdp->getNumberOfStates());
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
EXPECT_EQ(272ul, mdp->getNumberOfStates());
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
EXPECT_EQ(1038ul, mdp->getNumberOfStates());
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
EXPECT_EQ(4093ul, mdp->getNumberOfStates());
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
EXPECT_EQ(37ul, mdp->getNumberOfStates());
EXPECT_EQ(59ul, mdp->getNumberOfTransitions());
EXPECT_EQ(59ul, mdp->getNumberOfChoices());
}
TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
EXPECT_EQ(169ul, mdp->getNumberOfStates());
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
EXPECT_EQ(364ul, mdp->getNumberOfStates());
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
exit(-1);
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
EXPECT_EQ(272ul, mdp->getNumberOfStates());
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
EXPECT_EQ(1038ul, mdp->getNumberOfStates());
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
EXPECT_EQ(4093ul, mdp->getNumberOfStates());
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.translate();
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
EXPECT_EQ(37ul, mdp->getNumberOfStates());
EXPECT_EQ(59ul, mdp->getNumberOfTransitions());
EXPECT_EQ(59ul, mdp->getNumberOfChoices());
}

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

@ -211,6 +211,8 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices()); EXPECT_EQ(573ul, mdp->getNumberOfChoices());
exit(-1);
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program); model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);

Write Preview
Loading…
Cancel
Save