Output player info when loading/building games models.

prismmodelchecker · Jul 2, 2024 · 571a846 · 571a846
1 parent 4eaf933
commit 571a846
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java
@@ -45,6 +45,7 @@
 import parser.VarList;
 import prism.Evaluator;
 import prism.ModelType;
+import prism.PlayerInfoOwner;
 import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLog;
@@ -645,6 +646,9 @@ public default String infoString()
 	{
 		final int numStates = getNumStates();
 		String s = "";
+		if (this instanceof PlayerInfoOwner) {
+			s += ", " + ((PlayerInfoOwner) this).getNumPlayers() + " observables";
+		}
 		s += numStates + " states (" + getNumInitialStates() + " initial)";
 		if (this instanceof PartiallyObservableModel) {
 			s += ", " + ((PartiallyObservableModel) this).getNumObservations() + " observables";
@@ -665,6 +669,9 @@ public default String infoStringTable()
 	{
 		final int numStates = getNumStates();
 		String s = "";
+		if (this instanceof PlayerInfoOwner) {
+			s += "Players:     " + ((PlayerInfoOwner) this).getNumPlayers() + "\n";
+		}
 		s += "States:      " + numStates + " (" + getNumInitialStates() + " initial)\n";
 		if (this instanceof PartiallyObservableModel) {
 			s += "Obs/unobs:   " + ((PartiallyObservableModel) this).getNumObservations() + "/" + ((PartiallyObservableModel) this).getNumUnobservations() + "\n";

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
@@ -1632,6 +1632,9 @@ public void loadPRISMModel(ModulesFile modulesFile) throws PrismException
 		// Print basic model info
 		mainLog.println();
 		mainLog.println("Type:        " + currentModelInfo.getModelType());
+		if (currentModulesFile.getModelType().multiplePlayers()) {
+			mainLog.println("Players:     " + String.join(" ", currentModulesFile.getPlayerNames()));
+		}
 		mainLog.println("Modules:     " + String.join(" ", currentModulesFile.getModuleNames()));
 		mainLog.println("Variables:   " + String.join(" ", currentModelInfo.getVarNames()));
 		if (currentModulesFile.getModelType().partiallyObservable()) {