From d787b80fec2f6644c02f6ff948e6a52001c0df7d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 31 Mar 2015 20:01:20 +0200
Subject: [PATCH] CTMC examples now build properly using the DD-based model
generator.
Former-commit-id: ac97b005e3b94240f3c295057928f891247a66b2
---
resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h | 5 +
.../cudd-2.5.0/src/cudd/cuddAddApply.c | 171 ++++++++++++++++++
.../3rdparty/cudd-2.5.0/src/obj/cuddObj.cc | 51 ++++++
.../3rdparty/cudd-2.5.0/src/obj/cuddObj.hh | 5 +
src/adapters/AddExpressionAdapter.cpp | 9 +
src/models/symbolic/Model.cpp | 2 +-
src/models/symbolic/NondeterministicModel.cpp | 16 +-
src/settings/modules/GeneralSettings.cpp | 4 +
src/settings/modules/GeneralSettings.h | 9 +
src/storage/dd/CuddAdd.cpp | 26 +++
src/storage/dd/CuddAdd.h | 39 ++++
.../builder/DdPrismModelBuilderTest.cpp | 33 +++-
.../builder/ExplicitPrismModelBuilderTest.cpp | 5 +-
.../GmmxxCtmcCslModelCheckerTest.cpp | 17 +-
.../SparseCtmcCslModelCheckerTest.cpp | 17 +-
15 files changed, 403 insertions(+), 6 deletions(-)
diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
index 51d509b35..bba6713d2 100644
--- a/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
+++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
@@ -792,8 +792,13 @@ extern DdNode * Cudd_addGreaterThan (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addGreaterThanEquals (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addLessThan (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addLessThanEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addPow (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addMod (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addLogXY (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
+extern DdNode * Cudd_addFloor (DdManager * dd, DdNode * f);
+extern DdNode * Cudd_addCeil (DdManager * dd, DdNode * f);
extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addNotEquals (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addGreaterThan (DdManager *dd, DdNode **f, DdNode **g);
diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c
index 9a4d2179d..fc1ab8c15 100644
--- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c
+++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddApply.c
@@ -783,6 +783,59 @@ Cudd_addLog(
} /* end of Cudd_addLog */
+/**Function********************************************************************
+
+ Synopsis [Floor of an ADD.]
+
+ Description [Floor of an ADD. Returns NULL
+ if not a terminal case; floor(f) otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addMonadicApply]
+
+ ******************************************************************************/
+DdNode *
+Cudd_addFloor(
+ DdManager * dd,
+ DdNode * f)
+{
+ if (cuddIsConstant(f)) {
+ CUDD_VALUE_TYPE value = floor(cuddV(f));
+ DdNode *res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addFloor */
+
+
+/**Function********************************************************************
+
+ Synopsis [Ceiling of an ADD.]
+
+ Description [Ceiling of an ADD. Returns NULL
+ if not a terminal case; ceil(f) otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addMonadicApply]
+
+ ******************************************************************************/
+DdNode *
+Cudd_addCeil(
+ DdManager * dd,
+ DdNode * f)
+{
+ if (cuddIsConstant(f)) {
+ CUDD_VALUE_TYPE value = ceil(cuddV(f));
+ DdNode *res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addCeiling */
+
/**Function********************************************************************
Synopsis [1 if f==g; 0 otherwise.]
@@ -964,6 +1017,124 @@ Cudd_addLessThanEquals(
return(NULL);
} /* end of Cudd_addLessThanEquals */
+
+/**Function********************************************************************
+
+ Synopsis [f to the power of g.]
+
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is f to the power of g.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addApply]
+
+ ******************************************************************************/
+DdNode *
+Cudd_addPow(
+ DdManager * dd,
+ DdNode ** f,
+ DdNode ** g)
+{
+ DdNode *res;
+ DdNode *F, *G;
+ CUDD_VALUE_TYPE value;
+
+ F = *f; G = *g;
+ if (G == DD_ZERO(dd)) return(DD_ONE(dd));
+ if (cuddIsConstant(F) && cuddIsConstant(G)) {
+ value = pow(cuddV(F), cuddV(G));
+ res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addPow */
+
+
+/**Function********************************************************************
+
+ Synopsis [f modulo g.]
+
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is f modulo g.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addApply]
+
+ ******************************************************************************/
+DdNode *
+Cudd_addMod(
+ DdManager * dd,
+ DdNode ** f,
+ DdNode ** g)
+{
+ DdNode *res;
+ DdNode *F, *G;
+ int rem;
+ CUDD_VALUE_TYPE value;
+
+ F = *f; G = *g;
+ if (cuddIsConstant(F) && cuddIsConstant(G)) {
+ // If g is <=0, then result is NaN
+ if (cuddV(G) <= 0) value = (0.0/0.0);
+ // Take care of negative case (% is remainder, not modulo)
+ else {
+ rem = ((int)cuddV(F) % (int)cuddV(G));
+ if (rem < 0) rem += (int)cuddV(G);
+ value = rem;
+ }
+ // Create/return result
+ res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addMod */
+
+
+/**Function********************************************************************
+
+ Synopsis [log f base g.]
+
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is log f base g.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addApply]
+
+ ******************************************************************************/
+DdNode *
+Cudd_addLogXY(
+ DdManager * dd,
+ DdNode ** f,
+ DdNode ** g)
+{
+ DdNode *res;
+ DdNode *F, *G;
+ CUDD_VALUE_TYPE value;
+
+ F = *f; G = *g;
+ if (cuddIsConstant(F) && cuddIsConstant(G)) {
+ // If base is <=0 or ==1 (or +Inf/NaN), then result is NaN
+ if (cuddV(G) <= 0 || cuddV(G) == 1.0 || G==DD_PLUS_INFINITY(dd) || cuddV(G) != cuddV(G)) value = (0.0/0.0);
+ // If arg is <0 or NaN, then result is NaN
+ else if (cuddV(F) < 0 || cuddV(F) != cuddV(F)) value = (0.0/0.0);
+ // If arg is +Inf, then result is +Inf
+ else if (F==DD_PLUS_INFINITY(dd)) return DD_PLUS_INFINITY(dd);
+ // If arg is (positive/negative) 0, then result is -Inf
+ else if (cuddV(F) == 0.0 || cuddV(F) == -0.0) return DD_MINUS_INFINITY(dd);
+ // Default case: normal log
+ else value = log(cuddV(F)) / log(cuddV(G));
+ // Create/return result
+ res = cuddUniqueConst(dd,value);
+ return(res);
+ }
+ return(NULL);
+
+} /* end of Cudd_addLogXY */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
index fcec76782..3262108aa 100644
--- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
+++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
@@ -2614,6 +2614,38 @@ ADD::Xnor(
} // ADD::Xnor
+ADD
+ADD::Pow(
+ const ADD& g) const
+{
+ DdManager *mgr = checkSameManager(g);
+ DdNode *result = Cudd_addApply(mgr, Cudd_addPow, node, g.node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::Pow
+
+ADD
+ADD::Mod(
+ const ADD& g) const
+{
+ DdManager *mgr = checkSameManager(g);
+ DdNode *result = Cudd_addApply(mgr, Cudd_addMod, node, g.node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::Mod
+
+ADD
+ADD::LogXY(
+ const ADD& g) const
+{
+ DdManager *mgr = checkSameManager(g);
+ DdNode *result = Cudd_addApply(mgr, Cudd_addLogXY, node, g.node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::LogXY
ADD
ADD::Log() const
@@ -2625,6 +2657,25 @@ ADD::Log() const
} // ADD::Log
+ADD
+ADD::Floor() const
+{
+ DdManager *mgr = p->manager;
+ DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addFloor, node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::Floor
+
+ADD
+ADD::Ceil() const
+{
+ DdManager *mgr = p->manager;
+ DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addCeil, node);
+ checkReturnValue(result);
+ return ADD(p, result);
+
+} // ADD::Ceil
ADD
ADD::FindMax() const
diff --git a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh
index 1162a968c..0b5acf051 100644
--- a/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh
+++ b/resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh
@@ -392,7 +392,12 @@ public:
ADD Nor(const ADD& g) const;
ADD Xor(const ADD& g) const;
ADD Xnor(const ADD& g) const;
+ ADD Pow(const ADD& g) const;
+ ADD Mod(const ADD& g) const;
+ ADD LogXY(const ADD& g) const;
ADD Log() const;
+ ADD Floor() const;
+ ADD Ceil() const;
ADD FindMax() const;
ADD FindMin() const;
ADD IthBit(int bit) const;
diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp
index 12677b85e..284ff0b6b 100644
--- a/src/adapters/AddExpressionAdapter.cpp
+++ b/src/adapters/AddExpressionAdapter.cpp
@@ -78,6 +78,9 @@ namespace storm {
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
result = leftResult.minimum(rightResult);
break;
+ case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Power:
+ result = leftResult.pow(rightResult);
+ break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate expression containing power operator.");
}
@@ -143,6 +146,12 @@ namespace storm {
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
result = -result;
break;
+ case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor:
+ result = result.floor();
+ break;
+ case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:
+ result = result.ceil();
+ break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate expression containing floor/ceil operator.");
}
diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp
index 9f67ec7bd..07b9fda9f 100644
--- a/src/models/symbolic/Model.cpp
+++ b/src/models/symbolic/Model.cpp
@@ -148,7 +148,7 @@ namespace storm {
columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
}
- out << "Variables: \t" << "rows: " << this->rowVariables.size() << "(" << rowVariableCount << " dd variables)" << ", columns: " << this->columnVariables.size() << "(" << columnVariableCount << " dd variables)" << std::endl;
+ out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)" << std::endl;
out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl;
for (auto const& label : labelToExpressionMap) {
out << " * " << label.first << std::endl;
diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp
index 5572c3fe2..64b4cf6bc 100644
--- a/src/models/symbolic/NondeterministicModel.cpp
+++ b/src/models/symbolic/NondeterministicModel.cpp
@@ -52,7 +52,21 @@ namespace storm {
out << "States: \t" << this->getNumberOfStates() << " (" << this->getReachableStates().getNodeCount() << " nodes)" << std::endl;
out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << this->getTransitionMatrix().getNodeCount() << " nodes)" << std::endl;
out << "Choices: \t" << this->getNumberOfChoices() << std::endl;
- out << "Variables: \t" << "rows: " << this->getRowVariables().size() << ", columns: " << this->getColumnVariables().size() << ", nondeterminism: " << this->getNondeterminismVariables().size() << std::endl;
+
+ uint_fast64_t rowVariableCount = 0;
+ for (auto const& metaVariable : this->getRowVariables()) {
+ rowVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
+ }
+ uint_fast64_t columnVariableCount = 0;
+ for (auto const& metaVariable : this->getColumnVariables()) {
+ columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
+ }
+ uint_fast64_t nondeterminismVariableCount = 0;
+ for (auto const& metaVariable : this->getNondeterminismVariables()) {
+ nondeterminismVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables();
+ }
+
+ out << "Variables: \t" << "rows: " << this->getRowVariables().size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->getColumnVariables().size() << "meta variables (" << columnVariableCount << " DD variables), nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)" << std::endl;
out << "Labels: \t" << this->getLabelToExpressionMap().size() << std::endl;
for (auto const& label : this->getLabelToExpressionMap()) {
out << " * " << label.first << std::endl;
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 2f2ce0dbc..2d2d48eee 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -218,6 +218,10 @@ namespace storm {
return this->overrideOption(dontFixDeadlockOptionName, stateToSet);
}
+ std::unique_ptr<storm::settings::SettingMemento> GeneralSettings::overridePrismCompatibilityMode(bool stateToSet) {
+ return this->overrideOption(prismCompatibilityOptionName, stateToSet);
+ }
+
bool GeneralSettings::isTimeoutSet() const {
return this->getOption(timeoutOptionName).getHasOptionBeenSet();
}
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 23e98c8bf..8cab2e14f 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -234,6 +234,15 @@ namespace storm {
*/
std::unique_ptr<storm::settings::SettingMemento> overrideDontFixDeadlocksSet(bool stateToSet);
+ /*!
+ * Overrides the option to enable the PRISM compatibility mode by setting it to the specified value. As
+ * soon as the returned memento goes out of scope, the original value is restored.
+ *
+ * @param stateToSet The value that is to be set for the option.
+ * @return The memento that will eventually restore the original value.
+ */
+ std::unique_ptr<storm::settings::SettingMemento> overridePrismCompatibilityMode(bool stateToSet);
+
/*!
* Retrieves whether the timeout option was set.
*
diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp
index cc04c5f76..3d3695d15 100644
--- a/src/storage/dd/CuddAdd.cpp
+++ b/src/storage/dd/CuddAdd.cpp
@@ -150,6 +150,32 @@ namespace storm {
return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables);
}
+ Add<DdType::CUDD> Add<DdType::CUDD>::pow(Add<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables;
+ std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
+ return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Pow(other.getCuddAdd()), metaVariables);
+ }
+
+ Add<DdType::CUDD> Add<DdType::CUDD>::mod(Add<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables;
+ std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
+ return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Mod(other.getCuddAdd()), metaVariables);
+ }
+
+ Add<DdType::CUDD> Add<DdType::CUDD>::logxy(Add<DdType::CUDD> const& other) const {
+ std::set<storm::expressions::Variable> metaVariables;
+ std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
+ return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LogXY(other.getCuddAdd()), metaVariables);
+ }
+
+ Add<DdType::CUDD> Add<DdType::CUDD>::floor() const {
+ return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Floor(), this->getContainedMetaVariables());
+ }
+
+ Add<DdType::CUDD> Add<DdType::CUDD>::ceil() const {
+ return Add<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ceil(), this->getContainedMetaVariables());
+ }
+
Add<DdType::CUDD> Add<DdType::CUDD>::minimum(Add<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h
index a43738d85..02142705e 100644
--- a/src/storage/dd/CuddAdd.h
+++ b/src/storage/dd/CuddAdd.h
@@ -211,6 +211,45 @@ namespace storm {
* @return The resulting function represented as an ADD.
*/
Add<DdType::CUDD> greaterOrEqual(Add<DdType::CUDD> const& other) const;
+
+ /*!
+ * Retrieves the function that represents the current ADD to the power of the given ADD.
+ *
+ * @other The exponent function (given as an ADD).
+ * @retur The resulting ADD.
+ */
+ Add<DdType::CUDD> pow(Add<DdType::CUDD> const& other) const;
+
+ /*!
+ * Retrieves the function that represents the current ADD modulo the given ADD.
+ *
+ * @other The modul function (given as an ADD).
+ * @retur The resulting ADD.
+ */
+ Add<DdType::CUDD> mod(Add<DdType::CUDD> const& other) const;
+
+ /*!
+ * Retrieves the function that represents the logarithm of the current ADD to the bases given by the second
+ * ADD.
+ *
+ * @other The base function (given as an ADD).
+ * @retur The resulting ADD.
+ */
+ Add<DdType::CUDD> logxy(Add<DdType::CUDD> const& other) const;
+
+ /*!
+ * Retrieves the function that floors all values in the current ADD.
+ *
+ * @retur The resulting ADD.
+ */
+ Add<DdType::CUDD> floor() const;
+
+ /*!
+ * Retrieves the function that ceils all values in the current ADD.
+ *
+ * @retur The resulting ADD.
+ */
+ Add<DdType::CUDD> ceil() const;
/*!
* Retrieves the function that maps all evaluations to the minimum of the function values of the two ADDs.
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index 20dfb8361..ea88d24f1 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -1,6 +1,6 @@
#include "gtest/gtest.h"
#include "storm-config.h"
-
+#include "src/settings/SettingMemento.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Mdp.h"
#include "src/storage/dd/CuddDd.h"
@@ -35,6 +35,37 @@ TEST(DdPrismModelBuilderTest, Dtmc) {
EXPECT_EQ(2505, model->getNumberOfTransitions());
}
+TEST(DdPrismModelBuilderTest, Ctmc) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ EXPECT_EQ(276, model->getNumberOfStates());
+ EXPECT_EQ(1120, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ EXPECT_EQ(3478, model->getNumberOfStates());
+ EXPECT_EQ(14639, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ EXPECT_EQ(12, model->getNumberOfStates());
+ EXPECT_EQ(22, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ EXPECT_EQ(810, model->getNumberOfStates());
+ EXPECT_EQ(3699, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ EXPECT_EQ(66, model->getNumberOfStates());
+ EXPECT_EQ(189, model->getNumberOfTransitions());
+}
+
TEST(DdPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index 7e7599246..bf4ee90d8 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -1,6 +1,6 @@
#include "gtest/gtest.h"
#include "storm-config.h"
-
+#include "src/settings/SettingMemento.h"
#include "src/parser/PrismParser.h"
#include "src/builder/ExplicitPrismModelBuilder.h"
@@ -33,6 +33,9 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) {
}
TEST(ExplicitPrismModelBuilderTest, Ctmc) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index 0ad32ceaf..6a814d63d 100644
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -1,6 +1,6 @@
#include "gtest/gtest.h"
#include "storm-config.h"
-
+#include "src/settings/SettingMemento.h"
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
@@ -13,6 +13,9 @@
#include "src/settings/SettingsManager.h"
TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -68,6 +71,9 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
}
TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -123,6 +129,9 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
}
TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -147,10 +156,16 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
}
TEST(GmmxxCtmcCslModelCheckerTest, Fms) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// No properties to check at this point.
}
TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
diff --git a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
index 0c7e4cca7..3dfa1b6be 100644
--- a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
@@ -1,6 +1,6 @@
#include "gtest/gtest.h"
#include "storm-config.h"
-
+#include "src/settings/SettingMemento.h"
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
@@ -13,6 +13,9 @@
#include "src/settings/SettingsManager.h"
TEST(SparseCtmcCslModelCheckerTest, Cluster) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -68,6 +71,9 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
}
TEST(SparseCtmcCslModelCheckerTest, Embedded) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -123,6 +129,9 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
}
TEST(SparseCtmcCslModelCheckerTest, Polling) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -147,10 +156,16 @@ TEST(SparseCtmcCslModelCheckerTest, Polling) {
}
TEST(SparseCtmcCslModelCheckerTest, Fms) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// No properties to check at this point.
}
TEST(SparseCtmcCslModelCheckerTest, Tandem) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());