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(rate)) { // Get active failure rate for cold BE rate = dft.getBasicElement(id)->activeFailureRate(); + if (storm::utility::isZero(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>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); - 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 void DFTModelChecker::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 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(); 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(); name = stream.str();