Deal with module/model alphabets properly in PTAs, in particular when storing PTAs internally using pta.PTA. The definition of the alphabet of a PTA from a PRISM model is now correct and inline with the defition for other models.

Fixes https://github.com/prismmodelchecker/prism/issues/10



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11770 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/ast/Module.java

@@ -46,6 +46,8 @@ public class Module extends ASTElement
 	private ModulesFile parent;
 	// Base module (if was constructed through renaming; null if not)
 	private String baseModule;
+	// Alphabet (if defined explicitly rather than deduced from syntax)
+	private Vector<String> alphabet;
 
 	// Constructor
 	
@@ -113,6 +115,16 @@ public class Module extends ASTElement
 		baseModule = b;
 	}
 	
+	/**
+	 * Optionally, define the alphabet (of actions that can label transitions) for this module.
+	 * Normally, this is deduced syntactically (as the set of actions appearing in commands)
+	 * but you can override this if you want. Pass null to un-override;
+	 */
+	public void setAlphabet(List<String> alphabet)
+	{
+		this.alphabet = (alphabet == null) ? null : new Vector<String>(alphabet); 
+	}
+	
 	// Get methods
 	
 	public String getName()
@@ -195,9 +207,15 @@ public class Module extends ASTElement
 	 * Get the set of synchronising actions of this module, i.e. its alphabet.
 	 * Note that the definition of alphabet is syntactic: existence of an a-labelled command in this
 	 * module ensures that a is in the alphabet, regardless of whether the guard is true.
