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 = 

Step 4: Update All UNCHANGED Statements

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

\* Before:
UNCHANGED >

\* After:
UNCHANGED >

Search patterns to find UNCHANGED statements:

• `UNCHANGED >

### Step 5: Update vars Tuple

If a `vars` tuple exists, add the new variable:

```tla
\* Before:
vars == >

\* After:
vars == >

Step 6: Update TypeOk (if exists)

Add type constraint for the new variable:

TypeOk ==
    /\ existingVar1 \in SomeSet
    /\ newVar \in ExpectedType

Verification Checklist

After making changes, verify:

• [ ] Variable declared in VARIABLE block
• [ ] Variable initialized in Init
• [ ] Variable added to ALL UNCHANGED statements (use grep to count)
• [ ] Variable added to vars tuple
• [ ] Variable has type constraint in TypeOk (if TypeOk exists)
• [ ] No action modifies the new variable (per task requirements)

Common Patterns

Per-Thread Variables

For variables indexed by thread/process:

\* Declaration
newVar,

\* Initialization
/\ newVar = [thread \in Threads |-> InitialValue]

\* In UNCHANGED (same as scalar variables)
UNCHANGED >

Conditional UNCHANGED

Some actions have conditional branches with different UNCHANGED statements. Update ALL branches:

Action(thread) ==
    IF condition
        THEN
            /\ ...
            /\ UNCHANGED >  \* Update this
        ELSE
            /\ ...
            /\ UNCHANGED >  \* AND this

Nested Disjunctions

Actions with \/ may have UNCHANGED in each branch:

Action(thread) ==
    \/  /\ guard1
        /\ UNCHANGED >  \* Each branch
    \/  /\ guard2
        /\ UNCHANGED >  \* needs update

Example

Adding debug_log variable to track operations:

Before:

VARIABLE state, counter

Init ==
    /\ state = "idle"
    /\ counter = 0

Increment ==
    /\ counter' = counter + 1
    /\ UNCHANGED state

vars == >

After:

VARIABLE state, counter, debug_log

Init ==
    /\ state = "idle"
    /\ counter = 0
    /\ debug_log = >

Increment ==
    /\ counter' = counter + 1
    /\ UNCHANGED >

vars == >

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: tlaplus
• Source: tlaplus/AgentSkills
• License: MIT

Install and usage instructions live in the source repository linked above.