requirement-to-tlaplus-property-generator

Requirement to TLA+ Property Generator

Overview

This skill transforms natural-language requirements into formal TLA+ properties, enabling rigorous verification of system specifications. It handles invariants, safety properties, and liveness properties, resolving ambiguities and seeking clarification when needed.

Workflow

Step 1: Analyze the Requirement

Parse and understand the input requirement:

1. Identify requirement type:

   • Invariant: "The system always maintains property P"
   • Safety: "Bad thing X never happens"
   • Liveness: "Good thing Y eventually happens"
   • Fairness: "Process Z gets a fair chance"

2. Extract key elements:

   • State variables involved
   • Conditions and constraints
   • Temporal aspects (always, eventually, until, etc.)
   • Quantifiers (for all, exists)

3. Detect ambiguities:

   • Undefined terms or variables
   • Unclear temporal scope
   • Missing boundary conditions
   • Implicit assumptions

Step 2: Resolve Ambiguities

When ambiguities are detected, use one of these strategies:

Strategy A: Reasonable Interpretation If the ambiguity has a standard interpretation in the domain, resolve it automatically and document the assumption.

Example:

• Requirement: "The buffer never overflows"
• Interpretation: "buffer_size <= MAX_BUFFER_SIZE" (assuming MAX_BUFFER_SIZE is defined)

Strategy B: Ask Clarifying Questions For critical or non-obvious ambiguities, ask the user:

• "Does 'eventually' mean within a bounded time or unbounded?"
• "Should this property hold for all processes or just specific ones?"
• "What is the initial state assumption?"

See references/clarification_patterns.md for common question templates.

Step 3: Map to TLA+ Constructs

Translate the requirement into TLA+ syntax:

Invariants (Type Invariant or State Predicate):

TypeOK == /\ var1 \in ValidSet1
          /\ var2 \in ValidSet2
          /\ condition

StateInvariant == predicate_over_state_variables