search

UPPAALModelChecker / UPPAAL-Meta

This is the offcial meta repo for issue reporting, feature request and public roadmap for the development of UPPAAL.
http://www.uppaal.org
1 stars 0 forks source link

Broadcast explicit ordering #20

Closed marmux closed 3 years ago

marmux commented 3 years ago

Is your feature request related to a problem? Please describe. A clear and concise description of what the problem is. Ex. I'm always frustrated when [...] Yes, broadcast causes different answers depending on the operating system

Describe the solution you'd like A clear and concise description of what you want to happen. I would like that the user is able to specify and ordering on the receiving edges in a broadcast e.g. bcan?[2], where 2 is a natural number indicating the order. It should be a total order.

Additional context Add any other context or screenshots about the feature request here.

For the query A<> DriverFast.stable && desired_speed == 78 The following file produces satisfied in Windows and not satisfied in Ubuntu 20.04

sheet2CruiseController_sol.zip

mikucionisaau commented 3 years ago

I have tried this model+query on verifyta 4.1.24 and the results are identical (not satisfied) on both Linux and Windows. Am I missing something? perhaps query options?

yrke commented 3 years ago

Running on uppaal stratgo 4.1.20-stratego8-beta6 on windows it answers "not satisfied". But, I don't think you should or can rely on the syncornisation order (maybe the order should be random to discourage doing this).

If you events to happen in a specific order why not just add Tick1!, Tick2!, Tick3!... channels in the Cround process?

marmux commented 3 years ago

I am sorry for this, it is my bad. I had a different guard in one version. This was the reason of the dis agreement in Linux and Windows.

The problem is that there can be read write conflicts, and the ordering can lead to different states. Most users are not aware of this, thus either, an order should be clear to the user, or the tool should send a syntax error for the read write conflicts.

If the help manual is correct, then the declaration of the processes defines the unique order. That will be fine.