Interval POMDPs, POSMG rewards, POSMG constraints by PurpleDragon64 · Pull Request #70 · randriu/synthesis

PurpleDragon64 · 2025-07-02T14:42:13Z

No description provided.

… initial_memory setting to POSMG; updated POSMG synthesis to display game iterations; added new test POSMG model

This reverts commit b2abb5c.

This reverts commit cc8847f.

This reverts commit a3db3b3.

This reverts commit cc731c6, reversing changes made to be04fb4.

TheGreatfpmK

Remove the pomdp/sketches from models as these are used for policy tree experiments which is not part of this PR.
Add some tests if possible

paynt/family/family.py

TheGreatfpmK · 2025-07-03T08:53:45Z

paynt/parser/drn_parser.py

                    type = line.removeprefix(cls.TYPE_PREFIX).removesuffix('\n')
-                    return type
-                raise ValueError
+                if cls.INTERVAL_BEGINNING in line:


I don't like that we are going through to whole file if it's not an interval model but I don't know how to make this better

The problem is that not all transitions in the model have to be specified as intervals for the model to be an interval pomdp. In other words: if there is at least one transition with intervals, it is an interval model. So you cannot be sure, until you check the whole file. See e.g. model models/ipomdp/simple1/sketch.templ where action 1 is not defined with intervals but action 0 is.

TheGreatfpmK · 2025-07-03T08:55:17Z

paynt/parser/sketch.py

-        if updated is not None: explicit_quotient = updated
-        if not payntbind.synthesis.assertChoiceLabelingIsCanonic(explicit_quotient.nondeterministic_choice_indices,explicit_quotient.choice_labeling,False):
-            logger.warning("WARNING: choice labeling for the quotient is not canonic")
+        # TEMPORARY FIX


Would this be difficult to implement?

TheGreatfpmK · 2025-07-03T08:56:49Z

paynt/quotient/ipomdp.py

+        self.ipomdp = ipomdp
+        self.specification = specification
+
+        logger.debug(f'ipomdp has {max(self.ipomdp.observations)+1} observations')


Why is it max() here?

The goal is to print the number of distinct observations in the model. It was now improved to not require observations to be continuous sequence of numbers starting with 0.

paynt/quotient/ipomdp.py

paynt/synthesizer/statistic.py

TheGreatfpmK · 2025-07-03T12:34:26Z

paynt/synthesizer/synthesizer_ipomdp.py

+        synthesis_timer.stop()
+        time = synthesis_timer.time
+        logger.info(f'synthesis completed, value: {round(value, 6)}, time: {round(time, 2)} s')
+        # better summary?? use Statistic class? (specification, game iterations, ...)


This would be nice to be more in line with other synthesizers

Improved by adding statistics for ipomdp

TheGreatfpmK · 2025-07-03T12:36:06Z

paynt/synthesizer/synthesizer_pomdp_onebyone.py

+import paynt.quotient.pomdp
+import paynt.synthesizer.synthesizer_ar
+
+class SynthesizerPomdpOneByOne(paynt.synthesizer.synthesizer.Synthesizer):


Do we need this one-be-one synthesis in master? I would probably remove this, I understand it was used for experiments but this is not something anyone will use in PAYNT

And if we want to keep it then I would look into how to make use of the one-by-one synthesizer that's already in PAYNT

Resolved by removing POMDP family related code.

TheGreatfpmK · 2025-07-03T12:39:16Z

paynt/quotient/ipomdp.py

+    # the new states will have new action representing combinations of lower and upper bound of the interval
+    # new states (and their actions) will be at the end of the matrix
+    # IDEA use p1state,p2state,choice(action),destination,transition,probability or originalState,newState,row,column,entry,value?
+    # IDEA return just new state count instead of new states


Clean up the comments so it's only the important stuff, if something is potential TODO add it to where it belongs

removed ideas, kept description

TheGreatfpmK · 2025-07-03T12:40:10Z

paynt/quotient/ipomdp.py

+        posmg = payntbind.synthesis.posmg_from_smg(smg, observations)
+        logger.debug(f'constructed game abstraction having {posmg.nr_states} states and {posmg.nr_choices} choices.')
+
+        return posmg


So the whole purpose of this class and all the function inside is to create the POSMG right?

Yes. And the class also stores the specification.

Copilot

Pull Request Overview

This PR adds end-to-end support for interval POMDPs by extending the parser, quotient, POSMG reward handling, and synthesizer, along with corresponding tests.

Introduce IpomdpQuotient for interval POMDP abstraction into POSMG games.
Enhance PosmgManager to construct and propagate SMG reward models.
Update DRN parser to recognize and build interval models, and wire through a new SynthesizerIpomdp.
Add a comprehensive test suite for IPOMDP abstraction and synthesis.

Reviewed Changes

Copilot reviewed 126 out of 136 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tests/ipomdp/test_ipomdp.py	New tests validating IPOMDP abstraction and solving
paynt/quotient/ipomdp.py	Implements IPOMDP-to-POSMG quotient logic
paynt/parser/drn_parser.py	Detects IPOMDP sketches and builds interval models
payntbind/src/synthesis/posmg/PosmgManager.cpp	Adds `constructRewardModel` and integrates reward models
paynt/synthesizer/synthesizer_ipomdp.py	New synthesizer class for IPOMDP using POSMG abstraction
paynt/synthesizer/policy_tree.py	Refactors game-stat logging into `log_game_stats`

Comments suppressed due to low confidence (1)

