# Tlaplus Add Variable

> Add a new variable to an existing TLA+ specification without changing its semantics. Ensures the variable is declared, initialized, and added to all UNCHANGED statements. Use when the user asks to add, introduce, or declare a new variable in a TLA+ spec, or mentions UNCHANGED statements.

- **Type:** Skill
- **Install:** `agentstack add skill-tlaplus-agentskills-tlaplus-add-variable`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [tlaplus](https://agentstack.voostack.com/s/tlaplus)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [tlaplus](https://github.com/tlaplus)
- **Source:** https://github.com/tlaplus/AgentSkills/tree/main/skills/tlaplus-add-variable

## Install

```sh
agentstack add skill-tlaplus-agentskills-tlaplus-add-variable
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# 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:

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

### Step 3: Initialize in Init

Add initialization. Match the style of existing initializations:

```tla
Init ==
    /\ existingVar1 = ...
    /\ existingVar2 = ...
    /\ newVar = 
```

### Step 4: Update All UNCHANGED Statements

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

```tla
\* 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:

```tla
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:

```tla
\* 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:

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

### Nested Disjunctions

Actions with `\/` may have UNCHANGED in each branch:

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

## Example

Adding `debug_log` variable to track operations:

**Before:**
```tla
VARIABLE state, counter

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

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

vars == >
```

**After:**
```tla
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](https://github.com/tlaplus)
- **Source:** [tlaplus/AgentSkills](https://github.com/tlaplus/AgentSkills)
- **License:** MIT

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

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-tlaplus-agentskills-tlaplus-add-variable
- Seller: https://agentstack.voostack.com/s/tlaplus
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.