The problem of simulator

[李帅]

Dear sir or madam,

    When constructing two timed automata in UPPAAL, if both two initial states of them are committed type, two timed automata are deadlock. The detail information is as shown in Fig.1, where gtr is a global clock and t is a local clock.

    Furthermore, if I change the initial state in second time automata, it is still deadlock. The detail information is as shown in Fig.2.

  Please tell me why this situation happens, is it because there are some special mechanism in UPPAAL, or there are some mistakes in the usage of committed or channel ? How to change these models so that they can continue to execute.

    Thank you very much!

Fig.1 

Fig. 2

[Marius Mikučionis]

Dear 李帅,

The deadlock in Fig.1 is because the second process is in the committed location (meaning that no other process can progress until it leaves the committed location), but it cannot leave because the only edge available is waiting for input.

Basically the committed location contradicts the wait for inputs on the outgoing edge -- such a combination is almost always a specification mistake.

The deadlock in Fig.2 is because the first process is in the committed location and there is no outgoing transition available at all and thus prevents any progress.

The committed locations are specific to Uppaal and their purpose is to group atomic transitions into uninterruptable transition, e.g. multiple synchronisations at the same time (which is not possible otherwise), however the combination of input edge from committed location is not compositional, because such process cannot make progress without external process and thus deadlocks entire system.

Hope that helps.

Best regards,
Marius

[李帅]

Dear sir or madam,

  Thank you for your advice! 

  The propose that we construct this model is to verify the possible earliest completed and latest completed time of two timed automata: Template and Template 0. 

  As shown in Fig. 1, we used “gtr” (a global clock) to record the time intervals (two timed automata). Now, as shown in Fig. 2 and Fig. 3, our query language in verifier are inf {Template0.L23}:gtr and sup {Template0.L23}:gtr, but we can NOT obtain the result that we want, please give some advices about this problem. 

  Furthermore, is that the above idea correct (Namely, we use "gtr" to record the time intervals in two timed automata)? 

  Thank you very much!

Fig. 1

Fig. 2

Fig. 3

在 2020年1月6日星期一 UTC+8下午4:35:08，Marius Mikučionis写道：

[Marius Mikučionis]

On Monday, January 6, 2020 at 10:43:32 AM UTC+1, 李帅 wrote:

Dear sir or madam,

  Thank you for your advice! 

  The propose that we construct this model is to verify the possible earliest completed and latest completed time of two timed automata: Template and Template 0. 

  As shown in Fig. 1, we used “gtr” (a global clock) to record the time intervals (two timed automata). Now, as shown in Fig. 2 and Fig. 3, our query language in verifier are inf {Template0.L23}:gtr and sup {Template0.L23}:gtr, but we can NOT obtain the result that we want, please give some advices about this problem. 

  Furthermore, is that the above idea correct (Namely, we use "gtr" to record the time intervals in two timed automata)? 

Yes, that is all correct. You just measured the response time of the first process and not entire system, because the gtr is reset in the first process and the local t is *not* reset in the second process.

The lower bound on gtr is 1, because the system delays to arbitrary tiime, gtr ir reset and the guard t>=1 does not allow any earlier response.

Also there is no upper bound (gtr<infinity) because the process is allowed to delay forever in L13 and L14.

I guess that there are two local clocks t (i.e. t is not shared), the second process does not reset it, thus it gets delayed to arbitrary value (e.g. t>=4) when the first process is in L11, therefore the guard t>=4 does not stop it and thus does not create additional delay.

If the second process would reset t on L21->L22, then the lower bound on gtr should be 5. 

Is that what you are expecting?

[李帅]

Dear sir or madam,

    Thank you for your advice!

The result we expect is that the lower bound on gtr is 5 (calculated by t>=1 and t>=4) and the upper bound on gtr is 8 (calculated by t<=3 and t<=5). However, the range on gtr is not we expect.

Please tell me how to set the type of states or arcs in these two timed automaton to get the result above (Namely, the lower bound on gtr is 5 and the upper bound on gtr is 8). We learned that setting “committed” or “urgent” on the status can keep the time no delay, is this setting correct? If so, how should I set these.

Thank you very much.

在 2020年1月7日星期二 UTC+8下午2:25:19，Marius Mikučionis写道：

[Marius Mikučionis]

On Tuesday, January 7, 2020 at 9:15:27 AM UTC+1, 李帅 wrote:

Dear sir or madam,

    Thank you for your advice!

The result we expect is that the lower bound on gtr is 5 (calculated by t>=1 and t>=4) and the upper bound on gtr is 8 (calculated by t<=3 and t<=5). However, the range on gtr is not we expect.

Please tell me how to set the type of states or arcs in these two timed automaton to get the result above (Namely, the lower bound on gtr is 5 and the upper bound on gtr is 8). We learned that setting “committed” or “urgent” on the status can keep the time no delay, is this setting correct? If so, how should I set these.

