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
Infinite generation of states #18
Comments
Hi @Nightcro. Thanks for reaching out and for trying the library! There should not be a problem using In the meantime, have you tried running this in the Explorer UI to manually explore some behavior paths? Sometimes that will reveal cases where a path continues to grow beyond what had been intended. BTW one temporary caveat w that debugging technique is that Explorer uses BFS, which consumes quite a lot more memory. |
@Nightcro, I had a chance to look into this today. The state space is large but finite. Here are some techniques for reducing the state space:
Those changes aren't sufficient to get the model checking time into a convenient range, and I think I need to make a library update. You're using |
Thank you for the response and your explanation |
This commmit addresses feature request #4 and should also help improve the performance for #18. Regarding the latter, using this feature my laptop is able to model check https://github.com/Nightcro/ble-stateright with 3 nodes, which it could not do prior. The data structure to support this is a bit more complex, so I anticipated additional per-state overhead, which might noticeably impact check time for models that do not take advantage of the possible state space reduction by assuming an ordered network for directed flows. Unfortunately at the moment, the performance difference is larger than anticipated as the `linearizable-register` example ends up with a larger state space for some reason. This needs to be resolved before the change is merged to the `master` branch. Before: == paxos check 6 == Done. states=18972647, unique=9357525, sec=16 Done. states=18972647, unique=9357525, sec=17 Done. states=18972647, unique=9357525, sec=18 == single-copy-register check 4 == Done. states=731789, unique=400233, sec=6 Done. states=731789, unique=400233, sec=6 Done. states=731789, unique=400233, sec=6 == linearizable-register check 2 == Done. states=194646243, unique=41138199, sec=78 Done. states=194646243, unique=41138199, sec=79 Done. states=194646243, unique=41138199, sec=79 After: == paxos check 6 == Done. states=18972647, unique=9357525, sec=19 Done. states=18972647, unique=9357525, sec=19 Done. states=18972647, unique=9357525, sec=19 == single-copy-register check 4 == Done. states=731789, unique=400233, sec=5 Done. states=731789, unique=400233, sec=5 Done. states=731789, unique=400233, sec=5 == linearizable-register check 2 == Done. states=955073804, unique=209614941, sec=455 Done. states=955073804, unique=209614941, sec=465 Done. states=955073804, unique=209614941, sec=469
@Nightcro Please see 41a861d for an upcoming feature that should dramatically reduce the state space in this example. The feature isn't yet ready for publishing (see details in the commit message), but you could pull the
If you hit any snags, just let me know, as I would be more than happy to send you a PR. |
This commmit addresses feature request #4 and should also help improve the performance for #18. Regarding the latter, using this feature my laptop is able to model check https://github.com/Nightcro/ble-stateright with 3 nodes, which it could not do prior. Performance is virtually identical. Before (includes the 2PC model for reference even though this change only impacts `ActorModel`): == 2pc check 10 == Done. states=817760258, unique=61515776, sec=56 Done. states=817760258, unique=61515776, sec=57 Done. states=817760258, unique=61515776, sec=58 == paxos check 6 == Done. states=18972647, unique=9357525, sec=17 Done. states=18972647, unique=9357525, sec=17 Done. states=18972647, unique=9357525, sec=18 == single-copy-register check 4 == Done. states=731789, unique=400233, sec=6 Done. states=731789, unique=400233, sec=5 Done. states=731789, unique=400233, sec=5 == linearizable-register check 2 == Done. states=194646243, unique=41138199, sec=78 Done. states=194646243, unique=41138199, sec=80 Done. states=194646243, unique=41138199, sec=80 After: == 2pc check 10 == Done. states=817760258, unique=61515776, sec=56 Done. states=817760258, unique=61515776, sec=57 Done. states=817760258, unique=61515776, sec=58 == paxos check 6 == Done. states=18972647, unique=9357525, sec=18 Done. states=18972647, unique=9357525, sec=18 Done. states=18972647, unique=9357525, sec=18 == single-copy-register check 4 == Done. states=731789, unique=400233, sec=6 Done. states=731789, unique=400233, sec=5 Done. states=731789, unique=400233, sec=6 == linearizable-register check 2 == Done. states=194646243, unique=41138199, sec=79 Done. states=194646243, unique=41138199, sec=81 Done. states=194646243, unique=41138199, sec=80
I recently tried to write the Ballot Leader Election with Gossiping using Stateright and encountered some issues along the way.
I can not stop Stateright from generating new states. Even though I added a maximum of rounds to stop the set-up of the timer, it keeps generating states.
Are there issues with using the function on_timeout?
Repo: https://github.com/Nightcro/ble-stateright
The text was updated successfully, but these errors were encountered: