Uncontrollable edges in Uppaal Stratego

[Reza Soltani]

Hi,

I'm using Uppaal for a long time, but recently I started using Stratego. In the cruise control example (https://uppaal.org/casestudies/stratego/#safe-and-optimal-cruise-control), in the "system" template, why is the type of edges from "EgoNext" to "FrontNext" is uncontrollable since the "EgoNext" is an urgent location? I attached 4 pictures. Picture 1 shows the original "system" template, and picture 2 is the verification results for one of the queries. But, why when I change the edges that come out of the urgent location in the "system" template (please refer to picture 3), do the verification results change (picture 4)? Also, some queries return false in the later condition.

[Marius Mikučionis]

Hi,

Please see my answers below.

On Wednesday, 1 February 2023 at 18:52:31 UTC+1 Reza Soltani wrote:

Hi,

I'm using Uppaal for a long time, but recently I started using Stratego. In the cruise control example (https://uppaal.org/casestudies/stratego/#safe-and-optimal-cruise-control), in the "system" template, why is the type of edges from "EgoNext" to "FrontNext" is uncontrollable since the "EgoNext" is an urgent location?

Those transitions are periodic and hence not really controllable. 

Uncontrollable also means that optimization queries ("minE") do not have to record them as a viable choice.

The "chooseEgo!" synchronizes with Ego input, which is marked as controllable, but the entire transition is still uncontrollable (one of the synchronizing edges is uncontrollable means entire transition is uncontrollable).

 

I attached 4 pictures. Picture 1 shows the original "system" template, and picture 2 is the verification results for one of the queries.

If you make "chooseEgo!" as controllable, then TIGA and optimization queries will treat it as controllable transition, but from plain SMC queries, there should not be a difference.

 

But, why when I change the edges that come out of the urgent location in the "system" template (please refer to picture 3), do the verification results change (picture 4)? Also, some queries return false in the later condition.

Right. The issue is a bug the way the controllable/uncontrollable was being treated, there should not be any difference.

I just checked and Stratego 11 computes the same probability value.

Best regards,
Marius