learning_tla/lamport_video/specs/maximum.tla
2025-02-12 18:19:37 +01:00

7 lines
115 B
Text

---- MODULE maximum ----
Maximum(S) ==
IF S = {}
THEN -1
ELSE CHOOSE n \in S: \A m \in S: n >= m
====