From 6fcc97a7b4a7eee22cd94514fd9d4aeb4a9cf046 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sun, 30 Oct 2016 02:30:39 +0200
Subject: [PATCH] Implemented modularisation for MTTF via parallel composition
of CTMCs
Former-commit-id: 552949346b81a4c4def16dc68dd2206e3a993807
---
src/builder/ParallelCompositionBuilder.cpp | 172 ++++++++++++++++
src/builder/ParallelCompositionBuilder.h | 24 +++
src/modelchecker/dft/DFTModelChecker.cpp | 218 +++++++++++++++++----
src/modelchecker/dft/DFTModelChecker.h | 14 ++
src/storage/dft/DFT.cpp | 2 +-
src/storm-dyftee.cpp | 6 +-
6 files changed, 392 insertions(+), 44 deletions(-)
create mode 100644 src/builder/ParallelCompositionBuilder.cpp
create mode 100644 src/builder/ParallelCompositionBuilder.h
diff --git a/src/builder/ParallelCompositionBuilder.cpp b/src/builder/ParallelCompositionBuilder.cpp
new file mode 100644
index 000000000..5d78d74fa
--- /dev/null
+++ b/src/builder/ParallelCompositionBuilder.cpp
@@ -0,0 +1,172 @@
+#include "src/builder/ParallelCompositionBuilder.h"
+#include "src/models/sparse/StandardRewardModel.h"
+#include <src/utility/constants.h>
+
+namespace storm {
+ namespace builder {
+
+ template<typename ValueType>
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ParallelCompositionBuilder<ValueType>::compose(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcA, std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcB, bool labelAnd) {
+ STORM_LOG_TRACE("Parallel composition");
+
+ storm::storage::SparseMatrix<ValueType> matrixA = ctmcA->getTransitionMatrix();
+ storm::storage::SparseMatrix<ValueType> matrixB = ctmcB->getTransitionMatrix();
+ storm::models::sparse::StateLabeling labelingA = ctmcA->getStateLabeling();
+ storm::models::sparse::StateLabeling labelingB = ctmcB->getStateLabeling();
+ size_t sizeA = ctmcA->getNumberOfStates();
+ size_t sizeB = ctmcB->getNumberOfStates();
+ size_t size = sizeA * sizeB;
+ size_t rowIndex = 0;
+
+ // Build matrix
+ storm::storage::SparseMatrixBuilder<ValueType> builder(size, size, 0, true, false, 0);
+
+ for (size_t stateA = 0; stateA < sizeA; ++stateA) {
+ for (size_t stateB = 0; stateB < sizeB; ++stateB) {
+ STORM_LOG_ASSERT(rowIndex == stateA * sizeB + stateB, "Row " << rowIndex << " is not correct");
+
+ auto rowA = matrixA.getRow(stateA);
+ auto itA = rowA.begin();
+ auto rowB = matrixB.getRow(stateB);
+ auto itB = rowB.begin();
+
+ // First consider all target states of A < the current stateA
+ while (itA != rowA.end() && itA->getColumn() < stateA) {
+ builder.addNextValue(rowIndex, itA->getColumn() * sizeB + stateB, itA->getValue());
+ ++itA;
+ }
+
+ // Then consider all target states of B
+ while (itB != rowB.end()) {
+ builder.addNextValue(rowIndex, stateA * sizeB + itB->getColumn(), itB->getValue());
+ ++itB;
+ }
+
+ // Last consider all remaining target states of A > the current stateA
+ while (itA != rowA.end()) {
+ builder.addNextValue(rowIndex, itA->getColumn() * sizeB + stateB, itA->getValue());
+ ++itA;
+ }
+
+ ++rowIndex;
+ }
+ }
+
+ storm::storage::SparseMatrix<ValueType> matrixComposed = builder.build();
+ STORM_LOG_ASSERT(matrixComposed.getRowCount() == size, "Row count is not correct");
+ STORM_LOG_ASSERT(matrixComposed.getColumnCount() == size, "Column count is not correct");
+
+ // Build labeling
+ storm::models::sparse::StateLabeling labeling = storm::models::sparse::StateLabeling(sizeA * sizeB);
+
+ if (labelAnd) {
+ for (std::string const& label : labelingA.getLabels()) {
+ if (labelingB.containsLabel(label)) {
+ // Only consider labels contained in both CTMCs
+ storm::storage::BitVector labelStates(size, false);
+ for (auto entryA : labelingA.getStates(label)) {
+ for (auto entryB : labelingB.getStates(label)) {
+ labelStates.set(entryA * sizeB + entryB);
+ }
+ }
+ labeling.addLabel(label, labelStates);
+ }
+ }
+ } else {
+ // Set labels from A
+ for (std::string const& label : labelingA.getLabels()) {
+ if (label == "init") {
+ // Initial states must be initial in both CTMCs
+ STORM_LOG_ASSERT(labelingB.containsLabel(label), "B does not have init.");
+ storm::storage::BitVector labelStates(size, false);
+ for (auto entryA : labelingA.getStates(label)) {
+ for (auto entryB : labelingB.getStates(label)) {
+ labelStates.set(entryA * sizeB + entryB);
+ }
+ }
+ labeling.addLabel(label, labelStates);
+ } else {
+ storm::storage::BitVector labelStates(size, false);
+ for (auto entry : labelingA.getStates(label)) {
+ for (size_t index = entry * sizeB; index < entry * sizeB + sizeB; ++index) {
+ labelStates.set(index, true);
+ }
+ }
+ labeling.addLabel(label, labelStates);
+ }
+ }
+ // Set labels from B
+ for (std::string const& label : labelingB.getLabels()) {
+ if (label == "init") {
+ continue;
+ }
+ if (labeling.containsLabel(label)) {
+ // Label is already there from A
+ for (auto entry : labelingB.getStates(label)) {
+ for (size_t index = 0; index < sizeA; ++index) {
+ labeling.addLabelToState(label, index * sizeB + entry);
+ }
+ }
+ } else {
+ storm::storage::BitVector labelStates(size, false);
+ for (auto entry : labelingB.getStates(label)) {
+ for (size_t index = 0; index < sizeA; ++index) {
+ labelStates.set(index * sizeB + entry, true);
+ }
+ }
+ labeling.addLabel(label, labelStates);
+ }
+ }
+ }
+
+
+ // Build CTMC
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedCtmc = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(matrixComposed, labeling);
+
+ // Print for debugging
+ /*std::cout << "Matrix A:" << std::endl;
+ std::cout << matrixA << std::endl;
+ std::cout << "Matrix B:" << std::endl;
+ std::cout << matrixB << std::endl;
+ std::cout << "Composed matrix: " << std::endl << matrixComposed;
+ std::cout << "Labeling A" << std::endl;
+ labelingA.printLabelingInformationToStream(std::cout);
+ for (size_t stateA = 0; stateA < sizeA; ++stateA) {
+ std::cout << "State " << stateA << ": ";
+ for (auto label : labelingA.getLabelsOfState(stateA)) {
+ std::cout << label << ", ";
+ }
+ std::cout << std::endl;
+ }
+ std::cout << "Labeling B" << std::endl;
+ labelingB.printLabelingInformationToStream(std::cout);
+ for (size_t stateB = 0; stateB < sizeB; ++stateB) {
+ std::cout << "State " << stateB << ": ";
+ for (auto label : labelingB.getLabelsOfState(stateB)) {
+ std::cout << label << ", ";
+ }
+ std::cout << std::endl;
+ }
+ std::cout << "Labeling Composed" << std::endl;
+ labeling.printLabelingInformationToStream(std::cout);
+ for (size_t state = 0; state < size; ++state) {
+ std::cout << "State " << state << ": ";
+ for (auto label : labeling.getLabelsOfState(state)) {
+ std::cout << label << ", ";
+ }
+ std::cout << std::endl;
+ }*/
+
+ return composedCtmc;
+ }
+
+
+ // Explicitly instantiate the class.
+ template class ParallelCompositionBuilder<double>;
+
+#ifdef STORM_HAVE_CARL
+ template class ParallelCompositionBuilder<storm::RationalFunction>;
+#endif
+
+ } // namespace builder
+} // namespace storm
diff --git a/src/builder/ParallelCompositionBuilder.h b/src/builder/ParallelCompositionBuilder.h
new file mode 100644
index 000000000..3b0fab790
--- /dev/null
+++ b/src/builder/ParallelCompositionBuilder.h
@@ -0,0 +1,24 @@
+#ifndef PARALLELCOMPOSITIONBUILDER_H
+#define PARALLELCOMPOSITIONBUILDER_H
+
+#include <src/models/sparse/Ctmc.h>
+
+namespace storm {
+ namespace builder {
+
+ /*!
+ * Build a parallel composition of Markov chains.
+ */
+ template<typename ValueType>
+ class ParallelCompositionBuilder {
+
+ public:
+
+ static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> compose(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcA, std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcB, bool labelAnd);
+
+ };
+
+ }
+}
+
+#endif /* EXPLICITDFTMODELBUPARALLELCOMPOSITIONBUILDER_HILDERAPPROX_H */
diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp
index be5ad6913..748abe188 100644
--- a/src/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/modelchecker/dft/DFTModelChecker.cpp
@@ -2,6 +2,7 @@
#include "src/builder/ExplicitDFTModelBuilder.h"
#include "src/builder/ExplicitDFTModelBuilderApprox.h"
+#include "src/builder/ParallelCompositionBuilder.h"
#include "src/storage/dft/DFTIsomorphism.h"
#include "src/settings/modules/DFTSettings.h"
#include "src/utility/bitoperations.h"
@@ -28,10 +29,19 @@ namespace storm {
// Optimizing DFT
storm::storage::DFT<ValueType> dft = origDft.optimize();
- // TODO Matthias: check that all paths reach the target state!
+ // TODO Matthias: check that all paths reach the target state for approximation
// Checking DFT
- checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError);
+ if (formula->isProbabilityOperatorFormula() || !allowModularisation) {
+ checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError);
+ } else {
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelComposition(dft, formula, symred, allowModularisation, enableDC);
+ // Model checking
+ std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
+ result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
+ checkResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
+
+ }
this->totalTime = std::chrono::high_resolution_clock::now() - totalStart;
}
@@ -85,45 +95,44 @@ namespace storm {
if(modularisationPossible) {
STORM_LOG_TRACE("Recursive CHECK Call");
- // TODO Matthias: enable modularisation for approximation
- STORM_LOG_ASSERT(approximationError == 0.0, "Modularisation not possible for approximation.");
-
- // Recursively call model checking
- std::vector<ValueType> res;
- for(auto const ft : dfts) {
- dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0);
- res.push_back(boost::get<ValueType>(ftResult));
- }
+ if (formula->isProbabilityOperatorFormula()) {
+ // Recursively call model checking
+ std::vector<ValueType> res;
+ for(auto const ft : dfts) {
+ dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0);
+ res.push_back(boost::get<ValueType>(ftResult));
+ }
- // Combine modularisation results
- STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
- ValueType result = storm::utility::zero<ValueType>();
- int limK = invResults ? -1 : nrM+1;
- int chK = invResults ? -1 : 1;
- // WARNING: there is a bug for computing permutations with more than 32 elements
- STORM_LOG_ASSERT(res.size() < 32, "Permutations work only for < 32 elements");
- for(int cK = nrK; cK != limK; cK += chK ) {
- STORM_LOG_ASSERT(cK >= 0, "ck negative.");
- size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(cK));
- do {
- STORM_LOG_TRACE("Permutation="<<permutation);
- ValueType permResult = storm::utility::one<ValueType>();
- for(size_t i = 0; i < res.size(); ++i) {
- if(permutation & (1 << i)) {
- permResult *= res[i];
- } else {
- permResult *= storm::utility::one<ValueType>() - res[i];
+ // Combine modularisation results
+ STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
+ ValueType result = storm::utility::zero<ValueType>();
+ int limK = invResults ? -1 : nrM+1;
+ int chK = invResults ? -1 : 1;
+ // WARNING: there is a bug for computing permutations with more than 32 elements
+ STORM_LOG_ASSERT(res.size() < 32, "Permutations work only for < 32 elements");
+ for(int cK = nrK; cK != limK; cK += chK ) {
+ STORM_LOG_ASSERT(cK >= 0, "ck negative.");
+ size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(cK));
+ do {
+ STORM_LOG_TRACE("Permutation="<<permutation);
+ ValueType permResult = storm::utility::one<ValueType>();
+ for(size_t i = 0; i < res.size(); ++i) {
+ if(permutation & (1 << i)) {
+ permResult *= res[i];
+ } else {
+ permResult *= storm::utility::one<ValueType>() - res[i];
+ }
}
- }
- STORM_LOG_TRACE("Result for permutation:"<<permResult);
- permutation = nextBitPermutation(permutation);
- result += permResult;
- } while(permutation < (1 << nrM) && permutation != 0);
- }
- if(invResults) {
- result = storm::utility::one<ValueType>() - result;
+ STORM_LOG_TRACE("Result for permutation:"<<permResult);
+ permutation = nextBitPermutation(permutation);
+ result += permResult;
+ } while(permutation < (1 << nrM) && permutation != 0);
+ }
+ if(invResults) {
+ result = storm::utility::one<ValueType>() - result;
+ }
+ return result;
}
- return result;
}
}
@@ -132,6 +141,137 @@ namespace storm {
return checkDFT(dft, formula, symred, enableDC, approximationError);
}
+ template<typename ValueType>
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelComposition(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC) {
+ STORM_LOG_TRACE("Build model via composition");
+ // Use parallel composition for CTMCs for expected time
+ STORM_LOG_ASSERT(formula->isTimeOperatorFormula(), "Formula is not a time operator formula");
+ bool modularisationPossible = allowModularisation;
+
+ // Try modularisation
+ if(modularisationPossible) {
+ std::vector<storm::storage::DFT<ValueType>> dfts;
+ bool isAnd = true;
+
+ switch (dft.topLevelType()) {
+ case storm::storage::DFTElementType::AND:
+ STORM_LOG_TRACE("top modularisation called AND");
+ dfts = dft.topModularisation();
+ STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
+ modularisationPossible = dfts.size() > 1;
+ isAnd = true;
+ break;
+ case storm::storage::DFTElementType::OR:
+ STORM_LOG_TRACE("top modularisation called OR");
+ dfts = dft.topModularisation();
+ STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
+ modularisationPossible = dfts.size() > 1;
+ isAnd = false;
+ break;
+ case storm::storage::DFTElementType::VOT:
+ /*STORM_LOG_TRACE("top modularisation called VOT");
+ dfts = dft.topModularisation();
+ STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
+ std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
+ */
+ // TODO enable modularisation for voting gate
+ modularisationPossible = false;
+ break;
+ default:
+ // No static gate -> no modularisation applicable
+ modularisationPossible = false;
+ break;
+ }
+
+ if(modularisationPossible) {
+ STORM_LOG_TRACE("Recursive CHECK Call");
+ bool firstTime = true;
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedModel;
+ for (auto const ft : dfts) {
+ STORM_LOG_INFO("Building Model via parallel composition...");
+ std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
+
+ // Find symmetries
+ std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
+ storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
+ if(symred) {
+ auto colouring = ft.colourDFT();
+ symmetries = ft.findSymmetries(colouring);
+ STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
+ STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
+ }
+
+ // Build a single CTMC
+ STORM_LOG_INFO("Building Model...");
+ storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+ builder.buildModel(labeloptions, 0, 0.0);
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
+ //model->printModelInformationToStream(std::cout);
+ STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
+ STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
+ explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
+
+ STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
+
+ ctmc = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(ctmc, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+
+ if (firstTime) {
+ composedModel = ctmc;
+ firstTime = false;
+ } else {
+ composedModel = storm::builder::ParallelCompositionBuilder<ValueType>::compose(composedModel, ctmc, isAnd);
+ }
+
+ // Apply bisimulation
+ std::chrono::high_resolution_clock::time_point bisimulationStart = std::chrono::high_resolution_clock::now();
+ composedModel = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+ std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now();
+ bisimulationTime += bisimulationEnd - bisimulationStart;
+
+ STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
+ STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
+ if (composedModel->getNumberOfStates() <= 15) {
+ STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix());
+ } else {
+ STORM_LOG_TRACE("Transition matrix: too big to print");
+ }
+
+ }
+ return composedModel;
+ }
+ }
+
+ // If we are here, no composition was possible
+ STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible.");
+ std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
+ // Find symmetries
+ std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
+ storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
+ if(symred) {
+ auto colouring = dft.colourDFT();
+ symmetries = dft.findSymmetries(colouring);
+ STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
+ STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
+ }
+ // Build a single CTMC
+ STORM_LOG_INFO("Building Model...");
+
+
+ storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
+ builder.buildModel(labeloptions, 0, 0.0);
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
+ //model->printModelInformationToStream(std::cout);
+ STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
+ STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
+ explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
+ STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
+
+ return model->template as<storm::models::sparse::Ctmc<ValueType>>();
+ }
+
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_result DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
@@ -213,7 +353,7 @@ namespace storm {
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
- builder.buildModel(labeloptions, 0);
+ builder.buildModel(labeloptions, 0, 0.0);
model = builder.getModel();
} else {
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
diff --git a/src/modelchecker/dft/DFTModelChecker.h b/src/modelchecker/dft/DFTModelChecker.h
index 543bf97fd..67deb2af0 100644
--- a/src/modelchecker/dft/DFTModelChecker.h
+++ b/src/modelchecker/dft/DFTModelChecker.h
@@ -83,6 +83,20 @@ namespace storm {
*/
dft_result checkHelper(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError);
+ /*!
+ * Internal helper for building a CTMC from a DFT via parallel composition.
+ *
+ * @param dft DFT
+ * @param formula Formula to check for
+ * @param symred Flag indicating if symmetry reduction should be used
+ * @param allowModularisation Flag indication if modularisation is allowed
+ * @param enableDC Flag indicating if dont care propagation should be used
+ * @param approximationError Error allowed for approximation. Value 0 indicates no approximation
+ *
+ * @return CTMC representing the DFT
+ */
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelComposition(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC);
+
/*!
* Check model generated from DFT.
*
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 101f3f962..88be1df73 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -244,7 +244,7 @@ namespace storm {
for(auto const& child : children) {
std::vector<size_t> isubdft;
if(child->nrParents() > 1 || child->hasOutgoingDependencies() || child->hasRestrictions()) {
- STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
+ STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation.");
return {*this};
}
if (isGate(child->id())) {
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 5b040a3b0..05e01c6d1 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -142,7 +142,6 @@ int main(const int argc, const char** argv) {
// Construct pctlFormula
std::string pctlFormula = "";
- bool allowModular = true;
std::string operatorType = "";
std::string targetFormula = "";
@@ -153,7 +152,6 @@ int main(const int argc, const char** argv) {
STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "T";
targetFormula = "F \"failed\"";
- allowModular = false;
} else if (dftSettings.usePropProbability()) {
STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "P";;
@@ -180,9 +178,9 @@ int main(const int argc, const char** argv) {
// From this point on we are ready to carry out the actual computations.
if (parametric) {
- analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+ analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
} else {
- analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+ analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
}
// All operations have now been performed, so we clean up everything and terminate.