I've also opened https://github.com/tlaplus/tlaplus/pull/1016 to print the initial entry on this table. Thankfully the regex is able to handle the slightly different log line produced by the simulator output, so no additional changes were needed. Please let me know if this is the correct expectation for that ticket!
Tested with the spec from that ticket and run with "Check model with tlc" and additional parameters: -fpmem 0.9 -simulate -checkpoint 10.
Fixes #324.
I've also opened https://github.com/tlaplus/tlaplus/pull/1016 to print the initial entry on this table. Thankfully the regex is able to handle the slightly different log line produced by the simulator output, so no additional changes were needed. Please let me know if this is the correct expectation for that ticket! Tested with the spec from that ticket and run with "Check model with tlc" and additional parameters:
-fpmem 0.9 -simulate -checkpoint 10.