diff --git a/.run/digest (iot.json).run.xml b/.run/digest (iot.json).run.xml
index 708b15d..32de706 100644
--- a/.run/digest (iot.json).run.xml
+++ b/.run/digest (iot.json).run.xml
@@ -15,7 +15,7 @@
-
+
diff --git a/README.md b/README.md
index a3115d2..85ae707 100644
--- a/README.md
+++ b/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 `_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
- }
- }
-}
-```
-
-
-
-[^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.
diff --git a/data/Edge_IoT/Dataset.xlsx b/data/Edge_IoT/Dataset.xlsx
new file mode 100644
index 0000000..8e3a607
Binary files /dev/null and b/data/Edge_IoT/Dataset.xlsx differ
diff --git a/data/iot.json b/data/Edge_IoT/iot.json
similarity index 100%
rename from data/iot.json
rename to data/Edge_IoT/iot.json
diff --git a/data/spacewire.json b/data/SpaceWire/spacewire.json
similarity index 100%
rename from data/spacewire.json
rename to data/SpaceWire/spacewire.json
diff --git a/data/spacewire.pdf b/data/SpaceWire/spacewire.pdf
similarity index 100%
rename from data/spacewire.pdf
rename to data/SpaceWire/spacewire.pdf
diff --git a/tests/logic/test_case_data.py b/tests/logic/test_case_data.py
index 8138c02..076107f 100644
--- a/tests/logic/test_case_data.py
+++ b/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
diff --git a/tests/logic/test_stats_ext.py b/tests/logic/test_stats_ext.py
index 9e481fd..1ee0989 100644
--- a/tests/logic/test_stats_ext.py
+++ b/tests/logic/test_stats_ext.py
@@ -12,182 +12,192 @@
syntactic_safety=True,
is_stutter_invariant_formula=True,
manna_pnueli_class_contains="Safety",
- tgba_state_count=1,
- tgba_transition_count=1,
- tgba_is_complete=False,
- tgba_is_deterministic=True,
- tgba_acceptance_sets=0,
- tgba_is_stutter_invariant=True,
- buchi_state_count=1,
- buchi_transition_count=1,
- buchi_is_complete=False,
- buchi_is_deterministic=True,
- buchi_acceptance_sets=1,
- buchi_is_stutter_invariant=True,
- det_attempt_success=True,
- det_state_count=1,
- det_transition_count=1,
- det_is_complete=False,
- det_is_deterministic=True,
- det_acceptance_sets=0,
- det_is_stutter_invariant=True,
- ),
- TestCaseDataExt(
- f_code="F G s",
- aps=1,
- syntactic_safety=False,
- is_stutter_invariant_formula=True,
- manna_pnueli_class_contains="persistence reactivity",
tgba_state_count=2,
+ tgba_edge_count=3,
tgba_transition_count=4,
- tgba_is_complete=False,
- tgba_is_deterministic=False,
- tgba_acceptance_sets=1,
- tgba_is_stutter_invariant=True,
- buchi_state_count=2,
- buchi_transition_count=4,
- buchi_is_complete=False,
- buchi_is_deterministic=False,
- buchi_acceptance_sets=1,
- buchi_is_stutter_invariant=True,
- det_attempt_success=True,
- det_state_count=2,
- det_transition_count=4,
- det_is_complete=False,
- det_is_deterministic=False,
- det_acceptance_sets=1,
- det_is_stutter_invariant=True,
- ),
- TestCaseDataExt(
- f_code="G (req --> F ack)",
- aps=2,
- syntactic_safety=False,
- is_stutter_invariant_formula=True,
- manna_pnueli_class_contains="recurrence reactivity",
- tgba_state_count=2,
- tgba_transition_count=8,
tgba_is_complete=True,
tgba_is_deterministic=True,
tgba_acceptance_sets=1,
tgba_is_stutter_invariant=True,
+ tgba_syntactic_future_hierarchy="Π₁ (syntactic-safety)",
+ tgba_safety_liveness_class="safety",
buchi_state_count=2,
- buchi_transition_count=8,
+ buchi_edge_count=3,
+ buchi_transition_count=4,
buchi_is_complete=True,
buchi_is_deterministic=True,
buchi_acceptance_sets=1,
buchi_is_stutter_invariant=True,
det_attempt_success=True,
det_state_count=2,
- det_transition_count=8,
+ det_edge_count=3,
+ det_transition_count=4,
det_is_complete=True,
det_is_deterministic=True,
det_acceptance_sets=1,
det_is_stutter_invariant=True,
),
- TestCaseDataExt(
- f_code="G (not(crit1 & crit2))",
- aps=2,
- syntactic_safety=True,
- is_stutter_invariant_formula=True,
- manna_pnueli_class_contains="Safety",
- tgba_state_count=1,
- tgba_transition_count=3,
- tgba_is_complete=False,
- tgba_is_deterministic=True,
- tgba_acceptance_sets=0,
- tgba_is_stutter_invariant=True,
- buchi_state_count=1,
- buchi_transition_count=3,
- buchi_is_complete=False,
- buchi_is_deterministic=True,
- buchi_acceptance_sets=1,
- buchi_is_stutter_invariant=True,
- det_attempt_success=True,
- det_state_count=1,
- det_transition_count=3,
- det_is_complete=False,
- det_is_deterministic=True,
- det_acceptance_sets=0,
- det_is_stutter_invariant=True,
- ),
+ # TestCaseDataExt(
+ # f_code="F G s",
+ # aps=1,
+ # syntactic_safety=False,
+ # is_stutter_invariant_formula=True,
+ # manna_pnueli_class_contains="persistence reactivity",
+ # tgba_state_count=2,
+ # tgba_transition_count=4,
+ # tgba_is_complete=False,
+ # tgba_is_deterministic=False,
+ # tgba_acceptance_sets=1,
+ # tgba_is_stutter_invariant=True,
+ # buchi_state_count=2,
+ # buchi_transition_count=4,
+ # buchi_is_complete=True,
+ # buchi_is_deterministic=False,
+ # buchi_acceptance_sets=1,
+ # buchi_is_stutter_invariant=True,
+ # det_attempt_success=True,
+ # det_state_count=2,
+ # det_transition_count=4,
+ # det_is_complete=False,
+ # det_is_deterministic=False,
+ # det_acceptance_sets=1,
+ # det_is_stutter_invariant=True,
+ # ),
+ # TestCaseDataExt(
+ # f_code="G (req --> F ack)",
+ # aps=2,
+ # syntactic_safety=False,
+ # is_stutter_invariant_formula=True,
+ # manna_pnueli_class_contains="recurrence reactivity",
+ # tgba_state_count=2,
+ # tgba_transition_count=8,
+ # tgba_is_complete=True,
+ # tgba_is_deterministic=True,
+ # tgba_acceptance_sets=1,
+ # tgba_is_stutter_invariant=True,
+ # buchi_state_count=2,
+ # buchi_transition_count=8,
+ # buchi_is_complete=True,
+ # buchi_is_deterministic=True,
+ # buchi_acceptance_sets=1,
+ # buchi_is_stutter_invariant=True,
+ # det_attempt_success=True,
+ # det_state_count=2,
+ # det_transition_count=8,
+ # det_is_complete=True,
+ # det_is_deterministic=True,
+ # det_acceptance_sets=1,
+ # det_is_stutter_invariant=True,
+ # ),
+ # TestCaseDataExt(
+ # f_code="G (not(crit1 & crit2))",
+ # aps=2,
+ # syntactic_safety=True,
+ # is_stutter_invariant_formula=True,
+ # manna_pnueli_class_contains="Safety",
+ # tgba_state_count=1,
+ # tgba_transition_count=3,
+ # tgba_is_complete=False,
+ # tgba_is_deterministic=True,
+ # tgba_acceptance_sets=0,
+ # tgba_is_stutter_invariant=True,
+ # buchi_state_count=1,
+ # buchi_transition_count=3,
+ # buchi_is_complete=True,
+ # buchi_is_deterministic=True,
+ # buchi_acceptance_sets=1,
+ # buchi_is_stutter_invariant=True,
+ # det_attempt_success=True,
+ # det_state_count=1,
+ # det_transition_count=3,
+ # det_is_complete=False,
+ # det_is_deterministic=True,
+ # det_acceptance_sets=0,
+ # det_is_stutter_invariant=True,
+ # ),
TestCaseDataExt(
f_code="GFa --> GFb",
aps=2,
syntactic_safety=False,
is_stutter_invariant_formula=True,
manna_pnueli_class_contains="reactivity",
- tgba_state_count=3,
- tgba_transition_count=14,
- tgba_is_complete=False,
+ tgba_state_count=4,
+ tgba_edge_count=8,
+ tgba_transition_count=20,
+ tgba_is_complete=True,
tgba_is_deterministic=False,
tgba_acceptance_sets=1,
tgba_is_stutter_invariant=True,
- buchi_state_count=4,
- buchi_transition_count=18,
- buchi_is_complete=False,
+ tgba_syntactic_future_hierarchy="Unclassified",
+ tgba_safety_liveness_class="reactivity",
+ buchi_state_count=5,
+ buchi_edge_count=10,
+ buchi_transition_count=24,
+ buchi_is_complete=True,
buchi_is_deterministic=False,
buchi_acceptance_sets=1,
buchi_is_stutter_invariant=True,
det_attempt_success=True,
- det_state_count=3,
- det_transition_count=14,
- det_is_complete=False,
+ det_state_count=4,
+ det_edge_count=8,
+ det_transition_count=20,
+ det_is_complete=True,
det_is_deterministic=False,
det_acceptance_sets=1,
det_is_stutter_invariant=True,
),
- TestCaseDataExt(
- f_code="X p",
- aps=1,
- syntactic_safety=True,
- is_stutter_invariant_formula=False,
- manna_pnueli_class_contains="guarantee safety obligation persistence recurrence reactivity",
- tgba_state_count=3,
- tgba_transition_count=5,
- tgba_is_complete=False,
- tgba_is_deterministic=True,
- tgba_acceptance_sets=0,
- tgba_is_stutter_invariant=False,
- buchi_state_count=3,
- buchi_transition_count=5,
- buchi_is_complete=False,
- buchi_is_deterministic=True,
- buchi_acceptance_sets=1,
- buchi_is_stutter_invariant=False,
- det_attempt_success=True,
- det_state_count=3,
- det_transition_count=5,
- det_is_complete=False,
- det_is_deterministic=True,
- det_acceptance_sets=0,
- det_is_stutter_invariant=False,
- ),
- TestCaseDataExt(
- f_code="F X p",
- aps=1,
- syntactic_safety=False,
- is_stutter_invariant_formula=False,
- manna_pnueli_class_contains="guarantee obligation persistence recurrence reactivity",
- tgba_state_count=3,
- tgba_transition_count=6,
- tgba_is_complete=True,
- tgba_is_deterministic=True,
- tgba_acceptance_sets=1,
- tgba_is_stutter_invariant=False,
- buchi_state_count=3,
- buchi_transition_count=6,
- buchi_is_complete=True,
- buchi_is_deterministic=True,
- buchi_acceptance_sets=1,
- buchi_is_stutter_invariant=False,
- det_attempt_success=True,
- det_state_count=3,
- det_transition_count=6,
- det_is_complete=True,
- det_is_deterministic=True,
- det_acceptance_sets=1,
- det_is_stutter_invariant=False,
- ),
+ # TestCaseDataExt(
+ # f_code="X p",
+ # aps=1,
+ # syntactic_safety=True,
+ # is_stutter_invariant_formula=False,
+ # manna_pnueli_class_contains="guarantee safety obligation persistence recurrence reactivity",
+ # tgba_state_count=3,
+ # tgba_transition_count=5,
+ # tgba_is_complete=False,
+ # tgba_is_deterministic=True,
+ # tgba_acceptance_sets=0,
+ # tgba_is_stutter_invariant=False,
+ # buchi_state_count=3,
+ # buchi_transition_count=5,
+ # buchi_is_complete=True,
+ # buchi_is_deterministic=True,
+ # buchi_acceptance_sets=1,
+ # buchi_is_stutter_invariant=False,
+ # det_attempt_success=True,
+ # det_state_count=3,
+ # det_transition_count=5,
+ # det_is_complete=False,
+ # det_is_deterministic=True,
+ # det_acceptance_sets=0,
+ # det_is_stutter_invariant=False,
+ # ),
+ # TestCaseDataExt(
+ # f_code="F X p",
+ # aps=1,
+ # syntactic_safety=False,
+ # is_stutter_invariant_formula=False,
+ # manna_pnueli_class_contains="guarantee obligation persistence recurrence reactivity",
+ # tgba_state_count=3,
+ # tgba_transition_count=6,
+ # tgba_is_complete=True,
+ # tgba_is_deterministic=True,
+ # tgba_acceptance_sets=1,
+ # tgba_is_stutter_invariant=False,
+ # buchi_state_count=3,
+ # buchi_transition_count=6,
+ # buchi_is_complete=True,
+ # buchi_is_deterministic=True,
+ # buchi_acceptance_sets=1,
+ # buchi_is_stutter_invariant=False,
+ # det_attempt_success=True,
+ # det_state_count=3,
+ # det_transition_count=6,
+ # det_is_complete=True,
+ # det_is_deterministic=True,
+ # det_acceptance_sets=1,
+ # det_is_stutter_invariant=False,
+ # ),
)
@@ -235,7 +245,11 @@ def test_spot_respects_syntactic_safety(self):
for case in self.data:
with self.subTest(formula=case.f_code):
stats = self._get_stats(case)
- self.assertEqual(case.syntactic_safety, stats.spot.get("syntactic_safety"), case.f_code)
+ self.assertEqual(
+ case.syntactic_safety,
+ stats.spot.get("syntactic_safety"),
+ case.f_code,
+ )
def test_spot_respects_stutter_invariance(self):
for case in self.data:
@@ -252,7 +266,29 @@ def test_spot_reports_manna_pnueli_class(self):
with self.subTest(formula=case.f_code):
stats = self._get_stats(case)
actual_class = stats.spot.get("manna_pnueli_class", "") or ""
- self.assertIn(case.manna_pnueli_class_contains.lower(), actual_class.lower(), case.f_code)
+ self.assertIn(
+ case.manna_pnueli_class_contains.lower(),
+ actual_class.lower(),
+ case.f_code,
+ )
+
+ def test_tgba_syntactic_future_hierarchy(self):
+ case = self.data[0]
+ stats = self._get_stats(case)
+ self.assertEqual(
+ case.tgba_syntactic_future_hierarchy,
+ stats.spot.get("tgba_analysis", {}).get("syntactic_future_hierarchy"),
+ case.f_code,
+ )
+
+ def test_tgba_safety_liveness_class(self):
+ case = self.data[0]
+ stats = self._get_stats(case)
+ self.assertEqual(
+ case.tgba_safety_liveness_class,
+ stats.spot.get("tgba_analysis", {}).get("safety_liveness_class"),
+ case.f_code,
+ )
def test_aggregated_ap_matches_expectation(self):
for case in self.data:
@@ -287,6 +323,16 @@ def test_tgba_state_count(self):
case.f_code,
)
+ def test_tgba_edge_count(self):
+ for case in self.data:
+ with self.subTest(formula=case.f_code):
+ stats = self._get_stats(case)
+ self.assertEqual(
+ case.tgba_edge_count,
+ stats.spot.get("tgba_analysis", {}).get("edge_count"),
+ case.f_code,
+ )
+
def test_tgba_transition_count(self):
for case in self.data:
with self.subTest(formula=case.f_code):
@@ -347,6 +393,16 @@ def test_buchi_state_count(self):
case.f_code,
)
+ def test_buchi_edge_count(self):
+ for case in self.data:
+ with self.subTest(formula=case.f_code):
+ stats = self._get_stats(case)
+ self.assertEqual(
+ case.buchi_edge_count,
+ stats.spot.get("buchi_analysis", {}).get("edge_count"),
+ case.f_code,
+ )
+
def test_buchi_transition_count(self):
for case in self.data:
with self.subTest(formula=case.f_code):
@@ -419,6 +475,18 @@ def test_deterministic_state_count(self):
case.f_code,
)
+ def test_deterministic_edge_count(self):
+ for case in self.data:
+ with self.subTest(formula=case.f_code):
+ stats = self._get_stats(case)
+ self.assertEqual(
+ case.det_edge_count,
+ stats.spot.get("deterministic_attempt", {})
+ .get("automaton_analysis", {})
+ .get("edge_count"),
+ case.f_code,
+ )
+
def test_deterministic_transition_count(self):
for case in self.data:
with self.subTest(formula=case.f_code):
@@ -506,4 +574,6 @@ def test_null_analyzer_keeps_ap_counts(self):
_, stats_by_case = self._get_null_analyzer_results()
for case in self.data:
with self.subTest(formula=case.f_code):
- self.assertEqual(case.aps, stats_by_case[case.f_code].agg["aps"], case.f_code)
+ self.assertEqual(
+ case.aps, stats_by_case[case.f_code].agg["aps"], case.f_code
+ )
diff --git a/tlparser/cli.py b/tlparser/cli.py
index bd023ea..937ce22 100644
--- a/tlparser/cli.py
+++ b/tlparser/cli.py
@@ -185,7 +185,10 @@ def evaluate_formula(formula_tokens, extended, verbose, requirement_text):
[
"hist",
"viol",
+ "viol_req",
"pair",
+ "pair_req",
+ "ops",
"chord",
"sankey",
"dag",
@@ -225,9 +228,11 @@ def visualize_data(file, latest, selfonly, plot):
viz = Viz(config, file, selfonly)
plot_methods = {
"hist": viz.plot_histogram,
- "viol": viz.plot_violin_engcompl,
- "viol_req": viz.plot_violin_reqtext,
+ "viol": lambda: viz.plot_violin_engcompl(palette_index=1),
+ "viol_req": lambda: viz.plot_violin_reqtext(palette_index=0),
"pair": viz.plot_pairplot,
+ "pair_req": lambda: viz.plot_pairplot_reqwords(include_trend=True),
+ "ops": viz.plot_operator_bars,
"chord": viz.plot_chord,
"sankey": viz.plot_sankey,
"dag": viz.plot_dag_interactive,
diff --git a/tlparser/spot_tools.py b/tlparser/spot_tools.py
index 4490834..5c5618f 100644
--- a/tlparser/spot_tools.py
+++ b/tlparser/spot_tools.py
@@ -137,7 +137,11 @@ def invoke(command, input_data=None):
return stdout.strip()
-def get_automaton_and_stats(ltl_formula, to_buchi=False, to_deterministic=False):
+def get_automaton_and_stats(
+ ltl_formula,
+ to_buchi=False,
+ to_deterministic=False,
+):
"""
Translates LTL and attempts to get basic automaton statistics directly from ltl2tgba
Returns: (hoa_automaton_string, stats_dict)
@@ -147,12 +151,15 @@ def get_automaton_and_stats(ltl_formula, to_buchi=False, to_deterministic=False)
cmd_stats = ["ltl2tgba", "-f", ltl_formula]
if to_buchi:
- cmd_base.append("-B")
- cmd_stats.append("-B")
+ cmd_base.extend(["--ba"])
+ cmd_stats.extend(["--ba"])
if to_deterministic:
cmd_base.append("-D")
cmd_stats.append("-D")
+ cmd_base.extend(["--complete", "--low"])
+ cmd_stats.extend(["--complete", "--low"])
+
hoa_automaton = ""
try:
hoa_automaton = invoke(cmd_base)
@@ -162,17 +169,69 @@ def get_automaton_and_stats(ltl_formula, to_buchi=False, to_deterministic=False)
stats_dict = {}
try:
- stats_output = invoke(cmd_stats + ["--stats=%s %t %p %d %a"])
+ # Output: states, edges, transitions, is_complete, is_deterministic, acceptance_sets
+ stats_output = invoke(cmd_stats + ["--stats=%s %e %t %p %d %a"])
parts = stats_output.split()
- if len(parts) == 5:
+ if len(parts) == 6:
stats_dict["state_count"] = int(parts[0])
- stats_dict["transition_count"] = int(parts[1])
- stats_dict["is_complete"] = parts[2] == "1"
- stats_dict["is_deterministic"] = parts[3] == "1"
- stats_dict["acceptance_sets"] = int(parts[4])
+ stats_dict["edge_count"] = int(parts[1])
+ stats_dict["transition_count"] = int(parts[2])
+ stats_dict["is_complete"] = parts[3] == "1"
+ stats_dict["is_deterministic"] = parts[4] == "1"
+ stats_dict["acceptance_sets"] = int(parts[5])
stats_dict["analysis_source"] = "ltl2tgba_stats"
else:
stats_dict["error"] = "Unexpected stats output format from ltl2tgba."
+
+ # Syntactic-Future Hierarchy (Σ₁, Π₁, Σ₂, Π₂, Δ₁, Δ₂)
+ def get_syntactic_future_hierarchy(formula):
+ try:
+ # Order: sigma1, pi1, sigma2, pi2, delta1, delta2
+ if invoke(["ltlfilt", "-f", formula, "--sigma1"]):
+ return "Σ₁ (syntactic-guarantee)"
+ if invoke(["ltlfilt", "-f", formula, "--pi1"]):
+ return "Π₁ (syntactic-safety)"
+ if invoke(["ltlfilt", "-f", formula, "--sigma2"]):
+ return "Σ₂"
+ if invoke(["ltlfilt", "-f", formula, "--pi2"]):
+ return "Π₂"
+ if invoke(["ltlfilt", "-f", formula, "--delta1"]):
+ return "Δ₁"
+ if invoke(["ltlfilt", "-f", formula, "--delta2"]):
+ return "Δ₂"
+ return "Unclassified"
+ except Exception:
+ return "Error"
+
+ stats_dict["syntactic_future_hierarchy"] = get_syntactic_future_hierarchy(
+ ltl_formula
+ )
+
+ # Safety-Liveness classification (safety, liveness, guarantee, obligation, persistence, recurrence, universal, eventual)
+ def get_safety_liveness_class(formula):
+ try:
+ if invoke(["ltlfilt", "-f", formula, "--safety"]):
+ return "safety"
+ if invoke(["ltlfilt", "-f", formula, "--liveness"]):
+ return "liveness"
+ if invoke(["ltlfilt", "-f", formula, "--guarantee"]):
+ return "guarantee"
+ if invoke(["ltlfilt", "-f", formula, "--obligation"]):
+ return "obligation"
+ if invoke(["ltlfilt", "-f", formula, "--persistence"]):
+ return "persistence"
+ if invoke(["ltlfilt", "-f", formula, "--recurrence"]):
+ return "recurrence"
+ if invoke(["ltlfilt", "-f", formula, "--universal"]):
+ return "universal"
+ if invoke(["ltlfilt", "-f", formula, "--eventual"]):
+ return "eventual"
+ return "Unclassified"
+ except Exception:
+ return "Error"
+
+ stats_dict["safety_liveness_class"] = get_safety_liveness_class(ltl_formula)
+
except (subprocess.CalledProcessError, ValueError) as e:
stats_dict["error"] = f"Failed to get direct stats from ltl2tgba: {e}"
@@ -294,9 +353,7 @@ def get_manna_pnueli_class(ltl_formula):
)
return "Error"
except Exception as e:
- _debug(
- f"An unexpected error occurred during Manna-Pnueli class check: {e}"
- )
+ _debug(f"An unexpected error occurred during Manna-Pnueli class check: {e}")
return "Error"
@@ -331,7 +388,8 @@ def classify_ltl_property(ltl_formula, *, verbose: bool | None = None):
# Translate to default TGBA and analyze
hoa_tgba, tgba_stats = get_automaton_and_stats(
- ltl_formula, to_buchi=False, to_deterministic=False
+ ltl_formula,
+ to_buchi=False,
)
if "error" in tgba_stats:
_debug(f"Falling back to autfilt for TGBA analysis: {tgba_stats['error']}")
@@ -341,42 +399,49 @@ def classify_ltl_property(ltl_formula, *, verbose: bool | None = None):
tgba_automaton_stutter_check = analyze_automaton_fallback(hoa_tgba).get(
"is_stutter_invariant"
)
- classification["tgba_analysis"]["is_stutter_invariant"] = (
- tgba_automaton_stutter_check
- )
+ classification["tgba_analysis"][
+ "is_stutter_invariant"
+ ] = tgba_automaton_stutter_check
# Translate to Buchi (if possible) and analyze
hoa_buchi, buchi_stats = get_automaton_and_stats(
- ltl_formula, to_buchi=True, to_deterministic=False
+ ltl_formula,
+ to_buchi=True,
)
if "error" in buchi_stats:
- _debug(f"Falling back to autfilt for Buchi analysis: {buchi_stats['error']}")
+ _debug(
+ f"Falling back to autfilt for Buchi analysis: {buchi_stats['error']}"
+ )
classification["buchi_analysis"] = analyze_automaton_fallback(hoa_buchi)
else:
classification["buchi_analysis"] = buchi_stats
buchi_automaton_stutter_check = analyze_automaton_fallback(hoa_buchi).get(
"is_stutter_invariant"
)
- classification["buchi_analysis"]["is_stutter_invariant"] = (
- buchi_automaton_stutter_check
- )
+ classification["buchi_analysis"][
+ "is_stutter_invariant"
+ ] = buchi_automaton_stutter_check
# Attempt to produce a deterministic automaton and analyze
hoa_deterministic, deterministic_stats = get_automaton_and_stats(
- ltl_formula, to_buchi=False, to_deterministic=True
+ ltl_formula,
+ to_buchi=False,
+ to_deterministic=True,
)
if "error" in deterministic_stats:
classification["deterministic_attempt"]["success"] = False
- classification["deterministic_attempt"]["error"] = deterministic_stats["error"]
+ classification["deterministic_attempt"]["error"] = deterministic_stats[
+ "error"
+ ]
else:
classification["deterministic_attempt"]["success"] = True
classification["deterministic_attempt"][
"automaton_analysis"
] = deterministic_stats
- det_automaton_stutter_check = analyze_automaton_fallback(hoa_deterministic).get(
- "is_stutter_invariant"
- )
+ det_automaton_stutter_check = analyze_automaton_fallback(
+ hoa_deterministic
+ ).get("is_stutter_invariant")
classification["deterministic_attempt"]["automaton_analysis"][
"is_stutter_invariant"
] = det_automaton_stutter_check
diff --git a/tlparser/stats.py b/tlparser/stats.py
index 30ed0ba..71c43c8 100644
--- a/tlparser/stats.py
+++ b/tlparser/stats.py
@@ -5,6 +5,8 @@
import pprint
from scipy.stats import entropy
from typing import TYPE_CHECKING
+from tlparser.text_utils import count_sentences
+
if TYPE_CHECKING:
from tlparser.stats_ext import SpotAnalyzer
@@ -220,14 +222,28 @@ def _sanitize_for_json(value):
def __str__(self):
return pprint.pformat(self.get_stats(), indent=2)
- def get_requirement_text_stats(self, req_text: str) -> tuple[int | None, int | None, int | None]:
+ def get_requirement_text_stats(
+ self, req_text: str
+ ) -> tuple[int | None, int | None, int | None]:
if req_text:
cleaned_text = req_text.strip()
- if cleaned_text and cleaned_text[-1] not in '.!?':
- cleaned_text += '.'
+ if not cleaned_text:
+ return 0, 0, 0
+
+ base_text = cleaned_text
+ appended_terminal = False
+ if base_text[-1] not in ".!?":
+ cleaned_text = base_text + "."
+ appended_terminal = True
+
char_count = len(cleaned_text)
word_count = len(cleaned_text.split())
- sentence_count = len(re.findall(r'[.!?]+(?:\s|$)', cleaned_text))
+
+ sentence_source = base_text if appended_terminal else cleaned_text
+ sentence_count = count_sentences(sentence_source)
+ if sentence_count == 0 and appended_terminal:
+ sentence_count = 1
+
return char_count, word_count, sentence_count
else:
return None, None, None
diff --git a/tlparser/text_utils.py b/tlparser/text_utils.py
new file mode 100644
index 0000000..ffa8f71
--- /dev/null
+++ b/tlparser/text_utils.py
@@ -0,0 +1,93 @@
+from __future__ import annotations
+
+import re
+from typing import Match
+
+_DOT_PLACEHOLDER = ""
+_TIME_ABBREV_RE = re.compile(r"\b(?:a|p)\.m\.", re.IGNORECASE)
+_MULTI_DOT_ABBREV_RE = re.compile(r"\b(?:[A-Za-z]\.){2,}")
+_COMMON_ABBREV_RE = re.compile(
+ r"\b(?:Mr|Mrs|Ms|Mmes|Dr|Prof|Sr|Jr|St|Mt|No|Fig|Eq|Sec|Dept|Inc|Ltd|vs|etc|cf|approx|resp|Jan|Feb|Mar|Apr|Aug|Sep|Sept|Oct|Nov|Dec)\.",
+ re.IGNORECASE,
+)
+_NUMERIC_DOTTED_RE = re.compile(r"\b\d+(?:\.\d+)+\.?")
+_SENTENCE_BOUNDARY_RE = re.compile(r"[.!?;:]+(?=(?:\s|$|[\"'\)\]]))")
+
+
+def _replace_dots(match: Match[str]) -> str:
+ text = match.group(0)
+ if not text:
+ return text
+
+ trailing_dot = ""
+ if text.endswith(".") and match.end() == len(match.string):
+ trailing_dot = "."
+ text = text[:-1]
+
+ masked = text.replace(".", _DOT_PLACEHOLDER)
+ return masked + trailing_dot
+
+
+def _replace_time_abbrev(match: Match[str]) -> str:
+ text = match.group(0)
+ if not text:
+ return text
+
+ next_segment = match.string[match.end() :]
+ next_char = ""
+ if next_segment:
+ idx = 0
+ while idx < len(next_segment):
+ ch = next_segment[idx]
+ if ch.isspace():
+ idx += 1
+ continue
+ if ch in {'"', "'", ")", "]"} and idx + 1 < len(next_segment):
+ idx += 1
+ continue
+ next_char = ch
+ break
+
+ keep_trailing = match.end() == len(match.string)
+ if next_char and next_char.isupper():
+ keep_trailing = True
+
+ core = text[:-1].replace(".", _DOT_PLACEHOLDER)
+ return core + ("." if keep_trailing else "")
+
+
+def _mask_non_sentence_dots(text: str) -> str:
+ masked = _TIME_ABBREV_RE.sub(_replace_time_abbrev, text)
+ masked = _MULTI_DOT_ABBREV_RE.sub(_replace_dots, masked)
+ masked = _COMMON_ABBREV_RE.sub(_replace_dots, masked)
+ masked = _NUMERIC_DOTTED_RE.sub(_replace_dots, masked)
+ return masked
+
+
+def count_sentences(text: str) -> int:
+ if not text:
+ return 0
+
+ masked = _mask_non_sentence_dots(text)
+ segments = []
+ start = 0
+ for match in _SENTENCE_BOUNDARY_RE.finditer(masked):
+ end = match.end()
+ segment = masked[start:end]
+ if segment.strip():
+ segments.append(segment)
+ start = end
+
+ if start < len(masked):
+ tail = masked[start:]
+ if tail.strip():
+ segments.append(tail)
+
+ eligible = 0
+ for segment in segments:
+ plain_segment = segment.replace(_DOT_PLACEHOLDER, ".")
+ words = re.findall(r"[A-Za-z0-9']+", plain_segment)
+ if len(words) >= 3:
+ eligible += 1
+
+ return eligible
diff --git a/tlparser/utils.py b/tlparser/utils.py
index 0ad2c86..7403906 100644
--- a/tlparser/utils.py
+++ b/tlparser/utils.py
@@ -1,6 +1,6 @@
import json
-import openpyxl
import os
+import openpyxl
import pandas as pd
from contextlib import nullcontext
from datetime import datetime
@@ -11,6 +11,7 @@
from tlparser.config import Configuration
from tlparser.stats import Stats
from tlparser.stats_ext import SpotAnalyzer
+from tlparser.text_utils import count_sentences
class Utils:
@@ -159,6 +160,10 @@ def _echo_labelled(self, label: str, value: str, *, fg: str) -> None:
for line in rest:
click.echo(f"{indent} {line}", err=True)
+ @staticmethod
+ def count_sentences(text: str) -> int:
+ return count_sentences(text)
+
def write_to_excel(self, data):
flattened_data = [self.flatten_dict(item) for item in data]
@@ -249,6 +254,45 @@ def get_latest_excel(folder):
file = os.path.join(folder, latest_file)
return file
+ @staticmethod
+ def rotate_palette_map(
+ palette,
+ types,
+ *,
+ index: int = 0,
+ default_color: str = "#808080",
+ ):
+ """Return a dict mapping of types to colors, rotated by index.
+
+ - palette: mapping type -> color (preferred). If not a dict, attempts to
+ treat it as a sequence of colors aligned to the provided types.
+ - types: ordered sequence of type labels to include.
+ - index: rotation amount (wraps; negative allowed). 0 keeps original.
+ - default_color: color used when a type is missing from palette.
+ """
+ types = list(types)
+ if not types:
+ return {}
+
+ # Build color list aligned to the given types
+ if isinstance(palette, dict):
+ colors = [palette.get(t, default_color) for t in types]
+ else:
+ # Fallback: assume palette is a sequence of colors
+ palette_seq = list(palette or [])
+ if not palette_seq:
+ palette_seq = [default_color] * len(types)
+ # Repeat or trim to match types length
+ times = (len(types) + len(palette_seq) - 1) // len(palette_seq)
+ colors = (palette_seq * times)[: len(types)]
+
+ if len(colors) > 0 and isinstance(index, int):
+ k = index % len(colors)
+ if k:
+ colors = colors[k:] + colors[:k]
+
+ return dict(zip(types, colors))
+
@staticmethod
def lighten_color(hex_color, opacity=0.6):
hex_color = hex_color.lstrip("#")
@@ -314,13 +358,17 @@ def get_column_order(extended: bool = False):
"stats.spot.syntactic_safety",
"stats.spot.is_stutter_invariant_formula",
"stats.spot.manna_pnueli_class",
+ "stats.spot.tgba_analysis.syntactic_future_hierarchy",
+ "stats.spot.tgba_analysis.safety_liveness_class",
"stats.spot.tgba_analysis.state_count",
+ "stats.spot.tgba_analysis.edge_count",
"stats.spot.tgba_analysis.transition_count",
"stats.spot.tgba_analysis.is_complete",
"stats.spot.tgba_analysis.is_deterministic",
"stats.spot.tgba_analysis.acceptance_sets",
"stats.spot.tgba_analysis.is_stutter_invariant",
"stats.spot.buchi_analysis.state_count",
+ "stats.spot.buchi_analysis.edge_count",
"stats.spot.buchi_analysis.transition_count",
"stats.spot.buchi_analysis.is_complete",
"stats.spot.buchi_analysis.is_deterministic",
@@ -329,6 +377,7 @@ def get_column_order(extended: bool = False):
"stats.spot.deterministic_attempt.success",
"stats.spot.deterministic_attempt.error",
"stats.spot.deterministic_attempt.automaton_analysis.state_count",
+ "stats.spot.deterministic_attempt.automaton_analysis.edge_count",
"stats.spot.deterministic_attempt.automaton_analysis.transition_count",
"stats.spot.deterministic_attempt.automaton_analysis.is_complete",
"stats.spot.deterministic_attempt.automaton_analysis.is_deterministic",
diff --git a/tlparser/viz.py b/tlparser/viz.py
index 54b7975..9a74bc7 100644
--- a/tlparser/viz.py
+++ b/tlparser/viz.py
@@ -124,30 +124,76 @@ def plot_histogram(self):
return out
def _plot_violin(
- self, df_long, stats_values, metrics, title_map, out_prefix, include_strip=False
+ self,
+ df_long,
+ stats_values,
+ metrics,
+ title_map,
+ out_prefix,
+ include_strip=False,
+ palette_index=0,
):
type_palette = self.config.color_palette
+ # Build a palette for the present types, optionally rotated by palette_index.
+ present_types = list(df_long["type"].unique())
+ ordered_present_types = [
+ t for t in self.__get_reduced_logic_order() if t in present_types
+ ] or present_types
+
+ plot_palette = Utils.rotate_palette_map(
+ type_palette, ordered_present_types, index=palette_index
+ )
+
+ # Special case: if only one type is present, allow selecting a different
+ # color by index across the full configured palette, so different
+ # violin plots can visually alternate even for the same type.
+ if (
+ len(ordered_present_types) == 1
+ and isinstance(type_palette, dict)
+ and isinstance(palette_index, int)
+ ):
+ only_type = ordered_present_types[0]
+ full_order = self.config.logic_order or list(type_palette.keys())
+ if not full_order:
+ full_colors = list(type_palette.values())
+ else:
+ full_colors = [type_palette.get(t, "#808080") for t in full_order]
+ if len(full_colors) > 0:
+ idx = palette_index % len(full_colors)
+ plot_palette = {only_type: full_colors[idx]}
+
number_of_types = df_long["type"].unique().size
- fig, axes = plt.subplots(
- nrows=2 if len(metrics) > 3 else 1,
- ncols=3,
- figsize=(11, 8) if len(metrics) > 3 else (11, 4),
- sharex=False,
- sharey=False,
- )
- axes = axes.flatten()
- plt.subplots_adjust(hspace=0.05, wspace=0.05)
+ if len(metrics) == 3:
+ # Create a layout with the third plot centered by spanning both columns
+ fig = plt.figure(figsize=(7, 8))
+ gs = fig.add_gridspec(nrows=2, ncols=2)
+ axes_list = [
+ fig.add_subplot(gs[0, 0]),
+ fig.add_subplot(gs[0, 1]),
+ fig.add_subplot(gs[1, :]),
+ ]
+ fig.subplots_adjust(hspace=0.05, wspace=0.05)
+ else:
+ fig, axes = plt.subplots(
+ nrows=3 if len(metrics) > 3 else 1,
+ ncols=2,
+ figsize=(7, 12) if len(metrics) > 3 else (7, 4),
+ sharex=False,
+ sharey=False,
+ )
+ axes_list = axes.flatten().tolist()
+ plt.subplots_adjust(hspace=0.05, wspace=0.05)
i = 1
- for ax, agg in zip(axes, metrics):
+ for ax, agg in zip(axes_list, metrics):
y_max = df_long[df_long["aggregation"] == agg]["value"].max() * 1.8
violin = sns.violinplot(
x="type",
y="value",
data=df_long[df_long["aggregation"] == agg],
hue="type",
- palette=type_palette,
+ palette=plot_palette,
bw_method=0.5,
edgecolor="black",
linewidth=1,
@@ -160,7 +206,7 @@ def _plot_violin(
x="type",
y="value",
hue="type",
- palette=type_palette,
+ palette=plot_palette,
data=df_long[df_long["aggregation"] == agg],
width=0.12,
showcaps=True,
@@ -181,7 +227,7 @@ def _plot_violin(
hue="type",
data=df_long[df_long["aggregation"] == agg],
alpha=0.3,
- palette=type_palette,
+ palette=plot_palette,
size=3,
marker="d",
edgecolor="black",
@@ -202,7 +248,7 @@ def _plot_violin(
)
ax.text(
x_shift,
- 0.83,
+ 0.80,
annotation_text,
color="black",
ha="center",
@@ -241,16 +287,24 @@ def _plot_violin(
minor_tick_interval = major_interval / 5
ax.yaxis.set_minor_locator(ticker.MultipleLocator(minor_tick_interval))
- for j in range(len(metrics), len(axes)):
- axes[j].set_visible(False)
+ for j in range(len(metrics), len(axes_list)):
+ axes_list[j].set_visible(False)
fig.tight_layout()
+ # If exactly 3 metrics, keep the third axis centered without stretching.
+ if len(metrics) == 3:
+ ref = axes_list[0].get_position()
+ bottom = axes_list[2].get_position()
+ w = ref.width
+ h = ref.height
+ x = 0.5 - w / 2
+ axes_list[2].set_position([x, bottom.y0, w, h])
out = self.__get_file_name(out_prefix)
plt.savefig(out)
plt.close()
return out
- def plot_violin_engcompl(self, include_strip=False):
+ def plot_violin_engcompl(self, include_strip=False, palette_index=0):
df_filtered = self.data[self.data["translation"] == "self"]
metrics = df_filtered.filter(like=".agg.").columns.tolist()
metrics = metrics + ["stats.asth", "stats.entropy.lops_tops"]
@@ -274,11 +328,13 @@ def plot_violin_engcompl(self, include_strip=False):
self.title_map,
"viol_engcompl",
include_strip,
+ palette_index,
)
- def plot_violin_reqtext(self, include_strip=False):
+ def plot_violin_reqtext(self, include_strip=False, palette_index=0):
df_filtered = self.data[self.data["translation"] == "self"]
- metrics = df_filtered.filter(like=".req_").columns.tolist()
+ # metrics = df_filtered.filter(like=".req_").columns.tolist()
+ metrics = ["stats.req_word_count", "stats.req_sentence_count"]
df_long = pd.melt(
df_filtered,
id_vars=["id", "type"],
@@ -293,14 +349,23 @@ def plot_violin_reqtext(self, include_strip=False):
.reset_index()
)
return self._plot_violin(
- df_long, stats_values, metrics, self.title_map, "viol_req", include_strip
+ df_long,
+ stats_values,
+ metrics,
+ self.title_map,
+ "viol_req",
+ include_strip,
+ palette_index,
)
- def plot_pairplot(self):
+ def plot_pairplot(self, include_trend: bool = False):
type_palette = self.config.color_palette
df = self.data[self.data["translation"] == "self"]
metrics = df.filter(like=".agg.").columns.tolist()
df_pairplot = df[metrics + ["type", "stats.asth", "stats.entropy.lops_tops"]]
+ req_metrics = df.filter(like=".req_").columns.tolist()
+ if req_metrics:
+ df_pairplot = pd.concat([df_pairplot, df[req_metrics]], axis=1)
unique_types = df_pairplot["type"].nunique()
markers = ["o", "s", "D", "^", "v", "P"][:unique_types]
@@ -322,12 +387,133 @@ def plot_pairplot(self):
artist.set_edgecolor("black")
artist.set_alpha(0.6)
+ if include_trend:
+ # Overlay a single overall linear trend per subplot (off-diagonal only)
+ for r, row in enumerate(g.axes):
+ for c, ax in enumerate(row):
+ xvar = g.x_vars[c]
+ yvar = g.y_vars[r]
+ if xvar == yvar:
+ continue
+ if df_pairplot[xvar].nunique() <= 1:
+ continue
+ sns.regplot(
+ data=df_pairplot,
+ x=xvar,
+ y=yvar,
+ scatter=False,
+ ax=ax,
+ color="black",
+ line_kws={"linewidth": 1.2, "alpha": 0.8, "zorder": 5},
+ )
+ # Restore pretty labels (regplot resets them)
+ ax.set_xlabel(self.title_map.get(xvar, [xvar, ""])[0])
+ ax.set_ylabel(self.title_map.get(yvar, [yvar, ""])[0])
+
g._legend.set_title("")
out = self.__get_file_name("pairp")
plt.savefig(out)
plt.close()
return out
+ def plot_pairplot_reqwords(self, include_trend: bool = False):
+ # Scatter grids with Requirement Words on the Y-axis for selected X metrics
+ df = self.data[self.data["translation"] == "self"].copy()
+
+ x_metrics = [
+ "stats.agg.aps",
+ "stats.agg.cops",
+ "stats.agg.lops",
+ "stats.agg.tops",
+ "stats.asth",
+ "stats.entropy.lops_tops",
+ "stats.req_len",
+ "stats.req_sentence_count",
+ ]
+ y_metric = "stats.req_word_count"
+
+ available = [m for m in x_metrics if m in df.columns]
+ if y_metric not in df.columns or not available:
+ # Nothing to plot
+ return ""
+
+ # Build figure with 2 columns and dynamic rows
+ ncols = 2
+ n = len(available)
+ nrows = math.ceil(n / ncols)
+ fig_height = max(3, nrows * 3)
+ fig, axes = plt.subplots(
+ nrows=nrows, ncols=ncols, figsize=(7, fig_height), sharey=True, sharex=False
+ )
+ # Match _plot_violin spacing
+ plt.subplots_adjust(hspace=0.05, wspace=0.05)
+
+ if nrows * ncols == 1:
+ axes = [axes]
+ else:
+ axes = axes.flatten()
+
+ base_color = "#ffaf2d"
+
+ for ax, x in zip(axes, available):
+ ax.scatter(
+ df[x],
+ df[y_metric],
+ s=28,
+ c=base_color,
+ alpha=0.55,
+ edgecolors="black",
+ linewidths=0.5,
+ )
+
+ # Match _plot_violin: use subplot title above, empty x-label
+ x_title = self.title_map.get(x, [x, ""])[0]
+ ax.set_title(x_title, fontsize=plt.rcParams.get("axes.titlesize", 10))
+ ax.set_xlabel("")
+ ax.set_ylabel("Requirement Words")
+
+ if include_trend and df[x].nunique() > 1:
+ sns.regplot(
+ data=df,
+ x=x,
+ y=y_metric,
+ scatter=False,
+ ax=ax,
+ color="black",
+ line_kws={"linewidth": 1.2, "alpha": 0.8, "zorder": 5},
+ )
+ # Keep labels consistent after regplot overlay
+ ax.set_title(x_title, fontsize=plt.rcParams.get("axes.titlesize", 10))
+ ax.set_xlabel("")
+ ax.set_ylabel("Requirement Words")
+
+ fig.tight_layout()
+
+ # If the last row contains a single plot, center it within the bottom-row span (no stretching)
+ if n % ncols == 1 and len(axes) >= (nrows * ncols):
+ idx = (nrows - 1) * ncols # first axis in the last row
+ # Use both bottom axes to compute true span, even if the second is empty
+ left_pos = axes[idx].get_position()
+ right_pos = axes[idx + 1].get_position()
+ left_edge = left_pos.x0
+ right_edge = right_pos.x0 + right_pos.width
+ x_center = (left_edge + right_edge) / 2.0
+
+ W = left_pos.width
+ H = left_pos.height
+ Y0 = left_pos.y0
+ X0 = x_center - W / 2.0
+ axes[idx].set_position([X0, Y0, W, H])
+
+ # Hide any unused axes (if the grid is larger than available metrics)
+ for j in range(len(available), len(axes)):
+ axes[j].set_visible(False)
+
+ out = self.__get_file_name("pair_reqw")
+ plt.savefig(out)
+ plt.close()
+ return out
+
def plot_sankey(self):
df = self.data.copy()
flow_counts = {"yes": {}, "no": {}, "depends": {}}
@@ -540,3 +726,134 @@ def plot_dag_interactive(self):
outs.append(out)
return outs
+
+ def plot_operator_bars(self):
+ # Summarize operator counts across self translations and plot three bar charts:
+ # (a) Temporal, (b) Logical on the first row, and (c) Comparison centered in the second row.
+ df = self.data[self.data["translation"] == "self"].copy()
+
+ groups = [
+ (
+ "(a) Temporal",
+ {
+ "F": "stats.tops.F",
+ "G": "stats.tops.G",
+ "U": "stats.tops.U",
+ "X": "stats.tops.X",
+ },
+ ),
+ (
+ "(b) Logical",
+ {
+ "and": "stats.lops.and",
+ "implies": "stats.lops.impl",
+ "not": "stats.lops.not",
+ "or": "stats.lops.or",
+ },
+ ),
+ (
+ "(c) Comparison",
+ {
+ "eq": "stats.cops.eq",
+ "geq": "stats.cops.geq",
+ "gt": "stats.cops.gt",
+ "leq": "stats.cops.leq",
+ "lt": "stats.cops.lt",
+ "neq": "stats.cops.neq",
+ },
+ ),
+ ]
+
+ # Prepare data per group
+ bar_groups = []
+ for title, mapping in groups:
+ labels, values = [], []
+ cols = [col for col in mapping.values() if col in df.columns]
+ if cols:
+ sums = df[cols].sum()
+ for label, col in mapping.items():
+ if col in sums.index:
+ labels.append(label)
+ values.append(int(sums[col]))
+ if not labels:
+ labels, values = ["n/a"], [0]
+ bar_groups.append((title, labels, values))
+
+ # Compute separate y-limits: shared for first row, independent for third plot
+ first_row_max = max(
+ (max(vals) for _, _, vals in bar_groups[:2] if vals), default=0
+ )
+ third_max = max(bar_groups[2][2]) if bar_groups[2][2] else 0
+ y_top_first = max(1, int(first_row_max * 1.15) + 1)
+ y_top_third = max(1, int(third_max * 1.15) + 1)
+
+ # Make second row shorter
+ second_row_ratio = 0.7 # < 1.0 makes the second row less high than the first
+ fig = plt.figure(figsize=(6, 5))
+ gs = fig.add_gridspec(nrows=2, ncols=2, height_ratios=[1.0, second_row_ratio])
+
+ ax00 = fig.add_subplot(gs[0, 0])
+ ax01 = fig.add_subplot(gs[0, 1], sharey=ax00) # share y only within first row
+ ax10 = fig.add_subplot(gs[1, 0]) # independent y
+ ax11 = fig.add_subplot(gs[1, 1]) # placeholder to compute span
+ axes = [ax00, ax01, ax10, ax11]
+
+ palette = sns.color_palette("tab10")
+ alpha = 0.85
+
+ # Plot the three groups on the first three axes
+ for idx, (ax, (title, labels, values)) in enumerate(zip(axes[:3], bar_groups)):
+ base_colors = palette[: len(labels)]
+ bar_colors = [(r, g, b, alpha) for (r, g, b) in base_colors]
+ bars = ax.bar(labels, values, color=bar_colors, edgecolor="black")
+ ax.set_title(title)
+ ax.set_ylabel("Count")
+ if idx < 2:
+ ax.set_ylim(0, y_top_first)
+ else:
+ ax.set_ylim(0, y_top_third)
+
+ for rect, val in zip(bars, values):
+ ax.annotate(
+ str(val),
+ xy=(rect.get_x() + rect.get_width() / 2, rect.get_height()),
+ xytext=(0, 3),
+ textcoords="offset points",
+ ha="center",
+ va="bottom",
+ fontsize=9,
+ )
+
+ fig.tight_layout()
+
+ # Stretch the third plot to match bar pixel width of first row and center within bottom-row span
+ n_bars = [len(labels) for _, labels, _ in bar_groups]
+ if n_bars[2] > 0 and max(n_bars[0], n_bars[1]) > 0:
+ top_left = axes[0].get_position()
+
+ # Use both bottom axes to get the true span of the second row
+ bottom_left = axes[2].get_position()
+ bottom_right = axes[3].get_position()
+ left_edge = bottom_left.x0
+ right_edge = bottom_right.x0 + bottom_right.width
+ span_total = right_edge - left_edge
+
+ W_ref = top_left.width
+ N_ref = max(n_bars[0], n_bars[1])
+ desired_W3 = W_ref * (n_bars[2] / N_ref)
+
+ W3 = min(desired_W3, span_total)
+ H3 = bottom_left.height
+ Y3 = bottom_left.y0
+
+ X_center = (left_edge + right_edge) / 2.0
+ X3 = X_center - W3 / 2.0
+ axes[2].set_position([X3, Y3, W3, H3])
+
+ # Hide the unused 4th axis after layout adjustments
+ axes[3].set_visible(False)
+
+ out = self.__get_file_name("ops_bars")
+ plt.savefig(out)
+ plt.close()
+ return out