State indicated as violating an invariant, while it is not the case...

[Harveston James]

Hi,

I have been trying the modeling of a Gaussian distribution as proposed in the "UPPAAL SMC Tutorial" (see Fig 23 on page 20).

So, I defined the simple automaton attached here. Note that x, y, and delay are clocks.  

When running this automaton with the concrete simulator (seems the symbolic simulation does not work with this example?), it always ends up with the message state s1 violates the invariant! But, when checking the values of the clocks used in this state, they never show any property violation. 

Could you please explain why this example behaves like that? Thank you so much for your answer.

Best regards, 

[Marius Mikučionis]

Hi,

What property did you check?

The tutorial and the model are clearly meant for SMC queries, therefore please try "simulate [<=10] { x, y, delay}" or "E[<=10](max: delay)" or similar to inspect the generated values.

I cannot see the implementation of f(), but if you are trying Gaussian distribution, then the values of delay may in principle extend to both infinities and it may fail the invariant y<=delay, where y:=1 and delay<1 (provided that f() has no protection and can generate such values).

Note that the symbolic engine (simbolic simulator and queries like E<>, A[] etc) disables the floating point operations, and the example seem to depend on the floating point operations in invariant, i.e. it is not a simple cost function, thus it cannot work. Especially the random functions cannot work, because they act as hidden non-determinism.

The cost function pattern detection is not implemented thus Uppaal simply allowes it without warning -- we are working on that.

Best regards,
Marius

[Harveston James]

Hi,

Le lundi 25 mai 2020 11:39:11 UTC+2, Marius Mikučionis a écrit :

Hi,

On Saturday, May 23, 2020 at 4:53:03 PM UTC+2, Harveston James wrote:

Hi,

I have been trying the modeling of a Gaussian distribution as proposed in the "UPPAAL SMC Tutorial" (see Fig 23 on page 20).

So, I defined the simple automaton attached here. Note that x, y, and delay are clocks.  

When running this automaton with the concrete simulator (seems the symbolic simulation does not work with this example?), it always ends up with the message state s1 violates the invariant! But, when checking the values of the clocks used in this state, they never show any property violation. 

Could you please explain why this example behaves like that? Thank you so much for your answer.

What property did you check?

I did not try any property yet. I just tried to run the concrete simulator on this example. This simulator still produces the same error message.

 

The tutorial and the model are clearly meant for SMC queries, therefore please try "simulate [<=10] { x, y, delay}" or "E[<=10](max: delay)" or similar to inspect the generated values.

Great! I will check.

 

I cannot see the implementation of f(),

Here it is:

clock x, y, delay;

const double PI = 3.14159265358979323846;

double stdNormal() { // N(0, 1)

  return sqrt(-2*ln(1-random(1))) * cos(2*PI*random(1));

} 

double Normal(double mean, double stdDev) {

  return mean + stdDev * stdNormal();

}

double f() { // N(3.0, 1.0) 

  return Normal(3.0, 1.0);

}

but if you are trying Gaussian distribution, then the values of delay may in principle extend to both infinities and it may fail the invariant y<=delay, where y:=1 and delay<1 (provided that f() has no protection and can generate such values).

Okay. 

FYI, I attached a snapshot of the automaton with the clock values when the error occurs. It seems that the shown values should satisfy the invariant.

 

Note that the symbolic engine (simbolic simulator and queries like E<>, A[] etc) disables the floating point operations, and the example seem to depend on the floating point operations in invariant, i.e. it is not a simple cost function, thus it cannot work. Especially the random functions cannot work, because they act as hidden non-determinism.

The cost function pattern detection is not implemented thus Uppaal simply allowes it without warning -- we are working on that.

Good to know. That will be useful indeed. 

Thank you very much.

Best regards