Merge lp:~tapaal-contributor/tapaal/LTL-dialog into lp:tapaal

[Lena Ernstsen]

Added ability to make LTL queries

LTL query are available when the net is untimed and no game. It can be accessed by changing the query category through a drop down menu at the top of the query dialog.
It is possible to convert a CTL dialog to an LTL dialog and vice versa.

When the ltl category is chosen 'A' will always be in the beginning of the query property, and it should not be possible to delete it.

[Jiri Srba (srba)]

Three comments:

1. If the Tarjan is selected (please spell it with capital letter), the switch should be -ltl
   but if it is not selected, it should be -ltl ndfs so that it does not call Tarjan.

2. Please, rename the mouseover tooltips to "Globally" for G, "Next" for X, "Eventually" for F, and "Until" for U.

3. The supported search strategies are Heuristic, DFS and Random Search. Please, allow to choose between all three of them, the Heuristic should be the default option.

review: Needs Fixing

[Jiri Srba (srba)]

Conversion between CTL and LTL does not work. Make a simple LTL formula like F true and then change it to CTL (in dropdown menu). The formula still says F but this is not a valid CTL formula (this one has to have EF or AF - I would suggest by default to convert all operators to universal ones A - also for Until and neXt and G).

review: Needs Fixing

[Jiri Srba (srba)]

Also, manual parsing of LTL queries does not work. Write e.g. manually

true U true

and after parsing it only picks it up as

true.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/LTL-dialog]

1157. By Lena Ernstsen on 2021-08-10

Added the 'A' node file

1158. By Lena Ernstsen on 2021-08-10

Fixed incorrect ltl parser

1159. By Lena Ernstsen on 2021-08-10

Merged lp:tapaal

1160. By Kenneth Yrke Jørgensen on 2021-08-11

Updated Gradle to run javacc on compile

Updated gradle to run javacc on compile and removed old generated file from source tree.
This makes sure that manual changes does happen to generated files and forces changes to be done in the *.jj files.

1161. By Kenneth Yrke Jørgensen on 2021-08-12

Merged with upstream

1162. By Lena Ernstsen on 2021-08-12

Not possible to parse deadlock in manual edit of ltl query

1163. By Lena Ernstsen on 2021-08-12

Not possible to negate ltl selection if it starts with 'A'

1164. By Lena Ernstsen on 2021-08-12

deadlock button is not visible in ltl query

1165. By Lena Ernstsen on 2021-08-12

Fixes to using 'A' quantifier correctly

1166. By Lena Ernstsen on 2021-08-13

Fixed changing category for a negation query

1167. By Lena Ernstsen on 2021-08-16

Conversion between ltl and ctl should work correctly

1168. By Lena Ernstsen on 2021-08-16

When importing xml queries, we attempt to detect the category

1169. By Lena Ernstsen on 2021-08-16

Fixed wrong parsing of ltl imported queries and possible to choose all imported queries as one category

1170. By Lena Ernstsen on 2021-08-17

Fixed ltl/ctl import logic

1171. By Lena Ernstsen on 2021-08-17

Added additional checks to query category for pnml import

1172. By Lena Ernstsen on 2021-08-17

Added category checks when opening tapn files

1173. By Lena Ernstsen on 2021-08-18

Merged lp:tapaal

1174. By Lena Ernstsen on 2021-08-19

Fixed stackoverflow when parsing xml queries

1175. By Lena Ernstsen on 2021-08-20

Made null-pointer check and changed message

1176. By <email address hidden> on 2021-09-11

merged trunk to branch

1177. By Lena Ernstsen on 2021-09-15

Fixed run issues

1178. By Lena Ernstsen on 2021-09-24

Merged trunk

[Kenneth Yrke Jørgensen (yrke)]

review: Approve (code)

[Jiri Srba (srba)]

If you verify an LTL query and ask to open the reduced net (in the query answer dialog), it will fail. See this bug report:

https://bugs.launchpad.net/tapaal/+bug/1945318

review: Needs Fixing

[Jiri Srba (srba)]

Another problem with saving LTL options in .tapn is reported here:

https://bugs.launchpad.net/tapaal/+bug/1945320

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/LTL-dialog]

1179. By Lena Ernstsen on 2021-09-29

Fixed tarjan not being loaded from file

1180. By Kenneth Yrke Jørgensen on 2021-09-30

Synced with main

1181. By Jiri Srba <email address hidden> on 2021-09-30

merged in trunk

1182. By Jiri Srba on 2021-09-30

merged with trunk

1183. By Lena Ernstsen on 2021-10-02

--write-reduced is not ignored with ltl anymore

1184. By Lena Ernstsen on 2021-10-02

Fixed problem with ! and AU when manually parsing

1185. By Jiri Srba on 2021-10-02

merged with trunk

1186. By Lena Ernstsen on 2021-10-08

Added 'E' to the ltl dialog

1187. By Lena Ernstsen on 2021-10-08

Added ltl files

1188. By Jiri Srba on 2021-10-11

merged with trunk

1189. By Lena Ernstsen on 2021-10-13

'Open reduced net' uses the same options when called from query dialog and verification dialog

1190. By Lena Ernstsen on 2021-10-14

Added missing 'exists-path' in xml parser

1191. By Lena Ernstsen on 2021-10-14

Changed the ltl button functionality

1192. By Lena Ernstsen on 2021-10-15

Changed when ltl buttons are enabled. DeleteSelection does not automatically add A node to query when ltl

1193. By Lena Ernstsen on 2021-10-15

Added error message when trace failed to open

1194. By Lena Ernstsen on 2021-10-15

Corrected spelling mistakes

1195. By Lena Ernstsen on 2021-10-16

Updated enabledness of ltl buttons

1196. By Lena Ernstsen on 2021-10-16

updated addPredicate button for ltl queries

1197. By <email address hidden> on 2021-10-17

merged with trunk

1198. By <email address hidden> on 2021-10-17

merged with trunk

[Jiri Srba (srba)]

Tested and works, merging to trunk now :-)

review: Approve

=== modified file 'build.gradle'
--- build.gradle	2020-07-20 11:56:08 +0000
+++ build.gradle	2021-10-17 18:45:24 +0000
@@ -2,6 +2,7 @@
     id 'java'
     id 'application'
     id 'org.jetbrains.kotlin.jvm' version '1.3.71'
+    id "ca.coglinc.javacc" version "2.4.0"
 }
 
 group 'net.tapaal'
@@ -16,11 +17,16 @@
     mavenCentral()
 }
 
+compileJavacc {
+    inputDirectory = file('src/')
+    //outputDirectory = file(project.buildDir.absolutePath + '/generated/javacc')
+}
+
 //Set the soruce and resource dir
 sourceSets {
     main {
         java {
-            srcDirs = ['src/']
+            srcDirs = ['src/', compileJavacc.outputDirectory]
             exclude("resources/")
         }
         resources {

=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/ParseException.java'
=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/SimpleCharStream.java'
=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java'
=== renamed file 'src/resources/TCTLParser/TAPAALCTLQueryParser.jj' => 'src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.jj'
--- src/resources/TCTLParser/TAPAALCTLQueryParser.jj	2021-09-14 20:13:01 +0000
+++ src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.jj	2021-10-17 18:45:24 +0000
@@ -147,17 +147,15 @@
 	TCTLAbstractStateProperty child2 = null; 
 }
 {
-	( 
-		<EF> child = OrExpr() {return new TCTLEFNode(child); } 
-		| <EG> child = OrExpr() {return new TCTLEGNode(child); } 
-		| <EX> child = OrExpr() {return new TCTLEXNode(child); } 
-        | <E>  "(" child = OrExpr() <U> child2 = OrExpr() ")" {return new TCTLEUNode(child, child2); }
-		| <AF> child = OrExpr() {return new TCTLAFNode(child); } 
-		| <AG> child = OrExpr() {return new TCTLAGNode(child); } 
-        | <A>  "(" child = OrExpr() <U> child2 = OrExpr() ")" {return new TCTLAUNode(child, child2); }
-		| <AX> child = OrExpr() {return new TCTLAXNode(child); } 
-        | child = OrExpr() { return new TCTLStateToPathConverter(child); }
-	) 
+	<EF> child = OrExpr() {return new TCTLEFNode(child); }
+    | <EG> child = OrExpr() {return new TCTLEGNode(child); }
+    | <EX> child = OrExpr() {return new TCTLEXNode(child); }
+    | <E>  "(" child = OrExpr() <U> child2 = OrExpr() ")" {return new TCTLEUNode(child, child2); }
+    | <AF> child = OrExpr() {return new TCTLAFNode(child); }
+    | <AG> child = OrExpr() {return new TCTLAGNode(child); }
+    | <A>  "(" child = OrExpr() <U> child2 = OrExpr() ")" {return new TCTLAUNode(child, child2); }
+    | <AX> child = OrExpr() {return new TCTLAXNode(child); }
+    | child = OrExpr() { return new TCTLStateToPathConverter(child); }
 }
 
 TCTLAbstractStateProperty OrExpr() : 

=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParserConstants.java'
=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParserTokenManager.java'
=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/Token.java'
=== removed file 'src/dk/aau/cs/TCTL/CTLParsing/TokenMgrError.java'
=== added file 'src/dk/aau/cs/TCTL/LTLANode.java'
--- src/dk/aau/cs/TCTL/LTLANode.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLANode.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,107 @@
+package dk.aau.cs.TCTL;
+
+import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
+
+public class LTLANode extends TCTLAbstractPathProperty {
+    TCTLAbstractStateProperty property;
+
+    public void setProperty(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public TCTLAbstractStateProperty getProperty() {
+        return property;
+    }
+
+    public LTLANode(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public LTLANode() {
+        this.property = new TCTLStatePlaceHolder();
+        this.property.setParent(this);
+    }
+
+    @Override
+    public String toString() {
+        String s = property.isSimpleProperty() ? property.toString() : "("
+            + property.toString() + ")";
+        return "A " + s;
+    }
+
+    @Override
+    public boolean isSimpleProperty() {
+        return false;
+    }
+
+    @Override
+    public StringPosition[] getChildren() {
+        int start = property.isSimpleProperty() ? 0 : 1;
+        start = start + 2;
+        int end = start + property.toString().length();
+        StringPosition position = new StringPosition(start, end, property);
+
+        StringPosition[] children = { position };
+        return children;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty replace(TCTLAbstractProperty object1,
+                                            TCTLAbstractProperty object2) {
+        if (this == object1 && object2 instanceof TCTLAbstractPathProperty) {
+            return (TCTLAbstractPathProperty) object2;
+        } else {
+            property = property.replace(object1, object2);
+            return this;
+        }
+    }
+
+    @Override
+    public boolean containsPlaceHolder() {
+        return property.containsPlaceHolder();
+    }
+
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (o instanceof LTLANode) {
+            LTLANode node = (LTLANode) o;
+            return property.equals(node.getProperty());
+        }
+        return false;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty copy() {
+        return new LTLANode(property.copy());
+    }
+
+    @Override
+    public boolean hasNestedPathQuantifiers() {
+        return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
+    }
+
+    public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
+        return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
+    }
+
+    public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
+        return property.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
+    }
+
+    @Override
+    public TCTLAbstractProperty findFirstPlaceHolder() {
+        return property.findFirstPlaceHolder();
+    }
+
+    @Override
+    public void accept(ITCTLVisitor visitor, Object context) {
+        visitor.visit(this, context);
+    }
+}

=== added file 'src/dk/aau/cs/TCTL/LTLENode.java'
--- src/dk/aau/cs/TCTL/LTLENode.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLENode.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,107 @@
+package dk.aau.cs.TCTL;
+
+import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
+
+public class LTLENode extends TCTLAbstractPathProperty {
+    TCTLAbstractStateProperty property;
+
+    public void setProperty(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public TCTLAbstractStateProperty getProperty() {
+        return property;
+    }
+
+    public LTLENode(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public LTLENode() {
+        this.property = new TCTLStatePlaceHolder();
+        this.property.setParent(this);
+    }
+
+    @Override
+    public String toString() {
+        String s = property.isSimpleProperty() ? property.toString() : "("
+            + property.toString() + ")";
+        return "E " + s;
+    }
+
+    @Override
+    public boolean isSimpleProperty() {
+        return false;
+    }
+
+    @Override
+    public StringPosition[] getChildren() {
+        int start = property.isSimpleProperty() ? 0 : 1;
+        start = start + 2;
+        int end = start + property.toString().length();
+        StringPosition position = new StringPosition(start, end, property);
+
+        StringPosition[] children = { position };
+        return children;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty replace(TCTLAbstractProperty object1,
+                                            TCTLAbstractProperty object2) {
+        if (this == object1 && object2 instanceof TCTLAbstractPathProperty) {
+            return (TCTLAbstractPathProperty) object2;
+        } else {
+            property = property.replace(object1, object2);
+            return this;
+        }
+    }
+
+    @Override
+    public boolean containsPlaceHolder() {
+        return property.containsPlaceHolder();
+    }
+
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (o instanceof LTLENode) {
+            LTLENode node = (LTLENode) o;
+            return property.equals(node.getProperty());
+        }
+        return false;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty copy() {
+        return new LTLENode(property.copy());
+    }
+
+    @Override
+    public boolean hasNestedPathQuantifiers() {
+        return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
+    }
+
+    public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
+        return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
+    }
+
+    public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
+        return property.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
+    }
+
+    @Override
+    public TCTLAbstractProperty findFirstPlaceHolder() {
+        return property.findFirstPlaceHolder();
+    }
+
+    @Override
+    public void accept(ITCTLVisitor visitor, Object context) {
+        visitor.visit(this, context);
+    }
+}

=== added file 'src/dk/aau/cs/TCTL/LTLFNode.java'
--- src/dk/aau/cs/TCTL/LTLFNode.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLFNode.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,107 @@
+package dk.aau.cs.TCTL;
+
+import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
+
+public class LTLFNode extends TCTLAbstractPathProperty {
+    TCTLAbstractStateProperty property;
+
+    public void setProperty(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public TCTLAbstractStateProperty getProperty() {
+        return property;
+    }
+
+    public LTLFNode(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public LTLFNode() {
+        this.property = new TCTLStatePlaceHolder();
+        this.property.setParent(this);
+    }
+
+    @Override
+    public String toString() {
+        String s = property.isSimpleProperty() ? property.toString() : "("
+            + property.toString() + ")";
+        return "F " + s;
+    }
+
+    @Override
+    public boolean isSimpleProperty() {
+        return false;
+    }
+
+    @Override
+    public StringPosition[] getChildren() {
+        int start = property.isSimpleProperty() ? 0 : 1;
+        start = start + 2;
+        int end = start + property.toString().length();
+        StringPosition position = new StringPosition(start, end, property);
+
+        StringPosition[] children = { position };
+        return children;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty replace(TCTLAbstractProperty object1,
+                                            TCTLAbstractProperty object2) {
+        if (this == object1 && object2 instanceof TCTLAbstractPathProperty) {
+            return (TCTLAbstractPathProperty) object2;
+        } else {
+            property = property.replace(object1, object2);
+            return this;
+        }
+    }
+
+    @Override
+    public boolean containsPlaceHolder() {
+        return property.containsPlaceHolder();
+    }
+
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (o instanceof LTLFNode) {
+            LTLFNode node = (LTLFNode) o;
+            return property.equals(node.getProperty());
+        }
+        return false;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty copy() {
+        return new LTLFNode(property.copy());
+    }
+
+    @Override
+    public boolean hasNestedPathQuantifiers() {
+        return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
+    }
+
+    public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
+        return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
+    }
+
+    public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
+        return property.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
+    }
+
+    @Override
+    public TCTLAbstractProperty findFirstPlaceHolder() {
+        return property.findFirstPlaceHolder();
+    }
+
+    @Override
+    public void accept(ITCTLVisitor visitor, Object context) {
+        visitor.visit(this, context);
+    }
+}

=== added file 'src/dk/aau/cs/TCTL/LTLGNode.java'
--- src/dk/aau/cs/TCTL/LTLGNode.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLGNode.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,106 @@
+package dk.aau.cs.TCTL;
+
+import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
+
+public class LTLGNode extends TCTLAbstractPathProperty {
+    TCTLAbstractStateProperty property;
+
+    public void setProperty(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public TCTLAbstractStateProperty getProperty() {
+        return property;
+    }
+
+    public LTLGNode(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public LTLGNode() {
+        this.property = new TCTLStatePlaceHolder();;
+        this.property.setParent(this);
+    }
+
+    @Override
+    public String toString() {
+        String s = property.isSimpleProperty() ? property.toString() : "("
+            + property.toString() + ")";
+        return "G " + s;
+    }
+
+    @Override
+    public StringPosition[] getChildren() {
+        int start = property.isSimpleProperty() ? 0 : 1;
+        start = start + 2;
+        int end = start + property.toString().length();
+        StringPosition position = new StringPosition(start, end, property);
+
+        StringPosition[] children = { position };
+        return children;
+    }
+
+    @Override
+    public boolean isSimpleProperty() {
+        return false;
+    }
+
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (o instanceof LTLGNode) {
+            LTLGNode node = (LTLGNode) o;
+            return property.equals(node.getProperty());
+        }
+        return false;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty replace(TCTLAbstractProperty object1,
+                                            TCTLAbstractProperty object2) {
+        if (this == object1 && object2 instanceof TCTLAbstractPathProperty) {
+            return (TCTLAbstractPathProperty) object2;
+        } else {
+            property = property.replace(object1, object2);
+            return this;
+        }
+    }
+
+    @Override
+    public TCTLAbstractPathProperty copy() {
+        return new LTLGNode(property.copy());
+    }
+
+    @Override
+    public boolean containsPlaceHolder() {
+        return property.containsPlaceHolder();
+    }
+    @Override
+    public boolean hasNestedPathQuantifiers() {
+        return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
+    }
+
+    public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
+        return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
+    }
+
+    public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
+        return property.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
+    }
+
+    @Override
+    public TCTLAbstractProperty findFirstPlaceHolder() {
+        return property.findFirstPlaceHolder();
+    }
+
+    @Override
+    public void accept(ITCTLVisitor visitor, Object context) {
+        visitor.visit(this, context);
+    }
+}

=== added directory 'src/dk/aau/cs/TCTL/LTLParsing'
=== added file 'src/dk/aau/cs/TCTL/LTLParsing/TAPAALLTLQueryParser.jj'
--- src/dk/aau/cs/TCTL/LTLParsing/TAPAALLTLQueryParser.jj	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLParsing/TAPAALLTLQueryParser.jj	2021-10-17 18:45:24 +0000
@@ -0,0 +1,294 @@
+options {
+    LOOKAHEAD = 1;
+    CHOICE_AMBIGUITY_CHECK = 2;
+    OTHER_AMBIGUITY_CHECK = 1;
+    STATIC = false;
+    DEBUG_PARSER = false;
+    DEBUG_LOOKAHEAD = false;
+    DEBUG_TOKEN_MANAGER = false;
+    ERROR_REPORTING = true;
+    JAVA_UNICODE_ESCAPE = false;
+    UNICODE_INPUT = false;
+    IGNORE_CASE = false;
+    USER_TOKEN_MANAGER = false;
+    USER_CHAR_STREAM = false;
+    BUILD_PARSER = true;
+    BUILD_TOKEN_MANAGER = true;
+    SANITY_CHECK = true;
+    }
+
+    PARSER_BEGIN(TAPAALLTLQueryParser)
+
+    package dk.aau.cs.TCTL.LTLParsing;
+
+import java.io.StringReader;
+import java.util.ArrayList;
+
+import dk.aau.cs.TCTL.*;
+
+public class TAPAALLTLQueryParser {
+
+    private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query";
+
+    public static TCTLAbstractPathProperty parse(String query) throws ParseException {
+        TAPAALLTLQueryParser parser = new TAPAALLTLQueryParser(new StringReader(query));
+        return parser.Start();
+    }
+}
+
+    PARSER_END(TAPAALLTLQueryParser)
+
+TOKEN :
+    {
+<TRUE: "true" | "TRUE">
+    |
+<FALSE: "false" | "FALSE">
+    }
+
+    TOKEN :
+    {
+<A: "A">
+    |
+<E: "E">
+    |
+<U: "U">
+    |
+<F: "F">
+    |
+<G: "G">
+    |
+<X: "X">
+    }
+
+    TOKEN :
+    {
+<OR: "or" | "||">
+    |
+<AND: "and" | "&&">
+    |
+<NOT: "not" | "!">
+    }
+
+    TOKEN :
+    {
+<PLUS: "+">
+    |
+<MINUS: "-">
+    |
+<MULT: "*">
+    }
+
+    TOKEN :
+    {
+< NUM: ("-")? ( ["0"-"9"] )+ >
+    |
+<IDENT: ["a"-"z","A"-"Z","_"] ( ["a"-"z","A"-"Z","_","0"-"9"] )* >
+    }
+
+    TOKEN :
+    {
+<OP: "<" | "!=" | "<=" | ">" | "=" | "==" | ">=" | ">" >
+    }
+
+    SKIP :
+    {
+    " "
+    | "\t"
+    | "\n"
+    | "\r"
+    }
+
+/** Root production. */
+TCTLAbstractPathProperty Start() :
+{
+        TCTLAbstractPathProperty child = null;
+}
+{
+   child = AbstractPathProperty() <EOF> {return child; }
+}
+
+TCTLAbstractPathProperty AbstractPathProperty() :
+{
+        TCTLAbstractPathProperty pathChild = null;
+        TCTLAbstractStateProperty stateChild = null;
+}
+{
+    <A> pathChild = ParanthesesExpr() {return new LTLANode(new TCTLPathToStateConverter(pathChild)); }
+    | <E> pathChild = ParanthesesExpr() {return new LTLENode(new TCTLPathToStateConverter(pathChild)); }
+}
+
+TCTLAbstractPathProperty ParanthesesExpr() :
+{
+    TCTLAbstractPathProperty pathChild = null;
+            TCTLAbstractStateProperty stateChild = null;
+}
+{
+    "(" pathChild = QuantifierExpr() ")" {return pathChild;}
+    | stateChild = OrExpr() {return new TCTLStateToPathConverter(stateChild); }
+}
+
+TCTLAbstractPathProperty QuantifierExpr() :
+{
+    TCTLAbstractStateProperty child = null;
+    TCTLAbstractStateProperty child2 = null;
+}
+{
+    <F> child = OrExpr() {return new LTLFNode(child); }
+    | <G> child = OrExpr() {return new LTLGNode(child); }
+    | child = OrExpr() <U> child2 = OrExpr() {return new LTLUNode(child, child2); }
+    | <X> child = OrExpr() {return new LTLXNode(child); }
+}
+
+TCTLAbstractStateProperty OrExpr() :
+{
+    TCTLAbstractStateProperty currentChild;
+    ArrayList<TCTLAbstractStateProperty> disjunctions = new ArrayList<TCTLAbstractStateProperty>();
+}
+{
+    currentChild = AndExpr()
+    { disjunctions.add(currentChild); }
+    (
+    <OR> currentChild = AndExpr()
+    { disjunctions.add(currentChild); }
+    )*
+    { return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions); }
+}
+
+TCTLAbstractStateProperty AndExpr() :
+{
+    TCTLAbstractStateProperty currentChild;
+    ArrayList<TCTLAbstractStateProperty> conjunctions = new ArrayList<TCTLAbstractStateProperty>();
+}
+{
+    currentChild = NotExpr()
+    { conjunctions.add(currentChild); }
+    (
+    <AND> currentChild = NotExpr()
+    { conjunctions.add(currentChild); }
+    )*
+    { return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions); }
+}
+
+    TCTLAbstractStateProperty NotExpr() :
+    {
+    TCTLAbstractStateProperty child;
+    TCTLAbstractStateProperty child2 = null;
+    TCTLAbstractPathProperty childConverter;
+    }
+    {
+    <NOT> "(" child = OrExpr() [LOOKAHEAD(2) <U> child2 = OrExpr()] ")" { return new TCTLNotNode(child2 == null ? child : new TCTLPathToStateConverter(new LTLUNode(child, child2))); }
+    | child = Factor() { return child; }
+    | "(" childConverter = QuantifierExpr() ")" { return new TCTLPathToStateConverter(childConverter); }
+    }
+
+    TCTLAbstractStateProperty Factor() :
+    {
+    TCTLAbstractStateProperty thisProp;
+    Token temp = null;
+    Token transition;
+    }
+    {
+    (
+<TRUE> {thisProp = new TCTLTrueNode(); }
+    | <FALSE> {thisProp = new TCTLFalseNode(); }
+    | LOOKAHEAD(AtomicProposition())
+    thisProp = AtomicProposition()
+    | [ LOOKAHEAD(2) temp = <IDENT> "." ] transition = <IDENT> {
+    thisProp = new TCTLTransitionNode(temp == null ? "" : temp.image, transition.image); }
+    | "(" thisProp = OrExpr() ")"
+    | LOOKAHEAD(ParanthesesExpr()) {
+    thisProp = new TCTLPathToStateConverter(QuantifierExpr()); }
+
+    )
+    { return thisProp; }
+    }
+
+    TCTLAbstractStateProperty AtomicProposition() :
+    {
+    TCTLAbstractStateProperty left;
+    TCTLAbstractStateProperty right;
+    Token op;
+    }
+    {
+    (
+    left = AritmeticExpr() op = <OP> right = AritmeticExpr()
+    )
+    {
+    return new TCTLAtomicPropositionNode(left, op.image, right);
+    }
+    }
+
+    TCTLAbstractStateProperty AritmeticExpr() :
+    {
+    TCTLAbstractStateProperty currentChild;
+    ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
+    Token op;
+    }
+    {
+    currentChild = AritmeticMinusExpr()
+    { terms.add(currentChild); }
+    (
+    op = <PLUS> currentChild = AritmeticMinusExpr()
+    {
+    terms.add(new AritmeticOperator(op.image));
+    terms.add(currentChild);
+    }
+    )*
+    { return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms); }
+    }
+
+    TCTLAbstractStateProperty AritmeticMinusExpr() :
+    {
+    TCTLAbstractStateProperty currentChild;
+    ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
+    Token op;
+    }
+    {
+    currentChild = AritmeticTerm()
+    { terms.add(currentChild); }
+    (
+    op = <MINUS> currentChild = AritmeticTerm()
+    {
+    terms.add(new AritmeticOperator(op.image));
+    terms.add(currentChild);
+    }
+    )*
+    { return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms); }
+    }
+
+    TCTLAbstractStateProperty AritmeticTerm() :
+    {
+    TCTLAbstractStateProperty currentChild;
+    ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<TCTLAbstractStateProperty>();
+    Token op;
+    }
+    {
+    currentChild = AritmeticFactor()
+    { factors.add(currentChild); }
+    (
+    op = <MULT> currentChild = AritmeticFactor()
+    {
+    factors.add(new AritmeticOperator(op.image));
+    factors.add(currentChild);
+    }
+    )*
+    { return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors); }
+    }
+
+    TCTLAbstractStateProperty AritmeticFactor() :
+    {
+    TCTLAbstractStateProperty thisProp;
+    Token temp = null;
+    Token place;
+    Token op;
+    Token num;
+    }
+    {
+    (
+    [ LOOKAHEAD(2) temp = <IDENT> "." ] place = <IDENT> { thisProp = new TCTLPlaceNode(temp == null ? "" : temp.image, place.image); }
+    | num = <NUM> { thisProp = new TCTLConstNode(Integer.parseInt(num.image)); }
+    | "(" thisProp = AritmeticExpr() ")"
+    )
+
+    { return thisProp; }
+    }

=== added file 'src/dk/aau/cs/TCTL/LTLUNode.java'
--- src/dk/aau/cs/TCTL/LTLUNode.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLUNode.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,137 @@
+package dk.aau.cs.TCTL;
+
+import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
+
+public class LTLUNode extends TCTLAbstractPathProperty {
+    private TCTLAbstractStateProperty left;
+    private TCTLAbstractStateProperty right;
+
+    public TCTLAbstractStateProperty getLeft() {
+        return this.left;
+    }
+
+    public void setLeft(TCTLAbstractStateProperty left) {
+        this.left = left;
+    }
+
+    public TCTLAbstractStateProperty getRight() {
+        return this.right;
+    }
+
+    public void setRight(TCTLAbstractStateProperty right) {
+        this.right = right;
+    }
+
+    public LTLUNode(TCTLAbstractStateProperty left, TCTLAbstractStateProperty right) {
+        this.left = left;
+        this.right = right;
+        this.left.setParent(this);
+        this.right.setParent(this);
+    }
+
+    public LTLUNode() {
+        left = new TCTLStatePlaceHolder();
+        right = new TCTLStatePlaceHolder();
+        left.setParent(this);
+        right.setParent(this);
+    }
+
+    @Override
+    public String toString() {
+        String leftString = left.isSimpleProperty() ? left.toString() : "("
+            + left.toString() + ")";
+        String rightString = right.isSimpleProperty() ? right.toString() : "("
+            + right.toString() + ")";
+
+        return leftString + " U " + rightString;
+    }
+
+    @Override
+    public StringPosition[] getChildren() {
+        int leftStart = left.isSimpleProperty() ? 0 : 1;
+        leftStart  += 0;
+        int leftEnd = leftStart + left.toString().length();
+        StringPosition leftPos = new StringPosition(leftStart, leftEnd, left);
+
+        int rightStart = right.isSimpleProperty() ? 0 : 1;
+        rightStart += leftEnd + 3 + + (left.isSimpleProperty() ? 0 : 1);
+        int rightEnd = rightStart + right.toString().length();
+        StringPosition rightPos = new StringPosition(rightStart, rightEnd, right);
+
+        StringPosition[] children = { leftPos, rightPos };
+        return children;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty replace(TCTLAbstractProperty object1,
+                                            TCTLAbstractProperty object2) {
+        if (this == object1 && object2 instanceof TCTLAbstractPathProperty) {
+            return (TCTLAbstractPathProperty) object2;
+        } else {
+            left = left.replace(object1, object2);
+            right = right.replace(object1, object2);
+            return this;
+        }
+    }
+
+    @Override
+    public void convertForReducedNet(String templateName) {
+        left.convertForReducedNet(templateName);
+        right.convertForReducedNet(templateName);
+    }
+
+    @Override
+    public boolean isSimpleProperty() {
+        return false;
+    }
+
+    @Override
+    public boolean containsPlaceHolder() {
+        return left.containsPlaceHolder() || right.containsPlaceHolder();
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (o instanceof LTLUNode) {
+            LTLUNode node = (LTLUNode) o;
+            return this.left.equals(node.getLeft())
+                && this.right.equals(node.getRight());
+        }
+        return false;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty copy() {
+        return new LTLUNode(left.copy(), right.copy());
+    }
+
+    @Override
+    public boolean hasNestedPathQuantifiers() {
+        return left instanceof TCTLPathToStateConverter || right instanceof TCTLPathToStateConverter
+            || left.hasNestedPathQuantifiers() || right.hasNestedPathQuantifiers();
+    }
+
+    public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
+        return left.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName)
+            || right.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
+    }
+
+    public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
+        return right.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName) ||
+            left.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
+    }
+
+    @Override
+    public TCTLAbstractProperty findFirstPlaceHolder() {
+        TCTLAbstractProperty result = left.findFirstPlaceHolder();
+        if (result == null){
+            return right.findFirstPlaceHolder();
+        }
+        return result;
+    }
+
+    @Override
+    public void accept(ITCTLVisitor visitor, Object context) {
+        visitor.visit(this, context);
+    }
+}

=== added file 'src/dk/aau/cs/TCTL/LTLXNode.java'
--- src/dk/aau/cs/TCTL/LTLXNode.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/LTLXNode.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,107 @@
+package dk.aau.cs.TCTL;
+
+import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
+
+public class LTLXNode extends TCTLAbstractPathProperty {
+    TCTLAbstractStateProperty property;
+
+    public void setProperty(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public TCTLAbstractStateProperty getProperty() {
+        return property;
+    }
+
+    public LTLXNode(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
+
+    public LTLXNode() {
+        this.property = new TCTLStatePlaceHolder();
+        this.property.setParent(this);
+    }
+
+    @Override
+    public String toString() {
+        String s = property.isSimpleProperty() ? property.toString() : "("
+            + property.toString() + ")";
+        return "X " + s;
+    }
+
+    @Override
+    public StringPosition[] getChildren() {
+        int start = property.isSimpleProperty() ? 0 : 1;
+        start = start + 2;
+        int end = start + property.toString().length();
+        StringPosition position = new StringPosition(start, end, property);
+
+        StringPosition[] children = { position };
+        return children;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty replace(TCTLAbstractProperty object1,
+                                            TCTLAbstractProperty object2) {
+        if (this == object1 && object2 instanceof TCTLAbstractPathProperty) {
+            return (TCTLAbstractPathProperty) object2;
+        } else {
+            property = property.replace(object1, object2);
+            return this;
+        }
+    }
+
+    @Override
+    public boolean isSimpleProperty() {
+        return false;
+    }
+
+    @Override
+    public boolean containsPlaceHolder() {
+        return property.containsPlaceHolder();
+    }
+
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (o instanceof LTLXNode) {
+            LTLXNode node = (LTLXNode) o;
+            return property.equals(node.getProperty());
+        }
+        return false;
+    }
+
+    @Override
+    public TCTLAbstractPathProperty copy() {
+        return new LTLXNode(property.copy());
+    }
+
+    @Override
+    public boolean hasNestedPathQuantifiers() {
+        return property instanceof TCTLPathToStateConverter || property.hasNestedPathQuantifiers();
+    }
+
+    public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
+        return property.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
+    }
+
+    public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
+        return property.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
+    }
+
+    @Override
+    public TCTLAbstractProperty findFirstPlaceHolder() {
+        return property.findFirstPlaceHolder();
+    }
+
+    @Override
+    public void accept(ITCTLVisitor visitor, Object context) {
+        visitor.visit(this, context);
+    }
+}

=== removed file 'src/dk/aau/cs/TCTL/Parsing/ParseException.java'
=== removed file 'src/dk/aau/cs/TCTL/Parsing/SimpleCharStream.java'
=== removed file 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java'
=== renamed file 'src/resources/TCTLParser/TAPAALQueryParser.jj' => 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.jj'
=== removed file 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParserConstants.java'
=== removed file 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParserTokenManager.java'
=== removed file 'src/dk/aau/cs/TCTL/Parsing/Token.java'
=== removed file 'src/dk/aau/cs/TCTL/Parsing/TokenMgrError.java'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/ParseException.java'
=== renamed file 'src/resources/SUMOParser/SUMOParser.jj' => 'src/dk/aau/cs/TCTL/SUMOParsing/SUMOParser.jj'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/SUMOQueryParser.java'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/SUMOQueryParserConstants.java'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/SUMOQueryParserTokenManager.java'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/SimpleCharStream.java'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/Token.java'
=== removed file 'src/dk/aau/cs/TCTL/SUMOParsing/TokenMgrError.java'
=== modified file 'src/dk/aau/cs/TCTL/TCTLAGNode.java'
--- src/dk/aau/cs/TCTL/TCTLAGNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLAGNode.java	2021-10-17 18:45:24 +0000
@@ -4,12 +4,12 @@
 
 public class TCTLAGNode extends TCTLAbstractPathProperty {
 
-	private TCTLAbstractStateProperty property;
+    private TCTLAbstractStateProperty property;
 
-	public void setProperty(TCTLAbstractStateProperty property) {
-		this.property = property;
-		this.property.setParent(this);
-	}
+    public void setProperty(TCTLAbstractStateProperty property) {
+        this.property = property;
+        this.property.setParent(this);
+    }
 
 	public TCTLAbstractStateProperty getProperty() {
 		return property;
@@ -64,7 +64,7 @@
 
 	@Override
 	public TCTLAbstractPathProperty copy() {
-		return new TCTLAGNode(property.copy());
+        return new TCTLAGNode(property.copy());
 	}
 
 	@Override

=== modified file 'src/dk/aau/cs/TCTL/TCTLAbstractProperty.java'
--- src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2021-10-17 18:45:24 +0000
@@ -2,6 +2,8 @@
 
 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
@@ -62,7 +64,6 @@
     public abstract boolean hasNestedPathQuantifiers();
 	// This method assumes that a place holder exists in the current query
 	public abstract TCTLAbstractProperty findFirstPlaceHolder();
-
 	
 
 }

=== added file 'src/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java'
--- src/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,526 @@
+package dk.aau.cs.TCTL.XMLParsing;
+
+import java.util.ArrayList;
+import java.util.Iterator;
+import java.lang.NumberFormatException;
+
+import dk.aau.cs.TCTL.*;
+import dk.aau.cs.debug.Logger;
+
+import org.w3c.dom.NodeList;
+import org.w3c.dom.Node;
+
+public class XMLLTLQueryParser {
+
+    private Node property;
+    private QueryWrapper queryWrapper;
+    private static final String ERROR_MESSAGE = "Could not parse XML tag: ";
+
+    public static boolean parse(Node prop, QueryWrapper queryWrapper){
+
+        XMLLTLQueryParser parser = new XMLLTLQueryParser(prop, queryWrapper);
+        queryWrapper.setName(parser.parsePropertyName());
+
+        try{
+            queryWrapper.setProp(parser.AbstractProperty());
+        } catch (XMLQueryParseException e){
+            queryWrapper.setException(e);
+            Logger.log(e);
+            return false;
+        }
+
+        return true;
+    }
+
+    public static TCTLAbstractProperty parse(Node prop) throws XMLQueryParseException{
+        XMLLTLQueryParser parser = new XMLLTLQueryParser(prop);
+
+        return parser.AbstractProperty();
+    }
+
+    final public TCTLAbstractProperty AbstractProperty() throws XMLQueryParseException{
+        Node formula;
+
+        if((formula = findSubNode("formula", property)) != null){
+            return parseFormula(getFirstChildNode(formula));
+        } else{
+            throw new XMLQueryParseException(ERROR_MESSAGE + property.getNodeName());
+        }
+    }
+
+    private String parsePropertyName(){
+        Node idNode;
+        String result;
+
+        // Find <id> tag and get property name
+        if(((idNode = XMLLTLQueryParser.findSubNode("id", this.property)) == null) ||
+            ((result = XMLLTLQueryParser.getText(idNode)) == null)){
+
+            // If no name was found, set generic name
+            result = "Query Comment/Name Here";
+        }
+
+        return result;
+    }
+
+    private TCTLAbstractProperty parseFormula(Node property)
+        throws XMLQueryParseException{
+
+        TCTLAbstractProperty childProperty;
+        Node child = getFirstChildNode(property);
+        String nodeName = property.getNodeName();
+
+        ArrayList<Node> children;
+
+        if(nodeName.equals("invariant")){
+            childProperty = parseFormula(getFirstChildNode(property));
+            this.queryWrapper.negateQuery();
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                childProperty = new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty);
+            }
+            return new TCTLEFNode(new TCTLNotNode((TCTLAbstractStateProperty)childProperty));
+        } else if(nodeName.equals("impossibility")){
+            childProperty = parseFormula(getFirstChildNode(property));
+            this.queryWrapper.negateQuery();
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                childProperty = new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty);
+            }
+            return new TCTLEFNode((TCTLAbstractStateProperty)childProperty);
+        } else if(nodeName.equals("possibility")){
+            childProperty = parseFormula(getFirstChildNode(property));
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                childProperty = new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty);
+            }
+            return new TCTLEFNode((TCTLAbstractStateProperty)childProperty);
+        } else if(nodeName.equals("all-paths")){
+            childProperty = parseFormula(child);
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                return new LTLANode(new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty));
+            } else{
+                return new LTLANode((TCTLAbstractStateProperty)childProperty);
+            }
+        }  else if(nodeName.equals("exists-path")){
+            childProperty = parseFormula(child);
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                return new LTLENode(new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty));
+            } else{
+                return new LTLENode((TCTLAbstractStateProperty)childProperty);
+            }
+        } else if (nodeName.equals("finally")){
+            childProperty = parseFormula(child);
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                return new LTLFNode(new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty));
+            } else{
+                return new LTLFNode((TCTLAbstractStateProperty)childProperty);
+            }
+        } else if (nodeName.equals("globally")){
+            childProperty = parseFormula(child);
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                return new LTLGNode(new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty));
+            } else{
+                return new LTLGNode((TCTLAbstractStateProperty)childProperty);
+            }
+        } else if (nodeName.equals("next")){
+            childProperty = parseFormula(child);
+            if(childProperty instanceof TCTLAbstractPathProperty){
+                return new LTLXNode(new TCTLPathToStateConverter((TCTLAbstractPathProperty)childProperty));
+            } else{
+                return new LTLXNode((TCTLAbstractStateProperty)childProperty);
+            }
+        } else if (nodeName.equals("until")){
+            children = getAllChildren(property);
+            if(children.size() != 2){
+                Logger.log("ERROR");
+            }
+
+            TCTLAbstractProperty before = parseFormula(getFirstChildNode(children.get(0)));
+            TCTLAbstractProperty reach = parseFormula(getFirstChildNode(children.get(1)));
+
+            if(before instanceof TCTLAbstractPathProperty){
+                before = new TCTLPathToStateConverter((TCTLAbstractPathProperty)before);
+            }
+            if(reach instanceof TCTLAbstractPathProperty){
+                reach = new TCTLPathToStateConverter((TCTLAbstractPathProperty)reach);
+            }
+
+            return new LTLUNode((TCTLAbstractStateProperty)before, (TCTLAbstractStateProperty)reach);
+        } else if(nodeName.equals("true")){
+            return new TCTLTrueNode();
+        } else if(nodeName.equals("false")){
+            return new TCTLFalseNode();
+        } else if(nodeName.equals("negation")){
+            children = getAllChildren(property);
+
+            if(children.size() != 1){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            TCTLAbstractProperty booleanFormulaChild =
+                parseFormula(getFirstChildNode(property));
+            if(booleanFormulaChild instanceof TCTLAbstractPathProperty){
+                booleanFormulaChild = new TCTLPathToStateConverter((TCTLAbstractPathProperty)booleanFormulaChild);
+            }
+            return new TCTLNotNode((TCTLAbstractStateProperty)booleanFormulaChild);
+        } else if(nodeName.equals("conjunction") || nodeName.equals("disjunction")){
+            children = getAllChildren(property);
+
+            if(children.size() < 2){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            ArrayList<TCTLAbstractStateProperty> boolExpList =
+                new ArrayList<TCTLAbstractStateProperty>();
+
+            for (Node n : children){
+                TCTLAbstractProperty p = parseFormula(n);
+                if(p instanceof TCTLAbstractPathProperty){
+                    p = new TCTLPathToStateConverter((TCTLAbstractPathProperty)p);
+                }
+                boolExpList.add((TCTLAbstractStateProperty)p);
+            }
+
+            if(nodeName == "conjunction"){
+                return new TCTLAndListNode(boolExpList);
+            } else{
+                return new TCTLOrListNode(boolExpList);
+            }
+        } else if(nodeName.equals("exclusive-disjunction")){
+            children = getAllChildren(property);
+
+            if(children.size() != 2){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            ArrayList<TCTLAbstractStateProperty> boolExpList =
+                new ArrayList<TCTLAbstractStateProperty>();
+
+            TCTLAbstractProperty left = parseFormula(children.get(0));
+            TCTLAbstractProperty right = parseFormula(children.get(1));
+
+            if(left instanceof TCTLAbstractPathProperty){
+                left = new TCTLPathToStateConverter((TCTLAbstractPathProperty)left);
+            }
+            if(right instanceof TCTLAbstractPathProperty){
+                right = new TCTLPathToStateConverter((TCTLAbstractPathProperty)right);
+            }
+
+            // Parse boolean expressions
+            boolExpList.add((TCTLAbstractStateProperty)left);
+            boolExpList.add((TCTLAbstractStateProperty)right);
+
+            // Build left sub tree
+            TCTLAndListNode leftSubFormula =
+                new TCTLAndListNode(boolExpList.get(0), new TCTLNotNode(boolExpList.get(1)));
+
+            // Build right sub tree
+            TCTLAndListNode rightSubFormula =
+                new TCTLAndListNode(new TCTLNotNode(boolExpList.get(0)), boolExpList.get(1));
+
+            return new TCTLOrListNode(leftSubFormula, rightSubFormula);
+
+        } else if(nodeName.equals("implication")){
+            children = getAllChildren(property);
+
+            if(children.size() != 2){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            ArrayList<TCTLAbstractStateProperty> boolExpList =
+                new ArrayList<TCTLAbstractStateProperty>();
+
+            TCTLAbstractProperty left = parseFormula(children.get(0));
+            TCTLAbstractProperty right = parseFormula(children.get(1));
+
+            if(left instanceof TCTLAbstractPathProperty){
+                left = new TCTLPathToStateConverter((TCTLAbstractPathProperty)left);
+            }
+            if(right instanceof TCTLAbstractPathProperty){
+                right = new TCTLPathToStateConverter((TCTLAbstractPathProperty)right);
+            }
+
+            // Parse boolean expressions
+            boolExpList.add((TCTLAbstractStateProperty)left);
+            boolExpList.add((TCTLAbstractStateProperty)right);
+
+            return new TCTLOrListNode(new TCTLNotNode(boolExpList.get(0)), boolExpList.get(1));
+        } else if(nodeName.equals("equivalence")){
+            children = getAllChildren(property);
+
+            if(children.size() != 2){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            ArrayList<TCTLAbstractStateProperty> boolExpList =
+                new ArrayList<TCTLAbstractStateProperty>();
+
+            TCTLAbstractProperty left = parseFormula(children.get(0));
+            TCTLAbstractProperty right = parseFormula(children.get(1));
+
+            if(left instanceof TCTLAbstractPathProperty){
+                left = new TCTLPathToStateConverter((TCTLAbstractPathProperty)left);
+            }
+            if(right instanceof TCTLAbstractPathProperty){
+                right = new TCTLPathToStateConverter((TCTLAbstractPathProperty)right);
+            }
+
+            // Parse boolean expressions
+            boolExpList.add((TCTLAbstractStateProperty)left);
+            boolExpList.add((TCTLAbstractStateProperty)right);
+
+            // Build left sub tree
+            TCTLAndListNode leftSubFormula =
+                new TCTLAndListNode(boolExpList.get(0), boolExpList.get(1));
+
+            // Build right sub tree
+            TCTLAndListNode rightSubFormula =
+                new TCTLAndListNode(new TCTLNotNode(boolExpList.get(0)), new TCTLNotNode(boolExpList.get(1)));
+
+            return new TCTLOrListNode(leftSubFormula, rightSubFormula);
+        } else if(nodeName.equals("integer-eq") || nodeName.equals("integer-ne") ||
+            nodeName.equals("integer-lt") || nodeName.equals("integer-le") ||
+            nodeName.equals("integer-gt") || nodeName.equals("integer-ge")){
+
+            children = getAllChildren(property);
+
+            if(children.size() != 2){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            TCTLAbstractStateProperty subformula1 = parseIntegerExpression(children.get(0));
+            TCTLAbstractStateProperty subformula2 = parseIntegerExpression(children.get(1));
+
+            if(nodeName.equals("integer-eq")){
+                return new TCTLAtomicPropositionNode(subformula1, "=", subformula2);
+            } else if(nodeName.equals("integer-ne")){
+                return new TCTLAtomicPropositionNode(subformula1, "!=", subformula2);
+            } else if(nodeName.equals("integer-lt")){
+                return new TCTLAtomicPropositionNode(subformula1, "<", subformula2);
+            } else if(nodeName.equals("integer-le")){
+                return new TCTLAtomicPropositionNode(subformula1, "<=", subformula2);
+            } else if(nodeName.equals("integer-gt")){
+                return new TCTLAtomicPropositionNode(subformula1, ">", subformula2);
+            } 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()){
+                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 {
+                    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{
+            parseFormula(property);
+        }
+
+        throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+    }
+
+    private TCTLAbstractStateProperty parseIntegerExpression(Node integerExpression)
+        throws XMLQueryParseException{
+
+        ArrayList<Node> children;
+        String nodeName = integerExpression.getNodeName();
+
+        if(nodeName.equals("integer-constant")){
+            String value;
+            int result;
+
+            if((value = getText(integerExpression)) == null){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            value = value.replace("\n", "");
+
+            try{
+                result = Integer.parseInt(value);
+            } catch (NumberFormatException e){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            return new TCTLConstNode(result);
+        } else if(nodeName.equals("tokens-count")){
+            children = getAllChildren(integerExpression);
+
+            if(children.size() < 1){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            } else if (children.size() == 1) {
+                String[] splits = getText(children.get(0)).replace("\n", "").split("\\.");
+                // Check if place contains a template name
+                if(splits.length > 1){
+                    return new TCTLPlaceNode(splits[0], splits[1]);
+                } else {
+                    return new TCTLPlaceNode(splits[0]);
+                }
+            }
+
+            ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
+            Iterator<Node> itr = children.iterator();
+
+            while(itr.hasNext()){
+                Node n = itr.next();
+                String[] splits = getText(n).replace("\n", "").split("\\.");
+
+                // Check if place contains a template name
+                if(splits.length > 1){
+                    terms.add(new TCTLPlaceNode(splits[0], splits[1]));
+                } else {
+                    terms.add(new TCTLPlaceNode(splits[0]));
+                }
+
+                if(itr.hasNext()){
+                    terms.add(new AritmeticOperator("+"));
+                }
+            }
+
+            return new TCTLTermListNode(terms);
+        } else if(nodeName.equals("integer-sum") || nodeName.equals("integer-product") || nodeName.equals("integer-difference")){
+
+            children = getAllChildren(integerExpression);
+            Iterator<Node> itr = children.iterator();
+
+            if(children.size() < 2){
+                throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+            }
+
+            ArrayList<TCTLAbstractStateProperty> intExpList =
+                new ArrayList<TCTLAbstractStateProperty>();
+
+            while(itr.hasNext()){
+                Node n = itr.next();
+                intExpList.add(parseIntegerExpression(n));
+
+                if(itr.hasNext()){
+                    if(nodeName.equals("integer-sum")){
+                        intExpList.add(new AritmeticOperator("+"));
+                    } else if(nodeName.equals("integer-product")){
+                        intExpList.add(new AritmeticOperator("*"));
+                    } else{
+                        intExpList.add(new AritmeticOperator("-"));
+                    }
+                }
+            }
+
+            return new TCTLTermListNode(intExpList);
+        }
+
+        throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
+    }
+
+    public static Node findSubNode(String name, Node node){
+        if (node.getNodeType() != Node.ELEMENT_NODE) {
+            return null;
+        }
+
+        if (!node.hasChildNodes()){
+            return null;
+        }
+
+        NodeList children = node.getChildNodes();
+
+        for (int i = 0; i < children.getLength(); i++){
+            Node subNode = children.item(i);
+            if (subNode.getNodeType() == Node.ELEMENT_NODE) {
+                if (subNode.getNodeName().equals(name))
+                    return subNode;
+            }
+        }
+
+        return null;
+    }
+
+    private ArrayList<Node> getAllChildren(Node parentNode) {
+        NodeList children = parentNode.getChildNodes();
+        ArrayList<Node> elementNodes = new ArrayList<Node>();
+
+        for (int i = 0; i < children.getLength(); i++) {
+            Node node = children.item(i);
+            if (node.getNodeType() == Node.ELEMENT_NODE) {
+                elementNodes.add(node);
+            }
+        }
+
+        return elementNodes;
+    }
+
+    public static String getText(Node node){
+        String result = null;
+
+        if (!node.hasChildNodes()){
+            return null;
+        }
+
+        NodeList children = node.getChildNodes();
+
+        for (int i = 0; i < children.getLength(); i++){
+            Node subNode = children.item(i);
+            if (subNode.getNodeType() == Node.TEXT_NODE) {
+                result = subNode.getNodeValue();
+            }
+        }
+
+        return result;
+    }
+
+    public int getChildCount(Node node){
+        int result = 0;
+
+        if (!node.hasChildNodes()){
+            return result;
+        }
+
+        NodeList children = node.getChildNodes();
+
+        for (int i = 0; i < children.getLength(); i++){
+            Node subNode = children.item(i);
+            if (subNode.getNodeType() == Node.ELEMENT_NODE) {
+                result++;
+            }
+        }
+
+        return result;
+    }
+
+    private Node getFirstChildNode(Node parent){
+        Node child = parent.getFirstChild();
+
+        while (child != null && child.getNodeType() != Node.ELEMENT_NODE){
+            child = child.getNextSibling();
+        }
+
+        return child;
+    }
+
+    public XMLLTLQueryParser(Node prop, QueryWrapper qw){
+        this.property = prop;
+        this.queryWrapper = qw;
+    }
+
+    public XMLLTLQueryParser(Node prop){
+        this.property = prop;
+    }
+}

=== modified file 'src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java	2019-03-22 10:13:18 +0000
+++ src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java	2021-10-17 18:45:24 +0000
@@ -63,6 +63,10 @@
             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";
@@ -128,6 +132,32 @@
 		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));
+        afNode.getProperty().accept(this, context);
+        XMLQuery.append(endTag(XML_FINALLY) + endTag(XML_ALLPATHS));
+    }
+
+    public void visit(LTLGNode 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(LTLXNode 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(LTLUNode 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(TCTLPathToStateConverter pathConverter, Object context) {
 		pathConverter.getProperty().accept(this, context);

=== modified file 'src/dk/aau/cs/TCTL/visitors/ITCTLVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/ITCTLVisitor.java	2016-05-02 09:06:57 +0000
+++ src/dk/aau/cs/TCTL/visitors/ITCTLVisitor.java	2021-10-17 18:45:24 +0000
@@ -1,30 +1,6 @@
 package dk.aau.cs.TCTL.visitors;
 
-import dk.aau.cs.TCTL.AritmeticOperator;
-import dk.aau.cs.TCTL.TCTLAFNode;
-import dk.aau.cs.TCTL.TCTLAGNode;
-import dk.aau.cs.TCTL.TCTLAXNode;
-import dk.aau.cs.TCTL.TCTLAUNode;
-import dk.aau.cs.TCTL.TCTLAndListNode;
-import dk.aau.cs.TCTL.TCTLAtomicPropositionNode;
-import dk.aau.cs.TCTL.TCTLConstNode;
-import dk.aau.cs.TCTL.TCTLDeadlockNode;
-import dk.aau.cs.TCTL.TCTLEFNode;
-import dk.aau.cs.TCTL.TCTLEGNode;
-import dk.aau.cs.TCTL.TCTLEXNode;
-import dk.aau.cs.TCTL.TCTLEUNode;
-import dk.aau.cs.TCTL.TCTLFalseNode;
-import dk.aau.cs.TCTL.TCTLNotNode;
-import dk.aau.cs.TCTL.TCTLOrListNode;
-import dk.aau.cs.TCTL.TCTLPathPlaceHolder;
-import dk.aau.cs.TCTL.TCTLPathToStateConverter;
-import dk.aau.cs.TCTL.TCTLPlaceNode;
-import dk.aau.cs.TCTL.TCTLPlusListNode;
-import dk.aau.cs.TCTL.TCTLStatePlaceHolder;
-import dk.aau.cs.TCTL.TCTLStateToPathConverter;
-import dk.aau.cs.TCTL.TCTLTermListNode;
-import dk.aau.cs.TCTL.TCTLTransitionNode;
-import dk.aau.cs.TCTL.TCTLTrueNode;
+import dk.aau.cs.TCTL.*;
 
 public interface ITCTLVisitor {
 	void visit(TCTLAFNode afNode, Object context);
@@ -35,6 +11,14 @@
 	
 	void visit(TCTLAUNode auNode, Object context);
 
+    void visit(LTLFNode afNode, Object context);
+
+    void visit(LTLGNode agNode, Object context);
+
+    void visit(LTLXNode axNode, Object context);
+
+    void visit(LTLUNode auNode, Object context);
+
 	void visit(TCTLEFNode efNode, Object context);
 
 	void visit(TCTLEGNode egNode, Object context);
@@ -74,4 +58,8 @@
 	void visit(TCTLConstNode tctlConstNode, Object context);
 
 	void visit(TCTLTermListNode tctlTermListNode, Object context);
+
+    void visit(LTLANode ltlaNode, Object context);
+
+    void visit(LTLENode ltleNode, Object context);
 }

=== added file 'src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java'
--- src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,233 @@
+package dk.aau.cs.TCTL.visitors;
+
+import java.util.List;
+
+import dk.aau.cs.TCTL.*;
+import dk.aau.cs.io.XMLFormatter;
+
+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_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 LTLQueryVisitor() {
+        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 String getFormatted(StringBuffer CTLQueries) {
+        XMLFormatter formatter = new XMLFormatter();
+        XMLQuery.append(CTLQueries);
+        return formatter.format(getStartTag() + XMLQuery.toString() + getEndTag());
+    }
+
+    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(LTLANode aNode, Object context) {
+        XMLQuery.append(startTag(XML_ALLPATHS));
+        aNode.getProperty().accept(this, context);
+        XMLQuery.append(endTag(XML_ALLPATHS));
+    }
+
+    public void visit(LTLENode eNode, Object context) {
+        XMLQuery.append(startTag(XML_EXISTSPATH));
+        eNode.getProperty().accept(this, context);
+        XMLQuery.append(endTag(XML_EXISTSPATH));
+    }
+
+    public void visit(LTLFNode afNode, Object context) {
+        XMLQuery.append(startTag(XML_FINALLY));
+        afNode.getProperty().accept(this, context);
+        XMLQuery.append(endTag(XML_FINALLY));
+    }
+
+    public void visit(LTLGNode agNode, Object context) {
+        XMLQuery.append(startTag(XML_GLOBALLY));
+        agNode.getProperty().accept(this, context);
+        XMLQuery.append(endTag(XML_GLOBALLY));
+    }
+
+    public void visit(LTLXNode axNode, Object context) {
+        XMLQuery.append(startTag(XML_NEXT));
+        axNode.getProperty().accept(this, context);
+        XMLQuery.append(endTag(XML_NEXT));
+    }
+
+    public void visit(LTLUNode auNode, Object context) {
+        XMLQuery.append(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));
+    }
+
+    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 + "/");
+    }
+}

=== modified file 'src/dk/aau/cs/TCTL/visitors/VisitorBase.java'
--- src/dk/aau/cs/TCTL/visitors/VisitorBase.java	2016-05-02 09:06:57 +0000
+++ src/dk/aau/cs/TCTL/visitors/VisitorBase.java	2021-10-17 18:45:24 +0000
@@ -1,31 +1,6 @@
 package dk.aau.cs.TCTL.visitors;
 
-import dk.aau.cs.TCTL.AritmeticOperator;
-import dk.aau.cs.TCTL.TCTLAFNode;
-import dk.aau.cs.TCTL.TCTLAGNode;
-import dk.aau.cs.TCTL.TCTLAXNode;
-import dk.aau.cs.TCTL.TCTLAUNode;
-import dk.aau.cs.TCTL.TCTLAbstractStateProperty;
-import dk.aau.cs.TCTL.TCTLAndListNode;
-import dk.aau.cs.TCTL.TCTLAtomicPropositionNode;
-import dk.aau.cs.TCTL.TCTLConstNode;
-import dk.aau.cs.TCTL.TCTLDeadlockNode;
-import dk.aau.cs.TCTL.TCTLEFNode;
-import dk.aau.cs.TCTL.TCTLEGNode;
-import dk.aau.cs.TCTL.TCTLEXNode;
-import dk.aau.cs.TCTL.TCTLEUNode;
-import dk.aau.cs.TCTL.TCTLFalseNode;
-import dk.aau.cs.TCTL.TCTLNotNode;
-import dk.aau.cs.TCTL.TCTLOrListNode;
-import dk.aau.cs.TCTL.TCTLPathPlaceHolder;
-import dk.aau.cs.TCTL.TCTLPathToStateConverter;
-import dk.aau.cs.TCTL.TCTLPlaceNode;
-import dk.aau.cs.TCTL.TCTLPlusListNode;
-import dk.aau.cs.TCTL.TCTLStatePlaceHolder;
-import dk.aau.cs.TCTL.TCTLStateToPathConverter;
-import dk.aau.cs.TCTL.TCTLTermListNode;
-import dk.aau.cs.TCTL.TCTLTransitionNode;
-import dk.aau.cs.TCTL.TCTLTrueNode;
+import dk.aau.cs.TCTL.*;
 
 public abstract class VisitorBase implements ITCTLVisitor {
 
@@ -33,8 +8,15 @@
 		atomicPropositionNode.getLeft().accept(this, context);
 		atomicPropositionNode.getRight().accept(this, context);
 	}
-	
-	public void visit(TCTLAFNode afNode, Object context) { afNode.getProperty().accept(this, context); }
+
+    public void visit(LTLANode aNode, Object context) { aNode.getProperty().accept(this, context); }
+    public void visit(LTLENode eNode, Object context) { eNode.getProperty().accept(this, context); }
+    public void visit(LTLFNode afNode, Object context) { afNode.getProperty().accept(this, context); }
+    public void visit(LTLGNode agNode, Object context) { agNode.getProperty().accept(this, context); }
+    public void visit(LTLXNode axNode, Object context) { axNode.getProperty().accept(this, context); }
+    public void visit(LTLUNode auNode, Object context) { auNode.getLeft().accept(this, context);
+                                                            auNode.getRight().accept(this, context);  }
+    public void visit(TCTLAFNode afNode, Object context) { afNode.getProperty().accept(this, context); }
 	public void visit(TCTLAGNode agNode, Object context) { agNode.getProperty().accept(this, context); }
 	public void visit(TCTLAXNode axNode, Object context) { axNode.getProperty().accept(this, context); }
 	public void visit(TCTLAUNode auNode, Object context) { auNode.getLeft().accept(this, context); 

=== modified file 'src/dk/aau/cs/gui/BatchProcessingDialog.java'
--- src/dk/aau/cs/gui/BatchProcessingDialog.java	2021-03-02 16:02:35 +0000
+++ src/dk/aau/cs/gui/BatchProcessingDialog.java	2021-10-17 18:45:24 +0000
@@ -1581,6 +1581,10 @@
             s.append("Trace Abstract Refinement: ");
             s.append(query.isTarOptionEnabled() ? "Yes\n\n" : "No\n\n");
 
+            s.append("\n\n");
+            s.append("USe Tarjan: ");
+            s.append(query.isTarjan() ? "Yes\n\n" : "No\n\n");
+
 			s.append("Query Property:\n");
                         s.append(query.getProperty().toString());
 			

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2021-09-29 10:00:54 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2021-10-17 18:45:24 +0000
@@ -19,7 +19,7 @@
 import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
 import dk.aau.cs.gui.components.NameVisibilityPanel;
 import dk.aau.cs.gui.components.StatisticsPanel;
-import dk.aau.cs.gui.components.TransitionFireingComponent;
+import dk.aau.cs.gui.components.TransitionFiringComponent;
 import dk.aau.cs.gui.undo.*;
 import dk.aau.cs.io.*;
 import dk.aau.cs.io.queries.SUMOQueryLoader;
@@ -691,6 +691,11 @@
                 q.setReductionOption(ReductionOption.VerifyPN);
                 q.setUseOverApproximationEnabled(false);
                 q.setUseUnderApproximationEnabled(false);
+            } else {
+                if (q.getCategory() == TAPNQuery.QueryCategory.LTL) {
+                    queriesToRemove.add(q);
+                    tab.removeQuery(q);
+                }
             }
         }
         String message = "";
@@ -836,9 +841,9 @@
 	private JScrollPane animationControllerScrollPane;
 	private AnimationHistoryList abstractAnimationPane = null;
 	private JPanel animationControlsPanel;
-	private TransitionFireingComponent transitionFireing;
+	private TransitionFiringComponent transitionFiring;
 
-	private static final String transitionFireingName = "enabledTransitions";
+	private static final String transitionFiringName = "enabledTransitions";
 	private static final String animControlName = "animControl";
 
 	private JSplitPane animationHistorySplitter;
@@ -1126,14 +1131,14 @@
 		if (animControlerBox == null) {
             createAnimationControlSidePanel();
         }
-		if (transitionFireing == null) {
-            createTransitionFireing();
+		if (transitionFiring == null) {
+            createTransitionFiring();
         }
 		
 		boolean floatingDividers = false;
 		if(simulatorModelRoot == null){
 			Leaf templateExplorerLeaf = new Leaf(templateExplorerName);
-			Leaf enabledTransitionsListLeaf = new Leaf(transitionFireingName);
+			Leaf enabledTransitionsListLeaf = new Leaf(transitionFiringName);
 			Leaf animControlLeaf = new Leaf(animControlName);
 
 			templateExplorerLeaf.setWeight(0.25);
@@ -1181,10 +1186,10 @@
 				animationControlsPanel.getMinimumSize().height
             )
         );
-		transitionFireing.setPreferredSize(
+		transitionFiring.setPreferredSize(
 		    new Dimension(
-				transitionFireing.getPreferredSize().width,
-				transitionFireing.getMinimumSize().height
+				transitionFiring.getPreferredSize().width,
+				transitionFiring.getMinimumSize().height
             )
         );
 
@@ -1194,7 +1199,7 @@
         animatorSplitPane.add(new JPanel(), templateExplorerName);
 
 		animatorSplitPane.add(animationControlsPanel, animControlName);
-		animatorSplitPane.add(transitionFireing, transitionFireingName);
+		animatorSplitPane.add(transitionFiring, transitionFiringName);
 		
 		animatorSplitPaneScroller = createLeftScrollPane(animatorSplitPane);
 		animatorSplitPane.repaint();
@@ -1265,7 +1270,7 @@
 	}
 	
 	public DelayEnabledTransitionControl getDelayEnabledTransitionControl(){
-		return transitionFireing.getDelayEnabledTransitionControl();
+		return transitionFiring.getDelayEnabledTransitionControl();
 	}
 
 	public void addAbstractAnimationPane() {
@@ -1322,12 +1327,12 @@
 		return animationHistorySidePanel.getAnimationHistoryList();
 	}
 
-	private void createTransitionFireing() {
-		transitionFireing = new TransitionFireingComponent(CreateGui.getApp().isShowingDelayEnabledTransitions(), lens);
+	private void createTransitionFiring() {
+		transitionFiring = new TransitionFiringComponent(CreateGui.getApp().isShowingDelayEnabledTransitions(), lens);
 	}
 
-	public TransitionFireingComponent getTransitionFireingComponent() {
-		return transitionFireing;
+	public TransitionFiringComponent getTransitionFiringComponent() {
+		return transitionFiring;
 	}
 
     public TimedArcPetriNetNetwork network() {
@@ -1498,13 +1503,13 @@
 	public void showEnabledTransitionsList(boolean enable) {
 	    //displayNode fires and relayout, so we check of value is changed
         // else elements will be set to default size.
-		if (transitionFireing.isVisible() != enable) {
-			animatorSplitPane.getMultiSplitLayout().displayNode(transitionFireingName, enable);
+		if (transitionFiring.isVisible() != enable) {
+			animatorSplitPane.getMultiSplitLayout().displayNode(transitionFiringName, enable);
 		}
 	}
 	
 	public void showDelayEnabledTransitions(boolean enable){
-		transitionFireing.showDelayEnabledTransitions(enable);
+		transitionFiring.showDelayEnabledTransitions(enable);
 		drawingSurface.repaint();
 		
 		CreateGui.getAnimator().updateFireableTransitions();
@@ -2064,7 +2069,7 @@
 
 	@Override
 	public void delayAndFire() {
-		getTransitionFireingComponent().fireSelectedTransition();
+		getTransitionFiringComponent().fireSelectedTransition();
 	}
 
     @Override

=== removed file 'src/dk/aau/cs/gui/components/TransitionFireingComponent.java'
=== added file 'src/dk/aau/cs/gui/components/TransitionFiringComponent.java'
--- src/dk/aau/cs/gui/components/TransitionFiringComponent.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/gui/components/TransitionFiringComponent.java	2021-10-17 18:45:24 +0000
@@ -0,0 +1,169 @@
+package dk.aau.cs.gui.components;
+
+import java.awt.Dimension;
+import java.awt.GridBagConstraints;
+import java.awt.GridBagLayout;
+import java.awt.event.KeyAdapter;
+import java.awt.event.KeyEvent;
+
+import javax.swing.BorderFactory;
+import javax.swing.JButton;
+import javax.swing.JPanel;
+
+import dk.aau.cs.gui.TabContent;
+import pipe.dataLayer.Template;
+import pipe.gui.AnimationSettingsDialog;
+import pipe.gui.DelayEnabledTransitionControl;
+import pipe.gui.CreateGui;
+import pipe.gui.SimulationControl;
+import pipe.gui.graphicElements.Transition;
+
+public class TransitionFiringComponent extends JPanel {
+
+	private final EnabledTransitionsList enabledTransitionsList;
+	private final JButton fireButton;
+	private final JButton settingsButton;
+	private final TabContent.TAPNLens lens;
+
+	public TransitionFiringComponent(boolean showDelayEnabledTransitions, TabContent.TAPNLens lens) {
+		super(new GridBagLayout());
+		enabledTransitionsList = new EnabledTransitionsList();
+        this.lens = lens;
+		this.setBorder(
+		    BorderFactory.createCompoundBorder(
+				BorderFactory.createTitledBorder("Enabled Transitions"),
+				BorderFactory.createEmptyBorder(3, 3, 3, 3)
+            )
+        );
+		this.setToolTipText("List of currently enabled transitions (double click a transition to fire it)");
+		enabledTransitionsList.setPreferredSize(
+		    new Dimension(
+				enabledTransitionsList.getPreferredSize().width,
+				enabledTransitionsList.getMinimumSize().height
+            )
+        );
+
+		settingsButton = new JButton("Settings");
+		settingsButton.setPreferredSize(new Dimension(0, settingsButton.getPreferredSize().height)); //Make the two buttons equal in size
+		settingsButton.addActionListener(e -> AnimationSettingsDialog.showAnimationSettings(lens));
+
+		fireButton = new JButton("Delay & Fire");
+		fireButton.setPreferredSize(new Dimension(0, fireButton.getPreferredSize().height)); //Make the two buttons equal in size
+		fireButton.addActionListener(e -> {
+			if(SimulationControl.getInstance().randomSimulation() && CreateGui.getApp().isShowingDelayEnabledTransitions()){
+				SimulationControl.startSimulation();
+			} else {
+				fireSelectedTransition();
+			}
+		});
+
+		fireButton.addKeyListener(new KeyAdapter() {			
+			@Override
+			public void keyPressed(KeyEvent e) {
+				if(e.getKeyCode() == KeyEvent.VK_ENTER){
+					if(SimulationControl.getInstance().randomSimulation()){
+						SimulationControl.startSimulation();
+					} else {
+						fireSelectedTransition();
+					}
+				}
+			}
+		});
+
+		GridBagConstraints gbc = new GridBagConstraints();
+		gbc.gridx = 0;
+		gbc.gridy = 0;
+		gbc.fill = GridBagConstraints.BOTH;
+		gbc.gridwidth = 2;
+		gbc.weightx = 1;
+		gbc.weighty = 1;
+		gbc.anchor = GridBagConstraints.NORTHWEST;
+		this.add(enabledTransitionsList, gbc);
+
+		gbc = new GridBagConstraints();
+		gbc.gridx = 0;
+		gbc.gridy = 1;
+		gbc.weightx = 1;
+		gbc.fill = GridBagConstraints.HORIZONTAL;
+		gbc.anchor = GridBagConstraints.SOUTHWEST;
+		this.add(settingsButton, gbc);
+
+		gbc = new GridBagConstraints();
+		gbc.gridx = 1;
+		gbc.gridy = 1;
+		gbc.weightx = 1;
+		gbc.fill = GridBagConstraints.HORIZONTAL;
+		gbc.anchor = GridBagConstraints.SOUTHWEST;
+		this.add(fireButton, gbc);
+
+		showDelayEnabledTransitions(showDelayEnabledTransitions);
+	}
+
+	public static final String FIRE_BUTTON_DEACTIVATED_TOOL_TIP = "No transitions are enabled";
+	public static final String FIRE_BUTTON_ENABLED_TOOL_TIP = "Press to fire the selected transition";
+	public static final String SIMULATE_DEACTIVATED_TOOL_TIP = "Not able to simulate from this marking, no transitions are enabled";
+	public static final String SIMULATE_ACTIVATED_TOOL_TIP = "Do a random simulation of the net";
+
+	public void updateFireButton(){
+		//If the simulation is running deactivate the firebutton.
+		if(SimulationControl.getInstance().isRunning()){
+			fireButton.setEnabled(false);
+			return;
+		}
+		
+		//Make sure the firebutton is enabled
+		fireButton.setEnabled(true);
+		
+		//If random simulation is enabled
+		if(CreateGui.getApp().isShowingDelayEnabledTransitions() && SimulationControl.getInstance().randomSimulation()){
+			fireButton.setText("Simulate");
+			
+			if(enabledTransitionsList.getNumberOfTransitions() == 0){
+				fireButton.setEnabled(false);
+				fireButton.setToolTipText(SIMULATE_DEACTIVATED_TOOL_TIP);
+			} else {
+				fireButton.setEnabled(true);
+				fireButton.setToolTipText(SIMULATE_ACTIVATED_TOOL_TIP);
+			}
+		} else { //If random simulation is not enabled.
+			fireButton.setText(CreateGui.getApp().isShowingDelayEnabledTransitions()  ? "Delay & Fire" : "Fire");
+			if(!lens.isTimed()){
+			    fireButton.setText("Fire");
+            }
+
+			if(enabledTransitionsList.getNumberOfTransitions() == 0){
+				fireButton.setEnabled(false);
+				fireButton.setToolTipText(FIRE_BUTTON_DEACTIVATED_TOOL_TIP);
+			} else {
+				fireButton.setEnabled(true);
+				fireButton.setToolTipText(FIRE_BUTTON_ENABLED_TOOL_TIP);
+			}
+		}
+	}
+
+	public void addTransition(Template template, Transition transition){
+		enabledTransitionsList.addTransition(template, transition);
+	}
+
+	public void startReInit(){
+		enabledTransitionsList.startReInit();
+	}
+
+	public void reInitDone(){
+		updateFireButton();
+		enabledTransitionsList.reInitDone();
+	}
+
+	public DelayEnabledTransitionControl getDelayEnabledTransitionControl() {
+		return DelayEnabledTransitionControl.getInstance();
+	}
+
+	public void showDelayEnabledTransitions(boolean enable) {
+		settingsButton.setVisible(enable);
+		updateFireButton();
+	}
+	
+	public void fireSelectedTransition(){
+		enabledTransitionsList.fireSelectedTransition();
+	}
+}

=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
--- src/dk/aau/cs/io/TapnXmlLoader.java	2021-09-29 10:04:23 +0000
+++ src/dk/aau/cs/io/TapnXmlLoader.java	2021-10-17 18:45:24 +0000
@@ -140,8 +140,10 @@
 		Collection<Template> templates = parseTemplates(doc, network, constants);
 		LoadedQueries loadedQueries = new TAPNQueryLoader(doc, network).parseQueries();
 
-		for(String message : loadedQueries.getMessages()){
-		    messages.add(message);
+		if (loadedQueries != null) {
+            for (String message : loadedQueries.getMessages()) {
+                messages.add(message);
+            }
         }
 		network.buildConstraints();
 		

=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2021-03-02 16:05:51 +0000
+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2021-10-17 18:45:24 +0000
@@ -17,6 +17,7 @@
 import javax.xml.transform.dom.DOMSource;
 import javax.xml.transform.stream.StreamResult;
 
+import dk.aau.cs.TCTL.visitors.LTLQueryVisitor;
 import dk.aau.cs.gui.TabContent;
 import org.w3c.dom.Attr;
 import org.w3c.dom.DOMException;
@@ -287,7 +288,9 @@
 			Element newQuery;
 			if (query.getCategory() == QueryCategory.CTL){
 				newQuery = createCTLQueryElement(query, document);
-			} else {
+			} else if (query.getCategory() == QueryCategory.LTL){
+			    newQuery = createLTLQueryElement(query, document);
+            }else {
 				newQuery = createQueryElement(query, document);
 			}
 			root.appendChild(newQuery);
@@ -336,7 +339,7 @@
 		queryElement.appendChild(document.importNode(queryFormula, true));
 		
 		queryElement.setAttribute("name", query.getName());
-		queryElement.setAttribute("type", "CTL");
+		queryElement.setAttribute("type", query.getCategory().toString());
 		queryElement.setAttribute("capacity", "" + query.getCapacity());
 		queryElement.setAttribute("traceOption", ""	+ query.getTraceOption());
 		queryElement.setAttribute("searchOption", "" + query.getSearchOption());
@@ -360,9 +363,49 @@
 		queryElement.setAttribute("useQueryReduction", "" + query.isQueryReductionEnabled());
 		queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
 		queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled());
-		
-		return queryElement;
+        queryElement.setAttribute("useTarjan", "" + query.isTarjan());
+
+        return queryElement;
 	}
+
+    private Element createLTLQueryElement(TAPNQuery query, Document document) {
+        Require.that(query != null, "Error: query was null");
+        Require.that(document != null, "Error: document was null");
+
+        Element queryElement = document.createElement("query");
+
+        Node queryFormula = XMLQueryStringToElement(new LTLQueryVisitor().getXMLQueryFor(query.getProperty(), query.getName()));
+        queryElement.appendChild(document.importNode(queryFormula, true));
+
+        queryElement.setAttribute("name", query.getName());
+        queryElement.setAttribute("type", query.getCategory().toString());
+        queryElement.setAttribute("capacity", "" + query.getCapacity());
+        queryElement.setAttribute("traceOption", ""	+ query.getTraceOption());
+        queryElement.setAttribute("searchOption", "" + query.getSearchOption());
+        queryElement.setAttribute("hashTableSize", "" + query.getHashTableSize());
+        queryElement.setAttribute("extrapolationOption", "" + query.getExtrapolationOption());
+        queryElement.setAttribute("reductionOption", ""	+ query.getReductionOption());
+        queryElement.setAttribute("symmetry", "" + query.useSymmetry());
+        queryElement.setAttribute("gcd", "" + query.useGCD());
+        queryElement.setAttribute("timeDarts", "" + query.useTimeDarts());
+        queryElement.setAttribute("pTrie", "" + query.usePTrie());
+        queryElement.setAttribute("discreteInclusion", String.valueOf(query.discreteInclusion()));
+        queryElement.setAttribute("active", "" + query.isActive());
+        queryElement.setAttribute("inclusionPlaces", getInclusionPlacesString(query));
+        queryElement.setAttribute("overApproximation", "" + query.useOverApproximation());
+        queryElement.setAttribute("reduction", "" + query.useReduction());
+        queryElement.setAttribute("enableOverApproximation", "" + query.isOverApproximationEnabled());
+        queryElement.setAttribute("enableUnderApproximation", "" + query.isUnderApproximationEnabled());
+        queryElement.setAttribute("approximationDenominator", "" + query.approximationDenominator());
+        queryElement.setAttribute("algorithmOption", "" + query.getAlgorithmOption());
+        queryElement.setAttribute("useSiphonTrapAnalysis", "" + query.isSiphontrapEnabled());
+        queryElement.setAttribute("useQueryReduction", "" + query.isQueryReductionEnabled());
+        queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
+        queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled());
+        queryElement.setAttribute("useTarjan", "" + query.isTarjan());
+
+        return queryElement;
+    }
 	
 	private Node XMLQueryStringToElement(String formulaString){
 		

=== modified file 'src/dk/aau/cs/io/queries/QueryLoader.java'
--- src/dk/aau/cs/io/queries/QueryLoader.java	2020-10-30 12:00:55 +0000
+++ src/dk/aau/cs/io/queries/QueryLoader.java	2021-10-17 18:45:24 +0000
@@ -37,6 +37,7 @@
 	
 	public LoadedQueries parseQueries() {
 		ArrayList<TAPNQuery> queries = getQueries();
+		if (queries == null) return null;
 		
 		ArrayList<Tuple<String, String>> templatePlaceNames = getPlaceNames(network);
 		ArrayList<Tuple<String, String>> templateTransitionNames = getTransitionNames(network);

=== modified file 'src/dk/aau/cs/io/queries/TAPNQueryLoader.java'
--- src/dk/aau/cs/io/queries/TAPNQueryLoader.java	2021-03-02 16:05:51 +0000
+++ src/dk/aau/cs/io/queries/TAPNQueryLoader.java	2021-10-17 18:45:24 +0000
@@ -1,12 +1,10 @@
 package dk.aau.cs.io.queries;
 
-import java.awt.*;
 import java.util.ArrayList;
 import java.util.List;
 
-import javax.swing.JOptionPane;
-
-import dk.aau.cs.debug.Logger;
+import dk.aau.cs.TCTL.*;
+import dk.aau.cs.TCTL.XMLParsing.XMLLTLQueryParser;
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
 import org.w3c.dom.Node;
@@ -19,22 +17,9 @@
 import pipe.dataLayer.TAPNQuery.QueryCategory;
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
-import pipe.gui.CreateGui;
-import pipe.gui.MessengerImpl;
 import pipe.gui.widgets.InclusionPlaces;
 import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
-import dk.aau.cs.TCTL.StringPosition;
-import dk.aau.cs.TCTL.TCTLAUNode;
-import dk.aau.cs.TCTL.TCTLAXNode;
-import dk.aau.cs.TCTL.TCTLAbstractProperty;
-import dk.aau.cs.TCTL.TCTLAbstractStateProperty;
-import dk.aau.cs.TCTL.TCTLEUNode;
-import dk.aau.cs.TCTL.TCTLEXNode;
-import dk.aau.cs.TCTL.TCTLPathToStateConverter;
-import dk.aau.cs.TCTL.TCTLStateToPathConverter;
 import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser;
-import dk.aau.cs.TCTL.TCTLPlusListNode;
-import dk.aau.cs.TCTL.TCTLTransitionNode;
 import dk.aau.cs.TCTL.XMLParsing.XMLCTLQueryParser;
 import dk.aau.cs.TCTL.XMLParsing.XMLQueryParseException;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
@@ -87,14 +72,19 @@
 		InclusionPlaces inclusionPlaces = getInclusionPlaces(queryElement, network);
 		boolean reduction = getReductionOption(queryElement, "reduction", true);
 		String algorithmOption = queryElement.getAttribute("algorithmOption");
-		boolean isCTL = isCTLQuery(queryElement);
+        boolean isCTL = isTypeQuery(queryElement, "CTL");
+        boolean isLTL = isTypeQuery(queryElement, "LTL");
 		boolean siphontrap = getReductionOption(queryElement, "useSiphonTrapAnalysis", false);
 		boolean queryReduction = getReductionOption(queryElement, "useQueryReduction", true);
 		boolean stubborn = getReductionOption(queryElement, "useStubbornReduction", true);
-		boolean useTar = getTarOption(queryElement, "useTarOption", false);
+		boolean useTar = getAttributeOption(queryElement, "useTarOption", false);
+        boolean useTarjan = getAttributeOption(queryElement, "useTarjan", false);
 
 		TCTLAbstractProperty query;
-		if (queryElement.getElementsByTagName("formula").item(0) != null){
+		if (queryElement.hasAttribute("type") && queryElement.getAttribute("type").equals("LTL")) {
+		    query = parseLTLQueryProperty(queryElement);
+        }
+		else if (queryElement.getElementsByTagName("formula").item(0) != null){
 			query = parseCTLQueryProperty(queryElement);
 		} else {
 			query = parseQueryProperty(queryElement.getAttribute("query"));
@@ -104,11 +94,12 @@
 			TAPNQuery parsedQuery = new TAPNQuery(comment, capacity, query, traceOption, searchOption, reductionOption, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, hashTableSize, extrapolationOption, inclusionPlaces, isOverApproximationEnabled, isUnderApproximationEnabled, approximationDenominator);
 			parsedQuery.setActive(active);
 			parsedQuery.setDiscreteInclusion(discreteInclusion);
-			parsedQuery.setCategory(detectCategory(query, isCTL));
+			parsedQuery.setCategory(detectCategory(query, isCTL, isLTL));
 			parsedQuery.setUseSiphontrap(siphontrap);
 			parsedQuery.setUseQueryReduction(queryReduction);
 			parsedQuery.setUseStubbornReduction(stubborn);
-			parsedQuery.setUseTarOption(useTar);
+            parsedQuery.setUseTarOption(useTar);
+            parsedQuery.setUseTarjan(useTarjan);
 			if (parsedQuery.getCategory() == QueryCategory.CTL && algorithmOption != null){
 				parsedQuery.setAlgorithmOption(AlgorithmOption.valueOf(algorithmOption));
 //				RenameTemplateVisitor rt = new RenameTemplateVisitor("", 
@@ -120,45 +111,53 @@
 			return null;
 	}
 	
-	public static TAPNQuery.QueryCategory detectCategory(TCTLAbstractProperty query, boolean isCTL){
-                if (isCTL) return TAPNQuery.QueryCategory.CTL;
-                
-                StringPosition[] children = query.getChildren();
-
-                // If query is root and state property
-                if(query instanceof TCTLAbstractStateProperty){
-                        if(((TCTLAbstractStateProperty) query).getParent() == null){
-                                return TAPNQuery.QueryCategory.CTL;
-                        }
-                }
-        
-		if(query instanceof TCTLStateToPathConverter ||
+	public static TAPNQuery.QueryCategory detectCategory(TCTLAbstractProperty query, boolean isCTL, boolean isLTL){
+        if (isCTL) return TAPNQuery.QueryCategory.CTL;
+        if (isLTL) return QueryCategory.LTL;
+
+        StringPosition[] children = query.getChildren();
+
+        // If query is root and state property
+        if(query instanceof TCTLAbstractStateProperty){
+            if(((TCTLAbstractStateProperty) query).getParent() == null){
+                return TAPNQuery.QueryCategory.CTL;
+            }
+        }
+
+        if(query instanceof TCTLStateToPathConverter ||
 				query instanceof TCTLPathToStateConverter){
 			return TAPNQuery.QueryCategory.CTL;
 		}
 
-		if(query instanceof TCTLEUNode ||
-				query instanceof TCTLEXNode ||
+		if(query instanceof LTLGNode ||
+                query instanceof LTLFNode ||
+                query instanceof LTLUNode ||
+                query instanceof LTLXNode ||
+                query instanceof LTLANode ||
+                query instanceof LTLENode){
+            return TAPNQuery.QueryCategory.LTL;
+        } else if(query instanceof TCTLEUNode ||
+                query instanceof TCTLEXNode ||
 				query instanceof TCTLAUNode ||
-				query instanceof TCTLAXNode){
-			return TAPNQuery.QueryCategory.CTL;
-		}
-                
-                // If query is a fireability query
-                if(query instanceof TCTLTransitionNode) {
-                    return TAPNQuery.QueryCategory.CTL;
+				query instanceof TCTLAXNode) {
+            return TAPNQuery.QueryCategory.CTL;
+        }
+
+        // If query is a fireability query
+        if(query instanceof TCTLTransitionNode) {
+            return TAPNQuery.QueryCategory.CTL;
+        }
+        if(query instanceof TCTLPlusListNode){
+                for(TCTLAbstractStateProperty sp : ((TCTLPlusListNode)query).getProperties()) {
+                        if(TAPNQueryLoader.detectCategory(sp, isCTL, isLTL) == TAPNQuery.QueryCategory.CTL){
+                            return TAPNQuery.QueryCategory.CTL;
+                        }
                 }
-                if(query instanceof TCTLPlusListNode){
-                        for(TCTLAbstractStateProperty sp : ((TCTLPlusListNode)query).getProperties()) {
-                                if(TAPNQueryLoader.detectCategory(sp, isCTL) == TAPNQuery.QueryCategory.CTL){
-                                    return TAPNQuery.QueryCategory.CTL;
-                                }
-                        }
 		}
 		
                 // If any property has been converted
 		for (StringPosition child : children) {
-			if(TAPNQueryLoader.detectCategory(child.getObject(), isCTL) == TAPNQuery.QueryCategory.CTL){
+			if(TAPNQueryLoader.detectCategory(child.getObject(), isCTL, isLTL) == TAPNQuery.QueryCategory.CTL){
 				return TAPNQuery.QueryCategory.CTL;
 			} 
 		}
@@ -206,13 +205,18 @@
 		return new InclusionPlaces(InclusionPlacesOption.UserSpecified, places);
 	}
         
-	private boolean isCTLQuery(Element queryElement) {
+	private boolean isTypeQuery(Element queryElement, String type) {
 		if(!queryElement.hasAttribute("type")){
-			return false;
+		    if (type.equals("CTL")) {
+		        return XMLQueryLoader.canBeCTL(queryElement) && !XMLQueryLoader.canBeLTL(queryElement);
+            } else if (type.equals("LTL")) {
+                return !XMLQueryLoader.canBeCTL(queryElement) && XMLQueryLoader.canBeLTL(queryElement);
+            }
+            return false;
 		}
 		boolean result;
 		try {
-			result = queryElement.getAttribute("type").equals("CTL");
+			result = queryElement.getAttribute("type").equals(type);
 		} catch(Exception e) {
 			result = false;
 		}
@@ -232,7 +236,7 @@
 		return result;	
 	}
 
-	private boolean getTarOption(Element queryElement, String attributeName, boolean defaultValue) {
+	private boolean getAttributeOption(Element queryElement, String attributeName, boolean defaultValue) {
         if(!queryElement.hasAttribute(attributeName)){
             return defaultValue;
         }
@@ -244,8 +248,8 @@
         }
         return result;
     }
-	
-	private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
+
+    private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
 	{
 		if(!queryElement.hasAttribute(attributeName)){
 			return defaultValue;
@@ -294,6 +298,17 @@
 		return query;
 	}
 
+    private TCTLAbstractProperty parseLTLQueryProperty(Node queryElement){
+        TCTLAbstractProperty query = null;
+        try {
+            query = XMLLTLQueryParser.parse(queryElement);
+        } catch (XMLQueryParseException e) {
+            messages.add(ERROR_PARSING_QUERY_MESSAGE);
+        }
+
+        return query;
+    }
+
 	private TCTLAbstractProperty parseQueryProperty(String queryToParse) {
 		TCTLAbstractProperty query = null;
 		try {

=== modified file 'src/dk/aau/cs/io/queries/XMLQueryLoader.java'
--- src/dk/aau/cs/io/queries/XMLQueryLoader.java	2020-10-09 07:59:49 +0000
+++ src/dk/aau/cs/io/queries/XMLQueryLoader.java	2021-10-17 18:45:24 +0000
@@ -3,9 +3,9 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.Collection;
 import javax.swing.JOptionPane;
 
+import dk.aau.cs.TCTL.XMLParsing.XMLLTLQueryParser;
 import dk.aau.cs.io.LoadedQueries;
 import pipe.dataLayer.TAPNQuery;
 import pipe.dataLayer.TAPNQuery.ExtrapolationOption;
@@ -80,6 +80,7 @@
 
         // Get all properties from DOM
         NodeList propList = doc.getElementsByTagName("property");
+        int choice = -1;
 
         for(int i = 0; i < propList.getLength(); i++){
             Node prop = propList.item(i);
@@ -88,13 +89,43 @@
             // Save query for later use in dialog window
             this.faultyQueries.add(queryWrapper);
 
+            boolean canBeCTL = canBeCTL(prop);
+            boolean canBeLTL = canBeLTL(prop);
+
+            if (canBeCTL && canBeLTL && choice == -1) {
+                choice = JOptionPane.showOptionDialog(CreateGui.getApp(),
+                    "There were some queries that can be classified both as LTL and CTL. \nHow do you want to import them?",
+                    "Choose query category",
+                    JOptionPane.YES_NO_CANCEL_OPTION,
+                    JOptionPane.QUESTION_MESSAGE,
+                    null,
+                    new Object[]{"Import all as CTL", "Import all as LTL", "Cancel"},
+                    0);
+            } else if (!canBeCTL && !canBeLTL) {
+                JOptionPane.showMessageDialog(CreateGui.getApp(),
+                    "One or more queries do not have the correct format.");
+            }
+                if (choice == 2) return null;
+
+
+            boolean isCTL = (canBeCTL && !canBeLTL) || (canBeCTL && canBeLTL && choice == 0);
+            boolean isLTL = (!canBeCTL && canBeLTL) || (canBeCTL && canBeLTL && choice == 1 );
+
+
             // Update queryWrapper name and property
-            if(!XMLCTLQueryParser.parse(prop, queryWrapper)){
-                queries.add(null); 
-                continue; 
+            if (isCTL) {
+                if (!XMLCTLQueryParser.parse(prop, queryWrapper)) {
+                    queries.add(null);
+                    continue;
+                }
+            } else if (isLTL) {
+                if (!XMLLTLQueryParser.parse(prop, queryWrapper)) {
+                    queries.add(null);
+                    continue;
+                }
             }
 
-            // The number 9999 is the number of extra tokens allowed, 
+            // The number 9999 is the number of extra tokens allowed,
             // this is set high s.t. we don't have to change it manually
             TAPNQuery query = new TAPNQuery(queryWrapper.getName(), 9999,
                 queryWrapper.getProp(),TraceOption.NONE, SearchOption.HEURISTIC, 
@@ -103,9 +134,10 @@
 
             RenameTemplateVisitor rt = new RenameTemplateVisitor("", 
                 network.activeTemplates().get(0).name());
-            query.setCategory(TAPNQueryLoader.detectCategory(queryWrapper.getProp(), false));
+
+            query.setCategory(TAPNQueryLoader.detectCategory(queryWrapper.getProp(), isCTL, isLTL));
             
-            if(query.getCategory() == TAPNQuery.QueryCategory.CTL){
+            if(query.getCategory() == TAPNQuery.QueryCategory.CTL || query.getCategory() == TAPNQuery.QueryCategory.LTL){
             	query.setSearchOption(SearchOption.DFS);
             	query.setUseReduction(true);
             }
@@ -118,12 +150,72 @@
         return queries;
     }
 
+    public static boolean canBeCTL(Node prop) {
+        NodeList children = prop.getChildNodes();
+        boolean correctQuantifiers = false;
+
+        for (int i = 0; i < children.getLength(); i++) {
+            Node child = children.item(i);
+            if (child.getNodeName().equals("formula")) {
+                correctQuantifiers = checkQuantifiers(child);
+            }
+        }
+        return correctQuantifiers;
+    }
+
+    private static boolean checkQuantifiers(Node prop) {
+        NodeList children = prop.getChildNodes();
+
+        for (int i = 0; i < children.getLength(); i++) {
+            Node child = children.item(i);
+            if (child.getNodeName().equals("finally") || child.getNodeName().equals("globally") ||
+                child.getNodeName().equals("next") || child.getNodeName().equals("until")) {
+                Node parent = child.getParentNode();
+                if (parent == null || !(parent.getNodeName().equals("all-paths") || parent.getNodeName().equals("exists-path"))) {
+                    return false;
+                }
+            }
+            if (!checkQuantifiers(child)) return false;
+        }
+        return true;
+    }
+
+    public static boolean canBeLTL(Node prop) {
+        NodeList children = prop.getChildNodes();
+        int allPathsCounter = 0;
+
+        for (int i = 0; i < children.getLength(); i++) {
+            Node child = children.item(i);
+            if (child.getNodeName().equals("formula")) {
+                allPathsCounter += countAllPaths(child);
+            }
+        }
+        return allPathsCounter == 1;
+    }
+
+    private static int countAllPaths(Node prop) {
+        NodeList children = prop.getChildNodes();
+        int allPathsCounter = 0;
+
+        for (int i = 0; i < children.getLength(); i++) {
+            Node child = children.item(i);
+            if (child.getNodeName().equals("all-paths")) {
+                allPathsCounter++;
+            } else if (child.getNodeName().equals("exists-path") || child.getNodeName().equals("deadlock")){
+                return 100;
+            }
+            allPathsCounter += countAllPaths(child);
+        }
+        return allPathsCounter;
+    }
+
     public static void importQueries(File file, TimedArcPetriNetNetwork network){
         XMLQueryLoader loader = new XMLQueryLoader(file, network);
 
         // Suppress default error message
         loader.showErrorMessage = false;
         LoadedQueries loadedQueries = loader.parseQueries();
+        if (loadedQueries == null) return;
 	
         for(TAPNQuery query : loadedQueries.getQueries()){
             CreateGui.getCurrentTab().addQuery(query);

=== modified file 'src/dk/aau/cs/verification/ReductionStats.java'
--- src/dk/aau/cs/verification/ReductionStats.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/ReductionStats.java	2021-10-17 18:45:24 +0000
@@ -29,7 +29,7 @@
 
 	}
 	
-	public int getRemovedTrantitions() {
+	public int getRemovedTransitions() {
 		return removedTrantitions;
 	}
 

=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2020-12-17 21:03:12 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2021-10-17 18:45:24 +0000
@@ -183,7 +183,7 @@
 
 	public boolean reductionRulesApplied(){
         ReductionStats reductionStats = stats.getReductionStats();
-        return (reductionStats.getRemovedPlaces() + reductionStats.getRemovedTrantitions()) > 0;
+        return (reductionStats.getRemovedPlaces() + reductionStats.getRemovedTransitions()) > 0;
     }
 	
 	public NetworkMarking getCoveredMarking(TimedArcPetriNetNetwork model){

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2020-12-17 21:03:12 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2021-10-17 18:45:24 +0000
@@ -11,6 +11,7 @@
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
+import dk.aau.cs.TCTL.*;
 import dk.aau.cs.gui.TabContent;
 import net.tapaal.Preferences;
 import net.tapaal.TAPAAL;
@@ -24,8 +25,6 @@
 import pipe.gui.widgets.InclusionPlaces;
 import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption;
 import dk.aau.cs.Messenger;
-import dk.aau.cs.TCTL.TCTLAFNode;
-import dk.aau.cs.TCTL.TCTLEGNode;
 import dk.aau.cs.model.tapn.LocalTimedPlace;
 import dk.aau.cs.model.tapn.TAPNQuery;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
@@ -333,7 +332,16 @@
 				} else {
 					ctlOutput = queryResult.value1().isCTL;
 					boolean approximationResult = queryResult.value2().discoveredStates() == 0;	// Result is from over-approximation
-					TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
+                    TimedArcPetriNetTrace tapnTrace;
+                    if (!errorOutput.contains("Trace") && standardOutput.contains("<trace>")) {
+                        String trace = "Trace:\n";
+                        trace += (standardOutput.split("(?=<trace>)")[1]);
+                        trace = trace.split("(?<=</trace>)")[0];
+					    tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1());
+                    } else {
+                        tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
+
+                    }
 					return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput);
 				}
 			}
@@ -396,7 +404,7 @@
 		}
 	
 		public boolean supportsQuery(TimedArcPetriNet model, TAPNQuery query, VerificationOptions options) {
-			if(query.getCategory() == QueryCategory.CTL){
+			if(query.getCategory() == QueryCategory.CTL || query.getCategory() == QueryCategory.LTL){
 				return true;
 			}
 			if(query.getProperty() instanceof TCTLEGNode || query.getProperty() instanceof TCTLAFNode) {

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-08-24 11:06:31 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2021-10-17 18:45:24 +0000
@@ -21,10 +21,11 @@
 	private boolean useStubbornReduction = true;
 	private boolean useTarOption;
 	private String pathToReducedNet;
+	private boolean useTarjan = true;
 	
 	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
                            boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
-                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet, boolean useTarOption) {
+                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet, boolean useTarOption, boolean useTarjan) {
 		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, useTarOption);
 		this.modelReduction = modelReduction;
 		this.queryCategory = queryCategory;
@@ -34,20 +35,21 @@
 		this.useStubbornReduction = stubbornReduction;
 		this.useTarOption = useTarOption;
 		this.pathToReducedNet = pathToReducedNet;
+		this.useTarjan = useTarjan;
 	}
 
 	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
                            boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
                            boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {
 		this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, 
-			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false);
+			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false, true);
 	}
 
     public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
                            boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
                            boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, boolean useTarOption) {
         this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
-            enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, useTarOption);
+            enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, useTarOption, true);
     }
 
 	@Override
@@ -78,7 +80,13 @@
 		if (this.queryCategory == QueryCategory.CTL){
 			result.append(" -ctl " + (getAlgorithmOption() == AlgorithmOption.CERTAIN_ZERO ? "czero" : "local"));
 			result.append(" -x 1");
-		}
+		} else if (this.queryCategory == QueryCategory.LTL) {
+            result.append(" -ltl");
+            if (!this.useTarjan) {
+                result.append(" ndfs");
+            }
+            result.append(" -x 1");
+        }
 		
 		if (this.useSiphontrap) {
 			result.append(" -a 10 ");

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2021-09-22 15:56:33 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2021-10-17 18:45:24 +0000
@@ -7,6 +7,7 @@
 import java.util.Collection;
 import java.util.List;
 
+import dk.aau.cs.TCTL.visitors.LTLQueryVisitor;
 import dk.aau.cs.gui.TabContent;
 import dk.aau.cs.verification.NameMapping;
 import pipe.dataLayer.DataLayer;
@@ -32,7 +33,8 @@
 	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens, NameMapping mapping) {
 		File modelFile = createTempFile(".xml");
 		File queryFile;
-		if (query.getCategory() == QueryCategory.CTL){
+
+		if (query.getCategory() == QueryCategory.CTL || query.getCategory() == QueryCategory.LTL){
 			queryFile = createTempFile(".xml");
 		} else {
 			queryFile = createTempFile(".q");
@@ -59,6 +61,9 @@
             } else if (query.getCategory() == QueryCategory.CTL) {
                 CTLQueryVisitor XMLVisitor = new CTLQueryVisitor();
                 queryStream.append(XMLVisitor.getXMLQueryFor(query.getProperty(), null));
+            } else if (query.getCategory() == QueryCategory.LTL) {
+                LTLQueryVisitor XMLVisitor = new LTLQueryVisitor();
+                queryStream.append(XMLVisitor.getXMLQueryFor(query.getProperty(), null));
             } else if (lens != null && lens.isGame()) {
                 queryStream.append("control: " + query.getProperty().toString());
             } else {

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2021-02-06 17:11:07 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2021-10-17 18:45:24 +0000
@@ -16,7 +16,7 @@
 	protected int tokensInModel;
 	private final boolean symmetry;
 	private final boolean discreteInclusion;
-	private final boolean tarOption;
+    private final boolean tarOption;
 	private InclusionPlaces inclusionPlaces;
 	
 	//only used for boundedness analysis
@@ -44,7 +44,7 @@
 		this.enabledOverApproximation = enableOverApproximation;
 		this.enabledUnderApproximation = enableUnderApproximation;
 		this.approximationDenominator = approximationDenominator;
-		this.tarOption = tarOption;
+        this.tarOption = tarOption;
 	}
 
 	public TraceOption trace() {

=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2021-03-02 16:02:35 +0000
+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2021-10-17 18:45:24 +0000
@@ -356,7 +356,8 @@
 				boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions();
 				boolean overApproximation = query.isOverApproximationEnabled();
 				boolean underApproximation = query.isUnderApproximationEnabled();
-				boolean useTar = query.isTarOptionEnabled();
+                boolean useTar = query.isTarOptionEnabled();
+                boolean useTarjan = query.isTarjan();
 				int approximationDenominator = query.approximationDenominator();
 				if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) {
 					overApproximation = false;
@@ -382,7 +383,8 @@
 				changedQuery.setUseSiphontrap(query.isSiphontrapEnabled());
 				changedQuery.setUseQueryReduction(query.isQueryReductionEnabled());
 				changedQuery.setUseStubbornReduction(stubbornReduction);
-				changedQuery.setUseTarOption(useTar);
+                changedQuery.setUseTarOption(useTar);
+                changedQuery.setUseTarjan(useTarjan);
 				return changedQuery;
 			} else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness) {
 				isSoundnessCheck = true;

=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java	2021-03-02 16:02:35 +0000
+++ src/pipe/dataLayer/TAPNQuery.java	2021-10-17 18:45:24 +0000
@@ -33,7 +33,7 @@
 	}
 	
 	public enum QueryCategory{
-		Default, CTL
+		Default, CTL, LTL
 	}
 	
 	public enum AlgorithmOption{
@@ -72,7 +72,8 @@
 	private boolean useSiphontrap = false; 
 	private boolean useQueryReduction = true; 
 	private boolean useStubbornReduction = true;
-	private boolean useTarOption = false;
+    private boolean useTarOption = false;
+    private boolean useTarjan = false;
 
 	/**
 	 * @param name
@@ -117,6 +118,14 @@
 	    this.useTarOption = useTarOption;
     }
 
+    public boolean isTarjan() {
+        return this.useTarjan;
+    }
+
+    public void setUseTarjan(boolean useTarjan) {
+        this.useTarjan = useTarjan;
+    }
+
 	public int approximationDenominator() {
 		return this.denominator;
 	}

=== modified file 'src/pipe/gui/AnimationSettingsDialog.java'
--- src/pipe/gui/AnimationSettingsDialog.java	2020-08-17 06:18:11 +0000
+++ src/pipe/gui/AnimationSettingsDialog.java	2021-10-17 18:45:24 +0000
@@ -29,7 +29,7 @@
 			if(simControl.randomSimulation()){
 				simControl.randomMode.setSelected(true);
 			}
-			CreateGui.getCurrentTab().getTransitionFireingComponent().updateFireButton();
+			CreateGui.getCurrentTab().getTransitionFiringComponent().updateFireButton();
 		});
 		
 		content.add(delayEnabled, BorderLayout.NORTH);

=== modified file 'src/pipe/gui/Animator.java'
--- src/pipe/gui/Animator.java	2020-08-10 09:34:06 +0000
+++ src/pipe/gui/Animator.java	2021-10-17 18:45:24 +0000
@@ -16,7 +16,7 @@
 import pipe.gui.widgets.AnimationTokenSelectDialog;
 import pipe.gui.widgets.EscapableDialog;
 import dk.aau.cs.gui.TabContent;
-import dk.aau.cs.gui.components.TransitionFireingComponent;
+import dk.aau.cs.gui.components.TransitionFiringComponent;
 import dk.aau.cs.model.tapn.NetworkMarking;
 import dk.aau.cs.model.tapn.TimeInterval;
 import dk.aau.cs.model.tapn.TimedInputArc;
@@ -69,19 +69,26 @@
     public void setTrace(TAPNNetworkTrace trace) {
         CreateGui.getCurrentTab().setAnimationMode(true);
 
-        if (trace.isConcreteTrace()) {
-            this.trace = trace;
-            setTimedTrace(trace);
-        } else {
-            setUntimedTrace(trace);
-            isDisplayingUntimedTrace = true;
+        try {
+            if (trace.isConcreteTrace()) {
+                this.trace = trace;
+                setTimedTrace(trace);
+            } else {
+                setUntimedTrace(trace);
+                isDisplayingUntimedTrace = true;
+            }
+            currentAction = -1;
+            currentMarkingIndex = 0;
+            tab.network().setMarking(markings.get(currentMarkingIndex));
+            tab.getAnimationHistorySidePanel().setSelectedIndex(0);
+            updateAnimationButtonsEnabled();
+            updateFireableTransitions();
+        } catch (RequireException e) {
+            unhighlightDisabledTransitions();
+            CreateGui.getCurrentTab().toggleAnimationMode();
+            JOptionPane.showMessageDialog(CreateGui.getApp(), "There was an error in the trace. Reason: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);
+            return;
         }
-        currentAction = -1;
-        currentMarkingIndex = 0;
-        tab.network().setMarking(markings.get(currentMarkingIndex));
-        tab.getAnimationHistorySidePanel().setSelectedIndex(0);
-        updateAnimationButtonsEnabled();
-        updateFireableTransitions();
     }
 
     private void setUntimedTrace(TAPNNetworkTrace trace) {
@@ -111,7 +118,7 @@
         for (TAPNNetworkTraceStep step : trace) {
             addMarking(step, step.performStepFrom(currentMarking()));
         }
-        if(getTrace().getTraceType() != TraceType.NOT_EG){ //If the trace was not explicitly set, maybe we have calculated it is deadlock.
+        if (getTrace().getTraceType() != TraceType.NOT_EG) { //If the trace was not explicitly set, maybe we have calculated it is deadlock.
             tab.getAnimationHistorySidePanel().setLastShown(getTrace().getTraceType());
         }
     }
@@ -141,7 +148,7 @@
     }
 
     public void updateFireableTransitions(){
-        TransitionFireingComponent transFireComponent = tab.getTransitionFireingComponent();
+        TransitionFiringComponent transFireComponent = tab.getTransitionFiringComponent();
         transFireComponent.startReInit();
         isUrgentTransitionEnabled = false;
 
@@ -180,7 +187,7 @@
         for(Template template : tab.allTemplates())
         {
             for (Transition tempTransition : template.guiModel().transitions()) {
-                tempTransition.disableHightligh();
+                tempTransition.disableHightlight();
 
                 tempTransition.repaint();
             }

=== modified file 'src/pipe/gui/Export.java'
--- src/pipe/gui/Export.java	2020-12-17 21:03:12 +0000
+++ src/pipe/gui/Export.java	2021-10-17 18:45:24 +0000
@@ -7,6 +7,7 @@
 package pipe.gui;
 
 import dk.aau.cs.TCTL.CTLParsing.TAPAALCTLQueryParser;
+import dk.aau.cs.TCTL.LTLParsing.TAPAALLTLQueryParser;
 import dk.aau.cs.TCTL.TCTLAbstractProperty;
 import dk.aau.cs.TCTL.TCTLPathPlaceHolder;
 import java.awt.image.BufferedImage;
@@ -34,6 +35,7 @@
 import javax.xml.transform.TransformerConfigurationException;
 import javax.xml.transform.TransformerException;
 
+import dk.aau.cs.TCTL.visitors.*;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.util.Tuple;
 import dk.aau.cs.verification.VerifyTAPN.ExportedVerifyTAPNModel;
@@ -43,9 +45,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.w3c.dom.DOMException;
 
-import dk.aau.cs.TCTL.visitors.CTLQueryVisitor;
-import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
-import dk.aau.cs.TCTL.visitors.RenameAllTransitionsVisitor;
 import dk.aau.cs.gui.TabContent;
 import dk.aau.cs.io.PNMLWriter;
 import dk.aau.cs.model.tapn.NetworkMarking;
@@ -107,23 +106,35 @@
             NameMapping mapping = composer.transformModel(network).value2();
             Iterator<TAPNQuery> queryIterator = queries.iterator();
             PrintStream queryStream = new PrintStream(filename);
-            CTLQueryVisitor XMLVisitor = new CTLQueryVisitor();
+            LTLQueryVisitor LTLXMLVisitor = new LTLQueryVisitor();
+            CTLQueryVisitor CTLXMLVisitor = new CTLQueryVisitor();
 
             while (queryIterator.hasNext()) {
+                boolean isCTL = false;
                 TAPNQuery clonedQuery = queryIterator.next().copy();
 
                 // Attempt to parse and possibly transform the string query using the manual edit parser
                 TCTLAbstractProperty newProperty;
                 try {
-                    newProperty = TAPAALCTLQueryParser.parse(clonedQuery.getProperty().toString());
+                    if (clonedQuery.getCategory().equals(TAPNQuery.QueryCategory.LTL)) {
+                        newProperty = TAPAALLTLQueryParser.parse(clonedQuery.getProperty().toString());
+                    } else {
+                        newProperty = TAPAALCTLQueryParser.parse(clonedQuery.getProperty().toString());
+                        isCTL = true;
+                    }
                 } catch (Throwable ex) {
                     newProperty = clonedQuery == null ? new TCTLPathPlaceHolder() : clonedQuery.getProperty();
                 }
                 newProperty.accept(new RenameAllPlacesVisitor(mapping), null);
                 newProperty.accept(new RenameAllTransitionsVisitor(mapping), null);
-                XMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName());
+
+                if (!isCTL) {
+                    LTLXMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName());
+                } else {
+                    CTLXMLVisitor.buildXMLQuery(newProperty, clonedQuery.getName());
+                }
             }
-            queryStream.print(XMLVisitor.getFormatted());
+            queryStream.append(LTLXMLVisitor.getFormatted(CTLXMLVisitor.getXMLQuery()));
 
             queryStream.close();
         } catch (FileNotFoundException e) {

=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
--- src/pipe/gui/KBoundAnalyzer.java	2021-10-02 12:05:32 +0000
+++ src/pipe/gui/KBoundAnalyzer.java	2021-10-17 18:45:24 +0000
@@ -67,7 +67,7 @@
 
 	protected VerifyTAPNOptions verificationOptions() {
 		if(modelChecker instanceof VerifyPN){
-			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null, false);
+			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null, false, true);
 		} else if(modelChecker instanceof VerifyTAPN){
 			return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
 		} else if(modelChecker instanceof VerifyTAPNDiscreteVerification){

=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java	2021-08-25 10:11:18 +0000
+++ src/pipe/gui/RunVerification.java	2021-10-17 18:45:24 +0000
@@ -46,7 +46,18 @@
 
 	@Override
 	protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {
-		if (result != null && !result.error()) {
+        if (reduceNetOnly) {
+            //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
+            if (result != null && result.stats().transitionsCount() == 0 && result.stats().placeBoundCount() == 0) {
+                JOptionPane.showMessageDialog(
+                    CreateGui.getApp(),
+                    createMessagePanel(result),
+                    "Verification Result",
+                    JOptionPane.INFORMATION_MESSAGE,
+                    iconSelector.getIconFor(result)
+                );
+            }
+        } else if (result != null && !result.error()) {
 			if(callback != null){
 				callback.run(result);
 			}else{
@@ -63,9 +74,7 @@
 				}
 			}
 
-		} else if(reduceNetOnly) {
-            //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
-        }else{
+		} else {
 			
 			//Check if the is something like 
 			//verifyta: relocation_error:

=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java	2021-09-23 11:36:16 +0000
+++ src/pipe/gui/RunVerificationBase.java	2021-10-17 18:45:24 +0000
@@ -128,7 +128,8 @@
 										dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
 										dataLayerQuery.isStubbornReductionEnabled(),
                                         reducedNetFilePath,
-                                        dataLayerQuery.isTarOptionEnabled()
+                                        dataLayerQuery.isTarOptionEnabled(),
+                                        dataLayerQuery.isTarjan()
 								),
 								transformedModel,
 								clonedQuery
@@ -150,7 +151,8 @@
                                         pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
 										false,
                                         reducedNetFilePath,
-                                        false
+                                        false,
+                                        true
 								),
 								transformedModel,
 								clonedQuery
@@ -219,7 +221,7 @@
 			firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
 
 			if (showResult(result) && spinner != null) {
-			    options = new VerifyPNOptions(options.extraTokens(), pipe.dataLayer.TAPNQuery.TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, pipe.dataLayer.TAPNQuery.QueryCategory.Default, pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime, false, null, false);
+			    options = new VerifyPNOptions(options.extraTokens(), pipe.dataLayer.TAPNQuery.TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, pipe.dataLayer.TAPNQuery.QueryCategory.Default, pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime, false, null, false, false);
                 KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner);
                 optimizer.analyze((VerifyTAPNOptions) options, true);
             }

=== modified file 'src/pipe/gui/SimulationControl.java'
--- src/pipe/gui/SimulationControl.java	2020-08-17 06:18:11 +0000
+++ src/pipe/gui/SimulationControl.java	2021-10-17 18:45:24 +0000
@@ -23,7 +23,7 @@
 	final JSlider simulationSpeed = new JSlider();
 	final JCheckBox randomSimulation = new JCheckBox("Enable automatic random simulation");
     final JCheckBox randomMode = new JCheckBox("Choose next transition randomly");
-    final Timer timer = new Timer(simulationSpeed.getValue()*20, e -> CreateGui.getCurrentTab().getTransitionFireingComponent().fireSelectedTransition());
+    final Timer timer = new Timer(simulationSpeed.getValue()*20, e -> CreateGui.getCurrentTab().getTransitionFiringComponent().fireSelectedTransition());
     private static boolean defaultIsRandomTrasition;
     private static SimulationControl instance;
 	
@@ -114,12 +114,12 @@
 	
 	public void start(){
 		timer.start();
-		CreateGui.getCurrentTab().getTransitionFireingComponent().updateFireButton();
+		CreateGui.getCurrentTab().getTransitionFiringComponent().updateFireButton();
 	}
 	
 	public void stop(){
 		timer.stop();
-		CreateGui.getCurrentTab().getTransitionFireingComponent().updateFireButton();
+		CreateGui.getCurrentTab().getTransitionFiringComponent().updateFireButton();
 	}
 	
 	public boolean isRunning(){

=== modified file 'src/pipe/gui/Verifier.java'
--- src/pipe/gui/Verifier.java	2021-02-07 11:09:51 +0000
+++ src/pipe/gui/Verifier.java	2021-10-17 18:45:24 +0000
@@ -185,44 +185,24 @@
                 return;
             }
 
-            if (onlyCreateReducedNet) {
-                //These options should disable the verification and only produce the net after applying reduction rules
-                verifytapnOptions = new VerifyPNOptions(
-                    bound,
-                    query.getTraceOption(),
-                    TAPNQuery.SearchOption.OVERAPPROXIMATE,
-                    query.useOverApproximation(),
-                    query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
-                    query.isOverApproximationEnabled(),
-                    query.isUnderApproximationEnabled(),
-                    query.approximationDenominator(),
-                    query.getCategory(),
-                    query.getAlgorithmOption(),
-                    query.isSiphontrapEnabled(),
-                    TAPNQuery.QueryReductionTime.NoTime,
-                    query.isStubbornReductionEnabled(),
-                    reducedNetTempFile.getAbsolutePath(),
-                    query.isTarOptionEnabled()
-                );
-            } else {
-                verifytapnOptions = new VerifyPNOptions(
-                    bound,
-                    query.getTraceOption(),
-                    query.getSearchOption(),
-                    query.useOverApproximation(),
-                    query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
-                    query.isOverApproximationEnabled(),
-                    query.isUnderApproximationEnabled(),
-                    query.approximationDenominator(),
-                    query.getCategory(),
-                    query.getAlgorithmOption(),
-                    query.isSiphontrapEnabled(),
-                    query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
-                    query.isStubbornReductionEnabled(),
-                    reducedNetTempFile.getAbsolutePath(),
-                    query.isTarOptionEnabled()
-                );
-            }
+            verifytapnOptions = new VerifyPNOptions(
+                bound,
+                query.getTraceOption(),
+                query.getSearchOption(),
+                query.useOverApproximation(),
+                query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
+                query.isOverApproximationEnabled(),
+                query.isUnderApproximationEnabled(),
+                query.approximationDenominator(),
+                query.getCategory(),
+                query.getAlgorithmOption(),
+                query.isSiphontrapEnabled(),
+                query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
+                query.isStubbornReductionEnabled(),
+                reducedNetTempFile.getAbsolutePath(),
+                query.isTarOptionEnabled(),
+                query.isTarjan()
+            );
 		} else {
 			verifytapnOptions = new VerifyTAPNOptions(
 					bound,

=== modified file 'src/pipe/gui/graphicElements/Transition.java'
--- src/pipe/gui/graphicElements/Transition.java	2020-10-30 12:10:06 +0000
+++ src/pipe/gui/graphicElements/Transition.java	2021-10-17 18:45:24 +0000
@@ -156,7 +156,7 @@
 	public abstract TimeInterval getDInterval();
 
     /* Called at the end of animation to reset Transitions to false */
-	public void disableHightligh() {
+	public void disableHightlight() {
 		highlightedEnabled = false;
         highlightedDelayEnabled = false;
 	}

=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2021-10-04 17:31:24 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2021-10-17 18:45:24 +0000
@@ -31,6 +31,7 @@
 
 import dk.aau.cs.TCTL.*;
 import dk.aau.cs.TCTL.CTLParsing.TAPAALCTLQueryParser;
+import dk.aau.cs.TCTL.LTLParsing.TAPAALLTLQueryParser;
 import dk.aau.cs.TCTL.visitors.*;
 import dk.aau.cs.gui.TabContent;
 import dk.aau.cs.model.tapn.*;
@@ -86,6 +87,7 @@
 
 	// Query Name Panel;
 	private JPanel namePanel;
+	private JComboBox queryType;
 	private JButton advancedButton;
 
 	// Boundedness check panel
@@ -106,6 +108,12 @@
     private JButton forAllBox;
     private JButton forAllNext;
     private JButton forAllUntil;
+    private JButton globallyButton;
+    private JButton finallyButton;
+    private JButton nextButton;
+    private JButton untilButton;
+    private JButton aButton;
+    private JButton eButton;
 
 	private JTextPane queryField;
 
@@ -166,7 +174,8 @@
     private JCheckBox useQueryReduction;
     private JCheckBox useReduction;
 	private JCheckBox useStubbornReduction;
-	private JCheckBox useTraceRefinement;
+    private JCheckBox useTraceRefinement;
+    private JCheckBox useTarjan;
 
 	// Approximation options panel
 	private JPanel overApproximationOptionsPanel;
@@ -230,11 +239,13 @@
 	private static boolean hasForcedDisabledStubbornReduction = false;
 	private static boolean hasForcedDisabledGCD = false;
 	private static boolean disableSymmetryUpdate = false;
+	private boolean wasCTLType = true;
 
 	//Strings for tool tips
 	//Tool tips for top panel
 	private static final String TOOL_TIP_QUERYNAME = "Enter the name of the query.";
-	private static final String TOOL_TIP_INFO_BUTTON = "Get help on the different verification options.";
+    private static final String TOOL_TIP_INFO_BUTTON = "Get help on the different verification options.";
+    private static final String TOOL_TIP_QUERY_TYPE = "Choose the type of query.";
 	private static final String TOOL_TIP_ADVANCED_VIEW_BUTTON = "Switch to the advanced view.";
 	private static final String TOOL_TIP_SIMPLE_VIEW_BUTTON = "Switch to the simple view.";
 
@@ -253,6 +264,13 @@
     private static final String TOOL_TIP_FORALL_UNTIL = "On every computation the first formula holds until the second one holds";
     private static final String TOOL_TIP_FORALL_NEXT = "After any transition firing the reached marking satisfies the given property.";
 
+    private static final String TOOL_TIP_G = "Globally";
+    private static final String TOOL_TIP_F = "Eventually";
+    private static final String TOOL_TIP_U = "Until";
+    private static final String TOOL_TIP_X = "Next";
+    private static final String TOOL_TIP_E = "Switch to check if there exists a computation where the formula holds.";
+    private static final String TOOL_TIP_A = "Switch to check if the formula holds for every computation.";
+
     //Tool tips for logic panel
 	private static final String TOOL_TIP_CONJUNCTIONBUTTON = "Expand the currently selected part of the query with a conjunction.";
 	private static final String TOOL_TIP_DISJUNCTIONBUTTON = "Expand the currently selected part of the query with a disjunction.";
@@ -296,6 +314,7 @@
     private final static String TOOL_TIP_USE_SIPHONTRAP = "For a deadlock query, attempt to prove deadlock-freedom by using siphon-trap analysis via linear programming.";
     private final static String TOOL_TIP_USE_QUERY_REDUCTION = "Use query rewriting rules and linear programming (state equations) to reduce the size of the query.";
     private final static String TOOL_TIP_USE_TRACE_REFINEMENT = "Enables Trace Abstraction Refinement for reachability properties";
+    private final static String TOOL_TIP_USE_TARJAN= "Uses the Tarjan algorithm when verifying. If not selected it will verify using the nested DFS algorithm.";
 
 	//Tool tips for search options panel
 	private final static String TOOL_TIP_HEURISTIC_SEARCH = "<html>Uses a heuristic method in state space exploration.<br />" +
@@ -441,11 +460,16 @@
             /* enableUnderApproximation */false,
             0
         );
-        query.setCategory(TAPNQuery.QueryCategory.CTL);
+        if (queryType.getSelectedIndex() == 1) {
+            query.setCategory(TAPNQuery.QueryCategory.LTL);
+        } else {
+            query.setCategory(TAPNQuery.QueryCategory.CTL);
+        }
         query.setUseSiphontrap(useSiphonTrap.isSelected());
         query.setUseQueryReduction(useQueryReduction.isSelected());
         query.setUseStubbornReduction(useStubbornReduction.isSelected());
         query.setUseTarOption(useTraceRefinement.isSelected());
+        query.setUseTarjan(useTarjan.isSelected());
         return query;
     }
 
@@ -527,7 +551,7 @@
                 !(newProperty instanceof TCTLEGNode || newProperty instanceof TCTLAFNode));
             someTraceRadioButton.setEnabled(true);
             noTraceRadioButton.setEnabled(true);
-        } else if (queryIsReachability()) {
+        } else if (queryIsReachability() || queryType.getSelectedIndex() == 1) {
             fastestTraceRadioButton.setEnabled(false);
             someTraceRadioButton.setEnabled(true);
             noTraceRadioButton.setEnabled(true);
@@ -713,6 +737,12 @@
         if (!lens.isTimed() && !lens.isGame()) {
             setEnablednessOfOperatorAndMarkingBoxes();
         }
+        if (current instanceof LTLANode || current instanceof LTLENode ||
+            (queryType.getSelectedIndex() == 1 && current instanceof TCTLPathPlaceHolder)) {
+            negationButton.setEnabled(false);
+        } else {
+            negationButton.setEnabled(true);
+        }
 	}
 
     private void updateTimedQueryButtons(TCTLAtomicPropositionNode node) {
@@ -779,22 +809,21 @@
 	private void deleteSelection() {
 		if (currentSelection != null) {
 			TCTLAbstractProperty replacement = null;
-			if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
+            TCTLAbstractProperty selection = currentSelection.getObject();
+
+			if (selection instanceof TCTLAbstractStateProperty) {
 				replacement = new TCTLStatePlaceHolder();
-			} else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
+			} else if (selection instanceof TCTLAbstractPathProperty) {
 				replacement = new TCTLPathPlaceHolder();
 			}
 			if (replacement != null) {
-
-				UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), replacement);
-
-				newProperty = newProperty.replace(currentSelection.getObject(),	replacement);
-
-				if (currentSelection.getObject() instanceof TCTLAbstractPathProperty)
+				UndoableEdit edit = new QueryConstructionEdit(selection, replacement);
+				newProperty = newProperty.replace(selection,	replacement);
+
+				if (selection instanceof TCTLAbstractPathProperty)
 					resetQuantifierSelectionButtons();
 
 				updateSelection(replacement);
-
 				undoSupport.postEdit(edit);
 				queryChanged();
 			}
@@ -940,13 +969,25 @@
 			currentselected = randomSearch;
 		}
 
-		if(fastestTraceRadioButton.isSelected()){
+		if (fastestTraceRadioButton.isSelected()) {
 			breadthFirstSearch.setEnabled(false);
 			depthFirstSearch.setEnabled(false);
 			heuristicSearch.setEnabled(false);
 			randomSearch.setEnabled(false);
 			return;
-		}else{
+		} else if (queryType.getSelectedIndex() == 1) {
+            breadthFirstSearch.setEnabled(false);
+            heuristicSearch.setEnabled(true);
+            depthFirstSearch.setEnabled(true);
+            randomSearch.setEnabled(true);
+
+            if (!useTarjan.isSelected()) {
+                heuristicSearch.setEnabled(false);
+                if (someTraceRadioButton.isSelected()) {
+                    randomSearch.setEnabled(false);
+                }
+            }
+        } else {
 			breadthFirstSearch.setEnabled(true);
 			depthFirstSearch.setEnabled(true);
 			heuristicSearch.setEnabled(true);
@@ -981,6 +1022,12 @@
         existsNext.setEnabled(false);
         forAllUntil.setEnabled(false);
         forAllNext.setEnabled(false);
+        globallyButton.setEnabled(false);
+        finallyButton.setEnabled(false);
+        nextButton.setEnabled(false);
+        untilButton.setEnabled(false);
+        aButton.setEnabled(false);
+        eButton.setEnabled(false);
 
         conjunctionButton.setEnabled(false);
 		disjunctionButton.setEnabled(false);
@@ -995,6 +1042,26 @@
 		deadLockPredicateButton.setEnabled(false);
 	}
 
+	private void disableAllLTLButtons() {
+        globallyButton.setEnabled(false);
+        finallyButton.setEnabled(false);
+        nextButton.setEnabled(false);
+        untilButton.setEnabled(false);
+        aButton.setEnabled(false);
+        eButton.setEnabled(false);
+
+        conjunctionButton.setEnabled(false);
+        disjunctionButton.setEnabled(false);
+        negationButton.setEnabled(false);
+        templateBox.setEnabled(false);
+        placeTransitionBox.setEnabled(false);
+        relationalOperatorBox.setEnabled(false);
+        placeMarking.setEnabled(false);
+        addPredicateButton.setEnabled(false);
+        truePredicateButton.setEnabled(false);
+        falsePredicateButton.setEnabled(false);
+    }
+
 	private void enableOnlyPathButtons() {
 		existsBox.setEnabled(true);
 		existsDiamond.setEnabled(true);
@@ -1063,6 +1130,11 @@
         truePredicateButton.setEnabled(true);
         falsePredicateButton.setEnabled(true);
         deadLockPredicateButton.setEnabled(true);
+
+        if (queryType.getSelectedIndex() == 1) {
+            updateLTLButtons();
+        }
+
         setEnablednessOfAddPredicateButton();
     }
 
@@ -1092,7 +1164,8 @@
     }
 
 	private void setEnablednessOfAddPredicateButton() {
-		if (placeTransitionBox.getSelectedItem() == null)
+		if (placeTransitionBox.getSelectedItem() == null ||
+            (queryType.getSelectedIndex() == 1 && currentSelection.getObject() == newProperty))
 			addPredicateButton.setEnabled(false);
 		else
 			addPredicateButton.setEnabled(true);
@@ -1211,10 +1284,13 @@
             setupQuantificationFromQuery(queryToCreateFrom);
             setupApproximationOptionsFromQuery(queryToCreateFrom);
         }
+
+        setupQueryCategoryFromQuery(queryToCreateFrom);
 		setupSearchOptionsFromQuery(queryToCreateFrom);
 		setupReductionOptionsFromQuery(queryToCreateFrom);
 		setupTraceOptionsFromQuery(queryToCreateFrom);
 		setupTarOptionsFromQuery(queryToCreateFrom);
+        setupTarjanOptionsFromQuery(queryToCreateFrom);
 	}
 
 	private void setupTarOptionsFromQuery(TAPNQuery queryToCreateFrom) {
@@ -1223,6 +1299,10 @@
         }
     }
 
+    private void setupTarjanOptionsFromQuery(TAPNQuery queryToCreateFrom) {
+        useTarjan.setSelected(queryToCreateFrom.isTarjan());
+    }
+
 	private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {
 		if (queryToCreateFrom.isOverApproximationEnabled())
 			overApproximationEnable.setSelected(true);
@@ -1295,6 +1375,7 @@
         useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
         useReduction.setSelected(queryToCreateFrom.useReduction());
         useTraceRefinement.setSelected(queryToCreateFrom.isTarOptionEnabled());
+        useTarjan.setSelected(queryToCreateFrom.isTarjan());
     }
 
 	private void setupTraceOptionsFromQuery(TAPNQuery queryToCreateFrom) {
@@ -1335,6 +1416,17 @@
 		}
 	}
 
+	private void setupQueryCategoryFromQuery(TAPNQuery queryToCreateFrom) {
+        if (!lens.isTimed() && !lens.isGame()) {
+            TAPNQuery.QueryCategory category = queryToCreateFrom.getCategory();
+            if (category.equals(TAPNQuery.QueryCategory.CTL)) {
+                queryType.setSelectedIndex(0);
+            } else if (category.equals(TAPNQuery.QueryCategory.LTL)) {
+                queryType.setSelectedIndex(1);
+            }
+        }
+    }
+
 	private void initQueryNamePanel() {
 
 		JPanel splitter = new JPanel(new BorderLayout());
@@ -1365,6 +1457,10 @@
 
 			}
 		});
+		queryType = new JComboBox(new String[]{"CTL/Reachability", "LTL"});
+		queryType.setToolTipText(TOOL_TIP_QUERY_TYPE);
+		queryType.addActionListener(arg0 -> toggleDialogType());
+
 		advancedButton = new JButton("Advanced view");
 		advancedButton.setToolTipText(TOOL_TIP_ADVANCED_VIEW_BUTTON);
 		advancedButton.addActionListener(arg0 -> toggleAdvancedSimpleView(true));
@@ -1432,6 +1528,7 @@
 		});
 		JPanel topButtonPanel = new JPanel(new FlowLayout());
 		topButtonPanel.setComponentOrientation(ComponentOrientation.LEFT_TO_RIGHT);
+		if (!lens.isTimed() && !lens.isGame()) topButtonPanel.add(queryType);
 		topButtonPanel.add(advancedButton);
 		topButtonPanel.add(infoButton);
 
@@ -1486,6 +1583,309 @@
 		guiDialog.setLocation(location);
 	}
 
+	private void toggleDialogType() {
+       if (queryType.getSelectedIndex() == 1 && wasCTLType) {
+           String ltlType = checkLTLType();
+           boolean isA = ltlType.equals("A");
+           if (convertPropertyType(false, newProperty, true, isA) == null &&
+               !(newProperty instanceof TCTLStatePlaceHolder)) {
+               if (showWarningMessage(false) == JOptionPane.YES_OPTION) {
+                   deleteProperty();
+               } else {
+                   queryType.setSelectedIndex(0);
+                   return;
+               }
+           } else if (isA) {
+              addAllPathsToProperty(newProperty, null);
+           } else if (ltlType.equals("E")) {
+               addExistsPathsToProperty(newProperty, null);
+           }
+           showLTLButtons(true);
+           updateShiphonTrap(true);
+           queryChanged();
+           wasCTLType = false;
+       } else if (queryType.getSelectedIndex() == 0 && !wasCTLType) {
+           if (convertPropertyType(true, newProperty, true, newProperty instanceof LTLANode) == null &&
+               !(newProperty instanceof TCTLStatePlaceHolder)) {
+               if (showWarningMessage(true) == JOptionPane.YES_OPTION) {
+                   deleteProperty();
+                   newProperty = removeExistsAllPathsFromProperty(newProperty);
+               } else {
+                   queryType.setSelectedIndex(1);
+                   return;
+               }
+           }
+           showLTLButtons(false);
+           updateShiphonTrap(false);
+           wasCTLType = true;
+       }
+       if (undoManager != null) undoManager.discardAllEdits();
+       if (undoButton != null) undoButton.setEnabled(false);
+       if (redoButton != null) redoButton.setEnabled(false);
+       setEnabledOptionsAccordingToCurrentReduction();
+    }
+
+    private String checkLTLType() {
+	    if (newProperty.toString().equals("<*>"))
+	        return "placeholder";
+	    if (newProperty.toString().startsWith("A"))
+	        return "A";
+        if (newProperty.toString().startsWith("E"))
+            return "E";
+        if (newProperty.toString().startsWith("A", 2))
+            return "A";
+        if (newProperty.toString().startsWith("E", 2))
+            return "E";
+        if (newProperty.toString().startsWith("A", 3))
+            return "A";
+        if (newProperty.toString().startsWith("E", 3))
+            return "E";
+        return "placeholder";
+    }
+
+    private TCTLAbstractProperty convertPropertyType(boolean toCTL, TCTLAbstractProperty property, boolean isFirst, boolean isA) {
+        if (property != null) {
+            property = removeExistsAllPathsFromProperty(removeConverter(property));
+
+            if (!toCTL && (property instanceof TCTLDeadlockNode || !canBeConverted(property, isA))) {
+                return null;
+            } else if (property.isSimpleProperty() && !(property instanceof TCTLNotNode)) {
+                if (!isFirst) {
+                    return property;
+                } else if (property instanceof TCTLTrueNode || property instanceof TCTLFalseNode ||
+                           property instanceof TCTLAtomicPropositionNode || property instanceof TCTLTransitionNode) {
+                    property = ConvertToPathProperty((TCTLAbstractStateProperty) property);
+                    return replaceProperty(property);
+                }
+            }
+
+            TCTLAbstractProperty replacement = getReplacement(toCTL, property, isA);
+
+            if (!isFirst) {
+                return replacement;
+            }
+            return replaceProperty(replacement);
+        }
+        return null;
+	}
+
+	private boolean canBeConverted(TCTLAbstractProperty property, boolean isA) {
+	    if (isA && property.toString().startsWith("E")) {
+	        return false;
+        } else if (!isA && property.toString().startsWith("A")) {
+            return false;
+        }
+	    return true;
+	}
+
+	private TCTLAbstractProperty removeConverter(TCTLAbstractProperty property) {
+	    while (property instanceof TCTLPathToStateConverter || property instanceof TCTLStateToPathConverter) {
+            if (property instanceof TCTLStateToPathConverter) {
+                property = ConvertToStateProperty((TCTLStateToPathConverter) property);
+            } else {
+                property = ConvertToPathProperty((TCTLPathToStateConverter) property);
+            }
+        }
+        return property;
+    }
+
+	private TCTLAbstractProperty getReplacement(boolean toCTL, TCTLAbstractProperty property, boolean isA) {
+	    TCTLAbstractProperty replacement = null;
+        TCTLAbstractStateProperty firstChild = getChild(toCTL, property, 1, isA);
+        TCTLAbstractStateProperty secondChild = getChild(toCTL, property, 2, isA);
+        property = removeConverter(property);
+
+        if (firstChild == null || secondChild == null)
+            return null;
+        if (toCTL) {
+            if (property instanceof LTLGNode) {
+                replacement = isA? new TCTLAGNode(firstChild) : new TCTLEGNode(firstChild);
+            } else if (property instanceof LTLFNode) {
+                replacement = isA ? new TCTLAFNode(firstChild) : new TCTLEFNode(firstChild);
+            } else if (property instanceof LTLXNode) {
+                replacement = isA ? new TCTLAXNode(firstChild) : new TCTLEXNode(firstChild);
+            } else if (property instanceof LTLUNode) {
+                replacement = isA ? new TCTLAUNode(firstChild, secondChild): new TCTLEUNode(firstChild, secondChild);
+            }
+        } else {
+            if (property instanceof TCTLAGNode || property instanceof TCTLEGNode) {
+                replacement = new LTLGNode(firstChild);
+            } else if (property instanceof TCTLAFNode || property instanceof TCTLEFNode) {
+                replacement = new LTLFNode(firstChild);
+            } else if (property instanceof TCTLAXNode || property instanceof TCTLEXNode) {
+                replacement = new LTLXNode(firstChild);
+            } else if (property instanceof TCTLAUNode || property instanceof TCTLEUNode) {
+                replacement = new LTLUNode(firstChild, secondChild);
+            }
+        }
+
+        if (replacement == null) {
+            if (property instanceof TCTLStatePlaceHolder || property instanceof TCTLPathPlaceHolder) {
+                return property;
+            } else if (property instanceof TCTLNotNode) {
+                return new TCTLNotNode(firstChild);
+            } else if (property instanceof TCTLAndListNode) {
+                return new TCTLAndListNode(firstChild, secondChild);
+            } else if (property instanceof TCTLOrListNode) {
+                return new TCTLOrListNode(firstChild, secondChild);
+            } else {
+                replacement = property;
+            }
+        }
+	    return replacement;
+    }
+
+    private TCTLAbstractStateProperty getChild(boolean toCTL, TCTLAbstractProperty property, int childNumber, boolean isA) {
+        property = removeConverter(property);
+        TCTLAbstractProperty child = getSpecificChildOfProperty(childNumber, property);
+        child = removeConverter(child);
+
+        if (!(child instanceof TCTLStatePlaceHolder || child instanceof TCTLPathPlaceHolder)) {
+           if (!child.isSimpleProperty() || child instanceof TCTLNotNode) {
+                TCTLAbstractProperty replacement = convertPropertyType(toCTL, child, false, isA);
+                if (replacement == null) {
+                    return null;
+                }
+                replacement = removeConverter(replacement);
+                child = child.replace(child, replacement);
+          } else if (child instanceof TCTLDeadlockNode) {
+               return null;
+           }
+        }
+        if (child instanceof TCTLAbstractPathProperty) {
+            return ConvertToStateProperty((TCTLAbstractPathProperty)child);
+        }
+
+        return (TCTLAbstractStateProperty) child;
+    }
+
+    private TCTLAbstractProperty replaceProperty(TCTLAbstractProperty replacement) {
+        if (replacement != null) {
+            newProperty = removeConverter(newProperty);
+            if ((newProperty instanceof LTLANode || newProperty instanceof LTLENode)
+                && !(replacement instanceof TCTLAbstractPathProperty)) {
+                replacement = ConvertToPathProperty((TCTLAbstractStateProperty)replacement);
+            }
+            newProperty = newProperty.replace(newProperty, replacement);
+            replacement = removeConverter(replacement);
+
+            if (newProperty instanceof TCTLAbstractPathProperty) resetQuantifierSelectionButtons();
+
+            updateSelection(replacement);
+            queryChanged();
+
+            return newProperty;
+        }
+        return null;
+    }
+
+    private void deleteProperty() {
+        if (newProperty != null) {
+            TCTLAbstractProperty replacement = null;
+            newProperty = removeConverter(newProperty);
+            if (newProperty instanceof TCTLAbstractStateProperty) {
+                replacement = new TCTLStatePlaceHolder();
+            } else if (newProperty instanceof TCTLAbstractPathProperty) {
+                replacement = new TCTLPathPlaceHolder();
+            }
+            replaceProperty(replacement);
+        }
+    }
+
+    private int showWarningMessage(boolean toCTL) {
+	    String category = toCTL ? "CTL" : "LTL";
+	    String message = "The query property will be deleted, because it is not compatible with "+category+"-queries.\n" +
+            "Are you sure you want to change query category?";
+	    String title = "Incompatible query";
+
+	    return JOptionPane.showConfirmDialog(
+            CreateGui.getApp(),
+            message,
+            title,
+            JOptionPane.YES_NO_OPTION,
+            JOptionPane.WARNING_MESSAGE);
+    }
+
+    private void addAllPathsToProperty(TCTLAbstractProperty oldProperty, TCTLAbstractProperty selection) {
+        TCTLAbstractProperty property = null;
+
+        if (oldProperty instanceof LTLANode) {
+            property = oldProperty;
+        } else if (oldProperty instanceof TCTLPathPlaceHolder) {
+            property = new LTLANode();
+        } else if (oldProperty instanceof TCTLAbstractPathProperty) {
+            property = new LTLANode(ConvertToStateProperty((TCTLAbstractPathProperty) oldProperty));
+        } else if (oldProperty instanceof TCTLNotNode) {
+            property = new LTLANode((TCTLNotNode) oldProperty);
+            property = ConvertToStateProperty((TCTLAbstractPathProperty) property);
+        } else if (oldProperty instanceof TCTLAbstractStateProperty && (selection == null || selection instanceof LTLANode)) {
+            property = new LTLANode((TCTLAbstractStateProperty) oldProperty);
+            if (!(newProperty instanceof TCTLAbstractPathProperty)) newProperty = ConvertToPathProperty((TCTLAbstractStateProperty) newProperty);
+        }
+
+        if (property != null && selection != null) {
+            UndoableEdit edit = new QueryConstructionEdit(selection, property);
+            newProperty = newProperty.replace(newProperty, property);
+            updateSelection(property);
+            undoSupport.postEdit(edit);
+            queryChanged();
+        } else if (property != null) {
+            newProperty = newProperty.replace(newProperty, property);
+            updateSelection(property);
+            queryChanged();
+        }
+    }
+
+    private void addExistsPathsToProperty(TCTLAbstractProperty oldProperty, TCTLAbstractProperty selection) {
+        TCTLAbstractProperty property = null;
+
+        if (oldProperty instanceof LTLENode) {
+            property = oldProperty;
+        } else if (oldProperty instanceof TCTLPathPlaceHolder) {
+            property = new LTLENode();
+        } else if (oldProperty instanceof TCTLAbstractPathProperty) {
+            property = new LTLENode(ConvertToStateProperty((TCTLAbstractPathProperty) oldProperty));
+        } else if (oldProperty instanceof TCTLNotNode) {
+            property = new LTLENode((TCTLNotNode) oldProperty);
+            property = ConvertToStateProperty((TCTLAbstractPathProperty) property);
+        } else if (oldProperty instanceof TCTLAbstractStateProperty && (selection == null || selection instanceof LTLENode)) {
+            property = new LTLENode((TCTLAbstractStateProperty) oldProperty);
+            if (!(newProperty instanceof TCTLAbstractPathProperty)) newProperty = ConvertToPathProperty((TCTLAbstractStateProperty) newProperty);
+        }
+
+        if (property != null && selection != null) {
+            UndoableEdit edit = new QueryConstructionEdit(selection, property);
+            newProperty = newProperty.replace(newProperty, property);
+            updateSelection(property);
+            undoSupport.postEdit(edit);
+            queryChanged();
+        } else if (property != null) {
+            newProperty = newProperty.replace(newProperty, property);
+            updateSelection(property);
+            queryChanged();
+        }
+    }
+
+    private TCTLAbstractProperty removeExistsAllPathsFromProperty(TCTLAbstractProperty oldProperty) {
+        TCTLAbstractProperty property = oldProperty;
+        TCTLAbstractStateProperty firstChild = getSpecificChildOfProperty(1, oldProperty);
+
+        if (oldProperty instanceof TCTLPathToStateConverter) {
+            oldProperty = ((TCTLPathToStateConverter) oldProperty).getProperty();
+            firstChild = getSpecificChildOfProperty(1, oldProperty);
+        }
+        if (oldProperty instanceof LTLANode) {
+            TCTLAbstractPathProperty child = ConvertToPathProperty(firstChild);
+            property = oldProperty.replace(oldProperty, child);
+        }
+        if (oldProperty instanceof LTLENode) {
+            TCTLAbstractPathProperty child = ConvertToPathProperty(firstChild);
+            property = oldProperty.replace(oldProperty, child);
+        }
+
+        return property;
+    }
+
 	private void initBoundednessCheckPanel() {
 
 		// Number of extra tokens field
@@ -1644,6 +2044,12 @@
         existsNext = new JButton("EX");
         forAllUntil = new JButton("AU");
         forAllNext = new JButton("AX");
+        globallyButton = new JButton("G");
+        finallyButton = new JButton("F");
+        nextButton = new JButton("X");
+        untilButton = new JButton("U");
+        aButton = new JButton("A");
+        eButton = new JButton("E");
 
         // Add tool-tips
         existsDiamond.setToolTipText(TOOL_TIP_EXISTS_DIAMOND);
@@ -1654,6 +2060,12 @@
         existsNext.setToolTipText(TOOL_TIP_EXISTS_NEXT);
         forAllUntil.setToolTipText(TOOL_TIP_FORALL_UNTIL);
         forAllNext.setToolTipText(TOOL_TIP_FORALL_NEXT);
+        globallyButton.setToolTipText(TOOL_TIP_G);
+        finallyButton.setToolTipText(TOOL_TIP_F);
+        nextButton.setToolTipText(TOOL_TIP_X);
+        untilButton.setToolTipText(TOOL_TIP_U);
+        aButton.setToolTipText(TOOL_TIP_A);
+        eButton.setToolTipText(TOOL_TIP_E);
 
         // Add buttons to panel
         quantificationButtonGroup.add(existsDiamond);
@@ -1664,6 +2076,12 @@
         quantificationButtonGroup.add(existsNext);
         quantificationButtonGroup.add(forAllUntil);
         quantificationButtonGroup.add(forAllNext);
+        quantificationButtonGroup.add(globallyButton);
+        quantificationButtonGroup.add(finallyButton);
+        quantificationButtonGroup.add(nextButton);
+        quantificationButtonGroup.add(untilButton);
+        quantificationButtonGroup.add(aButton);
+        quantificationButtonGroup.add(eButton);
 
         // Place buttons in GUI
         GridBagConstraints gbc = new GridBagConstraints();
@@ -1674,24 +2092,32 @@
         gbc.gridy = 0;
         gbc.insets = new Insets(0, 0, 5, 0);
         quantificationPanel.add(existsDiamond, gbc);
+        quantificationPanel.add(globallyButton, gbc);
         gbc.gridy = 1;
         quantificationPanel.add(existsBox, gbc);
+        quantificationPanel.add(finallyButton, gbc);
         gbc.gridy = 2;
         quantificationPanel.add(existsUntil, gbc);
         gbc.gridy = 3;
         quantificationPanel.add(existsNext, gbc);
+        gbc.gridy = 4;
+        quantificationPanel.add(aButton, gbc);
 
         // Second column of buttons
         gbc.gridx = 2;
         gbc.gridy = 0;
         gbc.insets = new Insets(0, 0, 5, 0);
         quantificationPanel.add(forAllDiamond, gbc);
+        quantificationPanel.add(nextButton, gbc);
         gbc.gridy = 1;
         quantificationPanel.add(forAllBox, gbc);
+        quantificationPanel.add(untilButton, gbc);
         gbc.gridy = 2;
         quantificationPanel.add(forAllUntil, gbc);
         gbc.gridy = 3;
         quantificationPanel.add(forAllNext, gbc);
+        gbc.gridy = 4;
+        quantificationPanel.add(eButton, gbc);
 
         // Add quantification panel to query panel
 		gbc = new GridBagConstraints();
@@ -1703,8 +2129,10 @@
 
 		if (lens.isTimed()|| lens.isGame()) {
             addTimedQuantificationListeners();
+            showLTLButtons(false);
         } else {
             addUntimedQuantificationListeners();
+            showLTLButtons(false);
         }
     }
 
@@ -1775,6 +2203,18 @@
             }
         });
 
+        globallyButton.addActionListener(e -> {
+            LTLGNode property = new LTLGNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
+            addPropertyToQuery(property);
+            unselectButtons();
+        });
+
+        finallyButton.addActionListener(e -> {
+            LTLFNode property = new LTLFNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
+            addPropertyToQuery(property);
+            unselectButtons();
+        });
+
         forAllNext.addActionListener(new ActionListener() {
             public void actionPerformed(ActionEvent e) {
                 TCTLAbstractPathProperty property;
@@ -1800,16 +2240,104 @@
                 addPropertyToQuery(property);
             }
         });
+
+        nextButton.addActionListener(new ActionListener() {
+            public void actionPerformed(ActionEvent e) {
+                TCTLAbstractPathProperty property;
+                if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
+                    property = new LTLXNode((TCTLAbstractStateProperty) currentSelection.getObject());
+                } else {
+                    property = new LTLXNode(getSpecificChildOfProperty(1, currentSelection.getObject()));
+                }
+                addPropertyToQuery(property);
+            }
+        });
+
+        untilButton.addActionListener(new ActionListener() {
+            public void actionPerformed(ActionEvent e) {
+                TCTLAbstractPathProperty property;
+                if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
+                    property = new LTLUNode((TCTLAbstractStateProperty) currentSelection.getObject(),
+                        new TCTLStatePlaceHolder());
+                } else {
+                    property = new LTLUNode(getSpecificChildOfProperty(1, currentSelection.getObject()),
+                        getSpecificChildOfProperty(2, currentSelection.getObject()));
+                }
+                addPropertyToQuery(property);
+            }
+        });
+
+        aButton.addActionListener(new ActionListener() {
+            public void actionPerformed(ActionEvent e) {
+                TCTLAbstractProperty oldProperty = newProperty;
+
+                newProperty = removeExistsAllPathsFromProperty(newProperty);
+                addAllPathsToProperty(newProperty, null);
+                UndoableEdit edit = new QueryConstructionEdit(oldProperty, newProperty);
+                undoSupport.postEdit(edit);
+
+                queryChanged();
+            }
+        });
+
+        eButton.addActionListener(new ActionListener() {
+            public void actionPerformed(ActionEvent e) {
+                TCTLAbstractProperty oldProperty = newProperty;
+
+                newProperty = removeExistsAllPathsFromProperty(newProperty);
+                addExistsPathsToProperty(newProperty, null);
+                UndoableEdit edit = new QueryConstructionEdit(oldProperty, newProperty);
+                undoSupport.postEdit(edit);
+
+                queryChanged();
+            }
+        });
+    }
+
+    private void showLTLButtons(boolean isVisible) {
+        globallyButton.setVisible(isVisible);
+        finallyButton.setVisible(isVisible);
+        nextButton.setVisible(isVisible);
+        untilButton.setVisible(isVisible);
+        aButton.setVisible(isVisible);
+        eButton.setVisible(isVisible);
+        if (deadLockPredicateButton != null) deadLockPredicateButton.setVisible(!isVisible);
+        showCTLButtons(!isVisible);
+    }
+
+    private void showCTLButtons(boolean isVisible) {
+        forAllBox.setVisible(isVisible);
+        forAllDiamond.setVisible(isVisible);
+        forAllNext.setVisible(isVisible);
+        forAllUntil.setVisible(isVisible);
+        existsBox.setVisible(isVisible);
+        existsDiamond.setVisible(isVisible);
+        existsNext.setVisible(isVisible);
+        existsUntil.setVisible(isVisible);
+    }
+    private void updateShiphonTrap(boolean isLTL) {
+        useSiphonTrap.setEnabled(!isLTL);
     }
 
     private void addPropertyToQuery(TCTLAbstractPathProperty property) {
-        if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
+	    TCTLAbstractProperty selection = currentSelection.getObject();
+	    if (selection instanceof TCTLAbstractStateProperty) {
             addPropertyToQuery(ConvertToStateProperty(property));
             return;
         }
 
-        UndoableEdit edit = new QueryConstructionEdit(currentSelection.getObject(), property);
-        newProperty = newProperty.replace(currentSelection.getObject(), property);
+        if (selection instanceof LTLANode) {
+            newProperty = newProperty.replace(selection, property);
+            addAllPathsToProperty(newProperty, selection);
+            return;
+        } else if (selection instanceof LTLENode) {
+            newProperty = newProperty.replace(selection, property);
+            addExistsPathsToProperty(newProperty, selection);
+            return;
+        }
+
+        UndoableEdit edit = new QueryConstructionEdit(selection, property);
+        newProperty = newProperty.replace(selection, property);
         updateSelection(property);
         undoSupport.postEdit(edit);
         queryChanged();
@@ -1979,8 +2507,11 @@
             addPropertyToQuery(property);
         } else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
             TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
+
+            TCTLAbstractProperty oldProperty = removeExistsAllPathsFromProperty(currentSelection.getObject());
+
             andListNode = new TCTLAndListNode(getStateProperty(
-                new TCTLPathToStateConverter((TCTLAbstractPathProperty) currentSelection.getObject())), ph);
+                new TCTLPathToStateConverter((TCTLAbstractPathProperty) oldProperty)), ph);
 
             TCTLAbstractPathProperty property = new TCTLStateToPathConverter(andListNode);
             addPropertyToQuery(property);
