Lighthearted: TLA+ Syntax Puzzle

38 views

Skip to first unread message

Andrew Helwer

unread,

Apr 22, 2024, 1:48:54 PM4/22/24

to tlaplus

Lighthearted challenge - explain why this is valid TLA+ syntax:

---- MODULE Test ----

op == !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!(1,2)

====

(can be extended ad-infinitum with 3n+2 exclamation points)

Yes I know the SANY syntax checker doesn't handle this (due to a bug arguably) and you wouldn't be able to construct a spec that passes checking at the semantic level. But still! Infinite exclamation marks!