Re: [tlaplus] Checking temporal properties (2 quick questions)

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Liveness checking is single-threaded, although multi-threaded liveness checking is a long-wished-for feature. Adding workers only affects regular safety checking.

I don't believe there is currently any way to display percentage completion of liveness checking, although if liveness checking is done after safety checking when the entire state graph is known there should in principle be a way to derive some measure of completion percentage.

Andrew

On Thu, Oct 23, 2025 at 11:40 AM Shane Miller <gshanemiller6@xxxxxxxxx> wrote:

TLA's default model eval method is breadth-first, 1 worker per core. 

(1) But is temporal property checking MT or this check single-threaded? i.e. do more workers make checking temporal properties go faster?

(2) Is there anyway to know percent complete when cheking temporal properties?

Regards

--
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/8e6fb5b6-f275-44f3-be5c-172aed4a86een%40googlegroups.com.

-- 
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/CABj%3DxUWJU8ew-Msq0FnfQoKFyrrNp_2BqmJEOa%3DOgjyw7-u4bg%40mail.gmail.com.