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

Concrete Simulator: Broadcast receiver's update part is calculated even if the sending edge's guard is false #257

Open
GameMonkey opened this issue Apr 2, 2024 · 0 comments
Labels
bug Something isn't working confirmed

Comments

@GameMonkey
Copy link

Describe the bug
This bug happens only in the concrete simulator.

I have two processes during communication over a broadcast channel.

When the guard of the sending edge is false, the update part of the receiving process is still calculated. This can result in errors, such as our-of-bounds errors. However, the update part of the sending edge is not calculated.

To Reproduce
Steps to reproduce the behavior:

  1. Download the minimum example test_broadcast_fail.zip
  2. Go into the Concrete simulator
  3. Take one transition
  4. See error

Expected behavior
In this case, the model should enter a deadlock state.

If the update of the sink_values is commented out of foo(), the model enters the deadlock state.

Version(s) of UPPAAL tested
UPPAAL 5.0.0 (rev. 714BA9DB36F49691), 2023-06-21

Desktop (please complete the following information):

  • Kubuntu 23.10, Linux laptop 6.5.0-25-generic
  • openjdk 17.0.10 2024-01-16,
@mikucionisaau mikucionisaau added bug Something isn't working confirmed labels Apr 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working confirmed
Projects
None yet
Development

No branches or pull requests

2 participants