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

JANI model builder for DTMCs working 

Former-commit-id: 25f12f3e05
main
dehnert 9 years ago
parent
310db8a234
commit
7750480714
7 changed files with 92 additions and 87 deletions
Unified View
  1. 67
      src/builder/DdJaniModelBuilder.cpp
  2. 2
      src/storage/jani/BooleanVariable.h
  3. 2
      src/storage/jani/BoundedIntegerVariable.h
  4. 44
      src/storage/prism/Program.cpp
  5. 2
      src/storage/prism/Program.h
  6. 46
      test/functional/builder/DdJaniModelBuilderTest.cpp
  7. 4
      test/functional/builder/DdPrismModelBuilderTest.cpp

67
src/builder/DdJaniModelBuilder.cpp
View File

@ -252,13 +252,19 @@ namespace storm {
result.nondeterminismVariables.insert(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);
}
// Create global variables. // Create global variables.
storm::dd::Bdd<Type> globalVariableRanges = result.manager->getBddOne(); storm::dd::Bdd<Type> globalVariableRanges = result.manager->getBddOne();
for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) { for (auto const& variable : this->model.getGlobalVariables()) {
createVariable(variable, result);
globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
}
for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) {
createVariable(variable, result); createVariable(variable, result);
globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable())); globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
} }
@ -269,24 +275,14 @@ namespace storm {
storm::dd::Bdd<Type> identity = result.manager->getBddOne(); storm::dd::Bdd<Type> identity = result.manager->getBddOne();
storm::dd::Bdd<Type> range = result.manager->getBddOne(); storm::dd::Bdd<Type> range = result.manager->getBddOne();
// Start by creating a meta variable for the location of the automaton. // Add the identity and ranges of the location variables to the ones of the automaton.
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()];
result.automatonToLocationVariableMap[automaton.getName()] = variablePair; storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
identity &= variableIdentity.toBdd(); identity &= variableIdentity.toBdd();
range &= result.manager->getRange(variablePair.first); range &= result.manager->getRange(locationVariables.first);
// Add the location variable to the row/column variables.
result.rowMetaVariables.insert(variablePair.first);
result.columnMetaVariables.insert(variablePair.second);
// Then create variables for the variables of the automaton. // Then create variables for the variables of the automaton.
for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { for (auto const& variable : automaton.getVariables()) {
createVariable(variable, result);
identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
}
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
createVariable(variable, result); createVariable(variable, result);
identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd(); identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable())); range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
@ -299,6 +295,16 @@ namespace storm {
return result; return result;
} }
void createVariable(storm::jani::Variable const& variable, CompositionVariables<Type, ValueType>& result) {
if (variable.isBooleanVariable()) {
createVariable(variable.asBooleanVariable(), result);
} else if (variable.isBoundedIntegerVariable()) {
createVariable(variable.asBoundedIntegerVariable(), result);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid type of variable in JANI model.");
}
}
void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) { void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
int_fast64_t low = variable.getLowerBound().evaluateAsInt(); int_fast64_t low = variable.getLowerBound().evaluateAsInt();
int_fast64_t high = variable.getUpperBound().evaluateAsInt(); int_fast64_t high = variable.getUpperBound().evaluateAsInt();
@ -400,6 +406,14 @@ namespace storm {
EdgeDd<Type, ValueType> composeEdgesInParallel(EdgeDd<Type, ValueType> const& edge1, EdgeDd<Type, ValueType> const& edge2) { EdgeDd<Type, ValueType> composeEdgesInParallel(EdgeDd<Type, ValueType> const& edge1, EdgeDd<Type, ValueType> const& edge2) {
EdgeDd<Type, ValueType> result; EdgeDd<Type, ValueType> result;
// Compose the guards.
result.guardDd = edge1.guardDd * edge2.guardDd;
// If the composed guard is already zero, we can immediately return an empty result.
if (result.guardDd.isZero()) {
result.transitionsDd = edge1.transitionsDd.getDdManager().template getAddZero<ValueType>();
}
// Compute the set of variables written multiple times by the composition. // Compute the set of variables written multiple times by the composition.
std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes; std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin())); std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
@ -494,6 +508,7 @@ namespace storm {
// First, consider all actions in the left subcomposition. // First, consider all actions in the left subcomposition.
AutomatonDd<Type, ValueType> result(leftSubautomaton.identity * rightSubautomaton.identity); AutomatonDd<Type, ValueType> result(leftSubautomaton.identity * rightSubautomaton.identity);
uint64_t index = 0;
for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) {
// If we need to synchronize over this action, do so now. // If we need to synchronize over this action, do so now.
if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) {
@ -501,7 +516,11 @@ namespace storm {
if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { if (rightIt != rightSubautomaton.actionIndexToEdges.end()) {
for (auto const& edge1 : actionEdges.second) { for (auto const& edge1 : actionEdges.second) {
for (auto const& edge2 : rightIt->second) { for (auto const& edge2 : rightIt->second) {
result.actionIndexToEdges[actionEdges.first].push_back(composeEdgesInParallel(edge1, edge2)); EdgeDd<Type, ValueType> edgeDd = composeEdgesInParallel(edge1, edge2);
if (!edgeDd.guardDd.isZero()) {
result.actionIndexToEdges[actionEdges.first].push_back(edgeDd);
}
index++;
} }
} }
} }
@ -918,19 +937,15 @@ namespace storm {
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.nondeterminismVariables);
} }
transitionMatrixBdd.template toAdd<ValueType>().exportToDot("trans_before_reach.dot");
modelComponents.initialStates.template toAdd<ValueType>().exportToDot("initial.dot");
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);
modelComponents.reachableStates.template toAdd<ValueType>().exportToDot("reach.dot");
// Cut transitions to reachable states. // Cut transitions to reachable states.
storm::dd::Add<Type, ValueType> reachableStatesAdd = modelComponents.reachableStates.template toAdd<ValueType>(); storm::dd::Add<Type, ValueType> reachableStatesAdd = modelComponents.reachableStates.template toAdd<ValueType>();
modelComponents.transitionMatrix = system.transitionsDd * reachableStatesAdd; modelComponents.transitionMatrix = system.transitionsDd * reachableStatesAdd;
system.transitionsDd.exportToDot("trans_full.dot");
system.stateActionDd *= reachableStatesAdd; system.stateActionDd *= reachableStatesAdd;
// Fix deadlocks if existing. // Fix deadlocks if existing.
// fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables); fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
// Finally, create the model. // Finally, create the model.
return createModel(this->model->getModelType(), variables, modelComponents); return createModel(this->model->getModelType(), variables, modelComponents);

2
src/storage/jani/BooleanVariable.h
View File

@ -12,7 +12,7 @@ namespace storm {
*/ */
BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); BooleanVariable(std::string const& name, storm::expressions::Variable const& variable);
virtual bool isBooleanVariable() const; virtual bool isBooleanVariable() const override;
}; };
} }

