diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index bb70f53b5..15d46c381 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -418,12 +418,18 @@ else()
set(sylvan_dep lib_carl)
endif()
+if (STORM_DEBUG_SYLVAN)
+ set(SYLVAN_BUILD_TYPE "Debug")
+else()
+ set(SYLVAN_BUILD_TYPE "Release")
+endif()
+
ExternalProject_Add(
sylvan
DOWNLOAD_COMMAND ""
PREFIX "sylvan"
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
- CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DGMP_LOCATION=${GMP_LIB_LOCATION} -DGMP_INCLUDE=${GMP_INCLUDE_DIR} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF
+ CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DGMP_LOCATION=${GMP_LIB_LOCATION} -DGMP_INCLUDE=${GMP_INCLUDE_DIR} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF
BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
BUILD_IN_SOURCE 0
INSTALL_COMMAND ""
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 5bab54a87..33826447f 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -514,6 +514,7 @@ namespace storm {
result = preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
}
+ preprocessingWatch.stop();
if (result.second) {
STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
}
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp
index 77aa64f1d..e34a7ddf8 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/BisimulationDecomposition.cpp
@@ -7,6 +7,7 @@
#include "storm/models/symbolic/Model.h"
#include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidOperationException.h"
diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
index 914656d89..d26cc4111 100644
--- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
+++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
@@ -1,6 +1,7 @@
#include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h"
#include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
namespace storm {
namespace dd {
@@ -9,8 +10,6 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
MdpPartitionRefiner<DdType, ValueType>::MdpPartitionRefiner(storm::models::symbolic::Mdp<DdType, ValueType> const& mdp, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(mdp, initialStatePartition), choicePartition(Partition<DdType, ValueType>::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) {
// Intentionally left empty.
-
- mdp.getTransitionMatrix().exportToDot("fulltrans.dot");
}
template<storm::dd::DdType DdType, typename ValueType>
diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp
index bde87a5b9..fb64f9381 100644
--- a/src/storm/storage/dd/bisimulation/Partition.cpp
+++ b/src/storm/storage/dd/bisimulation/Partition.cpp
@@ -9,6 +9,7 @@
#include "storm/logic/AtomicLabelFormula.h"
#include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/BisimulationSettings.h"
diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
index 74a563363..cd064343f 100644
--- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
+++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
@@ -1,5 +1,7 @@
#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace dd {
namespace bisimulation {
diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp
index 363e88fdd..5009fa371 100644
--- a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp
+++ b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp
@@ -2,6 +2,8 @@
#include "storm/logic/Formulas.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidPropertyException.h"
@@ -15,7 +17,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const& bisimulationType) {
+ PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const&) {
for (auto const& label : labels) {
this->addLabel(label);
this->addExpression(model.getExpression(label));
@@ -23,14 +25,14 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const& bisimulationType) {
+ PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const&) {
for (auto const& e : expressions) {
this->addExpression(e);
}
}
template <storm::dd::DdType DdType, typename ValueType>
- PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) {
+ PreservationInformation<DdType, ValueType>::PreservationInformation(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const&) {
if (formulas.empty()) {
// Default to respect all labels if no formulas are given.
for (auto const& label : model.getLabels()) {
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index 3027badf0..32b9363b2 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -551,9 +551,6 @@ namespace storm {
// Sanity checks.
STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size.");
- partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).exportToDot("partstates.dot");
- model.getReachableStates().exportToDot("origstates.dot");
- std::cout << "equal? " << (partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).template toAdd<ValueType>().notZero() == model.getReachableStates().template toAdd<ValueType>().notZero()) << std::endl;
STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition.");
std::set<storm::expressions::Variable> blockVariableSet = {partition.getBlockVariable()};
@@ -567,36 +564,10 @@ namespace storm {
partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet);
}
- storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
- partitionAsAdd.exportToDot("partition.dot");
- model.getTransitionMatrix().sumAbstract(model.getColumnVariables()).exportToDot("origdist.dot");
auto start = std::chrono::high_resolution_clock::now();
- storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables());
- STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(model.getTransitionMatrix().sumAbstract(model.getColumnVariables()), ValueType(1e-6)), "Expected something else.");
- quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("sanity.dot");
- quotientTransitionMatrix.exportToDot("trans-1.dot");
- partitionAsAdd = partitionAsAdd / partitionAsAdd.sumAbstract(model.getColumnVariables());
- quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables());
- quotientTransitionMatrix.exportToDot("quottrans.dot");
- auto partCount = partitionAsAdd.sumAbstract(model.getColumnVariables());
- partCount.exportToDot("partcount.dot");
- auto end = std::chrono::high_resolution_clock::now();
-
- // Check quotient matrix for sanity.
- auto quotdist = quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet);
- quotdist.exportToDot("quotdists.dot");
- (quotdist / partCount).exportToDot("distcount.dot");
- STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
- STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd<ValueType>(), ValueType(1e-6)), "Illegal non-probabilistic matrix.");
-
- STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
- storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
-
- start = std::chrono::high_resolution_clock::now();
storm::dd::Bdd<DdType> partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables());
- storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
std::map<std::string, storm::dd::Bdd<DdType>> preservedLabelBdds;
for (auto const& label : preservationInformation.getLabels()) {
@@ -614,9 +585,29 @@ namespace storm {
preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables()));
}
}
- end = std::chrono::high_resolution_clock::now();
+ auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+ storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
+ start = std::chrono::high_resolution_clock::now();
+ storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables());
+
+ // Pick a representative from each block.
+ partitionAsBdd = partitionAsBdd.existsAbstractRepresentative(model.getColumnVariables());
+ partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
+
+ quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables());
+ end = std::chrono::high_resolution_clock::now();
+
+ // Check quotient matrix for sanity.
+ STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
+ STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd<ValueType>(), ValueType(1e-6)), "Illegal non-probabilistic matrix.");
+
+ STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+
+ storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
+ storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
+
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {}));
} else if (modelType == storm::models::ModelType::Ctmc) {
diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp
index 682085468..b4336adc8 100644
--- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp
+++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp
@@ -2,6 +2,8 @@
#include "storm/storage/dd/DdManager.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
#include "storm/utility/macros.h"
#include "storm/exceptions/OutOfRangeException.h"
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
index 11c7b09d6..4586e9890 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -67,8 +67,8 @@ namespace storm {
maxTableSize >>= 1;
}
- uint64_t initialTableSize = 1ull << std::max(powerOfTwo - 4, 16ull);
- uint64_t initialCacheSize = 1ull << std::max(powerOfTwo - 4, 16ull);
+ uint64_t initialTableSize = 1ull << std::max(powerOfTwo - 4, static_cast<uint_fast64_t>(16));
+ uint64_t initialCacheSize = initialTableSize;
STORM_LOG_DEBUG("Initializing sylvan. Initial/max table size: " << initialTableSize << "/" << maxTableSize << ", initial/max cache size: " << initialCacheSize << "/" << maxCacheSize << ".");
sylvan::Sylvan::initPackage(initialTableSize, maxTableSize, initialCacheSize, maxCacheSize);
diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.cpp b/src/storm/storage/expressions/LinearityCheckVisitor.cpp
index 18198ca0e..9eeb3ea56 100644
--- a/src/storm/storage/expressions/LinearityCheckVisitor.cpp
+++ b/src/storm/storage/expressions/LinearityCheckVisitor.cpp
@@ -125,7 +125,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator.");
}
- boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
+ boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const&, boost::any const& data) {
bool booleanIsLinear = boost::any_cast<bool>(data);
if (booleanIsLinear) {
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
index f7aa3236d..15a8d61eb 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
@@ -119,6 +119,8 @@ namespace storm {
return result;
break;
}
+ // Dummy return.
+ return result;
}
template<typename RationalNumberType>