Update storm version (#10)

Signed-off-by: Marco Lampacrescia <[email protected]>
convince-project · Jun 18, 2024 · 06d8b4b · 06d8b4b
1 parent addad6f
commit 06d8b4b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/.github/workflows/build_executable.yml b/.github/workflows/build_executable.yml
@@ -26,7 +26,7 @@ jobs:
               with:
                 repository: boschresearch/storm
                 # Temporary fixed commit. Remove once we switch to the official storm repo
-                ref: 77ad64ed21225b3f5d91bb606796ec64eab8c279
+                ref: af3337abf9f01100c009d5e38ee5867ceafd84b9
                 path: external_dependencies/storm
             # Enable ccache
             - name: ccache

diff --git a/src/parser/parsers.cpp b/src/parser/parsers.cpp
@@ -16,6 +16,7 @@
  */
 
 #include <storm/api/builder.h>
+#include <storm/api/properties.h>
 #include <storm-parsers/api/storm-parsers.h>
 #include <storm-parsers/parser/PrismParser.h>
 #include <storm-parsers/parser/JaniParser.h>
@@ -58,9 +59,13 @@ SymbolicModelAndProperty parseJaniModelAndProperty(const std::filesystem::path&
     // Add the user-defined constants
     const auto user_constants_map = model_and_property.model.parseConstantDefinitions(user_constants);
     model_and_property.model = model_and_property.model.preprocess(user_constants_map);
-    model_and_property.property.front() = model_and_property.property.front().substitute(user_constants_map);
-    STORM_LOG_THROW(model_and_property.property.front().getUndefinedConstants().empty(), storm::exceptions::InvalidPropertyException, 
-        "The property uses undefined constants!!!");
+    model_and_property.property = storm::api::substituteConstantsInProperties(model_and_property.property, user_constants_map);
+    model_and_property.property = storm::api::substituteTranscendentalNumbersInProperties(model_and_property.property);
+    // Make sure that all properties have no undefined constant
+    for (const auto& property : model_and_property.property) {
+        STORM_LOG_THROW(property.getUndefinedConstants().empty(), storm::exceptions::InvalidPropertyException, 
+            "The property uses undefined constants!!!");
+    }
     // Expand the model
     storm::jani::ModelFeatures supported_features = storm::api::getSupportedJaniFeatures(storm::builder::BuilderType::Explicit);
     storm::api::simplifyJaniModel(model_and_property.model.asJaniModel(), model_and_property.property, supported_features);