From c4327e91a969caeef3a3f985b24ddf922d3f6117 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 30 May 2016 20:59:54 +0200 Subject: [PATCH] more work on symbolic JANI model builder Former-commit-id: 4fe002c4f8d6d0e80f8cd2cf5d09540e4fadc229 --- src/adapters/AddExpressionAdapter.cpp | 6 +- src/adapters/AddExpressionAdapter.h | 6 +- src/builder/DdJaniModelBuilder.cpp | 44 +++++---- src/builder/DdPrismModelBuilder.cpp | 26 ++--- src/storage/jani/Model.cpp | 5 +- src/storage/jani/VariableSet.cpp | 19 +++- src/storage/jani/VariableSet.h | 4 - src/storage/prism/Program.cpp | 3 + .../builder/DdJaniModelBuilderTest.cpp | 94 +++++++++++++++++-- .../builder/DdPrismModelBuilderTest.cpp | 15 +++ 10 files changed, 168 insertions(+), 54 deletions(-) diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index 84e48e8a6..e50620db8 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -12,7 +12,7 @@ namespace storm { namespace adapters { template - AddExpressionAdapter::AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { + AddExpressionAdapter::AddExpressionAdapter(std::shared_ptr> ddManager, std::shared_ptr> const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { // Intentionally left empty. } @@ -140,8 +140,8 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { - auto const& variablePair = variableMapping.find(expression.getVariable()); - STORM_LOG_THROW(variablePair != variableMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); + auto const& variablePair = variableMapping->find(expression.getVariable()); + STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); if (expression.hasBooleanType()) { return ddManager->template getIdentity(variablePair->second).toBdd(); } else { diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h index ad82146f3..89d825d96 100644 --- a/src/adapters/AddExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -1,6 +1,8 @@ #ifndef STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_ #define STORM_ADAPTERS_DDEXPRESSIONADAPTER_H_ +#include + #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expressions.h" #include "src/storage/expressions/ExpressionVisitor.h" @@ -15,7 +17,7 @@ namespace storm { template class AddExpressionAdapter : public storm::expressions::ExpressionVisitor { public: - AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping); + AddExpressionAdapter(std::shared_ptr> ddManager, std::shared_ptr> const& variableMapping); storm::dd::Add translateExpression(storm::expressions::Expression const& expression); storm::dd::Bdd translateBooleanExpression(storm::expressions::Expression const& expression); @@ -36,7 +38,7 @@ namespace storm { std::shared_ptr> ddManager; // This member maps the variables used in the expressions to the variables used by the DD manager. - std::map variableMapping; + std::shared_ptr> variableMapping; }; } // namespace adapters diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 3a46a36c5..a2b29f34b 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -130,7 +130,11 @@ namespace storm { template struct CompositionVariables { - CompositionVariables() : manager(std::make_shared>()) { + CompositionVariables() : manager(std::make_shared>()), + variableToRowMetaVariableMap(std::make_shared>()), + rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), + variableToColumnMetaVariableMap(std::make_shared>()), + columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)) { // Intentionally left empty. } @@ -138,12 +142,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; - std::map variableToRowMetaVariableMap; + std::shared_ptr> variableToRowMetaVariableMap; std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; - std::map variableToColumnMetaVariableMap; + std::shared_ptr> variableToColumnMetaVariableMap; std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. @@ -197,7 +201,7 @@ namespace storm { boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { auto it = automata.find(composition.getAutomatonName()); - STORM_LOG_THROW(it != automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the same automaton multiple times."); + STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times."); automata.insert(it, composition.getAutomatonName()); return boost::none; } @@ -218,14 +222,16 @@ namespace storm { CompositionVariables result; for (auto const& action : this->model.getActions()) { - std::pair variablePair = result.manager->addMetaVariable(action.getName()); - result.actionVariables.push_back(variablePair.first); + if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) { + std::pair variablePair = result.manager->addMetaVariable(action.getName()); + result.actionVariables.push_back(variablePair.first); + } } // FIXME: check how many nondeterminism variables we should actually allocate. uint64_t numberOfNondeterminismVariables = this->model.getNumberOfAutomata(); for (auto const& automaton : this->model.getAutomata()) { - numberOfNondeterminismVariables *= automaton.getNumberOfEdges(); + numberOfNondeterminismVariables += automaton.getNumberOfEdges(); } for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { std::pair variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i)); @@ -256,12 +262,12 @@ namespace storm { 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())); + range &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable())); } for (auto const& variable : automaton.getVariables().getBooleanVariables()) { createVariable(variable, result); 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())); } result.automatonToIdentityMap[automaton.getName()] = identity.template toAdd(); @@ -279,10 +285,10 @@ namespace storm { STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "] and " << variablePair.second.getName() << "."); result.rowMetaVariables.insert(variablePair.first); - result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first); + result.variableToRowMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.first); result.columnMetaVariables.insert(variablePair.second); - result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second); + result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second); 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(); result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity); @@ -297,10 +303,10 @@ namespace storm { STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << "."); result.rowMetaVariables.insert(variablePair.first); - result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first); + result.variableToRowMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.first); result.columnMetaVariables.insert(variablePair.second); - result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second); + result.variableToColumnMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.second); storm::dd::Add variableIdentity = result.manager->template getIdentity(variablePair.first).equals(result.manager->template getIdentity(variablePair.second)).template toAdd(); result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity); @@ -326,11 +332,11 @@ namespace storm { // This structure represents an edge. template struct EdgeDd { - EdgeDd(storm::dd::Add const& guardDd = storm::dd::Add(), storm::dd::Add const& transitionsDd = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) { + EdgeDd(storm::dd::Add const& guardDd = storm::dd::Add(), storm::dd::Add const& transitionsDd = storm::dd::Add(), std::set const& writtenGlobalVariables = {}, std::set const& globalVariablesWrittenMultipleTimes = {}) : guardDd(guardDd), transitionsDd(transitionsDd), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) { // Intentionally left empty. } - EdgeDd(EdgeDd const& other) : globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes), writtenGlobalVariables(other.writtenGlobalVariables), guardDd(other.guardDd), transitionsDd(other.transitionsDd) { + EdgeDd(EdgeDd const& other) : guardDd(other.guardDd), transitionsDd(other.transitionsDd), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) { // Intentionally left empty. } @@ -344,10 +350,10 @@ namespace storm { return *this; } - std::set globalVariablesWrittenMultipleTimes; - std::set writtenGlobalVariables; storm::dd::Add guardDd; storm::dd::Add transitionsDd; + std::set writtenGlobalVariables; + std::set globalVariablesWrittenMultipleTimes; }; // This structure represents a subcomponent of a composition. @@ -509,11 +515,11 @@ namespace storm { std::set assignedVariables; for (auto const& assignment : destination.getAssignments()) { // Record the variable as being written. - STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap.at(assignment.getExpressionVariable()).getName()); + STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName()); assignedVariables.insert(assignment.getExpressionVariable()); // Translate the written variable. - auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap.at(assignment.getExpressionVariable()); + auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap->at(assignment.getExpressionVariable()); storm::dd::Add writtenVariable = variables.manager->template getIdentity(primedMetaVariable); // Translate the expression that is being assigned. diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index b013735d9..39a425380 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -31,7 +31,7 @@ namespace storm { template class DdPrismModelBuilder::GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); @@ -47,12 +47,12 @@ namespace storm { // The meta variables for the row encoding. std::set rowMetaVariables; - std::map variableToRowMetaVariableMap; + std::shared_ptr> variableToRowMetaVariableMap; std::shared_ptr> rowExpressionAdapter; // The meta variables for the column encoding. std::set columnMetaVariables; - std::map variableToColumnMetaVariableMap; + std::shared_ptr> variableToColumnMetaVariableMap; std::shared_ptr> columnExpressionAdapter; // All pairs of row/column meta variables. @@ -116,10 +116,10 @@ namespace storm { STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + variableToRowMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.first); columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); + variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second); storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); @@ -133,10 +133,10 @@ namespace storm { STORM_LOG_TRACE("Created meta variables for global 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); + variableToRowMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.first); columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second); storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd(); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); @@ -157,10 +157,10 @@ namespace storm { STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + variableToRowMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.first); columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); + variableToColumnMetaVariableMap->emplace(integerVariable.getExpressionVariable(), variablePair.second); storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); @@ -174,10 +174,10 @@ namespace storm { 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); + variableToRowMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.first); columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second); storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); @@ -591,11 +591,11 @@ namespace storm { std::set assignedVariables; for (auto const& assignment : assignments) { // Record the variable as being written. - STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap.at(assignment.getVariable()).getName()); + STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap->at(assignment.getVariable()).getName()); assignedVariables.insert(assignment.getVariable()); // Translate the written variable. - auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap.at(assignment.getVariable()); + auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap->at(assignment.getVariable()); storm::dd::Add writtenVariable = generationInfo.manager->template getIdentity(primedMetaVariable); // Translate the expression that is being assigned. diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 1d976d084..dc5c4f352 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -170,6 +170,10 @@ namespace storm { return *composition; } + void Model::setSystemComposition(std::shared_ptr const& composition) { + this->composition = composition; + } + std::set Model::getActionNames(bool includeSilent) const { std::set result; for (auto const& entry : actionToIndex) { @@ -257,7 +261,6 @@ namespace storm { // Substitute constants in all global variables. for (auto& variable : result.getGlobalVariables()) { - std::cout << "init: " << variable.getInitialValue() << std::endl; variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution)); } for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) { diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp index e3e183558..e7f2b42b7 100644 --- a/src/storage/jani/VariableSet.cpp +++ b/src/storage/jani/VariableSet.cpp @@ -36,12 +36,12 @@ namespace storm { template typename ConstVariables::const_iterator ConstVariables::begin() { - return boost::make_transform_iterator(it, Dereferencer()); + return boost::make_transform_iterator(it, Dereferencer()); } template typename ConstVariables::const_iterator ConstVariables::end() { - return boost::make_transform_iterator(ite, Dereferencer()); + return boost::make_transform_iterator(ite, Dereferencer()); } } @@ -148,6 +148,21 @@ namespace storm { bool VariableSet::containsUnboundedIntegerVariables() const { return !unboundedIntegerVariables.empty(); } + + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Dereferencer; + template class detail::Variables; + template class detail::Variables; + template class detail::Variables; + template class detail::ConstVariables; + template class detail::ConstVariables; + template class detail::ConstVariables; } } diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h index 8d5aa3aed..eeedcdc6f 100644 --- a/src/storage/jani/VariableSet.h +++ b/src/storage/jani/VariableSet.h @@ -26,9 +26,7 @@ namespace storm { class Variables { public: typedef typename std::vector>::iterator input_iterator; - typedef typename std::vector>::const_iterator const_input_iterator; typedef boost::transform_iterator, input_iterator> iterator; - typedef boost::transform_iterator, const_input_iterator> const_iterator; Variables(input_iterator it, input_iterator ite); @@ -43,9 +41,7 @@ namespace storm { template class ConstVariables { public: - typedef typename std::vector>::iterator input_iterator; typedef typename std::vector>::const_iterator const_input_iterator; - typedef boost::transform_iterator, input_iterator> iterator; typedef boost::transform_iterator, const_input_iterator> const_iterator; ConstVariables(const_input_iterator it, const_input_iterator ite); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 42cd1eb8a..711f68ad8 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1610,6 +1610,9 @@ namespace storm { janiModel.addAutomaton(automaton); } + // Set the standard system composition. This is possible, because we reject non-standard compositions anyway. + janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); + return janiModel; } diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 6b73c1a59..486a1b26e 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -16,34 +16,108 @@ TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) { storm::jani::Model janiModel = program.toJani(); storm::builder::DdJaniModelBuilder builder(janiModel); + auto t1 = std::chrono::high_resolution_clock::now(); std::shared_ptr> model = builder.translate(); - EXPECT_EQ(13ul, model->getNumberOfStates()); - EXPECT_EQ(20ul, model->getNumberOfTransitions()); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); janiModel = program.toJani(); 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()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + janiModel = program.toJani(); + 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()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + janiModel = program.toJani(); + 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()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + janiModel = program.toJani(); + + 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()); +} + +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::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()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + janiModel = program.toJani(); + builder = storm::builder::DdJaniModelBuilder(janiModel); + t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); - EXPECT_EQ(677ul, model->getNumberOfStates()); - EXPECT_EQ(867ul, model->getNumberOfTransitions()); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); janiModel = program.toJani(); + builder = storm::builder::DdJaniModelBuilder(janiModel); + t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); - EXPECT_EQ(8607ul, model->getNumberOfStates()); - EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); janiModel = program.toJani(); + builder = storm::builder::DdJaniModelBuilder(janiModel); + t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); - EXPECT_EQ(273ul, model->getNumberOfStates()); - EXPECT_EQ(397ul, model->getNumberOfTransitions()); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); janiModel = program.toJani(); + builder = storm::builder::DdJaniModelBuilder(janiModel); + t1 = std::chrono::high_resolution_clock::now(); model = builder.translate(); - EXPECT_EQ(1728ul, model->getNumberOfStates()); - EXPECT_EQ(2505ul, model->getNumberOfTransitions()); + 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()); } //TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index b95039058..f89bb19ab 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -13,27 +13,42 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + auto t1 = std::chrono::high_resolution_clock::now(); std::shared_ptr> model = storm::builder::DdPrismModelBuilder().translateProgram(program); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + t1 = std::chrono::high_resolution_clock::now(); model = storm::builder::DdPrismModelBuilder().translateProgram(program); + 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()); 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); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + t1 = std::chrono::high_resolution_clock::now(); model = storm::builder::DdPrismModelBuilder().translateProgram(program); + 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()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + t1 = std::chrono::high_resolution_clock::now(); model = storm::builder::DdPrismModelBuilder().translateProgram(program); + 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()); }