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)