| Summary: | TIGA can break SMC semantics for branching edges | ||
|---|---|---|---|
| Product: | UPPAAL Stratego | Reporter: | Peter Gjøl Jensen <pgj> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | enhancement | ||
| Priority: | P5 | ||
| Version: | 4.1.20-3 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: | No strategy exists ensuring the property | ||
Created attachment 298 [details] No strategy exists ensuring the property When using tiga to first synthesize a strategy, it violates sanity of controllable edges with branching. This enables tiga to have magical powers, and control which probabilistic branches should be taken. (Partly fixed in development branch stratego_2016_ndiscrete by throwing error for controllable edges with branching)