Merge lp:~tapaal-contributor/tapaal/cpn-gui-dev into lp:tapaal

[Kenneth Yrke Jørgensen]

Proposal of complete colored GUI including: Colortypes, variables, arc expression and colored arc intervals menu, guard expression menu, place and colored invariant menu, verification of colored nets and unfolding of colored nets.

To use all the features described in: https://docs.google.com/document/d/1SdUufTr0giizD-ZJ7BH0rcke-QQ-tp2MXfqb4c18sV8/edit

you will need verifydtapn with colors: https://github.com/TAPAAL-Developers/verifydtapn/tree/unfoldColor (PR: https://github.com/TAPAAL/verifydtapn/pull/10)
(Org branched from https://github.com/PeterHaahrTaankvist/verifydtapn/tree/unfolding_library)

and verifypn with colors: https://code.launchpad.net/~tapaal-contributor/verifypn/update-parser

I added a milestone for specifically to track bugs, so that we can keep the log in the pull request for code specific changes.

When creating a new bug related to the CPN branch, select the milestone TAPAAL CPN, this way we can easly filter bugs related to the branch, use this link: https://bugs.launchpad.net/tapaal/+bugs?field.searchtext=&orderby=-importance&field.status%3Alist=NEW&field.status%3Alist=CONFIRMED&field.status%3Alist=TRIAGED&field.status%3Alist=INPROGRESS&field.status%3Alist=FIXCOMMITTED&field.status%3Alist=INCOMPLETE_WITH_RESPONSE&field.status%3Alist=INCOMPLETE_WITHOUT_RESPONSE&assignee_option=any&field.assignee=&field.bug_reporter=&field.bug_commenter=&field.subscriber=&field.structural_subscriber=&field.milestone%3Alist=93479&field.tag=&field.tags_combinator=ANY&field.has_cve.used=&field.omit_dupes.used=&field.omit_dupes=on&field.affects_me.used=&field.has_patch.used=&field.has_branches.used=&field.has_branches=on&field.has_no_branches.used=&field.has_no_branches=on&field.has_blueprints.used=&field.has_blueprints=on&field.has_no_blueprints.used=&field.has_no_blueprints=on&search=Search

[Kenneth Yrke Jørgensen (yrke)]

All code only comments should be removed, unless it directly relates to something being explained.
Or if used for specialized debug. If for debug, please mark the beginning of block with DEBUG.

Internal members not mutated should be marked final.

(I will make a patch that fixes these to issues)

[Kenneth Yrke Jørgensen (yrke)]

File: ColoredArcGuardPanel.java
Function deleteSelections(), line 752

This "if" seems to have an flow error:

if (currentSelection.getObject() instanceof ArcExpression) {
    replacement = getSpecificChildOfProperty(1, currentSelection.getObject());
}
else if (currentSelection.getObject() instanceof ArcExpression) {
    replacement = new PlaceHolderColorExpression();
}

Second branch can't be reached, as it has the same guad as first branch. This must be a logical error.

[Kenneth Yrke Jørgensen (yrke)]

I noticed there seem to be a lot of TODO comments related to how colors should be handled.
I guess theses should all be adresse and can be removed safely?

If we leave in TODO comments for stuff that is already implemented or adresse elsewhere it can lead to confusion when we later revisit the code, as it might not be clear that the TODO comment is handled.

Intellij has a feature to list all todo/fixme etc. If there really is a todo, please add details about what is missing.

[Kenneth Yrke Jørgensen (yrke)]

It seems some shortcuts are updated, please remember to update documentation: https://github.com/TAPAAL/TAPAAL/wiki/Shortcut-keys

[Kenneth Yrke Jørgensen (yrke)]

I added a few more test to test out the api for new colors. I found a few problems in the interal consistency. Could you please have a look at this.

[lp:~tapaal-contributor/tapaal/cpn-gui-dev]

1625. By Jiri Srba on 2022-03-20

added explanation which color type cannot be removed (in case of multiple color type removal)

1626. By Kenneth Yrke Jørgensen on 2022-03-21

Potential fix for issue #1964937

Allow filter to be blank for selecting executable files in linux and macos

1627. By Jiri Srba on 2022-03-21

merged in lp:~tapaal-contributor/tapaal/cpn-remove-add fixing the transition guard dialog

1628. By Kenneth Yrke Jørgensen on 2022-03-22

Fixed bug #1964937

Iteration over a list that would be removed in the step above (list are references)

1629. By Lena Ernstsen on 2022-03-23

Fixed arc guard dialog not being able to display product colors

1630. By Lena Ernstsen on 2022-03-23

Fixed tuple selection problem in transition guard dialog

1631. By Lena Ernstsen on 2022-03-28

Fixed infinite loop when updating the color of an arc expression

1632. By Kenneth Yrke Jørgensen on 2022-03-29

Moved src files to gradle java project structure

1633. By Kenneth Yrke Jørgensen on 2022-03-31

Fixed what seems to be a logical error in selecting exporter

1634. By Kenneth Yrke Jørgensen on 2022-03-31

Fixed an issue where A E quantifiers would not show trace

1635. By Kenneth Yrke Jørgensen on 2022-04-02

Code cleanup

1636. By Kenneth Yrke Jørgensen on 2022-04-10

Fix for issue 1968474 Keep query cat when unfolding

1637. By Kenneth Yrke Jørgensen on 2022-04-10

Fixes #1968473, wrong filter applied in engine selection menu on windows

1638. By Kenneth Yrke Jørgensen on 2022-05-08

Fixed #1971420 unfolding empty net leads to error

It seems the unfolder genreates a dummy query to not have a empty list,
that query uses to reference the first templates first place, (which might not exist eg. net empty).
Insted change the dummy query to be E<>true.

1639. By Kenneth Yrke Jørgensen on 2022-05-08

Workarround for #1971422, need to make a propper fix later

1640. By Kenneth Yrke Jørgensen on 2022-05-15

Fixed a possible NPE

1641. By Jiri Srba on 2022-05-24

merged in lp:~tapaal-contributor/tapaal/conjunction-button-fix fixing a problem with and/or buttons in query dialog

1642. By Jiri Srba on 2022-05-24

merged in lp:~tapaal-contributor/tapaal/fix-product-display-1971421 fixing product colors editing in transitions guards

1643. By Kenneth Yrke Jørgensen on 2022-05-27

Added null check

1644. By Kenneth Yrke Jørgensen on 2022-05-27

refixed #1940418 via workarround

1645. By Jiri Srba on 2022-06-03

merged with trunk (fixing copying of components with environemnatl transitions)

1646. By Jiri Srba on 2022-06-03

merged with trunk (fixing editing of LTL queries)

1647. By Kenneth Yrke Jørgensen on 2022-06-20

Fixed long line error messages

1648. By Kenneth Yrke Jørgensen on 2022-06-20

Fixed an issue where shared transiations was "added" double due to parent network being reused when flatting net

1649. By Kenneth Yrke Jørgensen on 2022-07-11

Upgraded project dependency, removed junit4

1650. By Kenneth Yrke Jørgensen on 2022-07-21

Added support for opening files by dragging then on the canvas

=== modified file 'build.gradle'
--- build.gradle	2021-08-11 11:19:19 +0000
+++ build.gradle	2022-07-21 13:30:11 +0000
@@ -1,94 +1,70 @@
 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 {
         java {
-            srcDirs = ['src/', compileJavacc.outputDirectory]
-            exclude("resources/")
-        }
-        resources {
-            //Resources should be in folder called resources, so only add the resources folder
-            //adding srv/resources will places content of the folder in root of jar file
-            srcDirs = ['src/']
-            include("resources/")
-        }
-        test {
-            java {
-                srcDirs = ['tests/']
-            }
+            srcDir compileJavacc.outputDirectory
         }
     }
 }
 
