| Summary: | Adding a guard to the receiving end of a broadcast sznchronization freezes the simulation (and the verifier) | ||
|---|---|---|---|
| Product: | UPPAAL TIGA | Reporter: | florber |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | normal | ||
| Priority: | P5 | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Windows 10 | ||
| Architecture: | |||
| Attachments: |
example file, simulator shows a deadlock in the initial location
Updated example file, to proof verifier works corretly |
||
Created attachment 302 [details]
Updated example file, to proof verifier works corretly
control: A<> Process.TEST is satisfied
It seems that this is only a simulator bug, as the verification of properties seems to work correctly. |
Created attachment 301 [details] example file, simulator shows a deadlock in the initial location See attached example file. Removing the guard or switching to non-broadcast channels solves the deadlock. Interesting is that the guard does not have to be on a transition leaving the current location. If it is anywhere in the system, it will cause the freeze.