IoT/Edge Case Study

.run/digest (iot.json).run.xml

@@ -15,7 +15,7 @@
     <option name="ADD_SOURCE_ROOTS" value="true" />
     <EXTENSION ID="PythonCoverageRunConfigurationExtension" runner="coverage.py" />
     <option name="SCRIPT_NAME" value="$PROJECT_DIR$/tlparser" />
-    <option name="PARAMETERS" value="digest ./data/iot.json" />
+    <option name="PARAMETERS" value="digest ./data/Edge_IoT/iot.json" />
     <option name="SHOW_COMMAND_LINE" value="false" />
     <option name="EMULATE_TERMINAL" value="false" />
     <option name="MODULE_MODE" value="false" />

README.md

@@ -128,9 +128,20 @@ All plots are saved to `./tlparser/workingdir/`.
 You can parse the `spacewire` requirements using the following command:
 
 ```bash
-tlparser digest ./data/spacewire.json
+tlparser digest ./data/SpaceWire/spacewire.json
 ```
 
+You can parse the `Edge_IoT` requirements using the following command:
+
+```bash
+tlparser digest ./data/Edge_IoT/iot.json
+```
+
+> [!NOTE]  
+> So far, two data sets are available:
+> - Direct link to Spacewire dataset: [**JSON**](tbd) or [**PDF**](tbd)
+> - Direct link to Edge/IoT dataset: [**JSON**](tbd) or [**XLSX**](tbd)
+
 The resulting Excel file serves as basis for generating the plots.
 It contains the following columns:
 
