Integration of the new settings in the DFT analysis

src/storm-dft-cli/storm-dft.cpp

@@ -10,6 +10,7 @@
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/TransformationSettings.h"
 #include "storm/utility/initialize.h"
 #include "storm-cli-utilities/cli.h"
 #include "storm-parsers/api/storm-parsers.h"
@@ -28,6 +29,7 @@ void processOptions() {
     storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
     storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
     storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
+    storm::settings::modules::TransformationSettings const &transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
 
     auto dftTransformator = storm::transformations::dft::DftTransformator<ValueType>();
 
@@ -55,7 +57,7 @@ void processOptions() {
     }
 
     // Eliminate non-binary dependencies
-    if (dft->getDependencies().size() > 0) {
+    if (!dft->getDependencies().empty()) {
         dft = dftTransformator.transformBinaryFDEPs(*dft);
     }
     // Check well-formedness of DFT
@@ -81,7 +83,7 @@ void processOptions() {
     // SMT
     if (dftIOSettings.isExportToSmt()) {
         dft = dftTransformator.transformUniqueFailedBe(*dft);
-        if (dft->getDependencies().size() > 0) {
+        if (!dft->getDependencies().empty()) {
             dft = dftTransformator.transformBinaryFDEPs(*dft);
         }
         // Export to smtlib2
@@ -91,14 +93,13 @@ void processOptions() {
 
     // TODO introduce some flags
     bool useSMT = false;
-    bool printOutput = false;
     uint64_t solverTimeout = 10;
 #ifdef STORM_HAVE_Z3
     if (faultTreeSettings.solveWithSMT()) {
         useSMT = true;
         STORM_PRINT("Use SMT for preprocessing" << std::endl)
         dft = dftTransformator.transformUniqueFailedBe(*dft);
-        if (dft->getDependencies().size() > 0) {
+        if (!dft->getDependencies().empty()) {
             // Making the constantly failed BE unique may introduce non-binary FDEPs
             dft = dftTransformator.transformBinaryFDEPs(*dft);
         }
@@ -112,25 +113,20 @@ void processOptions() {
                                                                                             solverTimeout);
     preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT,
                                                                                             solverTimeout);
-    if (printOutput) {
-        STORM_PRINT("BE FAILURE BOUNDS" << std::endl <<
-                                        "========================================" << std::endl <<
+    STORM_LOG_DEBUG("BE FAILURE BOUNDS" << std::endl << "========================================" << std::endl <<
                                         "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl <<
-                                        "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl)
-    }
+                                        "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl);
 
     preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true,
                                                                                                solverTimeout);
 
-    if (printOutput) {
-        STORM_PRINT("========================================" << std::endl <<
+    STORM_LOG_DEBUG("========================================" << std::endl <<
                                                                "FDEP CONFLICTS" << std::endl <<
                                                                "========================================"
-                                                               << std::endl)
+                                                               << std::endl);
     for (auto pair: preResults.fdepConflicts) {
-            STORM_PRINT("Conflict between " << dft->getElement(pair.first)->name() << " and "
-                                            << dft->getElement(pair.second)->name() << std::endl)
-        }
+        STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and "
+                                            << dft->getElement(pair.second)->name() << std::endl);
     }
 
     // Set the conflict map of the dft
@@ -149,7 +145,7 @@ void processOptions() {
 #ifdef STORM_HAVE_Z3
     if (faultTreeSettings.solveWithSMT()) {
         // Solve with SMT
-        STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
+        STORM_LOG_DEBUG("Running DFT analysis with use of SMT" << std::endl);
         // Set dynamic behavior vector
         storm::api::analyzeDFTSMT(*dft, true);
     }
@@ -263,7 +259,10 @@ void processOptions() {
             approximationError = faultTreeSettings.getApproximationError();
         }
         storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents,
-                                          faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), true);
+                                          faultTreeSettings.isAllowDCForRelevantEvents(), approximationError,
+                                          faultTreeSettings.getApproximationHeuristic(),
+                                          transformationSettings.isChainEliminationSet(),
+                                          transformationSettings.isIgnoreLabelingSet(), true);
     }
 }
 

src/storm-dft/api/storm-dft.h

@@ -81,6 +81,8 @@ namespace storm {
          * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
          * @param approximationError Allowed approximation error.  Value 0 indicates no approximation.
          * @param approximationHeuristic Heuristic used for state space exploration.
+         * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+         * @param ignoreLabeling If true, the labeling of states is ignored during state elimination
          * @param printOutput If true, model information, timings, results, etc. are printed.
          * @return Results.
          */
@@ -88,11 +90,14 @@ namespace storm {
         typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
         analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true,
                    bool allowModularisation = true, std::set<size_t> const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
-                   storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) {
+                   storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
+                   bool eliminateChains = false, bool ignoreLabeling = false, bool printOutput = false) {
             storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents,
                                                                                                                allowDCForRelevantEvents, approximationError,
-                                                                                                               approximationHeuristic);
+                                                                                                               approximationHeuristic,
+                                                                                                               eliminateChains,
+                                                                                                               ignoreLabeling);
             if (printOutput) {
                 modelChecker.printTimings();
                 modelChecker.printResults(results);

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -652,11 +652,8 @@ namespace storm {
                     maComponents.exitRates = std::move(modelComponents.exitRates);
                     ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
                 }
-                if (ma->hasOnlyTrivialNondeterminism()) {
-                    // Markov automaton can be converted into CTMC
-                    // TODO apply transformer to all MAs
-                    model = storm::transformer::NonMarkovianChainTransformer<ValueType>::eliminateNonmarkovianStates(
-                            ma);
+                if (ma->isConvertibleToCtmc()) {
+                    model = ma->convertToCtmc();
                 } else {
                     model = ma;
                 }

src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@@ -7,6 +7,8 @@
 #include "storm/utility/DirectEncodingExporter.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/models/ModelType.h"
+#include "storm/transformer/NonMarkovianChainTransformer.h"
 
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
@@ -17,7 +19,13 @@ namespace storm {
     namespace modelchecker {
 
         template<typename ValueType>
-        typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
+        typename DFTModelChecker<ValueType>::dft_results
+        DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const &origDft,
+                                          std::vector<std::shared_ptr<const storm::logic::Formula>> const &properties,
+                                          bool symred, bool allowModularisation, std::set<size_t> const &relevantEvents,
+                                          bool allowDCForRelevantEvents, double approximationError,
+                                          storm::builder::ApproximationHeuristic approximationHeuristic,
+                                          bool eliminateChains, bool ignoreLabeling) {
             totalTimer.start();
             dft_results results;
 
@@ -30,21 +38,32 @@ namespace storm {
             // TODO: distinguish for all properties, not only for first one
             if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
                 // Use parallel composition as modularisation approach for expected time
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents);
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft,
+                                                                                                          properties,
+                                                                                                          symred, true,
+                                                                                                          relevantEvents);
                 // Model checking
                 std::vector<ValueType> resultsValue = checkModel(model, properties);
                 for (ValueType result : resultsValue) {
                     results.push_back(result);
                 }
             } else {
-                results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic);
+                results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents,
+                                      allowDCForRelevantEvents, approximationError, approximationHeuristic,
+                                      eliminateChains, ignoreLabeling);
             }
             totalTimer.stop();
             return results;
         }
 
         template<typename ValueType>
-        typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic)  {
+        typename DFTModelChecker<ValueType>::dft_results
+        DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const &dft,
+                                                property_vector const &properties, bool symred,
+                                                bool allowModularisation, std::set<size_t> const &relevantEvents,
+                                                bool allowDCForRelevantEvents, double approximationError,
+                                                storm::builder::ApproximationHeuristic approximationHeuristic,
+                                                bool eliminateChains, bool ignoreLabeling) {
             STORM_LOG_TRACE("Check helper called");
             std::vector<storm::storage::DFT<ValueType>> dfts;
             bool invResults = false;
@@ -73,7 +92,8 @@ namespace storm {
                         STORM_LOG_TRACE("top modularisation called VOT");
                         dfts = dft.topModularisation();
                         STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
-                        nrK = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
+                        nrK = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(
+                                dft.getTopLevelGate())->threshold();
                         nrM = dfts.size();
                         if (nrK <= nrM / 2) {
                             nrK -= 1;
@@ -99,18 +119,21 @@ namespace storm {
                         std::vector<ValueType> res;
                         for (auto const ft : dfts) {
                             // TODO: allow approximation in modularisation
-                            dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevantEvents, 0.0);
+                            dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents,
+                                                                allowDCForRelevantEvents, 0.0);
                             STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results");
                             res.push_back(boost::get<ValueType>(ftResults[0]));
                         }
 
                         // Combine modularisation results
-                        STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
+                        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_THROW(res.size() < 32, storm::exceptions::NotSupportedException, "Permutations work only for < 32 elements");
+                        STORM_LOG_THROW(res.size() < 32, storm::exceptions::NotSupportedException,
+                                        "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));
@@ -138,12 +161,18 @@ namespace storm {
                 return results;
             } else {
                 // No modularisation was possible
-                return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic);
+                return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError,
+                                approximationHeuristic, eliminateChains, ignoreLabeling);
             }
         }
 
         template<typename ValueType>
-        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents)  {
+        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>>
+        DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const &dft,
+                                                             property_vector const &properties, bool symred,
+                                                             bool allowModularisation,
+                                                             std::set<size_t> const &relevantEvents,
+                                                             bool allowDCForRelevantEvents) {
             // TODO: use approximation?
             STORM_LOG_TRACE("Build model via composition");
             std::vector<storm::storage::DFT<ValueType>> dfts;
@@ -194,29 +223,37 @@ namespace storm {
 
                     // Build a single CTMC
                     STORM_LOG_DEBUG("Building Model...");
-                    storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents);
+                    storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, relevantEvents,
+                                                                               allowDCForRelevantEvents);
                     builder.buildModel(0, 0.0);
                     std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                     explorationTimer.stop();
 
-                    STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
+                    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>>();
 
                     // Apply bisimulation to new CTMC
                     bisimulationTimer.start();
-                    ctmc =  storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(ctmc, properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+                    ctmc = storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
+                            ctmc, properties,
+                            storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
                     bisimulationTimer.stop();
 
                     if (firstTime) {
                         composedModel = ctmc;
                         firstTime = false;
                     } else {
-                        composedModel = storm::builder::ParallelCompositionBuilder<ValueType>::compose(composedModel, ctmc, isAnd);
+                        composedModel = storm::builder::ParallelCompositionBuilder<ValueType>::compose(composedModel,
+                                                                                                       ctmc, isAnd);
                     }
 
                     // Apply bisimulation to parallel composition
                     bisimulationTimer.start();
-                    composedModel = storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+                    composedModel = storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
+                            composedModel, properties,
+                            storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
                     bisimulationTimer.stop();
 
                     STORM_LOG_DEBUG("No. states (Composed): " << composedModel->getNumberOfStates());
@@ -245,18 +282,27 @@ namespace storm {
                 // Build a single CTMC
                 STORM_LOG_DEBUG("Building Model...");
 
-                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents);
+                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents,
+                                                                           allowDCForRelevantEvents);
                 builder.buildModel(0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
                 //model->printModelInformationToStream(std::cout);
                 explorationTimer.stop();
-                STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
+                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_results DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
+        typename DFTModelChecker<ValueType>::dft_results
+        DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const &dft,
+                                             property_vector const &properties, bool symred,
+                                             std::set<size_t> const &relevantEvents, bool allowDCForRelevantEvents,
+                                             double approximationError,
+                                             storm::builder::ApproximationHeuristic approximationHeuristic,
+                                             bool eliminateChains, bool ignoreLabeling) {
             explorationTimer.start();
 
             // Find symmetries
@@ -273,10 +319,12 @@ namespace storm {
                 // Comparator for checking the error of the approximation
                 storm::utility::ConstantsComparator<ValueType> comparator;
                 // Build approximate Markov Automata for lower and upper bound
-                approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
+                approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(),
+                                                                   storm::utility::zero<ValueType>());
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
                 std::vector<ValueType> newResult;
-                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents);
+                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents,
+                                                                           allowDCForRelevantEvents);
 
                 // TODO: compute approximation for all properties simultaneously?
                 std::shared_ptr<const storm::logic::Formula> property = properties[0];
