Re: [tlaplus] Describing unless condition in lisp

Hi Marta,

If you'd like, we can set up a video call to chat about your interest in TLA+ and what sort of problems you are looking to solve with it! You can reply directly to this message (not to the wider group) to set something up.

Andrew Helwer

On Tue, Mar 17, 2026 at 7:46 AM marta zhango <martazhango@xxxxxxxxx> wrote:

I have the following lisp code, which I want to describe in TLA.

(unless (and actm (not (eq actm 'go)))
;; Insert M newlines after label (default 0).
;; The first newline ends the label line itself
(dotimes (_ (1+ (or m 0))) (insert "\n"))) )

Came up with this but still now to this and unsure about correctness

(unless COND &rest BODY) If COND yields nil, do BODY.
LET: \not actm \imlp actm unspecified or nil
\knj means conjunction
\dsj means disjunction
ACTION: \knj \not COND
\knj \not (actm \knj \not (actm = 'go))
\knj \not actm \dsj actm = 'go
\knj actm = (unspecified, 'go)

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/c929677a-a59c-475c-a753-9090dabd6803n%40googlegroups.com.