Thank you very much.

The gtr would include the delay of the second process if the clock t is reset on the edge from L21 to L22.

So this will increase the lower bound to 5.

Then query concerns about gtr value in location L23, thus we do not want to waste any time (do not allow gtr to diverge to infinity in that location) and thus we need to stop the clock gtr in L23. 

This can be be achieved in several ways:

1) make L23 urgent, this will stop the time and force the second process to leave L23 in no time.

2) make L23 committed, this will stop the time and preempt other processes, but it is OK in this case (it can progress to L24 and delay there, which does not affect the gtr in L23).

3) stop the gtr clock in L23 by adding an invariant gtr'==0. Note that this will turn on an overapproximation, which may have precision consequences for other queries.

Once the clock is stopped in L23, the supremum on gtr should stay <=3+5==8.

Best regards,
Marius

[李帅]

Dear sir or madam:

  Thank you for your advice!

  we have tried several ways according to your advices (the details are as follows), but we cannot get the result we expect (Namely, the lower bound on gtr is 5 and the upper bound on gtr is 8). In our model, gtr is a global clock by setting “clock gtr” and R1 is a channel by setting “chan R1” in global declarations, and t is a local clock by setting “clock t” in local declarations.

Way 1): As shown in Fig. 1, according to your first way (make L23 urgent, this will stop the time and force the second process to leave L23 in no time), we set L23 as urgent state, but the result is NOT what we expect.

Fig. 1

Way 2): As shown in Fig. 2, according to your second way (make L23 committed, this will stop the time and preempt other processes, but it is OK in this case (it can progress to L24 and delay there, which does not affect the gtr in L23)), we set L23 as commited state, but the resule is still NOT what we exepect.

Fig. 2

Way 3): As shown in Fig. 3, according to your second way (stop the gtr clock in L23 by adding an invariant gtr'==0. Note that this will turn on an overapproximation, which may have precision consequences for other queries.), we add and invariant gtr1==0 on L23, but the resule is still NOT what we exepect.

Fig. 3

Please give us some more useful advice about the above problems. Then, in this round, we have uploaded our UPPAAL model in the attached file named as “Model”.

Thank you very much!

在 2020年1月8日星期三 UTC+8下午5:46:38，Marius Mikučionis写道：

[Marius Mikučionis]

Dear 李帅,

The solution is attached. See also the screenshot of simulator with bounds.

On Thursday, January 9, 2020 at 8:14:56 AM UTC+1, 李帅 wrote:

Dear sir or madam:

  Thank you for your advice!

  we have tried several ways according to your advices (the details are as follows), but we cannot get the result we expect (Namely, the lower bound on gtr is 5 and the upper bound on gtr is 8). In our model, gtr is a global clock by setting “clock gtr” and R1 is a channel by setting “chan R1” in global declarations, and t is a local clock by setting “clock t” in local declarations.

Way 1): As shown in Fig. 1, according to your first way (make L23 urgent, this will stop the time and force the second process to leave L23 in no time), we set L23 as urgent state, but the result is NOT what we expect.

Fig. 1

There is still no reset on L21 -> L22.

 

Way 2): As shown in Fig. 2, according to your second way (make L23 committed, this will stop the time and preempt other processes, but it is OK in this case (it can progress to L24 and delay there, which does not affect the gtr in L23)), we set L23 as commited state, but the resule is still NOT what we exepect.

Fig. 2