@@ -285,7 +333,9 @@ namespace storm {
                 }
 
                 bool probabilityFormula = property->isProbabilityOperatorFormula();
-                STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) || (!property->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly");
+                STORM_LOG_ASSERT((property->isTimeOperatorFormula() && !probabilityFormula) ||
+                                 (!property->isTimeOperatorFormula() && probabilityFormula),
+                                 "Probability formula not initialized correctly");
                 size_t iteration = 0;
                 do {
                     // Iteratively build finer models
@@ -310,7 +360,9 @@ namespace storm {
                     // Check lower bounds
                     newResult = checkModel(model, {property});
                     STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
-                    STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first), "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first);
+                    STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first),
+                                     "New under-approximation " << newResult[0] << " is smaller than old result "
+                                                                << approxResult.first);
                     approxResult.first = newResult[0];
 
                     // Build model for upper bound
@@ -321,17 +373,27 @@ namespace storm {
                     // Check upper bound
                     newResult = checkModel(model, {property});
                     STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
-                    STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]), "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second);
+                    STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]),
+                                     "New over-approximation " << newResult[0] << " is greater than old result "
+                                                               << approxResult.second);
                     approxResult.second = newResult[0];
 
                     ++iteration;
-                    STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second);
+                    STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) ||
+                                     comparator.isEqual(approxResult.first, approxResult.second),
+                                     "Under-approximation " << approxResult.first
+                                                            << " is greater than over-approximation "
+                                                            << approxResult.second);
                     //STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
                     totalTimer.stop();
                     printTimings();
                     totalTimer.start();
