From 4ad8e43e9f08f2c48b68537ef55a1b7c784a417b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 5 Sep 2016 16:07:00 +0000 Subject: [PATCH] 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 | 18 +++++++++++++ prism/src/pta/DBMList.java | 2 +- prism/src/pta/Modules2PTA.java | 5 +++- prism/src/pta/PTA.java | 19 ++++++------- prism/src/pta/PTAParallel.java | 42 ++++++++++++++--------------- prism/src/pta/parser/PTAParser.java | 15 ++++++++++- 6 files changed, 67 insertions(+), 34 deletions(-) diff --git a/prism/src/parser/ast/Module.java b/prism/src/parser/ast/Module.java index 5e555cc2..e604b557 100644 --- a/prism/src/parser/ast/Module.java +++ b/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 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 alphabet) + { + this.alphabet = (alphabet == null) ? null : new Vector(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 getAllSynchs() { + // If overridden, use this + if (alphabet != null) { + return alphabet; + } + // Otherwise, deduce syntactically int i, n; String s; Vector allSynchs = new Vector(); diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java index f9291b6c..f2ef3419 100644 --- a/prism/src/pta/DBMList.java +++ b/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); } diff --git a/prism/src/pta/Modules2PTA.java b/prism/src/pta/Modules2PTA.java index 6063c74c..bce33a8e 100644 --- a/prism/src/pta/Modules2PTA.java +++ b/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(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; diff --git a/prism/src/pta/PTA.java b/prism/src/pta/PTA.java index e867829c..d84ec767 100644 --- a/prism/src/pta/PTA.java +++ b/prism/src/pta/PTA.java @@ -50,14 +50,18 @@ public class PTA protected int numTransitions; protected ArrayList> transitions; // Alphabet - protected Set alphabet; + protected List 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 alphabet) { numClocks = 0; clockNames = new ArrayList(); @@ -67,7 +71,7 @@ public class PTA locationNameVars = null; numTransitions = 0; transitions = new ArrayList>(); - alphabet = new LinkedHashSet(); + 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 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 list = transitions.get(transition.getSource()); list.add(transition); numTransitions++; @@ -267,7 +268,7 @@ public class PTA return cMax; } - public Set getAlphabet() + public List 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 diff --git a/prism/src/pta/PTAParallel.java b/prism/src/pta/PTAParallel.java index 65bd5070..df07bab6 100644 --- a/prism/src/pta/PTAParallel.java +++ b/prism/src/pta/PTAParallel.java @@ -52,34 +52,23 @@ public class PTAParallel */ public PTA compose(PTA pta1, PTA pta2) { - Set 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(); - alpha1only = new LinkedHashSet(); - alpha2only = new LinkedHashSet(); + // Get alphabets, compute intersection, union etc. + List alpha1 = pta1.getAlphabet(); + List alpha2 = pta2.getAlphabet(); + LinkedHashSet sync = new LinkedHashSet(); + LinkedHashSet alpha1only = new LinkedHashSet(); + LinkedHashSet alpha2only = new LinkedHashSet(); + List alphaUnion = new ArrayList(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(); diff --git a/prism/src/pta/parser/PTAParser.java b/prism/src/pta/parser/PTAParser.java index 741fe85b..e4030f1f 100644 --- a/prism/src/pta/parser/PTAParser.java +++ b/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 alphabet = new LinkedHashSet(); + // Find alphabet + n = locationNames.size(); + for (i = 0; i < n; i++) { + ArrayList 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 (alphabet)); // Add all clocks n = clockNames.size(); for (i = 0; i < n; i++)