Skip to content

Monitor verification#886

Merged
sjunges merged 47 commits intostormchecker:masterfrom
lukovdm:monitor-verification
Apr 16, 2026
Merged

Monitor verification#886
sjunges merged 47 commits intostormchecker:masterfrom
lukovdm:monitor-verification

Conversation

@lukovdm
Copy link
Copy Markdown
Contributor

@lukovdm lukovdm commented Mar 10, 2026

Add ATVA25 and AAMAS 26 monitor verification code.

lukovdm added 14 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 #885.

@sjunges sjunges mentioned this pull request Apr 13, 2026
@lukovdm lukovdm marked this pull request as ready for review April 13, 2026 15:10
Comment thread src/storm-pomdp-cli/settings/modules/GenerateMonitorVerifierSettings.cpp Outdated
Comment thread src/storm-pomdp-cli/settings/modules/GenerateMonitorVerifierSettings.h Outdated
Comment thread src/storm-parsers/parser/ValueParser.cpp Outdated
Comment thread src/storm-pomdp-cli/settings/PomdpSettings.cpp Outdated
Comment thread src/storm/modelchecker/propositional/SparsePropositionalModelChecker.h Outdated
Comment thread src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp Outdated
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp Outdated
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.h Outdated
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.h Outdated
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.h Outdated
Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.h
Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.h Outdated
Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.h Outdated
Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.h
Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.h
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp Outdated
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.cpp Outdated
Comment thread src/storm-pomdp/transformer/ObservationTraceUnfolder.h Outdated
@sjunges
Copy link
Copy Markdown
Contributor

sjunges commented Apr 13, 2026

I think this is all quite minor.
Some of the TODOs may not be urgent,
but it could be good to track them in an github issue then (under some umbrella issue) to not loose track of that.

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 only quickly skimmed through the changes and they look good to me (besides the integer types mentioned)

Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.cpp Outdated
Comment thread src/storm-pomdp/generator/GenerateMonitorVerifier.cpp Outdated
@sjunges sjunges merged commit 46cdaa8 into stormchecker:master Apr 16, 2026
22 checks passed
@lukovdm lukovdm deleted the monitor-verification branch April 17, 2026 07:33
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.

3 participants