Checking temporal properties (2 quick questions)

[Shane Miller]

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

[Andrew Helwer]

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

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/8e6fb5b6-f275-44f3-be5c-172aed4a86een%40googlegroups.com.

[Shane Miller]

Thank you for your reply

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWJU8ew-Msq0FnfQoKFyrrNp_2BqmJEOa%3DOgjyw7-u4bg%40mail.gmail.com.