-                    STORM_LOG_THROW(!storm::utility::isInfinity<ValueType>(approxResult.first) && !storm::utility::isInfinity<ValueType>(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity.");
-                } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula));
+                    STORM_LOG_THROW(!storm::utility::isInfinity<ValueType>(approxResult.first) &&
+                                    !storm::utility::isInfinity<ValueType>(approxResult.second),
+                                    storm::exceptions::NotSupportedException,
+                                    "Approximation does not work if result might be infinity.");
+                } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError,
+                                                    probabilityFormula));
 
                 //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : "."));
                 dft_results results;
@@ -341,9 +403,15 @@ namespace storm {
                 // Build a single Markov Automaton
                 auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
                 STORM_LOG_DEBUG("Building Model...");
-                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents);
+                storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents,
+                                                                           allowDCForRelevantEvents);
                 builder.buildModel(0, 0.0);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
+                if (eliminateChains && model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    auto ma = std::static_pointer_cast<storm::models::sparse::MarkovAutomaton<ValueType>>(model);
+                    model = storm::transformer::NonMarkovianChainTransformer<ValueType>::eliminateNonmarkovianStates(ma,
+                                                                                                                     !ignoreLabeling);
+                }
                 explorationTimer.stop();
 
                 // Print model information
@@ -376,12 +444,17 @@ namespace storm {
         }
 
         template<typename ValueType>
