From 036d9c55d50f6f3a41cfe75147acd2ce3f8e30b7 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 8 Feb 2017 14:32:44 +0100
Subject: [PATCH] Small fixes

---
 .../builder/ExplicitDFTModelBuilderApprox.cpp         |  4 ++++
 src/storm-dft/modelchecker/dft/DFTModelChecker.cpp    | 11 +++++------
 src/storm-dft/parser/DFTJsonParser.cpp                |  2 ++
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index 48e564af0..9bb318cc1 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -563,6 +563,10 @@ namespace storm {
                         if (storm::utility::isZero<ValueType>(rate)) {
                             // Get active failure rate for cold BE
                             rate = dft.getBasicElement(id)->activeFailureRate();
+                            if (storm::utility::isZero<ValueType>(rate)) {
+                                // Ignore BE which cannot fail
+                                continue;
+                            }
                             // Mark BE as cold
                             coldBEs.set(i, true);
                         }
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 8ca775432..fadd6d6fe 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -224,7 +224,6 @@ namespace storm {
                         // Apply bisimulation
                         bisimulationTimer.start();
                         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();
                         bisimulationTimer.stop();
 
                         STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
@@ -412,11 +411,11 @@ namespace storm {
         template<typename ValueType>
         void DFTModelChecker<ValueType>::printTimings(std::ostream& os) {
             os << "Times:" << std::endl;
-            os << "Exploration:\t" << explorationTimer.getTimeInSeconds() << "s" << std::endl;
-            os << "Building:\t" << buildingTimer.getTimeInSeconds() << "s" << std::endl;
-            os << "Bisimulation:\t" << bisimulationTimer.getTimeInSeconds() << "s" << std::endl;
-            os << "Modelchecking:\t" << modelCheckingTimer.getTimeInSeconds() << "s" << std::endl;
-            os << "Total:\t\t" << totalTimer.getTimeInSeconds() << "s" << std::endl;
+            os << "Exploration:\t" << explorationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
+            os << "Building:\t" << buildingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
+            os << "Bisimulation:\t" << bisimulationTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
+            os << "Modelchecking:\t" << modelCheckingTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
+            os << "Total:\t\t" << totalTimer.getTimeInMilliseconds() / 1000.0 << "s" << std::endl;
         }
 
         template<typename ValueType>
diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp
index 7d4a64a64..80ccdec45 100644
--- a/src/storm-dft/parser/DFTJsonParser.cpp
+++ b/src/storm-dft/parser/DFTJsonParser.cpp
@@ -77,6 +77,7 @@ namespace storm {
                     // Append to id to distinguish elements with the same name
                     std::string name = data.at("name");
                     std::replace(name.begin(), name.end(), ' ', '_');
+                    std::replace(name.begin(), name.end(), '-', '_');
                     std::stringstream stream;
                     stream << name << "_" << data.at("id").get<std::string>();
                     name = stream.str();
@@ -95,6 +96,7 @@ namespace storm {
                 json data = element.at("data");
                 std::string name = data.at("name");
                 std::replace(name.begin(), name.end(), ' ', '_');
+                std::replace(name.begin(), name.end(), '-', '_');
                 std::stringstream stream;
                 stream << name << "_" << data.at("id").get<std::string>();
                 name = stream.str();