Way 3): As shown in Fig. 3, according to your second way (stop the gtr clock in L23 by adding an invariant gtr'==0. Note that this will turn on an overapproximation, which may have precision consequences for other queries.), we add and invariant gtr1==0 on L23, but the resule is still NOT what we exepect.

Fig. 3

Please give us some more useful advice about the above problems. Then, in this round, we have uploaded our UPPAAL model in the attached file named as “Model”.

Thank you very much!

There is an apostrophe on gtr.

Anyway, take a look here:

[李帅]

Dear professor,

Thank you very much for your constructive and useful suggestions! We really appreciate what you’ve done for us in several days.

Based on the last model, we add more states and arcs (with loop structure) on it, and find that the same problem will still exist, i.e., we can't verify the possible earliest completed and latest completed time in the two timed automata.

Our new model is as shown in Fig.1. When we want to verify the possible earliest completed and latest completed time in state Template2. L28 with the queries “inf {Template2.L28}:gtr” and “sup {Template2.L28}:gtr” in UPPAAL, and the results are all gtr>=21 and gtr<inf, but it is NOT we want.

The results we want are the lower bound of state L28 in Template2 is gtr>=21 (calculate by 1+3+1+1+3+6+1+3+1+1=15+6=21, where 15 is the sum of clocks in Template1 and 6 is the sum of clocks in Template2), and upper bound of state L28 in Template2 is gtr<=39 (calculate by 2+5+4+2+5+8+2+5+4+2=26+13=39, where 26 is the sum of clocks in Template1 and 13 is the sum of clocks in Template2), but the upper bound (Namely, gtr<=inf) in verifier with query “sup {Template2.L28}:gtr” is NOT we want.

Are we building the model in the wrong way or some states or arcs in UPPAAL not setting correctly? Please give us some more advice about above problem. Furthermore, we have uploaded this UPPAAL model in the attached file named as “Model1”.

Thank you very much.

Fig. 1

在 2020年1月11日星期六 UTC+8上午12:25:55，Marius Mikučionis写道：

[Marius Mikučionis]

Dear 李帅,

You should validate your model before using inf and sup queries -- they are really not a good start as they do not provide you with diagnostics.

Since you are not expecting gtr value beyond 39, I would suggest to get a diagnostic trace (see Options menu) when gtr grows beyond 39 by checking the following query:

E<> gtr>39

Then analyse that trace in the simulator and see how gtr grows beyond that bound.

Best regards,
Marius

[李帅]

Dear professor,

We apologize that perhaps we do not express our problem clearly to you.

Our problem is that we construct the model (the details are shown in Fig.1) according to your pervious advices, but it stops abnormally in simulator of UPPAAL.

Please give us some more useful advice, such that the model can execute continually. Furthermore, in this round, we have uploaded the model named “model2” in this reply.

Thank you very much!

Fig. 1

在 2020年1月12日星期日 UTC+8上午1:15:31，Marius Mikučionis写道：

[Marius Mikučionis]

Dear 李帅,

On Tuesday, January 14, 2020 at 8:09:13 AM UTC+1, 李帅 wrote:

Dear professor,

We apologize that perhaps we do not express our problem clearly to you.

No, everything is clear, it's just you keep changing the problem.

There is nothing wrong with Uppaal, you just need to learn the notation.

Perhaps it would be easier to consult with your instructor, or read the Uppaal tutorial.

 

Our problem is that we construct the model (the details are shown in Fig.1) according to your pervious advices, but it stops abnormally in simulator of UPPAAL.

Please give us some more useful advice, such that the model can execute continually. Furthermore, in this round, we have uploaded the model named “model2” in this reply.

Thank you very much!

Fig. 1

It is not my task to teach you, so I will just read what the simulator is showing, perhaps it'll be more useful:

Enabled Transitions panel shows "deadlock": it claims that there are no transitions that the system can take.

Sometimes it is also useful to select the "deadlock" transition to inspect the clock values to understand when exactly it happens, but in this case it is irrelevant as no other transition is available.

In order to understand why the system cannot progress, we need to examine why every process cannot progress.

Template1 is in location L12 which has one edge:

L12 to L13 is guarded by "t>=1", where the variable panel shows that the clock Template1.t=0, thus the guard "t>=1" is false and the edge is disabled, the Template1 cannot make any transition.

The variable panel shows Template1.t=0 which means that the clock cannot progress -- the time has been stopped (due to invariant, urgent or committed location somewhere in the system).

Note that L12 has an invariant "t<=2", but it has not been exhausted (Template1.t=0), therefore this invariant is not stopping the time in this state.

Template2 is in location L22 which has two edges:

L21 to L22 is guarded by "m==0", where the variable panel shows that Template2.m=0, the guard is true, hence the edge is enabled, however the edge also has a synchronization "R2?", but it is not paired (there are no other process which can sync "R1!") thus it cannot be taken.

L21 to L27 is guarded by "m==1", where the variable panel shows that Template2.m=0, the guard is false, hence the edge is disabled.

Therefore Template2 cannot make any transition.

In addition, L21 is urgent, meaning that it blocks the time passing (which prevents Template1.t from growing and reaching "t>=1" as we saw above).

Therefore no process can make a transition, therefore the system is in deadlock. Q.E.D.

To summarize, here is a chain of dependencies to solve the deadlock:

1) Template1 is waiting for the time to elapse (t needs to grow from 0 to 1 to satisfy the guard).

2) The time is blocked by Template2 because it is in urgent location L21.

3) Template2 cannot leave L21 because it is waiting for synchronization on R1 (or for m to become 1).

4) There is no process that could synchronize on R1.

Solving any one (only one) of these dependencies will solve this particular deadlock, i.e. do one of the following:

1) remove the guard from L12 to L13, or

2) remove "urgent" from L21, or

3) remove R1 synchronization (or set Template2.m to 1), or

4) add an extra process to send on R1.

There are no right or wrong solution, you are the author of this specification, thus you need to decide how the system should look like.

Best regards,
Marius