This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 623 - Adding a guard to the receiving end of a broadcast sznchronization freezes the simulation (and the verifier)
Summary: Adding a guard to the receiving end of a broadcast sznchronization freezes th...
Status: NEW
Alias: None
Product: UPPAAL TIGA
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Windows 10
: P5 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2016-10-19 11:56 CEST by florber
Modified: 2016-10-19 13:02 CEST (History)
0 users

See Also:
Architecture:

Attachments
example file, simulator shows a deadlock in the initial location (1.36 KB, text/xml)
2016-10-19 11:56 CEST, florber 		Details
Updated example file, to proof verifier works corretly (1.39 KB, text/xml)
2016-10-19 13:00 CEST, florber 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description florber 2016-10-19 11:56:49 CEST 
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.
Comment 1 florber 2016-10-19 13:00:46 CEST 
Created attachment 302 [details]
Updated example file, to proof verifier works corretly

control: A<> Process.TEST is satisfied
Comment 2 florber 2016-10-19 13:02:16 CEST 
It seems that this is only a simulator bug, as the verification of properties seems to work correctly.