Strange NaN result for multi-objective

[kleinj]

We are seeing a strange result for the following (heavily minimized) model:

mdp

module m
    loc : bool init true;
    yes : bool init false;

    [a] true -> 0.994005 : (loc'=true) + 0.000995 : (loc'=false) + 0.005  : true ;
    [g] true -> (yes'=true);
endmodule

Properties:

multi(Pmax=?[F false], P<=0.003[F yes])    // NaN
multi(Pmax=?[F false], P<=0.004[F yes])    // 0
multi(Pmax=?[F false], Pmin=?[F yes])      // [(0.0,0.0)]

We'd expect 0 for the first query as well.

This is using the default settings, if we switch to using the LP solver, we get the expected output. Increasing the termination epsilon does not seem to help.

Is this just due to the fact that the Pmax yields 0? I.e., could one add some pre-check that one of the target sets is empty or not reachable? Or is there something numerically going wrong?

Verbose log output for computation of the first query:

The initial target point is (1.0, 0.997)
The initial direction is (0.5007511266900351, 0.499248873309965)
Iterative method: 6 iterations in 0.00 seconds (average 0.000000, setup 0.00)
Optimal value for weights [0.500751,0.499249] from initial state: 0.499249
New point is (0.0, 9.999999999968754E-4).
Decided, target is (NaN, 0.997)
The value iteration(s) took 0.0 seconds altogether.
Number of weight vectors used: 1
Multi-objective value iterations took 0.0 s.

Value in the initial state: NaN

With smaller epsilon:

The initial target point is (1.0, 0.997)
The initial direction is (0.5007511266900351, 0.499248873309965)
Iterative method: 8 iterations in 0.00 seconds (average 0.000000, setup 0.00)
Optimal value for weights [0.500751,0.499249] from initial state: 0.499249
New point is (0.0, 0.0010000000000000002).
Decided, target is (NaN, 0.997)

And the second one:

The initial target point is (1.0, 0.996)
The initial direction is (0.501002004008016, 0.49899799599198397)
Iterative method: 2 iterations in 0.00 seconds (average 0.000000, setup 0.00)
Optimal value for weights [0.501002,0.498998] from initial state: 0.498998
New point is (0.0, 1.0).
Target lowered to (0.003984000000000114, 0.996)
New direction is (1.0, 0.0)
Iterative method: 2 iterations in 0.00 seconds (average 0.000000, setup 0.00)
Optimal value for weights [1.000000,0.000000] from initial state: 0.000000
New point is (0.0, 0.0).
Target lowered to (0.0, 0.996)
New direction is null
The value iteration(s) took 0.001 seconds altogether.
Number of weight vectors used: 2
Multi-objective value iterations took 0.001 s.

Value in the initial state: 0.0