From cf12b550adde1fa1164a54fdde03178524b7c109 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 22 Nov 2017 11:10:41 +0100 Subject: [PATCH] PTAParser.jj: update to include changes from PTAParser.java (fixes #32) And refresh PTAParser.java (only whitespace changes), correspondingly. Thanks @muhrik, @VojtechRehak, @Lkorenciak. --- prism/src/pta/parser/PTAParser.java | 14 +++++++------- prism/src/pta/parser/PTAParser.jj | 15 ++++++++++++++- 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/prism/src/pta/parser/PTAParser.java b/prism/src/pta/parser/PTAParser.java index e4030f1f..e2b83445 100644 --- a/prism/src/pta/parser/PTAParser.java +++ b/prism/src/pta/parser/PTAParser.java @@ -127,13 +127,13 @@ public class PTAParser implements PTAParserConstants { // 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); - } - } + 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)); diff --git a/prism/src/pta/parser/PTAParser.jj b/prism/src/pta/parser/PTAParser.jj index 419ad130..020ef285 100644 --- a/prism/src/pta/parser/PTAParser.jj +++ b/prism/src/pta/parser/PTAParser.jj @@ -154,7 +154,20 @@ public class PTAParser 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++)