+	 * The alphabet for a module can also be overridden using {@link #setAlphabet(List)}
 	 */
 	public Vector<String> getAllSynchs()
 	{
+		// If overridden, use this
+		if (alphabet != null) {
+			return alphabet;
+		}
+		// Otherwise, deduce syntactically
 		int i, n;
 		String s;
 		Vector<String> allSynchs = new Vector<String>();

prism/src/pta/DBMList.java

@@ -559,7 +559,7 @@ public class DBMList extends NCZone
 		int numClocks = 7;
 		int i, j, x, y, db;
 		Random generator = new Random();
-		PTA pta = new PTA();
+		PTA pta = new PTA(Collections.emptyList());
 		for (i = 0; i < numClocks; i++) {
 			pta.addClock("" + i);
 		}

prism/src/pta/Modules2PTA.java

@@ -195,7 +195,7 @@ public class Modules2PTA extends PrismComponent
 		}
 
 		// Create new PTA and add a clock for each clock variable
-		pta = new PTA();
+		pta = new PTA(new ArrayList<String>(module.getAllSynchs()));
 		for (String clockName : clocks)
 			pta.addClock(clockName);
 
@@ -546,6 +546,9 @@ public class Modules2PTA extends PrismComponent
 
 		// Create a new module
 		moduleNew = new Module(module.getName());
+		
+		// Preserve alphabet of old module (might change if some commands are not enabled)
+		moduleNew.setAlphabet(module.getAllSynchs());
 
 		// Create invariant - will be constructed below
 		invarNew = null;

prism/src/pta/PTA.java

@@ -50,14 +50,18 @@ public class PTA
 	protected int numTransitions;
 	protected ArrayList<ArrayList<Transition>> transitions;
 	// Alphabet
-	protected Set<String> alphabet;
+	protected List<String> alphabet;
 	// Maximum clock constraint value
 	protected int cMax;
 
 	/**
-	 * Constructor
+	 * Constructor: build an empty PTA.
+	 * 
+	 * @param alphabet The set of (non-tau) actions that can label transitions.
+	 * This is *syntactically* defined, e.g., in PRISM it's the list of all actions appearing in commands,
+	 * but may be a strict superset of the actions that actually label transitions.
 	 */
-	public PTA()
+	public PTA(List<String> alphabet)
 	{
 		numClocks = 0;
 		clockNames = new ArrayList<String>();
@@ -67,7 +71,7 @@ public class PTA
 		locationNameVars = null;
 		numTransitions = 0;
 		transitions = new ArrayList<ArrayList<Transition>>();
-		alphabet = new LinkedHashSet<String>();
+		this.alphabet = alphabet;
 		cMax = 0;
 	}
 
@@ -143,8 +147,6 @@ public class PTA
 	{
 		if (action == null)
 			action = "";
-		else
-			alphabet.add(action);
 		Transition transition = new Transition(this, loc, action);
 		ArrayList<Transition> list = transitions.get(loc);
 		list.add(transition);
@@ -158,7 +160,6 @@ public class PTA
 	public void addTransition(Transition transition)
 	{
 		transition.setParent(this);
-		alphabet.add(transition.getAction());
 		ArrayList<Transition> list = transitions.get(transition.getSource());
 		list.add(transition);
 		numTransitions++;
@@ -267,7 +268,7 @@ public class PTA
 		return cMax;
 	}
 
-	public Set<String> getAlphabet()
+	public List<String> getAlphabet()
 	{
 		return alphabet;
 	}
@@ -417,7 +418,7 @@ public class PTA
 		PTA pta;
 		Transition t;
 		Edge e;
-		pta = new PTA();
+		pta = new PTA(Collections.emptyList());
 		int x = pta.addClock("x");
 		int y = pta.addClock("y");
 		pta.addLocation(); // L0

prism/src/pta/PTAParallel.java

@@ -52,34 +52,23 @@ public class PTAParallel
 	 */
 	public PTA compose(PTA pta1, PTA pta2)
 	{
-		Set<String> alpha1, alpha2, alpha1only, alpha2only, sync;
 		Transition transition;
 		Edge edge;
 		double prob;
 		IndexPair state;
 		int src, dest;
 
-		// Store PTAs locally and create new one to store parallel composition
+		// Store PTAs locally
 		this.pta1 = pta1;
 		this.pta2 = pta2;
-		par = new PTA();
 
-		// New set of clocks is union of sets for two PTAs
-		for (String s : pta1.clockNames) {
-			par.getOrAddClock(s);
-		}
-		for (String s : pta2.clockNames) {
-			par.getOrAddClock(s);
-		}
-
-		// Get alphabets, compute intersection etc.
-		alpha1 = pta1.getAlphabet();
-		alpha2 = pta2.getAlphabet();
-		//System.out.println("alpha1: " + alpha1);
-		//System.out.println("alpha2: " + alpha2);
-		sync = new LinkedHashSet<String>();
-		alpha1only = new LinkedHashSet<String>();
-		alpha2only = new LinkedHashSet<String>();
+		// Get alphabets, compute intersection, union etc.
+		List<String> alpha1 = pta1.getAlphabet();
+		List<String> alpha2 = pta2.getAlphabet();
+		LinkedHashSet<String> sync = new LinkedHashSet<String>();
+		LinkedHashSet<String> alpha1only = new LinkedHashSet<String>();
+		LinkedHashSet<String> alpha2only = new LinkedHashSet<String>();
+		List<String> alphaUnion = new ArrayList<String>(pta1.getAlphabet());
 		for (String a : alpha1) {
 			if (!("".equals(a)) && alpha2.contains(a)) {
 				sync.add(a);
@@ -90,14 +79,23 @@ public class PTAParallel
 		for (String a : alpha2) {
 			if (!alpha1.contains(a)) {
 				alpha2only.add(a);
+				alphaUnion.add(a);
 			}
 		}
 		// Explicitly add tau to action lists
 		alpha1only.add("");
 		alpha2only.add("");
-		//System.out.println("alpha1only: " + alpha1only);
-		//System.out.println("alpha2only: " + alpha2only);
-		//System.out.println("sync: " + sync);
+
+		// Create new PTA to store parallel composition
+		par = new PTA(alphaUnion);
+
+		// New set of clocks is union of sets for two PTAs
+		for (String s : pta1.clockNames) {
+			par.getOrAddClock(s);
+		}
+		for (String s : pta2.clockNames) {
+			par.getOrAddClock(s);
+		}
 
 		// Initialise states storage
 		states = new IndexedSet<IndexPair>();

prism/src/pta/parser/PTAParser.java

@@ -123,7 +123,20 @@ public class PTAParser implements PTAParserConstants {
                         String name;
                         PTA pta;
                         Transition trans;
-                        pta = new PTA();
+                        LinkedHashSet <String> alphabet = new LinkedHashSet<String>();
+                        // Find alphabet
+                        n = locationNames.size();
+                        for (i = 0; i < n; i++) {
+                            ArrayList<astTransition> tt = transitions.get(locationNames.get(i));
+                            if (tt == null || tt.isEmpty()) continue;
+                            for (astTransition t : tt) {
+                            	if (t.action != null && !t.action.equals("")) {
+                            		alphabet.add(t.action);
+                            	}
+                            }
+                        }
+                        // Create new PTA
+                        pta = new PTA(new ArrayList<String> (alphabet));
                         // Add all clocks
                         n = clockNames.size();
                         for (i = 0; i < n; i++)