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<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.
storm::dd::Bdd<Type> 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<Type> identity = result.manager->getBddOne();
storm::dd::Bdd<Type> range = result.manager->getBddOne();
- // 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;
- 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>();
+ // Add the identity and ranges of the location variables to the ones of the automaton.
+ std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()];
+ 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>();
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<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) {
int_fast64_t low = variable.getLowerBound().evaluateAsInt();
int_fast64_t high = variable.getUpperBound().evaluateAsInt();
@@ -399,6 +405,14 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
EdgeDd<Type, ValueType> composeEdgesInParallel(EdgeDd<Type, ValueType> const& edge1, EdgeDd<Type, ValueType> const& edge2) {
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.
std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
@@ -494,6 +508,7 @@ namespace storm {
// First, consider all actions in the left subcomposition.
AutomatonDd<Type, ValueType> 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<Type, ValueType> 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<Type, ValueType> composer(*this->model, variables);
AutomatonDd<Type, ValueType> globalAutomaton = composer.compose();
-
+
// Combine the edges of the single automaton to the full system DD.
SystemDd<Type, ValueType> 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<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.template toAdd<ValueType>().exportToDot("reach.dot");
// Cut transitions to reachable states.
storm::dd::Add<Type, ValueType> reachableStatesAdd = modelComponents.reachableStates.template toAdd<ValueType>();
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<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 (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<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 (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<storm::dd::DdType::Sylvan, double> builder(janiModel);
auto t1 = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
auto t2 = std::chrono::high_resolution_clock::now();
std::cout << "die: " << std::chrono::duration_cast<std::chrono::milliseconds>(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<storm::dd::DdType::Sylvan, double>(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<std::chrono::milliseconds>(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<storm::dd::DdType::Sylvan, double>(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<std::chrono::milliseconds>(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<storm::dd::DdType::Sylvan, double>(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<std::chrono::milliseconds>(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<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.translate();
t2 = std::chrono::high_resolution_clock::now();
std::cout << "nand: " << std::chrono::duration_cast<std::chrono::milliseconds>(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<storm::dd::DdType::CUDD, double> builder(janiModel);
auto t1 = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.translate();
auto t2 = std::chrono::high_resolution_clock::now();
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(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<storm::dd::DdType::CUDD, double>(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<storm::dd::DdType::CUDD, double>(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<storm::dd::DdType::CUDD, double>(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<storm::dd::DdType::CUDD, double>(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<std::chrono::milliseconds>(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<storm::dd::DdType::Sylvan>().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<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(20ul, model->getNumberOfTransitions());
@@ -68,7 +64,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
@@ -78,7 +74,7 @@ TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().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<storm::dd::DdType::CUDD>().translateProgram(program);
EXPECT_EQ(1728ul, model->getNumberOfStates());