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

[Lena Ernstsen]

Autodetect of lens info added when loading nets

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.

[lp:~tapaal-contributor/tapaal/autodetect-lens-check]

1101. By Lena Ernstsen on 2020-08-18

Merged with untimed-timed-gui

1102. By Lena Ernstsen on 2020-08-19

Merge with trunk

Unmerged revisions

1102. By Lena Ernstsen on 2020-08-19

Merge with trunk

1101. By Lena Ernstsen on 2020-08-18

Merged with untimed-timed-gui

1100. By Lena Ernstsen on 2020-08-17

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

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2020-08-17 08:18:13 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2020-08-19 12:14:43 +0000
@@ -1988,7 +1988,8 @@
 					allTemplates(),
 					queriesOverwrite,
 					network().constants(),
-                    lens
+                    lens,
+                    false
 			);
 
 			tapnWriter.savePNML(outFile);
@@ -2072,7 +2073,8 @@
             allTemplates(),
             queries(),
             network().constants(),
-            overwriteLens
+            overwriteLens,
+            true
         );
 
         try {
 
=== modified file 'src/dk/aau/cs/io/LoadedModel.java'
--- src/dk/aau/cs/io/LoadedModel.java	2020-08-11 11:11:59 +0000
+++ src/dk/aau/cs/io/LoadedModel.java	2020-08-19 12:14:43 +0000
@@ -15,21 +15,23 @@
 	private final Collection<TAPNQuery> queries;
 	private final TimedArcPetriNetNetwork network;
     private final Collection<String> messages;
-    private final TabContent.TAPNLens lens;
+    private final boolean isFeatureChanged;
+    private TabContent.TAPNLens lens;
 
     public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages){
-        this(network, templates, queries, messages, TabContent.TAPNLens.Default);
+        this(network, templates, queries, messages, TabContent.TAPNLens.Default, false);
     }
 	public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries){
-		this(network, templates, queries, List.of(), TabContent.TAPNLens.Default);
+		this(network, templates, queries, List.of(), TabContent.TAPNLens.Default, false);
 	}
 
-    public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, TabContent.TAPNLens lens){
+    public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, TabContent.TAPNLens lens, boolean isFeatureChanged){
         this.templates = templates;
         this.network = network;
         this.queries = queries;
         this.lens = lens;
         this.messages = messages;
+        this.isFeatureChanged = isFeatureChanged;
     }
 
 	public Collection<Template> templates(){ return templates; }
@@ -48,4 +50,18 @@
 	    return lens.isGame();
     }
 
+    public void setLens(boolean isTimed, boolean isGame) {
+        if (lens == null || !isFeatureChanged) {
+            lens = new TabContent.TAPNLens(isTimed, isGame);
+        }
+    }
+
+    public void addMessage(String message) {
+        messages.add(message);
+    }
+
+    public boolean isFeatureChanged() {
+        return isFeatureChanged;
+    }
+
 }
 \ No newline at end of file
 
=== modified file 'src/dk/aau/cs/io/ModelLoader.java'
--- src/dk/aau/cs/io/ModelLoader.java	2020-07-14 10:47:03 +0000
+++ src/dk/aau/cs/io/ModelLoader.java	2020-08-19 12:14:43 +0000
@@ -7,7 +7,11 @@
 import java.io.InputStream;
 
 import dk.aau.cs.TCTL.Parsing.ParseException;
+import dk.aau.cs.debug.Logger;
 import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