-mainClassName = 'TAPAAL'
-
 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: '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
-
-    //Add jars from libs dir
-    implementation fileTree(dir: 'libs', include: ['*.jar'])
-
-    //Junit
-    testImplementation(
-        'org.junit.jupiter:junit-jupiter-api:5.4.2'
-    )
-    testRuntimeOnly(
-        'org.junit.jupiter:junit-jupiter-engine:5.4.2',
-        'org.junit.vintage:junit-vintage-engine:5.4.2'
-    )
-    implementation "org.jetbrains.kotlin:kotlin-stdlib-jdk8"
+    implementation 'commons-cli:commons-cli:1.5.0'
+    implementation 'org.swinglabs.swingx:swingx-all:1.6.5-1'
+    implementation 'net.java.dev.jna:jna:5.11.0'
+    implementation 'org.jetbrains:annotations:23.0.0'
+    implementation 'org.jetbrains.kotlinx:kotlinx-serialization-json:1.3.3'
+
+    testImplementation 'org.junit.jupiter:junit-jupiter-api:5.8.2'
+    testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.8.2'
 }
+
 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-07-21 13:30:11 +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-07-21 13:30:11 +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-07-21 13:30:11 +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

=== 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'
=== removed file 'src/dk/aau/cs/util/ExecutabilityChecker.java'
--- src/dk/aau/cs/util/ExecutabilityChecker.java	2016-03-16 18:05:19 +0000
+++ src/dk/aau/cs/util/ExecutabilityChecker.java	1970-01-01 00:00:00 +0000
@@ -1,42 +0,0 @@
-package dk.aau.cs.util;
-
-import java.io.BufferedReader;
-import java.io.InputStream;
-import java.io.InputStreamReader;
-
-public class ExecutabilityChecker {
-	public static void check(String path) throws IllegalArgumentException{
-		int rcode = -1;
-		try {
-			Process p = Runtime.getRuntime().exec(new String[] { path, "-v" });
-			
-			// Because some native platforms only provide limited buffer size 
-			// for standard input and output streams, failure to promptly write 
-			// the input stream or read the output stream of the subprocess may 
-			// cause the subprocess to block, and even deadlock.
-			
-			InputStream stream = p.getInputStream();
-            InputStreamReader isr = new InputStreamReader(stream);
-            BufferedReader br = new BufferedReader(isr);
-            while (br.readLine() != null){}
-            
-            stream = p.getErrorStream();
-            isr = new InputStreamReader(stream);
-            br = new BufferedReader(isr);
-            while (br.readLine() != null){}
-            
-			rcode = p.waitFor();	// Requires binary to accept -v flag
-		} catch (Exception e) {
-			// Do nothing
-		}
-		// Detect executable issues
-		switch(rcode){
-		case 0:
-			break;
-		case 126:
-			throw new IllegalArgumentException("The selected file is not executable on this system.");
-		default:
-			throw new IllegalArgumentException("The selected file is not executable or not compatible with your system (return value "+rcode+").");
-		}
-	}
-}
\ No newline at end of file

=== added directory 'src/main'
=== added directory 'src/main/java'
=== renamed file 'src/TAPAAL.java' => 'src/main/java/TAPAAL.java'
=== renamed directory 'src/dk' => 'src/main/java/dk'
=== modified file 'src/main/java/dk/aau/cs/TCTL/AritmeticOperator.java'
--- src/dk/aau/cs/TCTL/AritmeticOperator.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/AritmeticOperator.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/LTLGNode.java'
--- src/dk/aau/cs/TCTL/LTLGNode.java	2021-10-08 06:26:14 +0000
+++ src/main/java/dk/aau/cs/TCTL/LTLGNode.java	2022-07-21 13:30:11 +0000
@@ -20,7 +20,7 @@
     }
 
     public LTLGNode() {
-        this.property = new TCTLStatePlaceHolder();;
+        this.property = new TCTLStatePlaceHolder();
         this.property.setParent(this);
     }
 

=== modified file 'src/main/java/dk/aau/cs/TCTL/LTLUNode.java'
--- src/dk/aau/cs/TCTL/LTLUNode.java	2021-10-08 06:26:14 +0000
+++ src/main/java/dk/aau/cs/TCTL/LTLUNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/StringPosition.java'
--- src/dk/aau/cs/TCTL/StringPosition.java	2011-02-03 19:03:15 +0000
+++ src/main/java/dk/aau/cs/TCTL/StringPosition.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLAUNode.java'
--- src/dk/aau/cs/TCTL/TCTLAUNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLAUNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLAbstractProperty.java'
--- src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2021-08-16 07:29:37 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLAbstractStateProperty.java'
--- src/dk/aau/cs/TCTL/TCTLAbstractStateProperty.java	2011-02-03 19:03:15 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLAbstractStateProperty.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLAndListNode.java'
--- src/dk/aau/cs/TCTL/TCTLAndListNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLAndListNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java'
--- src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLConstNode.java'
--- src/dk/aau/cs/TCTL/TCTLConstNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLConstNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLEFNode.java'
--- src/dk/aau/cs/TCTL/TCTLEFNode.java	2021-09-14 20:13:01 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLEFNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLOrListNode.java'
--- src/dk/aau/cs/TCTL/TCTLOrListNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLOrListNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLPlusListNode.java'
--- src/dk/aau/cs/TCTL/TCTLPlusListNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLPlusListNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/TCTLTermListNode.java'
--- src/dk/aau/cs/TCTL/TCTLTermListNode.java	2020-11-06 19:41:50 +0000
+++ src/main/java/dk/aau/cs/TCTL/TCTLTermListNode.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java'
--- src/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java	2017-05-14 19:42:09 +0000
+++ src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/AddTemplateVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/AddTemplateVisitor.java	2014-05-22 20:26:41 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/AddTemplateVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/BroadcastTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/BroadcastTranslationQueryVisitor.java	2019-03-22 10:13:18 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/BroadcastTranslationQueryVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java	2021-10-08 06:22:05 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java	2022-07-21 13:30:11 +0000
@@ -1,271 +1,288 @@
 package dk.aau.cs.TCTL.visitors;
 
-import java.util.List;
-
 import dk.aau.cs.TCTL.*;
 import dk.aau.cs.io.XMLFormatter;
 
+import java.util.List;
+
 public class CTLQueryVisitor extends VisitorBase {
-	
-	private static final String XML_NS 			= "xmlns=\"http://tapaal.net/\"";
-	private static final String XML_PROPSET 		= "property-set";
-	private static final String XML_PROP			= "property";
-	private static final String XML_PROPID			= "id";
-	private static final String XML_PROPDESC		= "description";
-	private static final String XML_FORMULA			= "formula";	
-	private static final String XML_ALLPATHS		= "all-paths";
-	private static final String XML_EXISTSPATH	 	= "exists-path";
-	private static final String XML_NEGATION		= "negation";
-	private static final String XML_CONJUNCTION 		= "conjunction";
-	private static final String XML_DISJUNCTION 		= "disjunction";
-	private static final String XML_GLOBALLY		= "globally";
-	private static final String XML_FINALLY			= "finally";
-	private static final String XML_NEXT			= "next";
-	private static final String XML_UNTIL 			= "until";
-	private static final String XML_BEFORE 			= "before";
-	private static final String XML_REACH 			= "reach";
-	private static final String XML_DEADLOCK 		= "deadlock";
-	private static final String XML_TRUE 			= "true";
-	private static final String XML_FALSE 			= "false";
-	private static final String XML_INTEGERLT 		= "integer-lt";
-	private static final String XML_INTEGERLE 		= "integer-le";
-	private static final String XML_INTEGEREQ		= "integer-eq";
-	private static final String XML_INTEGERNE 		= "integer-ne";
-	private static final String XML_INTEGERGT 		= "integer-gt";
-	private static final String XML_INTEGERGE               = "integer-ge";
-	private static final String XML_ISFIREABLE		= "is-fireable";
-	private static final String XML_INTEGERCONSTANT 	= "integer-constant";
-	private static final String XML_TOKENSCOUNT 		= "tokens-count";
-	private static final String XML_PLACE 			= "place";
-	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 StringBuffer XMLQuery;
-        
-        public CTLQueryVisitor() {
-            this.XMLQuery = new StringBuffer();
-        }
-        
-        public String getXMLQueryFor(TCTLAbstractProperty property, String queryName) {
-            buildXMLQuery(property, queryName);
-            return getFormatted();
-        }
-	
-	public void buildXMLQuery(TCTLAbstractProperty property, String queryName) {
-                XMLQuery.append(startTag(XML_PROP) + queryInfo(queryName) + startTag(XML_FORMULA));
-		property.accept(this, null);
-		XMLQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));              
-	}
-        
-        public String getFormatted() {
-            XMLFormatter formatter = new XMLFormatter();
-            return formatter.format(getStartTag() + XMLQuery.toString() + getEndTag());
-        }
-
-        public StringBuffer getXMLQuery() {
-            return XMLQuery;
-        }
-        
-        public String getStartTag(){
-            return startTag(XML_PROPSET + " " + XML_NS) + "\n";
-        }
-        
-        public String getEndTag(){
-            return endTag(XML_PROPSET) + "\n";
-        }
-	
-	private String queryInfo(String queryName){
-		String nameToPrint = (queryName == null) ? "Query Comment/Name Here" : queryName;
-		return wrapInTag(nameToPrint, XML_PROPID) + wrapInTag(nameToPrint, XML_PROPDESC);
-	}
-	
-	public void visit(TCTLAFNode afNode, Object context) {
-		XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_FINALLY));
-		afNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_FINALLY) + endTag(XML_ALLPATHS));
-	}
-
-	public void visit(TCTLAGNode agNode, Object context) {
-		XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_GLOBALLY));
-		agNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_GLOBALLY) + endTag(XML_ALLPATHS));
-	}
-	
-	public void visit(TCTLAXNode axNode, Object context) {
-		XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_NEXT));
-		axNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_NEXT) + endTag(XML_ALLPATHS));
-	}
-	
-	public void visit(TCTLAUNode auNode, Object context) {
-		XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
-		auNode.getLeft().accept(this, context);
-		XMLQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
-		auNode.getRight().accept(this, context);
-		XMLQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_ALLPATHS));
-	}
-
-	public void visit(TCTLEFNode efNode, Object context) {
-		XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_FINALLY));
-		efNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_FINALLY) + endTag(XML_EXISTSPATH));
-	}
-
-	public void visit(TCTLEGNode egNode, Object context) {
-		XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_GLOBALLY));
-		egNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_GLOBALLY) + endTag(XML_EXISTSPATH));
-	}
-	
-	public void visit(TCTLEXNode exNode, Object context) {
-		XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_NEXT));
-		exNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_NEXT) + endTag(XML_EXISTSPATH));
-	}
-	
-	public void visit(TCTLEUNode euNode, Object context) {
-		XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
-		euNode.getLeft().accept(this, context);
-		XMLQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
-		euNode.getRight().accept(this, context);
-		XMLQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_EXISTSPATH));
-	}
+
+    private static final String XML_NS = "xmlns=\"http://tapaal.net/\"";
+    private static final String XML_PROPSET = "property-set";
+    private static final String XML_PROP = "property";
+    private static final String XML_PROPID = "id";
+    private static final String XML_PROPDESC = "description";
+    private static final String XML_FORMULA = "formula";
+    private static final String XML_ALLPATHS = "all-paths";
+    private static final String XML_EXISTSPATH = "exists-path";
+    private static final String XML_NEGATION = "negation";
+    private static final String XML_CONJUNCTION = "conjunction";
+    private static final String XML_DISJUNCTION = "disjunction";
+    private static final String XML_GLOBALLY = "globally";
+    private static final String XML_FINALLY = "finally";
+    private static final String XML_NEXT = "next";
+    private static final String XML_UNTIL = "until";
+    private static final String XML_BEFORE = "before";
+    private static final String XML_REACH = "reach";
+    private static final String XML_DEADLOCK = "deadlock";
+    private static final String XML_TRUE = "true";
+    private static final String XML_FALSE = "false";
+    private static final String XML_INTEGERLT = "integer-lt";
+    private static final String XML_INTEGERLE = "integer-le";
+    private static final String XML_INTEGEREQ = "integer-eq";
+    private static final String XML_INTEGERNE = "integer-ne";
+    private static final String XML_INTEGERGT = "integer-gt";
+    private static final String XML_INTEGERGE = "integer-ge";
+    private static final String XML_ISFIREABLE = "is-fireable";
+    private static final String XML_INTEGERCONSTANT = "integer-constant";
+    private static final String XML_TOKENSCOUNT = "tokens-count";
+    private static final String XML_PLACE = "place";
+    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 CONTROL = "control";
+
+    private final StringBuffer xmlQuery = new StringBuffer();
+
+    public CTLQueryVisitor() {
+        super();
+    }
+
+    public String getXMLQueryFor(TCTLAbstractProperty property, String queryName, boolean control) {
+        buildXMLQuery(property, queryName, control);
+        return getFormatted();
+    }
+
+    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);
+        if (control) xmlQuery.append(endTag(CONTROL));
+        xmlQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));
+    }
+
+    public String getFormatted() {
+        XMLFormatter formatter = new XMLFormatter();
+        return formatter.format(getStartTag() + xmlQuery.toString() + getEndTag());
+    }
+
+    public StringBuffer getXMLQuery() {
+        return xmlQuery;
+    }
+
+    public String getStartTag() {
+        return startTag(XML_PROPSET + " " + XML_NS) + "\n";
+    }
+
+    public String getEndTag() {
+        return endTag(XML_PROPSET) + "\n";
+    }
+
+    private String queryInfo(String queryName) {
+        String nameToPrint = (queryName == null) ? "Query Comment/Name Here" : queryName;
+        return wrapInTag(nameToPrint, XML_PROPID) + wrapInTag(nameToPrint, XML_PROPDESC);
+    }
+
+    public void visit(TCTLAFNode afNode, Object context) {
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_FINALLY));
+        afNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_FINALLY) + endTag(XML_ALLPATHS));
+    }
+
+    public void visit(TCTLAGNode agNode, Object context) {
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_GLOBALLY));
+        agNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_GLOBALLY) + endTag(XML_ALLPATHS));
+    }
+
+    public void visit(TCTLAXNode axNode, Object context) {
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_NEXT));
+        axNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_NEXT) + endTag(XML_ALLPATHS));
+    }
+
+    public void visit(TCTLAUNode auNode, Object context) {
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
+        auNode.getLeft().accept(this, context);
+        xmlQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
+        auNode.getRight().accept(this, context);
+        xmlQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_ALLPATHS));
+    }
+
+    public void visit(TCTLEFNode efNode, Object context) {
+        xmlQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_FINALLY));
+        efNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_FINALLY) + endTag(XML_EXISTSPATH));
+    }
+
+    public void visit(TCTLEGNode egNode, Object context) {
+        xmlQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_GLOBALLY));
+        egNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_GLOBALLY) + endTag(XML_EXISTSPATH));
+    }
+
+    public void visit(TCTLEXNode exNode, Object context) {
+        xmlQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_NEXT));
+        exNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_NEXT) + endTag(XML_EXISTSPATH));
+    }
+
+    public void visit(TCTLEUNode euNode, Object context) {
+        xmlQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
+        euNode.getLeft().accept(this, context);
+        xmlQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
+        euNode.getRight().accept(this, context);
+        xmlQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_EXISTSPATH));
+    }
 
     public void visit(LTLFNode afNode, Object context) {
-        XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_FINALLY));
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_FINALLY));
         afNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_FINALLY) + endTag(XML_ALLPATHS));
+        xmlQuery.append(endTag(XML_FINALLY) + endTag(XML_ALLPATHS));
     }
 
     public void visit(LTLGNode agNode, Object context) {
-        XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_GLOBALLY));
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_GLOBALLY));
         agNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_GLOBALLY) + endTag(XML_ALLPATHS));
+        xmlQuery.append(endTag(XML_GLOBALLY) + endTag(XML_ALLPATHS));
     }
 
     public void visit(LTLXNode axNode, Object context) {
-        XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_NEXT));
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_NEXT));
         axNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_NEXT) + endTag(XML_ALLPATHS));
+        xmlQuery.append(endTag(XML_NEXT) + endTag(XML_ALLPATHS));
     }
 
     public void visit(LTLUNode auNode, Object context) {
-        XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
+        xmlQuery.append(startTag(XML_ALLPATHS) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
         auNode.getLeft().accept(this, context);
-        XMLQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
+        xmlQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
         auNode.getRight().accept(this, context);
-        XMLQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_ALLPATHS));
-    }
-	
-	public void visit(TCTLPathToStateConverter pathConverter, Object context) {
-		pathConverter.getProperty().accept(this, context);
-	}
-
-	public void visit(TCTLAndListNode andListNode, Object context) {
-		createList(andListNode.getProperties(), context, XML_CONJUNCTION);
-	}
-	
-	public void visit(TCTLOrListNode orListNode, Object context) {
-		createList(orListNode.getProperties(), context, XML_DISJUNCTION);
-	}
-
-	public void visit(TCTLTermListNode termListNode, Object context) {
-		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);
-		}
-	}
-
-	private void createList(List<TCTLAbstractStateProperty> properties, Object context, String seperator) {
-		XMLQuery.append(startTag(seperator));
-
-		for (TCTLAbstractStateProperty p : properties) {
-			p.accept(this, context);
-		}
-
-		XMLQuery.append(endTag(seperator));
-	}
-
-	public void visit(TCTLNotNode notNode, Object context) {
-		XMLQuery.append(startTag(XML_NEGATION));
-		notNode.getProperty().accept(this, context);
-		XMLQuery.append(endTag(XML_NEGATION));
-	}
-	
-	public void visit(TCTLTrueNode tctlTrueNode, Object context) {		
-		XMLQuery.append(emptyElement(XML_TRUE));
-	}
-	
-	public void visit(TCTLFalseNode tctlFalseNode, Object context) {
-		XMLQuery.append(emptyElement(XML_FALSE));
-	}
-	
-	public void visit(TCTLDeadlockNode tctlDeadLockNode, Object context) {
-		XMLQuery.append(emptyElement(XML_DEADLOCK));
-	}
-	
-	public void visit(TCTLConstNode tctlConstNode, Object context){
-		XMLQuery.append(wrapInTag(String.valueOf(tctlConstNode.getConstant()) + "", XML_INTEGERCONSTANT));
-	}
-
-	public void visit(TCTLPlaceNode tctlPlaceNode, Object context){
-		XMLQuery.append(startTag(XML_TOKENSCOUNT));
-		XMLQuery.append(wrapInTag(tctlPlaceNode.toString() + "", XML_PLACE));
-		XMLQuery.append(endTag(XML_TOKENSCOUNT));
-	}
-
-	public void visit(TCTLTransitionNode tctlTransitionNode, Object context){		
-		XMLQuery.append(startTag(XML_ISFIREABLE));
-		XMLQuery.append(wrapInTag(tctlTransitionNode.toString() + "", XML_TRANSITION));
-		XMLQuery.append(endTag(XML_ISFIREABLE));
-	}
-	
-	@Override
-	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";
-		}
-		
-		XMLQuery.append(startTag(op));
-		atomicPropositionNode.getLeft().accept(this, context);
-		atomicPropositionNode.getRight().accept(this, context);
-		XMLQuery.append(endTag(op));
-	}
-	
-	private String wrapInTag(String str, String tag){
-		return startTag(tag) + str + endTag(tag);
-	}
-	private String startTag(String tag){
-		return "<" + tag + ">";
-	}
-	private String endTag(String tag){
-		return "</" + tag + ">";
-	}
-	private String emptyElement(String tag){
-		return startTag(tag + "/");
-	}	
+        xmlQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_ALLPATHS));
+    }
+
+    public void visit(TCTLPathToStateConverter pathConverter, Object context) {
+        pathConverter.getProperty().accept(this, context);
+    }
+
+    public void visit(TCTLAndListNode andListNode, Object context) {
+        createList(andListNode.getProperties(), context, XML_CONJUNCTION);
+    }
+
+    public void visit(TCTLOrListNode orListNode, Object context) {
+        createList(orListNode.getProperties(), context, XML_DISJUNCTION);
+    }
+
+    public void visit(TCTLTermListNode termListNode, Object context) {
+        assert termListNode.getProperties().get(1) instanceof AritmeticOperator;
+        AritmeticOperator operator = (AritmeticOperator) termListNode.getProperties().get(1);
+        String op = operator.toString();
+        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) {
+        xmlQuery.append(startTag(seperator));
+
+        for (TCTLAbstractStateProperty p : properties) {
+            p.accept(this, context);
+        }
+
+        xmlQuery.append(endTag(seperator));
+    }
+
+    public void visit(TCTLNotNode notNode, Object context) {
+        xmlQuery.append(startTag(XML_NEGATION));
+        notNode.getProperty().accept(this, context);
+        xmlQuery.append(endTag(XML_NEGATION));
+    }
+
+    public void visit(TCTLTrueNode tctlTrueNode, Object context) {
+        xmlQuery.append(emptyElement(XML_TRUE));
+    }
+
+    public void visit(TCTLFalseNode tctlFalseNode, Object context) {
+        xmlQuery.append(emptyElement(XML_FALSE));
+    }
+
+    public void visit(TCTLDeadlockNode tctlDeadLockNode, Object context) {
+        xmlQuery.append(emptyElement(XML_DEADLOCK));
+    }
+
+    public void visit(TCTLConstNode tctlConstNode, Object context) {
+        xmlQuery.append(wrapInTag(tctlConstNode.getConstant() + "", XML_INTEGERCONSTANT));
+    }
+
+    public void visit(TCTLPlaceNode tctlPlaceNode, Object context) {
+        xmlQuery.append(startTag(XML_TOKENSCOUNT));
+        xmlQuery.append(wrapInTag(tctlPlaceNode.toString() + "", XML_PLACE));
+        xmlQuery.append(endTag(XML_TOKENSCOUNT));
+    }
+
+    public void visit(TCTLTransitionNode tctlTransitionNode, Object context) {
+        xmlQuery.append(startTag(XML_ISFIREABLE));
+        xmlQuery.append(wrapInTag(tctlTransitionNode.toString() + "", XML_TRANSITION));
+        xmlQuery.append(endTag(XML_ISFIREABLE));
+    }
+
+    @Override
+    public void visit(TCTLAtomicPropositionNode atomicPropositionNode, Object context) {
+        String opTest = atomicPropositionNode.getOp();
+        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);
+        atomicPropositionNode.getRight().accept(this, context);
+        xmlQuery.append(endTag(op));
+    }
+
+    private String wrapInTag(String str, String tag) {
+        return startTag(tag) + str + endTag(tag);
+    }
+
+    private String startTag(String tag) {
+        return "<" + tag + ">";
+    }
+
+    private String endTag(String tag) {
+        return "</" + tag + ">";
+    }
+
+    private String emptyElement(String tag) {
+        return startTag(tag + "/");
+    }
 }

=== modified file 'src/main/java/dk/aau/cs/TCTL/visitors/CombiTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/CombiTranslationQueryVisitor.java	2019-03-22 10:13:18 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/CombiTranslationQueryVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/ContainsPlaceWithDisabledTemplateVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ContainsPlaceWithDisabledTemplateVisitor.java	2014-05-22 20:26:41 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/ContainsPlaceWithDisabledTemplateVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/ContainsSharedPlaceVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ContainsSharedPlaceVisitor.java	2014-05-22 20:26:41 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/ContainsSharedPlaceVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/ContainsSharedTransitionVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ContainsSharedTransitionVisitor.java	2017-03-12 00:33:00 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/ContainsSharedTransitionVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/FixAbbrivPlaceNames.java'
--- src/dk/aau/cs/TCTL/visitors/FixAbbrivPlaceNames.java	2014-11-01 09:31:54 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/FixAbbrivPlaceNames.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/FixAbbrivTransitionNames.java'
--- src/dk/aau/cs/TCTL/visitors/FixAbbrivTransitionNames.java	2017-03-12 00:33:00 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/FixAbbrivTransitionNames.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/HasDeadlockVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/HasDeadlockVisitor.java	2013-05-18 21:26:56 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/HasDeadlockVisitor.java	2022-07-21 13:30:11 +0000
@@ -16,7 +16,7 @@
 		((Context)context).hasDeadlock = true;
 	}
 
-	private class Context{
+	private static class Context{
 		public boolean hasDeadlock = true;
 	}
 }

=== modified file 'src/main/java/dk/aau/cs/TCTL/visitors/IsReachabilityVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/IsReachabilityVisitor.java	2017-08-03 11:48:35 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/IsReachabilityVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java	2021-10-14 06:28:05 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java	2022-07-21 13:30:11 +0000
@@ -7,45 +7,45 @@
 
 public class LTLQueryVisitor extends VisitorBase {
 
-    private static final String XML_NS 			= "xmlns=\"http://tapaal.net/\"";
-    private static final String XML_PROPSET 		= "property-set";
-    private static final String XML_PROP			= "property";
-    private static final String XML_PROPID			= "id";
-    private static final String XML_PROPDESC		= "description";
-    private static final String XML_FORMULA			= "formula";
-    private static final String XML_ALLPATHS		= "all-paths";
-    private static final String XML_EXISTSPATH	 	= "exists-path";
-    private static final String XML_NEGATION		= "negation";
+    private static final String XML_NS 			        = "xmlns=\"http://tapaal.net/\"";
+    private static final String XML_PROPSET 		    = "property-set";
+    private static final String XML_PROP			    = "property";
+    private static final String XML_PROPID			    = "id";
+    private static final String XML_PROPDESC		    = "description";
+    private static final String XML_FORMULA		    	= "formula";
+    private static final String XML_ALLPATHS	    	= "all-paths";
+    private static final String XML_EXISTSPATH	    	= "exists-path";
+    private static final String XML_NEGATION	    	= "negation";
     private static final String XML_CONJUNCTION 		= "conjunction";
     private static final String XML_DISJUNCTION 		= "disjunction";
-    private static final String XML_GLOBALLY		= "globally";
-    private static final String XML_FINALLY			= "finally";
-    private static final String XML_NEXT			= "next";
-    private static final String XML_UNTIL 			= "until";
-    private static final String XML_BEFORE 			= "before";
-    private static final String XML_REACH 			= "reach";
-    private static final String XML_DEADLOCK 		= "deadlock";
-    private static final String XML_TRUE 			= "true";
-    private static final String XML_FALSE 			= "false";
-    private static final String XML_INTEGERLT 		= "integer-lt";
-    private static final String XML_INTEGERLE 		= "integer-le";
-    private static final String XML_INTEGEREQ		= "integer-eq";
-    private static final String XML_INTEGERNE 		= "integer-ne";
-    private static final String XML_INTEGERGT 		= "integer-gt";
-    private static final String XML_INTEGERGE               = "integer-ge";
-    private static final String XML_ISFIREABLE		= "is-fireable";
+    private static final String XML_GLOBALLY		    = "globally";
+    private static final String XML_FINALLY			    = "finally";
+    private static final String XML_NEXT			    = "next";
+    private static final String XML_UNTIL 		    	= "until";
+    private static final String XML_BEFORE 			    = "before";
+    private static final String XML_REACH 		    	= "reach";
+    private static final String XML_DEADLOCK 		    = "deadlock";
+    private static final String XML_TRUE 			    = "true";
+    private static final String XML_FALSE 			    = "false";
+    private static final String XML_INTEGERLT 		    = "integer-lt";
+    private static final String XML_INTEGERLE 		    = "integer-le";
+    private static final String XML_INTEGEREQ		    = "integer-eq";
+    private static final String XML_INTEGERNE 		    = "integer-ne";
+    private static final String XML_INTEGERGT 		    = "integer-gt";
+    private static final String XML_INTEGERGE           = "integer-ge";
+    private static final String XML_ISFIREABLE		    = "is-fireable";
     private static final String XML_INTEGERCONSTANT 	= "integer-constant";
     private static final String XML_TOKENSCOUNT 		= "tokens-count";
-    private static final String XML_PLACE 			= "place";
-    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_PLACE 			    = "place";
+    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 StringBuffer XMLQuery;
+    private final StringBuffer xmlQuery = new StringBuffer();
 
     public LTLQueryVisitor() {
-        this.XMLQuery = new StringBuffer();
+        super();
     }
 
     public String getXMLQueryFor(TCTLAbstractProperty property, String queryName) {
@@ -54,20 +54,20 @@
     }
 
     public void buildXMLQuery(TCTLAbstractProperty property, String queryName) {
-        XMLQuery.append(startTag(XML_PROP) + queryInfo(queryName) + startTag(XML_FORMULA));
+        xmlQuery.append(startTag(XML_PROP) + queryInfo(queryName) + startTag(XML_FORMULA));
         property.accept(this, null);
-        XMLQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));
+        xmlQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));
     }
 
     public String getFormatted() {
         XMLFormatter formatter = new XMLFormatter();
-        return formatter.format(getStartTag() + XMLQuery.toString() + getEndTag());
+        return formatter.format(getStartTag() + xmlQuery.toString() + getEndTag());
     }
 
     public String getFormatted(StringBuffer CTLQueries) {
         XMLFormatter formatter = new XMLFormatter();
-        XMLQuery.append(CTLQueries);
-        return formatter.format(getStartTag() + XMLQuery.toString() + getEndTag());
+        xmlQuery.append(CTLQueries);
+        return formatter.format(getStartTag() + xmlQuery.toString() + getEndTag());
     }
 
     public String getStartTag(){
@@ -84,41 +84,41 @@
     }
 
     public void visit(LTLANode aNode, Object context) {
-        XMLQuery.append(startTag(XML_ALLPATHS));
+        xmlQuery.append(startTag(XML_ALLPATHS));
         aNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_ALLPATHS));
+        xmlQuery.append(endTag(XML_ALLPATHS));
     }
 
     public void visit(LTLENode eNode, Object context) {
-        XMLQuery.append(startTag(XML_EXISTSPATH));
+        xmlQuery.append(startTag(XML_EXISTSPATH));
         eNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_EXISTSPATH));
+        xmlQuery.append(endTag(XML_EXISTSPATH));
     }
 
     public void visit(LTLFNode afNode, Object context) {
-        XMLQuery.append(startTag(XML_FINALLY));
+        xmlQuery.append(startTag(XML_FINALLY));
         afNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_FINALLY));
+        xmlQuery.append(endTag(XML_FINALLY));
     }
 
     public void visit(LTLGNode agNode, Object context) {
-        XMLQuery.append(startTag(XML_GLOBALLY));
+        xmlQuery.append(startTag(XML_GLOBALLY));
         agNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_GLOBALLY));
+        xmlQuery.append(endTag(XML_GLOBALLY));
     }
 
     public void visit(LTLXNode axNode, Object context) {
-        XMLQuery.append(startTag(XML_NEXT));
+        xmlQuery.append(startTag(XML_NEXT));
         axNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_NEXT));
+        xmlQuery.append(endTag(XML_NEXT));
     }
 
     public void visit(LTLUNode auNode, Object context) {
-        XMLQuery.append(startTag(XML_UNTIL) + startTag(XML_BEFORE));
+        xmlQuery.append(startTag(XML_UNTIL) + startTag(XML_BEFORE));
         auNode.getLeft().accept(this, context);
-        XMLQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
+        xmlQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
         auNode.getRight().accept(this, context);
-        XMLQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL));
+        xmlQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL));
     }
 
     public void visit(TCTLPathToStateConverter pathConverter, Object context) {
@@ -137,85 +137,96 @@
         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) {
-        XMLQuery.append(startTag(seperator));
+        xmlQuery.append(startTag(seperator));
 
         for (TCTLAbstractStateProperty p : properties) {
             p.accept(this, context);
         }
 
-        XMLQuery.append(endTag(seperator));
+        xmlQuery.append(endTag(seperator));
     }
 
     public void visit(TCTLNotNode notNode, Object context) {
-        XMLQuery.append(startTag(XML_NEGATION));
+        xmlQuery.append(startTag(XML_NEGATION));
         notNode.getProperty().accept(this, context);
-        XMLQuery.append(endTag(XML_NEGATION));
+        xmlQuery.append(endTag(XML_NEGATION));
     }
 
     public void visit(TCTLTrueNode tctlTrueNode, Object context) {
-        XMLQuery.append(emptyElement(XML_TRUE));
+        xmlQuery.append(emptyElement(XML_TRUE));
     }
 
     public void visit(TCTLFalseNode tctlFalseNode, Object context) {
-        XMLQuery.append(emptyElement(XML_FALSE));
+        xmlQuery.append(emptyElement(XML_FALSE));
     }
 
     public void visit(TCTLDeadlockNode tctlDeadLockNode, Object context) {
-        XMLQuery.append(emptyElement(XML_DEADLOCK));
+        xmlQuery.append(emptyElement(XML_DEADLOCK));
     }
 
     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){
-        XMLQuery.append(startTag(XML_TOKENSCOUNT));
-        XMLQuery.append(wrapInTag(tctlPlaceNode.toString() + "", XML_PLACE));
-        XMLQuery.append(endTag(XML_TOKENSCOUNT));
+        xmlQuery.append(startTag(XML_TOKENSCOUNT));
+        xmlQuery.append(wrapInTag(tctlPlaceNode.toString() + "", XML_PLACE));
+        xmlQuery.append(endTag(XML_TOKENSCOUNT));
     }
 
     public void visit(TCTLTransitionNode tctlTransitionNode, Object context){
-        XMLQuery.append(startTag(XML_ISFIREABLE));
-        XMLQuery.append(wrapInTag(tctlTransitionNode.toString() + "", XML_TRANSITION));
-        XMLQuery.append(endTag(XML_ISFIREABLE));
+        xmlQuery.append(startTag(XML_ISFIREABLE));
+        xmlQuery.append(wrapInTag(tctlTransitionNode.toString() + "", XML_TRANSITION));
+        xmlQuery.append(endTag(XML_ISFIREABLE));
     }
 
     @Override
-    public void visit(TCTLAtomicPropositionNode atomicPropositionNode,
-                      Object context) {
+    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));
+        xmlQuery.append(startTag(op));
         atomicPropositionNode.getLeft().accept(this, context);
         atomicPropositionNode.getRight().accept(this, context);
-        XMLQuery.append(endTag(op));
+        xmlQuery.append(endTag(op));
     }
 
     private String wrapInTag(String str, String tag){

=== modified file 'src/main/java/dk/aau/cs/TCTL/visitors/OptimizedStandardTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/OptimizedStandardTranslationQueryVisitor.java	2019-03-23 07:51:29 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/OptimizedStandardTranslationQueryVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/RenamePlaceTCTLVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/RenamePlaceTCTLVisitor.java	2014-05-22 20:26:41 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/RenamePlaceTCTLVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/RenameTransitionTCTLVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/RenameTransitionTCTLVisitor.java	2017-03-12 00:33:00 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/RenameTransitionTCTLVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/StandardTranslationQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/StandardTranslationQueryVisitor.java	2019-03-23 07:51:29 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/StandardTranslationQueryVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java	2017-03-12 00:33:00 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/TCTL/visitors/VerifyTransitionNamesVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/VerifyTransitionNamesVisitor.java	2017-03-12 00:33:00 +0000
+++ src/main/java/dk/aau/cs/TCTL/visitors/VerifyTransitionNamesVisitor.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/approximation/ApproximationWorker.java'
--- src/dk/aau/cs/approximation/ApproximationWorker.java	2020-12-16 21:11:57 +0000
+++ src/main/java/dk/aau/cs/approximation/ApproximationWorker.java	2022-07-21 13:30:11 +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,17 @@
 						// 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 +119,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 +143,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 +166,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 +186,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 +221,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 +242,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 +261,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 +288,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 +312,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 +331,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 +376,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 +404,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 +426,8 @@
 					verificationResult.getSecondaryTrace(),
 					verificationResult.verificationTime(),
 					verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation());
+					false,
+                   verificationResult.getUnfoldedModel());
 				value.setNameMapping(composedModel.value2());
 	        } else {
 	            // If r > 1
@@ -385,14 +436,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 +460,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 +486,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 +506,8 @@
 						verificationResult.getSecondaryTrace(),
 						verificationResult.verificationTime(),
 						verificationResult.stats(),
-						verificationResult.isSolvedUsingStateEquation());
+						false,
+                        verificationResult.getUnfoldedModel());
 				    value.setNameMapping(composedModel.value2());
 	            }
 				else {
@@ -467,7 +523,8 @@
 						verificationResult.getSecondaryTrace(),
 						verificationResult.verificationTime(),
 						verificationResult.stats(),
-						verificationResult.isSolvedUsingStateEquation());
+						false,
+                        verificationResult.getUnfoldedModel());
 				    value.setNameMapping(composedModel.value2());
 				}
 	        }
@@ -485,7 +542,8 @@
                     verificationResult.getSecondaryTrace(),
                     verificationResult.verificationTime(),
                     verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation());
+					false,
+                    verificationResult.getUnfoldedModel());
                 value.setNameMapping(composedModel.value2());
 	        }
 	        else {
@@ -502,7 +560,8 @@
                             verificationResult.getSecondaryTrace(),
                             verificationResult.verificationTime(),
                             verificationResult.stats(),
-        					verificationResult.isSolvedUsingStateEquation());
+        					false,
+                            verificationResult.getUnfoldedModel());
                     value.setNameMapping(composedModel.value2());
 	                    
 				}
@@ -514,14 +573,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 +599,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 +629,8 @@
 	                            verificationResult.getSecondaryTrace(),
 	                            verificationResult.verificationTime() + approxResult.verificationTime(),
 	                            verificationResult.stats(),
-	        					verificationResult.isSolvedUsingStateEquation());
+	        					false,
+                                verificationResult.getUnfoldedModel());
 	                    value.setNameMapping(composedModel.value2());
 	                }
 	                else {
@@ -578,7 +644,8 @@
 							verificationResult.getSecondaryTrace(),
 							verificationResult.verificationTime(),
 							verificationResult.stats(),
-							verificationResult.isSolvedUsingStateEquation());
+							false,
+                            verificationResult.getUnfoldedModel());
 					    value.setNameMapping(composedModel.value2());
 	                }
 	            }
@@ -591,7 +658,8 @@
 	                verificationResult.getSecondaryTrace(),
 	                verificationResult.verificationTime(),
 	                verificationResult.stats(),
-					verificationResult.isSolvedUsingStateEquation());
+					false,
+                    verificationResult.getUnfoldedModel());
 	        value.setNameMapping(composedModel.value2());
 	    }
 		

=== modified file 'src/main/java/dk/aau/cs/approximation/OverApproximation.java'
--- src/dk/aau/cs/approximation/OverApproximation.java	2020-07-20 12:17:24 +0000
+++ src/main/java/dk/aau/cs/approximation/OverApproximation.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/approximation/UnderApproximation.java'
--- src/dk/aau/cs/approximation/UnderApproximation.java	2020-07-20 12:17:24 +0000
+++ src/main/java/dk/aau/cs/approximation/UnderApproximation.java	2022-07-21 13:30:11 +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
+        );
+    }
 
 }

=== added file 'src/main/java/dk/aau/cs/io/LoadTACPN.java'
--- src/main/java/dk/aau/cs/io/LoadTACPN.java	1970-01-01 00:00:00 +0000
+++ src/main/java/dk/aau/cs/io/LoadTACPN.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/LoadedModel.java'
--- src/dk/aau/cs/io/LoadedModel.java	2020-08-26 12:29:25 +0000
+++ src/main/java/dk/aau/cs/io/LoadedModel.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/LoadedQueries.java'
--- src/dk/aau/cs/io/LoadedQueries.java	2020-10-09 07:59:49 +0000
+++ src/main/java/dk/aau/cs/io/LoadedQueries.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/ModelLoader.java'
--- src/dk/aau/cs/io/ModelLoader.java	2021-08-10 11:37:11 +0000
+++ src/main/java/dk/aau/cs/io/ModelLoader.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/NetWriter.java'
--- src/pipe/dataLayer/NetWriter.java	2014-05-22 21:26:05 +0000
+++ src/main/java/dk/aau/cs/io/NetWriter.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/PNMLWriter.java'
--- src/dk/aau/cs/io/PNMLWriter.java	2020-07-13 13:58:47 +0000
+++ src/main/java/dk/aau/cs/io/PNMLWriter.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/PNMLoader.java'
--- src/dk/aau/cs/io/PNMLoader.java	2020-08-26 12:29:25 +0000
+++ src/main/java/dk/aau/cs/io/PNMLoader.java	2022-07-21 13:30:11 +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/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java'
--- src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java	1970-01-01 00:00:00 +0000
+++ src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java	2022-07-21 13:30:11 +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);