quint icon indicating copy to clipboard operation
quint copied to clipboard

Estimate the number of visited states in the simulator

Open konnov opened this issue 1 year ago • 0 comments

This is a more useful coverage estimate asked for in #1067. We could store the hashes of the states visited by the simulator and print out the number of visited states. Moreover, we could prune the search when we visit a previously visited state, similar to stateful model checking.

This will not give us a qualitative guarantee of spec correctness, since it would not be exhaustive state exploration (the way it is implemented in TLC), but if the user observes that simulations of N runs and 10*N runs produce roughly the same number of visited states, they can conclude that the simulation was good enough and it does not make sense to increase the number of runs. This is all given that the simulator is doing random execution, so it can only give us estimates.

There are some technical challenges in implementing this approach, since the simulator is written in TypeScript. We will have to figure out how store large bitvectors, e.g., 1G large. This does not seem to be anything JavaScript/TypeScript were designed for, but we can try to do it in AssemblyScript, which seem to be ok with performance computations in Wasm.

I would estimate this to be 1-2 weeks.

konnov avatar Jul 21 '23 10:07 konnov