Get tags, variable names, and constraints from reactions

COCOPATH_TECHNICAL_REPORT.md

@@ -119,20 +119,20 @@ CocoPath is a **concolic execution framework** for systematically exploring exec
 ```
 INPUT: Initial value (e.g., user_choice = 0)
    ↓
-[PathExplorer creates tagged Integer with label]
-   Tag stores: variable name + symbolic expression
+[PathExplorer passes concrete value to executor]
+   No tagging at this level
    ↓
-[Tagged value passed to execution wrapper]
+[Vitruvius reaction receives concrete value]
    ↓
-[Execution wrapper reads tag] ← NEW: Tag Reading Step
-   Extracts: varName = tag.getLabels()[0]
-   Extracts: symbolicExpr = GaletteSymbolicator.getExpressionForTag(tag)
+[Reaction calls GaletteSymbolicator.getOrMakeSymbolicInt]
+   Creates tag with qualified name: "CreateAscetTaskRoutine:execute:userChoice"
+   Reuses tag on subsequent iterations
+   Adds domain constraint automatically
    ↓
-[Tag propagates through execution via Galette shadow stack]
+[Tagged value used in reaction]
    ↓
-[Constraints collected using tag-derived variable name]
-   PathUtils.addIntDomainConstraint(varName, 0, 5)  ← Uses extracted varName
-   PathUtils.addSwitchConstraint(varName, concreteValue)
+[Reaction calls SymbolicComparison.symbolicVitruviusChoice]
+   Records switch constraint with qualified name from tag
    ↓
 [PathConditionWrapper stores constraints]
    ↓
@@ -775,7 +775,8 @@ For path (i, j):
 **Collection Timeline** (per execution):
 ```
 T0: PathExplorer creates Map<String,Object> inputs
-      {user_choice_1: taggedInt₁, user_choice_2: taggedInt₂}
+      {user_choice_1: concreteInt₁, user_choice_2: concreteInt₂}
+      (No tagging - reactions handle it)
 
 T1: Reset PathConditionWrapper
 

README.md

