Replaced settings by environments in storm-dft - #1037
Draft
volkm wants to merge 15 commits into
Draft
Conversation
There was a problem hiding this comment.
🔵 Needs a closer look
The new CLI settings contain a potential infinite loop in timepoints generation and incomplete validation for dependent GSPN options.
Pull request overview
This PR migrates storm-dft from using global settings modules to a dedicated storm::dft::DftEnvironment (with sub-environments for analysis, model building, and transformations), moving DFT-specific settings fully into storm-dft-cli while keeping Storm core settings available via the embedded storm::Environment.
Changes:
- Introduces
storm::dft::DftEnvironment(+AnalysisEnvironment,ModelBuilderEnvironment,TransformationEnvironment) and wires it through DFT model building and checking. - Splits the former monolithic
storm-dft/api/storm-dft.hintoanalysis.h,io.h,transformation.h, andgspn_transformation.h, updating CLI and tests accordingly. - Refactors
storm::SubEnvironmentand adds explicit template instantiations (CoreEnvironments.cpp/DftEnvironments.cpp) to support environment usage across libraries without redundant instantiation.
File summaries
| File | Description |
|---|---|
| src/test/storm-dft/transformations/DftTransformerTest.cpp | Update API include to io.h. |
| src/test/storm-dft/transformations/DftInstantiatorTest.cpp | Update API include to io.h. |
| src/test/storm-dft/storage/SymmetryTest.cpp | Update API include to io.h. |
| src/test/storm-dft/storage/DftModuleTest.cpp | Update API include to io.h and related headers. |
| src/test/storm-dft/storage/DftBETest.cpp | Use explicit BE element includes; fix comment typo. |
| src/test/storm-dft/storage/BEDistributionTest.cpp | Switch analysis calls to DftEnvironment + new property APIs. |
| src/test/storm-dft/simulator/ImportanceFunction.cpp | Update API includes; adapt computeRelevantEvents signature. |
| src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp | Update API includes; adjust const-correctness and relevant-events computation. |
| src/test/storm-dft/simulator/DftSimulatorTest.cpp | Update API includes; adapt relevant-events computation. |
| src/test/storm-dft/environment/DftEnvironmentTest.cpp | New unit tests for DftEnvironment defaults/get-set/copy. |
| src/test/storm-dft/CMakeLists.txt | Add environment testsuite target. |
| src/test/storm-dft/bdd/TestBddVarOrdering.cpp | Update includes to new API headers. |
| src/test/storm-dft/bdd/TestBddModularizer.cpp | Update includes to new API headers. |
| src/test/storm-dft/bdd/TestBdd.cpp | Update includes to new property + DFT API headers. |
| src/test/storm-dft/api/DftValidatorTest.cpp | Update includes to io.h/transformation.h. |
| src/test/storm-dft/api/DftSmtTest.cpp | Update includes; include checker/utility headers explicitly. |
| src/test/storm-dft/api/DftParserTest.cpp | Update includes to io.h/transformation.h. |
| src/test/storm-dft/api/DftModelCheckerTest.cpp | Refactor test configs to construct DftEnvironment; update analysis call. |
| src/test/storm-dft/api/DftModelBuildingTest.cpp | Pass DftEnvironment into model builder; update property APIs. |
| src/test/storm-dft/api/DftApproximationTest.cpp | Use DftEnvironment for approximation config; update analysis call. |
| src/storm/environment/SubEnvironment.h | Move SubEnvironment method definitions to header (for extern template usage). |
| src/storm/environment/solver/SolverEnvironment.h | Add extern-template decls; reorder declarations/accessors. |
| src/storm/environment/solver/SolverEnvironment.cpp | Reorder/adjust accessors and move flag accessors to end. |
| src/storm/environment/solver/MinMaxSolverEnvironment.h | Add extern-template for LP sub-environment; reorder members. |
| src/storm/environment/modelchecker/ModelCheckerEnvironment.h | Add extern-template decls for sub-environments. |
| src/storm/environment/Environment.h | Reorder core sub-environments; add extern-template decls. |
| src/storm/environment/Environment.cpp | Reorder accessors to match header layout. |
| src/storm/environment/dd/DdEnvironment.h | Add extern-template decls; reorder selector specializations/members. |
| src/storm/environment/CoreEnvironments.cpp | Centralize explicit instantiations for core environments/sub-environments. |
| src/storm-dft/utility/RelevantEvents.h | Remove settings dependency; pass addLabelsClaiming explicitly. |
| src/storm-dft/settings/DftSettings.cpp | Remove DFT-specific settings module registrations from library init. |
| src/storm-dft/parser/DFTJsonParser.h | Replace heavy includes with forward declarations. |
| src/storm-dft/parser/DFTJsonParser.cpp | Add explicit includes needed after forward declarations. |
| src/storm-dft/parser/DFTGalileoParser.h | Replace heavy includes with forward declarations; add <string>. |
| src/storm-dft/parser/DFTGalileoParser.cpp | Add explicit includes needed after forward declarations. |
| src/storm-dft/parser/BEOrderParser.h | Reduce includes; add forward declaration for DFT. |
| src/storm-dft/parser/BEOrderParser.cpp | Add explicit include for DFT. |
| src/storm-dft/modelchecker/DftModularizationChecker.h | Remove unused formula include. |
| src/storm-dft/modelchecker/DftModularizationChecker.cpp | Use environment-based check API; modernize .contains() usage. |
| src/storm-dft/modelchecker/DFTModelChecker.h | Switch to environment-based API; add model export callback. |
| src/storm-dft/modelchecker/DFTModelChecker.cpp | Thread DftEnvironment through checking/building/export; replace settings usage. |
| src/storm-dft/generator/DftNextStateGenerator.h | Make dependency-choice behavior an explicit expand parameter. |
| src/storm-dft/generator/DftNextStateGenerator.cpp | Remove settings dependency; pass dependency-choice via parameter. |
| src/storm-dft/environment/TransformationEnvironment.h | New transformation environment (bisimulation/chain elimination/labels). |
| src/storm-dft/environment/TransformationEnvironment.cpp | Implementation of transformation environment defaults + setters/getters. |
| src/storm-dft/environment/ModelBuilderEnvironment.h | New model builder environment (SR/DC/claiming/maxdepth/etc.). |
| src/storm-dft/environment/ModelBuilderEnvironment.cpp | Implementation of model builder environment defaults + validation. |
| src/storm-dft/environment/DftEnvironments.cpp | Explicit instantiations for DFT sub-environments. |
| src/storm-dft/environment/DftEnvironment.h | New combined DFT environment embedding Storm core environment. |
| src/storm-dft/environment/DftEnvironment.cpp | Implementation of DFT environment accessors/copy/assignment. |
| src/storm-dft/environment/AnalysisEnvironment.h | New analysis environment (modularisation/SMT/chunksize/approximation/etc.). |
| src/storm-dft/environment/AnalysisEnvironment.cpp | Implementation of analysis environment defaults + setters/getters. |
| src/storm-dft/environment/AllDftEnvironments.h | Aggregate include for DFT environments. |
| src/storm-dft/builder/ExplicitDFTModelBuilder.h | Pass/store DftEnvironment for model building configuration. |
| src/storm-dft/builder/ExplicitDFTModelBuilder.cpp | Use environment for max-depth/claiming/dependency selection instead of settings. |
| src/storm-dft/builder/DFTBuilder.h | Reduce includes via forward declarations. |
| src/storm-dft/api/transformation.h | New transformation API header (declarations). |
| src/storm-dft/api/transformation.cpp | Transformation API implementation + explicit instantiations. |
| src/storm-dft/api/storm-dft.h | Convert umbrella header to include the split API headers. |
| src/storm-dft/api/io.h | New IO API header (declarations). |
| src/storm-dft/api/io.cpp | IO API implementation + explicit instantiations. |
| src/storm-dft/api/gspn_transformation.h | New GSPN transformation API header (declarations). |
| src/storm-dft/api/gspn_transformation.cpp | GSPN transformation implementation + JANI property return. |
| src/storm-dft/api/analysis.h | New analysis API header (declarations + templates). |
| src/storm-dft/api/analysis.cpp | Analysis API implementation; environment-based analysis entry point. |
| src/storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h | Update relevant-events extraction API (claiming disabled for BDD). |
| src/storm-dft-cli/storm-dft.cpp | Build DftEnvironment from CLI settings; move exports to callback; use split APIs. |
| src/storm-dft-cli/settings/modules/FaultTreeSettings.h | New CLI-only DFT analysis settings module definition. |
| src/storm-dft-cli/settings/modules/FaultTreeSettings.cpp | CLI-only DFT analysis settings module implementation. |
| src/storm-dft-cli/settings/modules/DftIOSettings.h | New CLI-only DFT IO settings module definition. |
| src/storm-dft-cli/settings/modules/DftIOSettings.cpp | CLI-only DFT IO settings module implementation. |
| src/storm-dft-cli/settings/modules/DftGspnSettings.h | New CLI-only DFT→GSPN settings module definition. |
| src/storm-dft-cli/settings/modules/DftGspnSettings.cpp | CLI-only DFT→GSPN settings module implementation. |
| src/storm-dft-cli/CMakeLists.txt | Build settings-module sources into storm-dft-cli. |
Review details
- Files reviewed: 68/74 changed files
- Comments generated: 0
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
There was a problem hiding this comment.
🟡 Changes recommended
The review found unresolved API exposure, export-callback, and CLI validation defects.
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Review details
- Files reviewed: 68/74 changed files
- Comments generated: 2
- Review effort level: Balanced
Comment on lines
+3
to
+5
| #include "storm-dft/api/analysis.h" | ||
| #include "storm-dft/api/io.h" | ||
| #include "storm-dft/api/transformation.h" |
Comment on lines
+48
to
+50
| std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(env, dft, properties, relevantEvents); | ||
| // Model checking | ||
| std::vector<ValueType> resultsValue = checkModel(model, properties); | ||
| std::vector<ValueType> resultsValue = checkModel(env, model, properties); |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Builds on #1036 and #1034 which should be merged first.
Use DFT environment in storm-dft now instead of settings. The settings are completely moved into storm-dft-cli now, making it truly independent of the settings.
We still need to initialize the settings in the
storm-dftlibrary, because the Storm core might still need them. This could be moved in the future as well.Note that due to adding the DFT settings modules later,
storm-dft --helpnow shows all DFT related settings last.STORM_LOG_STATISTICS_LAZYfor statistics.