Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixed issue in computation of cumulative rewards #594

Merged
merged 1 commit into from
Aug 26, 2024

Conversation

tquatmann
Copy link
Member

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
Copy link
Contributor

sjunges commented Aug 26, 2024

LGTM

@tquatmann tquatmann merged commit 239889f into moves-rwth:master Aug 26, 2024
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants