vieirin · vieirin · Jul 19, 2026 · Jul 11, 2026 · Jul 11, 2026 · Jul 11, 2026
diff --git a/.DS_Store b/.DS_Store
diff --git a/.cursor/rules/edgev2-leave-edge-untouched.mdc b/.cursor/rules/edgev2-leave-edge-untouched.mdc
@@ -0,0 +1,22 @@
+---
+description: When working on edgeV2, never modify the legacy edge/ engine
+alwaysApply: true
+---
+
+# EdgeV2 vs Edge Engine
+
+When working on **edgeV2**, leave the legacy **edge** engine untouched.
+
+## Do
+
+- Implement, fix, and refactor only under `packages/lib/src/engines/edgeV2/`
+- Prefer copying or adapting patterns from `edge/` into `edgeV2/` when needed
+- Read `edge/` for reference only
+
+## Do not
+
+- Edit, delete, or refactor files under `packages/lib/src/engines/edge/`
+- "Keep them in sync" by changing both engines
+- Fix bugs in `edge/` unless the user explicitly asks to change the legacy engine
+
+If a change seems to require touching `edge/`, stop and ask first.
diff --git a/.ollie/audit.jsonl b/.ollie/audit.jsonl
diff --git a/dissertationExamples/dualGoalOrAny.txt b/dissertationExamples/dualGoalOrAny.txt
@@ -12,7 +12,7 @@
       "nodes": [
         {
           "id": "d201ecf8-634a-425e-8e6e-f59885442511",
-          "text": "G0: Collect sample [+]",
+          "text": "G0: Collect sample [T0?T1]",
           "type": "istar.Goal",
           "x": 373,
           "y": 152,

diff --git a/dissertationExamples/goalModel TAS 1.txt b/dissertationExamples/goalModel TAS 1.txt
@@ -113,7 +113,7 @@
         },
         {
           "id": "ef565838-6961-4f79-87eb-b9db1e57c409",
-          "text": "G10: Administer medicine [+]",
+          "text": "G10: Administer medicine [G11?G12]",
           "type": "istar.Goal",
           "x": 607,
           "y": 355,
@@ -351,7 +351,7 @@
         },
         {
           "id": "67c420f7-9c2d-4911-bdc5-bae573c73eb6",
-          "text": "G2: Track patient location [+]",
+          "text": "G2: Track patient location [T2?T3]",
           "type": "istar.Goal",
           "x": 665,
           "y": 170,

diff --git a/dissertationExamples/goalModel TAS 2.txt b/dissertationExamples/goalModel TAS 2.txt
@@ -113,7 +113,7 @@
         },
         {
           "id": "ef565838-6961-4f79-87eb-b9db1e57c409",
-          "text": "G10: Administer medicine [+]",
+          "text": "G10: Administer medicine [G11?G12]",
           "type": "istar.Goal",
           "x": 607,
           "y": 355,
@@ -354,7 +354,7 @@
         },
         {
           "id": "67c420f7-9c2d-4911-bdc5-bae573c73eb6",
-          "text": "G2: Track patient location [+]",
+          "text": "G2: Track patient location [T2?T3]",
           "type": "istar.Goal",
           "x": 665,
           "y": 170,

diff --git a/dissertationExamples/goalModel(16).txt b/dissertationExamples/goalModel(16).txt
@@ -328,7 +328,7 @@
         },
         {
           "id": "e1d797d6-5d27-4b65-a6fd-7ce9597c007a",
-          "text": "G13: Prepare sample [+]",
+          "text": "G13: Prepare sample [G3?G4]",
           "type": "istar.Goal",
           "x": 471,
           "y": 302,

diff --git a/dissertationExamples/goalModelTAS_new.txt b/dissertationExamples/goalModelTAS_new.txt
@@ -113,7 +113,7 @@
         },
         {
           "id": "ef565838-6961-4f79-87eb-b9db1e57c409",
-          "text": "G10: Administer medicine [+]",
+          "text": "G10: Administer medicine [G11?G12]",
           "type": "istar.Goal",
           "x": 712,
           "y": 353,
@@ -351,7 +351,7 @@
         },
         {
           "id": "67c420f7-9c2d-4911-bdc5-bae573c73eb6",
-          "text": "G2: Track patient location [+]",
+          "text": "G2: Track patient location [T2?T3]",
           "type": "istar.Goal",
           "x": 771,
           "y": 168,

diff --git a/examples/EDGEV2.txt b/examples/EDGEV2.txt
@@ -0,0 +1,158 @@
+// edgeV2 PRISM sketch — names aligned to packages/lib/src/engines/edgeV2
+//
+// Types (GoalExecutionDetail / Relation):
+//   relationToChildren: 'and' | 'or'
+//   executionDetail.type: 'sequence' | 'interleaved' | 'anyOrder' | 'alternative' | 'choice' | 'degradation'
+//     (also in types but unused here: 'decisionMaking')
+//
+// Module vars (template/common.ts):
+//   stateVariable(id)      → g<id>_state : [0..1]     // 0 not pursued, 1 pursued
+//   chosenVariable(id)     → g<id>_chosen : [0..n]    // OR + choice only
+//   goalFailedVariable(c)  → g<c.id>_failed : [0..N]  // degradation + child maxRetries
+//
+// Decision consts (decisionVariables.ts):
+//   decisionVariableName(id)    → decision_G<id>   // every goal
+//   selectionDecisionVariableName(id)  → _decision_G<id>  // OR goals + AND anyOrder
+//
+// Formulas / transitions:
+//   achieved is a formula (not a module var): g<id>_achieved
+//   labels: pursue_G<id>, skip_G<id>, achieved_G<id>
+//   achievability: G<id>_achievable
+
+
+// ─── AND + sequence ─────────────────────────────────────────────────────────
+// relationToChildren: 'and'
+// executionDetail: { type: 'sequence', sequence: ['G1', 'G2'] }
+
+module G0
+  g0_state : [0..1] init 0; // stateVariable('G0') — 0 not pursued, 1 currently pursued
+
+  [pursue_G0] !g0_achieved & g0_state=0 & GUARD -> (g0_state'=1); // triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0_state=1 & G0_achievable*10.0 > decision_G0 -> true; // decide whether to pursue a child or skip
+  [pursue_G2] !g0_achieved & g0_state=1 & G0_achievable*10.0 > decision_G0 & g1_achieved -> true; // sequence: G1 must be achieved first
+
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g2_state=0 & G0_achievable*10.0 <= decision_G0 -> (g0_state'=0); // skip only when no child is pursued
+
+  [achieved_G0] g0_state=1 & g0_achieved & g1_state=0 & g2_state=0 -> (g0_state'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved & g2_achieved);
+
+
+// ─── AND any order ──────────────────────────────────────────────────────────
+// relationToChildren: 'and'
+// executionDetail: { type: 'anyOrder', anyOrder: ['G1', 'G2'] }  // notation: [G1+G2]
+// decision: decision_G0 + _decision_G0 (child selection among idle siblings)
+
+module G0
+  g0_state : [0..1] init 0; // 0 not pursued, 1 currently pursued
+
+  [pursue_G0] !g0_achieved & g0_state=0 & GUARD -> (g0_state'=1); // triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0_state=1 & G0_achievable*10.0 > decision_G0 & g2_state!=1 & (g2_state=1 | (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0) -> true;
+  [pursue_G2] !g0_achieved & g0_state=1 & G0_achievable*10.0 > decision_G0 & g1_state!=1 & (g1_state=1 | (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0) -> true;
+
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g2_state=0 & G0_achievable*10.0 <= decision_G0 -> (g0_state'=0);
+
+  [achieved_G0] g0_state=1 & g0_achieved & g1_state=0 & g2_state=0 -> (g0_state'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved & g2_achieved);
+formula G0_achievable = G1_achievable * G2_achievable;
+
+
+// ─── AND + interleaved ──────────────────────────────────────────────────────
+// relationToChildren: 'and'
+// executionDetail: { type: 'interleaved', interleaved: ['G1', 'G2'] }
+
+module G0
+  g0_state : [0..1] init 0; // 0 not pursued, 1 currently pursued
+
+  [pursue_G0] !g0_achieved & g0_state=0 & GUARD -> (g0_state'=1); // triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0_state=1 & G1_achievable*10.0 > decision_G1 -> true;
+  [pursue_G2] !g0_achieved & g0_state=1 & G2_achievable*10.0 > decision_G2 -> true; // skip G0 if neither child should be pursued (avoids pursue-skip livelock)
+
+  [skip_G0] g0_state=1 & g1_state=0 & g2_state=0 & !g0_achieved & !(G2_achievable*10.0 > decision_G2 | G1_achievable*10.0 > decision_G1) -> (g0_state'=0);
+
+  [achieved_G0] g0_state=1 & g0_achieved & g1_state=0 & g2_state=0 -> (g0_state'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved & g2_achieved);
+
+
+// ─── OR + alternative ───────────────────────────────────────────────────────
+// relationToChildren: 'or'
+// executionDetail: { type: 'alternative', alternative: ['G1', 'G2'] }
+// decision: decision_G0 + _decision_G0 (OR)
+
+module G0
+  g0_state : [0..1] init 0; // 0 not pursued, 1 currently pursued
+
+  [pursue_G0] !g0_achieved & g0_state=0 & GUARD -> (g0_state'=1); // triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0_state=1 & G0_achievable*10.0 > decision_G0 & g2_state=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0 -> true;
+  [pursue_G2] !g0_achieved & g0_state=1 & G0_achievable*10.0 > decision_G0 & g1_state=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0 -> true;
+
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g2_state=0 & G0_achievable*10.0 <= decision_G0 -> (g0_state'=0);
+
+  [achieved_G0] g0_state=1 & g1_state=0 & g2_state=0 & g0_achieved -> (g0_state'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved | g2_achieved);
+
+
+// ─── OR + choice ("choose once") ────────────────────────────────────────────
+// relationToChildren: 'or'
+// executionDetail: { type: 'choice' }
+// module vars: stateVariable + chosenVariable (n = #pursueable children)
+
+module G0
+  g0_state : [0..1] init 0; // 0 not pursued, 1 currently pursued
+  g0_chosen : [0..2] init 0; // 0 not chosen, 1 chose G1, 2 chose G2
+
+  [pursue_G0] !g0_achieved & g0_state=0 & GUARD -> (g0_state'=1); // triggering the goal from upper layer
+  [pursue_G1] !g0_achieved & g0_state=1 & g0_chosen=0 & G0_achievable*10.0 > decision_G0 & g2_state=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0 -> (g0_chosen'=1);
+  [pursue_G2] !g0_achieved & g0_state=1 & g0_chosen=0 & G0_achievable*10.0 > decision_G0 & g1_state=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0 -> (g0_chosen'=2);
+
+  [pursue_G1] !g0_achieved & g0_state=1 & g0_chosen=1 & G1_achievable*10.0 > decision_G1 -> true;
+  [pursue_G2] !g0_achieved & g0_state=1 & g0_chosen=2 & G2_achievable*10.0 > decision_G2 -> true;
+
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g2_state=0 & g0_chosen=0 & G0_achievable*10.0 <= decision_G0 -> (g0_state'=0);
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g0_chosen=1 & G1_achievable*10.0 <= decision_G1 -> (g0_state'=0); // skip when g0_chosen=1
+  [skip_G0] !g0_achieved & g0_state=1 & g2_state=0 & g0_chosen=2 & G2_achievable*10.0 <= decision_G2 -> (g0_state'=0);
+
+  [achieved_G0] g0_state=1 & g1_state=0 & g2_state=0 & g0_achieved -> (g0_state'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved | g2_achieved);
+
+
+// ─── OR + degradation ───────────────────────────────────────────────────────
+// relationToChildren: 'or'
+// executionDetail: { type: 'degradation', degradationList: ['G1', 'G2'], retryMap?: { G1: N } }
+// module vars: stateVariable + goalFailedVariable(child) for childrenWithMaxRetries
+// Note: older sketches used parent g0_failed; codegen uses per-child g1_failed (below).
+
+module G0
+  g0_state : [0..1] init 0; // 0 not pursued, 1 currently pursued
+  g1_failed : [0..N] init 0; // goalFailedVariable('G1') — retry G1 up to N times
+
+  [pursue_G0] !g0_achieved & g0_state=0 & GUARD -> (g0_state'=1); // triggering the goal from upper layer
+
+  [pursue_G1] !g0_achieved & g0_state=1 & g1_failed<N & G1_achievable*10.0 > decision_G1 -> (g1_failed'=g1_failed+1); // retry G1 up to N
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g1_failed<N & G1_achievable*10.0 <= decision_G1 -> (g0_state'=0);
+
+  [pursue_G1] !g0_achieved & g0_state=1 & g1_failed=N & G0_achievable*10.0 > decision_G0 & g2_state=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 > _decision_G0 -> true;
+  [pursue_G2] !g0_achieved & g0_state=1 & g1_failed=N & G0_achievable*10.0 > decision_G0 & g1_state=0 & (G1_achievable/(G1_achievable+G2_achievable))*10.0 <= _decision_G0 -> true;
+
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g1_failed<N & G1_achievable*10.0 <= decision_G1 -> (g0_state'=0);
+  [skip_G0] !g0_achieved & g0_state=1 & g1_state=0 & g2_state=0 & g1_failed=N & G0_achievable*10.0 <= decision_G0 -> (g0_state'=0);
+
+  [achieved_G0] !g0_achieved & g0_state=1 & g1_state=0 & g2_state=0 & g0_achieved -> (g0_state'=0);
+
+endmodule
+
+formula g0_achieved = (g1_achieved | g2_achieved);
diff --git a/examples/experiments/10-minimalMaintainResource.txt b/examples/experiments/10-minimalMaintainResource.txt
@@ -43,7 +43,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 305,

diff --git a/examples/experiments/4-interleavedChoicePDegradation.txt b/examples/experiments/4-interleavedChoicePDegradation.txt
@@ -32,7 +32,7 @@
         },
         {
           "id": "912c8be2-1e4d-4b6a-b45c-9169f9fba033",
-          "text": "G2: Configure flight [+]",
+          "text": "G2: Configure flight [G7?G8]",
           "type": "istar.Goal",
           "x": 627,
           "y": 282,

diff --git a/examples/experiments/5-allAnnotations.txt b/examples/experiments/5-allAnnotations.txt
@@ -62,7 +62,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 304,

diff --git a/examples/experiments/6-allnotationsReduced.txt b/examples/experiments/6-allnotationsReduced.txt
@@ -62,7 +62,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 304,

diff --git a/examples/experiments/7-minimalAll.txt b/examples/experiments/7-minimalAll.txt
@@ -42,7 +42,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 304,

diff --git a/examples/experiments/8-minimalMaintain.txt b/examples/experiments/8-minimalMaintain.txt
@@ -42,7 +42,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 305,

diff --git a/examples/experiments/9-minimalMaintainContext copy.txt b/examples/experiments/9-minimalMaintainContext copy.txt
@@ -42,7 +42,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 305,

diff --git a/examples/experiments/9-minimalMaintainContext.txt b/examples/experiments/9-minimalMaintainContext.txt
@@ -43,7 +43,7 @@
         },
         {
           "id": "ee59bf52-abc8-4d5e-8148-f8cd0ab0d52c",
-          "text": "G3: Configure Flight Profile [+]",
+          "text": "G3: Configure Flight Profile [G9?G10?G11]",
           "type": "istar.Goal",
           "x": 813,
           "y": 305,

diff --git a/examples/experiments/goalModel_TAS_3.txt b/examples/experiments/goalModel_TAS_3.txt
@@ -103,7 +103,7 @@
         },
         {
           "id": "1300f48c-890f-41f9-9d53-faf08becfcce",
-          "text": "G11: Analyse data [+]",
+          "text": "G11: Analyse data [G14?G15]",
           "type": "istar.Goal",
           "x": 411,
           "y": 355,
@@ -113,7 +113,7 @@
         },
         {
           "id": "ef565838-6961-4f79-87eb-b9db1e57c409",
-          "text": "G12: Administer medicine [G16|G17]",
+          "text": "G12: Administer medicine [G16?G17]",
           "type": "istar.Goal",
           "x": 605,
           "y": 355,
@@ -201,7 +201,7 @@
         },
         {
           "id": "c6de8c50-a3a9-4dbd-b9c1-e2c8315ae1f6",
-          "text": "G19: Trigger Alarm Service [+]",
+          "text": "G19: Trigger Alarm Service [G20?G21]",
           "type": "istar.Goal",
           "x": 1037,
           "y": 345,

diff --git a/examples/experiments/labSamplesWithSideEffect.txt b/examples/experiments/labSamplesWithSideEffect.txt
@@ -303,7 +303,7 @@
         },
         {
           "id": "e1d797d6-5d27-4b65-a6fd-7ce9597c007a",
-          "text": "G13: Prepare sample [+]",
+          "text": "G13: Prepare sample [G3?G4]",
           "type": "istar.Goal",
           "x": 470,
           "y": 302,

diff --git a/examples/experiments/props/10-minimalMaintainResource.props b/examples/experiments/props/10-minimalMaintainResource.props
@@ -89,7 +89,7 @@ P>=1 [ G (G2_achieved=1 => G6_achieved=1) ];
 
 
 // ======================================================
-// Choice semantics for G3: Configure Flight Profile [+]
+// Choice semantics for G3: Configure Flight Profile [G9?G10?G11]
 // Branches: G9, G10, G11 with battery-dependent guards on R0
 // ======================================================
 

diff --git a/examples/experiments/props/4-interleavedChoicePDegradation.props b/examples/experiments/props/4-interleavedChoicePDegradation.props
@@ -1,5 +1,5 @@
 // ======================================================
-// CHOICE OR  (+)   —  G2: Configure flight [+]
+// CHOICE OR  (?)   —  G2: Configure flight [G7?G8]
 //   Children: G7 (Standard Mode) and G8 (High-Priority)
 //   Encoding: G2_chosen ∈ {0,1,2}, set by pursue_G7 / pursue_G8
 // ======================================================
@@ -114,7 +114,7 @@ P>=1 [
   G ( (G1_achieved=1) => (G5_achieved=1 & G6_achieved=1) )
 ];
 
-// G2 — Choice OR [+] (already partly covered above):
+// G2 — Choice OR [G7?G8] (already partly covered above):
 //      When G2 completes, exactly one branch has been achieved.
 //      (Given the model, “at most one” + “at least one” gives exactly one.)
 P>=1 [