Using exact model checking in PRISM with very small probabilities

[Arpan]

Hi,

I am using PRISM for some sort of reliability analysis. My input probabilities (each of type const double) are extremely small values. Unfortunately, I am getting a syntax error when representing the following value:

const double prob = 2867940088951973/288230376151711744;

and similar other values. It seems if the number of digits in the numerator and the denominator is small, the error goes away.

Any suggestions on how to supply such small probabilities (e.g., 10^-15) as constants? 

Thanks,

Arpan

[Joachim Klein]

Hi Arpan,

> I am using PRISM for some sort of reliability analysis. My input

> probabilities (each of type /const double/) are extremely small values.

> Unfortunately, I am getting a syntax error when representing the
> following value:
>
> const double prob = 2867940088951973/288230376151711744;
>
> and similar other values. It seems if the number of digits in the
> numerator and the denominator is small, the error goes away.
>
> Any suggestions on how to supply such small probabilities (e.g., 10^-15)
> as constants?

The issue is that the parser treats the numerator and denominator as
integer literals and those are stored as Java ints (range of around ~2^31).

If you use

const double prob = 2867940088951973.0/288230376151711744.0

both numerator and denominator are parsed as double values and you get a
constant with the corresponding double (IEEE floating-point) result.

You can also specify a value using the normal floating point scientific
notation, e.g., 1E-15 would correspond to 1 * 10^15.


If you have very small probabilities, there's a chance that you may run
into other issues with precision that you may want to keep in mind:

- In the standard computations, the values are processed using
floating-point arithmetic with the possibility of rounding-errors etc

- If you are using one of the engines making use of MTBDD-based
techniques (mtbdd, hybrid, sparse), some of the floating point values
can be truncated, adding further imprecision. You can tweak the
truncation point via the -cuddepsilon setting.

- There might be issues with convergence of the iterative solution
methods, you may want to try the interval iteration option to compare
the results.

- If your model is not that large you can try to use the exact engine,
which uses an arbitrary precision representation (biginteger for
numerator and denominator) for the values. Currently, however, you would
run into the same parsing issue as now; we are working on some
refactoring there.


Cheers,
Joachim

[Arpan Gujarati]

Thanks Joachim for your reply.

You can also specify a value using the normal floating point scientific

notation, e.g., 1E-15 would correspond to 1 * 10^15.

 

- If your model is not that large you can try to use the exact engine,

which uses an arbitrary precision representation (biginteger for
numerator and denominator) for the values. Currently, however, you would
run into the same parsing issue as now; we are working on some
refactoring there.

 

Yes, so I am actually using the exact engine. And as you suggested above, in my initial attempt, I provided the constant value as 1e-15.

To be precise, these were my definitions:

const double prob_event = 1.093271e-14;

const double prob_no_event = 1 - prob_event;

However, I get the following error: "Probabilities sum to 100000000000000003271/100000000000000000000 instead of 1 in state ...".

I suspected this was because of some conversion from float to arbitrary precision arithmetic during definition of the constants, and hence I moved to an approach where I define these constants as fractions in the first place.

Now that I move to the approach you suggested, i.e., define constants as:

const double prob = 2867940088951973.0/288230376151711744.0

I again run into the same error about the sum exceeding 1.

I guess I will try next some of the options you suggested regarding using floating points but with higher precision.

Thanks,

Arpan

--

Thanks and regards,
Arpan

[Joachim Klein]

Hi,

> Yes, so I am actually using the exact engine. And as you suggested
> above, in my initial attempt, I provided the constant value as 1e-15.
>
> To be precise, these were my definitions:
>
> const double prob_event = 1.093271e-14;
> const double prob_no_event = 1 - prob_event;
>
> However, I get the following error: "Probabilities sum to
> 100000000000000003271/100000000000000000000 instead of 1 in state ...".
>
> I suspected this was because of some conversion from float to arbitrary
> precision arithmetic during definition of the constants, and hence I
> moved to an approach where I define these constants as fractions in the
> first place.

Ok, I see. Yes, there are currently issues with the exact engine and
const double definitions that use arithmetic.

You could try the branch at

https://github.com/kleinj/prism/tree/exact-fixes-2017-10-13

The changes included there should address exactly that issue. In the
main version of PRISM, if you have constants that are defined via an
arithmetic expression, the value is computed using floating point
arithmetic and then converted to an exact fraction, so you get the
imprecision. The definition via literal (1.093271e-14) is directly
translated into the fraction (1093271/100000000000000000000). In the
branch, constant definitions with arithmetic should be handled properly.


Alternatively, you could just use a formula for the 1-p probability:

const double prob_event = 1.093271e-14;

formula prob_no_event = 1 - prob_event;

That way, all occurences of 'prob_no_event' are replaced in your model
source by the arithmetic expression and properly evaluated using exact
arithmetic.


Cheers,
Joachim