Skip to content

iMC changes inside of storm-pars#640

Merged
tquatmann merged 215 commits intostormchecker:masterfrom
linusheck:robustpla
Nov 17, 2025
Merged

iMC changes inside of storm-pars#640
tquatmann merged 215 commits intostormchecker:masterfrom
linusheck:robustpla

Conversation

@linusheck
Copy link
Copy Markdown
Contributor

@linusheck linusheck commented Nov 19, 2024 •
edited
Loading

  • Added BigStep transformation, generalised parameter lifting, support for not-graph-preserving regions and not-well-defined regions in PL
  • Updated the region verification API to use a consolidated RefinementOptions struct
  • Added iMC end component elimination
  • Added region support to gradient descent
  • Updated code in storm-pars to use std::optional instead of boost::optional for optional values
  • Moved various monotonicity-related files to more appropriate locations

linusheck and others added 30 commits February 12, 2024 16:33
@linusheck
Add Robust Parameter Lifting Algorithm
e16f242
@linusheck
Merge branch 'master' of github.com:moves-rwth/storm into robustpla
0d0675c
@linusheck
First version of horizon-bounded big-step and time-travelling
b829776
@linusheck
applyRowRobust optimization
fd8acbe
@linusheck
Revert changes in ValueIterationOperator.cpp
7cae91c
@linusheck
Add support for ill-defined regions
0e06f0c
@linusheck
Revert "Revert changes in ValueIterationOperator.cpp"
f2571c3 
This reverts commit 7cae91c.
@linusheck
WIP commit
135619b
@linusheck
Revert "Revert "Revert changes in ValueIterationOperator.cpp""
4b94de0 
This reverts commit f2571c3.
@linusheck
Best version of robust value iteration
bee2544
@linusheck
Fix: copy x here
49e2860
@tquatmann
New RegionRefinementChecker and AnnotatedRegion (work in progress)
a9f25c2
@linusheck
Almost works?
5a97d3d
@tquatmann
towards compiling again and a simpler ValidatingSparseParameterLiftin…
28f51ac 
…gModelChecker (work in progress)
@linusheck
A lot of stuff, everywhere
af044ee
@linusheck
Format
ac1d2f4
@linusheck
WIP refactor of TimeTravelling.cpp (does not compile yet)
d432df3
@tquatmann
towards compiling again and OrderBasedMonotonicityBackend (work in pr…
9c0ccc4 
…ogress)
@tquatmann
Finally compiling again. Not tested yet.
105b9d9
@tquatmann
work on order-based monotonicity backend & various fixes
d3cee7f
@tquatmann
Fixed build with cln numbers
878fe6f
@linusheck
refactor time-travelling
b325ea3
@linusheck
whoops
5f75b2a
@tquatmann
Fixed build with cln numbers [Part 2]
23d92f8
@linusheck
Fix cubicEquationZeroes code
faa786d
@tquatmann
3 fixes
b12e273
@linusheck
Correct preprocessing for b-vectors with intervals in ValueIterationH…
bd610ac 
…elper.h
@linusheck
Merge branch 'master' of github.com:moves-rwth/storm into robustpla
03c9f5d
@linusheck
Optimize time-travelling
26f31d6
@linusheck
Fix non-const ASSERT statement that broke in release mode
1595d86
sjunges
sjunges reviewed Oct 3, 2025
View reviewed changes
Comment thread src/storm-pars/api/analysis.h Outdated
sjunges
sjunges reviewed Oct 3, 2025
View reviewed changes
Comment thread src/storm-pars/transformer/BigStep.h Outdated
@linusheck
Copy link
Copy Markdown
Contributor Author

linusheck commented Oct 3, 2025 •
edited
Loading

whoops (will fix the CI on monday)

@linusheck
Copy link
Copy Markdown
Contributor Author

linusheck commented Oct 20, 2025

This is done from my side :)

sjunges
sjunges reviewed Oct 20, 2025
View reviewed changes
Comment thread src/storm-pars/parser/ParameterRegionParser.cpp Outdated
tquatmann
tquatmann approved these changes Nov 5, 2025
View reviewed changes
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.

I have a few nitpickings, but nothing serious. LGTM!

Comment thread src/storm-pars-cli/storm-pars.cpp
Comment thread src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp Outdated
Comment thread src/test/storm-pars/transformer/BigStepTest.cpp
Comment thread src/storm/adapters/RationalFunctionForward.h
@sjunges
Copy link
Copy Markdown
Contributor

sjunges commented Nov 7, 2025

My final suggestion. Make the PR description a bit clearer, in case we ever have to look up what changed here.

@tquatmann
Copy link
Copy Markdown
Contributor

tquatmann commented Nov 17, 2025

This can be merged now, right? :)

@linusheck
Copy link
Copy Markdown
Contributor Author

linusheck commented Nov 17, 2025

I think so

@tquatmann tquatmann merged commit a98b94d into stormchecker:master Nov 17, 2025
19 checks passed
This was referenced Nov 17, 2025
Closed
Merged
@tquatmann tquatmann mentioned this pull request Feb 1, 2026
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sjunges sjunges sjunges left review comments

@tquatmann tquatmann tquatmann approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

1.12

Development

Successfully merging this pull request may close these issues.

3 participants

@linusheck @sjunges @tquatmann