Skip to content

Commit 774f8de

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: add tlaiser state machine specs for config validation pipeline
Models StageExecution (pending/cache-hit/running/succeeded/failed/ skipped) and CacheEntry (absent/fresh/stale) with TLA+ safety properties for pipeline determinism and cache invalidation. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 67b9b0f commit 774f8de

File tree

9 files changed

+532
-0
lines changed

9 files changed

+532
-0
lines changed

‎generated/tlaiser/CacheEntry.cfg‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
\* TLC Configuration for CacheEntry
2+
\* Generated by tlaiser
3+
4+
SPECIFICATION FairSpec
5+
6+
\* State constants as model values
7+
CONSTANT Absent = Absent
8+
CONSTANT Fresh = Fresh
9+
CONSTANT Stale = Stale
10+
11+
\* Type invariant
12+
INVARIANT TypeInvariant
13+
14+
\* Safety properties (invariants)
15+
INVARIANT SucceededStageNeverReruns
16+
INVARIANT FailedStagePropagates
17+
18+
\* Liveness and fairness properties
19+
PROPERTY PipelineEventuallyTerminates
20+

‎generated/tlaiser/CacheEntry.tla‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
---- MODULE CacheEntry ----
2+
\* Cache entry lifecycle for a pipeline stage result. Entries are keyed by content hash or mtime.
3+
\* Generated by tlaiser — https://github.com/hyperpolymath/tlaiser
4+
5+
EXTENDS Naturals, Sequences, TLC
6+
7+
\* State constants — each represents a distinct state
8+
CONSTANTS Absent, Fresh, Stale
9+
10+
\* Variables tracked by this specification
11+
VARIABLES state, invalidation_policy
12+
13+
\* Type invariant: state is always one of the declared states
14+
TypeInvariant == state \in {Absent, Fresh, Stale}
15+
16+
\* Initial state predicate
17+
Init ==
18+
/\ state = Absent
19+
/\ invalidation_policy = 0
20+
21+
\* Transition actions
22+
\* Transition: Absent -> Fresh (store_result)
23+
store_result ==
24+
/\ state = Absent
25+
/\ state' = Fresh
26+
/\ UNCHANGED invalidation_policy
27+
28+
\* Transition: Fresh -> Stale (content_hash_changed)
29+
content_hash_changed ==
30+
/\ state = Fresh
31+
/\ invalidation_policy = 0
32+
/\ state' = Stale
33+
/\ UNCHANGED invalidation_policy
34+
35+
\* Transition: Fresh -> Stale (mtime_changed)
36+
mtime_changed ==
37+
/\ state = Fresh
38+
/\ invalidation_policy = 1
39+
/\ state' = Stale
40+
/\ UNCHANGED invalidation_policy
41+
42+
\* Transition: Stale -> Fresh (store_new_result)
43+
store_new_result ==
44+
/\ state = Stale
45+
/\ state' = Fresh
46+
/\ UNCHANGED invalidation_policy
47+
48+
\* Transition: Fresh -> Absent (cache_clear)
49+
cache_clear ==
50+
/\ state = Fresh
51+
/\ state' = Absent
52+
/\ UNCHANGED invalidation_policy
53+
54+
\* Transition: Stale -> Absent (cache_clear)
55+
cache_clear ==
56+
/\ state = Stale
57+
/\ state' = Absent
58+
/\ UNCHANGED invalidation_policy
59+
60+
\* Next-state relation: disjunction of all transitions
61+
Next ==
62+
\/ store_result
63+
\/ content_hash_changed
64+
\/ mtime_changed
65+
\/ store_new_result
66+
\/ cache_clear
67+
\/ cache_clear
68+
69+
\* All variables tuple (for stuttering)
70+
vars == <<state, invalidation_policy>>
71+
72+
\* Complete specification
73+
Spec == Init /\ [][Next]_vars
74+
75+
\* Fair specification (with weak fairness on Next)
76+
FairSpec == Spec /\ WF_vars(Next)
77+
78+
\* ---- Temporal Properties ----
79+
\* Property: SucceededStageNeverReruns (safety)
80+
SucceededStageNeverReruns == []([][StageExecution = Succeeded => UNCHANGED StageExecution]_StageExecution)
81+
82+
\* Property: FailedStagePropagates (safety)
83+
FailedStagePropagates == []([](StageExecution = Failed => allow_failure = FALSE))
84+
85+
\* Property: PipelineEventuallyTerminates (liveness)
86+
PipelineEventuallyTerminates == <>(<>(StageExecution = Succeeded \/ StageExecution = Failed \/ StageExecution = Skipped))
87+
88+
89+
====

