Bug 655

Summary: Nondeterministic select causes unexpected probabilities for equally weighted transitions.
Product: UPPAAL Reporter: Morten Korsholm Terndrup <mternd13>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: normal CC: adavid
Priority: P5    
Version: 4.1.19   
Hardware: PC   
OS: Linux   
Architecture: x86_64 (64bit)
Attachments: minimal example

Description Morten Korsholm Terndrup 2018-05-28 12:28:26 CEST
Created attachment 327 [details]
minimal example

Models with nondeterministic select statements causes the probabilites of taking  otherwise equally weighted transitions to be skewed. I believe that this is because UPPAAL (under the hood) generates an edge for every possible value from the domain of the select, which then multiplies the probabilities. The phenomenon is present on Linux and Windows 10.

I have attached a minimal example model with queries.

If this is not a bug in the engine, then it should probably be explicit in the documentation.

Comment 1 Marius Mikučionis 2018-05-30 11:30:42 CEST
I'll update the documentation, thanks for the report!