Model export + import improvements/refactoring

CHANGELOG.txt

@@ -1,18 +1,19 @@
 This file contains details of the changes in each new version of PRISM.
 
 -----------------------------------------------------------------------------
-Changes since last release (up to f25c788dd)
+Changes since last release (up to 4fc1eaed3)
 -----------------------------------------------------------------------------
 
 * Explicit engine improvements
   - support for transition rewards in Markov chains
   - storage (and export) of actions for Markov chains
 
-* Model export functionality (explicit engine)
+* Model export functionality
   - export of exact and parametric models
   - preliminary DRN (Storm) output
-  - actions=true/false option
-  - remove old options (MRMC format, unordered)
+  - actions=true/false option (explicit engine)
+  - multiple -exportmodel allowed and format=x option
+  - remove old options (MRMC format, unordered, spy)
 
 * Model import functionality (from explicit files)
   - import of transition rewards
@@ -32,17 +33,19 @@ Changes since last release (up to f25c788dd)
 * Various bugfixes
 
 * Development and code-level changes
-  - prism.Prism API: new model export methods
+  - prism.Prism API: new/updated model export methods
   - prism.Prism API: remove some old deprecated methods
   - prism.Prism: refactored storage/access for model info
   - prism.Prism: integration of exact model building/checking
+  - improved access to actions and their indices in models
   - redesign/refactoring of explicit engine reward classes
   - refactoring of explicit engine model import/export code
     (centralised in io package, export moved from model classes)
   - parametric engine refactored to use explicit models/rewards
   - symbolic code rearranged (new symbolic package)
   - symbolic model storage refactored, simplified, documented
   - extension of strategy classes, especially for induced models
+  - Java-based symbolic-to-explicit model conversion
   - prism-auto: --errors-only switch
 
 * [More minor development and code-level changes]
@@ -55,6 +58,7 @@ Changes since last release (up to f25c788dd)
   - VarList aware of EvaluationContext/EvalMode
   - parametric engine: improved error reporting and formatting
   - prism.API: exportprism moved from setting to API call
+  - model export refactoring, including ModelExportTask
 
 -----------------------------------------------------------------------------
 Version 4.8.1 (first released 13/1/2024)

prism-tests/functionality/import/dice-deadlock.lab

@@ -0,0 +1,8 @@
+0="init" 1="deadlock" 2="end" 3="six"
+0: 0
+7: 1 2
+8: 1 2
+9: 1 2
+10: 1 2
+11: 1 2
+12: 1 2 3

prism-tests/functionality/import/dice-deadlock.pm.importexport.auto

@@ -0,0 +1,2 @@
+-importmodel dice-deadlock.tra,lab -exportmodel dice-deadlock.tra,lab
+-importmodel dice-deadlock.tra,lab -exportmodel dice-deadlock.tra,lab -ex

prism-tests/functionality/import/dice-deadlock.pm.orig

@@ -0,0 +1,26 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+
+	[] s=0 -> 1/2 : (s'=1) + 1/2 : (s'=2);
+	[] s=1 -> 1/2 : (s'=3) + 1/2 : (s'=4);
+	[] s=2 -> 1/2 : (s'=5) + 1/2 : (s'=6);
+	[] s=3 -> 1/2 : (s'=1) + 1/2 : (s'=7) & (d'=1);
+	[] s=4 -> 1/2 : (s'=7) & (d'=2) + 1/2 : (s'=7) & (d'=3);
+	[] s=5 -> 1/2 : (s'=7) & (d'=4) + 1/2 : (s'=7) & (d'=5);
+	[] s=6 -> 1/2 : (s'=2) + 1/2 : (s'=7) & (d'=6);
+//	[] s=7 -> (s'=7);
+
+endmodule
+
+label "end" = s=7;
+label "six" = d=6;
+
+rewards "coin_flips"
+	s<7 : 1;
+endrewards

prism-tests/functionality/import/dice-deadlock.tra

@@ -0,0 +1,21 @@
+13 20
+0 1 0.5
+0 2 0.5
+1 3 0.5
+1 4 0.5
+2 5 0.5
+2 6 0.5
+3 1 0.5
+3 7 0.5
+4 8 0.5
+4 9 0.5
+5 10 0.5
+5 11 0.5
+6 2 0.5
+6 12 0.5
+7 7 1
+8 8 1
+9 9 1
+10 10 1
+11 11 1
+12 12 1

prism-tests/functionality/import/dtmc-deadlocks-fixed.lab

@@ -0,0 +1,5 @@
+0="init" 1="deadlock"
+0: 0
+2: 1
+3: 1
+5: 1

prism-tests/functionality/import/dtmc-deadlocks-fixed.tra

@@ -0,0 +1,9 @@
+6 8
+0 0 0.4 east
+0 1 0.6 east
+1 2 0.5 south
+1 4 0.5 south
+2 2 1
+3 3 1
+4 5 1 east
+5 5 1

prism-tests/functionality/import/dtmc-deadlocks.tra

@@ -0,0 +1,6 @@
+6 5
+0 0 0.4 east
+0 1 0.6 east
+1 2 0.5 south
+1 4 0.5 south
+4 5 1 east

prism-tests/functionality/import/dtmc-deadlocks.tra.importexport.auto

@@ -0,0 +1 @@
+-importmodel dtmc-deadlocks.tra -exportmodel dtmc-deadlocks-fixed.tra,lab -ex

prism-tests/functionality/import/mdp-deadlocks-fixed.lab

@@ -0,0 +1,5 @@
+0="init" 1="deadlock"
+0: 0
+2: 1
+3: 1
+5: 1

prism-tests/functionality/import/mdp-deadlocks-fixed.tra

@@ -0,0 +1,9 @@
+6 6 8
+0 0 0 0.4 east
+0 0 1 0.6 east
+1 0 2 0.5 south
+1 0 4 0.5 south
+2 0 2 1
+3 0 3 1
+4 0 5 1 east
+5 0 5 1

prism-tests/functionality/import/mdp-deadlocks.tra

@@ -0,0 +1,6 @@
+6 3 5
+0 0 0 0.4 east
+0 0 1 0.6 east
+1 0 2 0.5 south
+1 0 4 0.5 south
+4 0 5 1 east

prism-tests/functionality/import/mdp-deadlocks.tra.importexport.auto

@@ -0,0 +1 @@
+-importmodel mdp-deadlocks.tra -exportmodel mdp-deadlocks-fixed.tra,lab -ex

prism-tests/functionality/import/mdp_simple_mod.auto

@@ -0,0 +1 @@
+-importmodel mdp_simple_mod.tra -exportmodel mdp_simple.tra

prism-tests/functionality/import/mdp_simple_mod.tra

@@ -0,0 +1,21 @@
+10 15 20
+0 0 1 0.1 b
+0 0 2 0.9 b
+0 1 3 1 a
+1 0 1 1 
+2 0 2 1
+3 0 1 0.2 b
+3 0 2 0.8 b
+3 1 6 1 a
+4 0 4 1
+5 0 5 1
+6 0 4 0.3 b
+6 0 5 0.7 b
+6 1 7 1 a
+7 0 1 0.4 b
+7 0 2 0.6 b
+7 1 8 1 a
+8 0 1 0.5 b
+8 0 2 0.5 b
+8 1 9 1 a
+9 0 1 1

prism-tests/functionality/import/robot.prism.importcheck.auto.disabled

@@ -1,2 +1,2 @@
--mdp -importmodel robot.all robot.prism.props
--mdp -importmodel robot.all robot.prism.props -ex
+-importmodel robot.all robot.prism.props
+-importmodel robot.all robot.prism.props -ex

prism-tests/functionality/import/robot.prism.props

@@ -1,2 +1,17 @@
-// RESULT: 0.1
-Pmax=? [ (G !"hazard")&(G F "goal1") ]
+// RESULT: Infinity
+Rmin=? [ F "goal1" ]
+
+// RESULT: Infinity
+Rmax=? [ F "goal1" ]
+
+// RESULT: 19/15
+Rmin=? [ F "goal2" ]
+
+// RESULT: Infinity
+Rmax=? [ F "goal2" ]
+
+// RESULT: 1.2
+Rmin=? [ F ("goal1"|"goal2") ]
+
+// RESULT: 3.5
+Rmax=? [ F ("goal1"|"goal2") ]

prism/src/explicit/ChoiceActionsSimple.java

@@ -27,6 +27,10 @@
 package explicit;
 
 import java.util.ArrayList;
+import java.util.Collections;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.function.IntUnaryOperator;
 
 /**
  * Explicit-state storage of the action labels attached to choices in a model.
@@ -154,6 +158,56 @@ public void setAction(int s, int i, Object action)
 
 	// Accessors
 
+	/**
+	 * Produce a list of the action labels attached to choices/transitions.
+	 * Absence of an action label is denoted by null,
+	 * and null is also included in this list if there are unlabelled choices/transitions.
+	 * @param numStates The number of states in the model
+	 * @param counts A function giving the number of choices/transitions for each state
+	 */
+	public List<Object> findActionsUsed(int numStates, IntUnaryOperator counts)
+	{
+		if (actions == null) {
+			// Null storage means all choices/transitions are unlabelled
+			return Collections.singletonList(null);
+		} else {
+			LinkedHashSet<Object> allActions = new LinkedHashSet<>();
+			int numStatesStored = actions.size();
+			for (int s = 0; s < numStatesStored; s++) {
+				ArrayList<Object> list = actions.get(s);
+				if (list == null) {
+					// Null list means any/all choices/transitions are unlabelled for s
+					if (counts.applyAsInt(s) > 0) {
+						allActions.add(null);
+					}
+				} else {
+					allActions.addAll(list);
+					if (list.size() < counts.applyAsInt(s)) {
+						// Undersized list means there are unlabelled choices/transitions
+						allActions.add(null);
+					}
+				}
+			}
+			for (int s = numStatesStored; s < numStates; s++) {
+				// Missing list means any/all choices/transitions are unlabelled for s
+				if (counts.applyAsInt(s) > 0) {
+					allActions.add(null);
+				}
+			}
+			return new ArrayList<>(allActions);
+		}
+	}
+
+	/**
+	 * Do all choices/transitions have empty (null) action labels?
+	 */
+	public boolean onlyNullActionUsed()
+	{
+		// NB: it's still possible that action storage has been created but has ended up all null
+		// We ignore this possibility
+		return actions == null;
+	}
+
 	/**
 	 * Get the action label for choice {@code i} of state {@code s}.
 	 */

prism/src/explicit/DTMC.java

@@ -29,10 +29,13 @@
 import java.io.FileWriter;
 import java.io.IOException;
 import java.util.AbstractMap;
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.BitSet;
+import java.util.Collections;
 import java.util.Iterator;
-import java.util.Map;
+import java.util.LinkedHashSet;
+import java.util.List;
 import java.util.Map.Entry;
 import java.util.PrimitiveIterator;
 import java.util.PrimitiveIterator.OfInt;
@@ -43,12 +46,10 @@
 import common.iterable.FunctionalIterator;
 import common.iterable.PrimitiveIterable;
 import common.iterable.Reducible;
-import explicit.graphviz.Decorator;
 import explicit.rewards.MCRewards;
 import prism.ModelType;
 import prism.Pair;
 import prism.PrismException;
-import prism.PrismLog;
 
 /**
  * Interface for classes that provide (read) access to an explicit-state DTMC.
@@ -92,7 +93,25 @@ default void exportToPrismLanguage(final String filename, int precision) throws
 	}
 
 	// Accessors
-
+
+	@Override
+	default List<Object> findActionsUsed()
+	{
+		// Find unique actions across all transitions
+		if (onlyNullActionUsed()) {
+			return Collections.singletonList(null);
+		}
+		LinkedHashSet<Object> actions = new LinkedHashSet<>();
+		int numStates = getNumStates();
+		for (int s = 0; s < numStates; s++) {
+			for (Iterator<Entry<Integer, Pair<Value, Object>>> transitions = getTransitionsAndActionsIterator(s); transitions.hasNext();) {
+				final Entry<Integer, Pair<Value, Object>> transition = transitions.next();
+				actions.add(transition.getValue().second);
+			}
+		}
+		return new ArrayList<>(actions);
+	}
+
 	/**
 	 * Get an iterator over the transitions from state s.
 	 */
@@ -108,6 +127,42 @@ public default Iterator<Entry<Integer, Pair<Value, Object>>> getTransitionsAndAc
 		return Reducible.extend(transitions).map(transition -> attachAction(transition, null));
 	}
 
+	/**
+	 * Get an iterator over the actions attached to transitions from state s.
+	 */
+	public default Iterator<Object> getActionsIterator(int s)
+	{
+		// Default implementation just assumes null actions
+		return Collections.nCopies(getNumTransitions(s), null).iterator();
+	}
+
+	/**
+	 * Get an iterator over the indices of actions attached to transitions from state s.
+	 * Indices are into the list given by {@link #getActions()},
+	 * which includes null if there are unlabelled choices,
+	 * so this method should always return values >= 0.
+	 */
+	public default PrimitiveIterator.OfInt getActionIndicesIterator(int s)
+	{
+		// Default implementation looks up indices from getActionsIterator
+		return new PrimitiveIterator.OfInt()
+		{
+			private final Iterator<Object> iter = getActionsIterator(s);
+
+			@Override
+			public boolean hasNext()
+			{
+				return iter.hasNext();
+			}
+
+			@Override
+			public int nextInt()
+			{
+				return actionIndex(iter.next());
+			}
+		};
+	}
+
 	/**
 	 * Get an iterator over the transitions from state {@code s},
 	 * after mapping probability values using the provided function.