Skip to content

Conditional model checking#887

Open
lukovdm wants to merge 54 commits intostormchecker:masterfrom
lukovdm:conditional-model-checking
Open

Conditional model checking#887
lukovdm wants to merge 54 commits intostormchecker:masterfrom
lukovdm:conditional-model-checking

Conversation

@lukovdm
Copy link
Copy Markdown
Contributor

@lukovdm lukovdm commented Mar 10, 2026

No description provided.

lukovdm added 13 commits March 11, 2026 13:42
…related components and added tests

- Updated AddUncertainty transformer to handle RationalNumber types, allowing for exact arithmetic with RationalInterval.
- Modified various helper functions and model checkers to accommodate RationalNumber and RationalInterval.
- Introduced new tests for RationalNumber scenarios in model checking and uncertainty transformations.
- Ensured compatibility with existing models while expanding functionality for uncertain models using RationalNumber.
@lukovdm
Copy link
Copy Markdown
Contributor Author

lukovdm commented Apr 9, 2026

This PR builds on top of #886.

@lukovdm
Copy link
Copy Markdown
Contributor Author

lukovdm commented Apr 17, 2026

The failing tests have to deal with some irritating floating point errors leading to incorrect values for pMin and pMax in bisection advanced. The failing test specifically has a pMax that is about 10^-9 below the true value. This is also outside the standard 10^-12 bound we keep for floating point comparisons. The result of the floating point error is a lower bound > 1 by about 10^-6 (i.e. 1.0000001). I am not entirely sure how to tackle this. Using the conditional tolerance does not seem right.

@sjunges
Copy link
Copy Markdown
Contributor

sjunges commented Apr 19, 2026

Without sound methods in the backend, this can indeed happen. I would mark the tests as skip/expect fail maybe. We should probably open an issue to ensure that we have the ability to run this with a sound backend and make sure that we test the logic with exact arithmetic as well.

Comment thread src/storm/environment/modelchecker/ModelCheckerEnvironment.cpp Outdated
Comment thread src/storm/environment/modelchecker/ModelCheckerEnvironment.h Outdated
Comment thread src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp Outdated
Comment thread src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp Outdated
Comment thread src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp Outdated
Comment thread src/storm/utility/constants.cpp Outdated
Comment thread src/test/storm/modelchecker/prctl/mdp/ConditionalMdpPrctlModelCheckerTest.cpp Outdated
@lukovdm lukovdm marked this pull request as ready for review April 21, 2026 08:35
Copy link
Copy Markdown
Contributor

@tquatmann tquatmann left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the PR! Great Work :)

I have some of the usual nitpickings.

Most importantly, I'm not a big fan of introducing the top level tolerance in this PR because it would (for now) only apply to conditional probabilities.

Also, --minmax:precision 0 might have some weird side-effects that we are currently unaware of.

Comment thread src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp Outdated
Comment thread src/storm/modelchecker/helper/conditional/ConditionalHelper.h Outdated
Comment thread src/storm/modelchecker/CheckTask.h Outdated
Comment thread src/storm/modelchecker/CheckTask.h Outdated
Comment thread src/storm/settings/modules/MinMaxEquationSolverSettings.cpp Outdated
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/SettingsManager.h"
#include "storm/utility/constants.h"
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why does this include become necessary?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These were left over after removing conditional tolerance. But since they are now back this is necessary again.

#pragma once

#include "storm-config.h"
#include "storm/adapters/RationalNumberAdapter.h"
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Necessary?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(Without having any knowledge of the rest) Is it possible to use RationalNumberForward here? I think this include spreads through some parts of the code base and it would be best if we could avoid including the header here.

Comment thread src/storm/utility/constants.h Outdated
Comment thread src/test/storm/modelchecker/prctl/mdp/ConditionalMdpPrctlModelCheckerTest.cpp Outdated
Comment thread src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp Outdated
@sjunges
Copy link
Copy Markdown
Contributor

sjunges commented Apr 21, 2026

precision zero should not be necessary anymore if the precision does not control the tolerance... I think tolerance was introduced exactly to also allow non-zero precision in the exact case.

@tquatmann
Copy link
Copy Markdown
Contributor

Ahh, I see. Exact arithmetics with non-exact solutions is something that we can't really specify right now.

Imo, the current solution is a bit unclear (what is the difference between tolerance vs. precision?). But it's also not obvious to me how to solve this. Do we have to introduce support for that in this PR?

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.

5 participants