@@ -198,116 +209,3 @@ source venv/bin/activate
 # or on Windows:
 # venv\Scripts\activate
 ```
-
-## Extended Statistics
-
-For automaton-level insight, enable the optional Spot[^spot-citation] integration which will allow you to harvest extended statistics.
-Spot is not bundled with `tlparser`, so install the CLI tools (`ltl2tgba`, `ltlfilt`, `autfilt`) beforehand.
-You can find installation instructions on [Spot's webpage](https://spot.lre.epita.fr/).
-Homebrew users can also install it using the `brew install spot` command.
-
-With Spot on your `PATH`, add `--extended` to the `digest` or `evaluate` command:
-
-```bash
-tlparser digest ./data/spacewire.json --extended
-```
-
-Extended digests may also produce a companion `<filename>_errors.md` summarising formulas Spot could not analyse.
-You can experiment interactively as well:
-
-```bash
-tlparser evaluate "G (req --> F ack)" --extended
-```
-
-Sample output:
-
-```json
-{
-  "agg": {
-    "aps": 2,
-    "cops": 0,
-    "lops": 1,
-    "tops": 2
-  },
-  "ap": [
-    "ack",
-    "req"
-  ],
-  "asth": 3,
-  "cops": {
-    "eq": 0,
-    "geq": 0,
-    "gt": 0,
-    "leq": 0,
-    "lt": 0,
-    "neq": 0
-  },
-  "entropy": {
-    "lops": 1.0,
-    "lops_tops": 1.584962500721156,
-    "tops": 0.0
-  },
-  "formula_parsable": "G (req --> F ack)",
-  "formula_parsed": "G((req --> F(ack)))",
-  "formula_raw": "G (req --> F ack)",
-  "lops": {
-    "and": 0,
-    "impl": 1,
-    "not": 0,
-    "or": 0
-  },
-  "req_len": null,
-  "req_sentence_count": null,
-  "req_word_count": null,
-  "tops": {
-    "A": 0,
-    "E": 0,
-    "F": 1,
-    "G": 1,
-    "R": 0,
-    "U": 0,
-    "X": 0
-  },
-  "z_extended": {
-    "buchi_analysis": {
-      "acceptance_sets": 1,
-      "analysis_source": "ltl2tgba_stats",
-      "is_complete": true,
-      "is_deterministic": true,
-      "is_stutter_invariant": true,
-      "state_count": 2,
-      "transition_count": 8
-    },
-    "deterministic_attempt": {
-      "automaton_analysis": {
-        "acceptance_sets": 1,
-        "analysis_source": "ltl2tgba_stats",
-        "is_complete": true,
-        "is_deterministic": true,
-        "is_stutter_invariant": true,
-        "state_count": 2,
-        "transition_count": 8
-      },
-      "success": true
-    },
-    "formula": "G (req --> F ack)",
-    "is_stutter_invariant_formula": true,
-    "manna_pnueli_class": "recurrence reactivity",
-    "spot_formula": "G (req -> F ack)",
-    "syntactic_safety": false,
-    "tgba_analysis": {
-      "acceptance_sets": 1,
-      "analysis_source": "ltl2tgba_stats",
-      "is_complete": true,
-      "is_deterministic": true,
-      "is_stutter_invariant": true,
-      "state_count": 2,
-      "transition_count": 8
-    }
-  }
-}
-```
-
-</br>
-
-[^spot-citation]: Alexandre Duret-Lutz et al., “[From Spot 2.0 to Spot 2.10: What’s new?](https://doi.org/10.1007/978-3-031-13188-2_9)”, Proc. CAV 2022, LNCS 13372, pp. 174–187, Haifa, Israel, Aug. 2022.

tests/logic/test_case_data.py

@@ -1,6 +1,9 @@
 class TestCaseData:
     __test__ = False
-    def __init__(self, f_code='', asth='', aps=0, cops=0, lops=0, tops=0, entropy_lops_tops=None):
+
+    def __init__(
+        self, f_code="", asth="", aps=0, cops=0, lops=0, tops=0, entropy_lops_tops=None
+    ):
         self.f_code = f_code
         self.asth = asth
         self.aps = aps
@@ -15,8 +18,8 @@ class TestCaseDataExt(TestCaseData):
 
     def __init__(
         self,
-        f_code: str = '',
-        asth: int | str = '',
+        f_code: str = "",
+        asth: int | str = "",
         aps: int = 0,
         cops: int = 0,
         lops: int = 0,
@@ -28,12 +31,16 @@ def __init__(
         manna_pnueli_class=None,
         tgba_state_count=None,
         tgba_transition_count=None,
+        tgba_edge_count=None,
         tgba_is_complete=None,
         tgba_is_deterministic=None,
         tgba_acceptance_sets=None,
         tgba_is_stutter_invariant=None,
+        tgba_syntactic_future_hierarchy=None,
+        tgba_safety_liveness_class=None,
         buchi_state_count=None,
         buchi_transition_count=None,
+        buchi_edge_count=None,
         buchi_is_complete=None,
         buchi_is_deterministic=None,
         buchi_acceptance_sets=None,
@@ -43,6 +50,7 @@ def __init__(
         manna_pnueli_class_contains=None,
         det_state_count=None,
         det_transition_count=None,
+        det_edge_count=None,
         det_is_complete=None,
         det_is_deterministic=None,
         det_acceptance_sets=None,
@@ -62,12 +70,16 @@ def __init__(
         self.manna_pnueli_class = manna_pnueli_class
         self.tgba_state_count = tgba_state_count
         self.tgba_transition_count = tgba_transition_count
+        self.tgba_edge_count = tgba_edge_count
         self.tgba_is_complete = tgba_is_complete
         self.tgba_is_deterministic = tgba_is_deterministic
         self.tgba_acceptance_sets = tgba_acceptance_sets
         self.tgba_is_stutter_invariant = tgba_is_stutter_invariant
+        self.tgba_syntactic_future_hierarchy = tgba_syntactic_future_hierarchy
+        self.tgba_safety_liveness_class = tgba_safety_liveness_class
         self.buchi_state_count = buchi_state_count
         self.buchi_transition_count = buchi_transition_count
+        self.buchi_edge_count = buchi_edge_count
         self.buchi_is_complete = buchi_is_complete
         self.buchi_is_deterministic = buchi_is_deterministic
         self.buchi_acceptance_sets = buchi_acceptance_sets
@@ -77,6 +89,7 @@ def __init__(
         self.manna_pnueli_class_contains = manna_pnueli_class_contains
         self.det_state_count = det_state_count
         self.det_transition_count = det_transition_count
+        self.det_edge_count = det_edge_count
         self.det_is_complete = det_is_complete
         self.det_is_deterministic = det_is_deterministic
         self.det_acceptance_sets = det_acceptance_sets