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

[Kenneth Yrke Jørgensen]

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2020-08-24 09:50:07 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2020-08-26 12:31:11 +0000
@@ -613,60 +613,13 @@
 
             return tab;
 		} catch (Exception e) {
-			throw new Exception("TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n  - " + e.toString());
+			//throw new Exception("TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n  - " + e.toString());
+            throw e;
 		}
 
 	}
 
-    private TabContent createNewTabFromInputStream(InputStream file, String name, FeatureOption option, boolean isYes) throws Exception {
-
-        try {
-            ModelLoader loader = new ModelLoader();
-            LoadedModel loadedModel = loader.load(file);
-
-            if (loadedModel.getMessages().size() != 0) {
-                new Thread(new Runnable() {
-                    @Override
-                    public void run() {
-                        CreateGui.getAppGui().setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
-                        String message = "While loading the net we found one or more warnings: \n\n";
-                        for (String s : loadedModel.getMessages()) {
-                            message += s + "\n\n";
-                        }
-
-                        new MessengerImpl().displayInfoMessage(message, "Warning");
-                    }
-                }).start();
-            }
-
-            TabContent tab;
-
-            switch (option) {
-                case TIME:
-                    tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), isYes, lens.isGame());
-                    break;
-                case GAME:
-                    tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), lens.isTimed(), isYes);
-                    break;
-                default:
-                    tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), lens.isTimed(), lens.isGame());
-                    break;
-            }
-
-            tab.setInitialName(name);
-
-            tab.selectFirstElements();
-
-            tab.setFile(null);
-
-            return tab;
-        } catch (Exception e) {
-            throw new Exception("TAPAAL encountered an error while loading the file: " + name + "\n\nPossible explanations:\n  - " + e.toString());
-        }
-
-    }
-
-	public static TabContent createNewEmptyTab(String name, boolean isTimed, boolean isGame){
+    public static TabContent createNewEmptyTab(String name, boolean isTimed, boolean isGame){
 		TabContent tab = new TabContent(isTimed, isGame);
 		tab.setInitialName(name);
 
@@ -692,7 +645,7 @@
 				PNMLoader loader = new PNMLoader();
 				loadedModel = loader.load(file);
 
-                TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries());
+                TabContent tab = new TabContent(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), loadedModel.getLens());
 
                 String name = null;
 
@@ -816,14 +769,16 @@
 
         Require.that(network != null, "network cannot be null");
         Require.notNull(lens, "Lens can't be null");
+
+        tapnNetwork = network;
         this.lens = lens;
-        tapnNetwork = network;
 
         guiModels.clear();
         for (Template template : templates) {
             addGuiModel(template.model(), template.guiModel());
             zoomLevels.put(template.model(), template.zoomer());
             hasPositionalInfos.put(template.model(), template.getHasPositionalInfo());
+
             for(PetriNetObject o : template.guiModel().getPetriNetObjects()){
                 o.setLens(this.lens);
             }
@@ -867,13 +822,6 @@
         animationModeController = new CanvasAnimationController(getAnimator());
     }
 
-    private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, boolean isTimed, boolean isGame) {
-        this(network, templates, tapnqueries,  new TAPNLens(isTimed, isGame));
-    }
-
-    private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries) {
-        this(network, templates, tapnqueries,  new TAPNLens(true, false));
-    }
 	public TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, Iterable<TAPNQuery> tapnqueries, TAPNLens lens) {
         this(network, templates, lens);
 
 
=== 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-26 12:31:11 +0000
@@ -17,13 +17,6 @@
     private final Collection<String> messages;
     private final TabContent.TAPNLens lens;
 
-    public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages){
-        this(network, templates, queries, messages, TabContent.TAPNLens.Default);
-    }
-	public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries){
-		this(network, templates, queries, List.of(), TabContent.TAPNLens.Default);
-	}
-
     public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, Collection<String> messages, TabContent.TAPNLens lens){
         this.templates = templates;
         this.network = network;
@@ -38,14 +31,14 @@
     public Collection<String> getMessages() { return messages; }
 
     public TabContent.TAPNLens getLens(){
-        return lens;
-    }
+        if (lens != null) {
+            return lens;
+        } else {
+            boolean isNetTimed = !network().isUntimed();
+            boolean isNetGame = network().hasUncontrollableTransitions();
 
-	public boolean isTimed() {
-	    return lens.isTimed();
-    }
-    public boolean isGame() {
-	    return lens.isGame();
+            return new TabContent.TAPNLens(isNetTimed, isNetGame);
+        }
     }
 
 }
 \ 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-26 12:31:11 +0000
@@ -7,7 +7,6 @@
 import java.io.InputStream;
 
 import dk.aau.cs.TCTL.Parsing.ParseException;
-import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
 
 public class ModelLoader {
 
@@ -17,19 +16,19 @@
 	public LoadedModel load(File file) throws Exception{		
 		TapnXmlLoader newFormatLoader = new TapnXmlLoader();
 		try{
-			return newFormatLoader.load(file);
-		}catch(Throwable e1){
+            return newFormatLoader.load(file);
+        }catch(Throwable e1){
 			try {
 				TapnLegacyXmlLoader oldFormatLoader = new TapnLegacyXmlLoader();
-				return oldFormatLoader.load(file);
-			} catch(Throwable e2) {
+                return oldFormatLoader.load(file);
+            } catch(Throwable e2) {
 				throw new ParseException(e1.getMessage());
 			}
 		}
 	}
-	
-	
-	public LoadedModel load(InputStream file) throws Exception{
+
+
+    public LoadedModel load(InputStream file) throws Exception{
 		TapnXmlLoader newFormatLoader = new TapnXmlLoader();
 		ByteArrayOutputStream baos = new ByteArrayOutputStream();
 		byte[] buffer = new byte[1024];
@@ -45,13 +44,13 @@
 
             return newFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
 
-		}catch(Throwable e1){
+        }catch(Throwable e1){
 			try {
 				TapnLegacyXmlLoader oldFormatLoader = new TapnLegacyXmlLoader();
 
                 return oldFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
 
-			} catch(Throwable e2) {
+            } catch(Throwable e2) {
 				throw new ParseException(e1.getMessage());
 			}
 		}
 
=== modified file 'src/dk/aau/cs/io/PNMLoader.java'
--- src/dk/aau/cs/io/PNMLoader.java	2020-08-11 12:18:11 +0000
+++ src/dk/aau/cs/io/PNMLoader.java	2020-08-26 12:31:11 +0000
@@ -53,7 +53,7 @@
 
 public class PNMLoader {
 
-    private final TabContent.TAPNLens lens = new TabContent.TAPNLens(false, false);
+    private final TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
 
     enum GraphicsType { Position, Offset }
 
@@ -120,7 +120,7 @@
 		
 		network.setPaintNet(isNetDrawable());
 		tapn.setCheckNames(true);
-		return new LoadedModel(network, Arrays.asList(template), new ArrayList<TAPNQuery>());
+		return new LoadedModel(network, Arrays.asList(template), new ArrayList<TAPNQuery>(), new ArrayList<>(), null);
 	}
 
 	private String getTAPNName(Node netNode) {
 
=== modified file 'src/dk/aau/cs/io/TapnLegacyXmlLoader.java'
--- src/dk/aau/cs/io/TapnLegacyXmlLoader.java	2020-08-11 12:18:11 +0000
+++ src/dk/aau/cs/io/TapnLegacyXmlLoader.java	2020-08-26 12:31:11 +0000
@@ -84,7 +84,7 @@
 	private final IdResolver idResolver = new IdResolver();
 
     private final Collection<String> messages = new ArrayList<>(10);
-    private final TabContent.TAPNLens lens = new TabContent.TAPNLens(true, false);
+    private final TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
 
 
     public TapnLegacyXmlLoader() {}
@@ -145,8 +145,8 @@
 		templates.add(parseTimedArcPetriNetAsOldFormat(nets.item(0), network));
 		
 		checkThatQueriesUseExistingPlaces(network);
-		
-		return new LoadedModel(network, templates, queries, messages);
+
+		return new LoadedModel(network, templates, queries, messages, null);
 	}
 
 	private void checkThatQueriesUseExistingPlaces(TimedArcPetriNetNetwork network) {
 
=== 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-26 12:31:11 +0000
@@ -71,7 +71,8 @@
 	private final IdResolver idResolver = new IdResolver();
     private final Collection<String> messages = new ArrayList<>(10);
 
-    private TabContent.TAPNLens lens;
+    boolean hasFeatureTag = false;
+    private TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
 
 	public TapnXmlLoader() {
 
@@ -132,8 +133,11 @@
 		parseBound(doc, network);
 
 
-
-		return new LoadedModel(network, templates, queries,messages, lens);
+        if (hasFeatureTag) {
+            return new LoadedModel(network, templates, queries, messages, lens);
+        } else {
+            return new LoadedModel(network, templates, queries, messages, null);
+        }
 	}
 
 	private void parseBound(Document doc, TimedArcPetriNetNetwork network){
@@ -147,12 +151,12 @@
         if (doc.getElementsByTagName("feature").getLength() > 0) {
 	        NodeList nodeList = doc.getElementsByTagName("feature");
 
+	        hasFeatureTag = true;
+
             var isTimed = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isTimed").getNodeValue());
             var isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue());
 
             lens = new TabContent.TAPNLens(isTimed, isGame);
-        } else {
-            lens = new TabContent.TAPNLens(true, false);
         }
     }