Integrate complete array support (#17)

Signed-off-by: Marco Lampacrescia <[email protected]>

.github/workflows/build_executable.yml

@@ -56,7 +56,7 @@ jobs:
                     mkdir external_dependencies/storm/build
                     cd external_dependencies/storm/build
                     cmake -DSTORM_USE_SPOT_SHIPPED=ON ..
-                    make
+                    make storm-cli
             - name: Build smc_storm
               run: |
                     export STORM_BUILD_DIR=$PWD/external_dependencies/storm/build

src/parser/parsers.cpp

@@ -17,13 +17,12 @@
 
 #include <storm-parsers/api/storm-parsers.h>
 #include <storm-parsers/parser/FormulaParser.h>
-#include <storm-parsers/parser/JaniParser.h>
-#include <storm-parsers/parser/PrismParser.h>
 #include <storm/api/builder.h>
 #include <storm/api/properties.h>
 #include <storm/exceptions/InvalidModelException.h>
 #include <storm/exceptions/InvalidPropertyException.h>
 #include <storm/exceptions/NotSupportedException.h>
+#include <storm/storage/expressions/ExpressionManager.h>
 #include <storm/utility/macros.h>
 
 #include "parser/parsers.hpp"
@@ -46,7 +45,11 @@ SymbolicModelAndProperty parseModelAndProperties(const smc_storm::settings::User
 
 SymbolicModelAndProperty parseJaniModelAndProperties(const smc_storm::settings::UserSettings& settings) {
     // Load the required model and property
-    const auto model_and_formulae = storm::parser::JaniParser<storm::RationalNumber>::parse(settings.model_file, true);
+    storm::jani::ModelFeatures supported_features = storm::api::getSupportedJaniFeatures(storm::builder::BuilderType::Explicit);
+    // Removing the array feature ensures the array entries are substituted with the expanded name.
+    // e.g. array[0] -> array_at_0
+    supported_features.remove(storm::jani::ModelFeature::Arrays);
+    auto model_and_formulae = storm::api::parseJaniModel(settings.model_file, supported_features);
     model_and_formulae.first.checkValid();
     const auto model_constants_map = model_and_formulae.first.getConstantsSubstitution();
     std::vector<storm::jani::Property> loaded_properties;
@@ -59,15 +62,11 @@ SymbolicModelAndProperty parseJaniModelAndProperties(const smc_storm::settings::
         loaded_properties = filterProperties(model_and_formulae.second, properties_ids, model_constants_map);
     }
     // Add the user-defined constants
-    auto model_and_property = substituteConstants({model_and_formulae.first, loaded_properties}, settings.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);
-    return model_and_property;
+    return substituteConstants({model_and_formulae.first, loaded_properties}, settings.constants);
 }
 
 SymbolicModelAndProperty parsePrismModelAndProperties(const smc_storm::settings::UserSettings& settings) {
-    const auto prism_model = storm::parser::PrismParser::parse(settings.model_file);
+    const auto prism_model = storm::api::parseProgram(settings.model_file);
     prism_model.checkValidity();
     const auto model_constants_map = prism_model.getConstantsSubstitution();
     const storm::parser::FormulaParser formula_parser(prism_model);

test/system_tests/models/array_test.jani

@@ -0,0 +1,145 @@
+{
+  "jani-version": 1,
+  "name": "",
+  "type": "mdp",
+  "features": [
+    "arrays"
+  ],
+  "variables": [
+    {
+      "name": "normal_array",
+      "type": {
+        "kind": "array",
+        "base": "int"
+      },
+      "transient": false,
+      "initial-value": {
+        "op": "ac",
+        "var": "__array_iterator",
+        "length": 15,
+        "exp": 0
+      }
+    },
+    {
+      "name": "next_id",
+      "type": "int",
+      "transient": false,
+      "initial-value": 0
+    }
+  ],
+  "constants": [],
+  "actions": [
+    {
+      "name": "step"
+    }
+  ],
+  "automata": [
+    {
+      "name": "array_writer",
+      "locations": [
+        {
+          "name": "step"
+        }
+      ],
+      "initial-locations": [
+        "step"
+      ],
+      "edges": [
+        {
+          "location": "step",
+          "destinations": [
+            {
+              "location": "step",
+              "assignments": [
+                {
+                  "ref": {
+                    "op": "aa",
+                    "exp": "normal_array",
+                    "index": "next_id"
+                  },
+                  "value": "next_id",
+                  "index": 0
+                },
+                {
+                  "ref": "next_id",
+                  "value": {
+                    "op": "+",
+                    "left": "next_id",
+                    "right": 1
+                  },
+                  "index": 1
+                }
+              ]
+            }
+          ],
+          "action": "step"
+        }
+      ],
+      "variables": []
+    }
+  ],
+  "system": {
+    "elements": [
+      {
+        "automaton": "array_writer"
+      }
+    ],
+    "syncs": [
+      {
+        "result": "step",
+        "synchronise": [
+          "step"
+        ]
+      }
+    ]
+  },
+  "properties": [
+    {
+      "name": "property_no_array_access",
+      "expression": {
+        "op": "filter",
+        "fun": "values",
+        "values": {
+          "op": "Pmin",
+          "exp": {
+            "op": "F",
+            "exp": {
+              "op": "=",
+              "left": "next_id",
+              "right": 10
+            }
+          }
+        },
+        "states": {
+          "op": "initial"
+        }
+      }
+    },
+    {
+      "name": "property_with_array_access",
+      "comment": "Not working due to array access not supported in properties",
+      "expression": {
+        "op": "filter",
+        "fun": "values",
+        "values": {
+          "op": "Pmin",
+          "exp": {
+            "op": "F",
+            "exp": {
+              "op": "=",
+              "left": {
+                "op": "aa",
+                "exp": "normal_array",
+                "index": 10
+              },
+              "right": 10
+            }
+          }
+        },
+        "states": {
+          "op": "initial"
+        }
+      }
+    }
+  ]
+}

test/system_tests/test_jani_models.cpp

@@ -86,6 +86,20 @@ TEST(StatisticalModelCheckerJaniTest, TestTrigonometry) {
     }
 }
 
+TEST(StatisticalModelCheckerJaniTest, TestArray) {
+    const std::filesystem::path jani_file = TEST_PATH / "array_test.jani";
+    {
+        const auto user_settings = getSettings(jani_file, "property_no_array_access");
+        const double result = getVerificationResult<double>(user_settings);
+        EXPECT_NEAR(result, 1.0, user_settings.epsilon);
+    }
+    {
+        const auto user_settings = getSettings(jani_file, "property_with_array_access");
+        const double result = getVerificationResult<double>(user_settings);
+        EXPECT_NEAR(result, 1.0, user_settings.epsilon);
+    }
+}
+
 int main(int argc, char** argv) {
     ::testing::InitGoogleTest(&argc, argv);
     return RUN_ALL_TESTS();