Possible bugs in Reward model engine

[ivan.zapreev]

As reported by David Jansen.

The following look like errors to me in src/modelchecking/
transient_ctmrm.c :

1. In line 565, a rows x R-matrix is allocated. In lines 577 and 580,
accumulateRewardForStaying is called with parameter value R. In line
498, this function may call add_mtx_val with a column value == R.

Proposed correction: Change line 497 from

if( new_reward <= R ){

to

if( new_reward < R ){

2. In line 928, kIndex is assigned the value index_[col]. This is
supposed to be the value corresponding to the diagonal of the matrix
abs, but col now contains the number of the last nonzero column
in row state (as it has been set by get_mtx_next_val() in line 908).

Proposed correction: Change line 928 from

int kIndex = index_[col];

to

int kIndex = index_[state];

3. Line 466 tests result_error. Currently, this only tests of there
has been an error in the last iteration through the for loop in lines
448-463; however, I think you wanted to check whether there has been
an error in at least one iteration of the loop.
Proposed correction: change lines 458-461 from

result_error = result[i] < 0.0 result[i] > 1.0 + get_error_bound() isnan( result[i] ) isinf( result[i] );

if( result_error ){

result[i] = NaN; /* Set to nan value */

}
to

if ( result[i] < 0.0 result[i] > 1.0 + get_error_bound()

isnan(result[i]) )

{

result[i] = NaN; /* Set to nan value */
result_error = TRUE;

}
(The test for isinf(result[i]) is not necessary, as infinity > 1.0 + get_error_bound() .)

4. In line 921, you call

dfpg(..., r_impulse+value, ...)

but in line 933, you call

dfpg(..., value, ...)

However, in line 933, value is always == 0.0. Shouldn't it be
r_impulse+value also (or just r_impulse) in line 933?

[ivan.zapreev]

By David N. Jansen: Please check the attached .pdf. I have tried to prove for each issue that they do lead to wrong MRMC outputs.

[ivan.zapreev]

Issue: "2 Self-loops in Qureshi–Sanders’s Algorithm"

I do get exactly 0,69356828703 but 0.693568286937
with the error bound: 8.71e-11 we are much closer
than before but still off. Yet, there might be something
wrong with the way the error bounds are computed.