Questions about the simulate query

[tintengrun]

My problem is with the 'simulate' query. What I want to find out is, when a number of simulations of my whole system reach the last state in my templates and when they use a broadcast channel to change templates. If possible I would like to query the broadcast channels directly, but I have not yet found any information on whether that is even possible.
In the absence of that query, I have tried querying the last states of my templates with the simulate query. However, I'm not sure wether that approach even takes into account my whole system, or whether in only takes the individual templates and queries them. I have some temporal dependencies in my system, so some states cannot be reached without first reaching other states. When I tried queries to find out if those specific dependencies were correct, I got results that were pretty nonsensical.

So two questions:

1. Can I somehow query the broadcast channels?
2. How exactly does the 'simulate' query work? Does it simulate the whole system or just parts?

[mikucionisaau]

1. No, currently there is no way to relate to channel variables because they do not have a state, only the state variables and locations are available. Instead of channels, try locations reached by taking the synchronization of interest. For example, open Open Example > smc > train-gate-stat query: simulate[<=200] { Train(1).Cross } shows a bump from 0 to 1 when Train(1) is in location Cross and 0 otherwise:
   
   Each process also has a pseudo variable location which denotes the index of the location, for example: simulate[<=200] { Train(1).location }
   
   But it requires knowing the location index.. Alternatively one can supply custom location encoding:
   simulate [<=100] { Train(1).Safe+Train(1).Appr*2+Train(1).Stop*3+Train(1).Start*4+Train(1).Cross*5 }
   
   where 1=Safe, 2=Appr, 3=Stop, 4=Start, 5=Cross.
2. simulate query runs a complete system simulation (i.e. all the processes in the system statement) and then plots how the values of given expressions change over time. The above shows location expressions, but it can be arbitrary state expressions (variables, functions etc).

If you are interested in some certain behavior, then the stochastic system can be quite difficult to drive because there can be lots of different behaviors. You could try the following:

1. Request more simulation runs with simulate[<=100; N] { ... }, where N is the number of runs (by default it gives you just one).
2. Request to display only runs that end with certain condition P: simulate[<=100; N] {...} : P
3. Request to display at most M trajectories satisfying P: simulate[<=100; N]{...} : M : P
4. Use Concrete Simulator to get to some interesting place and then right-click on some variable and choose Add Plot
5. Use probability estimation query to find a state with the predicate of interest, load the trace into concrete simulator and inspect it there. For example, add a query Pr[<=100](<> Train(1).Cross), enable the diagnostic trace Options > Diagnostic trace > Some, click Check, observe a Load trace? dialog, click Yes and switch to Concrete Simulator.

Please see the documentation: https://docs.uppaal.org/language-reference/query-syntax/statistical_queries/

[tintengrun]

Uploading breakin-VAFT-Full.zip…
Of course

[mikucionisaau]

Looks like the link to file is broken, it does not lead to a zip. Please try again.

[tintengrun]

I'm sorry, I hope this works:
breakin-VAFT-Full.zip

[mikucionisaau]

The three lines represent states, where 0 probably means it does not get visited and 1 it gets visited.

Correct.

However, in the system I connected these states with a priority-AND, meaning they have to be visited in the order hide_key, find_key, open_front_door.

This does not seem to be the case. Here is how to generate a counter example:

1. Add a query:

Pr[<=5000](<> open_front_door.Success)

2. Enable diagnostic trace: Options > Diagnostic Trace > Shortest
   (I see that you have enabled bunch of other options, but most of the them are irrelevant for SMC, like: Exploration, State space reduction, State space representation, Extrapolation can be reset to default values)

3. Click Check and it should generate the trace quite quickly.

4. Go to Concrete Simulator tab and step through the trace to validate what goes on.

The model is quite big, so I do not know what exactly goes wrong. Below I show some states where I have reordered the processes for the processes you mentioned to be close together visually.

I see some red-flags on states like the following, where multiple processes end up in committed locations:

This means that (at least) these two processes will be racing and therefore atomicity between them is not preserved. There can be more processes going through committed locations like this and thus may break many of your assumptions.

In particular this:

and then this:

I did not inspect the rest of processes, but there can be even more such situations.

Then finally find_key and open_front_door end up in this combination:

where open_front_door is free to progress to Wait_success and receive attach_succ[id], but find_key can be stuck in Activated (in principle forever, I think we are lucky to hit the counterexample with such high probability), and find_key may also go into Wait_Failure (with some probability), where it will not be able to reach Wait_success.
Similarly hide_key can also fail by taking p_fail branch.

In summary, I think that either your assumptions about the committed locations are broken (looks like committed locations are abused through broadcast synchronization) or find_key can get stuck in Activated or Wait_failure and thus loose the race to open_front_door.

[tintengrun]

That is amazing, thank you so much!