@@ -34,11 +34,12 @@ This framework provides **concolic execution** (combined concrete + symbolic exe
 - **Location**: `knarr-runtime/src/main/java/edu/neu/ccs/prl/galette/concolic/knarr/runtime/`
 - **Key Classes**:
   - `GaletteSymbolicator` - Creates symbolic values with tags
-  - `PathUtils` - Manual constraint collection API
-    - `addIntDomainConstraint(varName, min, max)` - manually Define valid value ranges
-    - `addSwitchConstraint(varName, value)` - Record executed path for switch case
-    - `getCurPC()` - Retrieve current path condition
+    - `getOrMakeSymbolicInt(qualifiedName, value, min, max)` - Create or reuse tag with domain constraint
+    - Tag reuse across iterations using qualified names (e.g., "CreateAscetTaskRoutine:execute:userChoice")
+  - `SymbolicComparison` - Records switch constraints from reactions
+    - `symbolicVitruviusChoice(selected, min, max)` - Records the actual choice made
   - `PathExplorer` - Automatic path exploration orchestration
+  - `PathUtils` - Retrieves current path condition (`getCurPC()`)
   - `ConstraintSolver` - Negates and solves constraints using GREEN/Z3
 
 #### GreenSolver
@@ -160,6 +161,43 @@ amalthea-acset-integration/                    # Vitruvius example
 3. **Python 3.x** (for dependency switching)
 
 
+### Helper Classes
+
+- **`AutomaticVitruvPathExplorationHelper`** - Shared utilities for path exploration
+  - `verifyInstrumentation()` - Checks that Galette instrumentation is working
+  - `initializeEMF()` - Initializes EMF resource factories
+  - `loadVitruviusTestClass()` - Loads the Vitruvius Test class
+  - `createWorkingDirectory()` - Creates output directories
+  - `exportSingleVarResults()` - Exports single-variable exploration results
+  - `exportMultiVarResults()` - Exports multi-variable exploration results
+
+### Syncing Generated Reactions (After Upstream Changes)
+
+When the upstream Amalthea-acset project changes (e.g., renaming InterruptTask to InitTask), you need to sync the generated reactions code:
+
+```bash
+# 1. Build external Amalthea-acset to generate new reactions
+cd /path/to/Amalthea-acset
+mvn clean generate-sources
+
+# 2. Copy generated reactions to internal project
+cd knarr-runtime
+./copy-generated-reactions.sh
+
+# Or with custom paths:
+./copy-generated-reactions.sh --external-path /path/to/Amalthea-acset
+
+# 3. Build internal project with updated reactions
+cd ../amalthea-acset-integration
+mvn clean compile -Dcheckstyle.skip=true
+```
+
+The `copy-generated-reactions.sh` script:
+- Copies generated reactions from `Amalthea-acset/consistency/target/generated-sources/reactions/mir/`
+- To `amalthea-acset-integration/consistency/src/main/java/mir/`
+- Creates backups of existing files
+- Supports custom paths with `--external-path` and `--internal-path` flags
+
 ### Quick Start
 
 ```bash

WORKFLOW_DIAGRAM.md

@@ -20,13 +20,14 @@
 │ │    ├─ Create PathExplorer                                            │   │
 │ │    └─ Call exploreInteger()                                          │   │
 │ │                                                                       │   │
-│ │  executeVitruvWithInput(testInstance, taggedInteger)                 │   │
-│ │    ├─ [T3] PathUtils.addIntDomainConstraint("user_choice", 0, 5)    │   │
-│ │    │        → PC = [(0 <= user_choice < 5)]                          │   │
-│ │    ├─ [T4] insertTask.invoke(testInstance, workDir, taggedInteger)  │   │
-│ │    ├─ [T5] PathUtils.addSwitchConstraint("user_choice", value)      │   │
-│ │    │        → PC += [user_choice == N]                               │   │
-│ │    └─ [T6] return PathUtils.getCurPC()                              │   │
+│ │  executeVitruvWithInput(testInstance, concreteInteger)               │   │
+│ │    ├─ [T3] insertTask.invoke(testInstance, workDir, concreteInteger)│   │
+│ │    │        → Triggers Vitruvius reaction                           │   │
+│ │    │        → Reaction calls GaletteSymbolicator.getOrMakeSymbolicInt│   │
+│ │    │        → Creates/reuses tag + adds domain constraint           │   │
+│ │    │        → Reaction calls SymbolicComparison.symbolicVitruviusChoice│ │
+│ │    │        → Records switch constraint                              │   │
+│ │    └─ [T4] return PathUtils.getCurPC()                              │   │
 │ └──────────────────────────────────────────────────────────────────────┘   │
 │                                                                              │
 │ ┌──────────────────────────────────────────────────────────────────────┐   │
@@ -36,16 +37,15 @@
 │ │    │                                                                  │   │
 │ │    ├─ LOOP: while (hasUnexploredPaths && iteration < MAX)           │   │
 │ │    │   │                                                             │   │
-│ │    │   ├─ [T0] Create tagged Integer                                │   │
-│ │    │   │        GaletteSymbolicator.tagInteger(value, varName)      │   │
-│ │    │   │        → Tagged(concrete=N, symbolic=α, label=varName)     │   │
+│ │    │   ├─ [T0] Pass concrete value to executor                      │   │
+│ │    │   │        (No tagging - reactions handle it)                  │   │
 │ │    │   │                                                             │   │
-│ │    │   ├─ [T1] Reset PC: PathUtils.getCurPC().clear()              │   │
+│ │    │   ├─ [T1] Reset PC: PathUtils.resetPC()                       │   │
 │ │    │   │                                                             │   │
-│ │    │   ├─ [T2-T6] Execute: executor(taggedInteger)                 │   │
+│ │    │   ├─ [T2-T4] Execute: executor(concreteInteger)               │   │
 │ │    │   │        → Returns PathConditionWrapper                      │   │
 │ │    │   │                                                             │   │
-│ │    │   ├─ [T7] Store PathRecord {inputs, constraints, time}        │   │
+│ │    │   ├─ [T5] Store PathRecord {inputs, constraints, time}        │   │
 │ │    │   │                                                             │   │
 │ │    │   ├─ Find unexplored constraint to negate                      │   │
 │ │    │   │                                                             │   │
@@ -101,12 +101,14 @@
 ┌──────────────────────────────────────▼──────────────────────────────────────┐
 │                       TAG PROPAGATION LAYER (Galette)                        │
 │ ┌──────────────────────────────────────────────────────────────────────┐   │
-│ │  GaletteSymbolicator.java                                            │   │
+│ │  GaletteSymbolicator.java (Called from Reactions)                   │   │
 │ │                                                                       │   │
-│ │  tagInteger(int value, String label)                                │   │
-│ │    ├─ Create Tag(label, IntVariable(label))                         │   │
-│ │    ├─ Associate tag with Integer object                             │   │
-│ │    └─ return Tagged Integer                                         │   │
+│ │  getOrMakeSymbolicInt(qualifiedName, value, min, max)               │   │
+│ │    ├─ Check labelToTag map for existing tag                         │   │
+│ │    ├─ If exists: reuse tag (tag reuse across iterations)           │   │
+│ │    ├─ If new: create Tag + IntVariable + domain constraint         │   │
+│ │    ├─ Apply tag with Tainter.setTag(value, tag)                    │   │
+│ │    └─ Return tagged integer                                         │   │
 │ └──────────────────────────────────────────────────────────────────────┘   │
 │                                                                              │
 │ ┌──────────────────────────────────────────────────────────────────────┐   │
@@ -265,13 +267,37 @@ START: PathExplorer.exploreInteger("user_choice", 0, executor)
 END: Return List<PathRecord> with 5 paths
 ```
 
-## 3. Constraint Collection Timeline (Single Iteration)
+## 3. Vitruvius Reaction Flow (NEW - Tag Creation in Reactions)
+
+```
+┌────────────────────────────────────────────────────────────────────────┐
+│                     Vitruvius Reaction Execution                         │
+│                                                                          │
+│  1. UserInteraction.startInteraction() returns concrete value           │
+│       ↓                                                                 │
+│  2. Reaction calls GaletteSymbolicator.getOrMakeSymbolicInt()          │
+│       - qualifiedName: "CreateAscetTaskRoutine:execute:userChoice"      │
+│       - Creates tag on first iteration                                  │
+│       - Reuses tag on subsequent iterations                            │
+│       - Adds domain constraint [min, max]                              │
+│       ↓                                                                 │
+│  3. Tagged value returned to reaction                                   │
+│       ↓                                                                 │
+│  4. Reaction calls SymbolicComparison.symbolicVitruviusChoice()        │
+│       - Records switch constraint for specific choice                   │
+│       - Uses qualified name from tag                                    │
+│       ↓                                                                 │
+│  5. Reaction executes appropriate transformation                        │
+└────────────────────────────────────────────────────────────────────────┘
+```
+
+## 4. Constraint Collection Timeline (Single Iteration)
 
 ```
 Time  Event                          Location                           PC State
 ─────────────────────────────────────────────────────────────────────────────────────
-T0    Create tagged Integer          PathExplorer:69                    []
-      GaletteSymbolicator.tagInteger(0, "user_choice")
+T0    Pass concrete value           PathExplorer:69                    []
+      executor.execute(0)  (no tagging yet)
 
 T1    Reset PC                       PathExplorer:71                    []
       PathUtils.getCurPC().clear()

amalthea-acset-integration/consistency/src/main/java/mir/reactions/amalthea2ascet/Amalthea2ascetChangePropagationSpecification.java

@@ -8,10 +8,6 @@
 import tools.vitruv.dsls.reactions.runtime.state.ReactionExecutionState;
 import tools.vitruv.dsls.reactions.runtime.structure.ReactionsImportPath;
 
-/**
- * Generated Java Code from Reactions DSL.
- *
- */
 @SuppressWarnings("all")
 public class Amalthea2ascetChangePropagationSpecification extends AbstractReactionsChangePropagationSpecification
         implements ChangePropagationSpecification {