| Summary: | Nondeterministic select causes unexpected probabilities for equally weighted transitions. | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Morten Korsholm Terndrup <mternd13> |
| Component: | Engine | Assignee: | 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 | ||
I'll update the documentation, thanks for the report! |
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. Cheers.