‎generated/tlaiser/CacheEntryPlusCal.tla‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
---- MODULE CacheEntryPlusCal ----
2+
\* Cache entry lifecycle for a pipeline stage result. Entries are keyed by content hash or mtime.
3+
\* PlusCal version — generated by tlaiser
4+
\* https://github.com/hyperpolymath/tlaiser
5+
6+
EXTENDS Naturals, Sequences, TLC
7+
8+
CONSTANTS Absent, Fresh, Stale
9+
10+
(* --fair algorithm CacheEntry
11+
variables
12+
state = Absent;
13+
invalidation_policy = 0;
14+
begin
15+
MainLoop:
16+
while TRUE do
17+
either
18+
\* store_result
19+
await state = Absent;
20+
state := Fresh;
21+
or
22+
await state = Fresh;
23+
either
24+
await invalidation_policy = 0;
25+
state := Stale;
26+
or
27+
await invalidation_policy = 1;
28+
state := Stale;
29+
or
30+
state := Absent;
31+
end either;
32+
or
33+
await state = Stale;
34+
either
35+
state := Fresh;
36+
or
37+
state := Absent;
38+
end either;
39+
end either;
40+
end while;
41+
end algorithm; *)
42+
43+
\* BEGIN TRANSLATION
44+
\* (PlusCal translator will insert TLA+ here)
45+
\* END TRANSLATION
46+
47+
\* ---- Temporal Properties ----
48+
\* Property: SucceededStageNeverReruns (safety)
49+
SucceededStageNeverReruns == []([][StageExecution = Succeeded => UNCHANGED StageExecution]_StageExecution)
50+
51+
\* Property: FailedStagePropagates (safety)
52+
FailedStagePropagates == []([](StageExecution = Failed => allow_failure = FALSE))
53+
54+
\* Property: PipelineEventuallyTerminates (liveness)
55+
PipelineEventuallyTerminates == <>(<>(StageExecution = Succeeded \/ StageExecution = Failed \/ StageExecution = Skipped))
56+
57+
====

‎generated/tlaiser/StageExecution.cfg‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
\* TLC Configuration for StageExecution
2+
\* Generated by tlaiser
3+
4+
SPECIFICATION FairSpec
5+
6+
\* State constants as model values
7+
CONSTANT Pending = Pending
8+
CONSTANT CacheHit = CacheHit
9+
CONSTANT Running = Running
10+
CONSTANT Succeeded = Succeeded
11+
CONSTANT Failed = Failed
12+
CONSTANT Skipped = Skipped
13+
14+
\* Type invariant
15+
INVARIANT TypeInvariant
16+
17+
\* Safety properties (invariants)
18+
INVARIANT SucceededStageNeverReruns
19+
INVARIANT FailedStagePropagates
20+
21+
\* Liveness and fairness properties
22+
PROPERTY PipelineEventuallyTerminates
23+

‎generated/tlaiser/StageExecution.tla‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
---- MODULE StageExecution ----
2+
\* Lifecycle of a single pipeline stage during execution. Includes cache lookup, execution, and allow_failure handling.
3+
\* Generated by tlaiser — https://github.com/hyperpolymath/tlaiser
4+
5+
EXTENDS Naturals, Sequences, TLC
6+
7+
\* State constants — each represents a distinct state
8+
CONSTANTS Pending, CacheHit, Running, Succeeded, Failed, Skipped
9+
10+
\* Variables tracked by this specification
11+
VARIABLES state, allow_failure, cache_enabled
12+
13+
\* Type invariant: state is always one of the declared states
14+
TypeInvariant == state \in {Pending, CacheHit, Running, Succeeded, Failed, Skipped}
15+
16+
\* Initial state predicate
17+
Init ==
18+
/\ state = Pending
19+
/\ allow_failure = FALSE
20+
/\ cache_enabled = TRUE
21+
22+
\* Transition actions
23+
\* Transition: Pending -> Skipped (dry_run_or_condition_false)
24+
dry_run_or_condition_false ==
25+
/\ state = Pending
26+
/\ state' = Skipped
27+
/\ UNCHANGED <<allow_failure, cache_enabled>>
28+
29+
\* Transition: Pending -> CacheHit (cache_lookup_hit)
30+
cache_lookup_hit ==
31+
/\ state = Pending
32+
/\ cache_enabled = TRUE
33+
/\ state' = CacheHit
34+
/\ UNCHANGED <<allow_failure, cache_enabled>>
35+
36+
\* Transition: Pending -> Running (cache_miss_or_disabled)
37+
cache_miss_or_disabled ==
38+
/\ state = Pending
39+
/\ state' = Running
40+
/\ UNCHANGED <<allow_failure, cache_enabled>>
41+
42+
\* Transition: CacheHit -> Succeeded (cache_result_applied)
43+
cache_result_applied ==
44+
/\ state = CacheHit
45+
/\ state' = Succeeded
46+
/\ UNCHANGED <<allow_failure, cache_enabled>>
47+
48+
\* Transition: Running -> Succeeded (executor_succeeds)
49+
executor_succeeds ==
50+
/\ state = Running
51+
/\ state' = Succeeded
52+
/\ UNCHANGED <<allow_failure, cache_enabled>>
53+
54+
\* Transition: Running -> Failed (executor_fails)
55+
executor_fails ==
56+
/\ state = Running
57+
/\ allow_failure = FALSE
58+
/\ state' = Failed
59+
/\ UNCHANGED <<allow_failure, cache_enabled>>
60+
61+
\* Transition: Running -> Succeeded (executor_fails_but_allowed)
62+
executor_fails_but_allowed ==
63+
/\ state = Running
64+
/\ allow_failure = TRUE
65+
/\ state' = Succeeded
66+
/\ UNCHANGED <<allow_failure, cache_enabled>>
67+
68+
\* Next-state relation: disjunction of all transitions
69+
Next ==
70+
\/ dry_run_or_condition_false
71+
\/ cache_lookup_hit
72+
\/ cache_miss_or_disabled
73+
\/ cache_result_applied
74+
\/ executor_succeeds
75+
\/ executor_fails
76+
\/ executor_fails_but_allowed
77+
78+
\* All variables tuple (for stuttering)
79+
vars == <<state, allow_failure, cache_enabled>>
80+
81+
\* Complete specification
82+
Spec == Init /\ [][Next]_vars
83+
84+
\* Fair specification (with weak fairness on Next)
85+
FairSpec == Spec /\ WF_vars(Next)
86+
87+
\* ---- Temporal Properties ----
88+
\* Property: SucceededStageNeverReruns (safety)
89+
SucceededStageNeverReruns == []([][StageExecution = Succeeded => UNCHANGED StageExecution]_StageExecution)
90+
91+
\* Property: FailedStagePropagates (safety)
92+
FailedStagePropagates == []([](StageExecution = Failed => allow_failure = FALSE))
93+
94+
\* Property: PipelineEventuallyTerminates (liveness)
95+
PipelineEventuallyTerminates == <>(<>(StageExecution = Succeeded \/ StageExecution = Failed \/ StageExecution = Skipped))
96+
97+
98+
====

