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

Simulator wastes a lot of resources computing states that won't be used #1552

Open
bugarela opened this issue Nov 14, 2024 · 0 comments
Open

Comments

@bugarela
Copy link
Collaborator

When there is an any, Quint simulator will do the following:

  1. Execute all actions and save the result and the state after that action
  2. Filter out actions for which the result is false (i.e. pre-conditions not satisfied)
  3. From the remaining actions, randomly pick one
  4. Take the state from the picked action to be the next state in the simulation and proceed

This means that we can compute a bunch of stuff in 1 that will never be used.

I need to think if this won't affect the probability distribution too much, but an alternative approach would be:

  1. pick an action
  2. execute it. If the result is false, try the next one
  3. if we get back to the picked action, the result of any is false

This would also mean we would make a rand() call even on deterministic anys (that is, with disjoint pre-conditions). But I think is would be a much smaller problem than the performance issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant