Merge lp:~tapaal-contributor/tapaal/autodetect-lens-check into lp:tapaal

Proposed by Lena Ernstsen
Status: Rejected
Rejected by: Kenneth Yrke Jørgensen
Proposed branch: lp:~tapaal-contributor/tapaal/autodetect-lens-check
Merge into: lp:tapaal
Diff against target: 226 lines (+66/-16)
5 files modified
src/dk/aau/cs/gui/TabContent.java (+4/-2)
src/dk/aau/cs/io/LoadedModel.java (+20/-4)
src/dk/aau/cs/io/ModelLoader.java (+30/-7)
src/dk/aau/cs/io/TapnXmlLoader.java (+5/-1)
src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java (+7/-2)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/autodetect-lens-check
Reviewer Review Type Date Requested Status
Kenneth Yrke Jørgensen Pending
TAPAAL Reviewers Pending
Review via email: mp+389463@code.launchpad.net

Commit message

Autodetect of lens info added when loading nets

Description of the change

Checks whether the registered lens information in the .tapn file is correct.

If no lens information is found in the file then auto detection checks which lens information is true.

To post a comment you must log in.
1101. By Lena Ernstsen

Merged with untimed-timed-gui

1102. By Lena Ernstsen

Merge with trunk

Unmerged revisions

1102. By Lena Ernstsen

Merge with trunk

1101. By Lena Ernstsen

Merged with untimed-timed-gui

1100. By Lena Ernstsen

