Fixes and improvements for DFT symmetries and DFT simulation(#463)

moves-rwth · Dec 11, 2023 · 373f9bf · 373f9bf
2 parents 51a0781 + e4d1a1e
commit 373f9bf
Show file tree

Hide file tree

Showing 48 changed files with 1,250 additions and 892 deletions.
diff --git a/resources/examples/testfiles/dft/mutex4.dft b/resources/examples/testfiles/dft/mutex4.dft
@@ -0,0 +1,9 @@
+toplevel "T";
+"T" or "P" "A";
+"P" por "B" "O";
+"O" or "C" "D";
+"M" mutex "A" "C";
+"A" lambda=1.0 dorm=1.0;
+"B" lambda=1.0 dorm=1.0;
+"C" lambda=1.0 dorm=1.0;
+"D" lambda=1.0 dorm=1.0;
diff --git a/resources/examples/testfiles/dft/pand.dft b/resources/examples/testfiles/dft/pand.dft
@@ -1,4 +1,4 @@
 toplevel "A";
 "A" pand "B" "C";
 "B" lambda=0.4 dorm=0.3;
-"C" lambda=0.2 dorm=0.3;
+"C" lambda=0.4 dorm=0.3;
diff --git a/resources/examples/testfiles/dft/voting5.dft b/resources/examples/testfiles/dft/voting5.dft
@@ -0,0 +1,10 @@
+toplevel "A";
+"A" or "B" "C";
+"B" 2of3 "D" "E" "F";
+"C" 1of3 "G" "H" "I";
+"D" lambda=1 dorm=0.0;
+"E" lambda=2 dorm=0.0;
+"F" lambda=3 dorm=0.0;
+"G" lambda=1 dorm=0.0;
+"H" lambda=2 dorm=0.0;
+"I" lambda=3 dorm=0.0;
diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
@@ -214,7 +214,7 @@ void processOptions() {
         // All events are relevant
         additionalRelevantEventNames = {"all"};
     }
-    storm::dft::utility::RelevantEvents relevantEvents = storm::dft::api::computeRelevantEvents<ValueType>(*dft, props, additionalRelevantEventNames);
+    storm::dft::utility::RelevantEvents relevantEvents = storm::dft::api::computeRelevantEvents(props, additionalRelevantEventNames);
 
     // Analyze DFT
     dft = storm::dft::api::prepareForMarkovAnalysis<ValueType>(*dft);

diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp
@@ -234,6 +234,11 @@ std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::d
     return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId());
 }
 
+template<>
+std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::dft::storage::DFT<storm::RationalFunction> const& dft) {
+    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type.");
+}
+
 std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) {
     // Build Jani model
     storm::builder::JaniGSPNBuilder builder(gspn);
@@ -258,9 +263,11 @@ std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gsp
     return model;
 }
 
-template<>
-std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::dft::storage::DFT<storm::RationalFunction> const& dft) {
-    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type.");
+storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
+                                                          std::vector<std::string> const& additionalRelevantEventNames) {
+    storm::dft::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end());
+    events.insertNamesFromProperties(properties.begin(), properties.end());
+    return events;
 }
 
 // Explicitly instantiate methods

diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
@@ -144,19 +144,12 @@ bool computeDependencyConflicts(storm::dft::storage::DFT<ValueType>& dft, bool u
 /*!
  * Get relevant event ids from given relevant event names and labels in properties.
  *
- * @param dft DFT.
  * @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.
  */
-template<typename ValueType>
-storm::dft::utility::RelevantEvents computeRelevantEvents(storm::dft::storage::DFT<ValueType> const& dft,
-                                                          std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
-                                                          std::vector<std::string> const& additionalRelevantEventNames) {
-    storm::dft::utility::RelevantEvents events(additionalRelevantEventNames.begin(), additionalRelevantEventNames.end());
-    events.insertNamesFromProperties(properties.begin(), properties.end());
-    return events;
-}
+storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties,
+                                                          std::vector<std::string> const& additionalRelevantEventNames);
 
 /*!
  * Compute the exact or approximate analysis result of the given DFT according to the given properties.

diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp
@@ -394,7 +394,8 @@ void DFTBuilder<ValueType>::topologicalVisit(DFTElementPointer const& element,
                 topologicalVisit(child, visited, visitedElements);
             }
         } else if (element->isDependency()) {
-            for (DFTBEPointer const& child : std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType>>(element)->dependentEvents()) {
+            for (DFTElementPointer const& child :
+                 std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType>>(element)->dependentEvents()) {
                 // Recursively visit all dependent children
                 topologicalVisit(child, visited, visitedElements);
             }

diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h
@@ -28,7 +28,7 @@ class DFTExplorationHeuristic {
 
     virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0;
 
-    virtual void setBounds(ValueType lowerBound, ValueType upperBound) {
+    virtual void setBounds(ValueType /*lowerBound*/, ValueType /*upperBound*/) {
         STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Should be handled by specialized heuristic.");
     }
 

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -35,7 +35,7 @@ ExplicitDFTModelBuilder<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool
 
 template<typename ValueType, typename StateType>
 ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::dft::storage::DFT<ValueType> const& dft,
-                                                                       storm::dft::storage::DFTIndependentSymmetries const& symmetries)
+                                                                       storm::dft::storage::DftSymmetries const& symmetries)
     : dft(dft),
       stateGenerationInfo(std::make_shared<storm::dft::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
       generator(dft, *stateGenerationInfo),

diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -16,7 +16,7 @@
 #include "storm-dft/generator/DftNextStateGenerator.h"
 #include "storm-dft/storage/BucketPriorityQueue.h"
 #include "storm-dft/storage/DFT.h"
-#include "storm-dft/storage/SymmetricUnits.h"
+#include "storm-dft/storage/DftSymmetries.h"
 
 namespace storm::dft {
 namespace builder {
@@ -153,7 +153,7 @@ class ExplicitDFTModelBuilder {
      * @param dft DFT.
      * @param symmetries Symmetries in the dft.
      */
-    ExplicitDFTModelBuilder(storm::dft::storage::DFT<ValueType> const& dft, storm::dft::storage::DFTIndependentSymmetries const& symmetries);
+    ExplicitDFTModelBuilder(storm::dft::storage::DFT<ValueType> const& dft, storm::dft::storage::DftSymmetries const& symmetries);
 
     /*!
      * Build model from DFT.