‎generated/tlaiser/StageExecutionPlusCal.tla‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
---- MODULE StageExecutionPlusCal ----
2+
\* Lifecycle of a single pipeline stage during execution. Includes cache lookup, execution, and allow_failure handling.
3+
\* PlusCal version — generated by tlaiser
4+
\* https://github.com/hyperpolymath/tlaiser
5+
6+
EXTENDS Naturals, Sequences, TLC
7+
8+
CONSTANTS Pending, CacheHit, Running, Succeeded, Failed, Skipped
9+
10+
(* --fair algorithm StageExecution
11+
variables
12+
state = Pending;
13+
allow_failure = FALSE;
14+
cache_enabled = TRUE;
15+
begin
16+
MainLoop:
17+
while TRUE do
18+
either
19+
await state = Pending;
20+
either
21+
state := Skipped;
22+
or
23+
await cache_enabled = TRUE;
24+
state := CacheHit;
25+
or
26+
state := Running;
27+
end either;
28+
or
29+
\* cache_result_applied
30+
await state = CacheHit;
31+
state := Succeeded;
32+
or
33+
await state = Running;
34+
either
35+
state := Succeeded;
36+
or
37+
await allow_failure = FALSE;
38+
state := Failed;
39+
or
40+
await allow_failure = TRUE;
41+
state := Succeeded;
42+
end either;
43+
end either;
44+
end while;
45+
end algorithm; *)
46+
47+
\* BEGIN TRANSLATION
48+
\* (PlusCal translator will insert TLA+ here)
49+
\* END TRANSLATION
50+
51+
\* ---- Temporal Properties ----
52+
\* Property: SucceededStageNeverReruns (safety)
53+
SucceededStageNeverReruns == []([][StageExecution = Succeeded => UNCHANGED StageExecution]_StageExecution)
54+
55+
\* Property: FailedStagePropagates (safety)
56+
FailedStagePropagates == []([](StageExecution = Failed => allow_failure = FALSE))
57+
58+
\* Property: PipelineEventuallyTerminates (liveness)
59+
PipelineEventuallyTerminates == <>(<>(StageExecution = Succeeded \/ StageExecution = Failed \/ StageExecution = Skipped))
60+
61+
====

‎generated/tlaiser/run_tlc_CacheEntry.sh‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
# TLC run script for CacheEntry — generated by tlaiser
4+
# https://github.com/hyperpolymath/tlaiser
5+
#
6+
# Prerequisites:
7+
# - Java runtime (>= 11)
8+
# - tla2tools.jar on CLASSPATH or in current directory
9+
# - Or: install Community TLA+ Toolbox
10+
11+
set -euo pipefail
12+
13+
# Locate TLA+ tools
14+
TLA2TOOLS="${TLA2TOOLS:-tla2tools.jar}"
15+
if [[ ! -f "$TLA2TOOLS" ]]; then
16+
echo "Error: tla2tools.jar not found. Set TLA2TOOLS env var or download from:"
17+
echo " https://github.com/tlaplus/tlaplus/releases"
18+
exit 1
19+
fi
20+
21+
echo "Running TLC on CacheEntry.tla ..."
22+
java -XX:+UseParallelGC -Xmx4g -jar "$TLA2TOOLS" -workers 4 -config CacheEntry.cfg CacheEntry.tla
23+
24+
echo "TLC completed."

0 commit comments

Comments
 (0)