Various CSG storage fixes by davexparker · Pull Request #22 · prismmodelchecker/prism-games

davexparker · 2026-04-09T20:22:10Z

No description provided.

Copilot

Pull request overview

This PR focuses on fixing action/synchronisation label storage and indexing for concurrent stochastic games (CSGs), and updates/extends regression tests for CSG model export.

Changes:

Fix concurrent-transition action retrieval/formatting in the simulator model generator and adjust action-name sources to use synchronisations consistently.
Rework explicit CSG action handling to rely on the shared ActionList infrastructure (including extracting per-player actions from JointAction when deriving action sets).
Add/update CSG export regression fixtures and pin previously-undefined constants in a CSG test model.

Reviewed changes

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

Show a summary per file

File	Description
prism/src/simulator/ModulesFileModelGenerator.java	Fixes how concurrent transition action arrays are retrieved and how action indices are rendered to strings.
prism/src/prism/ModelGenerator.java	Removes action-index helper methods from the `ModelGenerator` interface.
prism/src/parser/ast/ModulesFile.java	Avoids adding a `null` action label to the action list for concurrent games.
prism/src/explicit/LTLModelChecker.java	Copies actions into CSG product models via the `ModelExplicit` API.
prism/src/explicit/CSGSimple.java	Removes CSG-local action-list storage; uses shared `ActionList` and adjusts idle action handling.
prism/src/explicit/ConstructModel.java	Changes when idle actions are added during CSG construction.
prism/src/explicit/ChoiceActionsSimple.java	When discovering used actions, extracts per-player actions from `JointAction` labels.
prism-tests/functionality/verify/csgs/zerosum/aloha_backoff2.prism	Pins previously-undefined constants to concrete values.
prism-tests/functionality/export/csg/medium_access2.prism	Adds a CSG model used for export regression testing.
prism-tests/functionality/export/csg/medium_access2.prism.exportmodel.auto	Adds export invocation script for the medium_access2 CSG model.
prism-tests/functionality/export/csg/medium_access2.prism.tra	Adds expected exported transitions for medium_access2.
prism-tests/functionality/export/csg/medium_access2.prism.sta	Adds expected exported state-vector info for medium_access2.
prism-tests/functionality/export/csg/medium_access2.prism.lab	Adds expected exported labels for medium_access2.
prism-tests/functionality/export/csg/medium_access2.prism1.srew	Adds expected exported state rewards (“r1”) for medium_access2.
prism-tests/functionality/export/csg/medium_access2.prism1.trew	Adds expected exported transition rewards (“r1”) for medium_access2.
prism-tests/functionality/export/csg/medium_access2.prism2.srew	Adds expected exported state rewards (“r2”) for medium_access2.
prism-tests/functionality/export/csg/medium_access2.prism2.trew	Adds expected exported transition rewards (“r2”) for medium_access2.
prism-tests/functionality/export/csg/aloha_backoff2.prism	Adds a CSG model used for export regression testing.
prism-tests/functionality/export/csg/aloha_backoff2.prism.export.auto	Adds export invocation script for the aloha_backoff2 CSG model.
prism-tests/functionality/export/csg/aloha_backoff2.prism.tra	Adds expected exported transitions for aloha_backoff2.
prism-tests/functionality/export/csg/aloha_backoff2.prism.sta	Adds expected exported state-vector info for aloha_backoff2.
prism-tests/functionality/export/csg/aloha_backoff2.prism.lab	Adds expected exported labels for aloha_backoff2.
prism-tests/functionality/export/csg/aloha_backoff2.prism.srew	Adds expected exported state rewards for aloha_backoff2.
prism-tests/functionality/export/csg/aloha_backoff2.prism.trew	Adds expected exported transition rewards for aloha_backoff2.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-04-09T20:28:09Z

-
+
+		// Add idle actions
+		if (modelType == ModelType.CSG)


csg.addIdleIndexes() is executed even when justReach is true. In that mode the CSG model instance is not constructed (so csg can be null), causing a NullPointerException during reachable-state exploration for CSGs. Guard this with !justReach (or check csg != null) so reachability-only runs work for CSG models.

Suggested change

if (modelType == ModelType.CSG)

if (!justReach && modelType == ModelType.CSG)

Copilot · 2026-04-09T20:28:09Z

 	public void addIdleIndexes()
 	{
-		int max = actions.size() + 1;
+		int max = getActions().size() + 1;
 		for (int p = 0; p < idles.length; p++) {
-			actions.add(max - 1, "<" + p + ">");
+			actionList.addAction("<" + p + ">");
 			idles[p] = max++;
 		}
 	}


addIdleIndexes() assumes each idle label is appended at the end by using max = getActions().size() + 1 and then incrementing. But ActionList.addAction() de-duplicates; if an action label like "<0>" already exists, addAction() will return an existing index and not append, leaving idles[p] inconsistent with the actual action index. Use the return value of actionList.addAction(...) (plus 1 for 1-indexing) when setting idles[p], or ensure generated idle labels cannot collide with user-defined actions.

