Repair TLA+ ordered serialisability invariant - #8134

Open

Amaury Chamayou (achamayou) wants to merge 11 commits into

microsoft:mainfrom

achamayou:tla-ordered-serializable-counterexample

Commits on Aug 9, 2026

Document TLA+ ordered serialisability counterexample

Amaury Chamayou (achamayou)
and
Copilot
committed
22802ef
Clarify expected TLC invariant failure

Amaury Chamayou (achamayou)
and
Copilot
committed
a77529d
Add trace-backed counterexample diagrams

Amaury Chamayou (achamayou)
and
Copilot
committed
f9952a6
Clarify counterexample diagrams

Amaury Chamayou (achamayou)
and
Copilot
committed
27116d2
Replace counterexample diagrams with linear trace

Amaury Chamayou (achamayou)
and
Copilot
committed
a9d1815

Commits on Aug 10, 2026

Repair ordered serialisability invariant

Amaury Chamayou (achamayou)
and
Copilot
committed
c0330a2
Merge branch 'main' into tla-ordered-serializable-counterexample
Amaury Chamayou (achamayou)
authored
d99c7af
Add minimal ordered serialisability regression

Amaury Chamayou (achamayou)
and
Copilot
committed
5fcdf53

Commits on Aug 11, 2026

Merge branch 'main' into tla-ordered-serializable-counterexample
Amaury Chamayou (achamayou)
authored
0a7324b

Commits on Aug 12, 2026