2
src/storage/jani/BoundedIntegerVariable.h
View File

@ -33,7 +33,7 @@ namespace storm {
*/ */
void setUpperBound(storm::expressions::Expression const& expression); void setUpperBound(storm::expressions::Expression const& expression);
virtual bool isBoundedIntegerVariable() const; virtual bool isBoundedIntegerVariable() const override;
private: private:
// The expression defining the lower bound of the variable. // The expression defining the lower bound of the variable.

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

@ -1475,7 +1475,7 @@ namespace storm {
return *this->manager; return *this->manager;
} }
storm::jani::Model Program::toJani() const { storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
STORM_LOG_THROW(!this->specifiesSystemComposition(), storm::exceptions::InvalidOperationException, "Cannot translate PRISM program with custom system composition to JANI."); STORM_LOG_THROW(!this->specifiesSystemComposition(), storm::exceptions::InvalidOperationException, "Cannot translate PRISM program with custom system composition to JANI.");
// Start by creating an empty JANI model. // Start by creating an empty JANI model.
@ -1502,16 +1502,16 @@ namespace storm {
} }
// Add all global variables of the PRISM program to the JANI model. // Add all global variables of the PRISM program to the JANI model.
for (auto const& variable : globalBooleanVariables) {
janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable()));
storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
}
for (auto const& variable : globalIntegerVariables) { for (auto const& variable : globalIntegerVariables) {
janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
} }
for (auto const& variable : globalBooleanVariables) {
janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable()));
storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
}
// Add all actions of the PRISM program to the JANI model. // Add all actions of the PRISM program to the JANI model.
for (auto const& action : indexToActionMap) { for (auto const& action : indexToActionMap) {
@ -1552,33 +1552,33 @@ namespace storm {
storm::jani::Automaton automaton(module.getName()); storm::jani::Automaton automaton(module.getName());
storm::expressions::Expression initialStatesExpression; storm::expressions::Expression initialStatesExpression;
for (auto const& variable : module.getBooleanVariables()) { for (auto const& variable : module.getIntegerVariables()) {
storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable()); storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
// If there is exactly one module reading and writing the variable, we can make the variable local to this module. // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
if (accessingModuleIndices.size() == 1) { if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
automaton.addBooleanVariable(newBooleanVariable); automaton.addBoundedIntegerVariable(newIntegerVariable);
storm::expressions::Expression variableInitialExpression = storm::expressions::iff(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.size() > 1) { } else { // if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global. // Otherwise, we need to make it global.
janiModel.addBooleanVariable(newBooleanVariable); janiModel.addBoundedIntegerVariable(newIntegerVariable);
storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
} }
} }
for (auto const& variable : module.getIntegerVariables()) { for (auto const& variable : module.getBooleanVariables()) {
storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable());
std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
// If there is exactly one module reading and writing the variable, we can make the variable local to this module. // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
if (accessingModuleIndices.size() == 1) { if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
automaton.addBoundedIntegerVariable(newIntegerVariable); automaton.addBooleanVariable(newBooleanVariable);
storm::expressions::Expression variableInitialExpression = 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.size() > 1) { } else { //if (!accessingModuleIndices.empty()) {
// Otherwise, we need to make it global. // Otherwise, we need to make it global.
janiModel.addBoundedIntegerVariable(newIntegerVariable); janiModel.addBooleanVariable(newBooleanVariable);
storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
} }
} }