@@ -2007,8 +2538,10 @@
             addPropertyToQuery(property);
         } else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
             TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
+            TCTLAbstractProperty oldProperty = removeExistsAllPathsFromProperty(currentSelection.getObject());
+
             orListNode = new TCTLOrListNode(getStateProperty(
-                new TCTLPathToStateConverter((TCTLAbstractPathProperty) currentSelection.getObject())), ph);
+                new TCTLPathToStateConverter((TCTLAbstractPathProperty) oldProperty)), ph);
 
             TCTLAbstractPathProperty property = new TCTLStateToPathConverter(orListNode);
             addPropertyToQuery(property);
@@ -2307,8 +2840,12 @@
                                 return;
                         } else if (lens.isTimed()) {
                             newQuery = TAPAALQueryParser.parse(queryField.getText());
-                        } else {
+                        } else if (queryType.getSelectedIndex() == 0) {
 						    newQuery = TAPAALCTLQueryParser.parse(queryField.getText());
+                        } else if (queryType.getSelectedIndex() == 1) {
+					        newQuery = TAPAALLTLQueryParser.parse(queryField.getText());
+                        } else {
+					        throw new Exception();
                         }
 					} catch (Throwable ex) {
 					    String message = ex.getMessage() == null ? "TAPAAL encountered an error while trying to parse the specified query\n" :
@@ -2374,6 +2911,13 @@
 				} else { // we are not in edit mode so the button should reset
 					// the query
 
+                    if (queryType.getSelectedIndex() == 1) {
+                        TCTLAbstractProperty oldProperty = newProperty;
+                        addAllPathsToProperty(new TCTLPathPlaceHolder(), oldProperty);
+                        resetQuantifierSelectionButtons();
+                        return;
+                    }
+
 					TCTLPathPlaceHolder ph = new TCTLPathPlaceHolder();
 					UndoableEdit edit = new QueryConstructionEdit(newProperty, ph);
 					newProperty = ph;
@@ -2695,6 +3239,7 @@
         usePTrie = new JCheckBox("Use PTrie");
         useOverApproximation = new JCheckBox("Use untimed state-equations check");
         useTraceRefinement = new JCheckBox("Use trace abstraction refinement");
+        useTarjan = new JCheckBox("Use Tarjan");
 
         useReduction.setSelected(true);
         useSiphonTrap.setSelected(false);
@@ -2708,6 +3253,7 @@
         usePTrie.setSelected(true);
         useOverApproximation.setSelected(true);
         useTraceRefinement.setSelected(false);
+        useTarjan.setSelected(true);
 
         useReduction.setToolTipText(TOOL_TIP_USE_STRUCTURALREDUCTION);
         useSiphonTrap.setToolTipText(TOOL_TIP_USE_SIPHONTRAP);
@@ -2721,6 +3267,9 @@
         usePTrie.setToolTipText(TOOL_TIP_PTRIE);
         useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
         useTraceRefinement.setToolTipText(TOOL_TIP_USE_TRACE_REFINEMENT);
+        useTarjan.setToolTipText(TOOL_TIP_USE_TARJAN);
+
+        useTarjan.addActionListener(e -> updateSearchStrategies());
 
         if (lens.isTimed() || lens.isGame()) {
             initTimedReductionOptions();
@@ -2809,6 +3358,9 @@
         gbc.gridx = 3;
         gbc.gridy = 0;
         reductionOptionsPanel.add(useTraceRefinement, gbc);
+        gbc.gridx = 3;
+        gbc.gridy = 1;
+        reductionOptionsPanel.add(useTarjan, gbc);
     }
 
 	protected void setEnabledOptionsAccordingToCurrentReduction() {
@@ -2822,6 +3374,7 @@
             refreshOverApproximationOption();
         } else if (!lens.isTimed()) {
             refreshTraceRefinement();
+            refreshTarjan();
         }
 		updateSearchStrategies();
 		refreshExportButtonText();
@@ -2831,13 +3384,21 @@
 	    ReductionOption reduction = getReductionOption();
 	    useTraceRefinement.setEnabled(false);
 
-	    if (reduction != null && reduction.equals(ReductionOption.VerifyPN) && !hasInhibitorArcs &&
+	    if (queryType.getSelectedIndex() != 1 && reduction != null && reduction.equals(ReductionOption.VerifyPN) &&
             (newProperty.toString().startsWith("AG") || newProperty.toString().startsWith("EF")) &&
-            !newProperty.hasNestedPathQuantifiers()) {
+            !hasInhibitorArcs && !newProperty.hasNestedPathQuantifiers()) {
 	        useTraceRefinement.setEnabled(true);
         }
     }
 
+    private void refreshTarjan() {
+        if (queryType.getSelectedIndex() == 1) {
+            useTarjan.setVisible(true);
+        } else {
+            useTarjan.setVisible(false);
+        }
+    }
+
 	private void refreshDiscreteInclusion() {
 		ReductionOption reduction = getReductionOption();
 		if(reduction == null){
@@ -3014,13 +3575,37 @@
 		}
 	}
 
+	private void updateLTLButtons() {
+        if (currentSelection.getObject() == newProperty) {
+            String ltlType = checkLTLType();
+            disableAllLTLButtons();
+            if (ltlType.equals("placeholder")) {
+                aButton.setEnabled(true);
+                eButton.setEnabled(true);
+            } else if (ltlType.equals("A")) {
+                eButton.setEnabled(true);
+            } else {
+                aButton.setEnabled(true);
+            }
+        } else {
+            aButton.setEnabled(false);
+            eButton.setEnabled(false);
+            globallyButton.setEnabled(true);
+            finallyButton.setEnabled(true);
+            nextButton.setEnabled(true);
+            untilButton.setEnabled(true);
+        }
+    }
+
 
 	private void queryChanged(){
-    		setEnabledReductionOptions();
+        setEnabledReductionOptions();
         if (lens.isTimed()) refreshOverApproximationOption();
+        if (queryType.getSelectedIndex() == 1) {
+            updateLTLButtons();
+        }
 	}
 
-
 	private void initButtonPanel(QueryDialogueOption option) {
 		buttonPanel = new JPanel(new BorderLayout());
 		if (option == QueryDialogueOption.Save) {

=== removed directory 'src/resources/SUMOParser'
=== removed directory 'src/resources/TCTLParser'