Parameter Ordering and Experiments change Modelchecking results

[S Linker]

Hi,

I'm currently working on a model of synchronising oscillators with discrete time (attached), and I noticed some strange behaviour while conducting experiments.

My model has three parameters:

refractoryPeriod (int)

mu (double)

epsilon (double)

Now, I want to get results for a certain property (attached) for several parameter combinations. 

However, for epsilon=.1, the results change depending on:

a) whether I use an experiment with 

  reftractoryPeriod in {0..10}

  mu=0

  epsilon =.1

or

  refractoryPeriod in {0..10}

  mu=0

  epsilon in {0, 0.1, 0.2, ..., 1.0}

b) the order of mu and epsilon in the model definition. 

The results for epsilon !=.1 stay the same, though. I assume it is related to the iterative methods, since the results also change if I change the precision or the iteration method. 

I was able to reproduce this behaviour both in Prism 4.4beta (Linux, 64bit) and 4.3.1 (compiled from source). 

Sorry for the rather large model, the behaviour seems to be rather fragile (a model with two sensors didn't show it).

Am I misunderstanding some basic properties of PRISM, or did I stumble upon a bug?

Cheers,

Sven Linker

[Joachim Klein]

Hi Sven,

> The results for epsilon !=.1 stay the same, though. I assume it is
> related to the iterative methods, since the results also change if I
> change the precision or the iteration method.
>
> I was able to reproduce this behaviour both in Prism 4.4beta (Linux,
> 64bit) and 4.3.1 (compiled from source).

This is curious. I could reproduce this for the command lines below:

> prism synchronisation_model.pm synchronisation.props -const refractoryPeriod=0:1:10,mu=0,epsilon=0:0.1:1 --exportresults epsilon-experiment.txt
> prism synchronisation_model.pm synchronisation.props -const refractoryPeriod=0:1:10,mu=0,epsilon=0.1 --exportresults epsilon-single.txt

I'm getting results:

> 0 0.1 0.694 0 0.694
> 1 0.1 0.694 1 0.694
> 2 0.1 0.937 2 0.694
> 3 0.1 0.769 3 0.769
> 4 0.1 0.82 4 0.82
> 5 0.1 0.898 5 0.898
> 6 0.1 0.586 6 0.586
> 7 0.1 0.268 7 0.268
> 8 0.1 0.076 8 0.076
> 9 0.1 0.01 9 0.01
> 10 0.1 0.01 10 0.01

3rd column is the result from the first run, 5th column from the second
run. Here, the results differ for refractoryPeriod=2.

When I'm running with the explicit engine (-explicit), I get the same
results.

This seems due to the constant value folding that is done in PRISM's
version of the CUDD MTBDD library, used for building and the symbolic
representation of the model and doing the computations there.
Floating-point values that differ by a configurable threshold are
collapsed to avoid a blowup in the symbolic representation due to having
many values that differ only marginally. If I lower the threshold
(-cuddepsilon 1E-20) I get the same results between both experiments.

As the folding looks at the values that have been previously used, it
looks like running some other calculations beforehand can change this
folding sufficiently in a model that is sensitive to that, such as yours
seems to be.

So, either use a small cuddepsilon or use the explicit engine, there you
should only get the "usual" floating-point precision errors.


Cheers,
Joachim Klein

PS: By the way, it looks like that your probabilities (for a given
state) are either 0 or 1 (in the logs, 'maybe' is 0), so the iterative
methods are not used at all.

[Sven Linker]

Hi Joachim,

On 17/11/17 09:58, Joachim Klein wrote:
> This is curious. I could reproduce this for the command lines below:
>
>> prism synchronisation_model.pm  synchronisation.props -const
>> refractoryPeriod=0:1:10,mu=0,epsilon=0:0.1:1 --exportresults
>> epsilon-experiment.txt
>> prism synchronisation_model.pm  synchronisation.props -const
>> refractoryPeriod=0:1:10,mu=0,epsilon=0.1 --exportresults
>> epsilon-single.txt
>
> I'm getting results:
>
>> 0    0.1    0.694    0    0.694
>> 1    0.1    0.694    1    0.694
>> 2    0.1    0.937    2    0.694
>> 3    0.1    0.769    3    0.769
>> 4    0.1    0.82    4    0.82
>> 5    0.1    0.898    5    0.898
>> 6    0.1    0.586    6    0.586
>> 7    0.1    0.268    7    0.268
>> 8    0.1    0.076    8    0.076
>> 9    0.1    0.01    9    0.01
>> 10    0.1    0.01    10    0.01

Yes, these are exactly the results I got as well.

> [snip]

> As the folding looks at the values that have been previously used, it
> looks like running some other calculations beforehand can change this
> folding sufficiently in a model that is sensitive to that, such as yours
> seems to be.
>
> So, either use a small cuddepsilon or use the explicit engine, there you
> should only get the "usual" floating-point precision errors.
>

Great, thank you, that solves the issue.

>
> Cheers,
> Joachim Klein
>
> PS: By the way, it looks like that your probabilities (for a given
> state) are either 0 or 1 (in the logs, 'maybe' is 0), so the iterative
> methods are not used at all.

Ok, that's interesting, since switching the iterative method also
changed the results I got for epsilon=0.1. So apparently the model
construction can be quite sensitive, if the floats get small enough.
I'll keep that im mind.

And yes, in this model probabilities are only introduced via the
mu-parameter (which is zero in these experiments).

Thanks again for the quick help!

Cheers,
Sven