Merge lp:~tapaal-contributor/tapaal/cpn-remove-add into lp:tapaal

[Lena Ernstsen]

Removed the add button and moved the color type combobox

The color type comobox is moved to the left side of the dialog.
The undo/redo should be able to revert colortype changes as well.
Added placeholders in the color combobox to make more intuitive.

[Jiri Srba (srba)]

If you make a product of enumaration and integer range, make a guard of that type. Things get broken. Also if you save/load the net again and click in the guard on equality sign, it will show that it is of type Dot, even though it was decleared as another color type. Also, the color type for equality etc. shows only too little of text and the > closing paranthesis for a tupple is broken (shows as \gte).

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/cpn-remove-add]

1629. By Jiri Srba on 2022-03-20

merged with cpn-gui-dev

1630. By Lena Ernstsen on 2022-03-21

variables are also displayed in color combobox for product types

[Jiri Srba (srba)]

review: Approve

=== modified file 'build.gradle'
--- build.gradle	2021-08-11 11:19:19 +0000
+++ build.gradle	2022-03-21 20:20:44 +0000
@@ -1,27 +1,38 @@
 plugins {
     id 'java'
     id 'application'
-    id 'org.jetbrains.kotlin.jvm' version '1.3.71'
+    id 'org.jetbrains.kotlin.jvm' version '1.6.10'
+    id 'org.jetbrains.kotlin.plugin.serialization' version '1.6.10'
     id "ca.coglinc.javacc" version "2.4.0"
 }
 
 group 'net.tapaal'
 version '4.0-SNAPSHOT'
 
+var targetJavaVersion = JavaVersion.VERSION_11
+var targetKotlinVersion = "1.6"
 java {
-    sourceCompatibility = JavaVersion.VERSION_11
-    targetCompatibility = JavaVersion.VERSION_11
-}
+    sourceCompatibility = targetJavaVersion
+    targetCompatibility = targetJavaVersion
+}
+
+compileKotlin {
+    sourceCompatibility = targetJavaVersion
+    targetCompatibility = targetJavaVersion
+
+    kotlinOptions {
+        jvmTarget = targetJavaVersion
+        apiVersion = targetKotlinVersion
+        languageVersion = targetKotlinVersion
+    }
+}
+
+mainClassName = 'TAPAAL'
 
 repositories {
     mavenCentral()
 }
 
-compileJavacc {
-    inputDirectory = file('src/')
-    //outputDirectory = file(project.buildDir.absolutePath + '/generated/javacc')
-}
-
 //Set the soruce and resource dir
 sourceSets {
     main {
@@ -43,52 +54,43 @@
     }
 }
 
-mainClassName = 'TAPAAL'
+compileJavacc {
+    inputDirectory = file('src/')
+}
+
 
 jar {
     exclude 'META-INF/*.SF', 'META-INF/*.DSA', 'META-INF/*.RSA', 'META-INF/*.MF'
 
     //Sets the main call for the Jar, you can double click to run the jar file
     manifest {
-        attributes 'Main-Class': 'TAPAAL'
+        attributes (
+            'Main-Class': mainClassName
+        )
     }
     //The following lines makes libs a part of the build jar file (standalone jar)
     //from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
 }
 
 dependencies {
-    implementation group: 'commons-cli', name: 'commons-cli', version: '1.4'
+    implementation group: 'commons-cli', name: 'commons-cli', version: '1.5.0'
     implementation group: 'org.swinglabs.swingx', name: 'swingx-all', version: '1.6.5-1'
-    implementation group: 'net.java.dev.jna', name: 'jna', version: '4.5.1'
-    implementation 'org.jetbrains:annotations:16.0.2'
-    //compile group: 'com.apple', name: 'AppleJavaExtensions', version: '1.4' // Not working
+    implementation group: 'net.java.dev.jna', name: 'jna', version: '5.9.0'
+    implementation 'org.jetbrains:annotations:22.0.0'
+    implementation 'org.jetbrains.kotlinx:kotlinx-serialization-json:1.3.2'
 
     //Add jars from libs dir
-    implementation fileTree(dir: 'libs', include: ['*.jar'])
+    //implementation fileTree(dir: 'libs', include: ['*.jar'])
 
-    //Junit
+    //JUnit
     testImplementation(
-        'org.junit.jupiter:junit-jupiter-api:5.4.2'
+        'org.junit.jupiter:junit-jupiter-api:5.8.2'
     )
     testRuntimeOnly(
-        'org.junit.jupiter:junit-jupiter-engine:5.4.2',
-        'org.junit.vintage:junit-vintage-engine:5.4.2'
+        'org.junit.jupiter:junit-jupiter-engine:5.8.2',
+        'org.junit.vintage:junit-vintage-engine:5.8.2'
     )
-    implementation "org.jetbrains.kotlin:kotlin-stdlib-jdk8"
 }
 test {
     useJUnitPlatform()
-    afterTest { desc, result ->
-        logger.quiet "Executing test ${desc.name} [${desc.className}] with result: ${result.resultType}"
-    }
-}
-compileKotlin {
-    kotlinOptions {
-        jvmTarget = JavaVersion.VERSION_11
-    }
-}
-compileTestKotlin {
-    kotlinOptions {
-        jvmTarget = JavaVersion.VERSION_11
-    }
 }

=== modified file 'gradle/wrapper/gradle-wrapper.jar'
Binary files gradle/wrapper/gradle-wrapper.jar and gradle/wrapper/gradle-wrapper.jar differ
=== modified file 'gradle/wrapper/gradle-wrapper.properties'
--- gradle/wrapper/gradle-wrapper.properties	2020-04-06 12:41:08 +0000
+++ gradle/wrapper/gradle-wrapper.properties	2022-03-21 20:20:44 +0000
@@ -1,6 +1,5 @@
-#Mon Apr 06 14:40:09 CEST 2020
-distributionUrl=https\://services.gradle.org/distributions/gradle-6.3-all.zip
-distributionBase=GRADLE_USER_HOME
-distributionPath=wrapper/dists
-zipStorePath=wrapper/dists
-zipStoreBase=GRADLE_USER_HOME
+distributionBase=GRADLE_USER_HOME
+distributionPath=wrapper/dists
+distributionUrl=https\://services.gradle.org/distributions/gradle-7.2-bin.zip
+zipStoreBase=GRADLE_USER_HOME
+zipStorePath=wrapper/dists

=== modified file 'gradlew'
--- gradlew	2020-09-01 08:14:52 +0000
+++ gradlew	2022-03-21 20:20:44 +0000
@@ -82,6 +82,7 @@
 
 CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar
 
+
 # Determine the Java command to use to start the JVM.
 if [ -n "$JAVA_HOME" ] ; then
     if [ -x "$JAVA_HOME/jre/sh/java" ] ; then
@@ -129,6 +130,7 @@
 if [ "$cygwin" = "true" -o "$msys" = "true" ] ; then
     APP_HOME=`cygpath --path --mixed "$APP_HOME"`
     CLASSPATH=`cygpath --path --mixed "$CLASSPATH"`
+
     JAVACMD=`cygpath --unix "$JAVACMD"`
 
     # We build the pattern for arguments to be converted via cygpath

=== modified file 'gradlew.bat'
--- gradlew.bat	2020-03-28 10:29:30 +0000
+++ gradlew.bat	2022-03-21 20:20:44 +0000
@@ -40,7 +40,7 @@
 
 set JAVA_EXE=java.exe
 %JAVA_EXE% -version >NUL 2>&1
-if "%ERRORLEVEL%" == "0" goto init
+if "%ERRORLEVEL%" == "0" goto execute
 
 echo.
 echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
@@ -54,7 +54,7 @@
 set JAVA_HOME=%JAVA_HOME:"=%
 set JAVA_EXE=%JAVA_HOME%/bin/java.exe
 
-if exist "%JAVA_EXE%" goto init
+if exist "%JAVA_EXE%" goto execute
 
 echo.
 echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
@@ -64,28 +64,14 @@
 
 goto fail
 
-:init
-@rem Get command-line arguments, handling Windows variants
-
-if not "%OS%" == "Windows_NT" goto win9xME_args
-
-:win9xME_args
-@rem Slurp the command line arguments.
-set CMD_LINE_ARGS=
-set _SKIP=2
-
-:win9xME_args_slurp
-if "x%~1" == "x" goto execute
-
-set CMD_LINE_ARGS=%*
-
 :execute
 @rem Setup the command line
 
 set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
 
+
 @rem Execute Gradle
-"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %CMD_LINE_ARGS%
+"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %*
 
 :end
 @rem End local scope for the variables with windows NT shell

=== modified file 'src/dk/aau/cs/TCTL/AritmeticOperator.java'
--- src/dk/aau/cs/TCTL/AritmeticOperator.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/AritmeticOperator.java	2022-03-21 20:20:44 +0000
@@ -4,7 +4,7 @@
 
 public class AritmeticOperator extends TCTLAbstractStateProperty {
 	
-	String operator;
+	final String operator;
 	
 	public AritmeticOperator(String operator) {
 		this.operator = operator;

=== modified file 'src/dk/aau/cs/TCTL/LTLGNode.java'
--- src/dk/aau/cs/TCTL/LTLGNode.java	2021-10-08 06:26:14 +0000
+++ src/dk/aau/cs/TCTL/LTLGNode.java	2022-03-21 20:20:44 +0000
@@ -20,7 +20,7 @@
     }
 
     public LTLGNode() {
-        this.property = new TCTLStatePlaceHolder();;
+        this.property = new TCTLStatePlaceHolder();
         this.property.setParent(this);
     }
 

=== modified file 'src/dk/aau/cs/TCTL/LTLUNode.java'
--- src/dk/aau/cs/TCTL/LTLUNode.java	2021-10-08 06:26:14 +0000
+++ src/dk/aau/cs/TCTL/LTLUNode.java	2022-03-21 20:20:44 +0000
@@ -54,7 +54,7 @@
         StringPosition leftPos = new StringPosition(leftStart, leftEnd, left);
 
         int rightStart = right.isSimpleProperty() ? 0 : 1;
-        rightStart += leftEnd + 3 + + (left.isSimpleProperty() ? 0 : 1);
+        rightStart += leftEnd + 3 + (left.isSimpleProperty() ? 0 : 1);
         int rightEnd = rightStart + right.toString().length();
         StringPosition rightPos = new StringPosition(rightStart, rightEnd, right);
 

=== modified file 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.jj'
--- src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.jj	2021-09-30 07:05:48 +0000
+++ src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.jj	2022-03-21 20:20:44 +0000
@@ -127,12 +127,12 @@
 	TCTLAbstractStateProperty child = null; 
 }
 {
-	( 
-		<EF> child = OrExpr() {return new TCTLEFNode(child); } 
-		| <EG> child = OrExpr() {return new TCTLEGNode(child); } 
-		| <AF> child = OrExpr() {return new TCTLAFNode(child); } 
-		| <AG> child = OrExpr() {return new TCTLAGNode(child); } 
-	) 
+	(
+		<EF> child = OrExpr() {return new TCTLEFNode(child); }
+		| <EG> child = OrExpr() {return new TCTLEGNode(child); }
+		| <AF> child = OrExpr() {return new TCTLAFNode(child); }
+		| <AG> child = OrExpr() {return new TCTLAGNode(child); }
+	)
 }
 
 TCTLAbstractStateProperty OrExpr() : 

=== modified file 'src/dk/aau/cs/TCTL/StringPosition.java'
--- src/dk/aau/cs/TCTL/StringPosition.java	2011-02-03 19:03:15 +0000
+++ src/dk/aau/cs/TCTL/StringPosition.java	2022-03-21 20:20:44 +0000
@@ -4,10 +4,9 @@
 
 	private int startIndex;
 	private int endIndex;
-	private TCTLAbstractProperty object;
+	private final TCTLAbstractProperty object;
 
-	public StringPosition(int startIndex, int endIndex,
-			TCTLAbstractProperty object) {
+	public StringPosition(int startIndex, int endIndex, TCTLAbstractProperty object) {
 		this.startIndex = startIndex;
 		this.endIndex = endIndex;
 		this.object = object;

=== modified file 'src/dk/aau/cs/TCTL/TCTLAUNode.java'
--- src/dk/aau/cs/TCTL/TCTLAUNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLAUNode.java	2022-03-21 20:20:44 +0000
@@ -50,7 +50,7 @@
 		StringPosition leftPos = new StringPosition(leftStart, leftEnd, left);
 		
 		int rightStart = right.isSimpleProperty() ? 0 : 1;
-		rightStart += leftEnd + 3 + + (left.isSimpleProperty() ? 0 : 1);
+		rightStart += leftEnd + 3 + (left.isSimpleProperty() ? 0 : 1);
 		int rightEnd = rightStart + right.toString().length();
 		StringPosition rightPos = new StringPosition(rightStart, rightEnd, right);
 

=== modified file 'src/dk/aau/cs/TCTL/TCTLAbstractProperty.java'
--- src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2021-08-16 07:29:37 +0000
+++ src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2022-03-21 20:20:44 +0000
@@ -2,8 +2,6 @@
 
 import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
 
-import java.util.Locale;
-
 public abstract class TCTLAbstractProperty {
 
 	// used to determine whether to put parenthesis around the property

=== modified file 'src/dk/aau/cs/TCTL/TCTLAbstractStateProperty.java'
--- src/dk/aau/cs/TCTL/TCTLAbstractStateProperty.java	2011-02-03 19:03:15 +0000
+++ src/dk/aau/cs/TCTL/TCTLAbstractStateProperty.java	2022-03-21 20:20:44 +0000
@@ -18,18 +18,4 @@
 
 	@Override
 	public abstract TCTLAbstractStateProperty copy();
-
-	// public abstract void accept(ICSLVisitor visitor) throws
-	// ModelCheckingException;
-
-	// protected abstract void setCompositionality(boolean
-	// withinSteadyStateOperator);
-
-	// public void setCompositionality() {
-	// setCompositionality(false);
-	// }
-	//	
-	// public boolean isCompositional() {
-	// return isCompositional;
-	// }
 }

=== modified file 'src/dk/aau/cs/TCTL/TCTLAndListNode.java'
--- src/dk/aau/cs/TCTL/TCTLAndListNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLAndListNode.java	2022-03-21 20:20:44 +0000
@@ -77,8 +77,7 @@
 				s.append(" and ");
 			}
 
-			s.append(prop.isSimpleProperty() ? prop.toString() : "("
-					+ prop.toString() + ")");
+			s.append(prop.isSimpleProperty() ? prop.toString() : "(" + prop + ")");
 			firstTime = false;
 		}
 

=== modified file 'src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java'
--- src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java	2022-03-21 20:20:44 +0000
@@ -94,31 +94,6 @@
         return false;
     }
 
-/*    @Override
-    public StringPosition[] getChildren() {
-        StringPosition[] children = new StringPosition[2];
-
-        int start = 0;
-        int end = 0;
-        boolean leftSimpleProperty = left.isSimpleProperty();
-
-        start = leftSimpleProperty ? 0 : 1;
-        end = start + left.toString().length();
-
-        StringPosition posLeft = new StringPosition(start, end, left);
-
-        start = end + 5 + (right.isSimpleProperty() ? 0 : 1)
-            + (leftSimpleProperty ? 0 : 1);
-
-        end = start + right.toString().length();
-
-        StringPosition posRight = new StringPosition(start, end, right);
-
-        children[0] = posLeft;
-        children[1] = posRight;
-        return children;
-    }*/
-
     @Override
 	public TCTLAbstractProperty findFirstPlaceHolder() {
 		TCTLAbstractProperty rightP = right.findFirstPlaceHolder(); 

=== modified file 'src/dk/aau/cs/TCTL/TCTLConstNode.java'
--- src/dk/aau/cs/TCTL/TCTLConstNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLConstNode.java	2022-03-21 20:20:44 +0000
@@ -4,7 +4,7 @@
 
 public class TCTLConstNode extends TCTLAbstractStateProperty {
 
-	int constant;
+	final int constant;
 
 	public TCTLConstNode(int constant) {
 		this.constant = constant;

=== modified file 'src/dk/aau/cs/TCTL/TCTLEFNode.java'
--- src/dk/aau/cs/TCTL/TCTLEFNode.java	2021-09-14 20:13:01 +0000
+++ src/dk/aau/cs/TCTL/TCTLEFNode.java	2022-03-21 20:20:44 +0000
@@ -2,8 +2,6 @@
 
 import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
 
-import java.util.HashMap;
-
 public class TCTLEFNode extends TCTLAbstractPathProperty {
 
 	private TCTLAbstractStateProperty property;

=== modified file 'src/dk/aau/cs/TCTL/TCTLOrListNode.java'
--- src/dk/aau/cs/TCTL/TCTLOrListNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLOrListNode.java	2022-03-21 20:20:44 +0000
@@ -77,8 +77,7 @@
 				s.append(" or ");
 			}
 
-			s.append(prop.isSimpleProperty() ? prop.toString() : "("
-					+ prop.toString() + ")");
+			s.append(prop.isSimpleProperty() ? prop.toString() : "(" + prop + ")");
 			firstTime = false;
 		}
 

=== modified file 'src/dk/aau/cs/TCTL/TCTLPlusListNode.java'
--- src/dk/aau/cs/TCTL/TCTLPlusListNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLPlusListNode.java	2022-03-21 20:20:44 +0000
@@ -8,7 +8,7 @@
 //Represents a list of terms and the operators between then, these are all stored in the terms list
 public class TCTLPlusListNode extends TCTLAbstractStateProperty {
 
-	ArrayList<TCTLAbstractStateProperty> terms;
+	final ArrayList<TCTLAbstractStateProperty> terms;
 	
 	public TCTLPlusListNode(ArrayList<TCTLAbstractStateProperty> terms) {
 		this.terms = terms;

=== modified file 'src/dk/aau/cs/TCTL/TCTLTermListNode.java'
--- src/dk/aau/cs/TCTL/TCTLTermListNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLTermListNode.java	2022-03-21 20:20:44 +0000
@@ -8,7 +8,7 @@
 //Represents a list of factors and the operators between then, these are all stored in the factors list
 public class TCTLTermListNode extends TCTLAbstractStateProperty {
 
-	ArrayList<TCTLAbstractStateProperty> factors;
+	final ArrayList<TCTLAbstractStateProperty> factors;
 
 	public TCTLTermListNode(ArrayList<TCTLAbstractStateProperty> factors) {
 		this.factors = factors;

=== modified file 'src/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java'
--- src/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java	2017-05-14 19:42:09 +0000
+++ src/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java	2022-03-21 20:20:44 +0000
@@ -44,9 +44,9 @@
         XMLCTLQueryParser parser = new XMLCTLQueryParser(prop, queryWrapper);
         queryWrapper.setName(parser.parsePropertyName());
 
-        try{
+        try {
             queryWrapper.setProp(parser.AbstractProperty());
-        } catch (XMLQueryParseException e){
+        } catch (XMLQueryParseException e) {
             queryWrapper.setException(e);
             Logger.log(e);
             return false;
@@ -87,14 +87,14 @@
     }
 
     private TCTLAbstractProperty parseFormula(Node property)
-        throws XMLQueryParseException{
+        throws XMLQueryParseException {
 
         TCTLAbstractProperty childProperty;
         Node child = getFirstChildNode(property);
         String nodeName = property.getNodeName();
         
         String childNodeName = "";
-        if(child != null){
+        if (child != null) {
         	childNodeName = child.getNodeName();
         }
         
@@ -366,38 +366,40 @@
             } else if(nodeName.equals("integer-ge")){
                 return new TCTLAtomicPropositionNode(subformula1, ">=", subformula2);
             }
-        } else if (nodeName.equals("is-fireable")){
-	    // Construct a nested disjunction of transitions.
-	    
-	    children = getAllChildren(property);
-
-            if(children.isEmpty()){
+        } else if (nodeName.equals("is-fireable")) {
+            // Construct a nested disjunction of transitions.
+
+            children = getAllChildren(property);
+
+            if (children.isEmpty()) {
                 throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
-            } else if(children.size() == 1) {
-		String[] splits = getText(children.get(0)).replace("\n", "").split("\\.");
-		
-		// Check if transition contains a template name
-                if(splits.length > 1){
-		    return new TCTLTransitionNode(splits[0], splits[1]);
+            } else if (children.size() == 1) {
+                String[] splits = getText(children.get(0)).replace("\n", "").split("\\.");
+
+                // Check if transition contains a template name
+                if (splits.length > 1) {
+                    return new TCTLTransitionNode(splits[0], splits[1]);
                 } else {
-		    return new TCTLTransitionNode(splits[0]);
-                }
-	    } else {
-		ArrayList<TCTLAbstractStateProperty> transitions = new ArrayList<TCTLAbstractStateProperty>();
-		
-		for(Node n : children) {
-		    String[] splits = getText(n).replace("\n", "").split("\\.");
-		    
-		    // Check if transition contains a template name
-		    if(splits.length > 1){
-			transitions.add(new TCTLTransitionNode(splits[0], splits[1]));
-		    } else {
-			transitions.add(new TCTLTransitionNode(splits[0]));
-		    }
-		}
-		return new TCTLOrListNode(transitions);
-	    }
-        } else{
+                    return new TCTLTransitionNode(splits[0]);
+                }
+            } else {
+                ArrayList<TCTLAbstractStateProperty> transitions = new ArrayList<TCTLAbstractStateProperty>();
+
+                for (Node n : children) {
+                    String[] splits = getText(n).replace("\n", "").split("\\.");
+
+                    // Check if transition contains a template name
+                    if (splits.length > 1) {
+                        transitions.add(new TCTLTransitionNode(splits[0], splits[1]));
+                    } else {
+                        transitions.add(new TCTLTransitionNode(splits[0]));
+                    }
+                }
+                return new TCTLOrListNode(transitions);
+            }
+        } else if (nodeName.equals("control")) {
+            return parseFormula(child);
+        }else{
         	parseFormula(property);
         }
 

=== modified file 'src/dk/aau/cs/TCTL/visitors/AddTemplateVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/AddTemplateVisitor.java	2014-05-22 20:26:41 +0000
+++ src/dk/aau/cs/TCTL/visitors/AddTemplateVisitor.java	2022-03-21 20:20:44 +0000
@@ -3,7 +3,7 @@
 import dk.aau.cs.TCTL.TCTLPlaceNode;
 
 public class AddTemplateVisitor extends VisitorBase {
-	private String templateName;
+	private final String templateName;
 
 	public AddTemplateVisitor(String templateName) {
 		this.templateName = templateName;

=== modified file 'src/dk/aau/cs/TCTL/visitors/BroadcastTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/BroadcastTranslationQueryVisitor.java	2019-03-22 10:13:18 +0000
+++ src/dk/aau/cs/TCTL/visitors/BroadcastTranslationQueryVisitor.java	2022-03-21 20:20:44 +0000
@@ -7,8 +7,8 @@
 	protected static final String PLOCK = "P_lock";
 	protected static final String TOKEN_TEMPLATE_NAME = "Token";
 
-	private boolean useSymmetry;
-	private int totalTokens;
+	private final boolean useSymmetry;
+	private final int totalTokens;
 
 	public BroadcastTranslationQueryVisitor(boolean useSymmetry, int totalTokens) {
 		this.useSymmetry = useSymmetry;

=== modified file 'src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java	2021-10-08 06:22:05 +0000
+++ src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java	2022-03-21 20:20:44 +0000
@@ -40,24 +40,27 @@
 	private static final String XML_TRANSITION		= "transition";
 	private static final String XML_INTEGERSUM = "integer-sum";
 	private static final String XML_INTEGERPRODUCT = "integer-product";
-	private static final String XML_INTEGERDIFFERENCE = "integer-difference";
+    private static final String XML_INTEGERDIFFERENCE = "integer-difference";
+    private static final String CONTROL = "control";
 
-	private StringBuffer XMLQuery;
-        
-        public CTLQueryVisitor() {
-            this.XMLQuery = new StringBuffer();
-        }
-        
-        public String getXMLQueryFor(TCTLAbstractProperty property, String queryName) {
-            buildXMLQuery(property, queryName);
-            return getFormatted();
-        }
+	private final StringBuffer XMLQuery;
+        
+    public CTLQueryVisitor() {
+        this.XMLQuery = new StringBuffer();
+    }
+        
+    public String getXMLQueryFor(TCTLAbstractProperty property, String queryName, boolean control) {
+        buildXMLQuery(property, queryName, control);
+        return getFormatted();
+    }
 	
-	public void buildXMLQuery(TCTLAbstractProperty property, String queryName) {
-                XMLQuery.append(startTag(XML_PROP) + queryInfo(queryName) + startTag(XML_FORMULA));
+	public void buildXMLQuery(TCTLAbstractProperty property, String queryName, boolean control) {
+        XMLQuery.append(startTag(XML_PROP) + queryInfo(queryName) + startTag(XML_FORMULA));
+        if (control) XMLQuery.append(startTag(CONTROL));
 		property.accept(this, null);
-		XMLQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));              
-	}
+        if (control) XMLQuery.append(endTag(CONTROL));
+		XMLQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));
+    }
         
         public String getFormatted() {
             XMLFormatter formatter = new XMLFormatter();
@@ -175,13 +178,17 @@
 		assert termListNode.getProperties().get(1) instanceof AritmeticOperator;
 		AritmeticOperator operator = (AritmeticOperator)termListNode.getProperties().get(1);
 		String op = operator.toString();
-		if (op.equals("+")) {
-		    createList(termListNode.getProperties(), context, XML_INTEGERSUM);
-		} else if (op.equals("*")) {
-		    createList(termListNode.getProperties(), context, XML_INTEGERPRODUCT);
-		} else if (op.equals("-")) {
-		    createList(termListNode.getProperties(), context, XML_INTEGERDIFFERENCE);
-		}
+        switch (op) {
+            case "+":
+                createList(termListNode.getProperties(), context, XML_INTEGERSUM);
+                break;
+            case "*":
+                createList(termListNode.getProperties(), context, XML_INTEGERPRODUCT);
+                break;
+            case "-":
+                createList(termListNode.getProperties(), context, XML_INTEGERDIFFERENCE);
+                break;
+        }
 	}
 
 	private void createList(List<TCTLAbstractStateProperty> properties, Object context, String seperator) {
@@ -213,7 +220,7 @@
 	}
 	
 	public void visit(TCTLConstNode tctlConstNode, Object context){
-		XMLQuery.append(wrapInTag(String.valueOf(tctlConstNode.getConstant()) + "", XML_INTEGERCONSTANT));
+		XMLQuery.append(wrapInTag(tctlConstNode.getConstant() + "", XML_INTEGERCONSTANT));
 	}
 
 	public void visit(TCTLPlaceNode tctlPlaceNode, Object context){
@@ -232,23 +239,31 @@
 	public void visit(TCTLAtomicPropositionNode atomicPropositionNode,
 			Object context) {
 		String opTest = atomicPropositionNode.getOp();
-		String op = new String();
-		
-		if (opTest.equals("<")){
-			op = XML_INTEGERLT;
-		} else if(opTest.equals("<=")){
-			op = XML_INTEGERLE;
-		} else if(opTest.equals("=")){
-			op = XML_INTEGEREQ;
-		} else if(opTest.equals("!=")){
-			op = XML_INTEGERNE;
-		} else if(opTest.equals(">")){
-			op = XML_INTEGERGT;
-		} else if(opTest.equals(">=")){
-			op = XML_INTEGERGE;
-		} else {
-			op = "MISSING_OPERATOR";
-		}
+		String op;
+
+        switch (opTest) {
+            case "<":
+                op = XML_INTEGERLT;
+                break;
+            case "<=":
+                op = XML_INTEGERLE;
+                break;
+            case "=":
+                op = XML_INTEGEREQ;
+                break;
+            case "!=":
+                op = XML_INTEGERNE;
+                break;
+            case ">":
+                op = XML_INTEGERGT;
+                break;
+            case ">=":
+                op = XML_INTEGERGE;
+                break;
+            default:
+                op = "MISSING_OPERATOR";
+                break;
+        }
 		
 		XMLQuery.append(startTag(op));
 		atomicPropositionNode.getLeft().accept(this, context);

=== modified file 'src/dk/aau/cs/TCTL/visitors/CombiTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/CombiTranslationQueryVisitor.java	2019-03-22 10:13:18 +0000
+++ src/dk/aau/cs/TCTL/visitors/CombiTranslationQueryVisitor.java	2022-03-21 20:20:44 +0000
@@ -11,13 +11,13 @@
 	protected static final String PLOCK = "P_lock";
 	protected static final String TOKEN_TEMPLATE_NAME = "Token";
 
-	private boolean useSymmetry;
-	private int totalTokens;
-	private TimedArcPetriNet model;
-	private Hashtable<String, Boolean> placeNameToTimed;
-	private int maxDegDif;
-	private int initTransitions;
-	private int maxTimeIn;
+	private final boolean useSymmetry;
+	private final int totalTokens;
+	private final TimedArcPetriNet model;
+	private final Hashtable<String, Boolean> placeNameToTimed;
+	private final int maxDegDif;
+	private final int initTransitions;
+	private final int maxTimeIn;
 
 	public CombiTranslationQueryVisitor(boolean useSymmetry, int totalTokens, TimedArcPetriNet model, Hashtable<String, Boolean> placeNameToTimed, int maxDegDif, int initTransitions, int maxTimeIn) {
 		this.useSymmetry = useSymmetry;

=== modified file 'src/dk/aau/cs/TCTL/visitors/ContainsPlaceWithDisabledTemplateVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ContainsPlaceWithDisabledTemplateVisitor.java	2014-05-22 20:26:41 +0000
+++ src/dk/aau/cs/TCTL/visitors/ContainsPlaceWithDisabledTemplateVisitor.java	2022-03-21 20:20:44 +0000
@@ -6,7 +6,7 @@
 
 public class ContainsPlaceWithDisabledTemplateVisitor extends VisitorBase implements ITCTLVisitor {
 	
-	private TimedArcPetriNetNetwork network;
+	private final TimedArcPetriNetNetwork network;
 
 	public ContainsPlaceWithDisabledTemplateVisitor(TimedArcPetriNetNetwork network){
 		this.network = network;
@@ -14,15 +14,18 @@
 
 	@Override
 	public void visit(TCTLPlaceNode placeNode, Object context) {
-		if(placeNode.getTemplate().equals("") && network.getSharedPlaceByName(placeNode.getPlace()) != null)
-			return;
+		if(placeNode.getTemplate().equals("") && network.getSharedPlaceByName(placeNode.getPlace()) != null) {
+            return;
+        }
 		
 		for(TimedArcPetriNet net : network.activeTemplates()) {
-			if(placeNode.getTemplate().equals(net.name()) && net.getPlaceByName(placeNode.getPlace()) != null) 
-				return;
+			if(placeNode.getTemplate().equals(net.name()) && net.getPlaceByName(placeNode.getPlace()) != null) {
+                return;
+            }
 		}
 		
-		if(context instanceof BooleanResult)
-			((BooleanResult)context).setResult(false);
+		if(context instanceof BooleanResult) {
+            ((BooleanResult)context).setResult(false);
+        }
 	}
 }

=== modified file 'src/dk/aau/cs/TCTL/visitors/ContainsSharedPlaceVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ContainsSharedPlaceVisitor.java	2014-05-22 20:26:41 +0000
+++ src/dk/aau/cs/TCTL/visitors/ContainsSharedPlaceVisitor.java	2022-03-21 20:20:44 +0000
@@ -3,7 +3,7 @@
 import dk.aau.cs.TCTL.TCTLPlaceNode;
 
 public class ContainsSharedPlaceVisitor extends VisitorBase implements ITCTLVisitor {
-	private String sharedPlaceName;
+	private final String sharedPlaceName;
 
 	public ContainsSharedPlaceVisitor(String sharedPlaceName){
 		this.sharedPlaceName = sharedPlaceName;
@@ -11,8 +11,9 @@
 
 	@Override
 	public void visit(TCTLPlaceNode placeNode, Object context) {
-		if(placeNode.getTemplate().equals("") && placeNode.getPlace().equals(sharedPlaceName)) 
-			((BooleanResult)context).setResult(true);
+		if(placeNode.getTemplate().equals("") && placeNode.getPlace().equals(sharedPlaceName)) {
+            ((BooleanResult)context).setResult(true);
+        }
 	}
 
 }

=== modified file 'src/dk/aau/cs/TCTL/visitors/ContainsSharedTransitionVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ContainsSharedTransitionVisitor.java	2017-03-12 00:33:00 +0000
+++ src/dk/aau/cs/TCTL/visitors/ContainsSharedTransitionVisitor.java	2022-03-21 20:20:44 +0000
@@ -3,7 +3,7 @@
 import dk.aau.cs.TCTL.TCTLTransitionNode;
 
 public class ContainsSharedTransitionVisitor extends VisitorBase implements ITCTLVisitor {
-	private String sharedTransitionName;
+	private final String sharedTransitionName;
 
 	public ContainsSharedTransitionVisitor(String sharedTransitionName){
 		this.sharedTransitionName = sharedTransitionName;

=== modified file 'src/dk/aau/cs/TCTL/visitors/FixAbbrivPlaceNames.java'
--- src/dk/aau/cs/TCTL/visitors/FixAbbrivPlaceNames.java	2014-11-01 09:31:54 +0000
+++ src/dk/aau/cs/TCTL/visitors/FixAbbrivPlaceNames.java	2022-03-21 20:20:44 +0000
@@ -1,8 +1,3 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
 package dk.aau.cs.TCTL.visitors;
 
 import dk.aau.cs.TCTL.TCTLAbstractProperty;
@@ -10,13 +5,9 @@
 import dk.aau.cs.util.Tuple;
 import java.util.ArrayList;
 
-/**
- *
- * @author jakob
- */
 public class FixAbbrivPlaceNames extends VisitorBase {
 
-        private ArrayList<Tuple<String, String>> templatePlaceNames;
+        private final ArrayList<Tuple<String, String>> templatePlaceNames;
 
         public FixAbbrivPlaceNames(ArrayList<Tuple<String, String>> templatePlaceNames) {
                 this.templatePlaceNames = templatePlaceNames;

=== modified file 'src/dk/aau/cs/TCTL/visitors/FixAbbrivTransitionNames.java'
--- src/dk/aau/cs/TCTL/visitors/FixAbbrivTransitionNames.java	2017-03-12 00:33:00 +0000
+++ src/dk/aau/cs/TCTL/visitors/FixAbbrivTransitionNames.java	2022-03-21 20:20:44 +0000
@@ -12,7 +12,7 @@
 
 public class FixAbbrivTransitionNames extends VisitorBase {
 
-        private ArrayList<Tuple<String, String>> templateTransitionNames;
+        private final ArrayList<Tuple<String, String>> templateTransitionNames;
 
         public FixAbbrivTransitionNames(ArrayList<Tuple<String, String>> templateTransitionNames) {
                 this.templateTransitionNames = templateTransitionNames;

=== modified file 'src/dk/aau/cs/TCTL/visitors/HasDeadlockVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/HasDeadlockVisitor.java	2013-05-18 21:26:56 +0000
+++ src/dk/aau/cs/TCTL/visitors/HasDeadlockVisitor.java	2022-03-21 20:20:44 +0000
@@ -16,7 +16,7 @@
 		((Context)context).hasDeadlock = true;
 	}
 
-	private class Context{
+	private static class Context{
 		public boolean hasDeadlock = true;
 	}
 }

=== modified file 'src/dk/aau/cs/TCTL/visitors/IsReachabilityVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/IsReachabilityVisitor.java	2017-08-03 11:48:35 +0000
+++ src/dk/aau/cs/TCTL/visitors/IsReachabilityVisitor.java	2022-03-21 20:20:44 +0000
@@ -4,7 +4,7 @@
 
 public class IsReachabilityVisitor extends VisitorBase {
 
-    private class Context{
+    private static class Context{
         public boolean isReachability = true;
         public int nTempOp = 0; // number of temporal operators
     }

=== modified file 'src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java	2021-10-14 06:28:05 +0000
+++ src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java	2022-03-21 20:20:44 +0000
@@ -42,7 +42,7 @@
     private static final String XML_INTEGERPRODUCT = "integer-product";
     private static final String XML_INTEGERDIFFERENCE = "integer-difference";
 
-    private StringBuffer XMLQuery;
+    private final StringBuffer XMLQuery;
 
     public LTLQueryVisitor() {
         this.XMLQuery = new StringBuffer();
@@ -137,12 +137,16 @@
         assert termListNode.getProperties().get(1) instanceof AritmeticOperator;
         AritmeticOperator operator = (AritmeticOperator)termListNode.getProperties().get(1);
         String op = operator.toString();
-        if (op.equals("+")) {
-            createList(termListNode.getProperties(), context, XML_INTEGERSUM);
-        } else if (op.equals("*")) {
-            createList(termListNode.getProperties(), context, XML_INTEGERPRODUCT);
-        } else if (op.equals("-")) {
-            createList(termListNode.getProperties(), context, XML_INTEGERDIFFERENCE);
+        switch (op) {
+            case "+":
+                createList(termListNode.getProperties(), context, XML_INTEGERSUM);
+                break;
+            case "*":
+                createList(termListNode.getProperties(), context, XML_INTEGERPRODUCT);
+                break;
+            case "-":
+                createList(termListNode.getProperties(), context, XML_INTEGERDIFFERENCE);
+                break;
         }
     }
 
@@ -175,7 +179,7 @@
     }
 
     public void visit(TCTLConstNode tctlConstNode, Object context){
-        XMLQuery.append(wrapInTag(String.valueOf(tctlConstNode.getConstant()) + "", XML_INTEGERCONSTANT));
+        XMLQuery.append(wrapInTag(tctlConstNode.getConstant() + "", XML_INTEGERCONSTANT));
     }
 
     public void visit(TCTLPlaceNode tctlPlaceNode, Object context){
@@ -194,22 +198,30 @@
     public void visit(TCTLAtomicPropositionNode atomicPropositionNode,
                       Object context) {
         String opTest = atomicPropositionNode.getOp();
-        String op = new String();
+        String op;
 
-        if (opTest.equals("<")){
-            op = XML_INTEGERLT;
-        } else if(opTest.equals("<=")){
-            op = XML_INTEGERLE;
-        } else if(opTest.equals("=")){
-            op = XML_INTEGEREQ;
-        } else if(opTest.equals("!=")){
-            op = XML_INTEGERNE;
-        } else if(opTest.equals(">")){
-            op = XML_INTEGERGT;
-        } else if(opTest.equals(">=")){
-            op = XML_INTEGERGE;
-        } else {
-            op = "MISSING_OPERATOR";
+        switch (opTest) {
+            case "<":
+                op = XML_INTEGERLT;
+                break;
+            case "<=":
+                op = XML_INTEGERLE;
+                break;
+            case "=":
+                op = XML_INTEGEREQ;
+                break;
+            case "!=":
+                op = XML_INTEGERNE;
+                break;
+            case ">":
+                op = XML_INTEGERGT;
+                break;
+            case ">=":
+                op = XML_INTEGERGE;
+                break;
+            default:
+                op = "MISSING_OPERATOR";
+                break;
         }
 
         XMLQuery.append(startTag(op));

=== modified file 'src/dk/aau/cs/TCTL/visitors/OptimizedStandardTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/OptimizedStandardTranslationQueryVisitor.java	2019-03-23 07:51:29 +0000
+++ src/dk/aau/cs/TCTL/visitors/OptimizedStandardTranslationQueryVisitor.java	2022-03-21 20:20:44 +0000
@@ -11,8 +11,8 @@
 	protected static final String LOCK_BOOL = "lock";
 
 	protected static final String TOKEN_TEMPLATE_NAME = "Token";
-	private boolean useSymmetry;
-	private int totalTokens;
+	private final boolean useSymmetry;
+	private final int totalTokens;
 
 	public OptimizedStandardTranslationQueryVisitor(int totalTokens, boolean useSymmetry) {
 		this.useSymmetry = useSymmetry;

=== modified file 'src/dk/aau/cs/TCTL/visitors/RenamePlaceTCTLVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/RenamePlaceTCTLVisitor.java	2014-05-22 20:26:41 +0000
+++ src/dk/aau/cs/TCTL/visitors/RenamePlaceTCTLVisitor.java	2022-03-21 20:20:44 +0000
@@ -4,8 +4,8 @@
 
 public class RenamePlaceTCTLVisitor extends VisitorBase{
 
-	private String oldPlaceName;
-	private String newPlaceName;
+	private final String oldPlaceName;
+	private final String newPlaceName;
 
 	public RenamePlaceTCTLVisitor(String oldName, String newName) {
 		oldPlaceName = oldName;

=== modified file 'src/dk/aau/cs/TCTL/visitors/RenameTransitionTCTLVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/RenameTransitionTCTLVisitor.java	2017-03-12 00:33:00 +0000
+++ src/dk/aau/cs/TCTL/visitors/RenameTransitionTCTLVisitor.java	2022-03-21 20:20:44 +0000
@@ -4,8 +4,8 @@
 
 public class RenameTransitionTCTLVisitor extends VisitorBase{
 
-	private String oldTransitionName;
-	private String newTransitionName;
+	private final String oldTransitionName;
+	private final String newTransitionName;
 
 	public RenameTransitionTCTLVisitor(String oldName, String newName) {
 		oldTransitionName = oldName;

=== modified file 'src/dk/aau/cs/TCTL/visitors/StandardTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/StandardTranslationQueryVisitor.java	2019-03-23 07:51:29 +0000
+++ src/dk/aau/cs/TCTL/visitors/StandardTranslationQueryVisitor.java	2022-03-21 20:20:44 +0000
@@ -12,7 +12,7 @@
 
 	protected static final String TOKEN_TEMPLATE_NAME = "Token";
 
-	private int totalTokens;
+	private final int totalTokens;
 
 	public StandardTranslationQueryVisitor(int totalTokens) {
 		this.totalTokens = totalTokens;

=== modified file 'src/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java	2017-03-12 00:33:00 +0000
+++ src/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java	2022-03-21 20:20:44 +0000
@@ -9,7 +9,7 @@
 
 public class VerifyPlaceNamesVisitor extends VisitorBase {
 
-	private ArrayList<Tuple<String, String>> templatePlaceNames;
+	private final ArrayList<Tuple<String, String>> templatePlaceNames;
 
 	public VerifyPlaceNamesVisitor(ArrayList<Tuple<String, String>> templatePlaceNames) {
 		this.templatePlaceNames = templatePlaceNames;
@@ -31,11 +31,10 @@
 			c.setResult(false);
 		}
 	}
-	
-	// / context class
-	public class Context {
+
+	public static class Context {
 		private Boolean result;
-		private HashSet<String> incorrectPlaceNames;
+		private final HashSet<String> incorrectPlaceNames;
 
 		public Boolean getResult() {
 			return result;

=== modified file 'src/dk/aau/cs/TCTL/visitors/VerifyTransitionNamesVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/VerifyTransitionNamesVisitor.java	2017-03-12 00:33:00 +0000
+++ src/dk/aau/cs/TCTL/visitors/VerifyTransitionNamesVisitor.java	2022-03-21 20:20:44 +0000
@@ -8,7 +8,7 @@
 import dk.aau.cs.util.Tuple;
 
 public class VerifyTransitionNamesVisitor extends VisitorBase {
-	private ArrayList<Tuple<String, String>> templateTransitionNames;
+	private final ArrayList<Tuple<String, String>> templateTransitionNames;
 
 	public VerifyTransitionNamesVisitor(ArrayList<Tuple<String, String>> templateTransitionNames) {
 		this.templateTransitionNames = templateTransitionNames;
@@ -30,11 +30,10 @@
 			c.setResult(false);
 		}
 	}
-	
-	// / context class
-	public class Context {
+
+	public static class Context {
 		private Boolean result;
-		private HashSet<String> incorrectTransitionNames;
+		private final HashSet<String> incorrectTransitionNames;
 
 		public Boolean getResult() {
 			return result;

=== modified file 'src/dk/aau/cs/approximation/ApproximationWorker.java'
--- src/dk/aau/cs/approximation/ApproximationWorker.java	2020-12-16 21:11:57 +0000
+++ src/dk/aau/cs/approximation/ApproximationWorker.java	2022-03-21 20:20:44 +0000
@@ -2,9 +2,12 @@
 
 import java.math.BigDecimal;
 
-import pipe.dataLayer.TAPNQuery.TraceOption;
-import pipe.gui.RunVerificationBase;
-import pipe.gui.widgets.InclusionPlaces;
+import net.tapaal.gui.petrinet.TAPNLens;
+import pipe.gui.petrinet.dataLayer.DataLayer;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
+import pipe.gui.TAPAALGUI;
+import net.tapaal.gui.petrinet.verification.RunVerificationBase;
+import net.tapaal.gui.petrinet.verification.InclusionPlaces;
 import dk.aau.cs.Messenger;
 import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
 import dk.aau.cs.model.tapn.TAPNQuery;
@@ -32,14 +35,17 @@
 
 public class ApproximationWorker {
 	public VerificationResult<TAPNNetworkTrace> normalWorker(
-			VerificationOptions options,
-			ModelChecker modelChecker,
-			Tuple<TimedArcPetriNet, NameMapping> transformedModel,
-			ITAPNComposer composer,
-			TAPNQuery clonedQuery,
-			RunVerificationBase verificationBase,
-			TimedArcPetriNetNetwork model
-	) throws Exception {
+        VerificationOptions options,
+        ModelChecker modelChecker,
+        Tuple<TimedArcPetriNet, NameMapping> transformedModel,
+        ITAPNComposer composer,
+        TAPNQuery clonedQuery,
+        RunVerificationBase verificationBase,
+        TimedArcPetriNetNetwork model,
+        DataLayer guiModel,
+        net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery,
+        TAPNLens lens
+    ) throws Exception {
 		
 		// If options is of an instance of VerifyTAPNOptions then save the inclusion places before verify alters them
 		InclusionPlaces oldInclusionPlaces = null;
@@ -53,7 +59,9 @@
 		}
 		
 		VerificationResult<TAPNNetworkTrace> toReturn = null;
-		VerificationResult<TimedArcPetriNetTrace> result = modelChecker.verify(options, transformedModel, clonedQuery);
+		VerificationResult<TimedArcPetriNetTrace> result;
+
+		result = modelChecker.verify(options, transformedModel, clonedQuery, guiModel, dataLayerQuery, lens);
 
 		if (result.error()) {
 			options.setTraceOption(oldTraceOption);
@@ -66,14 +74,19 @@
 				// If r = 1
 				// No matter what it answered -> return that answer
 				QueryResult queryResult = result.getQueryResult();
-				toReturn =  new VerificationResult<TAPNNetworkTrace>(
-						queryResult,
-						decomposeTrace(result.getTrace(), transformedModel.value2(), model),
-						decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
-						result.verificationTime(),
-						result.stats(),
-						result.isSolvedUsingStateEquation());
-				toReturn.setNameMapping(transformedModel.value2());
+                NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                toReturn =  new VerificationResult<TAPNNetworkTrace>(
+                    queryResult,
+                    decomposeTrace(result.getTrace(),  nameMapping, netNetwork),
+                    decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
+                    result.verificationTime(),
+                    result.stats(),
+                    false,
+                    result.getUnfoldedModel());
+                toReturn.setNameMapping(transformedModel.value2());
+
+
 			} else {
 				// If r > 1
 				if (result.getTrace() != null && (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && result.getQueryResult().isQuerySatisfied())
@@ -82,14 +95,19 @@
 						// The results are inconclusive, but we get a trace and can use trace TAPN for verification.
 					
 						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
-						toReturn = new VerificationResult<TAPNNetworkTrace>(
-								approxResult.getQueryResult(),
-								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
-								approxResult.verificationTime(),
-								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation());
-						toReturn.setNameMapping(transformedModel.value2());
+                        NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                        TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                        toReturn = new VerificationResult<TAPNNetworkTrace>(
+                            approxResult.getQueryResult(),
+                            decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+                            decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
+                            approxResult.verificationTime(),
+                            approxResult.stats(),
+                            false,
+                            approxResult.getUnfoldedModel());
+                        toReturn.setNameMapping(nameMapping);
+
+
 						
 						OverApproximation overaprx = new OverApproximation();
 			
@@ -103,7 +121,7 @@
 			
 						// run model checker again for trace TAPN
 						MemoryMonitor.cumulateMemory();
-						result = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+						result = modelChecker.verify(options, transformedOriginalModel, clonedQuery, guiModel, dataLayerQuery, null);
 
 						if (result.error()) {
 							options.setTraceOption(oldTraceOption);
@@ -127,14 +145,17 @@
 						
 						// If satisfied trace -> Return result
 						// This is satisfied for EF and EG and not satisfied for AG and AF
-						toReturn = new VerificationResult<TAPNNetworkTrace>(
-								queryResult,
-								decomposeTrace(result.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
-								approxResult.verificationTime() + result.verificationTime(),
-								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation());
-						toReturn.setNameMapping(transformedModel.value2());
+                        toReturn = new VerificationResult<TAPNNetworkTrace>(
+                            queryResult,
+                            decomposeTrace(result.getTrace(), nameMapping, netNetwork),
+                            decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
+                            approxResult.verificationTime() + result.verificationTime(),
+                            approxResult.stats(),
+                            false,
+                            approxResult.getUnfoldedModel());
+                        toReturn.setNameMapping(nameMapping);
+
+
 					} 
 					else if (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && !result.getQueryResult().isQuerySatisfied())
 							|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && result.getQueryResult().isQuerySatisfied())) {
@@ -147,14 +168,19 @@
 						}
 						
 						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
-						toReturn = new VerificationResult<TAPNNetworkTrace>(
-								approxResult.getQueryResult(),
-								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
-								approxResult.verificationTime(),
-								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation());
-						toReturn.setNameMapping(transformedModel.value2());
+                    NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                    TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                        toReturn = new VerificationResult<TAPNNetworkTrace>(
+                            approxResult.getQueryResult(),
+                            decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+                            decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
+                            approxResult.verificationTime(),
+                            approxResult.stats(),
+                            false,
+                            approxResult.getUnfoldedModel());
+                        toReturn.setNameMapping(nameMapping);
+
+
 					} else {
 						// We cannot use the result directly, and did not get a trace.
 						
@@ -162,15 +188,18 @@
 						queryResult.setApproximationInconclusive(true);
 						
 						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
-						toReturn = new VerificationResult<TAPNNetworkTrace>(
-								approxResult.getQueryResult(),
-								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
-								approxResult.verificationTime(),
-								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation());
-						toReturn.setNameMapping(transformedModel.value2());
-						
+                    NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                    TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                    toReturn = new VerificationResult<TAPNNetworkTrace>(
+                        approxResult.getQueryResult(),
+                        decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+                        decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
+                        approxResult.verificationTime(),
+                        approxResult.stats(),
+                        false,
+                        approxResult.getUnfoldedModel());
+                    toReturn.setNameMapping(nameMapping);
+
 					}
 			}
 		} 
@@ -194,14 +223,19 @@
 				// If r = 1
 				// No matter it answered -> return that answer
 				QueryResult queryResult= result.getQueryResult();
-				toReturn =  new VerificationResult<TAPNNetworkTrace>(
-						queryResult,
-						decomposeTrace(result.getTrace(), transformedModel.value2(), model),
-						decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
-						result.verificationTime(),
-						result.stats(),
-						result.isSolvedUsingStateEquation());
-				toReturn.setNameMapping(transformedModel.value2());
+                NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                toReturn =  new VerificationResult<TAPNNetworkTrace>(
+                    queryResult,
+                    decomposeTrace(result.getTrace(), nameMapping, netNetwork),
+                    decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
+                    result.verificationTime(),
+                    result.stats(),
+                    false,
+                    result.getUnfoldedModel());
+                toReturn.setNameMapping(nameMapping);
+
+
 			}
 			else {
 				// If r > 1
@@ -210,14 +244,18 @@
 					// If ((EF OR EG) AND not satisfied) OR ((AG OR AF) and satisfied) -> Inconclusive
 					QueryResult queryResult= result.getQueryResult();
 					queryResult.setApproximationInconclusive(true);
-					toReturn =  new VerificationResult<TAPNNetworkTrace>(
-							queryResult,
-							decomposeTrace(result.getTrace(), transformedModel.value2(), model),
-							decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
-							result.verificationTime(),
-							result.stats(),
-							result.isSolvedUsingStateEquation());
-					toReturn.setNameMapping(transformedModel.value2());
+                    NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                    TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                    toReturn =  new VerificationResult<TAPNNetworkTrace>(
+                        queryResult,
+                        decomposeTrace(result.getTrace(), nameMapping, netNetwork),
+                        decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
+                        result.verificationTime(),
+                        result.stats(),
+                        false,
+                        result.getUnfoldedModel());
+                    toReturn.setNameMapping(nameMapping);
+
 				} else if ((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && result.getQueryResult().isQuerySatisfied()
 						|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && ! result.getQueryResult().isQuerySatisfied())) {
 										
@@ -225,14 +263,19 @@
 						// If query does have deadlock or EG or AF a trace -> create trace TAPN
 						//Create the verification satisfied result for the approximation
 						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
-						toReturn = new VerificationResult<TAPNNetworkTrace>(
-								approxResult.getQueryResult(),
-								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
-								approxResult.verificationTime(),
-								approxResult.stats(),
-								result.isSolvedUsingStateEquation());
-						toReturn.setNameMapping(transformedModel.value2());
+                        NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                        TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+                        toReturn = new VerificationResult<TAPNNetworkTrace>(
+                            approxResult.getQueryResult(),
+                            decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+                            decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
+                            approxResult.verificationTime(),
+                            approxResult.stats(),
+                            false,
+                            result.getUnfoldedModel());
+                        toReturn.setNameMapping(nameMapping);
+
+
 						
 						OverApproximation overaprx = new OverApproximation();
 						
@@ -247,7 +290,7 @@
 			
 						//run model checker again for trace TAPN
 						MemoryMonitor.cumulateMemory();
-						result = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+						result = modelChecker.verify(options, transformedOriginalModel, clonedQuery, guiModel, dataLayerQuery, null);
 
 						if (result.error()) {
 							options.setTraceOption(oldTraceOption);
@@ -271,16 +314,17 @@
 							|| (result.getQueryResult().queryType() == QueryType.AF && queryResult.isQuerySatisfied())) {
 							queryResult.setApproximationInconclusive(true);
 						}
-						
+
 						// If satisfied trace) -> Return result
 						// This is satisfied for EF and EG and not satisfied for AG and AF
 						toReturn = new VerificationResult<TAPNNetworkTrace>(
 								queryResult,
-								decomposeTrace(result.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+								decomposeTrace(result.getTrace(), nameMapping, netNetwork),
+								decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
 								approxResult.verificationTime() + result.verificationTime(),
 								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation());
+								false,
+                                approxResult.getUnfoldedModel());
 						toReturn.setNameMapping(transformedModel.value2());
 					}
 					else {
@@ -289,28 +333,36 @@
 						queryResult.setApproximationInconclusive(true);
 						
 						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
+                        NameMapping nameMapping = model.isColored()? result.getUnfoldedModel().value2(): transformedModel.value2();
+                        TimedArcPetriNetNetwork netNetwork = model.isColored()? result.getUnfoldedModel().value1().parentNetwork(): model;
+
 						toReturn = new VerificationResult<TAPNNetworkTrace>(
 								approxResult.getQueryResult(),
-								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
-								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
+								decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+								decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
 								approxResult.verificationTime(),
 								approxResult.stats(),
-								approxResult.isSolvedUsingStateEquation());
-						toReturn.setNameMapping(transformedModel.value2());
+								false,
+                                approxResult.getUnfoldedModel());
+						toReturn.setNameMapping(nameMapping);
 					}
 				}
 			}
 		} 
 		else {
+            boolean isColored = (lens != null && lens.isColored() || model.isColored());
+            NameMapping nameMapping = isColored? result.getUnfoldedModel().value2(): transformedModel.value2();
+            TimedArcPetriNetNetwork netNetwork = isColored? result.getUnfoldedModel().value1().parentNetwork(): model;
 			toReturn =  new VerificationResult<TAPNNetworkTrace>(
 					result.getQueryResult(),
-					decomposeTrace(result.getTrace(), transformedModel.value2(), model),
-					decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+					decomposeTrace(result.getTrace(), nameMapping, netNetwork),
+					decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
 					result.verificationTime(),
 					result.stats(),
-					result.isSolvedUsingStateEquation(),
-                    result.getRawOutput());
-			toReturn.setNameMapping(transformedModel.value2());
+					false,
+                    result.getRawOutput(),
+                    result.getUnfoldedModel());
+			toReturn.setNameMapping(nameMapping);
 		}
 		
 		options.setTraceOption(oldTraceOption);
@@ -326,7 +378,7 @@
 	public VerificationResult<TimedArcPetriNetTrace> batchWorker(
 			Tuple<TimedArcPetriNet, NameMapping> composedModel,
 			VerificationOptions options,
-			pipe.dataLayer.TAPNQuery query,
+			net.tapaal.gui.petrinet.verification.TAPNQuery query,
 			LoadedBatchProcessingModel model,
 			ModelChecker modelChecker,
 			TAPNQuery queryToVerify,
@@ -354,7 +406,7 @@
 			options.setTraceOption(TraceOption.SOME);
 		}
 		
-		VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify);
+		VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify, null, query, null);
 		
 		VerificationResult<TAPNNetworkTrace> valueNetwork = null;	//The final result is meant to be a PetriNetTrace but to make traceTAPN we make a networktrace
 		VerificationResult<TimedArcPetriNetTrace> value = null;
@@ -376,7 +428,8 @@
 					verificationResult.getSecondaryTrace(),
 					verificationResult.verificationTime(),
 					verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation());
+					false,
+                   verificationResult.getUnfoldedModel());
 				value.setNameMapping(composedModel.value2());
 	        } else {
 	            // If r > 1
@@ -385,14 +438,17 @@
 					// If ((EF OR EG) AND satisfied) OR ((AG OR AF) AND not satisfied)
 					//Create the verification satisfied result for the approximation
 	                VerificationResult<TimedArcPetriNetTrace> approxResult = verificationResult;
+                    NameMapping nameMapping = model.network().isColored()? verificationResult.getUnfoldedModel().value2(): composedModel.value2();
+                    TimedArcPetriNetNetwork netNetwork = model.network().isColored()? verificationResult.getUnfoldedModel().value1().parentNetwork(): model.network();
 	                valueNetwork = new VerificationResult<TAPNNetworkTrace>(
 	                            approxResult.getQueryResult(),
-	                            decomposeTrace(approxResult.getTrace(), composedModel.value2(), model.network()),
-	                            decomposeTrace(approxResult.getSecondaryTrace(), composedModel.value2(), model.network()),
+	                            decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+	                            decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
 	                            approxResult.verificationTime(),
 	                            approxResult.stats(),
-	        					verificationResult.isSolvedUsingStateEquation());
-	                valueNetwork.setNameMapping(composedModel.value2());
+	        					false,
+                                verificationResult.getUnfoldedModel());
+	                valueNetwork.setNameMapping(nameMapping);
 	                
 	                OverApproximation overaprx = new OverApproximation();
 	                
@@ -406,7 +462,7 @@
 
 	                //run model checker again for trace TAPN
 	                MemoryMonitor.cumulateMemory();
-	                verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+	                verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery, null, query, null);
 
 	                if (verificationResult.error()) {
 	                	options.setTraceOption(oldTraceOption);
@@ -432,7 +488,8 @@
 	                        approxResult.getSecondaryTrace(),
 	                        approxResult.verificationTime() + verificationResult.verificationTime(),
 	                        approxResult.stats(),
-	    					verificationResult.isSolvedUsingStateEquation());
+	    					false,
+                            verificationResult.getUnfoldedModel());
 	                value.setNameMapping(composedModel.value2());
 	            }
 				else if (((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && !verificationResult.getQueryResult().isQuerySatisfied())
@@ -451,7 +508,8 @@
 						verificationResult.getSecondaryTrace(),
 						verificationResult.verificationTime(),
 						verificationResult.stats(),
-						verificationResult.isSolvedUsingStateEquation());
+						false,
+                        verificationResult.getUnfoldedModel());
 				    value.setNameMapping(composedModel.value2());
 	            }
 				else {
@@ -467,7 +525,8 @@
 						verificationResult.getSecondaryTrace(),
 						verificationResult.verificationTime(),
 						verificationResult.stats(),
-						verificationResult.isSolvedUsingStateEquation());
+						false,
+                        verificationResult.getUnfoldedModel());
 				    value.setNameMapping(composedModel.value2());
 				}
 	        }
@@ -485,7 +544,8 @@
                     verificationResult.getSecondaryTrace(),
                     verificationResult.verificationTime(),
                     verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation());
+					false,
+                    verificationResult.getUnfoldedModel());
                 value.setNameMapping(composedModel.value2());
 	        }
 	        else {
@@ -502,7 +562,8 @@
                             verificationResult.getSecondaryTrace(),
                             verificationResult.verificationTime(),
                             verificationResult.stats(),
-        					verificationResult.isSolvedUsingStateEquation());
+        					false,
+                            verificationResult.getUnfoldedModel());
                     value.setNameMapping(composedModel.value2());
 	                    
 				}
@@ -514,14 +575,20 @@
 	                    // If query does have deadlock -> create trace TAPN
 	                    //Create the verification satisfied result for the approximation
 						VerificationResult<TimedArcPetriNetTrace> approxResult = verificationResult;
-	                    valueNetwork = new VerificationResult<TAPNNetworkTrace>(
-	                    		approxResult.getQueryResult(),
-	                        decomposeTrace(approxResult.getTrace(), composedModel.value2(), model.network()),
-	                        decomposeTrace(approxResult.getSecondaryTrace(), composedModel.value2(), model.network()),
-	                        approxResult.verificationTime(),
-	                        approxResult.stats(),
-	                        approxResult.isSolvedUsingStateEquation());
-	                    valueNetwork.setNameMapping(composedModel.value2());
+
+                        NameMapping nameMapping = model.network().isColored()? verificationResult.getUnfoldedModel().value2(): composedModel.value2();
+                        TimedArcPetriNetNetwork netNetwork = model.network().isColored()? verificationResult.getUnfoldedModel().value1().parentNetwork(): model.network();
+                        valueNetwork = new VerificationResult<TAPNNetworkTrace>(
+                            approxResult.getQueryResult(),
+                            decomposeTrace(approxResult.getTrace(), nameMapping, netNetwork),
+                            decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
+                            approxResult.verificationTime(),
+                            approxResult.stats(),
+                            false,
+                            verificationResult.getUnfoldedModel());
+                        valueNetwork.setNameMapping(nameMapping);
+
+
 	                    
 	                    OverApproximation overaprx = new OverApproximation();
 	        
@@ -534,7 +601,7 @@
 	        
 	                    //run model checker again for trace TAPN
 	                    MemoryMonitor.cumulateMemory();
-	                    verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+	                    verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery, null, query, null);
 
 	                    if (verificationResult.error()) {
 	                    	options.setTraceOption(oldTraceOption);
@@ -564,7 +631,8 @@
 	                            verificationResult.getSecondaryTrace(),
 	                            verificationResult.verificationTime() + approxResult.verificationTime(),
 	                            verificationResult.stats(),
-	        					verificationResult.isSolvedUsingStateEquation());
+	        					false,
+                                verificationResult.getUnfoldedModel());
 	                    value.setNameMapping(composedModel.value2());
 	                }
 	                else {
@@ -578,7 +646,8 @@
 							verificationResult.getSecondaryTrace(),
 							verificationResult.verificationTime(),
 							verificationResult.stats(),
-							verificationResult.isSolvedUsingStateEquation());
+							false,
+                            verificationResult.getUnfoldedModel());
 					    value.setNameMapping(composedModel.value2());
 	                }
 	            }
@@ -591,7 +660,8 @@
 	                verificationResult.getSecondaryTrace(),
 	                verificationResult.verificationTime(),
 	                verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation());
+					false,
+                    verificationResult.getUnfoldedModel());
 	        value.setNameMapping(composedModel.value2());
 	    }
 		

=== modified file 'src/dk/aau/cs/approximation/OverApproximation.java'
--- src/dk/aau/cs/approximation/OverApproximation.java	2020-07-20 12:17:24 +0000
+++ src/dk/aau/cs/approximation/OverApproximation.java	2022-03-21 20:20:44 +0000
@@ -13,6 +13,7 @@
 import dk.aau.cs.TCTL.TCTLNotNode;
 import dk.aau.cs.TCTL.TCTLOrListNode;
 import dk.aau.cs.TCTL.TCTLPlaceNode;
+import dk.aau.cs.model.CPN.ColorType;
 import dk.aau.cs.model.tapn.*;
 import dk.aau.cs.model.tapn.simulation.*;
 import dk.aau.cs.util.Tuple;
@@ -69,18 +70,18 @@
 			 oldInterval.isUpperBoundNonStrict()
 			 );
 	}
-	
+
 	public void makeTraceTAPN(Tuple<TimedArcPetriNet, NameMapping> transformedModel, VerificationResult<TAPNNetworkTrace> result, dk.aau.cs.model.tapn.TAPNQuery query) {
 		TimedArcPetriNet net = transformedModel.value1();
                 
 		LocalTimedPlace currentPlace = new LocalTimedPlace("PTRACE0");
-		TimedToken currentToken = new TimedToken(currentPlace);
+		TimedToken currentToken = new TimedToken(currentPlace, ColorType.COLORTYPE_DOT.getFirstColor());
 		net.add(currentPlace);
 		currentPlace.addToken(currentToken);
 		
 		// Block place, which secures the net makes at most one transition not in the trace.
-		LocalTimedPlace blockPlace = new LocalTimedPlace("PBLOCK", TimeInvariant.LESS_THAN_INFINITY);
-		TimedToken blockToken = new TimedToken(blockPlace);
+		LocalTimedPlace blockPlace = new LocalTimedPlace("PBLOCK");
+		TimedToken blockToken = new TimedToken(blockPlace, ColorType.COLORTYPE_DOT.getFirstColor());
 		net.add(blockPlace);
 		blockPlace.addToken(blockToken);
 		
@@ -140,7 +141,7 @@
 						(((TAPNNetworkTimedTransitionStep) step).getTransition().sharedTransition() == null ? tmpStep.getTransition().model().name() : ""), 
 						tmpStep.getTransition().name()); 
 				TimedTransition firedTransition = net.getTransitionByName(nameMap.get(key));
-				TimedTransition copyTransition = new TimedTransition(firedTransition.name() + "_traceNet_" + Integer.toString(++transitionInteger), firedTransition.isUrgent());
+				TimedTransition copyTransition = new TimedTransition(firedTransition.name() + "_traceNet_" + Integer.toString(++transitionInteger), firedTransition.isUrgent(), null);
 				
 				net.add(copyTransition);
 				net.add(new TimedInputArc(currentPlace, copyTransition, TimeInterval.ZERO_INF));
@@ -163,17 +164,17 @@
 				
 				for (TimedInputArc arc : originalInput) {
 					if (arc.destination() == firedTransition) {
-						net.add(new TimedInputArc(arc.source(), copyTransition, arc.interval(), arc.getWeight()));
+						net.add(new TimedInputArc(arc.source(), copyTransition, arc.interval(), arc.getWeight(), arc.getArcExpression()));
 					}
 				}
 				for (TimedOutputArc arc : originalOutput) {
 					if (arc.source() == firedTransition) {
-						net.add(new TimedOutputArc(copyTransition, arc.destination(), arc.getWeight()));
+						net.add(new TimedOutputArc(copyTransition, arc.destination(), arc.getWeight(), arc.getExpression()));
 					}
 				}
 				for (TimedInhibitorArc arc : originalInhibitor) {
 					if (arc.destination() == firedTransition) {
-						net.add(new TimedInhibitorArc(arc.source(), copyTransition, arc.interval(), arc.getWeight()));
+						net.add(new TimedInhibitorArc(arc.source(), copyTransition, arc.interval(), arc.getWeight(), arc.getArcExpression()));
 					}
 				}
 				for (TransportArc arc : originalTransport) {
@@ -200,7 +201,7 @@
 		
 		// An input arc from pBlock to all original transitions makes sure, that we can do deadlock checks.
 		for (TimedTransition transition : originalTransitions) {
-			net.add(new TimedInputArc(blockPlace, transition, TimeInterval.ZERO_INF));	
+			net.add(new TimedInputArc(blockPlace, transition, TimeInterval.ZERO_INF));
 		}           
 	}
 

=== modified file 'src/dk/aau/cs/approximation/UnderApproximation.java'
--- src/dk/aau/cs/approximation/UnderApproximation.java	2020-07-20 12:17:24 +0000
+++ src/dk/aau/cs/approximation/UnderApproximation.java	2022-03-21 20:20:44 +0000
@@ -1,23 +1,13 @@
 package dk.aau.cs.approximation;
 
+import dk.aau.cs.model.tapn.*;
+import pipe.gui.petrinet.dataLayer.DataLayer;
+import pipe.gui.petrinet.graphicElements.Arc;
+import pipe.gui.petrinet.graphicElements.Place;
+import pipe.gui.petrinet.graphicElements.Transition;
+
 import java.util.ArrayList;
 
-import dk.aau.cs.model.tapn.Bound;
-import dk.aau.cs.model.tapn.IntBound;
-import dk.aau.cs.model.tapn.TimeInterval;
-import dk.aau.cs.model.tapn.TimeInvariant;
-import dk.aau.cs.model.tapn.TimedArcPetriNet;
-import dk.aau.cs.model.tapn.TimedInhibitorArc;
-import dk.aau.cs.model.tapn.TimedInputArc;
-import dk.aau.cs.model.tapn.TimedOutputArc;
-import dk.aau.cs.model.tapn.TimedPlace;
-import dk.aau.cs.model.tapn.TimedTransition;
-import dk.aau.cs.model.tapn.TransportArc;
-import pipe.dataLayer.DataLayer;
-import pipe.gui.graphicElements.Arc;
-import pipe.gui.graphicElements.Place;
-import pipe.gui.graphicElements.Transition;
-
 public class UnderApproximation implements ITAPNApproximation {
 	@Override
 	public void modifyTAPN(TimedArcPetriNet net, int approximationDenominator) {
@@ -141,44 +131,42 @@
 	}
 	
 	//Returns a copy of an approximated interval
-	private TimeInterval modifyIntervals(TimeInterval oldInterval, int denominator){
-		Bound newUpperBound;
-		// Do not calculate upper bound for infinite
-		if ( ! (oldInterval.upperBound() instanceof Bound.InfBound)) {
-			
-			 // Calculate the new upper bound value.
-			int oldUpperBoundValue = oldInterval.upperBound().value();
-			newUpperBound = new IntBound((int) Math.floor((double)oldUpperBoundValue /  denominator));
-		}
-		else
-			newUpperBound = Bound.Infinity;
-		 
-		// Calculate the new lower bound
-		IntBound newLowerBound = new IntBound((int) Math.ceil((double)oldInterval.lowerBound().value() / denominator));
-		 
-		// if the lower bound has become greater than the upper bound by rounding
-				if ( ! (oldInterval.upperBound() instanceof Bound.InfBound) && newLowerBound.value() > newUpperBound.value())
-				{
-					newLowerBound = new IntBound((int) Math.floor((double)oldInterval.lowerBound().value() / denominator));
-					newUpperBound = new IntBound((int) Math.floor((double)oldInterval.upperBound().value() / denominator));
-				}
-				
-				boolean isLowerBoundNonStrict = oldInterval.isLowerBoundNonStrict();
-				boolean isUpperBoundNonStrict = oldInterval.isUpperBoundNonStrict();
-				
-				// if the interval becomes too small we make it a bit bigger to secure, that we do not have to delete the arc
-				if ( (newUpperBound.value() == newLowerBound.value()) && !(oldInterval.isLowerBoundNonStrict() && oldInterval.isUpperBoundNonStrict()))
-				{
-					isUpperBoundNonStrict = true;
-					isLowerBoundNonStrict = true;
-				}
-
-				return new TimeInterval(
-					 isLowerBoundNonStrict,
-					 newLowerBound,
-					 newUpperBound,
-					 isUpperBoundNonStrict
-					 );
-	}
+    private TimeInterval modifyIntervals(TimeInterval oldInterval, int denominator) {
+        Bound newUpperBound;
+        // Do not calculate upper bound for infinite
+        if (!(oldInterval.upperBound() instanceof Bound.InfBound)) {
+
+            // Calculate the new upper bound value.
+            int oldUpperBoundValue = oldInterval.upperBound().value();
+            newUpperBound = new IntBound((int) Math.floor((double) oldUpperBoundValue / denominator));
+        } else {
+            newUpperBound = Bound.Infinity;
+        }
+
+        // Calculate the new lower bound
+        IntBound newLowerBound = new IntBound((int) Math.ceil((double) oldInterval.lowerBound().value() / denominator));
+
+        // if the lower bound has become greater than the upper bound by rounding
+        if (!(oldInterval.upperBound() instanceof Bound.InfBound) && newLowerBound.value() > newUpperBound.value()) {
+            newLowerBound = new IntBound((int) Math.floor((double) oldInterval.lowerBound().value() / denominator));
+            newUpperBound = new IntBound((int) Math.floor((double) oldInterval.upperBound().value() / denominator));
+        }
+
+        boolean isLowerBoundNonStrict = oldInterval.isLowerBoundNonStrict();
+        boolean isUpperBoundNonStrict = oldInterval.isUpperBoundNonStrict();
+
+        // if the interval becomes too small we make it a bit bigger to secure, that we do not have to delete the arc
+        if ((newUpperBound.value() == newLowerBound.value()) && !(oldInterval.isLowerBoundNonStrict() && oldInterval.isUpperBoundNonStrict())) {
+            isUpperBoundNonStrict = true;
+            isLowerBoundNonStrict = true;
+        }
+
+        return new TimeInterval(
+            isLowerBoundNonStrict,
+            newLowerBound,
+            newUpperBound,
+            isUpperBoundNonStrict
+        );
+    }
 
 }

=== removed directory 'src/dk/aau/cs/gui'
=== removed directory 'src/dk/aau/cs/gui/components'
=== removed directory 'src/dk/aau/cs/gui/components/handlers'
=== removed directory 'src/dk/aau/cs/gui/smartDraw'
=== removed directory 'src/dk/aau/cs/gui/undo'
=== added file 'src/dk/aau/cs/io/LoadTACPN.java'
--- src/dk/aau/cs/io/LoadTACPN.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/io/LoadTACPN.java	2022-03-21 20:20:44 +0000
@@ -0,0 +1,439 @@
+package dk.aau.cs.io;
+
+import dk.aau.cs.model.CPN.*;
+import dk.aau.cs.model.CPN.Expressions.*;
+import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
+import dk.aau.cs.util.FormatException;
+import dk.aau.cs.util.Require;
+import dk.aau.cs.util.Tuple;
+import org.w3c.dom.Element;
+import org.w3c.dom.Node;
+
+import java.util.*;
+
+public class LoadTACPN { //the import feature for CPN and load for TACPN share similarities. These similarities are shared here. Feel free to find a better name for this class
+
+    private final HashMap<String, ColorType> colortypes = new HashMap<>();
+    private final HashMap<String, Variable> variables = new HashMap<>();
+    private final HashMap<String, ColorExpression> tupleVarExpressions = new HashMap<>();
+    private final Collection<String> messages = new ArrayList<>(10);
+
+    public HashMap<String, ColorType> getColortypes() {
+        return colortypes;
+    }
+
+    public HashMap<String, Variable> getVariables() {
+        return variables;
+    }
+
+    public Collection<String> getMessages() {return  messages;}
+    //skipWS
+    //  Takes a given node and returns it if it is an element,
+    //  otherwise returns its first element sibling.
+    //  This allows skipping past whitespace nodes.
+    private static Node skipWS(Node node) {
+        if (node != null && !(node instanceof Element)) {
+            return skipWS(node.getNextSibling());
+        } else {
+            return node;
+        }
+    }
+
+    private static Node getAttribute(Node node, String attribute) {
+        return node.getAttributes().getNamedItem(attribute);
+    }
+
+    public void parseDeclarations(Node node, TimedArcPetriNetNetwork network) throws FormatException {
+        if(!(node instanceof Element)){
+            return;
+        }
+        Node child = skipWS(node.getFirstChild());
+        while(child != null){
+            String childName = child.getNodeName();
+            if (childName.equals("namedsort")){
+                parseNamedSort(child, network);
+            } else if (childName.equals("variabledecl")){
+                String id = getAttribute(child, "id").getNodeValue();
+                String name = getAttribute(child, "name").getNodeValue();
+                ColorType ct = parseUserSort(child);
+                Variable var = new Variable(name, id, ct);
+                Require.that(variables.put(id, var) == null, "the id " + id + ", was already used");
+                network.add(var);
+            } else {
+                parseDeclarations(child, network);
+            }
+
+            child = skipWS(child.getNextSibling());
+        }
+        Vector<String> variablesForRemoval = new Vector<>();
+        HashMap<String, Variable> newVars = new HashMap<>();
+        StringBuilder renameWarnings = new StringBuilder();
+        // Convert product variables into variables for the constituent of the product
+        for(String varName : variables.keySet()){
+            Variable var = variables.get(varName);
+            if(var.getColorType().isProductColorType()){
+                int constituentCounter = 1;
+
+                Vector<ColorExpression> constituentVarExpressions = new Vector<>();
+                renameWarnings.append("The product variable ").append(var.getName()).append(", was unfolded to (");
+
+                for(ColorType colorType : var.getColorType().getProductColorTypes()){
+                    StringBuilder elementSubstring = new StringBuilder("_" + constituentCounter);
+                    while (variables.containsKey(varName + elementSubstring) || newVars.containsKey(varName + elementSubstring)){
+                        elementSubstring.append("_1");
+                    }
+
+                    renameWarnings.append(varName).append(elementSubstring).append(",");
+
+                    Variable newVar = new Variable(var.getName() + elementSubstring, varName + elementSubstring, colorType);
+                    Require.that(newVars.put(varName + elementSubstring, newVar) == null, "the id " + varName + elementSubstring + ", was already used");
+                    network.add(newVar);
+                    constituentVarExpressions.addElement(new VariableExpression(newVar));
+                    constituentCounter++;
+                }
+                renameWarnings.deleteCharAt(renameWarnings.length()-1);
+                renameWarnings.append(")\n");
+
+                tupleVarExpressions.put(varName, new TupleExpression(constituentVarExpressions));
+                network.remove(var);
+                variablesForRemoval.addElement(varName);
+            }
+        }
+        for(String varName : variablesForRemoval){
+            variables.remove(varName);
+        }
+        for(String varName : newVars.keySet()){
+            variables.put(varName, newVars.get(varName));
+        }
+
+        if(renameWarnings.length() > 0){
+            messages.add(renameWarnings.toString());
+            //JOptionPane.showConfirmDialog(CreateGui.getApp(), renameWarnings.toString(), "Product Variables unfolded", JOptionPane.OK_OPTION, JOptionPane.WARNING_MESSAGE);
+        }
+    }
+    private void parseNamedSort(Node node, TimedArcPetriNetNetwork network) throws FormatException {
+        //We always use the dot colortype
+        colortypes.put("dot", ColorType.COLORTYPE_DOT);
+        network.add(ColorType.COLORTYPE_DOT);
+
+        Node type = skipWS(node.getFirstChild());
+        String typetag = type.getNodeName();
+        String name = getAttribute(node, "name").getNodeValue();
+        String id = getAttribute(node, "id").getNodeValue();
+
+        if (typetag.equals("productsort")) {
+            ProductType pt = new ProductType(name);
+            Node typechild = skipWS(type.getFirstChild());
+            while (typechild != null) {
+                if (typechild.getNodeName().equals("usersort")) {
+                    String constituent = getAttribute(typechild, "declaration").getNodeValue();
+                    pt.addType(colortypes.get(constituent));
+                }
+                typechild = skipWS(typechild.getNextSibling());
+            }
+            Require.that(colortypes.put(id, pt) == null, "the name " + id + ", was already used");
+            network.add(pt);
+        } else {
+            ColorType ct = new ColorType(name, id);
+            if (typetag.equals("dot")) {
+                return;
+            } else if (typetag.equals("finiteintrange")){
+                int start = Integer.parseInt(getAttribute(type, "start").getNodeValue());
+                int end = Integer.parseInt(getAttribute(type, "end").getNodeValue());
+                for(int i = start; i <= end; i++){
+                    ct.addColor(String.valueOf(i));
+                }
+            } else {
+                Node typechild = skipWS(type.getFirstChild());
+                while (typechild != null) {
+                    Node colorId = getAttribute(typechild, "id");
+                    if (colorId != null) {
+                        ct.addColor(colorId.getNodeValue());
+                        typechild = skipWS(typechild.getNextSibling());
+                    } else {
+                        throw new FormatException(String.format("No id found on %s\n", typechild.getNodeName()));
+                    }
+                }
+            }
+            Require.that(colortypes.put(id, ct) == null, "the name " + id + ", was already used");
+            network.add(ct);
+        }
+    }
+
+    public ColorType parseUserSort(Node node) throws FormatException {
+        if (node instanceof Element) {
+            Node child = skipWS(node.getFirstChild());
+            while (child != null) {
+                String name = child.getNodeName();
+                if (name.equals("usersort")) {
+                    Node decl = getAttribute(child, "declaration");
+                    return colortypes.get(decl.getNodeValue());
+                } else if (name.matches("structure|type|subterm")) {
+                    return parseUserSort(child);
+                }
+                child = skipWS(child.getNextSibling());
+            }
+        }
+        throw new FormatException(String.format("Could not parse %s as an usersort\n", node.getNodeName()));
+    }
+
+    public ArcExpression parseArcExpression(Node node) throws FormatException {
+        String name = node.getNodeName();
+        if (name.equals("numberof")) {
+            return parseNumberOfExpression(node);
+        } else if (name.equals("add")) {
+            Vector<ArcExpression> constituents = new Vector<>();
+
+            Node child = skipWS(node.getFirstChild());
+            while (child != null) {
+                ArcExpression subterm = parseArcExpression(child);
+                constituents.add(subterm);
+                child = skipWS(child.getNextSibling());
+            }
+            return new AddExpression(constituents);
+        } else if (name.equals("subtract")) {
+            Node headchild = skipWS(node.getFirstChild());
+            ArcExpression headexp = parseArcExpression(headchild);
+
+            Node nextchild = skipWS(headchild.getNextSibling());
+            while (nextchild != null) {
+                ArcExpression nextexp = parseArcExpression(nextchild);
+                headexp = new SubtractExpression(headexp, nextexp);
+                nextchild = skipWS(nextchild.getNextSibling());
+            }
+            return headexp;
+        } else if (name.equals("scalarproduct")) {
+            Node scalar = skipWS(node.getFirstChild());
+            Integer scalarval = parseNumberConstantExpression(scalar);
+
+            Node child = skipWS(scalar.getNextSibling());
+            ArcExpression childexp = parseArcExpression(child);
+
+            return new ScalarProductExpression(scalarval, childexp);
+        }else if (name.equals("all")){
+            ColorType ct = parseUserSort(node);
+            Vector<ColorExpression> ceVector = new Vector<>();
+            ceVector.add(new AllExpression(ct));
+            return new NumberOfExpression(1,ceVector);
+
+        } else if (name.matches("subterm|structure")) {
+            Node child = skipWS(node.getFirstChild());
+            return parseArcExpression(child);
+        } else if (name.matches("tuple")){
+            Vector<ColorExpression> ceVector = new Vector<>();
+            ceVector.add(parseColorExpression(node));
+            return new NumberOfExpression(1, ceVector);
+        } else{
+            throw new FormatException(String.format("Could not parse %s as an arc expression\n", name));
+        }
+    }
+
+    private NumberOfExpression parseNumberOfExpression(Node node) throws FormatException {
+        Node number = skipWS(node.getFirstChild());
+        //The number constant may be omitted.
+        //In that case, this parsing returns null.
+        Integer numberval = parseNumberConstantExpression(number);
+        Node subnode;
+        if (numberval != null) {
+            //The subexpression comes after the number constant.
+            subnode = skipWS(number.getNextSibling());
+        } else {
+            //The number we read was actually the subexpression.
+            subnode = number;
+            numberval = 1;
+        }
+        Vector<ColorExpression> colorexps = new Vector<>();
+        while (subnode != null) {
+            ColorExpression colorexp = parseColorExpression(subnode);
+            colorexps.add(colorexp);
+            subnode = skipWS(subnode.getNextSibling());
+        }
+        return new NumberOfExpression(numberval, colorexps);
+
+    }
+
+    private Integer parseNumberConstantExpression(Node node) {
+        String name = node.getNodeName();
+        if (name.equals("numberconstant")) {
+            String value = getAttribute(node, "value").getNodeValue();
+            return Integer.valueOf(value);
+        } else if (name.equals("subterm")) {
+            Node child = skipWS(node.getFirstChild());
+            return parseNumberConstantExpression(child);
+        } else {
+            return null;
+        }
+    }
+
+    private ColorExpression parseColorExpression(Node node) throws FormatException {
+        String name = node.getNodeName();
+        if (name.equals("dotconstant")) {
+            return new DotConstantExpression();
+        } else if (name.equals("variable")) {
+            String varname = getAttribute(node, "refvariable").getNodeValue();
+            Variable var = variables.get(varname);
+            if(var != null){
+                return new VariableExpression(var);
+            } else {
+                return tupleVarExpressions.get(varname);
+            }
+        } else if (name.equals("useroperator")) {
+            String colorname = getAttribute(node, "declaration").getNodeValue();
+            Color color = getColor(colorname);
+            return new UserOperatorExpression(color);
+        } else if (name.equals("successor")) {
+            Node child = skipWS(node.getFirstChild());
+            ColorExpression childexp = parseColorExpression(child);
+            return new SuccessorExpression(childexp);
+        } else if (name.equals("predecessor")) {
+            Node child = skipWS(node.getFirstChild());
+            ColorExpression childexp = parseColorExpression(child);
+            return new PredecessorExpression(childexp);
+        } else if(name.equals("all")){
+            ColorType ct = parseUserSort(node);
+            return new AllExpression(ct);
+        } else if (name.equals("tuple")) {
+            Vector<ColorExpression> colorexps = new Vector<>();
+
+            Node child = skipWS(node.getFirstChild());
+            while (child != null) {
+                ColorExpression colorexp = parseColorExpression(child);
+                colorexps.add(colorexp);
+                child = skipWS(child.getNextSibling());
+            }
+            //Sometimes PNML nets have tuples with only 1 color, we just remove the tuple
+            if(colorexps.size() < 2){
+                return colorexps.get(0);
+            }
+            return new TupleExpression(colorexps);
+        } else if (name.matches("subterm|structure")) {
+            Node child = skipWS(node.getFirstChild());
+            return parseColorExpression(child);
+        } else if (name.equals("finiteintrangeconstant")){
+            String value = getAttribute(node, "value").getNodeValue();
+            //we assume first child is finiteintrange
+            Node intRangeElement = skipWS(node.getFirstChild());
+            String start = getAttribute(intRangeElement, "start").getNodeValue();
+            String end = getAttribute(intRangeElement, "end").getNodeValue();
+            return new UserOperatorExpression(findColorForIntRange(value,start,end));
+
+        } else {
+            throw new FormatException(String.format("Could not parse %s as an color expression\n", name));
+        }
+    }
+
+    /// This will select the wrong color if the is overlap in naming, eg for IntegerRangeExpr (1,2,3,4) & (1,2)
+    private dk.aau.cs.model.CPN.Color getColor(String colorname) throws FormatException {
+        for (ColorType ct : colortypes.values()) {
+            for (dk.aau.cs.model.CPN.Color c : ct) {
+                if (c.getName().equals(colorname)) {
+                    return c;
+                }
+            }
+        }
+        throw new FormatException(String.format("The color \"%s\" was not declared\n", colorname));
+    }
+
+    public GuardExpression parseGuardExpression(Node node) throws FormatException {
+        String name = node.getNodeName();
+        if (name.matches("lt|lessthan")) {
+            Tuple<ColorExpression, ColorExpression> subexps = parseLRColorExpressions(node);
+            return new LessThanExpression(subexps.value1(), subexps.value2());
+        } else if (name.matches("gt|greaterthan")) {
+            Tuple<ColorExpression, ColorExpression> subexps = parseLRColorExpressions(node);
+            return new GreaterThanExpression(subexps.value1(), subexps.value2());
+        } else if (name.matches("leq|lessthanorequal")) {
+            Tuple<ColorExpression, ColorExpression> subexps = parseLRColorExpressions(node);
+            return new LessThanEqExpression(subexps.value1(), subexps.value2());
+        } else if (name.matches("geq|greaterthanorequal")) {
+            Tuple<ColorExpression, ColorExpression> subexps = parseLRColorExpressions(node);
+            return new GreaterThanEqExpression(subexps.value1(), subexps.value2());
+        } else if (name.matches("eq|equality")) {
+            Tuple<ColorExpression, ColorExpression> subexps = parseLRColorExpressions(node);
+            return new EqualityExpression(subexps.value1(), subexps.value2());
+        } else if (name.matches("neq|inequality")) {
+            Tuple<ColorExpression, ColorExpression> subexps = parseLRColorExpressions(node);
+            return new InequalityExpression(subexps.value1(), subexps.value2());
+        } else if (name.equals("not")) {
+            Node child = skipWS(node.getFirstChild());
+            GuardExpression childexp = parseGuardExpression(child);
+            return new NotExpression(childexp);
+        } else if (name.equals("and")) {
+            Tuple<GuardExpression, GuardExpression> subexps = parseLRGuardExpressions(node);
+            return new AndExpression(subexps.value1(), subexps.value2());
+        } else if (name.equals("or")) {
+            Node left = skipWS(node.getFirstChild());
+            Node right = skipWS(left.getNextSibling());
+            if(right == null){
+                return parseGuardExpression(left);
+            }
+            GuardExpression parentOr = new OrExpression(parseGuardExpression(left), parseGuardExpression(right));
+            for (var it = skipWS(right.getNextSibling()); it != null; it = skipWS(it.getNextSibling())){
+                parentOr = new OrExpression(parentOr, parseGuardExpression(it));
+            }
+            return parentOr;
+        } else if (name.matches("subterm|structure")) {
+            Node child = skipWS(node.getFirstChild());
+            return parseGuardExpression(child);
+        } else {
+            throw new FormatException(String.format("Could not parse %s as a guard expression\n", name));
+        }
+    }
+
+    private Tuple<ColorExpression,ColorExpression> parseLRColorExpressions(Node node) throws FormatException {
+        Node left = skipWS(node.getFirstChild());
+        ColorExpression leftexp = parseColorExpression(left);
+        Node right = skipWS(left.getNextSibling());
+        ColorExpression rightexp = parseColorExpression(right);
+        return new Tuple<>(leftexp, rightexp);
+    }
+
+    private Tuple<GuardExpression,GuardExpression> parseLRGuardExpressions(Node node) throws FormatException {
+        Node left = skipWS(node.getFirstChild());
+        GuardExpression leftexp = parseGuardExpression(left);
+        Node right = skipWS(left.getNextSibling());
+        GuardExpression rightexp = parseGuardExpression(right);
+        return new Tuple<>(leftexp, rightexp);
+    }
+
+    Color findColorForIntRange(String value, String start, String end) throws FormatException {
+        for(var ct : colortypes.values()){
+            if(ct.getColors().get(0).getColorName().equals(start) && ct.getColors().get(ct.getColors().size()-1).getColorName().equals(end)){
+                for (dk.aau.cs.model.CPN.Color c : ct) {
+                    if (c.getName().equals(value)) {
+                        return c;
+                    }
+                }
+            }
+        }
+        throw new FormatException(String.format("The color \"%s\" was not declared in an int range\n", value));
+    }
+
+    public AddExpression constructCleanAddExpression(ColorType ct, ColorMultiset multiset){
+        Vector<ArcExpression> coloredTokenList = new Vector<>();
+
+        for(Color c : ct.getColors()){
+            int numberOf = multiset.get(c);
+            if(numberOf < 1){
+                continue;
+            }
+            Vector<ColorExpression> v = new Vector<>();
+            if(ct.isProductColorType()){
+                Vector<ColorExpression> tupleColors = new Vector<>();
+                for(Color tupleCol : c.getTuple()){
+                    UserOperatorExpression color = new UserOperatorExpression(tupleCol);
+                    tupleColors.add(color);
+                }
+                TupleExpression tupleExpr = new TupleExpression(tupleColors);
+                v.add(tupleExpr);
+            } else {
+                UserOperatorExpression color = new UserOperatorExpression(c);
+                v.add(color);
+            }
+            NumberOfExpression numOf = new NumberOfExpression(numberOf,v);
+            coloredTokenList.add(numOf);
+
+        }
+        return new AddExpression(coloredTokenList);
+    }
+}

=== modified file 'src/dk/aau/cs/io/LoadedModel.java'
--- src/dk/aau/cs/io/LoadedModel.java	2020-08-26 12:29:25 +0000
+++ src/dk/aau/cs/io/LoadedModel.java	2022-03-21 20:20:44 +0000
@@ -1,12 +1,11 @@
 package dk.aau.cs.io;
 
 import java.util.Collection;
-import java.util.List;
 
-import dk.aau.cs.gui.TabContent;
+import net.tapaal.gui.petrinet.TAPNLens;
 import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
-import pipe.dataLayer.TAPNQuery;
-import pipe.dataLayer.Template;
+import net.tapaal.gui.petrinet.verification.TAPNQuery;
+import net.tapaal.gui.petrinet.Template;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 
 public class LoadedModel implements LoadedBatchProcessingModel {
@@ -15,9 +14,9 @@
 	private final Collection<TAPNQuery> queries;
 	private final TimedArcPetriNetNetwork network;
     private final Collection<String> messages;
-    private final TabContent.TAPNLens lens;
+    private final TAPNLens lens;
 
-    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, TAPNLens lens){
         this.templates = templates;
         this.network = network;
         this.queries = queries;
@@ -30,15 +29,18 @@
 	public TimedArcPetriNetNetwork network(){ return network; }
     public Collection<String> getMessages() { return messages; }
 
-    public TabContent.TAPNLens getLens(){
+    public TAPNLens getLens(){
         if (lens != null) {
             return lens;
         } else {
             boolean isNetTimed = !network().isUntimed();
             boolean isNetGame = network().hasUncontrollableTransitions();
+            boolean isNetColored = network.isColored();
 
-            return new TabContent.TAPNLens(isNetTimed, isNetGame);
+            return new TAPNLens(isNetTimed, isNetGame, isNetColored);
         }
     }
-
+    public boolean isColored(){
+	    return lens.isColored();
+    }
 }
\ No newline at end of file

=== modified file 'src/dk/aau/cs/io/LoadedQueries.java'
--- src/dk/aau/cs/io/LoadedQueries.java	2020-10-09 07:59:49 +0000
+++ src/dk/aau/cs/io/LoadedQueries.java	2022-03-21 20:20:44 +0000
@@ -1,6 +1,5 @@
 package dk.aau.cs.io;
-import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
-import pipe.dataLayer.TAPNQuery;
+import net.tapaal.gui.petrinet.verification.TAPNQuery;
 import java.util.Collection;
 
 public class LoadedQueries {

=== modified file 'src/dk/aau/cs/io/ModelLoader.java'
--- src/dk/aau/cs/io/ModelLoader.java	2021-08-10 11:37:11 +0000
+++ src/dk/aau/cs/io/ModelLoader.java	2022-03-21 20:20:44 +0000
@@ -7,7 +7,7 @@
 import java.io.InputStream;
 
 import dk.aau.cs.TCTL.Parsing.ParseException;
-import dk.aau.cs.gui.TabContent;
+import net.tapaal.gui.petrinet.TAPNLens;
 
 public class ModelLoader {
 
@@ -52,12 +52,12 @@
                 return oldFormatLoader.load(new ByteArrayInputStream(baos.toByteArray()));
 
             } catch(Throwable e2) {
-				throw new ParseException(e1.getMessage());
+				throw new Exception(e1.getMessage(), e1);
 			}
 		}
 	}
 
-    public TabContent.TAPNLens loadLens(InputStream file) throws Exception{
+    public TAPNLens loadLens(InputStream file) throws Exception{
         TapnXmlLoader newFormatLoader = new TapnXmlLoader();
         ByteArrayOutputStream baos = new ByteArrayOutputStream();
         byte[] buffer = new byte[1024];

=== renamed file 'src/pipe/dataLayer/NetWriter.java' => 'src/dk/aau/cs/io/NetWriter.java'
--- src/pipe/dataLayer/NetWriter.java	2014-05-22 21:26:05 +0000
+++ src/dk/aau/cs/io/NetWriter.java	2022-03-21 20:20:44 +0000
@@ -1,4 +1,4 @@
-package pipe.dataLayer;
+package dk.aau.cs.io;
 
 import java.io.ByteArrayOutputStream;
 import java.io.File;
@@ -12,7 +12,7 @@
 public interface NetWriter {
 	void savePNML(File file) throws NullPointerException, IOException,
 			ParserConfigurationException, DOMException,
-			TransformerConfigurationException, TransformerException;
+        TransformerException;
 
-	ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException;
+	ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerException;
 }

=== modified file 'src/dk/aau/cs/io/PNMLWriter.java'
--- src/dk/aau/cs/io/PNMLWriter.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/io/PNMLWriter.java	2022-03-21 20:20:44 +0000
@@ -17,20 +17,20 @@
 import javax.xml.transform.dom.DOMSource;
 import javax.xml.transform.stream.StreamResult;
 
+import net.tapaal.gui.petrinet.TAPNLens;
 import org.w3c.dom.DOMException;
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
 
-import pipe.dataLayer.DataLayer;
-import pipe.dataLayer.NetWriter;
+import pipe.gui.petrinet.dataLayer.DataLayer;
 import pipe.gui.MessengerImpl;
-import pipe.gui.graphicElements.Arc;
-import pipe.gui.graphicElements.Place;
-import pipe.gui.graphicElements.Transition;
-import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
-import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
-import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
+import pipe.gui.petrinet.graphicElements.Arc;
+import pipe.gui.petrinet.graphicElements.Place;
+import pipe.gui.petrinet.graphicElements.Transition;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedOutputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedTransitionComponent;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 import dk.aau.cs.util.Require;
@@ -41,19 +41,21 @@
 	private final TimedArcPetriNetNetwork network;
 	private TimedArcPetriNet composedNetwork;
 	private final HashMap<TimedArcPetriNet, DataLayer> guiModels;
+	private final TAPNLens lens;
+	private final writeTACPN writeTACPN;
 
-	public PNMLWriter(
-			TimedArcPetriNetNetwork network, 
-			HashMap<TimedArcPetriNet, DataLayer> guiModels) {
+	public PNMLWriter(TimedArcPetriNetNetwork network, HashMap<TimedArcPetriNet, DataLayer> guiModels, TAPNLens lens) {
 		this.network = network;
 		this.guiModels = guiModels;
+		this.lens = lens;
+		writeTACPN = new writeTACPN(network);
 	}
 	
-	public ByteArrayOutputStream savePNML() throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException {
+	public ByteArrayOutputStream savePNML() throws ParserConfigurationException, DOMException, TransformerException {
 		Document document = null;
 		Transformer transformer = null;
 		ByteArrayOutputStream os = new ByteArrayOutputStream();
-		TAPNComposer composer = new TAPNComposer(new MessengerImpl(), guiModels, true, true);
+		TAPNComposer composer = new TAPNComposer(new MessengerImpl(), guiModels, lens, true, true);
 		composedNetwork = composer.transformModel(network).value1();
 		
 		// Build a Petri Net XML Document
@@ -69,17 +71,21 @@
 		pnmlRootNode.appendChild(netNode);
 		netNode.setAttribute("id", composedNetwork.name());
 		netNode.setAttribute("type", "http://www.pnml.org/version-2009/grammar/ptnet");
-		
+
+        Element nameNode = document.createElement("name"); //Name of the net
+        netNode.appendChild(nameNode);
+        Element nameText = document.createElement("text");
+        nameNode.appendChild(nameText);
+        nameText.setTextContent(composedNetwork.name());
+
+        if(lens.isColored()) {
+            writeTACPN.appendDeclarations(document, netNode);
+        }
+
 		Element pageNode = document.createElement("page"); //Page node
 		netNode.appendChild(pageNode);
 		pageNode.setAttribute("id", "page0");
-		
-		Element nameNode = document.createElement("name"); //Name of the net
-		netNode.appendChild(nameNode);
-		Element nameText = document.createElement("text");
-		nameNode.appendChild(nameText);
-		nameText.setTextContent(composedNetwork.name());
-		
+
 		appendPlaces(document, composer.getGuiModel(), pageNode);
 		appendTransitions(document, composer.getGuiModel(), pageNode);
 		appendArcs(document, composer.getGuiModel(), pageNode);
@@ -96,7 +102,7 @@
 		return os;
 	}
 
-	public void savePNML(File file) throws IOException, ParserConfigurationException, DOMException, TransformerConfigurationException, TransformerException {
+	public void savePNML(File file) throws IOException, ParserConfigurationException, DOMException, TransformerException {
 		Require.that(file != null, "Error: file to save to was null");
 		
 		try {
@@ -130,21 +136,36 @@
 	private void appendPlaces(Document document, DataLayer guiModel, Element NET) {
 		Place[] places = guiModel.getPlaces();
 		for (Place place : places) {
-			NET.appendChild(createPlaceElement((TimedPlaceComponent) place, guiModel, document));
+            if (lens.isColored()){
+                NET.appendChild(createColorPlaceElement((TimedPlaceComponent) place, guiModel, document));
+            }
+            else {
+                NET.appendChild(createPlaceElement((TimedPlaceComponent) place, guiModel, document));
+            }
 		}
 	}
 
 	private void appendTransitions(Document document, DataLayer guiModel, Element NET) {
 		Transition[] transitions = guiModel.getTransitions();
 		for (Transition transition : transitions) {
-			NET.appendChild(createTransitionElement((TimedTransitionComponent) transition, document));
+            if(lens.isColored()) {
+                NET.appendChild(createColoredTransitionElement((TimedTransitionComponent) transition, document));
+            }
+            else {
+                NET.appendChild(createTransitionElement((TimedTransitionComponent) transition, document));
+            }
 		}
 	}
 	
 	private void appendArcs(Document document, DataLayer guiModel, Element NET) {
 		Arc[] arcs = guiModel.getArcs();
 		for (Arc arc : arcs) {
-			NET.appendChild(createArcElement(arc, guiModel, document));
+            if(lens.isColored()) {
+                NET.appendChild(createColoredArcElement(arc,guiModel , document));
+            }
+            else {
+                NET.appendChild(createArcElement(arc, guiModel, document));
+            }
 		}
 	}
 
@@ -188,6 +209,38 @@
 		return placeElement;
 	}
 
+    private Element createColorPlaceElement(TimedPlaceComponent inputPlace, DataLayer guiModel, Document document) {
+        Require.that(inputPlace != null, "Error: inputPlace was null");
+        Require.that(guiModel != null, "Error: guiModel was null");
+        Require.that(document != null, "Error: document was null");
+
+        Element placeElement = document.createElement("place");
+        placeElement.setAttribute("id", (inputPlace.getId() != null ? inputPlace.getId() : inputPlace.getName()));
+
+
+        Element name = document.createElement("name"); //Name
+        placeElement.appendChild(name);
+        Element nameText = document.createElement("text");
+        name.appendChild(nameText);
+        nameText.setTextContent(inputPlace.underlyingPlace().name());
+        Element nameGraphics = document.createElement("graphics");
+        name.appendChild(nameGraphics);
+        Element nameOffset = document.createElement("offset");
+        nameGraphics.appendChild(nameOffset);
+        nameOffset.setAttribute("x", String.valueOf(Math.round(inputPlace.getNameOffsetX())));
+        nameOffset.setAttribute("y", String.valueOf(Math.round(inputPlace.getNameOffsetY())));
+
+        Element graphics = document.createElement("graphics");
+        placeElement.appendChild(graphics);
+        Element offset = document.createElement("position");
+        graphics.appendChild(offset);
+        offset.setAttribute("x", String.valueOf(Math.round(inputPlace.getPositionX())));
+        offset.setAttribute("y", String.valueOf(Math.round(inputPlace.getPositionY())));
+
+        writeTACPN.appendColoredPlaceDependencies(inputPlace.underlyingPlace(), document, placeElement);
+        return placeElement;
+    }
+
 	private Element createTransitionElement(TimedTransitionComponent inputTransition, Document document) {
 		Require.that(inputTransition != null, "Error: inputTransition was null");
 		Require.that(document != null, "Error: document was null");
@@ -217,6 +270,36 @@
 		return transitionElement;
 	}
 
+    private Element createColoredTransitionElement (TimedTransitionComponent inputTransition, Document document) {
+        Require.that(inputTransition != null, "Error: inputTransition was null");
+        Require.that(document != null, "Error: document was null");
+
+        Element transitionElement = document.createElement("transition");
+        transitionElement.setAttribute("id", (inputTransition.getId() != null ? inputTransition.getId()	: "error"));
+
+        Element name = document.createElement("name"); //Name
+        transitionElement.appendChild(name);
+        Element nameGraphics = document.createElement("graphics");
+        name.appendChild(nameGraphics);
+        Element nameOffset = document.createElement("offset");
+        nameGraphics.appendChild(nameOffset);
+        nameOffset.setAttribute("x", String.valueOf(Math.round(inputTransition.getNameOffsetX())));
+        nameOffset.setAttribute("y", String.valueOf(Math.round(inputTransition.getNameOffsetY())));
+        Element nameText = document.createElement("text");
+        name.appendChild(nameText);
+        nameText.setTextContent(inputTransition.underlyingTransition().name());
+
+        Element graphics = document.createElement("graphics");
+        transitionElement.appendChild(graphics);
+        Element offset = document.createElement("position");
+        graphics.appendChild(offset);
+        offset.setAttribute("x", String.valueOf(Math.round(inputTransition.getPositionX())));
+        offset.setAttribute("y", String.valueOf(Math.round(inputTransition.getPositionY())));
+
+        writeTACPN.appendColoredTransitionDependencies(inputTransition.underlyingTransition(), document, transitionElement);
+        return transitionElement;
+    }
+
 	private Element createArcElement(Arc arc, DataLayer guiModel, Document document) {
 		Require.that(arc != null, "Error: inputArc was null");
 		Require.that(guiModel != null, "Error: guiModel was null");
@@ -258,6 +341,47 @@
 		
 		return arcElement;
 	}
+
+    private Element createColoredArcElement(Arc arc, DataLayer guiModel, Document document) {
+        Require.that(arc != null, "Error: inputArc was null");
+        Require.that(guiModel != null, "Error: guiModel was null");
+        Require.that(document != null, "Error: document was null");
+
+        Element arcElement = document.createElement("arc");
+        arcElement.setAttribute("id", (arc.getId() != null ? arc.getId() : "error"));
+        arcElement.setAttribute("source", (arc.getSource().getId() != null ? arc.getSource().getId() : ""));
+        arcElement.setAttribute("target", (arc.getTarget().getId() != null ? arc.getTarget().getId() : ""));
+
+        writeTACPN.appendColoredArcsDependencies(arc, guiModel, document, arcElement);
+
+        if (arc instanceof TimedOutputArcComponent && arc.getWeight().value() > 1 ) {
+            Element inscription = document.createElement("inscription");
+            arcElement.appendChild(inscription);
+            Element text = document.createElement("text");
+            inscription.appendChild(text);
+            text.setTextContent(arc.getWeight().nameForSaving(false)+"");
+        }
+
+        if(arc instanceof TimedInhibitorArcComponent){
+            arcElement.setAttribute("type", "inhibitor");
+        } else {
+            arcElement.setAttribute("type", "normal");
+        }
+
+        //ArcPath
+        int arcPoints = arc.getArcPath().getArcPathDetails().length;
+        if (arcPoints > 2) {
+            Element graphics = document.createElement("graphics");
+            arcElement.appendChild(graphics);
+
+            String[][] point = arc.getArcPath().getArcPathDetails();
+            for (int j = 1; j < arcPoints-1; j++) { // Do not write the first and last point
+                graphics.appendChild(createArcPoint(point[j][0],
+                    point[j][1], point[j][2], document, j));
+            }
+        }
+        return arcElement;
+    }
 	
 	private Element createArcPoint(String x, String y, String type, Document document, int id) {
 		Require.that(document != null, "Error: document was null");

=== modified file 'src/dk/aau/cs/io/PNMLoader.java'
--- src/dk/aau/cs/io/PNMLoader.java	2020-08-26 12:29:25 +0000
+++ src/dk/aau/cs/io/PNMLoader.java	2022-03-21 20:20:44 +0000
@@ -6,28 +6,25 @@
 import java.io.FileNotFoundException;
 import java.io.IOException;
 import java.io.InputStream;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.HashMap;
-import java.util.HashSet;
+import java.util.*;
 
 import javax.xml.parsers.DocumentBuilder;
 import javax.xml.parsers.DocumentBuilderFactory;
 import javax.xml.parsers.ParserConfigurationException;
 
-import dk.aau.cs.gui.TabContent;
+import net.tapaal.gui.petrinet.TAPNLens;
+import dk.aau.cs.model.CPN.*;
+import dk.aau.cs.model.CPN.Expressions.*;
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
 import org.w3c.dom.Node;
 import org.w3c.dom.NodeList;
 import org.xml.sax.SAXException;
 
-import dk.aau.cs.gui.NameGenerator;
-import dk.aau.cs.model.tapn.Bound;
+import net.tapaal.gui.petrinet.NameGenerator;
 import dk.aau.cs.model.tapn.IntWeight;
 import dk.aau.cs.model.tapn.LocalTimedPlace;
 import dk.aau.cs.model.tapn.TimeInterval;
-import dk.aau.cs.model.tapn.TimeInvariant;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 import dk.aau.cs.model.tapn.TimedInhibitorArc;
@@ -38,463 +35,534 @@
 import dk.aau.cs.model.tapn.TimedTransition;
 import dk.aau.cs.util.FormatException;
 import dk.aau.cs.util.Require;
-import pipe.dataLayer.DataLayer;
-import pipe.dataLayer.TAPNQuery;
-import pipe.dataLayer.Template;
-import pipe.gui.Pipe;
-import pipe.gui.Zoomer;
-import pipe.gui.graphicElements.Arc;
-import pipe.gui.graphicElements.PlaceTransitionObject;
-import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
-import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
-import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
+import pipe.gui.petrinet.dataLayer.DataLayer;
+import net.tapaal.gui.petrinet.verification.TAPNQuery;
+import net.tapaal.gui.petrinet.Template;
+import pipe.gui.Constants;
+import pipe.gui.canvas.Zoomer;
+import pipe.gui.petrinet.graphicElements.Arc;
+import pipe.gui.petrinet.graphicElements.PlaceTransitionObject;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedOutputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedTransitionComponent;
 
 public class PNMLoader {
-
-    private final TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
+    private TAPNLens lens;
 
     enum GraphicsType { Position, Offset }
 
-	private final NameGenerator nameGenerator = new NameGenerator();
-	private final IdResolver idResolver = new IdResolver();
-	private final HashSet<String> arcs = new HashSet<String>();
-	private final HashMap<String, TimedPlace> places = new HashMap<String, TimedPlace>();
-	private final HashMap<String, TimedTransition> transitions = new HashMap<String, TimedTransition>();
-	
-	//If the net is too big, do not make the graphics
-	private int netSize = 0;
-	private final int maxNetSize = 4000;
-	private boolean hasPositionalInfo = false;
-	
-	public PNMLoader() {
-	}
-	
-	public LoadedModel load(File file) throws FormatException{
-		try{
-			return load(new FileInputStream(file));
-		} catch (FileNotFoundException e){
-			return null;
-		} catch (NullPointerException e){
-			throw new FormatException("the PNML file cannot be parsed due to syntax errors");
-		}
-	}
-	
-	public LoadedModel load(InputStream file) throws FormatException{
-		Document doc = loadDocument(file);
-		
-		return parse(doc);
-	}
-
-	private Document loadDocument(InputStream file) {
-		try {
-			DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder();
-			return builder.parse(file);
-		} catch (ParserConfigurationException | IOException | SAXException e) {
-			return null;
-		}
-	}
-	
-	private LoadedModel parse(Document doc) throws FormatException {
-		idResolver.clear();
-		
-		TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork();
-		
-		//We assume there is only one net per file (this is what we call a TAPN Network) 
-		Node pnmlElement = doc.getElementsByTagName("pnml").item(0);
-		Node netNode = getFirstDirectChild(pnmlElement, "net");
-		
-		String name = getTAPNName(netNode);
-		
-		TimedArcPetriNet tapn = new TimedArcPetriNet(name);
-		tapn.setCheckNames(false);
-		network.add(tapn);
-		nameGenerator.add(tapn);
-
-		//We assume there is only one page pr. file (this is what we call a net) 
-		Template template = new Template(tapn, new DataLayer(), new Zoomer());
-	
-		parseTimedArcPetriNet(netNode, tapn, template);
-		template.setHasPositionalInfo(hasPositionalInfo);
-		
-		network.setPaintNet(isNetDrawable());
-		tapn.setCheckNames(true);
-		return new LoadedModel(network, Arrays.asList(template), new ArrayList<TAPNQuery>(), new ArrayList<>(), null);
-	}
-
-	private String getTAPNName(Node netNode) {
-		if(!(netNode instanceof Element)){
-			return nameGenerator.getNewTemplateName();
-		}
-		String result = null;
-
-		Node name =  getFirstDirectChild(netNode, "name");
-		if(name != null){
-			result = getFirstDirectChild(name, "text").getTextContent();
-		}
-		
-		if(name == null || name.equals("")){
-			return nameGenerator.getNewTemplateName();
-		}
-		
-		return NamePurifier.purify(result);
-	}
-
-	private void parseTimedArcPetriNet(Node netNode, TimedArcPetriNet tapn, Template template) throws FormatException {
-		//We assume there is only one page pr. file (this is what we call a net) 
-		Node node = getFirstDirectChild(netNode, "page").getFirstChild();
-		Node first = node;
-		
-		//Calculate netsize
-		while(node != null){
-			netSize += 1;
-			node = node.getNextSibling();
-		}
-		
-		node = first;
-		//We parse the places and transitions first
-		while(node != null){
-			String tag = node.getNodeName();
-			if(tag.equals("place")){
-				parsePlace(node, tapn, template);
-			} else if(tag.equals("transition")){
-				parseTransition(node, tapn, template);
-			}
-			node = node.getNextSibling();
-		}
-		
-		//We parse the transitions last, as we need the places and transitions it refers to
-		node = first;
-		while(node != null){
-			String tag = node.getNodeName();
-			if(tag.equals("arc")){
-				parseArc(node, template);
-			} 
-			node = node.getNextSibling();
-		}
-	}
-
-	private void parsePlace(Node node, TimedArcPetriNet tapn, Template template) {
-		if(!(node instanceof Element)){
-			return;
-		}
-		
-		Name name = parseName(getFirstDirectChild(node, "name"));
-		if(name == null){
-			name = new Name(nameGenerator.getNewPlaceName(template.model()));
-		}
-		Point position = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Position);
-		String id = NamePurifier.purify(((Element) node).getAttribute("id"));
-		InitialMarking marking = parseMarking(getFirstDirectChild(node, "initialMarking")); 
-		
-		TimedPlace place = new LocalTimedPlace(id, new TimeInvariant(false, new Bound.InfBound()));
-		Require.that(places.put(id, place) == null && !transitions.containsKey(id), 
-				"The name: " + id + ", was already used");
-		tapn.add(place);
-		
-		if(isNetDrawable()){
-			//We parse the id as both the name and id as in tapaal name = id, and name/id has to be unique 
-			TimedPlaceComponent placeComponent = new TimedPlaceComponent(position.x, position.y, id, name.point.x, name.point.y, lens);
-			placeComponent.setUnderlyingPlace(place);
-			template.guiModel().addPetriNetObject(placeComponent);
-		}
-		
-		idResolver.add(tapn.name(), id, id);
-		
-		for (int i = 0; i < marking.marking; i++) {
-			tapn.parentNetwork().marking().add(new TimedToken(place));
-		}
-	}
-	
-	private InitialMarking parseMarking(Node node) {
-		if(!(node instanceof Element)){
-			return new InitialMarking();
-		}
-		
-		Point offset = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Offset);
-		
-		int marking = Integer.parseInt(getFirstDirectChild(node, "text").getTextContent());
-		
-		return new InitialMarking(marking, offset);
-	}
-
-	private void parseTransition(Node node, TimedArcPetriNet tapn, Template template) {
-		if(!(node instanceof Element)){
-			return;
-		}
-		
-		Point position = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Position);
-		Name name = parseName(getFirstDirectChild(node, "name"));
-		if(name == null){
-			name = new Name(nameGenerator.getNewTransitionName(template.model()));
-		}
-		String id = NamePurifier.purify(((Element) node).getAttribute("id"));
-		
-		TimedTransition transition = new TimedTransition(id);
-		Require.that(transitions.put(id, transition) == null && !places.containsKey(id), 
-				"The id: " + id + ", was already used");
-		tapn.add(transition);
-		
-		if(isNetDrawable()){
-			TimedTransitionComponent transitionComponent = 
-				//We parse the id as both the name and id as in tapaal name = id, and name/id has to be unique 
-				new TimedTransitionComponent(position.x, position.y, id, name.point.x, name.point.y, true, false, 0, 0, lens);
-			transitionComponent.setUnderlyingTransition(transition);
-			template.guiModel().addPetriNetObject(transitionComponent);
-		}
-		idResolver.add(tapn.name(), id, id);
-	}
-	
-	private void parseArc(Node node, Template template) throws FormatException {
-		if(!(node instanceof Element)){
-			return;
-		}
-		
-		Element element = (Element) node;
-		
-		String id = element.getAttribute("id");
-		String sourceId = NamePurifier.purify(element.getAttribute("source"));
-		String targetId = NamePurifier.purify(element.getAttribute("target"));
-		String type = element.getAttribute("type");
-		
-		String sourceName = idResolver.get(template.model().name(), sourceId);
-		String targetName = idResolver.get(template.model().name(), targetId);
-		
-		TimedPlace sourcePlace = places.get(sourceName);
-		TimedPlace targetPlace = places.get(targetName);
-		
-		TimedTransition sourceTransition = transitions.get(sourceName);
-		TimedTransition targetTransition = transitions.get(targetName);
-		
-		PlaceTransitionObject source = template.guiModel().getPlaceTransitionObject(sourceName);
-		PlaceTransitionObject target = template.guiModel().getPlaceTransitionObject(targetName);
-		
-		//Inscription
-		int weight = 1;
-		Node inscription  = getFirstDirectChild(node, "inscription");
-		if(inscription != null){
-			Node text = getFirstDirectChild(inscription, "text");
-			if(text != null){
-				String weightString = text.getTextContent().trim();
+    private final NameGenerator nameGenerator = new NameGenerator();
+    private final IdResolver idResolver = new IdResolver();
+    private final HashSet<String> arcs = new HashSet<String>();
+    private final HashMap<String, TimedPlace> places = new HashMap<String, TimedPlace>();
+    private final HashMap<String, TimedTransition> transitions = new HashMap<String, TimedTransition>();
+    private final HashMap<String, ColorType> colortypes = new HashMap<String, ColorType>();
+    private final HashMap<String, Variable> variables = new HashMap<String, Variable>();
+
+    //If the net is too big, do not make the graphics
+    private int netSize = 0;
+    private final int maxNetSize = 4000;
+    private boolean hasPositionalInfo = false;
+    private final LoadTACPN loadTACPN;
+
+    public PNMLoader() {
+        this.lens = TAPNLens.Default;
+        loadTACPN = new LoadTACPN();
+    }
+
+    public LoadedModel load(File file) throws FormatException{
+        try{
+            return load(new FileInputStream(file));
+        } catch (FileNotFoundException e){
+            return null;
+        } catch (NullPointerException e){
+            throw new FormatException("the PNML file cannot be parsed due to syntax errors", e);
+        }
+    }
+
+    public LoadedModel load(InputStream file) throws FormatException{
+        Document doc = loadDocument(file);
+
+        return parse(doc);
+    }
+
+    private Document loadDocument(InputStream file) {
+        try {
+            DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder();
+            return builder.parse(file);
+        } catch (ParserConfigurationException | IOException | SAXException e) {
+            return null;
+        }
+    }
+
+    private LoadedModel parse(Document doc) throws FormatException {
+        idResolver.clear();
+
+        TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork();
+
+        //We assume there is only one net per file (this is what we call a TAPN Network)
+        Node pnmlElement = doc.getElementsByTagName("pnml").item(0);
+        Node netNode = getFirstDirectChild(pnmlElement, "net");
+
+        lens = new TAPNLens(false, false, getFirstDirectChild(netNode, "declaration") != null);
+
+        String name = getTAPNName(netNode);
+
+        TimedArcPetriNet tapn = new TimedArcPetriNet(name);
+        tapn.setCheckNames(false);
+        network.add(tapn);
+        nameGenerator.add(tapn);
+
+        //We assume there is only one page pr. file (this is what we call a net)
+        Template template = new Template(tapn, new DataLayer(), new Zoomer());
+
+        parseTimedArcPetriNet(netNode, tapn, template, network);
+        template.setHasPositionalInfo(hasPositionalInfo);
+
+        network.setPaintNet(isNetDrawable());
+        tapn.setCheckNames(true);
+
+        return new LoadedModel(network, List.of(template), new ArrayList<TAPNQuery>(), new ArrayList<>(), lens);
+    }
+
+    private String getTAPNName(Node netNode) {
+        if(!(netNode instanceof Element)){
+            return nameGenerator.getNewTemplateName();
+        }
+        String result = null;
+
+        Node name =  getFirstDirectChild(netNode, "name");
+        if(name != null){
+            result = getFirstDirectChild(name, "text").getTextContent();
+        }
+
+        if(name == null || name.equals("")){
+            return nameGenerator.getNewTemplateName();
+        }
+
+        return NamePurifier.purify(result);
+    }
+
+    private void parseTimedArcPetriNet(Node netNode, TimedArcPetriNet tapn, Template template, TimedArcPetriNetNetwork network) throws FormatException {
+        if (lens.isColored()) {
+            Node declarations = getFirstDirectChild(netNode, "declaration");
+            loadTACPN.parseDeclarations(declarations, network);
+        }
+
+        //We assume there is only one page pr. file (this is what we call a net)
+        Node node = getFirstDirectChild(netNode, "page").getFirstChild();
+        Node first = node;
+
+        //Calculate netsize
+        while(node != null){
+            netSize += 1;
+            node = node.getNextSibling();
+        }
+
+        node = first;
+        //We parse the places and transitions first
+        while(node != null){
+            String tag = node.getNodeName();
+            if(tag.equals("place")){
+                parsePlace(node, tapn, template);
+            } else if(tag.equals("transition")){
+                parseTransition(node, tapn, template);
+            }
+            node = node.getNextSibling();
+        }
+        //We parse the transitions last, as we need the places and transitions it refers to
+        node = first;
+        while(node != null){
+            String tag = node.getNodeName();
+            if(tag.equals("arc")){
+                parseArc(node, template);
+            }
+            node = node.getNextSibling();
+        }
+    }
+    private void parsePlace(Node node, TimedArcPetriNet tapn, Template template) throws FormatException {
+        if (!(node instanceof Element)) {
+            return;
+        }
+
+        Name name = parseName(getFirstDirectChild(node, "name"));
+        if (name == null) {
+            name = new Name(nameGenerator.getNewPlaceName(template.model()));
+        }
+        Point position = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Position);
+        String id = NamePurifier.purify(((Element) node).getAttribute("id"));
+        ArcExpression colorMarking = null;
+        Point markingOffset = null;
+        TimedPlace place;
+        InitialMarking marking = parseMarking(getFirstDirectChild(node, "initialMarking"));
+        ColorType colorType = ColorType.COLORTYPE_DOT;
+        Node typeNode = getFirstDirectChild(node, "type");
+        if (typeNode != null) {
+            try {
+                colorType = loadTACPN.parseUserSort(typeNode);
+            } catch (FormatException e) {
+                e.printStackTrace();
+            }
+        }
+        Node markingNode = getFirstDirectChild(node, "hlinitialMarking");
+        if (markingNode instanceof Element) {
+            try {
+                colorMarking = loadTACPN.parseArcExpression(((Element) markingNode).getElementsByTagName("structure").item(0));
+            } catch (FormatException e) {
+                e.printStackTrace();
+            }
+        }
+        place = new LocalTimedPlace(id, colorType);
+
+        Require.that(places.put(id, place) == null && !transitions.containsKey(id),
+            "The name: " + id + ", was already used");
+        tapn.add(place);
+
+        if (isNetDrawable()) {
+            //We parse the id as both the name and id as in tapaal name = id, and name/id has to be unique
+            TimedPlaceComponent placeComponent;
+            placeComponent = new TimedPlaceComponent(position.x, position.y, id, name.point.x, name.point.y, lens);
+            placeComponent.setUnderlyingPlace(place);
+            template.guiModel().addPetriNetObject(placeComponent);
+        }
+
+        idResolver.add(tapn.name(), id, id);
+
+
+        if (colorMarking != null) {
+            ExpressionContext context = new ExpressionContext(new HashMap<String, Color>(), loadTACPN.getColortypes());
+            ColorMultiset cm = colorMarking.eval(context);
+            place.setTokenExpression(loadTACPN.constructCleanAddExpression(colorType,cm));
+            for (TimedToken ct : cm.getTokens(place)) {
+                tapn.parentNetwork().marking().add(ct);
+            }
+
+        } else {
+            for (int i = 0; i < marking.marking; i++) {
+                tapn.parentNetwork().marking().add(new TimedToken(place, ColorType.COLORTYPE_DOT.getFirstColor()));
+            }
+            if (marking.marking > 1) {
+                Vector<ColorExpression> v = new Vector<>();
+                v.add(new DotConstantExpression());
+                Vector<ArcExpression> numbOfExpression = new Vector<>();
+                numbOfExpression.add(new NumberOfExpression(marking.marking, v));
+                place.setTokenExpression(new AddExpression(numbOfExpression));
+            }
+        }
+    }
+
+
+    private static Node skipWS(Node node) {
+        if (node != null && !(node instanceof Element)) {
+            return skipWS(node.getNextSibling());
+        } else {
+            return node;
+        }
+    }
+
+    private static Node getAttribute(Node node, String attribute) {
+        return node.getAttributes().getNamedItem(attribute);
+    }
+
+
+    private InitialMarking parseMarking(Node node) {
+        if(!(node instanceof Element)){
+            return new InitialMarking();
+        }
+
+        Point offset = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Offset);
+
+        int marking = Integer.parseInt(getFirstDirectChild(node, "text").getTextContent());
+
+        return new InitialMarking(marking, offset);
+    }
+
+    private void parseTransition(Node node, TimedArcPetriNet tapn, Template template) throws FormatException {
+        if(!(node instanceof Element)){
+            return;
+        }
+
+        Point position = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Position);
+        Name name = parseName(getFirstDirectChild(node, "name"));
+        if(name == null){
+            name = new Name(nameGenerator.getNewTransitionName(template.model()));
+        }
+        String id = NamePurifier.purify(((Element) node).getAttribute("id"));
+
+        GuardExpression guardExpression = null;
+        Node conditionNode = getFirstDirectChild(node, "condition");
+        if (conditionNode != null) {
+            guardExpression = loadTACPN.parseGuardExpression(getFirstDirectChild(conditionNode, "structure"));
+        }
+
+        TimedTransition transition = new TimedTransition(id, guardExpression);
+        Require.that(transitions.put(id, transition) == null && !places.containsKey(id),
+            "The id: " + id + ", was already used");
+        tapn.add(transition);
+
+        if(isNetDrawable()){
+            TimedTransitionComponent transitionComponent =
+                //We parse the id as both the name and id as in tapaal name = id, and name/id has to be unique
+                new TimedTransitionComponent(position.x, position.y, id, name.point.x, name.point.y, 0, lens);
+            transitionComponent.setUnderlyingTransition(transition);
+            template.guiModel().addPetriNetObject(transitionComponent);
+        }
+        idResolver.add(tapn.name(), id, id);
+    }
+
+    private void parseArc(Node node, Template template) throws FormatException {
+        if(!(node instanceof Element)){
+            return;
+        }
+
+        Element element = (Element) node;
+
+        String id = element.getAttribute("id");
+        String sourceId = NamePurifier.purify(element.getAttribute("source"));
+        String targetId = NamePurifier.purify(element.getAttribute("target"));
+        String type = element.getAttribute("type");
+
+        String sourceName = idResolver.get(template.model().name(), sourceId);
+        String targetName = idResolver.get(template.model().name(), targetId);
+
+        TimedPlace sourcePlace = places.get(sourceName);
+        TimedPlace targetPlace = places.get(targetName);
+
+        TimedTransition sourceTransition = transitions.get(sourceName);
+        TimedTransition targetTransition = transitions.get(targetName);
+
+        PlaceTransitionObject source = template.guiModel().getPlaceTransitionObject(sourceName);
+        PlaceTransitionObject target = template.guiModel().getPlaceTransitionObject(targetName);
+
+        //Inscription
+        int weight = 1;
+        Node inscription  = getFirstDirectChild(node, "inscription");
+        if(inscription != null){
+            Node text = getFirstDirectChild(inscription, "text");
+            if(text != null){
+                String weightString = text.getTextContent().trim();
                 try {
                     weight = Integer.parseInt(weightString);
                 } catch (NumberFormatException ignored) {} //Default values is 1
-			}
-		}
-		
-		int _startx = 0, _starty = 0, _endx = 0, _endy = 0;
-		
-		if(isNetDrawable()){
-			// add the insets and offset
-			_startx = source.getX() + source.centreOffsetLeft();
-			_starty = source.getY() + source.centreOffsetTop();
-
-			_endx = target.getX() + target.centreOffsetLeft();
-			_endy = target.getY() + target.centreOffsetTop();
-		}
-		
-		Arc tempArc;
-		
-		if(type != null && type.equals("inhibitor")) {
-			tempArc = parseAndAddTimedInhibitorArc(id, sourcePlace, targetTransition, source, target, weight, _endx, _endy, template);
-		} else if(sourcePlace != null && targetTransition != null) {
-			tempArc = parseInputArc(id, sourcePlace, targetTransition, source, target, weight, _endx, _endy, template);
-		} else if(sourceTransition != null && targetPlace != null) {
-			tempArc = parseOutputArc(id,  sourceTransition, targetPlace, source, target, weight, _endx, _endy, template);
-		} else {
-			throw new FormatException("Arcs must be only between places and transitions");
-		}
-		
-		if(isNetDrawable()) parseArcPath(element, tempArc);
-	}
-	
-	private void parseArcPath(Element arc, Arc tempArc) {
-		Element element = (Element) getFirstDirectChild(arc, "graphics");
-		if(element == null) return;
-		NodeList nodelist = element.getElementsByTagName("position");
-		if (nodelist.getLength() > 0) {
-			for (int i = 0; i < nodelist.getLength(); i++) {
-				Node node = nodelist.item(i);
-				if (node instanceof Element) {
-					Element position = (Element) node;
-					if ("position".equals(position.getNodeName())) {
-						String arcTempX = position.getAttribute("x");
-						String arcTempY = position.getAttribute("y");
-
-						double arcPointX = Double.parseDouble(arcTempX);
+            }
+        }
+
+        int _startx = 0, _starty = 0, _endx = 0, _endy = 0;
+
+        if(isNetDrawable()){
+            // add the insets and offset
+            _startx = source.getX() + source.centreOffsetLeft();
+            _starty = source.getY() + source.centreOffsetTop();
+
+            _endx = target.getX() + target.centreOffsetLeft();
+            _endy = target.getY() + target.centreOffsetTop();
+        }
+
+        Arc tempArc;
+        ArcExpression arcExpression = null;
+        Node hlInscriptionNode = getFirstDirectChild(node, "hlinscription");
+        if (hlInscriptionNode != null) {
+            arcExpression = loadTACPN.parseArcExpression(getFirstDirectChild(hlInscriptionNode, "structure"));
+        }
+
+        if(type != null && type.equals("inhibitor")) {
+            tempArc = parseAndAddTimedInhibitorArc(id, sourcePlace, targetTransition, source, target, weight, arcExpression, _endx, _endy, template);
+        } else if(sourcePlace != null && targetTransition != null) {
+            tempArc = parseInputArc(id, sourcePlace, targetTransition, source, target, weight, arcExpression, _endx, _endy, template);
+        } else if(sourceTransition != null && targetPlace != null) {
+            tempArc = parseOutputArc(id,  sourceTransition, targetPlace, source, target, weight, arcExpression, _endx, _endy, template);
+        } else {
+            throw new FormatException("Arcs must be only between places and transitions");
+        }
+
+        if(isNetDrawable()) parseArcPath(element, tempArc);
+    }
+
+    private void parseArcPath(Element arc, Arc tempArc) {
+        Element element = (Element) getFirstDirectChild(arc, "graphics");
+        if(element == null) return;
+        NodeList nodelist = element.getElementsByTagName("position");
+        if (nodelist.getLength() > 0) {
+            for (int i = 0; i < nodelist.getLength(); i++) {
+                Node node = nodelist.item(i);
+                if (node instanceof Element) {
+                    Element position = (Element) node;
+                    if ("position".equals(position.getNodeName())) {
+                        String arcTempX = position.getAttribute("x");
+                        String arcTempY = position.getAttribute("y");
+
+                        double arcPointX = Double.parseDouble(arcTempX);
                         double arcPointY = Double.parseDouble(arcTempY);
-						arcPointX += Pipe.ARC_CONTROL_POINT_CONSTANT + 1;
-						arcPointY += Pipe.ARC_CONTROL_POINT_CONSTANT + 1;
-						
-						//We add the point at i+1 as the starting and end points of 
-						//the arc is already in the path as point number 0 and 1
-						tempArc.getArcPath().addPoint(i+1,arcPointX, arcPointY, false);
-					}
-				}
-			}
-		}
-	}
-
-	private Name parseName(Node node){
-		if(!(node instanceof Element)){
-			return null;
-		}
-		Point offset = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Offset);
-		
-		String name = getFirstDirectChild(node, "text").getTextContent();
-		if(name == null || name.equals("")){
-			return null;
-		}
-		
-		name = NamePurifier.purify(name);
-		return new Name(name, offset);
-	}
-	
-	private Point parseGraphics(Node node, GraphicsType type){
-		if(!(node instanceof Element)){
-			if(type == GraphicsType.Offset)
-				return new Point(0, -10);
-			else 
-				return new Point(100, 100);
-		}
-		
-		hasPositionalInfo = true;
-		Element offset = (Element)getFirstDirectChild(node, type == GraphicsType.Offset ? "offset" : "position");
-		
-		String x = offset.getAttribute("x");
-		String y = offset.getAttribute("y");
-		
-                int xd = Math.round(Float.parseFloat(x));
-                int yd = Math.round(Float.parseFloat(y));
-               
-		return new Point(xd, yd);
-	}
-
-	private static class Name{
-		String name;
-		Point point;
-		
-		public Name(String newPlaceName) {
-			this(newPlaceName, new Point());
-		}
-		
-		public Name(String name, Point p) {
-			this.name = name;
-			this.point = p;
-		}
-
-		@Override
-		public String toString() {
-			return name + ";" + point;
-		}
-	}
-	
-	private static class InitialMarking{
-		int marking;
-		Point point;
-		
-		public InitialMarking() {
-			this(0, new Point());
-		}
-			
-		
-		public InitialMarking(int marking, Point p) {
-			this.marking = marking;
-			this.point = p;
-		}
-		
-		@Override
-		public String toString() {
-			return marking + ";" + point;
-		}
-	}
-	
-	private TimedInputArcComponent parseInputArc(String arcId, TimedPlace place, TimedTransition transition, PlaceTransitionObject source,
-                                                 PlaceTransitionObject target, int weight, int _endx,
+                        arcPointX += Constants.ARC_CONTROL_POINT_CONSTANT + 1;
+                        arcPointY += Constants.ARC_CONTROL_POINT_CONSTANT + 1;
+
+                        //We add the point at i+1 as the starting and end points of
+                        //the arc is already in the path as point number 0 and 1
+                        tempArc.getArcPath().addPoint(i+1,arcPointX, arcPointY, false);
+                    }
+                }
+            }
+        }
+    }
+
+    private Name parseName(Node node){
+        if(!(node instanceof Element)){
+            return null;
+        }
+        Point offset = parseGraphics(getFirstDirectChild(node, "graphics"), GraphicsType.Offset);
+
+        String name = getFirstDirectChild(node, "text").getTextContent();
+        if(name == null || name.equals("")){
+            return null;
+        }
+
+        name = NamePurifier.purify(name);
+        return new Name(name, offset);
+    }
+
+    private Point parseGraphics(Node node, GraphicsType type){
+        if(!(node instanceof Element)){
+            if(type == GraphicsType.Offset)
+                return new Point(0, -10);
+            else
+                return new Point(100, 100);
+        }
+
+        hasPositionalInfo = true;
+        Element offset = (Element)getFirstDirectChild(node, type == GraphicsType.Offset ? "offset" : "position");
+
+        String x = offset.getAttribute("x");
+        String y = offset.getAttribute("y");
+
+        int xd = Math.round(Float.parseFloat(x));
+        int yd = Math.round(Float.parseFloat(y));
+
+        return new Point(xd, yd);
+    }
+
+    private static class Name{
+        final String name;
+        final Point point;
+
+        public Name(String newPlaceName) {
+            this(newPlaceName, new Point());
+        }
+
+        public Name(String name, Point p) {
+            this.name = name;
+            this.point = p;
+        }
+
+        @Override
+        public String toString() {
+            return name + ";" + point;
+        }
+    }
+
+    private static class InitialMarking{
+        final int marking;
+        final Point point;
+
+        public InitialMarking() {
+            this(0, new Point());
+        }
+
+
+        public InitialMarking(int marking, Point p) {
+            this.marking = marking;
+            this.point = p;
+        }
+
+        @Override
+        public String toString() {
+            return marking + ";" + point;
+        }
+    }
+
+    private TimedInputArcComponent parseInputArc(String arcId, TimedPlace place, TimedTransition transition, PlaceTransitionObject source,
+                                                 PlaceTransitionObject target, int weight, ArcExpression arcExpression, int _endx,
                                                  int _endy, Template template) throws FormatException {
-
-		TimedInputArc inputArc = new TimedInputArc(place, transition, TimeInterval.ZERO_INF, new IntWeight(weight));
-		
-		Require.that(places.containsKey(inputArc.source().name()),	"The source place must be part of the petri net.");
-		Require.that(transitions.containsKey(inputArc.destination().name()), "The destination transition must be part of the petri net");
-		if(!arcs.add(inputArc.source().name() + "-in-" + inputArc.destination().name())) {
-			throw new FormatException("Multiple arcs between a place and a transition is not allowed");
-		}
-		
-		TimedInputArcComponent arc = null;
-		
-		if(isNetDrawable()){
-			arc = new TimedInputArcComponent(new TimedOutputArcComponent(source, target, weight, arcId), lens);
-			arc.setUnderlyingArc(inputArc);
-
-			template.guiModel().addPetriNetObject(arc);
-		}
-		
-		template.model().add(inputArc);
-		
-		return arc;
-
-		
-	}
-	
-	private Arc parseOutputArc(String arcId, TimedTransition transition, TimedPlace place, PlaceTransitionObject source,
-                               PlaceTransitionObject target, int weight, int _endx,
+        TimedInputArc inputArc = new TimedInputArc(place, transition, TimeInterval.ZERO_INF, new IntWeight(weight), arcExpression);
+
+        Require.that(places.containsKey(inputArc.source().name()),	"The source place must be part of the petri net.");
+        Require.that(transitions.containsKey(inputArc.destination().name()), "The destination transition must be part of the petri net");
+        if(!arcs.add(inputArc.source().name() + "-in-" + inputArc.destination().name())) {
+            throw new FormatException("Multiple arcs between a place and a transition is not allowed");
+        }
+
+        TimedInputArcComponent arc = null;
+
+        if(isNetDrawable()){
+            arc = new TimedInputArcComponent(new TimedOutputArcComponent(source, target, weight, arcId), lens);
+            arc.setUnderlyingArc(inputArc);
+
+            template.guiModel().addPetriNetObject(arc);
+        }
+
+        template.model().add(inputArc);
+
+        return arc;
+
+
+    }
+
+    private Arc parseOutputArc(String arcId, TimedTransition transition, TimedPlace place, PlaceTransitionObject source,
+                               PlaceTransitionObject target, int weight, ArcExpression arcExpression, int _endx,
                                int _endy, Template template) throws FormatException {
-		
-		TimedOutputArc outputArc = new TimedOutputArc(transition, place, new IntWeight(weight));
-		
-		Require.that(places.containsKey(outputArc.destination().name()), "The destination place must be part of the petri net.");
-		Require.that(transitions.containsKey(outputArc.source().name()), "The source transition must be part of the petri net");
-		if(!arcs.add(outputArc.source().name() + "-out-" + outputArc.destination().name())) {
-			throw new FormatException("Multiple arcs between a place and a transition is not allowed");
-		}
-		
-		TimedOutputArcComponent arc = null;
-		
-		if(isNetDrawable()){
-			arc = new TimedOutputArcComponent(
+        TimedOutputArc outputArc = new TimedOutputArc(transition, place, new IntWeight(weight),arcExpression);
+
+        Require.that(places.containsKey(outputArc.destination().name()), "The destination place must be part of the petri net.");
+        Require.that(transitions.containsKey(outputArc.source().name()), "The source transition must be part of the petri net");
+        if(!arcs.add(outputArc.source().name() + "-out-" + outputArc.destination().name())) {
+            throw new FormatException("Multiple arcs between a place and a transition is not allowed");
+        }
+
+        TimedOutputArcComponent arc = null;
+
+        if(isNetDrawable()){
+            arc = new TimedOutputArcComponent(
                 source, target, weight,	arcId);
-			arc.setUnderlyingArc(outputArc);
-
-			template.guiModel().addPetriNetObject(arc);
-
-		}
-		
-		template.model().add(outputArc);
-		return arc;
-	}
-	
-	private Arc parseAndAddTimedInhibitorArc(String arcId, TimedPlace place, TimedTransition transition, PlaceTransitionObject source,
-                                             PlaceTransitionObject target, int weight, int _endx,
+            arc.setUnderlyingArc(outputArc);
+
+            template.guiModel().addPetriNetObject(arc);
+
+        }
+
+        template.model().add(outputArc);
+        return arc;
+    }
+
+    private Arc parseAndAddTimedInhibitorArc(String arcId, TimedPlace place, TimedTransition transition, PlaceTransitionObject source,
+                                             PlaceTransitionObject target, int weight, ArcExpression arcExpression, int _endx,
                                              int _endy, Template template) {
-		TimedInhibitorArcComponent tempArc = new TimedInhibitorArcComponent(
-				new TimedInputArcComponent(
-						new TimedOutputArcComponent(source, target, weight, arcId)
-				),
-				(""));
-		
-		TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, TimeInterval.ZERO_INF, new IntWeight(weight));
-
-		tempArc.setUnderlyingArc(inhibArc);
-		template.guiModel().addPetriNetObject(tempArc);
-		template.model().add(inhibArc);
-
-		return tempArc;
-	}
-	
-	private boolean isNetDrawable(){
-		return netSize <= maxNetSize;
-	}
-	
-	Node getFirstDirectChild(Node parent, String tagName){
-		NodeList children = parent.getChildNodes();
-		for(int i = 0; i < children.getLength(); i++){
-			if(children.item(i).getNodeName().equals(tagName)){
-				return children.item(i);
-			}
-		}
-		return null;
-	}
+        TimedInhibitorArcComponent tempArc = new TimedInhibitorArcComponent(
+            new TimedInputArcComponent(
+                new TimedOutputArcComponent(source, target, weight, arcId)
+            ));
+
+        TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, TimeInterval.ZERO_INF, new IntWeight(weight), arcExpression);
+
+        tempArc.setUnderlyingArc(inhibArc);
+        template.guiModel().addPetriNetObject(tempArc);
+        template.model().add(inhibArc);
+
+        return tempArc;
+    }
+
+    private boolean isNetDrawable(){
+        return netSize <= maxNetSize;
+    }
+
+    Node getFirstDirectChild(Node parent, String tagName){
+        NodeList children = parent.getChildNodes();
+        for(int i = 0; i < children.getLength(); i++){
+            if(children.item(i).getNodeName().equals(tagName)){
+                return children.item(i);
+            }
+        }
+        return null;
+    }
 
 }

=== added file 'src/dk/aau/cs/io/TapnEngineXmlLoader.java'
--- src/dk/aau/cs/io/TapnEngineXmlLoader.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/io/TapnEngineXmlLoader.java	2022-03-21 20:20:44 +0000
@@ -0,0 +1,993 @@
+package dk.aau.cs.io;
+
+import net.tapaal.gui.petrinet.NameGenerator;
+import net.tapaal.gui.petrinet.TAPNLens;
+import dk.aau.cs.io.queries.TAPNQueryLoader;
+import dk.aau.cs.model.CPN.*;
+import dk.aau.cs.model.CPN.Expressions.*;
+import dk.aau.cs.model.tapn.*;
+import dk.aau.cs.util.FormatException;
+import dk.aau.cs.util.Require;
+import kotlin.Pair;
+import org.w3c.dom.Document;
+import org.w3c.dom.Element;
+import org.w3c.dom.Node;
+import org.w3c.dom.NodeList;
+import org.xml.sax.SAXException;
+import pipe.gui.petrinet.dataLayer.DataLayer;
+import net.tapaal.gui.petrinet.Template;
+import pipe.gui.Constants;
+import pipe.gui.canvas.Zoomer;
+import pipe.gui.petrinet.graphicElements.AnnotationNote;
+import pipe.gui.petrinet.graphicElements.Arc;
+import pipe.gui.petrinet.graphicElements.Place;
+import pipe.gui.petrinet.graphicElements.PlaceTransitionObject;
+import pipe.gui.petrinet.graphicElements.tapn.*;
+
+import javax.xml.parsers.DocumentBuilder;
+import javax.xml.parsers.DocumentBuilderFactory;
+import javax.xml.parsers.ParserConfigurationException;
+import java.io.File;
+import java.io.IOException;
+import java.util.*;
+
+/*
+    This is a huge quick hack to allow reading an unfolded net from then engine.
+    The engine format uses <graphics> tags to store elements unlike the tapn format.
+
+    It feel like this should not work, but it seems to do, and we needed a quick hack to get it working.
+
+ */
+
+public class TapnEngineXmlLoader {
+	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 final HashMap<TimedTransitionComponent, TimedTransportArcComponent> presetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
+	private final HashMap<TimedTransitionComponent, TimedTransportArcComponent> postsetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
+	private final HashMap<TimedTransportArcComponent, TimeInterval> transportArcsTimeIntervals = new HashMap<TimedTransportArcComponent, TimeInterval>();
+    private final HashMap<TimedTransportArcComponent, List<ColoredTimeInterval>> coloredTransportArcsTimeIntervals = new HashMap<TimedTransportArcComponent, List<ColoredTimeInterval>>();
+    private ArcExpression transportExpr;
+
+    private final NameGenerator nameGenerator = new NameGenerator();
+	private boolean firstInhibitorIntervalWarning = true;
+	private boolean firstPlaceRenameWarning = true;
+	private final IdResolver idResolver = new IdResolver();
+    private final Collection<String> messages = new ArrayList<>(10);
+    private final LoadTACPN loadTACPN = new LoadTACPN();
+
+    boolean hasFeatureTag = false;
+    private TAPNLens lens = TAPNLens.Default;
+
+	public TapnEngineXmlLoader() {}
+	
+	public LoadedModel load(File file) throws Exception {
+		Require.that(file != null && file.exists(), "file must be non-null and exist");
+
+		Document doc = loadDocument(file);
+		if(doc == null) return null;
+        try {
+            return parse(doc);
+        } catch (FormatException | NullPointerException e) {
+            throw e;
+        } catch (Exception e) {
+            throw new Exception("One or more necessary attributes were not found\n  - One or more attribute values have an incorrect type", e);
+        }
+	}
+
+	private Document loadDocument(File file) {
+		try {
+			DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder();
+			return builder.parse(file);
+		} catch (ParserConfigurationException | IOException | SAXException e) {
+			return null;
+		}
+	}
+
+	private LoadedModel parse(Document doc) throws FormatException {
+		idResolver.clear();
+
+		ConstantStore constants = new ConstantStore(parseConstants(doc));
+		TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(constants, new ArrayList<>());
+        NodeList declarations = doc.getElementsByTagName("declaration");
+
+        if (declarations.getLength() > 0) {
+            for (int i = 0; i < declarations.getLength(); i++) {
+                Node node = declarations.item(i);
+                if (node.getNodeName().equals("declaration")) {
+                    loadTACPN.parseDeclarations(node, network);
+                }
+            }
+            for(String message : loadTACPN.getMessages()){
+                messages.add(message);
+            }
+        } else{
+            network.add(ColorType.COLORTYPE_DOT);
+        }
+		parseSharedPlaces(doc, network, constants);
+		parseSharedTransitions(doc, network);
+		
+		Collection<Template> templates = parseTemplates(doc, network, constants);
+		LoadedQueries loadedQueries = new TAPNQueryLoader(doc, network).parseQueries();
+
+		if (loadedQueries != null) {
+            for (String message : loadedQueries.getMessages()) {
+                messages.add(message);
+            }
+        }
+		network.buildConstraints();
+		
+		parseBound(doc, network);
+
+		parseFeature(doc, network);
+
+        if (hasFeatureTag) {
+            return new LoadedModel(network, templates, loadedQueries.getQueries(), messages, lens);
+        } else {
+            return new LoadedModel(network, templates, loadedQueries.getQueries(), messages, null);
+        }
+	}
+
+	private void parseBound(Document doc, TimedArcPetriNetNetwork network){
+		if(doc.getElementsByTagName("k-bound").getLength() > 0){
+			int i = Integer.parseInt(doc.getElementsByTagName("k-bound").item(0).getAttributes().getNamedItem("bound").getNodeValue());
+			network.setDefaultBound(i);
+		}
+	}
+
+    private void parseFeature(Document doc, TimedArcPetriNetNetwork network) {
+        if (doc.getElementsByTagName("feature").getLength() > 0) {
+	        NodeList nodeList = doc.getElementsByTagName("feature");
+
+	        hasFeatureTag = true;
+
+            var isTimedElement = nodeList.item(0).getAttributes().getNamedItem("isTimed");
+            boolean isTimed = isTimedElement == null ? network.isTimed() : Boolean.parseBoolean(isTimedElement.getNodeValue());
+
+            var isGameElement = nodeList.item(0).getAttributes().getNamedItem("isGame");
+            boolean isGame = isGameElement == null ? network.hasUncontrollableTransitions() : Boolean.parseBoolean(isGameElement.getNodeValue());
+
+            var isColoredElement = nodeList.item(0).getAttributes().getNamedItem("isColored");
+            boolean isColored = isColoredElement == null ? network.isColored() : Boolean.parseBoolean(isColoredElement.getNodeValue());
+
+            lens = new TAPNLens(isTimed, isGame, isColored);
+        }
+    }
+
+    private void parseFeature(Document doc) {
+        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());
+            var isColored = Boolean.parseBoolean(nodeList.item(0).getAttributes().getNamedItem("isColored").getNodeValue());
+
+            lens = new TAPNLens(isTimed, isGame, isColored);
+        }
+    }
+
+	private void parseSharedPlaces(Document doc, TimedArcPetriNetNetwork network, ConstantStore constants) {
+		NodeList sharedPlaceNodes = doc.getElementsByTagName("shared-place");
+
+		for(int i = 0; i < sharedPlaceNodes.getLength(); i++){
+			Node node = sharedPlaceNodes.item(i);
+
+			if(node instanceof Element){
+				SharedPlace place = parseSharedPlace((Element)node, network, constants);
+				network.add(place);
+			}
+		}
+	}
+
+	private SharedPlace parseSharedPlace(Element element, TimedArcPetriNetNetwork network, ConstantStore constants) {
+		String name = element.getAttribute("name");
+		TimeInvariant invariant = TimeInvariant.parse(element.getAttribute("invariant"), constants);
+		//int numberOfTokens = Integer.parseInt(element.getAttribute("initialMarking"));
+
+		if(name.equalsIgnoreCase("true") || name.equalsIgnoreCase("false")) {
+			name = "_" + name;
+			if(firstPlaceRenameWarning) {
+				messages.add(PLACENAME_ERROR_MESSAGE);
+				firstPlaceRenameWarning = false;
+			}
+		}
+		SharedPlace place = new SharedPlace(name, invariant);
+        place.setCurrentMarking(network.marking());
+        place.setColorType(parsePlaceColorType(element));
+		//place.addTokens(numbesrOfTokens);
+        addColoredDependencies(place,element, network, constants);
+
+
+        return place;
+	}
+
+	private void parseSharedTransitions(Document doc, TimedArcPetriNetNetwork network) {
+		NodeList sharedTransitionNodes = doc.getElementsByTagName("shared-transition");
+
+		for(int i = 0; i < sharedTransitionNodes.getLength(); i++){
+			Node node = sharedTransitionNodes.item(i);
+
+			if(node instanceof Element){
+				SharedTransition transition = parseSharedTransition((Element)node);
+				network.add(transition);
+			}
+		}
+	}
+
+	private SharedTransition parseSharedTransition(Element element) {
+		String name = element.getAttribute("name");
+		boolean urgent = Boolean.parseBoolean(element.getAttribute("urgent"));
+        boolean isUncontrollable = element.getAttribute("player").equals("1");
+		
+		SharedTransition st = new SharedTransition(name);
+		st.setUrgent(urgent);
+		st.setUncontrollable(isUncontrollable);
+		return st;
+	}
+
+	private Collection<Template> parseTemplates(Document doc, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
+		Collection<Template> templates = new ArrayList<Template>();
+		NodeList nets = doc.getElementsByTagName("net");
+		
+		if(nets.getLength() <= 0)
+			throw new FormatException("File did not contain any TAPN components.");
+		
+		for (int i = 0; i < nets.getLength(); i++) {
+			Template template = parseTimedArcPetriNet(nets.item(i), network, constants);
+            template.setHasPositionalInfo(true); //We assume that all templates have positional info
+			templates.add(template);
+		}
+		return templates;
+	}
+
+	private List<Constant> parseConstants(Document doc) {
+		List<Constant> constants = new ArrayList<Constant>();
+		NodeList constantNodes = doc.getElementsByTagName("constant");
+		for (int i = 0; i < constantNodes.getLength(); i++) {
+			Node c = constantNodes.item(i);
+
+			if (c instanceof Element) {
+				Constant constant = parseConstant((Element) c);
+				constants.add(constant);
+			}
+		}
+		return constants;
+	}
+
+	private Template parseTimedArcPetriNet(Node tapnNode, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
+        String name = getTAPNName(tapnNode);
+
+		boolean active = getActiveStatus(tapnNode);
+
+		TimedArcPetriNet tapn = new TimedArcPetriNet(name);
+		tapn.setActive(active);
+		network.add(tapn);
+		nameGenerator.add(tapn);
+		
+		DataLayer guiModel = new DataLayer();
+		Template template = new Template(tapn, guiModel, new Zoomer());
+
+		NodeList nodeList = tapnNode.getChildNodes();
+		for (int i = 0; i < nodeList.getLength(); i++) {
+
+			Node node = nodeList.item(i);
+			if(node instanceof Element){
+				parseElement((Element)node, template, network, constants);
+			}
+		}
+
+		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;
+        }
+    }
+
+	private void parseElement(Element element, Template template, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
+		if ("labels".equals(element.getNodeName())) {
+			AnnotationNote note = parseAnnotation(element);
+			template.guiModel().addPetriNetObject(note);
+		} else if ("place".equals(element.getNodeName())) {
+			TimedPlaceComponent place = parsePlace(element, network, template.model(), constants);
+			template.guiModel().addPetriNetObject(place);
+		} else if ("transition".equals(element.getNodeName())) {
+			TimedTransitionComponent transition = parseTransition(element, network, template.model());
+			template.guiModel().addPetriNetObject(transition);
+		} else if (element.getNodeName().matches("arc|outputArc|inputArc|inhibitorArc|transportArc")) {
+            parseAndAddArc(element, template, constants, network);
+        }
+	}
+
+	private boolean isNameAllowed(String name) {
+		Require.that(name != null, "name was null");
+
+		return !name.isEmpty() && java.util.regex.Pattern.matches("[a-zA-Z]([_a-zA-Z0-9])*", name);
+	}
+
+
+	private String getTAPNName(Node tapnNode) {
+		if (tapnNode instanceof Element) {
+			Element element = (Element)tapnNode;
+			String name = element.getAttribute("name");
+
+			if (name == null || name.equals(""))
+				name = element.getAttribute("id");
+
+			if(!isNameAllowed(name)){
+				name = nameGenerator.getNewTemplateName();
+			}
+			nameGenerator.updateTemplateIndex(name);
+			return name;
+		} else {
+			return nameGenerator.getNewTemplateName();
+		}
+	}
+
+	private AnnotationNote parseAnnotation(Element annotation) {
+		int positionXInput = 0;
+		int positionYInput = 0;
+		int widthInput = 0;
+		int heightInput = 0;
+		boolean borderInput = true;
+
+		String positionXTempStorage = annotation.getAttribute("positionX");
+		String positionYTempStorage = annotation.getAttribute("positionY");
+		String widthTemp = annotation.getAttribute("width");
+		String heightTemp = annotation.getAttribute("height");
+		String borderTemp = annotation.getAttribute("border");
+
+		String text = annotation.getTextContent();
+
+		if (positionXTempStorage.length() > 0) {
+			positionXInput = Integer.parseInt(positionXTempStorage) + 1;
+		}
+
+		if (positionYTempStorage.length() > 0) {
+			positionYInput = Integer.parseInt(positionYTempStorage) + 1;
+		}
+
+		if (widthTemp.length() > 0) {
+			widthInput = Integer.parseInt(widthTemp) + 1;
+		}
+
+		if (heightTemp.length() > 0) {
+			heightInput = Integer.parseInt(heightTemp) + 1;
+		}
+
+		if (borderTemp.length() > 0) {
+			borderInput = Boolean.parseBoolean(borderTemp);
+		} else {
+			borderInput = true;
+		}
+        return new AnnotationNote(text, positionXInput, positionYInput, widthInput, heightInput, borderInput);
+	}
+
+	private TimedTransitionComponent parseTransition(Element transition, TimedArcPetriNetNetwork network, TimedArcPetriNet tapn) {
+		String posX = transition.getAttribute("positionX");
+		String posY = transition.getAttribute("positionY");
+		String nameOffsetX = transition.getAttribute("nameOffsetX");
+		String nameOffsetY = transition.getAttribute("nameOffsetY");
+		String angleStr = transition.getAttribute("angle");
+		String priorityStr = transition.getAttribute("priority");
+	    int positionXInput = 0;
+		int positionYInput = 0;
+		int nameOffsetXInput = 0;
+		int nameOffsetYInput = 0;
+		int angle = 0;
+        int priority = 0;
+		if(!posX.isEmpty()){
+		    positionXInput = (int)Double.parseDouble(posX);
+        }
+		if(!posY.isEmpty()){
+		    positionYInput = (int)Double.parseDouble(posY);
+        }
+
+        var g = transition.getElementsByTagName("position");
+        if (g.getLength() > 0) {
+            positionXInput = Integer.parseInt(((Element) g.item(0)).getAttribute("x"));
+            positionYInput = Integer.parseInt(((Element) g.item(0)).getAttribute("y"));
+        }
+
+		if(!nameOffsetX.isEmpty()){
+		    nameOffsetXInput = (int)Double.parseDouble(nameOffsetX);
+        }
+		if(!nameOffsetY.isEmpty()){
+		    nameOffsetYInput = (int)Double.parseDouble(nameOffsetY);
+        }
+		if(!angleStr.isEmpty()){
+		    angle = Integer.parseInt(angleStr);
+        }
+		if(!priorityStr.isEmpty()){
+		    priority = Integer.parseInt(priorityStr);
+        }
+		String idInput = transition.getAttribute("id");
+		String nameInput = transition.getAttribute("name");
+		boolean isUrgent = Boolean.parseBoolean(transition.getAttribute("urgent"));
+
+		String player = transition.getAttribute("player");
+
+		idResolver.add(tapn.name(), idInput, nameInput);
+
+		boolean infiniteServer = transition.getAttribute("infiniteServer").equals("true");
+
+		boolean displayName = transition.getAttribute("displayName").equals("false") ? false : true;
+
+
+		if (idInput.length() == 0 && nameInput.length() > 0) {
+			idInput = nameInput;
+		}
+
+		if (nameInput.length() == 0 && idInput.length() > 0) {
+			nameInput = idInput;
+		}
+        GuardExpression guardExpr = null;
+
+        Node conditionNode = getFirstDirectChild(transition, "condition");
+        if (conditionNode != null) {
+            try {
+                guardExpr = loadTACPN.parseGuardExpression(getFirstDirectChild(conditionNode, "structure"));
+            } catch (FormatException e) {
+                e.printStackTrace();
+            }
+        }
+		
+		TimedTransition t = new TimedTransition(nameInput, guardExpr);
+		t.setUrgent(isUrgent);
+		t.setUncontrollable(player.equals("1"));
+		if(network.isNameUsedForShared(nameInput)){
+			t.setName(nameGenerator.getNewTransitionName(tapn)); // introduce temporary name to avoid exceptions
+			tapn.add(t);
+			network.getSharedTransitionByName(nameInput).makeShared(t);
+		}else{
+			tapn.add(t);
+		}
+		nameGenerator.updateIndicesForAllModels(nameInput);
+		TimedTransitionComponent transitionComponent = new TimedTransitionComponent(
+				positionXInput, positionYInput, idInput,
+				nameOffsetXInput, nameOffsetYInput,
+            angle, lens);
+		transitionComponent.setUnderlyingTransition(t);
+		
+		if (!displayName){
+			transitionComponent.setAttributesVisible(false);
+		}
+		return transitionComponent;
+	}
+
+	private TimedPlaceComponent parsePlace(Element place, TimedArcPetriNetNetwork network, TimedArcPetriNet tapn, ConstantStore constants) {
+        String placePosX = place.getAttribute("positionX");
+        String placePosY = place.getAttribute("positionY");
+        String nameOffsetX = place.getAttribute("nameOffsetX");
+        String nameOffsetY = place.getAttribute("nameOffsetY");
+        int positionXInput = 0;
+        int positionYInput = 0;
+	    if(!placePosX.isBlank()){
+	        positionXInput = (int)Double.parseDouble(placePosX);
+        }
+	    if(!placePosY.isBlank()){
+            positionYInput = (int)Double.parseDouble(placePosY);
+        }
+
+        var g = place.getElementsByTagName("position");
+        if (g.getLength() > 0) {
+            positionXInput = Integer.parseInt(((Element) g.item(0)).getAttribute("x"));
+            positionYInput = Integer.parseInt(((Element) g.item(0)).getAttribute("y"));
+        }
+
+		String idInput = place.getAttribute("id");
+		String nameInput = place.getAttribute("name");
+
+		int nameOffsetXInput = 0;
+        int nameOffsetYInput = 0;
+		if(!nameOffsetX.isEmpty()){
+		    nameOffsetXInput = (int)Double.parseDouble(nameOffsetX);
+        }
+		if(!nameOffsetY.isEmpty()){
+		    nameOffsetYInput = (int)Double.parseDouble(nameOffsetY);
+        }
+
+		String invariant = place.getAttribute("invariant");
+		boolean displayName = place.getAttribute("displayName").equals("false") ? false : true;
+
+		if (idInput.length() == 0 && nameInput.length() > 0) {
+			idInput = nameInput;
+		}
+
+		if (nameInput.length() == 0 && idInput.length() > 0) {
+			nameInput = idInput;
+		}
+
+		if(nameInput.equalsIgnoreCase("true") || nameInput.equalsIgnoreCase("false")) {
+			nameInput = "_" + nameInput;
+			if(firstPlaceRenameWarning) {
+                messages.add(PLACENAME_ERROR_MESSAGE);
+				firstPlaceRenameWarning = false;
+			}
+		}
+
+		idResolver.add(tapn.name(), idInput, nameInput);
+
+		TimedPlace p;
+		if(network.isNameUsedForShared(nameInput)){
+			p = network.getSharedPlaceByName(nameInput);
+            tapn.add(p);
+		}else{
+		    p = new LocalTimedPlace(nameInput, TimeInvariant.parse(invariant, constants), parsePlaceColorType(place));
+		    tapn.add(p);
+		    addColoredDependencies(p,place, network, constants);
+
+		}
+		nameGenerator.updateIndicesForAllModels(nameInput);
+		TimedPlaceComponent placeComponent = new TimedPlaceComponent(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput, lens);
+		placeComponent.setUnderlyingPlace(p);
+
+		if (!displayName){
+			placeComponent.setAttributesVisible(false);
+		}
+
+        return placeComponent;
+	}
+
+	private ColorType parsePlaceColorType(Element element){
+        ColorType ct = ColorType.COLORTYPE_DOT;
+        Node typeNode = element.getElementsByTagName("type").item(0);
+        if (typeNode != null) {
+            try {
+                ct = loadTACPN.parseUserSort(typeNode);
+            } catch (FormatException e) {
+                e.printStackTrace();
+            }
+        }
+        return ct;
+    }
+
+	private void addColoredDependencies(TimedPlace p, Element place, TimedArcPetriNetNetwork network, ConstantStore constants){
+        List<ColoredTimeInvariant> ctiList = new ArrayList<ColoredTimeInvariant>();
+        int initialMarkingInput = Integer.parseInt(place.getAttribute("initialMarking"));
+
+        ArcExpression colorMarking = null;
+        NodeList nodes = place.getElementsByTagName("colorinvariant");
+        if (nodes != null) {
+            for (int i = 0; i < nodes.getLength(); i++) {
+                Pair<String, Vector<Color>> pair = parseColorInvariant((Element) nodes.item(i), network);
+                ColoredTimeInvariant cti = ColoredTimeInvariant.parse(pair.getFirst(), constants, pair.getSecond());
+                ctiList.add(cti);
+            }
+        }
+        if (place.getAttribute("inscription").length() > 0) {
+            ctiList.add(ColoredTimeInvariant.parse(place.getAttribute("inscription"), constants, new Vector<Color>() {{
+                add(Color.STAR_COLOR);
+            }}));
+        }
+        Node hlInitialMarkingNode = place.getElementsByTagName("hlinitialMarking").item(0);
+
+        if (hlInitialMarkingNode instanceof Element) {
+            try {
+                colorMarking = loadTACPN.parseArcExpression(((Element)hlInitialMarkingNode).getElementsByTagName("structure").item(0));
+            } catch (FormatException e) {
+                e.printStackTrace();
+            }
+        }
+
+
+	    p.setCtiList(ctiList);
+        ExpressionContext context = new ExpressionContext(new HashMap<String, Color>(), loadTACPN.getColortypes());
+        if(colorMarking!= null){
+            ColorMultiset cm = colorMarking.eval(context);
+
+            p.setTokenExpression(loadTACPN.constructCleanAddExpression(p.getColorType(),cm));
+
+
+            for (TimedToken ctElement : cm.getTokens(p)) {
+                network.marking().add(ctElement);
+                //p.addToken(ctElement);
+            }
+
+        } else {
+            for (int i = 0; i < initialMarkingInput; i++) {
+                //Regular tokens will just be dotconstant
+                network.marking().add(new TimedToken(p, ColorType.COLORTYPE_DOT.getFirstColor()));
+            }
+            if(initialMarkingInput > 1) {
+                Vector<ColorExpression> v = new Vector<>();
+                v.add(new DotConstantExpression());
+                Vector<ArcExpression> numbOfExpression = new Vector<>();
+                numbOfExpression.add(new NumberOfExpression(initialMarkingInput, v));
+                p.setTokenExpression(new AddExpression(numbOfExpression));
+            }
+        }
+    }
+
+	private void parseAndAddArc(Element arc, Template template, ConstantStore constants, TimedArcPetriNetNetwork network) throws FormatException {
+		String idInput = arc.getAttribute("id");
+		String sourceInput = arc.getAttribute("source");
+		String targetInput = arc.getAttribute("target");
+		boolean taggedArc = arc.getAttribute("tagged").equals("true") ? true : false;
+		String inscriptionTempStorage = arc.getAttribute("inscription");
+		String type = arc.getAttribute("type");
+		if(type.isEmpty()){
+            switch (arc.getNodeName()) {
+                case "transportArc":
+                    type = "transport";
+                    break;
+                case "inhibitorArc":
+                    type = "inhibitor";
+                    break;
+                case "inputArc":
+                    type = "timed";
+                    break;
+                default:
+                    type = "";
+                    break;
+            }
+        }
+		int nameOffsetXInput;
+		int nameOffsetYInput;
+		
+		//This check is done, as arcs in nets saved before this change do not have a nameOffset
+		if(!arc.getAttribute("nameOffsetX").equals("") && !arc.getAttribute("nameOffsetY").equals("")) {
+			nameOffsetXInput = (int) Double.parseDouble(arc.getAttribute("nameOffsetX"));
+			nameOffsetYInput = (int) Double.parseDouble(arc.getAttribute("nameOffsetY"));
+		} else {
+			nameOffsetXInput = 0;
+			nameOffsetYInput = 0;
+		}
+		
+		sourceInput = idResolver.get(template.model().name(), sourceInput);
+		targetInput = idResolver.get(template.model().name(), targetInput);
+		
+		PlaceTransitionObject sourceIn = template.guiModel().getPlaceTransitionObject(sourceInput);
+		PlaceTransitionObject targetIn = template.guiModel().getPlaceTransitionObject(targetInput);
+
+		// add the insets and offset
+		int _startx = sourceIn.getX() + sourceIn.centreOffsetLeft();
+		int _starty = sourceIn.getY() + sourceIn.centreOffsetTop();
+
+		int _endx = targetIn.getX() + targetIn.centreOffsetLeft();
+		int _endy = targetIn.getY() + targetIn.centreOffsetTop();
+
+		//Get weight if any
+		Weight weight = new IntWeight(1);
+		if(arc.hasAttribute("weight")){
+			weight = Weight.parseWeight(arc.getAttribute("weight"), constants);
+		}
+        ArcExpression arcExpr = null;
+        List<ColoredTimeInterval> ctiList = new ArrayList<ColoredTimeInterval>();
+        Node hlInscription = getFirstDirectChild(arc, "hlinscription");
+        if (hlInscription != null)
+            hlInscription = getFirstDirectChild(hlInscription, "structure");
+        if (hlInscription != null)
+            arcExpr = loadTACPN.parseArcExpression(hlInscription);
+
+        NodeList intervalNodes = arc.getElementsByTagName("colorinterval");
+        if (intervalNodes != null) {
+            for (int i = 0; i < intervalNodes.getLength(); i++) {
+                if (intervalNodes.item(i) instanceof  Element) {
+                    Element interval = (Element) intervalNodes.item(i);
+                    Pair<String, Vector<Color>> pair =  parseColorInvariant(interval, network);
+                    ColoredTimeInterval coloredinterval = ColoredTimeInterval.parse(pair.getFirst(), constants, pair.getSecond());
+                    ctiList.add(coloredinterval);
+                }
+            }
+        }
+
+		Arc tempArc;
+        Arc tempArc2 = null;
+
+		if (type.equals("tapnInhibitor") || type.equals("inhibitor")) {
+
+			tempArc = parseAndAddTimedInhibitorArc(idInput, taggedArc,
+					inscriptionTempStorage, sourceIn, targetIn,
+                _endx, _endy,template, constants, weight, arcExpr);
+
+		} else {
+			if (type.equals("timed")) {
+				tempArc = parseAndAddTimedInputArc(idInput, taggedArc,
+						inscriptionTempStorage, sourceIn, targetIn,
+                    _endx, _endy, template, constants, weight, ctiList, arcExpr);
+
+			} else if (type.equals("transport")) {
+                String transition = arc.getAttribute("transition");
+                if(transition.isEmpty()){
+                    tempArc = parseAndAddTransportArc(idInput, taggedArc,
+                        inscriptionTempStorage, sourceIn, targetIn,
+                        _endx, _endy, template, constants, weight, ctiList, arcExpr);
+                } else {
+                    transition = idResolver.get(template.model().name(), transition);
+                    PlaceTransitionObject transitionIn = template.guiModel().getPlaceTransitionObject(transition);
+
+                    tempArc = parseAndAddTransportArc(idInput, taggedArc,
+                        inscriptionTempStorage, sourceIn, transitionIn,
+                        _endx, _endy, template, constants, weight, ctiList, arcExpr);
+
+                    tempArc2 = parseAndAddTransportArc(idInput, taggedArc,
+                        inscriptionTempStorage, transitionIn, targetIn,
+                        _endx, _endy, template, constants, weight, ctiList, arcExpr);
+                }
+			} else {
+				tempArc = parseAndAddTimedOutputArc(idInput, taggedArc,
+						inscriptionTempStorage, sourceIn, targetIn,
+                    _endx, _endy, template, weight, arcExpr);
+			}
+
+		}
+		tempArc.setNameOffsetX(nameOffsetXInput);
+		tempArc.setNameOffsetY(nameOffsetYInput);
+
+		parseArcPath(arc, tempArc);
+		if(tempArc2 != null){
+            tempArc2.setNameOffsetX(nameOffsetXInput);
+            tempArc2.setNameOffsetY(nameOffsetYInput);
+
+            parseArcPath(arc, tempArc2);
+        }
+	}
+
+	private TimedOutputArcComponent parseAndAddTimedOutputArc(String idInput, boolean taggedArc,
+                                                              String inscriptionTempStorage, PlaceTransitionObject sourceIn,
+                                                              PlaceTransitionObject targetIn,
+                                                              int _endx, int _endy, Template template, Weight weight, ArcExpression expr) throws FormatException {
+
+		TimedOutputArcComponent tempArc = new TimedOutputArcComponent(sourceIn, targetIn,	(!inscriptionTempStorage.equals("") ? Integer.parseInt(inscriptionTempStorage) : 1), idInput);
+
+		TimedPlace place = template.model().getPlaceByName(targetIn.getName());
+		TimedTransition transition = template.model().getTransitionByName(sourceIn.getName());
+
+		TimedOutputArc outputArc = new TimedOutputArc(transition, place, weight, expr);
+		tempArc.setUnderlyingArc(outputArc);
+
+		if(template.model().hasArcFromTransitionToPlace(outputArc.source(),outputArc.destination())) {
+			throw new FormatException("Multiple arcs between a place and a transition is not allowed");
+		}
+
+		template.guiModel().addPetriNetObject(tempArc);
+		template.model().add(outputArc);
+
+		return tempArc;
+	}
+
+	private TimedTransportArcComponent parseAndAddTransportArc(String idInput, boolean taggedArc,
+                                                               String inscriptionTempStorage, PlaceTransitionObject sourceIn,
+                                                               PlaceTransitionObject targetIn,
+                                                               int _endx, int _endy, Template template, ConstantStore constants, Weight weight, List<ColoredTimeInterval> ctiList, ArcExpression expr) {
+
+		
+		String[] inscriptionSplit = {};
+		if (inscriptionTempStorage.contains(":")) {
+			inscriptionSplit = inscriptionTempStorage.split(":");
+		} else{
+		    inscriptionSplit = new String[]{inscriptionTempStorage};
+        }
+		boolean isInPreSet = false;
+		if (sourceIn instanceof Place) {
+			isInPreSet = true;
+		}
+
+		TimedTransportArcComponent tempArc = new TimedTransportArcComponent(new TimedInputArcComponent(new TimedOutputArcComponent(sourceIn, targetIn, 1, idInput)), -1, isInPreSet);
+
+
+		if (isInPreSet) {
+			if (postsetArcs.containsKey(targetIn)) {
+				TimedTransportArcComponent postsetTransportArc = postsetArcs.get(targetIn);
+				TimedPlace sourcePlace = template.model().getPlaceByName(sourceIn.getName());
+				TimedTransition trans = template.model().getTransitionByName(targetIn.getName());
+				TimedPlace destPlace = template.model().getPlaceByName(postsetTransportArc.getTarget().getName());
+
+                TimeInterval timeInterval = TimeInterval.parse(inscriptionSplit[0],	constants);
+
+				assert (sourcePlace != null);
+				assert (trans != null);
+				assert (destPlace != null);
+				int groupNr = 1;
+                if(inscriptionSplit.length < 2){
+                    for (Object pt : tempArc.getTarget().getPostset()) {
+                        if (pt instanceof TimedTransportArcComponent) {
+                            if (((TimedTransportArcComponent) pt).getGroupNr() > groupNr) {
+                                groupNr = ((TimedTransportArcComponent) pt).getGroupNr();
+                            }
+                        }
+                    }
+                } else {
+                    groupNr = Integer.parseInt(inscriptionSplit[1]);
+                }
+                tempArc.setGroupNr(groupNr);
+                postsetTransportArc.setGroupNr(groupNr);
+
+				TransportArc transArc = new TransportArc(sourcePlace, trans, destPlace, timeInterval, weight,expr,transportExpr);
+				transArc.setColorTimeIntervals(ctiList);
+
+				tempArc.setUnderlyingArc(transArc);
+				postsetTransportArc.setUnderlyingArc(transArc);
+				template.guiModel().addPetriNetObject(tempArc);
+				template.guiModel().addPetriNetObject(postsetTransportArc);
+				template.model().add(transArc);
+
+				postsetArcs.remove(targetIn);
+			} else {
+                transportExpr = expr;
+                presetArcs.put((TimedTransitionComponent) targetIn,	tempArc);
+				transportArcsTimeIntervals.put(tempArc, TimeInterval.parse(inscriptionSplit[0], constants));
+                coloredTransportArcsTimeIntervals.put(tempArc, ctiList);
+
+            }
+		} else {
+			if (presetArcs.containsKey(sourceIn)) {
+				TimedTransportArcComponent presetTransportArc = presetArcs.get(sourceIn);
+				TimedPlace sourcePlace = template.model().getPlaceByName(presetTransportArc.getSource().getName());
+				TimedTransition trans = template.model().getTransitionByName(sourceIn.getName());
+				TimedPlace destPlace = template.model().getPlaceByName(targetIn.getName());
+				TimeInterval interval = transportArcsTimeIntervals.get(presetTransportArc);
+                List<ColoredTimeInterval> timeIntervals = coloredTransportArcsTimeIntervals.get(presetTransportArc);
+
+                assert (sourcePlace != null);
+				assert (trans != null);
+				assert (destPlace != null);
+                int groupNr = 1;
+                if(inscriptionSplit.length < 2){
+                    for (Object pt : tempArc.getSource().getPostset()) {
+                        if (pt instanceof TimedTransportArcComponent) {
+                            if (((TimedTransportArcComponent) pt).getGroupNr() > groupNr) {
+                                groupNr = ((TimedTransportArcComponent) pt).getGroupNr();
+                            }
+                        }
+                    }
+                } else {
+                    groupNr = Integer.parseInt(inscriptionSplit[1]);
+                }
+                tempArc.setGroupNr(groupNr);
+                presetTransportArc.setGroupNr(groupNr);
+
+				TransportArc transArc = new TransportArc(sourcePlace, trans, destPlace, interval, weight,transportExpr,expr);
+				transArc.setColorTimeIntervals(timeIntervals);
+                transportExpr = null;
+
+				tempArc.setUnderlyingArc(transArc);
+				presetTransportArc.setUnderlyingArc(transArc);
+				template.guiModel().addPetriNetObject(presetTransportArc);
+				template.guiModel().addPetriNetObject(tempArc);
+				template.model().add(transArc);
+
+				presetArcs.remove(sourceIn);
+				transportArcsTimeIntervals.remove(presetTransportArc);
+			} else {
+				postsetArcs.put((TimedTransitionComponent) sourceIn, tempArc);
+				transportExpr = expr;
+			}
+		}
+		return tempArc;
+	}
+
+	private Arc parseAndAddTimedInputArc(String idInput, boolean taggedArc,
+                                         String inscriptionTempStorage, PlaceTransitionObject sourceIn,
+                                         PlaceTransitionObject targetIn,
+                                         int _endx, int _endy, Template template, ConstantStore constants, Weight weight,List<ColoredTimeInterval> ctiList, ArcExpression expr ) throws FormatException {
+        TimedInputArcComponent tempArc = new TimedInputArcComponent(new TimedOutputArcComponent(sourceIn, targetIn, 1, idInput), lens);
+
+
+
+
+		TimedPlace place = template.model().getPlaceByName(sourceIn.getName());
+		TimedTransition transition = template.model().getTransitionByName(targetIn.getName());
+
+		TimeInterval timeInterval = TimeInterval.parse(inscriptionTempStorage, constants);
+        //ctiList.add(ColoredTimeInterval.parse(inscriptionTempStorage, constants, new Vector<Color>(){{add(Color.STAR_COLOR);}}));
+
+
+        TimedInputArc inputArc = new TimedInputArc(place, transition, timeInterval, weight, expr);
+        inputArc.setColorTimeIntervals(ctiList);
+		tempArc.setUnderlyingArc(inputArc);
+
+		if(template.model().hasArcFromPlaceToTransition(inputArc.source(), inputArc.destination())) {
+			throw new FormatException("Multiple arcs between a place and a transition is not allowed");
+		}
+
+		template.guiModel().addPetriNetObject(tempArc);
+		template.model().add(inputArc);
+
+		return tempArc;
+	}
+
+	private Arc parseAndAddTimedInhibitorArc(String idInput, boolean taggedArc,
+                                             String inscriptionTempStorage, PlaceTransitionObject sourceIn,
+                                             PlaceTransitionObject targetIn,
+                                             int _endx, int _endy, Template template, ConstantStore constants, Weight weight, ArcExpression arcExpr) {
+		TimedPlace place = template.model().getPlaceByName(sourceIn.getName());
+		TimedTransition transition = template.model().getTransitionByName(targetIn.getName());
+		TimeInterval interval = TimeInterval.parse(inscriptionTempStorage, constants);
+		
+		if(!interval.equals(TimeInterval.ZERO_INF) && firstInhibitorIntervalWarning) {
+            messages.add("The chosen model contained inhibitor arcs with unsupported intervals.\n\nTAPAAL only supports inhibitor arcs with intervals [0,inf).\n\nAny other interval on inhibitor arcs will be replaced with [0,inf).");
+			firstInhibitorIntervalWarning = false;
+		}
+
+		TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, interval, weight, arcExpr);
+        TimedInhibitorArcComponent tempArc = new TimedInhibitorArcComponent((TimedPlaceComponent)sourceIn, (TimedTransitionComponent)targetIn, inhibArc);
+		tempArc.setUnderlyingArc(inhibArc);
+		template.guiModel().addPetriNetObject(tempArc);
+		template.model().add(inhibArc);
+
+		return tempArc;
+	}
+
+	private void parseArcPath(Element arc, Arc tempArc) {
+		NodeList nodelist = arc.getElementsByTagName("arcpath");
+		if (nodelist.getLength() > 0) {
+			tempArc.getArcPath().purgePathPoints();
+			for (int i = 0; i < nodelist.getLength(); i++) {
+				Node node = nodelist.item(i);
+				if (node instanceof Element) {
+					Element element = (Element) node;
+					if ("arcpath".equals(element.getNodeName())) {
+						String arcTempX = element.getAttribute("xCoord");
+						String arcTempY = element.getAttribute("yCoord");
+
+						// Wierd naming convention in pipe: this represents if
+						// the arc point is a curve point or not
+						String arcTempType = element.getAttribute("arcPointType");
+						double arcPointX = Double.parseDouble(arcTempX);
+						double arcPointY = Double.parseDouble(arcTempY);
+						arcPointX += Constants.ARC_CONTROL_POINT_CONSTANT + 1;
+						arcPointY += Constants.ARC_CONTROL_POINT_CONSTANT + 1;
+						boolean arcPointType = Boolean.parseBoolean(arcTempType);
+						tempArc.getArcPath().addPoint(arcPointX, arcPointY,	arcPointType);
+					}
+				}
+			}
+		}
+	}
+
+	private Constant parseConstant(Element constantElement) {
+		String name = constantElement.getAttribute("name");
+		int value = Integer.parseInt(constantElement.getAttribute("value"));
+
+		return new Constant(name, value);
+	}
+
+    private Pair<String, Vector<Color>> parseColorInvariant(Element colorinvariant, TimedArcPetriNetNetwork network)  {
+        String inscription, colorTypeName;
+        Vector<Color> colors = new Vector<Color>();
+        Element colorTypeELe = (Element) colorinvariant.getElementsByTagName("colortype").item(0);
+        inscription = colorinvariant.getElementsByTagName("inscription").item(0).getAttributes().getNamedItem("inscription").getNodeValue();
+        colorTypeName = colorTypeELe.getAttributes().getNamedItem("name").getNodeValue();
+        if (network.isNameUsedForColorType(colorTypeName)) {
+            NodeList colorNodeList = colorTypeELe.getElementsByTagName("color");
+            String colorName;
+            ColorType ct = network.getColorTypeByName(colorTypeName);
+            for (int i = 0; i < colorNodeList.getLength(); i++) {
+                colorName = colorNodeList.item(i).getAttributes().getNamedItem("value").getNodeValue();
+                colors.add(new Color(ct, 0, colorName));
+            }
+        } else {
+            try {
+                throw new FormatException("The color type used for an invariant does not exist");
+            } catch (FormatException e) {
+                e.printStackTrace();
+            }
+        }
+
+        Pair<String, Vector<Color>> pair = new Pair<String, Vector<Color>>(inscription, colors);
+        return pair;
+    }
+
+    Node getFirstDirectChild(Node parent, String tagName){
+        NodeList children = parent.getChildNodes();
+        for(int i = 0; i < children.getLength(); i++){
+            if(children.item(i).getNodeName().equals(tagName)){
+                return children.item(i);
+            }
+        }
+        return null;
+    }
+
+}

=== modified file 'src/dk/aau/cs/io/TapnLegacyXmlLoader.java'
--- src/dk/aau/cs/io/TapnLegacyXmlLoader.java	2020-08-26 12:29:25 +0000
+++ src/dk/aau/cs/io/TapnLegacyXmlLoader.java	2022-03-21 20:20:44 +0000
@@ -8,43 +8,42 @@
 import java.util.Collection;
 import java.util.HashMap;
 
-import javax.swing.JOptionPane;
 import javax.xml.parsers.DocumentBuilder;
 import javax.xml.parsers.DocumentBuilderFactory;
 import javax.xml.parsers.ParserConfigurationException;
 
-import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.model.CPN.ColorType;
+import net.tapaal.gui.petrinet.TAPNLens;
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
 import org.w3c.dom.Node;
 import org.w3c.dom.NodeList;
 import org.xml.sax.SAXException;
-import pipe.dataLayer.TAPNQuery;
-import pipe.dataLayer.TAPNQuery.ExtrapolationOption;
-import pipe.dataLayer.TAPNQuery.HashTableSize;
-import pipe.dataLayer.TAPNQuery.SearchOption;
-import pipe.dataLayer.TAPNQuery.TraceOption;
-import pipe.dataLayer.DataLayer;
-import pipe.dataLayer.Template;
-import pipe.gui.CreateGui;
-import pipe.gui.Pipe;
-import pipe.gui.Zoomer;
-import pipe.gui.graphicElements.AnnotationNote;
-import pipe.gui.graphicElements.Arc;
-import pipe.gui.graphicElements.Place;
-import pipe.gui.graphicElements.PlaceTransitionObject;
-import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
-import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
-import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
-import pipe.gui.graphicElements.tapn.TimedTransportArcComponent;
-import pipe.gui.widgets.InclusionPlaces;
+import net.tapaal.gui.petrinet.verification.TAPNQuery;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.ExtrapolationOption;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.HashTableSize;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
+import pipe.gui.petrinet.dataLayer.DataLayer;
+import net.tapaal.gui.petrinet.Template;
+import pipe.gui.Constants;
+import pipe.gui.canvas.Zoomer;
+import pipe.gui.petrinet.graphicElements.AnnotationNote;
+import pipe.gui.petrinet.graphicElements.Arc;
+import pipe.gui.petrinet.graphicElements.Place;
+import pipe.gui.petrinet.graphicElements.PlaceTransitionObject;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedOutputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedTransitionComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedTransportArcComponent;
+import net.tapaal.gui.petrinet.verification.InclusionPlaces;
 import dk.aau.cs.TCTL.TCTLAbstractProperty;
 import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser;
 import dk.aau.cs.TCTL.visitors.AddTemplateVisitor;
 import dk.aau.cs.TCTL.visitors.VerifyPlaceNamesVisitor;
-import dk.aau.cs.gui.NameGenerator;
+import net.tapaal.gui.petrinet.NameGenerator;
 import dk.aau.cs.model.tapn.Constant;
 import dk.aau.cs.model.tapn.ConstantStore;
 import dk.aau.cs.model.tapn.LocalTimedPlace;
@@ -82,9 +81,8 @@
 	private boolean firstInhibitorIntervalWarning = true;
 	private boolean firstPlaceRenameWarning = true;
 	private final IdResolver idResolver = new IdResolver();
-
     private final Collection<String> messages = new ArrayList<>(10);
-    private final TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
+    private final TAPNLens lens = TAPNLens.Default;
 
 
     public TapnLegacyXmlLoader() {}
@@ -136,7 +134,7 @@
 			}
 		}
 
-		TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(constants);
+		TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(constants, new ArrayList<>());
 		NodeList nets = tapnDoc.getElementsByTagName("net");
 		
 		if(nets.getLength() <= 0)
@@ -318,7 +316,7 @@
 			firstInhibitorIntervalWarning = false;
 		}
 		
-		TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, interval);
+		TimedInhibitorArc inhibArc = new TimedInhibitorArc(place, transition, interval,null);
 
 		tempArc.setUnderlyingArc(inhibArc);
 		guiModel.addPetriNetObject(tempArc);
@@ -430,23 +428,29 @@
 		Element element;
 		if (node instanceof Element) {
 			element = (Element) node;
-			if ("labels".equals(element.getNodeName())) {
-				parseAndAddAnnotationAsOldFormat(element);
-			} else if ("place".equals(element.getNodeName())) {
-				parseAndAddPlaceAsOldFormat(element, marking);
-			} else if ("transition".equals(element.getNodeName())) {
-				parseAndAddTransitionAsOldFormat(element);
-			} else if ("arc".equals(element.getNodeName())) {
-				parseAndAddArcAsOldFormat(element);
-			} else if ("queries".equals(element.getNodeName())) {
-				TAPNQuery query = parseQueryAsOldFormat(element);
-				
-				
-				if (query != null) {
-					query.getProperty().accept(new AddTemplateVisitor(templateName), null);
-					queries.add(query);
-				}
-			}
+            switch (element.getNodeName()) {
+                case "labels":
+                    parseAndAddAnnotationAsOldFormat(element);
+                    break;
+                case "place":
+                    parseAndAddPlaceAsOldFormat(element, marking);
+                    break;
+                case "transition":
+                    parseAndAddTransitionAsOldFormat(element);
+                    break;
+                case "arc":
+                    parseAndAddArcAsOldFormat(element);
+                    break;
+                case "queries":
+                    TAPNQuery query = parseQueryAsOldFormat(element);
+
+
+                    if (query != null) {
+                        query.getProperty().accept(new AddTemplateVisitor(templateName), null);
+                        queries.add(query);
+                    }
+                    break;
+            }
 		}
 	}
 
@@ -524,13 +528,13 @@
 
 		TimedTransitionComponent transition = new TimedTransitionComponent(
 				positionXInput, positionYInput, idInput,
-				nameOffsetXInput, nameOffsetYInput, timedTransition,
-				infiniteServer, angle, priority, lens);
+				nameOffsetXInput, nameOffsetYInput,
+            angle, lens);
 		transition.setUnderlyingTransition(t);
 		guiModel.addPetriNetObject(transition);
 		tapn.add(t);
 	}
-
+    //TODO: implement color
     private void parseAndAddPlaceAsOldFormat(Element element, TimedMarking marking) throws FormatException {
         int positionXInput = (int) getPositionAttribute(element, "x");
         int positionYInput = (int) getPositionAttribute(element, "y");
@@ -549,7 +553,7 @@
             nameInput = idInput;
         }
 
-        if (nameInput.toLowerCase().equals("true") || nameInput.toLowerCase().equals("false")) {
+        if (nameInput.equalsIgnoreCase("true") || nameInput.equalsIgnoreCase("false")) {
             nameInput = "_" + nameInput;
             if (firstPlaceRenameWarning) {
                 messages.add(PLACENAME_ERROR_MESSAGE);
@@ -560,14 +564,14 @@
 
         TimedPlaceComponent place = new TimedPlaceComponent(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput, lens);
 
-        LocalTimedPlace p = new LocalTimedPlace(nameInput, TimeInvariant.parse(invariant, constants));
+        LocalTimedPlace p = new LocalTimedPlace(nameInput, TimeInvariant.parse(invariant, constants), ColorType.COLORTYPE_DOT);
         tapn.add(p);
 
         place.setUnderlyingPlace(p);
         guiModel.addPetriNetObject(place);
 
         for (int i = 0; i < initialMarkingInput; i++) {
-            marking.add(new TimedToken(p, new BigDecimal(0.0)));
+            marking.add(new TimedToken(p, new BigDecimal(0.0), ColorType.COLORTYPE_DOT.getFirstColor()));
         }
     }
 
@@ -651,8 +655,8 @@
 						String arcTempType = element.getAttribute("curvePoint");
 						double arcPointX = Double.parseDouble(arcTempX);
 						double arcPointY = Double.parseDouble(arcTempY);
-						arcPointX += Pipe.ARC_CONTROL_POINT_CONSTANT + 1;
-						arcPointY += Pipe.ARC_CONTROL_POINT_CONSTANT + 1;
+						arcPointX += Constants.ARC_CONTROL_POINT_CONSTANT + 1;
+						arcPointY += Constants.ARC_CONTROL_POINT_CONSTANT + 1;
 						boolean arcPointType = Boolean.parseBoolean(arcTempType);
 						tempArc.getArcPath().addPoint(arcPointX, arcPointY,	arcPointType);
 					}
@@ -683,7 +687,7 @@
 		if (query != null) {
 			TAPNQuery parsedQuery = new TAPNQuery(comment, capacity, query, traceOption,
 					searchOption, reductionOption, symmetry, true, true, true, false, false, hashTableSize,
-					extrapolationOption,inclusionPlaces);
+					extrapolationOption,inclusionPlaces, lens.isColored());
 			parsedQuery.setActive(active);
 			parsedQuery.setDiscreteInclusion(discreteInclusion);
 			return parsedQuery;

=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
--- src/dk/aau/cs/io/TapnXmlLoader.java	2021-10-21 10:21:25 +0000
+++ src/dk/aau/cs/io/TapnXmlLoader.java	2022-03-21 20:20:44 +0000
@@ -3,38 +3,34 @@
 import java.io.File;
 import java.io.IOException;
 import java.io.InputStream;
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.HashMap;
-import java.util.List;
+import java.util.*;
 
-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 dk.aau.cs.gui.TabContent;
-import org.w3c.dom.Document;
-import org.w3c.dom.Element;
-import org.w3c.dom.Node;
-import org.w3c.dom.NodeList;
+import dk.aau.cs.model.CPN.*;
+import dk.aau.cs.model.CPN.Expressions.*;
+import kotlin.Pair;
+import net.tapaal.gui.petrinet.TAPNLens;
+import org.w3c.dom.*;
 import org.xml.sax.SAXException;
 
-import pipe.dataLayer.TAPNQuery;
-import pipe.dataLayer.DataLayer;
-import pipe.dataLayer.Template;
-import pipe.gui.CreateGui;
-import pipe.gui.Pipe;
-import pipe.gui.Zoomer;
-import pipe.gui.graphicElements.*;
-import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
-import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
-import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
-import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
-import pipe.gui.graphicElements.tapn.TimedTransportArcComponent;
-import dk.aau.cs.gui.NameGenerator;
+import pipe.gui.petrinet.dataLayer.DataLayer;
+import net.tapaal.gui.petrinet.Template;
+import pipe.gui.Constants;
+import pipe.gui.canvas.Zoomer;
+import pipe.gui.petrinet.graphicElements.AnnotationNote;
+import pipe.gui.petrinet.graphicElements.Arc;
+import pipe.gui.petrinet.graphicElements.Place;
+import pipe.gui.petrinet.graphicElements.PlaceTransitionObject;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInhibitorArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedInputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedOutputArcComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedPlaceComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedTransitionComponent;
+import pipe.gui.petrinet.graphicElements.tapn.TimedTransportArcComponent;
+import net.tapaal.gui.petrinet.NameGenerator;
 import dk.aau.cs.io.queries.TAPNQueryLoader;
 import dk.aau.cs.model.tapn.Constant;
 import dk.aau.cs.model.tapn.ConstantStore;
@@ -48,7 +44,6 @@
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 import dk.aau.cs.model.tapn.TimedInhibitorArc;
 import dk.aau.cs.model.tapn.TimedInputArc;
-import dk.aau.cs.model.tapn.TimedMarking;
 import dk.aau.cs.model.tapn.TimedOutputArc;
 import dk.aau.cs.model.tapn.TimedPlace;
 import dk.aau.cs.model.tapn.TimedToken;
@@ -64,21 +59,24 @@
 	private final HashMap<TimedTransitionComponent, TimedTransportArcComponent> presetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
 	private final HashMap<TimedTransitionComponent, TimedTransportArcComponent> postsetArcs = new HashMap<TimedTransitionComponent, TimedTransportArcComponent>();
 	private final HashMap<TimedTransportArcComponent, TimeInterval> transportArcsTimeIntervals = new HashMap<TimedTransportArcComponent, TimeInterval>();
+    private final HashMap<TimedTransportArcComponent, List<ColoredTimeInterval>> coloredTransportArcsTimeIntervals = new HashMap<TimedTransportArcComponent, List<ColoredTimeInterval>>();
+    private ArcExpression transportExpr;
 
-	private final NameGenerator nameGenerator = new NameGenerator();
+    private final NameGenerator nameGenerator = new NameGenerator();
 	private boolean firstInhibitorIntervalWarning = true;
 	private boolean firstPlaceRenameWarning = true;
 	private final IdResolver idResolver = new IdResolver();
     private final Collection<String> messages = new ArrayList<>(10);
-
+    int groupPlaceHolder = 1;
+    private final LoadTACPN loadTACPN = new LoadTACPN();
     boolean hasFeatureTag = false;
-    private TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
+    private TAPNLens lens = TAPNLens.Default;
 
 	public TapnXmlLoader() {
 
 	}
 
-    public TabContent.TAPNLens loadLens(InputStream file) throws FormatException {
+    public TAPNLens loadLens(InputStream file) throws FormatException {
         Require.that(file != null, "file must be non-null and exist");
 
         Document doc = loadDocument(file);
@@ -103,7 +101,7 @@
         } catch (FormatException | NullPointerException e) {
             throw e;
         } catch (Exception e) {
-            throw new Exception("One or more necessary attributes were not found\n  - One or more attribute values have an incorrect type");
+            throw new Exception("One or more necessary attributes were not found\n  - One or more attribute values have an incorrect type", e);
         }
 	}
 	
@@ -143,12 +141,26 @@
 	private LoadedModel parse(Document doc) throws FormatException {
 		idResolver.clear();
 
-        parseFeature(doc);
-		
+
 		ConstantStore constants = new ConstantStore(parseConstants(doc));
-
-		TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(constants);
-
+		TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(constants, new ArrayList<>());
+        NodeList declarations = doc.getElementsByTagName("declaration");
+
+        if (declarations.getLength() > 0) {