You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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 and10*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.
The text was updated successfully, but these errors were encountered: