Visualize simulations coverage metrics

[lemmy]

Simulation is the only viable approach for checking very large specifications. However, evaluating the coverage of simulation remains challenging. Recent TLC improvements (https://github.com/tlaplus/tlaplus/commit/05d755591382ce1a574142b004e918074807c23f, https://github.com/tlaplus/tlaplus/commit/f764fbf321340298151c6b5e40892619116a12c4, https://github.com/tlaplus/tlaplus/commit/52f54453775dd3a11d4444cc657a2b8a506c802a, https://github.com/tlaplus/tlaplus/commit/84ac43463380ee6ceb02b245c63d223adaaf0b1b, https://github.com/tlaplus/tlaplus/commit/23f765078cd098a2bc2bc3d19889ba0c64583ca4, https://github.com/tlaplus/tlaplus/pull/897, ...) enable the simulator to generate relevant data with minimal overhead. The data provides detailed statistics, including the frequency of each action during the simulation run. Additionally, it reports the number of distinct states as well as the distinct values observed for each variable. Below is the `TLCGet("stats") output of some spec that has been periodically serialized and appended to a ndjson file:

{"traces":34008,"duration":60,"generated":4494285,"behavior":{"actions":{},"id":34001},"worker":0,"distinct":114033,"distinctvalues":{"view":12906,"byzActions":3,"byzCommitIndex":815,"log":46310,"crashCommitIndex":2875,"viewStable":7,"prepareQC":11881,"primary":11,"network":132576},"retries":1072284,"actions":{"ByzPrimaryEquivocate":718,"ReceiveNewView":1345,"TLCInit":3863,"DiscardMessage":35400,"ByzOmitEntries":1039,"ReceiveVote":19495,"ReceiveEntries":22039,"BecomePrimary":2211,"SendEntries":15310,"SIMTimeout":39448},"levelmean":40,"levelvariance":3598}
{"traces":55070,"duration":120,"generated":7731406,"behavior":{"actions":{},"id":55045},"worker":0,"distinct":197538,"distinctvalues":{"view":15302,"byzActions":3,"byzCommitIndex":1507,"log":100942,"crashCommitIndex":5987,"viewStable":7,"prepareQC":24650,"primary":11,"network":228738},"retries":1916909,"actions":{"ByzPrimaryEquivocate":1253,"ReceiveNewView":1658,"TLCInit":6476,"DiscardMessage":45686,"ByzOmitEntries":1881,"ReceiveVote":46795,"ReceiveEntries":52333,"BecomePrimary":2747,"SendEntries":34179,"SIMTimeout":50139},"levelmean":40,"levelvariance":3599}
{"traces":73621,"duration":180,"generated":10719760,"behavior":{"actions":{},"id":73603},"worker":0,"distinct":285915,"distinctvalues":{"view":16531,"byzActions":3,"byzCommitIndex":1960,"log":157986,"crashCommitIndex":8146,"viewStable":7,"prepareQC":36543,"primary":11,"network":305309},"retries":2688213,"actions":{"ByzPrimaryEquivocate":1698,"ReceiveNewView":1820,"TLCInit":8732,"DiscardMessage":51342,"ByzOmitEntries":2573,"ReceiveVote":73822,"ReceiveEntries":82462,"BecomePrimary":3052,"SendEntries":53313,"SIMTimeout":56217},"levelmean":40,"levelvariance":3599}
{"traces":91259,"duration":240,"generated":13621215,"behavior":{"actions":{},"id":91246},"worker":0,"distinct":408069,"distinctvalues":{"view":17197,"byzActions":3,"byzCommitIndex":2849,"log":222994,"crashCommitIndex":10350,"viewStable":7,"prepareQC":46790,"primary":11,"network":399602},"retries":3451052,"actions":{"ByzPrimaryEquivocate":2183,"ReceiveNewView":1972,"TLCInit":10931,"DiscardMessage":55897,"ByzOmitEntries":3259,"ReceiveVote":101518,"ReceiveEntries":112795,"BecomePrimary":3288,"SendEntries":72996,"SIMTimeout":60832},"levelmean":40,"levelvariance":3599}
{"traces":108707,"duration":300,"generated":16505833,"behavior":{"actions":{},"id":108691},"worker":0,"distinct":475861,"distinctvalues":{"view":17707,"byzActions":3,"byzCommitIndex":3261,"log":286325,"crashCommitIndex":11558,"viewStable":8,"prepareQC":55935,"primary":11,"network":488048},"retries":4215577,"actions":{"ByzPrimaryEquivocate":2593,"ReceiveNewView":2095,"TLCInit":13113,"DiscardMessage":59892,"ByzOmitEntries":3930,"ReceiveVote":129800,"ReceiveEntries":143794,"BecomePrimary":3507,"SendEntries":92792,"SIMTimeout":65029},"levelmean":40,"levelvariance":3600}
{"traces":143730,"duration":360,"generated":21148903,"behavior":{"actions":{},"id":143712},"worker":0,"distinct":617491,"distinctvalues":{"view":25658,"byzActions":3,"byzCommitIndex":3416,"log":326387,"crashCommitIndex":11835,"viewStable":9,"prepareQC":59906,"primary":11,"network":622257},"retries":5321678,"actions":{"ByzPrimaryEquivocate":3386,"ReceiveNewView":3437,"TLCInit":17049,"DiscardMessage":97038,"ByzOmitEntries":4937,"ReceiveVote":149567,"ReceiveEntries":165896,"BecomePrimary":5869,"SendEntries":108035,"SIMTimeout":106604},"levelmean":40,"levelvariance":3600}
{"traces":165211,"duration":420,"generated":24433212,"behavior":{"actions":{},"id":165203},"worker":0,"distinct":694114,"distinctvalues":{"view":27429,"byzActions":3,"byzCommitIndex":3690,"log":380037,"crashCommitIndex":13507,"viewStable":9,"prepareQC":66216,"primary":11,"network":723477},"retries":6163977,"actions":{"ByzPrimaryEquivocate":4000,"ReceiveNewView":3769,"TLCInit":19689,"DiscardMessage":107570,"ByzOmitEntries":5680,"ReceiveVote":176642,"ReceiveEntries":195457,"BecomePrimary":6413,"SendEntries":126777,"SIMTimeout":117604},"levelmean":40,"levelvariance":3600}
{"traces":183742,"duration":480,"generated":27425643,"behavior":{"actions":{},"id":183741},"worker":0,"distinct":805771,"distinctvalues":{"view":28363,"byzActions":3,"byzCommitIndex":3962,"log":431900,"crashCommitIndex":14709,"viewStable":9,"prepareQC":72556,"primary":11,"network":815484},"retries":6948086,"actions":{"ByzPrimaryEquivocate":4549,"ReceiveNewView":3973,"TLCInit":22009,"DiscardMessage":113791,"ByzOmitEntries":6361,"ReceiveVote":203984,"ReceiveEntries":225983,"BecomePrimary":6727,"SendEntries":146346,"SIMTimeout":124126},"levelmean":40,"levelvariance":3600}
{"traces":201383,"duration":540,"generated":30332605,"behavior":{"actions":{},"id":201359},"worker":0,"distinct":888312,"distinctvalues":{"view":28975,"byzActions":3,"byzCommitIndex":4179,"log":485666,"crashCommitIndex":16319,"viewStable":9,"prepareQC":77091,"primary":11,"network":892538},"retries":7714189,"actions":{"ByzPrimaryEquivocate":4964,"ReceiveNewView":4104,"TLCInit":24233,"DiscardMessage":118267,"ByzOmitEntries":7063,"ReceiveVote":231933,"ReceiveEntries":257258,"BecomePrimary":6940,"SendEntries":165917,"SIMTimeout":128824},"levelmean":40,"levelvariance":3600}

Using the (serialized) data, users can manually create various statistics and plots to visualize the simulator's coverage (examples of such plots are available at https://github.com/microsoft/CCF/issues/6537#issuecomment-2398295103). An earlier prototype even automatically regenerated the plot during simulation (https://www.youtube.com/watch?v=btikdh4xZQ0). I propose that the TLA+ VSCode extension should automatically generate these plots from the ndjson file and display them, for instance, within the model checking view.

Technology candidates

• https://github.com/kroitor/asciichart
• https://marketplace.visualstudio.com/items?itemName=fizzybreezy.gnuplot
• https://www.visidata.org