There was a problem with computing R=?[C<=t]-like properties on CTMCs. With the rather simple 2-state model
ctmc
module main
x : [0..1] init 0;
[] x=0 -> 6 : (x'=1);
endmodule
rewards
x=0: 1;
endreward
we currently get
Model checking property "1": R=? [C<=1/10] ...
Result (for initial states): inf
Time for model checking: 0.000s.
This PR fixes the issue and adds the model as a test case.
The problem was that we are supposed to scale the values obtained before the left truncation point.
However, the case where the left truncation point is 0 was handled incorrectly: Essentially the scaling had been applied twice: once when multiplying with foxGlynnResult.weights.front() in what is now line 705 and then again with foxGlynnResult.totalWeight in line 737.
I also improved numerical stability in the weight adjustment. The previous implementation sometimes resulted in negative weights because the weights were summed up in a non-optimal order.
sjunges
commented
2 months ago
There was a problem with computing
R=?[C<=t]-like properties on CTMCs. With the rather simple 2-state modelwe currently get
This PR fixes the issue and adds the model as a test case.
The problem was that we are supposed to scale the values obtained before the left truncation point. However, the case where the left truncation point is 0 was handled incorrectly: Essentially the scaling had been applied twice: once when multiplying with
foxGlynnResult.weights.front()in what is now line 705 and then again withfoxGlynnResult.totalWeightin line 737.I also improved numerical stability in the weight adjustment. The previous implementation sometimes resulted in negative weights because the weights were summed up in a non-optimal order.