From 1e0ffc1c49afb64b3bccb7805349f079cd5dd0f3 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 17 Oct 2019 22:51:26 +0100
Subject: [PATCH] Fix format of exported transient/steady-state vectors.

Introduced in symbolic engines during recent-ish refactoring.
Seems to have been wrong in explicit engines for longer.
Format is 0=0.27109177824020264, not 0:=0.27109177824020264
---
 prism/src/explicit/StateValues.java       | 10 +++++++---
 prism/src/prism/StateAndValuePrinter.java |  8 ++++++--
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java
index f0566de1..a7366057 100644
--- a/prism/src/explicit/StateValues.java
+++ b/prism/src/explicit/StateValues.java
@@ -1706,15 +1706,19 @@ public class StateValues implements StateVector
 			} else {
 				if (printIndices) {
 					log.print(n);
-					log.print(":");
 				}
-				if (printStates && statesList != null)
+				if (printStates && statesList != null) {
+					if (printIndices) {
+						log.print(":");
+					}
 					log.print(statesList.get(n).toString());
+				}
 				if (printSparse && type instanceof TypeBool) {
 					log.println();
 				} else {
-					if (printIndices || printStates)
+					if (printIndices || printStates) {
 						log.print("=");
+					}
 					log.println(getValue(n));
 				}
 			}
diff --git a/prism/src/prism/StateAndValuePrinter.java b/prism/src/prism/StateAndValuePrinter.java
index 95443a08..2ee1772d 100644
--- a/prism/src/prism/StateAndValuePrinter.java
+++ b/prism/src/prism/StateAndValuePrinter.java
@@ -94,9 +94,12 @@ class StateAndValuePrinter implements StateAndValueConsumer
 
 		// PRISM format
 		if (printIndices) {
-			outputLog.print(stateIndex + ":");
+			outputLog.print(stateIndex);
 		}
 		if (printStates) {
+			if (printIndices) {
+				outputLog.print(":");
+			}
 			outputLog.print("(");
 			int n = varList.getNumVars();
 			for (int i = 0; i < n; i++) {
@@ -114,8 +117,9 @@ class StateAndValuePrinter implements StateAndValueConsumer
 			}
 			outputLog.print(")");
 		}
-		if (printIndices || printStates)
+		if (printIndices || printStates) {
 			outputLog.print("=");
+		}
 		outputLog.println(value);
 	}