2
src/storage/prism/Program.h
View File

@ -558,7 +558,7 @@ namespace storm {
/*! /*!
* Converts the PRISM model into an equivalent JANI model. * Converts the PRISM model into an equivalent JANI model.
*/ */
storm::jani::Model toJani() const; storm::jani::Model toJani(bool allVariablesGlobal = false) const;
private: private:
/*! /*!

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

@ -13,78 +13,72 @@
TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = program.toJani(); storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel); storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
auto t1 = std::chrono::high_resolution_clock::now(); auto t1 = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate(); std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
auto t2 = std::chrono::high_resolution_clock::now(); auto t2 = std::chrono::high_resolution_clock::now();
std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl; std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
EXPECT_EQ(13ul, model->getNumberOfStates());
// EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions());
// EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();
t2 = std::chrono::high_resolution_clock::now(); t2 = std::chrono::high_resolution_clock::now();
std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl; std::cout << "brp: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
// EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(677ul, model->getNumberOfStates());
// EXPECT_EQ(867ul, model->getNumberOfTransitions()); EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();
t2 = std::chrono::high_resolution_clock::now(); t2 = std::chrono::high_resolution_clock::now();
std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl; std::cout << "crowds: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
// EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(8607ul, model->getNumberOfStates());
// EXPECT_EQ(15113ul, model->getNumberOfTransitions()); EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();
t2 = std::chrono::high_resolution_clock::now(); t2 = std::chrono::high_resolution_clock::now();
std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl; std::cout << "lead: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
// EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(273ul, model->getNumberOfStates());
// EXPECT_EQ(397ul, model->getNumberOfTransitions()); EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate(); model = builder.translate();
t2 = std::chrono::high_resolution_clock::now(); t2 = std::chrono::high_resolution_clock::now();
std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl; std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
// EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(1728ul, model->getNumberOfStates());
// EXPECT_EQ(2505ul, model->getNumberOfTransitions()); EXPECT_EQ(2505ul, model->getNumberOfTransitions());
} }
TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = program.toJani(); storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel); storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
auto t1 = std::chrono::high_resolution_clock::now(); auto t1 = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate(); std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate();
auto t2 = std::chrono::high_resolution_clock::now(); auto t2 = std::chrono::high_resolution_clock::now();
std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl; std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(t2 - t1).count() << std::endl;
model->getTransitionMatrix().exportToDot("trans.dot");
std::cout << "nnz: " << model->getTransitionMatrix().getNonZeroCount() << std::endl;
std::cout << "nodes: " << model->getTransitionMatrix().getNodeCount() << std::endl;
std::cout << "vars: " << model->getTransitionMatrix().getContainedMetaVariables().size() << std::endl;
EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions()); EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();
@ -94,7 +88,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
EXPECT_EQ(867ul, model->getNumberOfTransitions()); EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();
@ -104,7 +98,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
EXPECT_EQ(15113ul, model->getNumberOfTransitions()); EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();
@ -114,7 +108,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
EXPECT_EQ(397ul, model->getNumberOfTransitions()); EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
janiModel = program.toJani(); janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel); builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
t1 = std::chrono::high_resolution_clock::now(); t1 = std::chrono::high_resolution_clock::now();
model = builder.translate(); model = builder.translate();

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

@ -57,10 +57,6 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program); std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
model->getTransitionMatrix().exportToDot("trans_prism.dot");
std::cout << "nnz: " << model->getTransitionMatrix().getNonZeroCount() << std::endl;
std::cout << "nodes: " << model->getTransitionMatrix().getNodeCount() << std::endl;
std::cout << "vars: " << model->getTransitionMatrix().getContainedMetaVariables().size() << std::endl;
EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions()); EXPECT_EQ(20ul, model->getNumberOfTransitions());

Write Preview
|||||||
100:0
Loading…
Cancel
Save