Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Estimate the number of visited states in the simulator #1069

Open
konnov opened this issue Jul 21, 2023 · 0 comments
Open

Estimate the number of visited states in the simulator #1069

konnov opened this issue Jul 21, 2023 · 0 comments
Labels
simulator Quint simulator usability Usability issues

Comments

@konnov
Copy link
Contributor

konnov commented Jul 21, 2023

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 konnov added W8 usability Usability issues simulator Quint simulator labels Jul 21, 2023
@shonfeder shonfeder removed the W8 label Jan 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
simulator Quint simulator usability Usability issues
Projects
None yet
Development

No branches or pull requests

2 participants