Re: [tlaplus] Model based testing

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Yes, this would be the place to incorporate trace dumping into the simulation for formats other than TLA+. The majority of the infrastructure is already in place. In essence, you can follow the implementation of `-dumptrace`. In fact, calling `tool.checkPostConditionWithCounterExample(new CounterExample(curState));` from the for loop is almost sufficient.

I suggest that we move the technical discussion to an issue on GitHub at github.com/tlaplus/issues.

M.

> On Jul 22, 2025, at 2:51 PM, Anatoliy Bilenko <anatoliy.bilenko@xxxxxxxxx> wrote:
> 
> Also, I found this loop in TLC code which dumps the trace I expected to be dumped in JSON. 
> Is it worth adding a JSON output for dumps? Maybe, I can do it.


-- 
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/ECF34AAA-8099-4555-99CD-D39945982041%40lemmster.de.