Merge lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties into lp:tapaal

[Lena Ernstsen]

Added the possibility to choose which time and game properties a net should include.

When creating a new net, it is possible to choose which kind of properties should be accessible (whether is is timed or untimed and whether it should contain game features).

This information is displayed in the toolbar beside the tokens.

The information will also be displayed when loading a file. However, only timing information is displayed. Game information is not displayed yet because the implementation of games is not included in this branch.

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1072. By Lena Ernstsen on 2020-07-14

Net information is saved in .tapn files (games are not implemented fully because these features are not included in this branch)

1073. By Lena Ernstsen on 2020-07-14

Minor fix

[Kenneth Yrke Jørgensen (yrke)]

review: Needs Fixing

[Kenneth Yrke Jørgensen (yrke)]

See comments in code.

[Jiri Srba (srba)]

Loading and saving of net features does not work. Make a game untimed net and add just one place. Then save the net and open it again and it will say that the game is not a game net anymore.

When creating a new net, the layout is confusing. Instead, try to make a dialog like:

Use time semantics: [ ] Yes [ ] No
Use game semantics: [ ] Yes [ ] No

The status can contain information saying: "Time: Yes, Game: No" etc.
Kenneth, I like the current placement of this information next to the buttons, as it should be always
visible, the status bar is used more as context sensitive guide.

When you make a new query, it should offer either the CTL or Reachability dialog without asking,
depending on the Timed flag (if Timed, offer Reachability, if not Timed offer CTL).

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1074. By Lena Ernstsen on 2020-07-23

Changed the dialog message when creating a new net. Changed the text in the toolbar. When saving, the time/game info is placed on each tapn instead of the entire net. Removed global lense information from TimedArcPetriNet. Made lense information invisble for guiframe again.

1075. By Lena Ernstsen on 2020-07-23

When net is timed, only reachability queries are available. When net is untimed, only CTL queries are available.

1076. By Lena Ernstsen on 2020-07-27

Net information is saved correctly.

1077. By Lena Ernstsen on 2020-07-27

Net information is loaded correctly.

1078. By Lena Ernstsen on 2020-07-27

Added the property as a tag for the entire net net, instead of each tapn.

[Lena Ernstsen (lsaid)]

The saving and loading should work now.
CTL queries are only available when the net is untimed.
Dialog message is changed to be more readable, as well as the text in the toolbar.
Made the lens information as a tag to the entire net instead of for each tapn.

review: Needs Resubmitting

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1079. By Lena Ernstsen on 2020-07-29

Minor fix

1080. By Lena Ernstsen on 2020-07-29

Renamed property to feature

[Jiri Srba (srba)]

When you open a .tapn file that does not have any information about whether it is timed/untimed
and game/not game, it should autodetect the type of the net. In net statistics you can find the check for timed/untimed - all components, even the nonactive ones must be untimed in order to call the net untimed. The test for game must be implemented - if there is any controllable/environmental player information in the XML file then it is a game, otherwise it is not.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1081. By Lena Ernstsen on 2020-08-03

Added sanity check for loading the time/game info of nets. Renamed property to feature and removed unused methods.

1082. By Lena Ernstsen on 2020-08-03

Added warning message when net is timed/game and the feature says otherwise.

[Lena Ernstsen (lsaid)]

Added sanity check for loading time/game info of nets. A warning will appear if the net is timed/game, but the loaded info says otherwise.

The warning for the game feature is not fully implemented, because it can't be tested whether the network is a game yet.

review: Needs Resubmitting

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1083. By Lena Ernstsen on 2020-08-03

Removed warning messages

1084. By Lena Ernstsen on 2020-08-03

Warning messages for time/game is shown in debugger

[Jiri Srba (srba)]

We need to change the method checking if a net is timed. At the moment, if there are no time intervals but the net has urgent transitions or age invariants, it will be still declared as "untimed" which we don't want anymore. So change the definition of untimed such that it will also check whether the net has urgent transitions or age invariants (except for the trivial one < infty), and if yes then report the net as timed.

review: Needs Fixing

[Jiri Srba (srba)]

The default options when making a new net should be No/No both for time and game semantics.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1085. By Lena Ernstsen on 2020-08-03

Set default game/time features to 'No'. Changed isUntimed to check urgent transitions and nontrivial age invariants.

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1086. By Lena Ernstsen on 2020-08-03

Fixed logic

[Jiri Srba (srba)]

The new semantics of inUntimed() where urgent transitions and nontrivial age invariants make the net timed it not reflected in net statistics panel.

review: Needs Fixing

[Kenneth Yrke Jørgensen (yrke)]

review: Approve

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1087. By Lena Ernstsen on 2020-08-03

Fixed statistics concering untimed net

1088. By Lena Ernstsen on 2020-08-03

Merge

[Jiri Srba (srba)]

The statistics cannot be fixed this way. It must be done online, everytime the dialog is called
it should be recomputed as the net could have been edited in between.
E.g. make two components, first one has urgent transition, the second one not - it will report the statistics in a wrong way.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1089. By Lena Ernstsen on 2020-08-03

Fixed wrong untimed information in statistics

[Jiri Srba (srba)]

Still does not work. Try to make several components, some untimed, other with urgent transition. Now depending which component is shown, different answer are given. E.g. if you are in the untimed component it will claim that all components are untimed.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/load-and-save-time-and-game-net-properties]

1090. By Lena Ernstsen on 2020-08-03

urgent transitions are checked correctly when checking whether net is untimed

[Jiri Srba (srba)]

Works as expected now.

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2020-07-09 12:55:25 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2020-08-03 12:48:32 +0000
@@ -476,21 +476,23 @@
 			ModelLoader loader = new ModelLoader();
 			LoadedModel 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.isTimed(), loadedModel.isGame());
+
             tab.setInitialName(name);
 
 			tab.selectFirstElements();
 
 			tab.setFile(null);
-			return tab;
+
+            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){
-		TabContent tab = new TabContent();
+	public static TabContent createNewEmptyTab(String name, boolean isTimed, boolean isGame){
+		TabContent tab = new TabContent(isTimed, isGame);
 		tab.setInitialName(name);
 
 		//Set Default Template
@@ -631,8 +633,8 @@
 	private WorkflowDialog workflowDialog = null;
 
 
-	private TabContent() {
-	    this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(true,false));
+	private TabContent(boolean isTimed, boolean isGame) {
+	    this(new TimedArcPetriNetNetwork(), new ArrayList<>(), new TAPNLens(isTimed,isGame));
     }
 
 	private TabContent(TimedArcPetriNetNetwork network, Collection<Template> templates, TAPNLens lens) {
@@ -687,6 +689,10 @@
         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));
     }
@@ -697,7 +703,7 @@
         setQueries(tapnqueries);
         setConstants(network().constants());
 	}
-	
+
 	public SharedPlacesAndTransitionsPanel getSharedPlacesAndTransitionsPanel(){
 		return sharedPTPanel;
 	}
@@ -1646,6 +1652,8 @@
 		this.app = Optional.ofNullable(newApp);
 		undoManager.setApp(newApp);
 
+		updateFeatureText();
+
 		//XXX
 		if (isInAnimationMode()) {
 			app.ifPresent(o->o.setGUIMode(GuiFrame.GUIMode.animation));
@@ -1761,7 +1769,7 @@
 	final AbstractDrawingSurfaceManager animationModeController;
 
 	//Writes a tapaal net to a file, with the posibility to overwrite the quires
-	public void writeNetToFile(File outFile, List<TAPNQuery> queriesOverwrite) {
+	public void writeNetToFile(File outFile, List<TAPNQuery> queriesOverwrite, TAPNLens lens) {
 		try {
 			NetworkMarking currentMarking = null;
 			if(isInAnimationMode()){
@@ -1773,7 +1781,9 @@
 					network(),
 					allTemplates(),
 					queriesOverwrite,
-					network().constants()
+					network().constants(),
+                    lens.timed,
+					lens.game
 			);
 
 			tapnWriter.savePNML(outFile);
@@ -1790,7 +1800,7 @@
 	}
 
 	public void writeNetToFile(File outFile) {
-		writeNetToFile(outFile, (List<TAPNQuery>) queries());
+		writeNetToFile(outFile, (List<TAPNQuery>) queries(), lens);
 	}
 
 	@Override
@@ -2244,6 +2254,26 @@
 		managerRef.get().registerManager(drawingSurface);
     }
 
+    public void updateFeatureText() {
+
+        String properties = "Timed: " + (lens.isTimed() ? "Yes" : "No") +
+                            ", Game: " + (lens.isGame() ? "Yes" : "No");
+        app.ifPresent(o->o.setFeatureInfoText(properties));
+
+    }
+
+    public boolean isNetTimed() {
+        return lens.isTimed();
+    }
+
+    public boolean isNetGame() {
+        return lens.isGame();
+    }
+
+    public TAPNLens getLens() {
+        return lens;
+    }
+
     private final class CanvasTransportarcDrawController extends AbstractDrawingSurfaceManager {
 
         private TimedTransitionComponent transition;

=== modified file 'src/dk/aau/cs/io/LoadedModel.java'
--- src/dk/aau/cs/io/LoadedModel.java	2019-03-22 09:17:07 +0000
+++ src/dk/aau/cs/io/LoadedModel.java	2020-08-03 12:48:32 +0000
@@ -9,15 +9,31 @@
 public class LoadedModel{
 	private Collection<Template> templates;
 	private Collection<TAPNQuery> queries;
-	private TimedArcPetriNetNetwork network; 
-	
+	private TimedArcPetriNetNetwork network;
+    private boolean isTimed;
+    private boolean isGame;
+
 	public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries){
 		this.templates = templates;
 		this.network = network;
-		this.queries = queries; 
+		this.queries = queries;
 	}
 
+    public LoadedModel(TimedArcPetriNetNetwork network, Collection<Template> templates, Collection<TAPNQuery> queries, boolean isTimed, boolean isGame){
+        this.templates = templates;
+        this.network = network;
+        this.queries = queries;
+        this.isTimed = isTimed;
+        this.isGame = isGame;
+    }
+
 	public Collection<Template> templates(){ return templates; }
 	public Collection<TAPNQuery> queries(){ return queries; }
 	public TimedArcPetriNetNetwork network(){ return network; }
+	public boolean isTimed() {
+	    return isTimed;
+    }
+    public boolean isGame() {
+	    return isGame;
+    }
 }
\ No newline at end of file

=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
--- src/dk/aau/cs/io/TapnXmlLoader.java	2020-07-14 11:18:47 +0000
+++ src/dk/aau/cs/io/TapnXmlLoader.java	2020-08-03 12:48:32 +0000
@@ -8,11 +8,12 @@
 import java.util.HashMap;
 import java.util.List;
 
-import javax.swing.JOptionPane;
+import javax.swing.*;
 import javax.xml.parsers.DocumentBuilder;
 import javax.xml.parsers.DocumentBuilderFactory;
 import javax.xml.parsers.ParserConfigurationException;
 
+import dk.aau.cs.debug.Logger;
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
 import org.w3c.dom.Node;
@@ -61,7 +62,7 @@
 
 public class TapnXmlLoader {
 	private static final String PLACENAME_ERROR_MESSAGE = "The keywords \"true\" and \"false\" are reserved and can not be used as place names.\nPlaces with these names will be renamed to \"_true\" and \"_false\" respectively.\n\n Note that any queries using these places may not be parsed correctly.";
-	private HashMap<TimedTransitionComponent, TimedTransportArcComponent> presetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
+    private HashMap<TimedTransitionComponent, TimedTransportArcComponent> presetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
 	private HashMap<TimedTransitionComponent, TimedTransportArcComponent> postsetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
 	private HashMap<TimedTransportArcComponent, TimeInterval> transportArcsTimeIntervals = new HashMap<TimedTransportArcComponent, TimeInterval>();
 
@@ -70,6 +71,10 @@
 	private boolean firstPlaceRenameWarning = true;
 	private IdResolver idResolver = new IdResolver();
 
+	private boolean isTimed;
+	private boolean isGame;
+	private boolean hasUncontrollableTransitions = false;
+
 	public TapnXmlLoader() {
 	}
 
@@ -124,8 +129,10 @@
 		network.buildConstraints();
 		
 		parseBound(doc, network);
-		
-		return new LoadedModel(network, templates, queries);
+
+		parseFeature(doc, network);
+
+		return new LoadedModel(network, templates, queries, isTimed, isGame);
 	}
 
 	private void parseBound(Document doc, TimedArcPetriNetNetwork network){
@@ -135,6 +142,30 @@
 		}
 	}
 
+    private void parseFeature(Document doc, TimedArcPetriNetNetwork network) {
+	    boolean networkIsTimed = !network.isUntimed();
+
+        if (doc.getElementsByTagName("feature").getLength() > 0) {
+	        NodeList nodeList = doc.getElementsByTagName("feature");
+
+            isTimed = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isTimed").getNodeValue());
+            isGame = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isGame").getNodeValue());
+
+            if (networkIsTimed && !isTimed) {
+                isTimed = true;
+                Logger.log("The net contains time features. The entire net will be changed to include time features.");
+            }
+            if (hasUncontrollableTransitions && !isGame) {
+                isGame = true;
+                Logger.log("The net contains game features. The entire net will be changed to include game features.");
+
+            }
+        } else {
+            isTimed = networkIsTimed;
+            isGame = hasUncontrollableTransitions;
+        }
+    }
+
 	private void parseSharedPlaces(Document doc, TimedArcPetriNetNetwork network, ConstantStore constants) {
 		NodeList sharedPlaceNodes = doc.getElementsByTagName("shared-place");
 
@@ -220,10 +251,10 @@
 	}
 
 	private Template parseTimedArcPetriNet(Node tapnNode, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
-		String name = getTAPNName(tapnNode);
+        String name = getTAPNName(tapnNode);
 
 		boolean active = getActiveStatus(tapnNode);
-		
+
 		TimedArcPetriNet tapn = new TimedArcPetriNet(name);
 		tapn.setActive(active);
 		network.add(tapn);
@@ -240,23 +271,22 @@
 			}
 		}
 
-
 		return template;
 	}
 
 	private boolean getActiveStatus(Node tapnNode) {
-		if (tapnNode instanceof Element) {
-			Element element = (Element)tapnNode;
-			String activeString = element.getAttribute("active");
-			
-			if (activeString == null || activeString.equals(""))
-				return true;
-			else
-				return activeString.equals("true");
-		} else {
-			return true;
-		}
-	}
+        if (tapnNode instanceof Element) {
+            Element element = (Element)tapnNode;
+            String activeString = element.getAttribute("active");
+
+            if (activeString == null || activeString.equals(""))
+                return true;
+            else
+                return activeString.equals("true");
+        } else {
+            return true;
+        }
+    }
 
 	private void parseElement(Element element, Template template, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
 		if ("labels".equals(element.getNodeName())) {
@@ -269,8 +299,8 @@
 			TimedTransitionComponent transition = parseTransition(element, network, template.model());
 			template.guiModel().addPetriNetObject(transition);
 		} else if ("arc".equals(element.getNodeName())) {
-			parseAndAddArc(element, template, constants);
-		}
+            parseAndAddArc(element, template, constants);
+        }
 	}
 
 	private boolean isNameAllowed(String name) {
@@ -343,6 +373,11 @@
 		String idInput = transition.getAttribute("id");
 		String nameInput = transition.getAttribute("name");
 		boolean isUrgent = Boolean.parseBoolean(transition.getAttribute("urgent"));
+
+		String player = transition.getAttribute("player");
+		if (player.length() > 0 && player.equals("1")) {
+		    hasUncontrollableTransitions = true;
+        }
 		
 		idResolver.add(tapn.name(), idInput, nameInput);
 		

=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2020-06-18 08:32:13 +0000
+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2020-08-03 12:48:32 +0000
@@ -55,6 +55,8 @@
 	private Iterable<TAPNQuery> queries;
 	private Iterable<Constant> constants;
 	private final TimedArcPetriNetNetwork network;
+    private boolean isTimed;
+    private boolean isGame;
 
 	public TimedArcPetriNetNetworkWriter(
 			TimedArcPetriNetNetwork network, 
@@ -66,6 +68,21 @@
 		this.queries = queries;
 		this.constants = constants;
 	}
+
+    public TimedArcPetriNetNetworkWriter(
+        TimedArcPetriNetNetwork network,
+        Iterable<Template> templates,
+        Iterable<TAPNQuery> queries,
+        Iterable<Constant> constants,
+        boolean isTimed,
+        boolean isGame) {
+        this.network = network;
+        this.templates = templates;
+        this.queries = queries;
+        this.constants = constants;
+        this.isTimed = isTimed;
+        this.isGame = isGame;
+    }
 	
 	public ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException {
 		Document document = null;
@@ -89,6 +106,7 @@
 		appendTemplates(document, pnmlRootNode);
 		appendQueries(document, pnmlRootNode);
 		appendDefaultBound(document, pnmlRootNode);
+		appendFeature(document, pnmlRootNode);
 
 		document.normalize();
 		// Create Transformer with XSL Source File
@@ -139,6 +157,29 @@
 		element.setAttribute("bound", network.getDefaultBound() + "");
 		root.appendChild(element);
 	}
+
+    private void appendFeature(Document document, Element root) {
+        String isTimed = "true";
+        String isGame = "true";
+        if (!this.isTimed) {
+            isTimed = "false";
+        }
+        if (!this.isGame) {
+            isGame = "false";
+        }
+
+        root.appendChild(createFeatureElement(isTimed, isGame, document));
+    }
+
+    private Element createFeatureElement(String isTimed, String isGame, Document document) {
+        Require.that(document != null, "Error: document was null");
+        Element feature = document.createElement("feature");
+
+        feature.setAttribute("isTimed", isTimed);
+        feature.setAttribute("isGame", isGame);
+
+        return feature;
+    }
 	
 	private void appendSharedPlaces(Document document, Element root) {
 		for(SharedPlace place : network.sharedPlaces()){
@@ -194,7 +235,6 @@
 
 			Attr netAttrType = document.createAttribute("type");
 			netAttrType.setValue("P/T net");
-
 			NET.setAttributeNode(netAttrType);
 
 			appendAnnotationNotes(document, guiModel, NET);

=== modified file 'src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java'
--- src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java	2019-03-22 12:45:44 +0000
+++ src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java	2020-08-03 12:48:32 +0000
@@ -232,10 +232,10 @@
 	}
 
 	private void parseTimedArcPetriNet(Node tapnNode, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
-		String name = getTAPNName(tapnNode);
+        String name = getTAPNName(tapnNode);
 		boolean active = getActiveStatus(tapnNode);
 
-		TimedArcPetriNet tapn = new TimedArcPetriNet(name);
+        TimedArcPetriNet tapn = new TimedArcPetriNet(name);
 		tapn.setActive(active);
 		network.add(tapn);
 		nameGenerator.add(tapn);
@@ -263,6 +263,29 @@
 		}
 	}
 
+    private boolean getInfo(Node tapnNode, String attribute) {
+        Element element = (Element)tapnNode;
+        String string = element.getAttribute(attribute);
+        return string.equals("true");
+    }
+
+    private boolean canGetInfo(Node tapnNode) {
+        if (tapnNode instanceof Element) {
+            Element element = (Element)tapnNode;
+            String timedString = element.getAttribute("timed");
+            String gameString = element.getAttribute("game");
+
+            if (timedString == null || timedString.equals("") ||
+                gameString == null || gameString.equals("")) {
+                return false;
+            } else {
+                return true;
+            }
+        } else {
+            return false;
+        }
+    }
+
 	private void parseElement(Element element, TimedArcPetriNet tapn, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
 		if ("place".equals(element.getNodeName())) {
 			parsePlace(element, network, tapn, constants);

=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNet.java'
--- src/dk/aau/cs/model/tapn/TimedArcPetriNet.java	2020-06-22 08:20:47 +0000
+++ src/dk/aau/cs/model/tapn/TimedArcPetriNet.java	2020-08-03 12:48:32 +0000
@@ -12,8 +12,8 @@
 public class TimedArcPetriNet {
 	private String name;
 	private TimedArcPetriNetNetwork parentNetwork;
-	private boolean isActive;
-	
+    private boolean isActive;
+
 	//Should the names be checked to see if the name is already used 
 	//This is used when loading big nets as the checking  of names is slow.
 	private boolean checkNames = true; 
@@ -28,9 +28,9 @@
 	private TimedMarking currentMarking = new LocalTimedMarking();
 
 	public TimedArcPetriNet(String name) {
-		setName(name);
-		isActive = true;
-	}
+        setName(name);
+        isActive = true;
+    }
 
 	public TimedMarking marking(){
 		return currentMarking;
@@ -436,7 +436,7 @@
             numberOfOrphanPlaces += t.getOrphanPlaces().size();
 			//Test if all inputarcs is untimed and get the number of untimed input arcs
 			for(TimedInputArc in : t.inputArcs()){
-				if(!((in.interval().lowerBound().value() == 0 && in.interval().IsLowerBoundNonStrict() && in.interval().upperBound().equals(Bound.Infinity)))){
+				if(!(in.interval().lowerBound().value() == 0 && in.interval().IsLowerBoundNonStrict() && in.interval().upperBound().equals(Bound.Infinity))){
 					networkUntimed = false;
 				} else {
 					numberOfUntimedInputArcs++;
@@ -447,7 +447,7 @@
 			}
 			//Test if all tansportarcs is untimed and get the number of untimed transport arcs
 			for(TransportArc in : t.transportArcs()){
-				if(!((in.interval().lowerBound().value() == 0 && in.interval().IsLowerBoundNonStrict() && in.interval().upperBound().equals(Bound.Infinity)))){
+				if(!(in.interval().lowerBound().value() == 0 && in.interval().IsLowerBoundNonStrict() && in.interval().upperBound().equals(Bound.Infinity))){
 					networkUntimed = false;
 				} else {
 					numberOfUntimedTransportArcs++;
@@ -456,6 +456,18 @@
 					networkWeighted = true;
 				}
 			}
+
+			for (TimedPlace p : t.places) {
+			    if (!p.invariant().upperBound().equals(Bound.Infinity)) {
+			        networkUntimed = false;
+                }
+            }
+
+			for (TimedTransition transition : t.transitions) {
+			    if (transition.isUrgent()) {
+			        networkUntimed = false;
+                }
+            }
 			
 			// Test all output arcs for weights
 			if(!networkWeighted){
@@ -613,6 +625,16 @@
 				return false;
 			}
 		}
+
+		if (hasUrgentTransitions()) {
+		    return false;
+        }
+
+		for (TimedPlace p : places) {
+		    if (!p.invariant().upperBound().toString().equals("inf")) {
+		        return false;
+            }
+        }
 		
 		return true;
 	}

=== modified file 'src/pipe/dataLayer/Template.java'
--- src/pipe/dataLayer/Template.java	2020-06-12 10:28:49 +0000
+++ src/pipe/dataLayer/Template.java	2020-08-03 12:48:32 +0000
@@ -54,7 +54,7 @@
 	public void setHasPositionalInfo(boolean positionalInfo) {
 		hasPositionalInfo = positionalInfo;
 	}
-	
+
 	@Override
 	public boolean equals(Object obj) {
 		if(obj instanceof Template){

=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java	2020-07-05 18:13:46 +0000
+++ src/pipe/gui/GuiFrame.java	2020-08-03 12:48:32 +0000
@@ -58,6 +58,7 @@
     private StatusBar statusBar;
     private JMenuBar menuBar;
     private JToolBar drawingToolBar;
+    private final JLabel featureInfoText = new JLabel();
     private JComboBox<String> zoomComboBox;
 
     private static final int shortcutkey = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask();
@@ -898,6 +899,10 @@
         drawingToolBar.add(new ToggleButtonWithoutText(tokenAction));
         drawingToolBar.add(new ToggleButtonWithoutText(deleteTokenAction));
 
+        //Net Type
+        drawingToolBar.addSeparator();
+        drawingToolBar.add(featureInfoText);
+
         // Create panel to put toolbars in
         JPanel toolBarPanel = new JPanel();
         toolBarPanel.setLayout(new FlowLayout(FlowLayout.LEFT, 0, 0));
@@ -1271,6 +1276,7 @@
 
                 break;
             case noNet:
+                setFeatureInfoText("");
                 break;
 
             default:
@@ -1642,4 +1648,10 @@
         return CreateGui.getCurrentTab();
     }
 
+    @Override
+    public void setFeatureInfoText(String s) {
+        if (s == null) s = "";
+        featureInfoText.setText(s);
+    }
+
 }

=== modified file 'src/pipe/gui/GuiFrameActions.java'
--- src/pipe/gui/GuiFrameActions.java	2020-05-18 18:17:06 +0000
+++ src/pipe/gui/GuiFrameActions.java	2020-08-03 12:48:32 +0000
@@ -44,4 +44,5 @@
     void setShowZeroToInfinityIntervalsSelected(boolean b);
     void setShowTokenAgeSelected(boolean b);
 
+    void setFeatureInfoText(String s);
 }

=== modified file 'src/pipe/gui/GuiFrameController.java'
--- src/pipe/gui/GuiFrameController.java	2020-07-14 11:18:47 +0000
+++ src/pipe/gui/GuiFrameController.java	2020-08-03 12:48:32 +0000
@@ -147,6 +147,7 @@
 
         currentTab.ifPresent(t -> t.setApp(guiFrame));
         guiFrameDirectAccess.setTitle(currentTab.map(TabContentActions::getTabTitle).orElse(null));
+
     }
 
     @Override

=== modified file 'src/pipe/gui/widgets/NewTAPNPanel.java'
--- src/pipe/gui/widgets/NewTAPNPanel.java	2020-04-30 12:52:28 +0000
+++ src/pipe/gui/widgets/NewTAPNPanel.java	2020-08-03 12:48:32 +0000
@@ -4,17 +4,15 @@
 import java.awt.GridBagConstraints;
 import java.awt.GridBagLayout;
 import java.awt.Insets;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
 import java.awt.event.KeyEvent;
 
-import javax.swing.JButton;
-import javax.swing.JLabel;
-import javax.swing.JOptionPane;
-import javax.swing.JPanel;
-import javax.swing.JRootPane;
-import javax.swing.JTextField;
+import javax.swing.*;
 
 import dk.aau.cs.gui.TabContent;
 import pipe.gui.CreateGui;
+import pipe.gui.Grid;
 import pipe.gui.GuiFrame;
 
 public class NewTAPNPanel extends JPanel {
@@ -22,6 +20,8 @@
 	private JRootPane rootPane;
 	private GuiFrame frame;
 	private JTextField nameTextBox;
+	private JRadioButton timedNet;
+	private JRadioButton gameNet;
 
 	public NewTAPNPanel(JRootPane rootPane, GuiFrame frame) {
 		this.rootPane = rootPane;
@@ -34,6 +34,7 @@
 		this.setLayout(new GridBagLayout());
 
 		initNamePanel();
+		initSelectionPanel();
 		initButtonPanel();
 	}
 
@@ -64,7 +65,7 @@
 		gbc.anchor = GridBagConstraints.EAST;
 		buttonPanel.add(cancelButton,gbc);		
 
-		okButton.addActionListener(e -> createNewTAPNBasedOnSelection(nameTextBox.getText()));
+		okButton.addActionListener(e -> createNewTAPNBasedOnSelection(nameTextBox.getText(), timedNet.isSelected(), gameNet.isSelected()));
 
 		rootPane.setDefaultButton(okButton);
 		
@@ -72,7 +73,7 @@
 
 		gbc = new GridBagConstraints();
 		gbc.gridx = 0;
-		gbc.gridy = 1;
+		gbc.gridy = 2;
 		gbc.insets = new Insets(0, 8, 5, 8);
 		gbc.anchor = GridBagConstraints.EAST;
 		add(buttonPanel, gbc);
@@ -82,7 +83,7 @@
 		rootPane.getParent().setVisible(false);
 	}
 
-	protected void createNewTAPNBasedOnSelection(String name) {
+	protected void createNewTAPNBasedOnSelection(String name, boolean isTimed, boolean isGame) {
 		if (!name.endsWith(".tapn")) {
 			name = name + ".tapn";
 		}
@@ -95,7 +96,7 @@
 		}
 
 		try {
-			TabContent tab = TabContent.createNewEmptyTab(name);
+			TabContent tab = TabContent.createNewEmptyTab(name, isTimed, isGame);
 			CreateGui.openNewTabFromStream(tab);
 		} catch (Exception e) {
 			JOptionPane
@@ -113,7 +114,7 @@
 
 	private void initNamePanel() {
 		JPanel namePanel = new JPanel(new GridBagLayout());
-		
+
 		JLabel nameLabel = new JLabel("Name:");
 		GridBagConstraints gbc = new GridBagConstraints();
 		gbc.gridx = 0;
@@ -145,4 +146,104 @@
 		gbc.insets = new Insets(5, 5, 5, 5);
 		add(namePanel, gbc);
 	}
+
+	private void initSelectionPanel() {
+        JPanel selectionPanel = new JPanel(new GridBagLayout());
+
+        initTimeOptions(selectionPanel);
+        initGameOptions(selectionPanel);
+
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 1;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(5, 5, 5, 5);
+        add(selectionPanel, gbc);
+    }
+
+    private void initTimeOptions(JPanel selectionPanel) {
+        JPanel isTimedPanel = new JPanel(new GridBagLayout());
+        ButtonGroup isTimedRadioButtonGroup = new ButtonGroup();
+
+        JLabel timedText = new JLabel("Use time semantics: ");
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        isTimedPanel.add(timedText, gbc);
+
+        JRadioButton untimedNet = new JRadioButton("No");
+        untimedNet.setSelected(true);
+        gbc = new GridBagConstraints();
+        gbc.gridx = 1;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        isTimedPanel.add(untimedNet, gbc);
+        isTimedRadioButtonGroup.add(untimedNet);
+
+        timedNet = new JRadioButton("Yes");
+        gbc = new GridBagConstraints();
+        gbc.gridx = 2;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        isTimedPanel.add(timedNet, gbc);
+        isTimedRadioButtonGroup.add(timedNet);
+
+        gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 1;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(5, 5, 5, 5);
+        selectionPanel.add(isTimedPanel, gbc);
+    }
+
+    private void initGameOptions(JPanel selectionPanel) {
+        JPanel isGamePanel = new JPanel(new GridBagLayout());
+        ButtonGroup isGameRadioButtonGroup = new ButtonGroup();
+
+        JLabel gameText = new JLabel("Use game semantics:");
+        GridBagConstraints gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        isGamePanel.add(gameText, gbc);
+
+        JRadioButton nonGameNet = new JRadioButton("No");
+        nonGameNet.setSelected(true);
+        gbc = new GridBagConstraints();
+        gbc.gridx = 1;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        isGamePanel.add(nonGameNet, gbc);
+        isGameRadioButtonGroup.add(nonGameNet);
+
+        gameNet = new JRadioButton("Yes");
+        gbc = new GridBagConstraints();
+        gbc.gridx = 2;
+        gbc.gridy = 0;
+        gbc.weightx = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(3, 3, 3, 3);
+        isGamePanel.add(gameNet, gbc);
+        isGameRadioButtonGroup.add(gameNet);
+
+        gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 2;
+        gbc.anchor = GridBagConstraints.EAST;
+        gbc.insets = new Insets(5, 5, 5, 5);
+        selectionPanel.add(isGamePanel, gbc);
+    }
 }

=== modified file 'src/pipe/gui/widgets/QueryPane.java'
--- src/pipe/gui/widgets/QueryPane.java	2020-05-27 13:15:44 +0000
+++ src/pipe/gui/widgets/QueryPane.java	2020-08-03 12:48:32 +0000
@@ -320,31 +320,18 @@
 		addQueryButton.setPreferredSize(dimension);
 		addQueryButton.setToolTipText(toolTipNewQuery);
 		addQueryButton.addActionListener(new ActionListener() {
-			public void actionPerformed(ActionEvent e) {				
-				int openCTLDialog = JOptionPane.YES_OPTION;
-				boolean netIsUntimed = tabContent.network().isUntimed();
-				String optionText = "Do you want to create a CTL query (use for untimed nets) \n or a Reachability query (use for timed nets)?";
-				
-				// YES_OPTION = CTL dialog, NO_OPTION = Reachability dialog
-				Object[] options = {
-					"CTL",
-					"Reachability"};
-				
-				TAPNQuery q = null;
-				if(netIsUntimed){
-					openCTLDialog = JOptionPane.showOptionDialog(CreateGui.getApp(), optionText, "Query Dialog", JOptionPane.YES_NO_OPTION, JOptionPane.QUESTION_MESSAGE, null, options, options[0]);
-					if(openCTLDialog == JOptionPane.YES_OPTION){
-						q = CTLQueryDialog.showQueryDialogue(CTLQueryDialog.QueryDialogueOption.Save, null, tabContent.network(), tabContent.getGuiModels());
-					} else if(openCTLDialog == JOptionPane.NO_OPTION){
-						q = QueryDialog.showQueryDialogue(QueryDialogueOption.Save, null, tabContent.network(), tabContent.getGuiModels());
-					}
-				} else{
+			public void actionPerformed(ActionEvent e) {
+
+				TAPNQuery q;
+				if (!tabContent.isNetTimed()){
+                    q = CTLQueryDialog.showQueryDialogue(CTLQueryDialog.QueryDialogueOption.Save, null, tabContent.network(), tabContent.getGuiModels());
+				} else {
 					q = QueryDialog.showQueryDialogue(QueryDialogueOption.Save, null, tabContent.network(), tabContent.getGuiModels());
 				}
-				if (q != null) {
-					undoManager.addNewEdit(new AddQueryCommand(q, tabContent));
-					addQuery(q);
-				}
+
+                undoManager.addNewEdit(new AddQueryCommand(q, tabContent));
+                addQuery(q);
+
 				updateQueryButtons();
 			}
 		});
@@ -496,7 +483,7 @@
 			tempFile = File.createTempFile(CreateGui.getAppGui().getCurrentTabName(), ".xml");
 
 			TabContent tab = CreateGui.getApp().getCurrentTab();
-			tab.writeNetToFile(tempFile, selectedQueries);
+			tab.writeNetToFile(tempFile, selectedQueries, tab.getLens());
 			BatchProcessingDialog.showBatchProcessingDialog(queryList);
 			tempFile.deleteOnExit();
 			if(tempFile == null) {