tlaplus-add-variable

Add Variable to TLA+ Specification

Add a new variable to a TLA+ specification while preserving semantics. The new variable must appear in all necessary locations so the specification remains valid and its behavior is unchanged.

Required Locations for New Variables

When adding a variable newVar to a TLA+ specification, update these locations:

1. VARIABLE declaration block - Add the variable name
2. Init - Initialize the variable
3. All UNCHANGED statements - Add variable to every UNCHANGED that doesn't modify it
4. vars tuple - Add to the tuple used in temporal formulas (if exists)
5. TypeOk (optional) - Add type constraint if TypeOk invariant exists

Workflow

Step 1: Analyze the Specification

Read the TLA+ file and identify:

• All existing variables in the VARIABLE block
• The Init predicate
• All actions and their UNCHANGED statements
• The vars tuple or similardefinition (usually near Next or Spec)
• TypeOk invariant if present

Step 2: Add Variable Declaration

Add the new variable to the VARIABLE block. Preserve formatting:

VARIABLE
    existingVar1,
    existingVar2,
    newVar  \* Add with comment explaining purpose

Step 3: Initialize in Init

Add initialization. Match the style of existing initializations:

Init ==
    /\ existingVar1 = ...
    /\ existingVar2 = ...
    /\ newVar = <initial_value>

Step 4: Update All UNCHANGED Statements

Critical step. Find every UNCHANGED statement and add the new variable:

\* Before:
UNCHANGED << existingVar1, existingVar2 >>

\* After:
UNCHANGED << existingVar1, existingVar2, newVar >>

Search patterns to find UNCHANGED statements:

• UNCHANGED << - tuple form
• UNCHANGED followed by variable name - single variable form

For single-variable UNCHANGED, convert to tuple form:

\* Before:
UNCHANGED existingVar

\* After:
UNCHANGED << existingVar, newVar >>

Step 5: Update vars Tuple

If a vars tuple exists, add the new variable: