From 7750480714ff12612609d9dd6b863bb2b7fc7f13 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 2 Jun 2016 15:21:25 +0200 Subject: [PATCH] JANI model builder for DTMCs working Former-commit-id: 25f12f3e05274d24fcbaa087633751dbcca8f7b5 --- src/builder/DdJaniModelBuilder.cpp | 71 +++++++++++-------- src/storage/jani/BooleanVariable.h | 2 +- src/storage/jani/BoundedIntegerVariable.h | 2 +- src/storage/prism/Program.cpp | 44 ++++++------ src/storage/prism/Program.h | 2 +- .../builder/DdJaniModelBuilderTest.cpp | 48 ++++++------- .../builder/DdPrismModelBuilderTest.cpp | 10 +-- 7 files changed, 92 insertions(+), 87 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 013f837dd..b2c76e174 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -252,13 +252,19 @@ namespace storm { 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 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. storm::dd::Bdd globalVariableRanges = result.manager->getBddOne(); - for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) { - createVariable(variable, result); - globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable())); - } - for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) { + for (auto const& variable : this->model.getGlobalVariables()) { createVariable(variable, result); globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable())); } @@ -269,24 +275,14 @@ namespace storm { storm::dd::Bdd identity = result.manager->getBddOne(); storm::dd::Bdd range = result.manager->getBddOne(); - // Start by creating a meta variable for the location of the automaton. - std::pair variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); - result.automatonToLocationVariableMap[automaton.getName()] = variablePair; - storm::dd::Add variableIdentity = result.manager->template getIdentity(variablePair.first).equals(result.manager->template getIdentity(variablePair.second)).template toAdd() * result.manager->getRange(variablePair.first).template toAdd() * result.manager->getRange(variablePair.second).template toAdd(); + // Add the identity and ranges of the location variables to the ones of the automaton. + std::pair const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()]; + storm::dd::Add variableIdentity = result.manager->template getIdentity(locationVariables.first).equals(result.manager->template getIdentity(locationVariables.second)).template toAdd() * result.manager->getRange(locationVariables.first).template toAdd() * result.manager->getRange(locationVariables.second).template toAdd(); identity &= variableIdentity.toBdd(); - range &= result.manager->getRange(variablePair.first); - - // Add the location variable to the row/column variables. - result.rowMetaVariables.insert(variablePair.first); - result.columnMetaVariables.insert(variablePair.second); + range &= result.manager->getRange(locationVariables.first); // Then create variables for the variables of the automaton. - for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - 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()) { + 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())); @@ -299,6 +295,16 @@ namespace storm { return result; } + void createVariable(storm::jani::Variable const& variable, CompositionVariables& 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& result) { int_fast64_t low = variable.getLowerBound().evaluateAsInt(); int_fast64_t high = variable.getUpperBound().evaluateAsInt(); @@ -399,6 +405,14 @@ namespace storm { template EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) { EdgeDd 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(); + } // Compute the set of variables written multiple times by the composition. std::set oldVariablesWrittenMultipleTimes; @@ -494,6 +508,7 @@ namespace storm { // First, consider all actions in the left subcomposition. AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity); + uint64_t index = 0; for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) { // If we need to synchronize over this action, do so now. if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) { @@ -501,7 +516,11 @@ namespace storm { if (rightIt != rightSubautomaton.actionIndexToEdges.end()) { for (auto const& edge1 : actionEdges.second) { for (auto const& edge2 : rightIt->second) { - result.actionIndexToEdges[actionEdges.first].push_back(composeEdgesInParallel(edge1, edge2)); + EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2); + if (!edgeDd.guardDd.isZero()) { + result.actionIndexToEdges[actionEdges.first].push_back(edgeDd); + } + index++; } } } @@ -900,10 +919,10 @@ namespace storm { // Compose the automata to a single automaton. AutomatonComposer composer(*this->model, variables); AutomatonDd globalAutomaton = composer.compose(); - + // Combine the edges of the single automaton to the full system DD. SystemDd system = buildSystemDd(*this->model, globalAutomaton, variables); - + // Postprocess the system. This modifies the systemDd in place. postprocessSystemAndVariables(*this->model, system, variables, options); @@ -918,19 +937,15 @@ namespace storm { if (this->model->getModelType() == storm::jani::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.nondeterminismVariables); } - transitionMatrixBdd.template toAdd().exportToDot("trans_before_reach.dot"); - modelComponents.initialStates.template toAdd().exportToDot("initial.dot"); modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); - modelComponents.reachableStates.template toAdd().exportToDot("reach.dot"); // Cut transitions to reachable states. storm::dd::Add reachableStatesAdd = modelComponents.reachableStates.template toAdd(); modelComponents.transitionMatrix = system.transitionsDd * reachableStatesAdd; - system.transitionsDd.exportToDot("trans_full.dot"); system.stateActionDd *= reachableStatesAdd; // 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. return createModel(this->model->getModelType(), variables, modelComponents); diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 4e6f5d504..eacff6fb4 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -12,7 +12,7 @@ namespace storm { */ BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); - virtual bool isBooleanVariable() const; + virtual bool isBooleanVariable() const override; }; } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 16f7f6eb5..43212992c 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -33,7 +33,7 @@ namespace storm { */ void setUpperBound(storm::expressions::Expression const& expression); - virtual bool isBoundedIntegerVariable() const; + virtual bool isBoundedIntegerVariable() const override; private: // The expression defining the lower bound of the variable. diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index ef0b32909..44a61d7f7 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1475,7 +1475,7 @@ namespace storm { 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."); // 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. - 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) { janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); 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. for (auto const& action : indexToActionMap) { @@ -1552,33 +1552,33 @@ namespace storm { storm::jani::Automaton automaton(module.getName()); storm::expressions::Expression initialStatesExpression; - for (auto const& variable : module.getBooleanVariables()) { - storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable()); + for (auto const& variable : module.getIntegerVariables()) { + storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); std::set 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 (accessingModuleIndices.size() == 1) { - automaton.addBooleanVariable(newBooleanVariable); - storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { + automaton.addBoundedIntegerVariable(newIntegerVariable); + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; - } else if (accessingModuleIndices.size() > 1) { + } else { // if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. - janiModel.addBooleanVariable(newBooleanVariable); - storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + janiModel.addBoundedIntegerVariable(newIntegerVariable); + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; } } - for (auto const& variable : module.getIntegerVariables()) { - storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); + for (auto const& variable : module.getBooleanVariables()) { + storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable()); std::set 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 (accessingModuleIndices.size() == 1) { - automaton.addBoundedIntegerVariable(newIntegerVariable); - storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + if (!allVariablesGlobal && accessingModuleIndices.size() == 1) { + automaton.addBooleanVariable(newBooleanVariable); + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; - } else if (accessingModuleIndices.size() > 1) { + } else { //if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. - janiModel.addBoundedIntegerVariable(newIntegerVariable); - storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + janiModel.addBooleanVariable(newBooleanVariable); + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; } } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 02732f74d..cf0445503 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -558,7 +558,7 @@ namespace storm { /*! * Converts the PRISM model into an equivalent JANI model. */ - storm::jani::Model toJani() const; + storm::jani::Model toJani(bool allVariablesGlobal = false) const; private: /*! diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 732d2aae1..1fe2d7e47 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -13,78 +13,72 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { 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 builder(janiModel); auto t1 = std::chrono::high_resolution_clock::now(); std::shared_ptr> model = builder.translate(); auto t2 = std::chrono::high_resolution_clock::now(); std::cout << "die: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; - -// EXPECT_EQ(13ul, model->getNumberOfStates()); -// EXPECT_EQ(20ul, model->getNumberOfTransitions()); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "brp: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; -// EXPECT_EQ(677ul, model->getNumberOfStates()); -// EXPECT_EQ(867ul, model->getNumberOfTransitions()); - + EXPECT_EQ(677ul, model->getNumberOfStates()); + EXPECT_EQ(867ul, model->getNumberOfTransitions()); + 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "crowds: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; -// EXPECT_EQ(8607ul, model->getNumberOfStates()); -// EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + EXPECT_EQ(8607ul, model->getNumberOfStates()); + EXPECT_EQ(15113ul, model->getNumberOfTransitions()); 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "lead: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; -// EXPECT_EQ(273ul, model->getNumberOfStates()); -// EXPECT_EQ(397ul, model->getNumberOfTransitions()); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); 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(); builder = storm::builder::DdJaniModelBuilder(janiModel); model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "nand: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; -// EXPECT_EQ(1728ul, model->getNumberOfStates()); -// EXPECT_EQ(2505ul, model->getNumberOfTransitions()); + EXPECT_EQ(1728ul, model->getNumberOfStates()); + EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { 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 builder(janiModel); auto t1 = std::chrono::high_resolution_clock::now(); std::shared_ptr> model = builder.translate(); auto t2 = std::chrono::high_resolution_clock::now(); std::cout << "die: " << std::chrono::duration_cast(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(20ul, model->getNumberOfTransitions()); 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); @@ -94,7 +88,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { EXPECT_EQ(867ul, model->getNumberOfTransitions()); 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); @@ -104,7 +98,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { EXPECT_EQ(15113ul, model->getNumberOfTransitions()); 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); @@ -114,7 +108,7 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { EXPECT_EQ(397ul, model->getNumberOfTransitions()); 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(janiModel); t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index 4cd262a6f..dc78c5c59 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -27,7 +27,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { std::cout << "brp: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); t1 = std::chrono::high_resolution_clock::now(); model = storm::builder::DdPrismModelBuilder().translateProgram(program); @@ -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"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().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(20ul, model->getNumberOfTransitions()); @@ -68,7 +64,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { model = storm::builder::DdPrismModelBuilder().translateProgram(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); model = storm::builder::DdPrismModelBuilder().translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); @@ -78,7 +74,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { model = storm::builder::DdPrismModelBuilder().translateProgram(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); model = storm::builder::DdPrismModelBuilder().translateProgram(program); EXPECT_EQ(1728ul, model->getNumberOfStates());