+import pipe.gui.CreateGui;
+
+import javax.swing.*;
 
 public class ModelLoader {
 
@@ -17,11 +21,13 @@
 	public LoadedModel load(File file) throws Exception{		
 		TapnXmlLoader newFormatLoader = new TapnXmlLoader();
 		try{
-			return newFormatLoader.load(file);
+		    LoadedModel model = newFormatLoader.load(file);
+			return checkLens(model);
 		}catch(Throwable e1){
 			try {
 				TapnLegacyXmlLoader oldFormatLoader = new TapnLegacyXmlLoader();
-				return oldFormatLoader.load(file);
+				LoadedModel model = oldFormatLoader.load(file);
+				return checkLens(model);
 			} catch(Throwable e2) {
 				throw new ParseException(e1.getMessage());
 			}
@@ -42,19 +48,36 @@
 			System.out.println(e.getMessage());
 		}
 		try{
-
-            return newFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
-
+            LoadedModel model = newFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
+            return checkLens(model);
 		}catch(Throwable e1){
 			try {
 				TapnLegacyXmlLoader oldFormatLoader = new TapnLegacyXmlLoader();
 
-                return oldFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
-
+                LoadedModel model = oldFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
+                return checkLens(model);
 			} catch(Throwable e2) {
 				throw new ParseException(e1.getMessage());
 			}
 		}
 	}
+
+	private LoadedModel checkLens(LoadedModel model) {
+	    boolean isNetTimed = !model.network().isUntimed();
+	    boolean isNetGame = model.network().hasUncontrollableTransitions();
+	    String timeMessage = "The net contains time features. The entire net will be changed to include time features.";
+	    String gameMessage = "The net contains game features. The entire net will be changed to include game features.";
+
+	    if (model.getLens() != null && !model.isFeatureChanged()) {
+            if (!model.isGame() && isNetGame) {
+                model.addMessage(gameMessage);
+            }
+            if (!model.isTimed() && isNetTimed) {
+                model.addMessage(timeMessage);
+            }
+        }
+        model.setLens(isNetTimed, isNetGame);
+	    return model;
+    }
 	
 }
 
=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
--- src/dk/aau/cs/io/TapnXmlLoader.java	2020-08-11 12:18:11 +0000
+++ src/dk/aau/cs/io/TapnXmlLoader.java	2020-08-19 12:14:43 +0000
@@ -71,6 +71,7 @@
 	private final IdResolver idResolver = new IdResolver();
     private final Collection<String> messages = new ArrayList<>(10);
 
+    private boolean isFeatureChanged = false;
     private TabContent.TAPNLens lens;
 
 	public TapnXmlLoader() {
@@ -133,7 +134,7 @@
 
 
 
-		return new LoadedModel(network, templates, queries,messages, lens);
+		return new LoadedModel(network, templates, queries,messages, lens, isFeatureChanged);
 	}
 
 	private void parseBound(Document doc, TimedArcPetriNetNetwork network){
@@ -149,6 +150,9 @@
 
             var isTimed = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isTimed").getNodeValue());
             var isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue());
+            if (nodeList.item(0).getAttributes().getNamedItem("isChanged") != null) {
+                isFeatureChanged = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isChanged").getNodeValue());
+            }
 
             lens = new TabContent.TAPNLens(isTimed, isGame);
         } else {
 
=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2020-08-11 13:25:25 +0000
+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2020-08-19 12:14:43 +0000
@@ -57,6 +57,7 @@
 	private final Iterable<Constant> constants;
 	private final TimedArcPetriNetNetwork network;
     private final TabContent.TAPNLens lens;
+    private final String isFeatureChanged;
 
 	public TimedArcPetriNetNetworkWriter(
 			TimedArcPetriNetNetwork network, 
@@ -69,20 +70,23 @@
 		this.queries = queries;
 		this.constants = constants;
 		this.lens = TabContent.TAPNLens.Default;
-	}
+        this.isFeatureChanged = "false";
+    }
 
     public TimedArcPetriNetNetworkWriter(
         TimedArcPetriNetNetwork network,
         Iterable<Template> templates,
         Iterable<TAPNQuery> queries,
         Iterable<Constant> constants,
-        TabContent.TAPNLens lens
+        TabContent.TAPNLens lens,
+        boolean isFeatureChanged
     ) {
         this.network = network;
         this.templates = templates;
         this.queries = queries;
         this.constants = constants;
         this.lens = lens;
+        this.isFeatureChanged = String.valueOf(isFeatureChanged);
     }
 	
 	public ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException {
@@ -178,6 +182,7 @@
 
         feature.setAttribute("isTimed", isTimed);
         feature.setAttribute("isGame", isGame);
+        feature.setAttribute("isChanged", isFeatureChanged);
 
         return feature;
     }