-
Notifications
You must be signed in to change notification settings - Fork 74
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
symbolic bisimulation changes results #498
Comments
Thanks for the bug report. Can you privately share the model file with us via the following email address: [email protected] |
Sure, thanks for looking into this. |
This seems to work if instead of Side note: the expression for the label |
Awesome, that workaround does work. Thank you! Also thanks for the sidenote, this has been a typo, indeed. Cheers! |
Hello everyone,
i am currently working on branch 1.8.0 (due to compatibility with stormpy) and trying to solve timed reachability properties for markov automata.
I have encountered a difference in the results depending on whether bisimulation is used.
Log 1 (without bisim):
Log 2 (with bisim):
In both cases the enginge 'hybrid' has been used, as the sparse engine does not seem to support bisimulation for markov automata.
Unfortunately, i can only share the full model file in private.
Best regards :)
The text was updated successfully, but these errors were encountered: