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

Bug 619 - TIGA can break SMC semantics for branching edges
Summary: TIGA can break SMC semantics for branching edges
Status: ASSIGNED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.20-3
Hardware: PC Linux
: P5 enhancement
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2016-09-27 03:30 CEST by Peter Gjøl Jensen
Modified: 2017-03-15 12:29 CET (History)
0 users

See Also:
Architecture:


Attachments
No strategy exists ensuring the property (1.36 KB, text/xml)
2016-09-27 03:30 CEST, Peter Gjøl Jensen
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Peter Gjøl Jensen 2016-09-27 03:30:46 CEST
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)