Copilot · 2026-04-09T20:28:09Z

 	/**
 	 * Get the action label of a transition within a choice, specified by its index/offset.
 	 * The label can be any Object, but will often be treated as a string, so it should at least
 	 * have a meaningful toString() method implemented. Absence of an action label is denoted by null.
 	 * Note: For most types of models, the action label will be the same for all transitions within
 	 * the same nondeterministic choice (i.e. for each different value of {@code offset}),
 	 * but for Markov chains this may not necessarily be the case.
 	 * @param i Index of the nondeterministic choice
 	 * @param offset Index of the transition within the choice
 	 */
 	public Object getTransitionAction(int i, int offset) throws PrismException;

-	/**
-	 * Get the action label of a transition within a choice, specified by its index/offset.
-	 * This method provides the index of the action in the list of all actions,
-	 * available from {@link #getActions()}. This information is optional - only
-	 * {@link #getTransitionAction} has to be implemented, but if {@link #getActions()}
-	 * returns non-null, then you can rely on this method to work.
-	 * Absence of an action label is denoted by -1.
-	 * Note: For most types of models, the action label will be the same for all transitions within
-	 * the same nondeterministic choice (i.e. for each different value of {@code offset}),
-	 * but for Markov chains this may not necessarily be the case.
-	 * @param i Index of the nondeterministic choice
-	 * @param offset Index of the transition within the choice
-	 */
-	public default int getTransitionActionIndex(int i, int offset) throws PrismException
-	{
-		List<Object> actions;
-		if ((actions = getActions()) != null) {
-			int a = actions.indexOf(getTransitionAction(i, offset));
-			if (a != -1) {
-				return i;
-			} else {
-				throw new PrismException("Action name \"" + getTransitionAction(i, offset) + "\" is not in the list of actions");
-			}
-		} else {
-			throw new PrismException("Action index information not available");
-		}
-	}
-
 	/**


This PR removes getTransitionActionIndex() / getChoiceActionIndex() from the public ModelGenerator interface. Even if unused internally, this is a breaking API change for downstream code that depends on these helpers. Consider keeping them (and fixing/adjusting the implementation) with a deprecation cycle, or provide an alternative supported way to obtain action indices.

Actions were off by one in CSG models that include unlabelled commands. This is because, after recent model export changes, null gets included in the action list in these cases. But CSG code current hard-codes action indices that do not take this into account. Currently unlabelled commands appear only in special cases in non-player modules, so there will never be unlabelled actions in the final CSG. For now, the list is set up differently for CSGs, but it would be preferable to later align CSGs with other models in this regard.

Not currently used; will be added in PRISM and ported in. And the current implementation is inconsistent, since it does not include unlabelled ("") actions in the list.

Action indices are (1-indexed) references to list of synchronising actions from the ModulesFile. Currently this coincides with getActions(), but that will not always be true.

Also update findActionsUsed to handle joint actions, although this is not currently needed since the action list for CSGs is set up front to allow action indexing. Also remove CSGSimple.getActionsForPlayer (unused, and seems broken).

Triggered by, e.g.: prism-games ../prism-examples/csgs/aloha/aloha_backoff2.prism -const bcmax=2,D=8,q=0.9 -simpath 10 stdout

davexparker requested a review from Copilot April 9, 2026 20:22

Copilot started reviewing on behalf of davexparker April 9, 2026 20:23 View session

Copilot AI reviewed Apr 9, 2026

View reviewed changes

davexparker force-pushed the csg branch from f7e7bd6 to 4fbd2be Compare April 9, 2026 20:35

davexparker added 6 commits April 9, 2026 21:44

CSG model export regression tests.

4ce4432

Remove (for now) action index querying from ModelGenerator.

131e9ec

Not currently used; will be added in PRISM and ported in. And the current implementation is inconsistent, since it does not include unlabelled ("") actions in the list.

ModulesFileModelGenerator fix: use correct action list.

fdc0ed2

Action indices are (1-indexed) references to list of synchronising actions from the ModulesFile. Currently this coincides with getActions(), but that will not always be true.

Bug fix in getTransitionAction for CSGs.

14ead6a

Triggered by, e.g.: prism-games ../prism-examples/csgs/aloha/aloha_backoff2.prism -const bcmax=2,D=8,q=0.9 -simpath 10 stdout

Small CSG model construction fix.

2da8158

davexparker force-pushed the csg branch from 4fbd2be to 2da8158 Compare April 9, 2026 20:47

davexparker merged commit 6cd6655 into prismmodelchecker:master Apr 9, 2026
6 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Various CSG storage fixes#22

Various CSG storage fixes#22
davexparker merged 7 commits into
prismmodelchecker:masterfrom
davexparker:csg

davexparker commented Apr 9, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Apr 9, 2026

Uh oh!

Copilot AI Apr 9, 2026

Uh oh!

Copilot AI Apr 9, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	if (modelType == ModelType.CSG)
	if (!justReach && modelType == ModelType.CSG)

Uh oh!

Conversation

davexparker commented Apr 9, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Apr 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 9, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants