From 034fc013669327f90cfe3962e77c4822cd0905a8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 23 Aug 2026 19:07:21 +0200 Subject: [PATCH 1/6] Forward declarations in DFT parsers --- src/storm-dft/builder/DFTBuilder.h | 8 +------- src/storm-dft/modelchecker/DFTModelChecker.h | 7 ++++--- src/storm-dft/parser/BEOrderParser.cpp | 1 + src/storm-dft/parser/BEOrderParser.h | 11 ++++++++--- src/storm-dft/parser/DFTGalileoParser.cpp | 3 +++ src/storm-dft/parser/DFTGalileoParser.h | 19 ++++++++++++++++--- src/storm-dft/parser/DFTJsonParser.cpp | 2 ++ src/storm-dft/parser/DFTJsonParser.h | 17 +++++++++++++++-- 8 files changed, 50 insertions(+), 18 deletions(-) diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 2e83174463..d32d946db0 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -1,19 +1,13 @@ #pragma once -#include #include #include #include "storm-dft/storage/DFTLayoutInfo.h" #include "storm-dft/storage/elements/DFTElements.h" -#include "storm-dft/storage/elements/DFTRestriction.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/utility/ConstantsComparator.h" -#include "storm/utility/macros.h" - -namespace storm::storage { // Forward declaration +namespace storm::storage { template class DFT; } // namespace storm::storage diff --git a/src/storm-dft/modelchecker/DFTModelChecker.h b/src/storm-dft/modelchecker/DFTModelChecker.h index a78318ca66..8f558bdc81 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/DFTModelChecker.h @@ -1,13 +1,14 @@ #pragma once +#include + +#include "storm-dft/storage/DFT.h" +#include "storm-dft/utility/RelevantEvents.h" #include "storm/api/storm.h" #include "storm/logic/Formula.h" #include "storm/modelchecker/results/CheckResult.h" #include "storm/utility/Stopwatch.h" -#include "storm-dft/storage/DFT.h" -#include "storm-dft/utility/RelevantEvents.h" - namespace storm::dft { namespace modelchecker { diff --git a/src/storm-dft/parser/BEOrderParser.cpp b/src/storm-dft/parser/BEOrderParser.cpp index 634aaf198d..2961ebd395 100644 --- a/src/storm-dft/parser/BEOrderParser.cpp +++ b/src/storm-dft/parser/BEOrderParser.cpp @@ -3,6 +3,7 @@ #include #include "storm-dft/parser/DFTGalileoParser.h" +#include "storm-dft/storage/DFT.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/io/file.h" diff --git a/src/storm-dft/parser/BEOrderParser.h b/src/storm-dft/parser/BEOrderParser.h index 5467c94e19..628e506901 100644 --- a/src/storm-dft/parser/BEOrderParser.h +++ b/src/storm-dft/parser/BEOrderParser.h @@ -1,10 +1,15 @@ #pragma once -#include "storm-dft/builder/DFTBuilder.h" -#include "storm-dft/storage/DFT.h" -#include "storm-parsers/parser/ValueParser.h" +#include namespace storm::dft { + +// Forward declaration +namespace storage { +template +class DFT; +} + namespace parser { /*! diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 222385cc8c..cca92ec6c5 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -4,6 +4,9 @@ #include #include +#include "storm-dft/builder/DFTBuilder.h" +#include "storm-dft/storage/DFT.h" +#include "storm-parsers/parser/ValueParser.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index 94dda9c6a7..3021b34b18 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -1,8 +1,21 @@ #pragma once -#include "storm-dft/builder/DFTBuilder.h" -#include "storm-dft/storage/DFT.h" -#include "storm-parsers/parser/ValueParser.h" +#include + +// Forward declarations +namespace storm::parser { +template +class ValueParser; +; +} // namespace storm::parser +namespace storm::dft::builder { +template +class DFTBuilder; +} +namespace storm::dft::storage { +template +class DFT; +} namespace storm::dft { namespace parser { diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 98b8f1b852..228ae2a884 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -3,7 +3,9 @@ #include #include "storm-dft/builder/DFTBuilder.h" +#include "storm-dft/storage/DFT.h" #include "storm-dft/utility/RelevantEvents.h" +#include "storm-parsers/parser/ValueParser.h" #include "storm/adapters/JsonAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index 8377c1e2e5..99ffa77883 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -1,9 +1,22 @@ #pragma once -#include "storm-dft/storage/DFT.h" -#include "storm-parsers/parser/ValueParser.h" #include "storm/adapters/JsonForward.h" +// Forward declarations +namespace storm::parser { +template +class ValueParser; +; +} // namespace storm::parser +namespace storm::dft::builder { +template +class DFTBuilder; +} +namespace storm::dft::storage { +template +class DFT; +} + namespace storm::dft { namespace parser { From 416e6a69d0c6fcd02c0168166b186c22e29f5dac Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 23 Aug 2026 22:03:31 +0200 Subject: [PATCH 2/6] Split storm-dft.h into analysis.h, io.h and transformation.h --- src/storm-dft-cli/storm-dft.cpp | 9 +- .../api/{storm-dft.cpp => analysis.cpp} | 154 ++++----- src/storm-dft/api/analysis.h | 94 ++++++ src/storm-dft/api/io.cpp | 66 ++++ src/storm-dft/api/io.h | 65 ++++ src/storm-dft/api/storm-dft.h | 311 +----------------- src/storm-dft/api/transformation.cpp | 124 +++++++ src/storm-dft/api/transformation.h | 72 ++++ .../modelchecker/DFTModelChecker.cpp | 2 +- .../modelchecker/DftModularizationChecker.cpp | 2 +- src/test/storm-dft/api/DftSmtTest.cpp | 3 + 11 files changed, 499 insertions(+), 403 deletions(-) rename src/storm-dft/api/{storm-dft.cpp => analysis.cpp} (68%) create mode 100644 src/storm-dft/api/analysis.h create mode 100644 src/storm-dft/api/io.cpp create mode 100644 src/storm-dft/api/io.h create mode 100644 src/storm-dft/api/transformation.cpp create mode 100644 src/storm-dft/api/transformation.h diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index a126e6100e..0deb52fdaf 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -1,14 +1,15 @@ -#include "storm-dft/api/storm-dft.h" #include "storm-cli-utilities/cli.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/parser/BEOrderParser.h" #include "storm-dft/settings/DftSettings.h" #include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" -#include "storm-parsers/api/storm-parsers.h" -#include "storm/adapters/IntervalAdapter.h" +#include "storm-gspn/api/storm-gspn.h" +#include "storm-parsers/api/properties.h" #include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/adapters/RationalNumberAdapter.h" #include "storm/exceptions/UnmetRequirementException.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/IOSettings.h" diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/analysis.cpp similarity index 68% rename from src/storm-dft/api/storm-dft.cpp rename to src/storm-dft/api/analysis.cpp index c00e4eac1e..6fe9f6a55a 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/analysis.cpp @@ -1,26 +1,46 @@ -#include "storm-dft/api/storm-dft.h" +#include "analysis.h" #include #include -#include "storm-conv/api/storm-conv.h" -#include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h" #include "storm-dft/modelchecker/DftModularizationChecker.h" #include "storm-dft/modelchecker/SFTBDDChecker.h" -#include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm-dft/storage/DFT.h" -#include "storm-dft/storage/DftJsonExporter.h" #include "storm-dft/storage/SylvanBddManager.h" -#include "storm-dft/transformations/SftToBddTransformator.h" +#include "storm-dft/utility/FDEPConflictFinder.h" +#include "storm-dft/utility/FailureBoundFinder.h" #include "storm-dft/utility/MTTFHelper.h" - -#include "storm/environment/Environment.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm::dft { namespace api { +storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector> const& properties, + std::vector const& additionalRelevantEventNames) { + storm::dft::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end()); + events.insertNamesFromProperties(properties.begin(), properties.end()); + return events; +} + +template +typename storm::dft::modelchecker::DFTModelChecker::dft_results analyzeDFT( + storm::dft::storage::DFT const& dft, std::vector> const& properties, bool symred, + bool allowModularisation, storm::dft::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant, double approximationError, + storm::dft::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior, + bool printOutput) { + storm::dft::modelchecker::DFTModelChecker modelChecker(printOutput); + typename storm::dft::modelchecker::DFTModelChecker::dft_results results = + modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, + eliminateChains, labelBehavior); + if (printOutput) { + modelChecker.printTimings(); + modelChecker.printResults(results); + } + return results; +} + template<> void analyzeDFTBdd(std::shared_ptr> const& dft, bool const exportToDot, std::string const& filename, bool const calculateMttf, double const mttfPrecision, double const mttfStepsize, std::string const mttfAlgorithmName, bool const calculateMCS, @@ -178,30 +198,6 @@ void analyzeDFTBdd(std::shared_ptr -void exportDFTToJsonFile(storm::dft::storage::DFT const& dft, std::string const& file) { - storm::dft::storage::DftJsonExporter::toFile(dft, file); -} - -template -std::string exportDFTToJsonString(storm::dft::storage::DFT const& dft) { - std::stringstream stream; - storm::dft::storage::DftJsonExporter::toStream(dft, stream); - return stream.str(); -} - -template<> -void exportDFTToSMT(storm::dft::storage::DFT const& dft, std::string const& file) { - storm::dft::modelchecker::DFTASFChecker asfChecker(dft); - asfChecker.convert(); - asfChecker.toFile(file); -} - -template<> -void exportDFTToSMT(storm::dft::storage::DFT const& dft, std::string const& file) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); -} - template<> void analyzeDFTSMT(storm::dft::storage::DFT const& dft, bool printOutput) { uint64_t solverTimeout = 10; @@ -219,71 +215,51 @@ void analyzeDFTSMT(storm::dft::storage::DFT const& dft, STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Analysis by SMT not supported for this data type."); } -template<> -std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { - storm::dft::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); - storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - - // Set Don't Care elements - std::set dontCareElements; - if (!ftSettings.isDisableDC()) { - // Insert all elements as Don't Care elements - for (std::size_t i = 0; i < dft.nrElements(); i++) { - dontCareElements.insert(dft.getElement(i)->id()); - } - } - - // Transform to GSPN - storm::dft::transformations::DftToGspnTransformator gspnTransformator(dft); - auto priorities = gspnTransformator.computePriorities(dftGspnSettings.isExtendPriorities()); - gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed(), - dftGspnSettings.isExtendPriorities()); - std::shared_ptr gspn(gspnTransformator.obtainGSPN()); - return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId()); -} - -template<> -std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); +template +std::pair computeBEFailureBounds(storm::dft::storage::DFT const& dft, bool useSMT, double solverTimeout) { + uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout); + uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout); + return std::make_pair(lowerBEBound, upperBEBound); } -std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) { - // Build Jani model - storm::builder::JaniGSPNBuilder builder(gspn); - std::shared_ptr model(builder.build("dft_gspn")); - - // Build properties - std::shared_ptr const& exprManager = gspn.getExpressionManager(); - storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); - storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); - // Add variable for easier access to 'failed' state - builder.addTransientVariable(model.get(), "failed", targetExpression); - auto failedFormula = std::make_shared(targetExpression); - auto properties = builder.getStandardProperties(model.get(), failedFormula, "Failed", "a failed state", true); +template +bool computeDependencyConflicts(storm::dft::storage::DFT& dft, bool useSMT, double solverTimeout) { + std::vector> fdepConflicts = + storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, useSMT, solverTimeout); - // Export Jani to file - storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - if (dftGspnSettings.isWriteToJaniSet()) { - auto const& jani = storm::settings::getModule(); - storm::api::exportJaniToFile(*model, properties, dftGspnSettings.getWriteToJaniFilename(), jani.isCompactJsonSet()); + for (auto const& pair : fdepConflicts) { + STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); } - return model; -} - -storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector> const& properties, - std::vector const& additionalRelevantEventNames) { - storm::dft::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end()); - events.insertNamesFromProperties(properties.begin(), properties.end()); - return events; + // Set the conflict map of the dft + std::set conflict_set; + for (auto const& conflict : fdepConflicts) { + conflict_set.insert(size_t(conflict.first)); + conflict_set.insert(size_t(conflict.second)); + } + for (size_t depId : dft.getDependencies()) { + if (!conflict_set.count(depId)) { + dft.setDependencyNotInConflict(depId); + } + } + return !fdepConflicts.empty(); } // Explicitly instantiate methods -template void exportDFTToJsonFile(storm::dft::storage::DFT const&, std::string const&); -template std::string exportDFTToJsonString(storm::dft::storage::DFT const&); - -template void exportDFTToJsonFile(storm::dft::storage::DFT const&, std::string const&); -template std::string exportDFTToJsonString(storm::dft::storage::DFT const&); +template typename storm::dft::modelchecker::DFTModelChecker::dft_results analyzeDFT(storm::dft::storage::DFT const&, + std::vector> const&, + bool, bool, storm::dft::utility::RelevantEvents const&, bool, + double, storm::dft::builder::ApproximationHeuristic, bool, + storm::transformer::EliminationLabelBehavior, bool); +template std::pair computeBEFailureBounds(storm::dft::storage::DFT const&, bool, double); +template bool computeDependencyConflicts(storm::dft::storage::DFT&, bool, double); + +template typename storm::dft::modelchecker::DFTModelChecker::dft_results analyzeDFT( + storm::dft::storage::DFT const&, std::vector> const&, bool, bool, + storm::dft::utility::RelevantEvents const&, bool, double, storm::dft::builder::ApproximationHeuristic, bool, storm::transformer::EliminationLabelBehavior, + bool); +template std::pair computeBEFailureBounds(storm::dft::storage::DFT const&, bool, double); +template bool computeDependencyConflicts(storm::dft::storage::DFT&, bool, double); } // namespace api } // namespace storm::dft diff --git a/src/storm-dft/api/analysis.h b/src/storm-dft/api/analysis.h new file mode 100644 index 0000000000..48b23b82e0 --- /dev/null +++ b/src/storm-dft/api/analysis.h @@ -0,0 +1,94 @@ +#pragma once + +#include +#include +#include +#include + +#include "storm-dft/builder/DftExplorationHeuristic.h" +#include "storm-dft/modelchecker/DFTModelChecker.h" +#include "storm-dft/storage/DFT.h" +#include "storm-dft/utility/RelevantEvents.h" +#include "storm/logic/Formula.h" + +namespace storm::dft { +namespace api { + +/*! + * Get relevant event ids from given relevant event names and labels in properties. + * + * @param properties List of properties. All events occurring in a property are relevant. + * @param additionalRelevantEventNames List of names of additional relevant events. + * @return Relevant events. + */ +storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector> const& properties, + std::vector const& additionalRelevantEventNames); + +/*! + * Compute the exact or approximate analysis result of the given DFT according to the given properties. + * First the Markov model is built from the DFT and then this model is checked against the given properties. + * + * @param dft DFT. + * @param properties PCTL formulas capturing the properties to check. + * @param symred Flag whether symmetry reduction should be used. + * @param allowModularisation Flag whether modularisation should be applied if possible. + * @param relevantEvents Relevant events which should be observed. + * @param allowDCForRelevant Whether to allow Don't Care propagation 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 eliminated from the resulting MA. + * @param labelBehavior Behavior of labels of eliminated states + * @param printOutput If true, model information, timings, results, etc. are printed. + * @return Results. + */ +template +typename storm::dft::modelchecker::DFTModelChecker::dft_results analyzeDFT( + storm::dft::storage::DFT const& dft, std::vector> const& properties, bool symred = true, + bool allowModularisation = true, storm::dft::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false, + double approximationError = 0.0, storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH, + bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, + bool printOutput = false); + +/*! + * Analyze the DFT using BDDs + * + * @param dft DFT + * @param exportToDot If true exports the bdd representing the top level event of the dft in the dot format + * @param filename The name of the file for exporting to dot + * @param calculateMTTF If true calculates the mean time to failure + * @param mttfPrecision A constant that is used to determine if the mttf calculation converged + * @param mttfStepsize A constant that is used in the mttf calculation + * @param mttfAlgorithmName The name of the mttf algorithm to use + * @param calculateMCS If true calculates the minimal cut sets + * @param calculateProbability If true calculates the system failure propbability + * @param useModularisation If true tries modularisation + * @param importanceMeasureName The name of the importance measure to calculate + * @param timepoints The timebounds for probability calculations + * @param properties The bounded until formulas to check (emulating the CTMC method) + * @param additionalRelevantEventNames A vector of relevant events to be considered + * @param chunksize The size of the chunks of doubles to work on at a time + */ +template +void analyzeDFTBdd(std::shared_ptr> const& dft, bool const exportToDot, std::string const& filename, + bool const calculateMttf, double const mttfPrecision, double const mttfStepsize, std::string const mttfAlgorithmName, + bool const calculateMCS, bool const calculateProbability, bool const useModularisation, std::string const importanceMeasureName, + std::vector const& timepoints, std::vector> const& properties, + std::vector const& additionalRelevantEventNames, size_t const chunksize); + +/*! + * Analyze the DFT using the SMT encoding + * + * @param dft DFT. + * @param printOutput If true, output is printed. + */ +template +void analyzeDFTSMT(storm::dft::storage::DFT const& dft, bool printOutput); + +template +std::pair computeBEFailureBounds(storm::dft::storage::DFT const& dft, bool useSMT, double solverTimeout); + +template +bool computeDependencyConflicts(storm::dft::storage::DFT& dft, bool useSMT, double solverTimeout); + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/api/io.cpp b/src/storm-dft/api/io.cpp new file mode 100644 index 0000000000..528a82b908 --- /dev/null +++ b/src/storm-dft/api/io.cpp @@ -0,0 +1,66 @@ +#include "io.h" + +#include + +#include "storm-dft/modelchecker/DFTASFChecker.h" +#include "storm-dft/parser/DFTGalileoParser.h" +#include "storm-dft/parser/DFTJsonParser.h" +#include "storm-dft/storage/DftJsonExporter.h" + +namespace storm::dft { +namespace api { + +template +std::shared_ptr> loadDFTGalileoFile(std::string const& file) { + return std::make_shared>(parser::DFTGalileoParser::parseDFT(file)); +} + +template +std::shared_ptr> loadDFTJsonString(std::string const& jsonString) { + return std::make_shared>(parser::DFTJsonParser::parseJsonFromString(jsonString)); +} + +template +std::shared_ptr> loadDFTJsonFile(std::string const& file) { + return std::make_shared>(storm::dft::parser::DFTJsonParser::parseJsonFromFile(file)); +} + +template +void exportDFTToJsonFile(storm::dft::storage::DFT const& dft, std::string const& file) { + storm::dft::storage::DftJsonExporter::toFile(dft, file); +} + +template +std::string exportDFTToJsonString(storm::dft::storage::DFT const& dft) { + std::stringstream stream; + storm::dft::storage::DftJsonExporter::toStream(dft, stream); + return stream.str(); +} + +template<> +void exportDFTToSMT(storm::dft::storage::DFT const& dft, std::string const& file) { + storm::dft::modelchecker::DFTASFChecker asfChecker(dft); + asfChecker.convert(); + asfChecker.toFile(file); +} + +template<> +void exportDFTToSMT(storm::dft::storage::DFT const& dft, std::string const& file) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); +} + +// Explicitly instantiate methods +template std::shared_ptr> loadDFTGalileoFile(std::string const&); +template std::shared_ptr> loadDFTJsonString(std::string const&); +template std::shared_ptr> loadDFTJsonFile(std::string const&); +template void exportDFTToJsonFile(storm::dft::storage::DFT const&, std::string const&); +template std::string exportDFTToJsonString(storm::dft::storage::DFT const&); + +template std::shared_ptr> loadDFTGalileoFile(std::string const&); +template std::shared_ptr> loadDFTJsonString(std::string const&); +template std::shared_ptr> loadDFTJsonFile(std::string const&); +template void exportDFTToJsonFile(storm::dft::storage::DFT const&, std::string const&); +template std::string exportDFTToJsonString(storm::dft::storage::DFT const&); + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/api/io.h b/src/storm-dft/api/io.h new file mode 100644 index 0000000000..5f5e2d5894 --- /dev/null +++ b/src/storm-dft/api/io.h @@ -0,0 +1,65 @@ +#pragma once + +#include + +#include "storm-dft/storage/DFT.h" + +namespace storm::dft { +namespace api { + +/*! + * Load DFT from Galileo file. + * + * @param file File containing DFT description in Galileo format. + * @return DFT. + */ +template +std::shared_ptr> loadDFTGalileoFile(std::string const& file); + +/*! + * Load DFT from JSON string. + * + * @param jsonString String containing DFT description in JSON format. + * @return DFT. + */ +template +std::shared_ptr> loadDFTJsonString(std::string const& jsonString); + +/*! + * Load DFT from JSON file. + * + * @param file File containing DFT description in JSON format. + * @return DFT. + */ +template +std::shared_ptr> loadDFTJsonFile(std::string const& file); + +/*! + * Export DFT to JSON file. + * + * @param dft DFT. + * @param file File. + */ +template +void exportDFTToJsonFile(storm::dft::storage::DFT const& dft, std::string const& file); + +/*! + * Export DFT to JSON string. + * + * @param dft DFT. + * @return DFT in JSON format. + */ +template +std::string exportDFTToJsonString(storm::dft::storage::DFT const& dft); + +/*! + * Export DFT to SMT encoding. + * + * @param dft DFT. + * @param file File. + */ +template +void exportDFTToSMT(storm::dft::storage::DFT const& dft, std::string const& file); + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 757e73ffb3..3043a29150 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -1,310 +1,5 @@ #pragma once -#include -#include -#include - -#include "storm-dft/modelchecker/DFTASFChecker.h" -#include "storm-dft/modelchecker/DFTModelChecker.h" -#include "storm-dft/parser/DFTGalileoParser.h" -#include "storm-dft/parser/DFTJsonParser.h" -#include "storm-dft/transformations/DftToGspnTransformator.h" -#include "storm-dft/transformations/DftTransformer.h" -#include "storm-dft/utility/DftValidator.h" -#include "storm-dft/utility/FDEPConflictFinder.h" -#include "storm-dft/utility/FailureBoundFinder.h" -#include "storm-dft/utility/RelevantEvents.h" -#include "storm-gspn/api/storm-gspn.h" - -namespace storm::dft { -namespace api { - -/*! - * Load DFT from Galileo file. - * - * @param file File containing DFT description in Galileo format. - * @return DFT. - */ -template -std::shared_ptr> loadDFTGalileoFile(std::string const& file) { - return std::make_shared>(storm::dft::parser::DFTGalileoParser::parseDFT(file)); -} - -/*! - * Load DFT from JSON string. - * - * @param jsonString String containing DFT description in JSON format. - * @return DFT. - */ -template -std::shared_ptr> loadDFTJsonString(std::string const& jsonString) { - return std::make_shared>(storm::dft::parser::DFTJsonParser::parseJsonFromString(jsonString)); -} - -/*! - * Load DFT from JSON file. - * - * @param file File containing DFT description in JSON format. - * @return DFT. - */ -template -std::shared_ptr> loadDFTJsonFile(std::string const& file) { - return std::make_shared>(storm::dft::parser::DFTJsonParser::parseJsonFromFile(file)); -} - -/*! - * Check whether the DFT is well-formed. - * - * @param dft DFT. - * @param validForMarkovianAnalysis If true, additional checks are performed to check whether the DFT is valid for analysis via Markov models. - * @return Pair where the first entry is true iff the DFT is well-formed. The second entry contains the error messages for ill-formed parts. - */ -template -std::pair isWellFormed(storm::dft::storage::DFT const& dft, bool validForMarkovianAnalysis = true) { - std::stringstream stream; - bool wellFormed = false; - if (validForMarkovianAnalysis) { - wellFormed = storm::dft::utility::DftValidator::isDftValidForMarkovianAnalysis(dft, stream); - } else { - wellFormed = storm::dft::utility::DftValidator::isDftWellFormed(dft, stream); - } - return std::pair(wellFormed, stream.str()); -} - -/*! - * Check whether the DFT has potential modeling issues. - * - * @param dft DFT. - * @return Pair where the first entry is true iff the DFT has potential modeling issues. The second entry contains the warning messages for the issues. - */ -template -std::pair hasPotentialModelingIssues(storm::dft::storage::DFT const& dft) { - std::stringstream stream; - bool modelingIssues = storm::dft::utility::DftValidator::hasPotentialModelingIssues(dft, stream); - return std::pair(modelingIssues, stream.str()); -} - -/*! - * Apply transformations for DFT. - * - * @param dft DFT. - * @param uniqueBE Flag whether a unique constant failed BE is created. - * @param binaryFDEP Flag whether all dependencies should be binary (only one dependent child). - * @param exponentialDistributions Flag whether distributions should be transformed to exponential distributions (if possible). - * @return Transformed DFT. - */ -template -std::shared_ptr> applyTransformations(storm::dft::storage::DFT const& dft, bool uniqueBE, bool binaryFDEP, - bool exponentialDistributions) { - std::shared_ptr> transformedDft = std::make_shared>(dft); - if (exponentialDistributions && !storm::dft::transformations::DftTransformer::hasOnlyExponentialDistributions(*transformedDft)) { - transformedDft = storm::dft::transformations::DftTransformer::transformExponentialDistributions(*transformedDft); - } - if (uniqueBE && !storm::dft::transformations::DftTransformer::hasUniqueFailedBE(*transformedDft)) { - transformedDft = storm::dft::transformations::DftTransformer::transformUniqueFailedBE(*transformedDft); - } - if (binaryFDEP && storm::dft::transformations::DftTransformer::hasNonBinaryDependency(*transformedDft)) { - transformedDft = storm::dft::transformations::DftTransformer::transformBinaryDependencies(*transformedDft); - } - return transformedDft; -} - -/*! - * Apply transformations to make DFT feasible for Markovian analysis. - * - * @param dft DFT. - * @return Transformed DFT. - */ -template -std::shared_ptr> prepareForMarkovAnalysis(storm::dft::storage::DFT const& dft) { - return storm::dft::api::applyTransformations(dft, true, true, true); -} - -template -std::pair computeBEFailureBounds(storm::dft::storage::DFT const& dft, bool useSMT, double solverTimeout) { - uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout); - uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout); - return std::make_pair(lowerBEBound, upperBEBound); -} - -template -bool computeDependencyConflicts(storm::dft::storage::DFT& dft, bool useSMT, double solverTimeout) { - std::vector> fdepConflicts = - storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, useSMT, solverTimeout); - - for (auto const& pair : fdepConflicts) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); - } - - // Set the conflict map of the dft - std::set conflict_set; - for (auto const& conflict : fdepConflicts) { - conflict_set.insert(size_t(conflict.first)); - conflict_set.insert(size_t(conflict.second)); - } - for (size_t depId : dft.getDependencies()) { - if (!conflict_set.count(depId)) { - dft.setDependencyNotInConflict(depId); - } - } - return !fdepConflicts.empty(); -} - -/*! - * Get relevant event ids from given relevant event names and labels in properties. - * - * @param properties List of properties. All events occurring in a property are relevant. - * @param additionalRelevantEventNames List of names of additional relevant events. - * @return Relevant events. - */ -storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector> const& properties, - std::vector const& additionalRelevantEventNames); - -/*! - * Compute the exact or approximate analysis result of the given DFT according to the given properties. - * First the Markov model is built from the DFT and then this model is checked against the given properties. - * - * @param dft DFT. - * @param properties PCTL formulas capturing the properties to check. - * @param symred Flag whether symmetry reduction should be used. - * @param allowModularisation Flag whether modularisation should be applied if possible. - * @param relevantEvents Relevant events which should be observed. - * @param allowDCForRelevant Whether to allow Don't Care propagation 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 eliminated from the resulting MA. - * @param labelBehavior Behavior of labels of eliminated states - * @param printOutput If true, model information, timings, results, etc. are printed. - * @return Results. - */ -template -typename storm::dft::modelchecker::DFTModelChecker::dft_results analyzeDFT( - storm::dft::storage::DFT const& dft, std::vector> const& properties, bool symred = true, - bool allowModularisation = true, storm::dft::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false, - double approximationError = 0.0, storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH, - bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, - bool printOutput = false) { - storm::dft::modelchecker::DFTModelChecker modelChecker(printOutput); - typename storm::dft::modelchecker::DFTModelChecker::dft_results results = - modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, - eliminateChains, labelBehavior); - if (printOutput) { - modelChecker.printTimings(); - modelChecker.printResults(results); - } - return results; -} - -/*! - * Analyze the DFT using BDDs - * - * @param dft DFT - * - * @param exportToDot - * If true exports the bdd representing the top level event of the dft - * in the dot format - * - * @param filename - * The name of the file for exporting to dot - * - * @param calculateMTTF - * If true calculates the mean time to failure - * - * @parameter mttfPrecision - * A constant that is used to determine if the mttf calculation converged - * - * @parameter mttfStepsize - * A constant that is used in the mttf calculation - * - * @parameter mttfAlgorithmName - * The name of the mttf algorithm to use - * - * @param calculateMCS - * If true calculates the minimal cut sets - * - * @param calculateProbability - * If true calculates the system failure propbability - * - * @param useModularisation - * If true tries modularisation - * - * @param importanceMeasureName - * The name of the importance measure to calculate - * - * @param timepoints - * The timebounds for probability calculations - * - * @param properties - * The bounded until formulas to check (emulating the CTMC method) - * - * @param additionalRelevantEventNames - * A vector of relevant events to be considered - * - * @param chunksize - * The size of the chunks of doubles to work on at a time - * - */ -template -void analyzeDFTBdd(std::shared_ptr> const& dft, bool const exportToDot, std::string const& filename, - bool const calculateMttf, double const mttfPrecision, double const mttfStepsize, std::string const mttfAlgorithmName, - bool const calculateMCS, bool const calculateProbability, bool const useModularisation, std::string const importanceMeasureName, - std::vector const& timepoints, std::vector> const& properties, - std::vector const& additionalRelevantEventNames, size_t const chunksize); - -/*! - * Analyze the DFT using the SMT encoding - * - * @param dft DFT. - * - * @return Result result vector - */ -template -void analyzeDFTSMT(storm::dft::storage::DFT const& dft, bool printOutput); - -/*! - * Export DFT to JSON file. - * - * @param dft DFT. - * @param file File. - */ -template -void exportDFTToJsonFile(storm::dft::storage::DFT const& dft, std::string const& file); - -/*! - * Export DFT to JSON string. - * - * @param dft DFT. - * @return DFT in JSON format. - */ -template -std::string exportDFTToJsonString(storm::dft::storage::DFT const& dft); - -/*! - * Export DFT to SMT encoding. - * - * @param dft DFT. - * @param file File. - */ -template -void exportDFTToSMT(storm::dft::storage::DFT const& dft, std::string const& file); - -/*! - * Transform DFT to GSPN. - * - * @param dft DFT. - * @return Pair of GSPN and id of failed place corresponding to the top level element. - */ -template -std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft); - -/*! - * Transform GSPN to Jani model. - * - * @param gspn GSPN. - * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. - * @return JANI model. - */ -std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace); - -} // namespace api -} // namespace storm::dft +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" diff --git a/src/storm-dft/api/transformation.cpp b/src/storm-dft/api/transformation.cpp new file mode 100644 index 0000000000..2a57b53f59 --- /dev/null +++ b/src/storm-dft/api/transformation.cpp @@ -0,0 +1,124 @@ +#include "transformation.h" + +#include + +#include "storm-conv/api/storm-conv.h" +#include "storm-conv/settings/modules/JaniExportSettings.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm-dft/storage/DFT.h" +#include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-dft/transformations/DftTransformer.h" +#include "storm-dft/utility/DftValidator.h" +#include "storm-gspn/builder/JaniGSPNBuilder.h" +#include "storm/settings/SettingsManager.h" + +namespace storm::dft { +namespace api { + +template +std::pair isWellFormed(storm::dft::storage::DFT const& dft, bool validForMarkovianAnalysis) { + std::stringstream stream; + bool wellFormed = false; + if (validForMarkovianAnalysis) { + wellFormed = storm::dft::utility::DftValidator::isDftValidForMarkovianAnalysis(dft, stream); + } else { + wellFormed = storm::dft::utility::DftValidator::isDftWellFormed(dft, stream); + } + return std::pair(wellFormed, stream.str()); +} + +template +std::pair hasPotentialModelingIssues(storm::dft::storage::DFT const& dft) { + std::stringstream stream; + bool modelingIssues = storm::dft::utility::DftValidator::hasPotentialModelingIssues(dft, stream); + return std::pair(modelingIssues, stream.str()); +} + +template +std::shared_ptr> applyTransformations(storm::dft::storage::DFT const& dft, bool uniqueBE, bool binaryFDEP, + bool exponentialDistributions) { + std::shared_ptr> transformedDft = std::make_shared>(dft); + if (exponentialDistributions && !storm::dft::transformations::DftTransformer::hasOnlyExponentialDistributions(*transformedDft)) { + transformedDft = storm::dft::transformations::DftTransformer::transformExponentialDistributions(*transformedDft); + } + if (uniqueBE && !storm::dft::transformations::DftTransformer::hasUniqueFailedBE(*transformedDft)) { + transformedDft = storm::dft::transformations::DftTransformer::transformUniqueFailedBE(*transformedDft); + } + if (binaryFDEP && storm::dft::transformations::DftTransformer::hasNonBinaryDependency(*transformedDft)) { + transformedDft = storm::dft::transformations::DftTransformer::transformBinaryDependencies(*transformedDft); + } + return transformedDft; +} + +template +std::shared_ptr> prepareForMarkovAnalysis(storm::dft::storage::DFT const& dft) { + return storm::dft::api::applyTransformations(dft, true, true, true); +} + +template<> +std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { + storm::dft::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); + storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + + // Set Don't Care elements + std::set dontCareElements; + if (!ftSettings.isDisableDC()) { + // Insert all elements as Don't Care elements + for (std::size_t i = 0; i < dft.nrElements(); i++) { + dontCareElements.insert(dft.getElement(i)->id()); + } + } + + // Transform to GSPN + storm::dft::transformations::DftToGspnTransformator gspnTransformator(dft); + auto priorities = gspnTransformator.computePriorities(dftGspnSettings.isExtendPriorities()); + gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed(), + dftGspnSettings.isExtendPriorities()); + std::shared_ptr gspn(gspnTransformator.obtainGSPN()); + return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId()); +} + +template<> +std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); +} + +std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) { + // Build Jani model + storm::builder::JaniGSPNBuilder builder(gspn); + std::shared_ptr model(builder.build("dft_gspn")); + + // Build properties + std::shared_ptr const& exprManager = gspn.getExpressionManager(); + storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); + storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); + // Add variable for easier access to 'failed' state + builder.addTransientVariable(model.get(), "failed", targetExpression); + auto failedFormula = std::make_shared(targetExpression); + auto properties = builder.getStandardProperties(model.get(), failedFormula, "Failed", "a failed state", true); + + // Export Jani to file + storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + if (dftGspnSettings.isWriteToJaniSet()) { + auto const& jani = storm::settings::getModule(); + storm::api::exportJaniToFile(*model, properties, dftGspnSettings.getWriteToJaniFilename(), jani.isCompactJsonSet()); + } + + return model; +} + +// Explicitly instantiate methods +template std::pair isWellFormed(storm::dft::storage::DFT const&, bool); +template std::pair hasPotentialModelingIssues(storm::dft::storage::DFT const&); +template std::shared_ptr> applyTransformations(storm::dft::storage::DFT const&, bool, bool, bool); +template std::shared_ptr> prepareForMarkovAnalysis(storm::dft::storage::DFT const&); + +template std::pair isWellFormed(storm::dft::storage::DFT const&, bool); +template std::pair hasPotentialModelingIssues(storm::dft::storage::DFT const&); +template std::shared_ptr> applyTransformations(storm::dft::storage::DFT const&, bool, + bool, bool); +template std::shared_ptr> prepareForMarkovAnalysis(storm::dft::storage::DFT const&); + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/api/transformation.h b/src/storm-dft/api/transformation.h new file mode 100644 index 0000000000..119f24c302 --- /dev/null +++ b/src/storm-dft/api/transformation.h @@ -0,0 +1,72 @@ +#pragma once + +#include + +#include "storm-dft/storage/DFT.h" +#include "storm-gspn/storage/gspn/GSPN.h" +#include "storm/storage/jani/Model.h" + +namespace storm::dft { +namespace api { + +/*! + * Check whether the DFT is well-formed. + * + * @param dft DFT. + * @param validForMarkovianAnalysis If true, additional checks are performed to check whether the DFT is valid for analysis via Markov models. + * @return Pair where the first entry is true iff the DFT is well-formed. The second entry contains the error messages for ill-formed parts. + */ +template +std::pair isWellFormed(storm::dft::storage::DFT const& dft, bool validForMarkovianAnalysis = true); + +/*! + * Check whether the DFT has potential modeling issues. + * + * @param dft DFT. + * @return Pair where the first entry is true iff the DFT has potential modeling issues. The second entry contains the warning messages for the issues. + */ +template +std::pair hasPotentialModelingIssues(storm::dft::storage::DFT const& dft); + +/*! + * Apply transformations for DFT. + * + * @param dft DFT. + * @param uniqueBE Flag whether a unique constant failed BE is created. + * @param binaryFDEP Flag whether all dependencies should be binary (only one dependent child). + * @param exponentialDistributions Flag whether distributions should be transformed to exponential distributions (if possible). + * @return Transformed DFT. + */ +template +std::shared_ptr> applyTransformations(storm::dft::storage::DFT const& dft, bool uniqueBE, bool binaryFDEP, + bool exponentialDistributions); + +/*! + * Apply transformations to make DFT feasible for Markovian analysis. + * + * @param dft DFT. + * @return Transformed DFT. + */ +template +std::shared_ptr> prepareForMarkovAnalysis(storm::dft::storage::DFT const& dft); + +/*! + * Transform DFT to GSPN. + * + * @param dft DFT. + * @return Pair of GSPN and id of failed place corresponding to the top level element. + */ +template +std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft); + +/*! + * Transform GSPN to Jani model. + * + * @param gspn GSPN. + * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. + * @return JANI model. + */ +std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace); + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/modelchecker/DFTModelChecker.cpp b/src/storm-dft/modelchecker/DFTModelChecker.cpp index 0f378ead7d..4983244ea2 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/DFTModelChecker.cpp @@ -1,6 +1,6 @@ #include "storm-dft/modelchecker/DFTModelChecker.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/utility/SymmetryFinder.h" diff --git a/src/storm-dft/modelchecker/DftModularizationChecker.cpp b/src/storm-dft/modelchecker/DftModularizationChecker.cpp index 3b301675c8..4559b9913a 100644 --- a/src/storm-dft/modelchecker/DftModularizationChecker.cpp +++ b/src/storm-dft/modelchecker/DftModularizationChecker.cpp @@ -3,7 +3,7 @@ #include #include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h" -#include "storm-dft/api/storm-dft.h" + #include "storm-dft/builder/DFTBuilder.h" #include "storm-dft/modelchecker/DFTModelChecker.h" #include "storm-dft/modelchecker/SFTBDDChecker.h" diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index d61db3061c..fde3b9746b 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -2,6 +2,9 @@ #include "test/storm_gtest.h" #include "storm-dft/api/storm-dft.h" +#include "storm-dft/modelchecker/DFTASFChecker.h" +#include "storm-dft/utility/FDEPConflictFinder.h" +#include "storm-dft/utility/FailureBoundFinder.h" namespace { class DftSmt : public ::testing::Test { From ce5c4145da3b277d2831befec6c85ebd8b2c5a62 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 23 Aug 2026 22:54:47 +0200 Subject: [PATCH 3/6] Clean up includes --- src/storm-dft-cli/storm-dft.cpp | 1 + src/storm-dft/modelchecker/DFTModelChecker.cpp | 5 ++++- src/storm-dft/modelchecker/DFTModelChecker.h | 3 +-- src/storm-dft/modelchecker/DftModularizationChecker.cpp | 5 +---- src/storm-dft/modelchecker/DftModularizationChecker.h | 1 - src/test/storm-dft/api/DftApproximationTest.cpp | 8 ++++++-- src/test/storm-dft/api/DftModelBuildingTest.cpp | 8 ++++++-- src/test/storm-dft/api/DftModelCheckerTest.cpp | 8 ++++++-- src/test/storm-dft/api/DftParserTest.cpp | 3 ++- src/test/storm-dft/api/DftSmtTest.cpp | 3 ++- src/test/storm-dft/api/DftValidatorTest.cpp | 3 ++- src/test/storm-dft/bdd/TestBdd.cpp | 6 +++--- src/test/storm-dft/bdd/TestBddModularizer.cpp | 2 +- src/test/storm-dft/bdd/TestBddVarOrdering.cpp | 3 +-- src/test/storm-dft/simulator/DftSimulatorTest.cpp | 6 +++--- src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp | 5 +++-- src/test/storm-dft/simulator/ImportanceFunction.cpp | 6 +++--- src/test/storm-dft/storage/BEDistributionTest.cpp | 9 ++++++--- src/test/storm-dft/storage/DftBETest.cpp | 8 +++++++- src/test/storm-dft/storage/DftModuleTest.cpp | 3 +-- src/test/storm-dft/storage/SymmetryTest.cpp | 2 +- .../storm-dft/transformations/DftInstantiatorTest.cpp | 2 +- .../storm-dft/transformations/DftTransformerTest.cpp | 2 +- 23 files changed, 62 insertions(+), 40 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 0deb52fdaf..b41d3a300e 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -10,6 +10,7 @@ #include "storm-gspn/api/storm-gspn.h" #include "storm-parsers/api/properties.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/api/properties.h" #include "storm/exceptions/UnmetRequirementException.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/IOSettings.h" diff --git a/src/storm-dft/modelchecker/DFTModelChecker.cpp b/src/storm-dft/modelchecker/DFTModelChecker.cpp index 4983244ea2..821ecadc4f 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/DFTModelChecker.cpp @@ -1,10 +1,13 @@ -#include "storm-dft/modelchecker/DFTModelChecker.h" +#include "DFTModelChecker.h" #include "storm-dft/api/transformation.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/utility/SymmetryFinder.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/api/bisimulation.h" +#include "storm/api/export.h" +#include "storm/api/verification.h" #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/exceptions/InvalidModelException.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" diff --git a/src/storm-dft/modelchecker/DFTModelChecker.h b/src/storm-dft/modelchecker/DFTModelChecker.h index 8f558bdc81..7716017d44 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/DFTModelChecker.h @@ -4,9 +4,8 @@ #include "storm-dft/storage/DFT.h" #include "storm-dft/utility/RelevantEvents.h" -#include "storm/api/storm.h" #include "storm/logic/Formula.h" -#include "storm/modelchecker/results/CheckResult.h" +#include "storm/transformer/NonMarkovianChainTransformer.h" #include "storm/utility/Stopwatch.h" namespace storm::dft { diff --git a/src/storm-dft/modelchecker/DftModularizationChecker.cpp b/src/storm-dft/modelchecker/DftModularizationChecker.cpp index 4559b9913a..e308aa2abb 100644 --- a/src/storm-dft/modelchecker/DftModularizationChecker.cpp +++ b/src/storm-dft/modelchecker/DftModularizationChecker.cpp @@ -3,16 +3,13 @@ #include #include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h" - #include "storm-dft/builder/DFTBuilder.h" #include "storm-dft/modelchecker/DFTModelChecker.h" #include "storm-dft/modelchecker/SFTBDDChecker.h" #include "storm-dft/utility/DftModularizer.h" -#include "storm/environment/Environment.h" - #include "storm-parsers/api/properties.h" #include "storm/api/properties.h" -#include "storm/exceptions/InvalidModelException.h" +#include "storm/storage/jani/Property.h" namespace storm::dft { namespace modelchecker { diff --git a/src/storm-dft/modelchecker/DftModularizationChecker.h b/src/storm-dft/modelchecker/DftModularizationChecker.h index 9d27948c42..15198fb9a4 100644 --- a/src/storm-dft/modelchecker/DftModularizationChecker.h +++ b/src/storm-dft/modelchecker/DftModularizationChecker.h @@ -7,7 +7,6 @@ #include "storm-dft/storage/DFT.h" #include "storm-dft/storage/DftModule.h" #include "storm-dft/storage/SylvanBddManager.h" -#include "storm/logic/Formula.h" namespace storm::dft { namespace modelchecker { diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index 3649365162..85269fad69 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -1,8 +1,12 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" -#include "storm-parsers/api/storm-parsers.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" +#include "storm-parsers/api/properties.h" +#include "storm/api/properties.h" +#include "storm/storage/jani/Property.h" namespace { diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index cde9633854..cc5eb9f767 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -1,9 +1,13 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" -#include "storm-parsers/api/storm-parsers.h" +#include "storm-dft/utility/RelevantEvents.h" +#include "storm-parsers/api/properties.h" +#include "storm/api/properties.h" +#include "storm/storage/jani/Property.h" namespace { diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index b62c99fd38..79f99b2822 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -1,8 +1,12 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" -#include "storm-parsers/api/storm-parsers.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" +#include "storm-parsers/api/properties.h" +#include "storm/api/properties.h" +#include "storm/storage/jani/Property.h" namespace { diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp index 1fe9bcfb2d..f9f5e14bcf 100644 --- a/src/test/storm-dft/api/DftParserTest.cpp +++ b/src/test/storm-dft/api/DftParserTest.cpp @@ -1,7 +1,8 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index fde3b9746b..8c009cefb6 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -1,7 +1,8 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/modelchecker/DFTASFChecker.h" #include "storm-dft/utility/FDEPConflictFinder.h" #include "storm-dft/utility/FailureBoundFinder.h" diff --git a/src/test/storm-dft/api/DftValidatorTest.cpp b/src/test/storm-dft/api/DftValidatorTest.cpp index 7b426decd1..94b1c89851 100644 --- a/src/test/storm-dft/api/DftValidatorTest.cpp +++ b/src/test/storm-dft/api/DftValidatorTest.cpp @@ -2,7 +2,8 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm/exceptions/WrongFormatException.h" namespace { diff --git a/src/test/storm-dft/bdd/TestBdd.cpp b/src/test/storm-dft/bdd/TestBdd.cpp index d25ff81dbc..1c166abdef 100644 --- a/src/test/storm-dft/bdd/TestBdd.cpp +++ b/src/test/storm-dft/bdd/TestBdd.cpp @@ -2,12 +2,12 @@ #include "test/storm_gtest.h" #include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" #include "storm-dft/modelchecker/SFTBDDChecker.h" -#include "storm-dft/transformations/SftToBddTransformator.h" #include "storm-dft/utility/MTTFHelper.h" #include "storm-parsers/api/properties.h" -#include "storm/environment/Environment.h" +#include "storm/api/properties.h" +#include "storm/storage/jani/Property.h" namespace { diff --git a/src/test/storm-dft/bdd/TestBddModularizer.cpp b/src/test/storm-dft/bdd/TestBddModularizer.cpp index 311d83285f..0b7b9f27d7 100644 --- a/src/test/storm-dft/bdd/TestBddModularizer.cpp +++ b/src/test/storm-dft/bdd/TestBddModularizer.cpp @@ -1,7 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" #include "storm-dft/modelchecker/DftModularizationChecker.h" namespace { diff --git a/src/test/storm-dft/bdd/TestBddVarOrdering.cpp b/src/test/storm-dft/bdd/TestBddVarOrdering.cpp index ed5577f9d1..7bbd05ceba 100644 --- a/src/test/storm-dft/bdd/TestBddVarOrdering.cpp +++ b/src/test/storm-dft/bdd/TestBddVarOrdering.cpp @@ -1,10 +1,9 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" #include "storm-dft/parser/BEOrderParser.h" #include "storm-dft/transformations/SftToBddTransformator.h" -#include "storm/environment/Environment.h" namespace { diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 93beba164c..b7dbb89293 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -1,10 +1,10 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" -#include "storm-dft/generator/DftNextStateGenerator.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/simulator/DFTTraceSimulator.h" -#include "storm-dft/storage/DftSymmetries.h" namespace { diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index a0feb68aa4..b40e54c8a1 100644 --- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp +++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp @@ -1,11 +1,12 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/generator/DftNextStateGenerator.h" #include "storm-dft/simulator/DFTTraceSimulator.h" #include "storm-dft/utility/SymmetryFinder.h" -#include "storm-parsers/api/storm-parsers.h" namespace { diff --git a/src/test/storm-dft/simulator/ImportanceFunction.cpp b/src/test/storm-dft/simulator/ImportanceFunction.cpp index 8a3ee078cb..a0c5c31d49 100644 --- a/src/test/storm-dft/simulator/ImportanceFunction.cpp +++ b/src/test/storm-dft/simulator/ImportanceFunction.cpp @@ -1,11 +1,11 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" -#include "storm-dft/generator/DftNextStateGenerator.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/simulator/DFTTraceSimulator.h" #include "storm-dft/simulator/ImportanceFunction.h" -#include "storm-dft/storage/DftSymmetries.h" namespace { diff --git a/src/test/storm-dft/storage/BEDistributionTest.cpp b/src/test/storm-dft/storage/BEDistributionTest.cpp index d0ecabfd99..3bf01079bd 100644 --- a/src/test/storm-dft/storage/BEDistributionTest.cpp +++ b/src/test/storm-dft/storage/BEDistributionTest.cpp @@ -1,10 +1,13 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/analysis.h" +#include "storm-dft/api/io.h" +#include "storm-dft/api/transformation.h" #include "storm-dft/modelchecker/SFTBDDChecker.h" -#include "storm-parsers/api/storm-parsers.h" -#include "storm/environment/Environment.h" +#include "storm-parsers/api/properties.h" +#include "storm/api/properties.h" +#include "storm/storage/jani/Property.h" namespace { diff --git a/src/test/storm-dft/storage/DftBETest.cpp b/src/test/storm-dft/storage/DftBETest.cpp index 1004b3ebd5..631f3dc7b0 100644 --- a/src/test/storm-dft/storage/DftBETest.cpp +++ b/src/test/storm-dft/storage/DftBETest.cpp @@ -3,7 +3,13 @@ #include -#include "storm-dft/storage/elements/DFTElements.h" +#include "storm-dft/storage/elements/BEConst.h" +#include "storm-dft/storage/elements/BEErlang.h" +#include "storm-dft/storage/elements/BEExponential.h" +#include "storm-dft/storage/elements/BELogNormal.h" +#include "storm-dft/storage/elements/BEProbability.h" +#include "storm-dft/storage/elements/BESamples.h" +#include "storm-dft/storage/elements/BEWeibull.h" namespace { diff --git a/src/test/storm-dft/storage/DftModuleTest.cpp b/src/test/storm-dft/storage/DftModuleTest.cpp index 11de41eec7..06a0ab6638 100644 --- a/src/test/storm-dft/storage/DftModuleTest.cpp +++ b/src/test/storm-dft/storage/DftModuleTest.cpp @@ -1,8 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" -#include "storm-dft/storage/DftModule.h" +#include "storm-dft/api/io.h" #include "storm-dft/utility/DftModularizer.h" namespace { diff --git a/src/test/storm-dft/storage/SymmetryTest.cpp b/src/test/storm-dft/storage/SymmetryTest.cpp index b9e6bbd486..1fbd934950 100644 --- a/src/test/storm-dft/storage/SymmetryTest.cpp +++ b/src/test/storm-dft/storage/SymmetryTest.cpp @@ -1,7 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" #include "storm-dft/utility/SymmetryFinder.h" namespace { diff --git a/src/test/storm-dft/transformations/DftInstantiatorTest.cpp b/src/test/storm-dft/transformations/DftInstantiatorTest.cpp index dec8d8eb07..e02f77b505 100644 --- a/src/test/storm-dft/transformations/DftInstantiatorTest.cpp +++ b/src/test/storm-dft/transformations/DftInstantiatorTest.cpp @@ -1,7 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" #include "storm-dft/transformations/DftInstantiator.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/test/storm-dft/transformations/DftTransformerTest.cpp b/src/test/storm-dft/transformations/DftTransformerTest.cpp index 8e1eb73162..4c3ee639eb 100644 --- a/src/test/storm-dft/transformations/DftTransformerTest.cpp +++ b/src/test/storm-dft/transformations/DftTransformerTest.cpp @@ -1,7 +1,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm-dft/api/storm-dft.h" +#include "storm-dft/api/io.h" #include "storm-dft/transformations/DftTransformer.h" namespace { From 282c439ef682379fd1e8e8065c2d390b3eccefe4 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 23 Aug 2026 22:55:18 +0200 Subject: [PATCH 4/6] Minor improvements --- src/storm-dft/api/analysis.cpp | 8 ++++---- src/storm-dft/api/analysis.h | 4 ++-- src/storm-dft/modelchecker/DFTModelChecker.cpp | 7 +++---- src/storm-dft/modelchecker/DFTModelChecker.h | 10 +++++----- .../modelchecker/DftModularizationChecker.cpp | 4 ++-- src/test/storm-dft/api/DftApproximationTest.cpp | 4 ++-- src/test/storm-dft/api/DftModelCheckerTest.cpp | 14 +++++++------- .../storm-dft/simulator/DftTraceGeneratorTest.cpp | 2 +- src/test/storm-dft/storage/DftBETest.cpp | 2 +- 9 files changed, 27 insertions(+), 28 deletions(-) diff --git a/src/storm-dft/api/analysis.cpp b/src/storm-dft/api/analysis.cpp index 6fe9f6a55a..322f52188c 100644 --- a/src/storm-dft/api/analysis.cpp +++ b/src/storm-dft/api/analysis.cpp @@ -232,13 +232,13 @@ bool computeDependencyConflicts(storm::dft::storage::DFT& dft, bool u } // Set the conflict map of the dft - std::set conflict_set; + std::set conflict_set; for (auto const& conflict : fdepConflicts) { - conflict_set.insert(size_t(conflict.first)); - conflict_set.insert(size_t(conflict.second)); + conflict_set.insert(conflict.first); + conflict_set.insert(conflict.second); } for (size_t depId : dft.getDependencies()) { - if (!conflict_set.count(depId)) { + if (!conflict_set.contains(depId)) { dft.setDependencyNotInConflict(depId); } } diff --git a/src/storm-dft/api/analysis.h b/src/storm-dft/api/analysis.h index 48b23b82e0..e664bae054 100644 --- a/src/storm-dft/api/analysis.h +++ b/src/storm-dft/api/analysis.h @@ -55,12 +55,12 @@ typename storm::dft::modelchecker::DFTModelChecker::dft_results analy * @param dft DFT * @param exportToDot If true exports the bdd representing the top level event of the dft in the dot format * @param filename The name of the file for exporting to dot - * @param calculateMTTF If true calculates the mean time to failure + * @param calculateMttf If true calculates the mean time to failure * @param mttfPrecision A constant that is used to determine if the mttf calculation converged * @param mttfStepsize A constant that is used in the mttf calculation * @param mttfAlgorithmName The name of the mttf algorithm to use * @param calculateMCS If true calculates the minimal cut sets - * @param calculateProbability If true calculates the system failure propbability + * @param calculateProbability If true calculates the system failure probability * @param useModularisation If true tries modularisation * @param importanceMeasureName The name of the importance measure to calculate * @param timepoints The timebounds for probability calculations diff --git a/src/storm-dft/modelchecker/DFTModelChecker.cpp b/src/storm-dft/modelchecker/DFTModelChecker.cpp index 821ecadc4f..c3d2d06695 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/DFTModelChecker.cpp @@ -178,7 +178,7 @@ std::shared_ptr> DFTModelChecker::dft_results DFTModelChecker::che return results; } else { // Build a single Markov Automaton - auto ioSettings = storm::settings::getModule(); STORM_LOG_DEBUG("Building Model..."); storm::dft::builder::ExplicitDFTModelBuilder builder(dft, symmetries); builder.buildModel(0, 0.0); @@ -500,7 +499,7 @@ bool DFTModelChecker::isApproximationSufficient(double lowerBound, doubl } template -void DFTModelChecker::printTimings(std::ostream& os) { +void DFTModelChecker::printTimings(std::ostream& os) const { os << "Times:\n"; os << "Exploration:\t" << explorationTimer << '\n'; os << "Building:\t" << buildingTimer << '\n'; @@ -510,7 +509,7 @@ void DFTModelChecker::printTimings(std::ostream& os) { } template -void DFTModelChecker::printResults(dft_results const& results, std::ostream& os) { +void DFTModelChecker::printResults(dft_results const& results, std::ostream& os) const { bool first = true; os << "Result: ["; for (auto result : results) { diff --git a/src/storm-dft/modelchecker/DFTModelChecker.h b/src/storm-dft/modelchecker/DFTModelChecker.h index 7716017d44..7a93de0ce7 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/DFTModelChecker.h @@ -48,7 +48,7 @@ class DFTModelChecker { * @param allowDCForRelevant Whether to allow Don't Care propagation 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 eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA * @param labelBehavior Behavior of labels of eliminated states * @return Model checking results for the given properties.. */ @@ -64,7 +64,7 @@ class DFTModelChecker { * * @param os Output stream to write to. */ - void printTimings(std::ostream& os = std::cout); + void printTimings(std::ostream& os = std::cout) const; /*! * Print result to stream. @@ -72,7 +72,7 @@ class DFTModelChecker { * @param results List of results. * @param os Output stream to write to. */ - void printResults(dft_results const& results, std::ostream& os = std::cout); + void printResults(dft_results const& results, std::ostream& os = std::cout) const; private: bool printInfo; @@ -95,7 +95,7 @@ class DFTModelChecker { * @param allowDCForRelevant Whether to allow Don't Care propagation 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 eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA * @param labelBehavior Behavior of labels of eliminated states * @return Model checking results (or in case of approximation two results for lower and upper bound) */ @@ -131,7 +131,7 @@ class DFTModelChecker { * @param allowDCForRelevant Whether to allow Don't Care propagation 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 eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA * @param labelBehavior Behavior of labels of eliminated states * * @return Model checking result diff --git a/src/storm-dft/modelchecker/DftModularizationChecker.cpp b/src/storm-dft/modelchecker/DftModularizationChecker.cpp index e308aa2abb..15688137ac 100644 --- a/src/storm-dft/modelchecker/DftModularizationChecker.cpp +++ b/src/storm-dft/modelchecker/DftModularizationChecker.cpp @@ -96,7 +96,7 @@ std::shared_ptr> DftModularizationCheckername(), it->second); - } else if (dynamicElements.find(id) == dynamicElements.end()) { + } else if (!dynamicElements.contains(id)) { // Element is not part of a dynamic module -> keep builder.cloneElement(element); // Remember dependency conflict @@ -111,7 +111,7 @@ std::shared_ptr> DftModularizationCheckergetDependencies()) { // Set dependencies not in conflict - if (depInConflict.find(newDft->getElement(id)->name()) == depInConflict.end()) { + if (!depInConflict.contains(newDft->getElement(id)->name())) { newDft->setDependencyNotInConflict(id); } } diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index 85269fad69..07214bba3c 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -55,7 +55,7 @@ class DftApproximationTest : public ::testing::Test { return config; } - std::pair analyzeMTTF(std::string const& file, double errorBound) { + std::pair analyzeMTTF(std::string const& file, double errorBound) const { std::shared_ptr> dft = storm::dft::api::prepareForMarkovAnalysis(*storm::dft::api::loadDFTGalileoFile(file)); EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first); @@ -66,7 +66,7 @@ class DftApproximationTest : public ::testing::Test { return boost::get::approximation_result>(results[0]); } - std::pair analyzeTimebound(std::string const& file, double timeBound, double errorBound) { + std::pair analyzeTimebound(std::string const& file, double timeBound, double errorBound) const { std::shared_ptr> dft = storm::dft::api::prepareForMarkovAnalysis(*storm::dft::api::loadDFTGalileoFile(file)); EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first); diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 79f99b2822..b98d314f46 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -92,7 +92,7 @@ class DftModelCheckerTest : public ::testing::Test { return config; } - double analyze(std::string const& file, std::string const& property) { + double analyze(std::string const& file, std::string const& property) const { // Load, build and prepare DFT std::shared_ptr> dft = storm::dft::api::prepareForMarkovAnalysis(*(storm::dft::api::loadDFTGalileoFile(file))); @@ -114,26 +114,26 @@ class DftModelCheckerTest : public ::testing::Test { return boost::get(results[0]); } - double analyzeMTTF(std::string const& file) { + double analyzeMTTF(std::string const& file) const { std::string property = "Tmin=? [F \"failed\"]"; return analyze(file, property); } - double analyzeReliability(std::string const& file, double bound) { + double analyzeReliability(std::string const& file, double bound) const { std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; return analyze(file, property); } - double analyzeReachability(std::string const& file) { + double analyzeReachability(std::string const& file) const { std::string property = "Pmin=? [F \"failed\"]"; return analyze(file, property); } - double precision() { + double precision() const { return 1e-12; } - double precisionReliability() { + double precisionReliability() const { return 1e-10; } @@ -192,7 +192,7 @@ TYPED_TEST(DftModelCheckerTest, FdepMTTF) { STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"), storm::exceptions::NotSupportedException); STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft"), storm::exceptions::NotSupportedException); } else { - double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"); + result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"); EXPECT_NEAR(result, 2 / 3.0, this->precision()); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"); EXPECT_NEAR(result, 1, this->precision()); diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index b40e54c8a1..cd7c225773 100644 --- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp +++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp @@ -64,7 +64,7 @@ class DftTraceGeneratorTest : public ::testing::Test { return config; } - std::pair>, storm::dft::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) { + std::pair>, storm::dft::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) const { // Load, build and prepare DFT std::shared_ptr> dft = storm::dft::api::prepareForMarkovAnalysis(*(storm::dft::api::loadDFTGalileoFile(file))); diff --git a/src/test/storm-dft/storage/DftBETest.cpp b/src/test/storm-dft/storage/DftBETest.cpp index 631f3dc7b0..2ac80fbb36 100644 --- a/src/test/storm-dft/storage/DftBETest.cpp +++ b/src/test/storm-dft/storage/DftBETest.cpp @@ -113,7 +113,7 @@ TEST(DftBETest, FailureWeibullExponential) { EXPECT_NEAR(boost::math::cdf(dist2, t), be2.getUnreliability(t), 1e-10); } - // Decreasing faiure rate + // Decreasing failure rate storm::dft::storage::elements::BEWeibull be3(0, "TestBE", 0.4, 2); EXPECT_TRUE(be3.canFail()); From 0e891f4232c5e9b98a53cd9050f210741e2fa9e8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 23 Aug 2026 23:26:19 +0200 Subject: [PATCH 5/6] Added missing include --- src/storm-dft/parser/BEOrderParser.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm-dft/parser/BEOrderParser.h b/src/storm-dft/parser/BEOrderParser.h index 628e506901..7cc574055c 100644 --- a/src/storm-dft/parser/BEOrderParser.h +++ b/src/storm-dft/parser/BEOrderParser.h @@ -1,5 +1,6 @@ #pragma once +#include #include namespace storm::dft { From 650bf5807a8fc206d25ecee3d5f963c09428ef63 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Aug 2026 21:25:38 +0200 Subject: [PATCH 6/6] Separate api file gspn_transformation --- src/storm-dft-cli/storm-dft.cpp | 1 + src/storm-dft/api/gspn_transformation.cpp | 69 +++++++++++++++++++++++ src/storm-dft/api/gspn_transformation.h | 31 ++++++++++ src/storm-dft/api/transformation.cpp | 60 -------------------- src/storm-dft/api/transformation.h | 20 ------- 5 files changed, 101 insertions(+), 80 deletions(-) create mode 100644 src/storm-dft/api/gspn_transformation.cpp create mode 100644 src/storm-dft/api/gspn_transformation.h diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index b41d3a300e..9d3b9b3faf 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -1,5 +1,6 @@ #include "storm-cli-utilities/cli.h" #include "storm-dft/api/analysis.h" +#include "storm-dft/api/gspn_transformation.h" #include "storm-dft/api/io.h" #include "storm-dft/api/transformation.h" #include "storm-dft/parser/BEOrderParser.h" diff --git a/src/storm-dft/api/gspn_transformation.cpp b/src/storm-dft/api/gspn_transformation.cpp new file mode 100644 index 0000000000..f388d7ba42 --- /dev/null +++ b/src/storm-dft/api/gspn_transformation.cpp @@ -0,0 +1,69 @@ +#include "gspn_transformation.h" + +#include + +#include "storm-conv/api/storm-conv.h" +#include "storm-conv/settings/modules/JaniExportSettings.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" +#include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-gspn/builder/JaniGSPNBuilder.h" +#include "storm/settings/SettingsManager.h" + +namespace storm::dft { +namespace api { + +template<> +std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { + storm::dft::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); + storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + + // Set Don't Care elements + std::set dontCareElements; + if (!ftSettings.isDisableDC()) { + // Insert all elements as Don't Care elements + for (std::size_t i = 0; i < dft.nrElements(); i++) { + dontCareElements.insert(dft.getElement(i)->id()); + } + } + + // Transform to GSPN + storm::dft::transformations::DftToGspnTransformator gspnTransformator(dft); + auto priorities = gspnTransformator.computePriorities(dftGspnSettings.isExtendPriorities()); + gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed(), + dftGspnSettings.isExtendPriorities()); + std::shared_ptr gspn(gspnTransformator.obtainGSPN()); + return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId()); +} + +template<> +std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); +} + +std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) { + // Build Jani model + storm::builder::JaniGSPNBuilder builder(gspn); + std::shared_ptr model(builder.build("dft_gspn")); + + // Build properties + std::shared_ptr const& exprManager = gspn.getExpressionManager(); + storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); + storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); + // Add variable for easier access to 'failed' state + builder.addTransientVariable(model.get(), "failed", targetExpression); + auto failedFormula = std::make_shared(targetExpression); + auto properties = builder.getStandardProperties(model.get(), failedFormula, "Failed", "a failed state", true); + + // Export Jani to file + storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); + if (dftGspnSettings.isWriteToJaniSet()) { + auto const& jani = storm::settings::getModule(); + storm::api::exportJaniToFile(*model, properties, dftGspnSettings.getWriteToJaniFilename(), jani.isCompactJsonSet()); + } + + return model; +} + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/api/gspn_transformation.h b/src/storm-dft/api/gspn_transformation.h new file mode 100644 index 0000000000..6b8b0f2669 --- /dev/null +++ b/src/storm-dft/api/gspn_transformation.h @@ -0,0 +1,31 @@ +#pragma once + +#include + +#include "storm-dft/storage/DFT.h" +#include "storm-gspn/storage/gspn/GSPN.h" +#include "storm/storage/jani/Model.h" + +namespace storm::dft { +namespace api { + +/*! + * Transform DFT to GSPN. + * + * @param dft DFT. + * @return Pair of GSPN and id of failed place corresponding to the top level element. + */ +template +std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft); + +/*! + * Transform GSPN to Jani model. + * + * @param gspn GSPN. + * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. + * @return JANI model. + */ +std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace); + +} // namespace api +} // namespace storm::dft diff --git a/src/storm-dft/api/transformation.cpp b/src/storm-dft/api/transformation.cpp index 2a57b53f59..3e4dfb2402 100644 --- a/src/storm-dft/api/transformation.cpp +++ b/src/storm-dft/api/transformation.cpp @@ -2,16 +2,8 @@ #include -#include "storm-conv/api/storm-conv.h" -#include "storm-conv/settings/modules/JaniExportSettings.h" -#include "storm-dft/settings/modules/DftGspnSettings.h" -#include "storm-dft/settings/modules/FaultTreeSettings.h" -#include "storm-dft/storage/DFT.h" -#include "storm-dft/transformations/DftToGspnTransformator.h" #include "storm-dft/transformations/DftTransformer.h" #include "storm-dft/utility/DftValidator.h" -#include "storm-gspn/builder/JaniGSPNBuilder.h" -#include "storm/settings/SettingsManager.h" namespace storm::dft { namespace api { @@ -56,58 +48,6 @@ std::shared_ptr> prepareForMarkovAnalysis(st return storm::dft::api::applyTransformations(dft, true, true, true); } -template<> -std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { - storm::dft::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); - storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - - // Set Don't Care elements - std::set dontCareElements; - if (!ftSettings.isDisableDC()) { - // Insert all elements as Don't Care elements - for (std::size_t i = 0; i < dft.nrElements(); i++) { - dontCareElements.insert(dft.getElement(i)->id()); - } - } - - // Transform to GSPN - storm::dft::transformations::DftToGspnTransformator gspnTransformator(dft); - auto priorities = gspnTransformator.computePriorities(dftGspnSettings.isExtendPriorities()); - gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed(), - dftGspnSettings.isExtendPriorities()); - std::shared_ptr gspn(gspnTransformator.obtainGSPN()); - return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId()); -} - -template<> -std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type."); -} - -std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) { - // Build Jani model - storm::builder::JaniGSPNBuilder builder(gspn); - std::shared_ptr model(builder.build("dft_gspn")); - - // Build properties - std::shared_ptr const& exprManager = gspn.getExpressionManager(); - storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); - storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); - // Add variable for easier access to 'failed' state - builder.addTransientVariable(model.get(), "failed", targetExpression); - auto failedFormula = std::make_shared(targetExpression); - auto properties = builder.getStandardProperties(model.get(), failedFormula, "Failed", "a failed state", true); - - // Export Jani to file - storm::dft::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - if (dftGspnSettings.isWriteToJaniSet()) { - auto const& jani = storm::settings::getModule(); - storm::api::exportJaniToFile(*model, properties, dftGspnSettings.getWriteToJaniFilename(), jani.isCompactJsonSet()); - } - - return model; -} - // Explicitly instantiate methods template std::pair isWellFormed(storm::dft::storage::DFT const&, bool); template std::pair hasPotentialModelingIssues(storm::dft::storage::DFT const&); diff --git a/src/storm-dft/api/transformation.h b/src/storm-dft/api/transformation.h index 119f24c302..32b294b562 100644 --- a/src/storm-dft/api/transformation.h +++ b/src/storm-dft/api/transformation.h @@ -3,8 +3,6 @@ #include #include "storm-dft/storage/DFT.h" -#include "storm-gspn/storage/gspn/GSPN.h" -#include "storm/storage/jani/Model.h" namespace storm::dft { namespace api { @@ -50,23 +48,5 @@ std::shared_ptr> applyTransformations(storm: template std::shared_ptr> prepareForMarkovAnalysis(storm::dft::storage::DFT const& dft); -/*! - * Transform DFT to GSPN. - * - * @param dft DFT. - * @return Pair of GSPN and id of failed place corresponding to the top level element. - */ -template -std::pair, uint64_t> transformToGSPN(storm::dft::storage::DFT const& dft); - -/*! - * Transform GSPN to Jani model. - * - * @param gspn GSPN. - * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. - * @return JANI model. - */ -std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace); - } // namespace api } // namespace storm::dft