paynt/parser/drn_parser.py:56

[nitpick] Using type shadows the built-in. Consider renaming this variable to model_type or similar.

                    type = line.removeprefix(cls.TYPE_PREFIX).removesuffix('\n')

payntbind/src/synthesis/posmg/PosmgManager.cpp

paynt/synthesizer/synthesizer_ipomdp.py

Copilot · 2025-07-03T12:43:40Z

paynt/synthesizer/policy_tree.py



+    def log_game_stats(self, states, game_solver):
+        self.stat.iteration_game(states)


[nitpick] The game_solver parameter is unused in log_game_stats. Either remove it or use it for logging.

Suggested change

self.stat.iteration_game(states)

self.stat.iteration_game(states)

logger.info("Game solver stats: solution value = {}, solution state-to-action mapping size = {}".format(

game_solver.solution_value, len(game_solver.solution_state_to_player1_action)))

I said this in my review as well. Please resolve!

Resolved by removing POMDP family related code.

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

This reverts commit 25e0663, reversing changes made to cc731c6.

PurpleDragon64 and others added 30 commits July 11, 2024 11:22

add .DS_Store to .gitignore

f12d235

create POSMG class

9fed216

bind POSMG to python

66a29a5

implement POSMG parsing from .drn file

0f9c411

fix: add posmg's parent class to binding

6a47472

add case for posmg in build_quotient_container

90a1ff8

Merge branch 'randriu:master' into master

9427844

Merge remote-tracking branch 'origin/master' into posmg-manager

3993f6a

add Smg class to models.py

037fe37

rename PomdpParser to DrnParser

26d1fc4

add posmg specification parsing

ce50a91

add getMdp and getPomdp methods to Posmg class

17fff9a

rename posg to posmg

5465f40

add simple posmg to models

e9409b1

add methods to Posmg class

79d1c42

start implementing PosmgManager (constructMdp)

30df56c

finish posmg manager and posmg quotient

0983be9

improve posmg specification parsing

cbfa942

rename check_specification_for_mdp method to check_specification

668e735

implement synthesizer_posmg

2ab56c6

add action holes to non optimizing player states

565256b

override check_specification method in PosmgQuotient

a0973d0

Removed duplicate quotient unfolding for POMDP/Dec-POMDP/POSMG; added…

c70b49b

… initial_memory setting to POSMG; updated POSMG synthesis to display game iterations; added new test POSMG model

add pursuit-evasion game model

13d355d

WIP solving the MEC problem in game solver; added more test models

eae10e2

Fixed the SMG solver

af0088d

Optimized the code for producing schedulers in SMGs

68dc485

Added support for Pmin properties

9bd6c5a

fix: now accept probability specification for non-game models

7914a2e

add support for constraints in posmg quotient

aaf2079

PurpleDragon64 added 21 commits April 16, 2025 11:47

allow to set optimum threshold in ipomdp synthesizer

4fd0be2

export also sat fscs from experiments

d7b0a97

Revert "stop optimality posmg synthesis when threshold is reached"

28dbe01

This reverts commit b2abb5c.

Revert "set memory size for individual subfamilies of pomdps"

87ef0a8

This reverts commit cc8847f.

add helper script to transform parametric models to interval

6439ecd

add ipomdp models

57d2b07

delete helper script

cc76560

Merge remote-tracking branch 'upstream/master'

7909dfa

Merge branch 'posmg-rewards'

be04fb4

Merge branch 'pomdp-family'

cc731c6

Merge branch 'experiments'

25e0663

Merge branch 'interval-pomdp'

c48f216

move corridor models

97e8434

modify experiment scripts

5c94e20

add headers to files, remove clones from install.sh

a3db3b3

Revert "add headers to files, remove clones from install.sh"

f2a6601

This reverts commit a3db3b3.

delete experiments scripts

1c6a0e0

fix constraint specifications for posmg

27dcb36

Merge branch 'posmg-constraints'

74ffbd3

Revert "Merge branch 'pomdp-family'"

a9fb311

This reverts commit cc731c6, reversing changes made to be04fb4.

Merge remote-tracking branch 'upstream/master'

f182f31

TheGreatfpmK reviewed Jul 3, 2025

View reviewed changes

TheGreatfpmK requested a review from Copilot July 3, 2025 12:41

Copilot AI reviewed Jul 3, 2025

View reviewed changes

PurpleDragon64 and others added 3 commits July 3, 2025 18:24

fix typo in paynt/synthesizer/synthesizer_ipomdp.py

1fe9df9

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

Revert "Merge branch 'experiments'"

4a1142d

This reverts commit 25e0663, reversing changes made to cc731c6.

remove comments from ipomdp.py

afbeb75

PurpleDragon64 force-pushed the master branch from a74e412 to afbeb75 Compare July 3, 2025 16:46

PurpleDragon64 added 2 commits July 4, 2025 19:20

improve logging for ipomdp synthesis

0a8a68d

add simple tests for posmg synthesis

33a3478



		def log_game_stats(self, states, game_solver):
		self.stat.iteration_game(states)

Conversation

PurpleDragon64 commented Jul 2, 2025

Uh oh!

TheGreatfpmK left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull Request Overview

Reviewed Changes

Uh oh!

Uh oh!

Uh oh!

Copilot AI Jul 3, 2025

Choose a reason for hiding this comment

Uh oh!

TheGreatfpmK Jul 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

TheGreatfpmK Jul 3, 2025 •

edited

Loading