Added check for whether the lens is correct according to the net

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/gui/TabContent.java'
2--- src/dk/aau/cs/gui/TabContent.java 2020-08-17 08:18:13 +0000
3+++ src/dk/aau/cs/gui/TabContent.java 2020-08-19 12:14:43 +0000
4@@ -1988,7 +1988,8 @@
5 allTemplates(),
6 queriesOverwrite,
7 network().constants(),
8- lens
9+ lens,
10+ false
11 );
12
13 tapnWriter.savePNML(outFile);
14@@ -2072,7 +2073,8 @@
15 allTemplates(),
16 queries(),
17 network().constants(),
18- overwriteLens
19+ overwriteLens,
20+ true
21 );
22
23 try {
24
25=== modified file 'src/dk/aau/cs/io/LoadedModel.java'
26--- src/dk/aau/cs/io/LoadedModel.java 2020-08-11 11:11:59 +0000
27+++ src/dk/aau/cs/io/LoadedModel.java 2020-08-19 12:14:43 +0000
28@@ -15,21 +15,23 @@
29 private final Collection<TAPNQuery> queries;
30 private final TimedArcPetriNetNetwork network;
31 private final Collection<String> messages;
32- private final TabContent.TAPNLens lens;
33+ private final boolean isFeatureChanged;
34+ private TabContent.TAPNLens lens;
35
36 public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages){
37- this(network, templates, queries, messages, TabContent.TAPNLens.Default);
38+ this(network, templates, queries, messages, TabContent.TAPNLens.Default, false);
39 }
40 public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries){
41- this(network, templates, queries, List.of(), TabContent.TAPNLens.Default);
42+ this(network, templates, queries, List.of(), TabContent.TAPNLens.Default, false);
43 }
44
45- public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, TabContent.TAPNLens lens){
46+ public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, TabContent.TAPNLens lens, boolean isFeatureChanged){
47 this.templates = templates;
48 this.network = network;
49 this.queries = queries;
50 this.lens = lens;
51 this.messages = messages;
52+ this.isFeatureChanged = isFeatureChanged;
53 }
54
55 public Collection<Template> templates(){ return templates; }
56@@ -48,4 +50,18 @@
57 return lens.isGame();
58 }
59
60+ public void setLens(boolean isTimed, boolean isGame) {
61+ if (lens == null || !isFeatureChanged) {
62+ lens = new TabContent.TAPNLens(isTimed, isGame);
63+ }
64+ }
65+
66+ public void addMessage(String message) {
67+ messages.add(message);
68+ }
69+
70+ public boolean isFeatureChanged() {
71+ return isFeatureChanged;
72+ }
73+
74 }
75\ No newline at end of file
76
77=== modified file 'src/dk/aau/cs/io/ModelLoader.java'
78--- src/dk/aau/cs/io/ModelLoader.java 2020-07-14 10:47:03 +0000
79+++ src/dk/aau/cs/io/ModelLoader.java 2020-08-19 12:14:43 +0000
80@@ -7,7 +7,11 @@
81 import java.io.InputStream;
82
83 import dk.aau.cs.TCTL.Parsing.ParseException;
84+import dk.aau.cs.debug.Logger;
85 import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
86+import pipe.gui.CreateGui;
87+
88+import javax.swing.*;
89
90 public class ModelLoader {
91
92@@ -17,11 +21,13 @@
93 public LoadedModel load(File file) throws Exception{
94 TapnXmlLoader newFormatLoader = new TapnXmlLoader();
95 try{
96- return newFormatLoader.load(file);
97+ LoadedModel model = newFormatLoader.load(file);
98+ return checkLens(model);
99 }catch(Throwable e1){
100 try {
101 TapnLegacyXmlLoader oldFormatLoader = new TapnLegacyXmlLoader();
102- return oldFormatLoader.load(file);
103+ LoadedModel model = oldFormatLoader.load(file);
104+ return checkLens(model);
105 } catch(Throwable e2) {
106 throw new ParseException(e1.getMessage());
107 }
108@@ -42,19 +48,36 @@
109 System.out.println(e.getMessage());
110 }
111 try{
112-
113- return newFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
114-
115+ LoadedModel model = newFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
116+ return checkLens(model);
117 }catch(Throwable e1){
118 try {
119 TapnLegacyXmlLoader oldFormatLoader = new TapnLegacyXmlLoader();
120
121- return oldFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
122-
123+ LoadedModel model = oldFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
124+ return checkLens(model);
125 } catch(Throwable e2) {
126 throw new ParseException(e1.getMessage());
127 }
128 }
129 }
130+
131+ private LoadedModel checkLens(LoadedModel model) {
132+ boolean isNetTimed = !model.network().isUntimed();
133+ boolean isNetGame = model.network().hasUncontrollableTransitions();
134+ String timeMessage = "The net contains time features. The entire net will be changed to include time features.";
135+ String gameMessage = "The net contains game features. The entire net will be changed to include game features.";
136+
137+ if (model.getLens() != null && !model.isFeatureChanged()) {
138+ if (!model.isGame() && isNetGame) {
139+ model.addMessage(gameMessage);
140+ }
141+ if (!model.isTimed() && isNetTimed) {
142+ model.addMessage(timeMessage);
143+ }
144+ }
145+ model.setLens(isNetTimed, isNetGame);
146+ return model;
147+ }
148
149 }
150
151=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
152--- src/dk/aau/cs/io/TapnXmlLoader.java 2020-08-11 12:18:11 +0000
153+++ src/dk/aau/cs/io/TapnXmlLoader.java 2020-08-19 12:14:43 +0000
154@@ -71,6 +71,7 @@
155 private final IdResolver idResolver = new IdResolver();
156 private final Collection<String> messages = new ArrayList<>(10);
157
158+ private boolean isFeatureChanged = false;
159 private TabContent.TAPNLens lens;
160
161 public TapnXmlLoader() {
162@@ -133,7 +134,7 @@
163
164
165
166- return new LoadedModel(network, templates, queries,messages, lens);
167+ return new LoadedModel(network, templates, queries,messages, lens, isFeatureChanged);
168 }
169
170 private void parseBound(Document doc, TimedArcPetriNetNetwork network){
171@@ -149,6 +150,9 @@
172
173 var isTimed = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isTimed").getNodeValue());
174 var isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue());
175+ if (nodeList.item(0).getAttributes().getNamedItem("isChanged") != null) {
176+ isFeatureChanged = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isChanged").getNodeValue());
177+ }
178
179 lens = new TabContent.TAPNLens(isTimed, isGame);
180 } else {
181
182=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
183--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-08-11 13:25:25 +0000
184+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-08-19 12:14:43 +0000
185@@ -57,6 +57,7 @@
186 private final Iterable<Constant> constants;
187 private final TimedArcPetriNetNetwork network;
188 private final TabContent.TAPNLens lens;
189+ private final String isFeatureChanged;
190
191 public TimedArcPetriNetNetworkWriter(
192 TimedArcPetriNetNetwork network,
193@@ -69,20 +70,23 @@
194 this.queries = queries;
195 this.constants = constants;
196 this.lens = TabContent.TAPNLens.Default;
197- }
198+ this.isFeatureChanged = "false";
199+ }
200
201 public TimedArcPetriNetNetworkWriter(
202 TimedArcPetriNetNetwork network,
203 Iterable<Template> templates,
204 Iterable<TAPNQuery> queries,
205 Iterable<Constant> constants,
206- TabContent.TAPNLens lens
207+ TabContent.TAPNLens lens,
208+ boolean isFeatureChanged
209 ) {
210 this.network = network;
211 this.templates = templates;
212 this.queries = queries;
213 this.constants = constants;
214 this.lens = lens;
215+ this.isFeatureChanged = String.valueOf(isFeatureChanged);
216 }
217
218 public ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException {
219@@ -178,6 +182,7 @@
220
221 feature.setAttribute("isTimed", isTimed);
222 feature.setAttribute("isGame", isGame);
223+ feature.setAttribute("isChanged", isFeatureChanged);
224
225 return feature;
226 }

Subscribers

People subscribed via source and target branches