-        std::vector<ValueType> DFTModelChecker<ValueType>::checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, property_vector const& properties) {
+        std::vector<ValueType>
+        DFTModelChecker<ValueType>::checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> &model,
+                                               property_vector const &properties) {
             // Bisimulation
-            if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
+            if (model->isOfType(storm::models::ModelType::Ctmc) &&
+                storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
                 bisimulationTimer.start();
                 STORM_LOG_DEBUG("Bisimulation...");
-                model =  storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), properties, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
+                model = storm::api::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
+                        model->template as<storm::models::sparse::Ctmc<ValueType>>(), properties,
+                        storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
                 STORM_LOG_DEBUG("No. states (Bisimulation): " << model->getNumberOfStates());
                 STORM_LOG_DEBUG("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
                 bisimulationTimer.stop();
@@ -398,7 +471,9 @@ namespace storm {
                 singleModelCheckingTimer.reset();
                 singleModelCheckingTimer.start();
                 //STORM_PRINT_AND_LOG("Model checking property " << *property << " ..." << std::endl);
-                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property, true)));
+                std::unique_ptr<storm::modelchecker::CheckResult> result(
+                        storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property,
+                                                                                                               true)));
                 STORM_LOG_ASSERT(result, "Result does not exist.");
                 result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                 ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
@@ -418,8 +493,10 @@ namespace storm {
         }
 
         template<>
-        bool DFTModelChecker<double>::isApproximationSufficient(double lowerBound, double upperBound, double approximationError, bool relative) {
-            STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN.");
+        bool DFTModelChecker<double>::isApproximationSufficient(double lowerBound, double upperBound,
+                                                                double approximationError, bool relative) {
+            STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound),
+                            storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN.");
             if (relative) {
                 return upperBound - lowerBound <= approximationError;
             } else {
@@ -453,10 +530,14 @@ namespace storm {
         }
 
 
-        template class DFTModelChecker<double>;
+        template
+        class DFTModelChecker<double>;
 
 #ifdef STORM_HAVE_CARL
-        template class DFTModelChecker<storm::RationalFunction>;
+
+        template
+        class DFTModelChecker<storm::RationalFunction>;
+
 #endif
     }
 }

src/storm-dft/modelchecker/dft/DFTModelChecker.h

@@ -55,11 +55,14 @@ namespace storm {
              * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
              * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
              * @param approximationHeuristic Heuristic used for state space exploration.
+             * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+             * @param ignoreLabeling If true, the labeling of states is ignored during state elimination
              * @return Model checking results for the given properties..
              */
             dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true,
                               std::set<size_t> const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
-                              storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
+                              storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
+                              bool eliminateChains = false, bool ignoreLabeling = false);
 
             /*!
              * Print timings of all operations to stream.
@@ -98,11 +101,14 @@ namespace storm {
              * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
              * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
              * @param approximationHeuristic Heuristic used for approximation.
+             * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+             * @param ignoreLabeling If true, the labeling of states is ignored during state elimination
              * @return Model checking results (or in case of approximation two results for lower and upper bound)
              */
             dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation,
                                     std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
-                                    storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
+                                    storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
+                                    bool eliminateChains = false, bool ignoreLabeling = false);
 
             /*!
              * Internal helper for building a CTMC from a DFT via parallel composition.
@@ -129,12 +135,15 @@ namespace storm {
              * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
              * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
              * @param approximationHeuristic Heuristic used for approximation.
+             * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+             * @param ignoreLabeling If true, the labeling of states is ignored during state elimination
              *
              * @return Model checking result
              */
             dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents = {},
                                  bool allowDCForRelevantEvents = true, double approximationError = 0.0,
-                                 storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
+                                 storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH,
+                                 bool eliminateChains = false, bool ignoreLabeling = false);
 
             /*!
              * Check the given markov model for the given properties.

src/storm-dft/settings/DftSettings.cpp

@@ -23,6 +23,7 @@
 #include "storm-conv/settings/modules/JaniExportSettings.h"
 #include "storm-gspn/settings/modules/GSPNSettings.h"
 #include "storm-gspn/settings/modules/GSPNExportSettings.h"
+#include "storm/settings/modules/TransformationSettings.h"
 
 
 namespace storm {
@@ -37,6 +38,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::DftGspnSettings>();
             storm::settings::addModule<storm::settings::modules::IOSettings>();
             storm::settings::addModule<storm::settings::modules::CoreSettings>();
+            storm::settings::addModule<storm::settings::modules::TransformationSettings>();
 
             storm::settings::addModule<storm::settings::modules::DebugSettings>();
             storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();