Merge lp:~tapaal-approx/tapaal/tapaal-approx-new into lp:tapaal

[Jiri Srba]

Implements over and under-approximation of time intervals both in the query dialog and for batch processing. A new net composed with GUI is
added too.

Implements over and under-approximation of time intervals both in the query dialog and for batch processing. A new net composed with GUI is
added too.

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

930. By Jiri Srba on 2014-05-03

removed file src/dk/aau/cs/gui/BatchProcessingDialog.java.bak

931. By Jiri Srba on 2014-05-03

removing src/dk/aau/cs/io/TapnXmlLoader.java.bak

932. By Jiri Srba on 2014-05-03

removed more .bak files

933. By Jiri Srba on 2014-05-03

fix in batch processing name text string

[Mathias Grund Sørensen (mathias.grund)]

Nothing major comes to mind, a few comments though:

- Please remove dumpToConsole function (no debug code in trunk)
- please remove commented code (I spotted a commented call to dumpToConsole and something around line 3935)
- some funny comment thing is going on around line 1273, this should probably go
- some funny thing going on with null in line 980, but I assume it's ok (looks A little hacksy)
- maybe one could consider attaching to memory monitor with commulative flag for process, rather than the current design where you have to remember to turn it off again (I hope you remember to do this in all places! Have you handled aborts etc? I did not go through the code to verify this :) )

The code generally looks okay, but I believe at least the first two comments should be addressed before merge.

review: Needs Fixing (code)

[Jakob Taankvist (jakob-taankvist)]

I've looked through the code and one think i think should be fixed are some very long functions. Is it possible to split these into multiple functions in a logical way? Very long functions are e.g.:

makeTraceTAPN lines: 93 - 275
modifyTAPN lines: 315 - 421
verify lines: 2557 - 2841
doInBackground lines: 3135 - 3468

I also noticed a lot of nesting of for and if in these functions, it would be nice if could somehow be avoided:
reduceTraceForOriginalNet and removeTokens lines: 1084 - 1115

Some of the code in the action listener in lines 4020 - 4062 should maybe be done in the composer class - at least I think it's a very long action listener, which might make it hard to use the composer in other parts of the code later. (an option would be to move the code to a function somewhere logical, and then calling this function from the action listener).

[Kenneth Yrke Jørgensen (yrke)]

Just a quick question about the following lines:

910 s.append((query != null) ? (query.useSymmetry() ? "Yes" : "No") : "");
911 s.append(DELIMITER);
912 s.append((query != null) ? getVerificationMethod(query) : "");
913 + s.append(DELIMITER);
914 + s.append((query != null) ? getApproximationMethod(query) : "");
915 + s.append(DELIMITER);
916 + s.append((query != null) ? query.approximationDenominator() : "");

For me it seems more natural to make one if one query and then do all the append stuff:

if (query != null) {
  //build string
  s.append(query.useSymmetry() ? "Yes" : "No");
  s.append(....)
  ...
}

The other way seams a little strange to me (unless there is something special about how query works, which really should be fixed then). (i know i was done this way in the original code as well, but i still think it needs to be fixed)

review: Needs Fixing (code)

[Jakob Taankvist (jakob-taankvist)]

Another comment - should TAPNComposer be replaced by the new TAPNComposerExtended?

If not the name "TAPNComposerExtended" is not very explanatory.

review: Needs Fixing

[Thomas Stig Jacobsen (tsja10)]

The dumpToConsole in the TAPNComposerExtended was originally in TAPNComposer but has now been removed completely.
    I am not quite sure where the code for verification aborts are, but if you can lead me the right direction I'll check it or add it to the code.

> Nothing major comes to mind, a few comments though:
>
> - Please remove dumpToConsole function (no debug code in trunk)
> - please remove commented code (I spotted a commented call to dumpToConsole
> and something around line 3935)
> - some funny comment thing is going on around line 1273, this should probably
> go
> - some funny thing going on with null in line 980, but I assume it's ok (looks
> A little hacksy)
> - maybe one could consider attaching to memory monitor with commulative flag
> for process, rather than the current design where you have to remember to turn
> it off again (I hope you remember to do this in all places! Have you handled
> aborts etc? I did not go through the code to verify this :) )
>
> The code generally looks okay, but I believe at least the first two comments
> should be addressed before merge.

[Thomas Stig Jacobsen (tsja10)]

The verify and doInBackground methods could maybe be moved to the OverApproximation and UnderApproximation, however, since verify and doInBackground returns different and works with different types the code could not be reused. I can have a try with moving the code if you want to, but I am not quite sure that it would work perfectly at the moment.

    Both makeTraceTAPN and modifyTAPN represents complete algorithms from the article and I think it is nicer to keep these together as a whole rather than splitting them up, even though the methods are 100+ lines of code.

    The TAPNComposer should not be replaced by the new TAPNComposerExtended, the TAPNComposerExtended should only be used when a new guiModel (DataLayer) is needed, otherwise the normal TAPNComposer should be used.
    The TAPNComposerExtended does the same work to the network (combining the nets in the network into one net), but is also builds a new DataLayer for this new net so it can be opened in TAPAAL for viewing. I'm not quite sure what it should be called but I'm open for suggestions.

> I've looked through the code and one think i think should be fixed are some
> very long functions. Is it possible to split these into multiple functions in
> a logical way? Very long functions are e.g.:
>
> makeTraceTAPN lines: 93 - 275
> modifyTAPN lines: 315 - 421
> verify lines: 2557 - 2841
> doInBackground lines: 3135 - 3468
>
> I also noticed a lot of nesting of for and if in these functions, it would be
> nice if could somehow be avoided:
> reduceTraceForOriginalNet and removeTokens lines: 1084 - 1115
>
> Some of the code in the action listener in lines 4020 - 4062 should maybe be
> done in the composer class - at least I think it's a very long action
> listener, which might make it hard to use the composer in other parts of the
> code later. (an option would be to move the code to a function somewhere
> logical, and then calling this function from the action listener).

[Thomas Stig Jacobsen (tsja10)]

Regarding the exportToCSV method from which the lines 910-016 is from, we've used the style of code which was already used with the multiple appends, if the lines should be refactored, I think the rest of the method (or the class) should be refactored as well. A possible explanation to the way this is done now is that the XmlLoader when opening nets expects a certain number of delimiters for padding but I haven't check up on that. If not, I do agree this should be redone.

> Just a quick question about the following lines:
>
> 910 s.append((query != null) ?
> (query.useSymmetry() ? "Yes" : "No") : "");
> 911 s.append(DELIMITER);
> 912 s.append((query != null) ?
> getVerificationMethod(query) : "");
> 913 + s.append(DELIMITER);
> 914 + s.append((query != null) ?
> getApproximationMethod(query) : "");
> 915 + s.append(DELIMITER);
> 916 + s.append((query != null) ?
> query.approximationDenominator() : "");
>
> For me it seems more natural to make one if one query and then do all the
> append stuff:
>
> if (query != null) {
> //build string
> s.append(query.useSymmetry() ? "Yes" : "No");
> s.append(....)
> ...
> }
>
> The other way seams a little strange to me (unless there is something special
> about how query works, which really should be fixed then). (i know i was done
> this way in the original code as well, but i still think it needs to be fixed)

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

934. By Thomas Stig Jacobsen on 2014-05-09

Initial merge fixes

[Jakob Taankvist (jakob-taankvist)]

> The verify and doInBackground methods could maybe be moved to the
> OverApproximation and UnderApproximation, however, since verify and
> doInBackground returns different and works with different types the code could
> not be reused. I can have a try with moving the code if you want to, but I am
> not quite sure that it would work perfectly at the moment.

I think it's a good idea to move this code somewhere else, I also think it would be crucial to split the functions (but I guess it's part of moving them)

> Both makeTraceTAPN and modifyTAPN represents complete algorithms from the
> article and I think it is nicer to keep these together as a whole rather than
> splitting them up, even though the methods are 100+ lines of code.

I think it would be fine to split these up, they have their own class anyway, and if they are doing something algorithmic it's probably hard to understand from the code what they are doing. So i think it would be better to make some more methods.

I don't think this would split up the algorithm. It would merely move technical details to helper methods.

All that said i think the two other comments are more important, and as the methods are in separate files it might be ok.

> The TAPNComposer should not be replaced by the new TAPNComposerExtended,
> the TAPNComposerExtended should only be used when a new guiModel (DataLayer)
> is needed, otherwise the normal TAPNComposer should be used.
> The TAPNComposerExtended does the same work to the network (combining the
> nets in the network into one net), but is also builds a new DataLayer for this
> new net so it can be opened in TAPAAL for viewing. I'm not quite sure what it
> should be called but I'm open for suggestions.

To me it sounds like TAPNComposerExtended does the same as TAPNComposer + some more. Doesn't that mean that large parts of the code in the two different classes does the same thing?
It feels like maybe they should inherit from each other or have a common superclass?
Maybe we could just send a flag to TAPNComposerExtended to tell it wether it should build the GUI or not?

As for a name I think TAPNComposerWithGUI would be more explanatory.

PS: I'm looking forward to have this merged, it's a really cool idea, and the code will definitely raise the average code quality in TAPAAL :P

> > I've looked through the code and one think i think should be fixed are some
> > very long functions. Is it possible to split these into multiple functions
> in
> > a logical way? Very long functions are e.g.:
> >
> > makeTraceTAPN lines: 93 - 275
> > modifyTAPN lines: 315 - 421
> > verify lines: 2557 - 2841
> > doInBackground lines: 3135 - 3468
> >
> > I also noticed a lot of nesting of for and if in these functions, it would
> be
> > nice if could somehow be avoided:
> > reduceTraceForOriginalNet and removeTokens lines: 1084 - 1115
> >
> > Some of the code in the action listener in lines 4020 - 4062 should maybe be
> > done in the composer class - at least I think it's a very long action
> > listener, which might make it hard to use the composer in other parts of the
> > code later. (an option would be to move the code to a function somewhere
> > logica...

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

935. By Thomas Stig Jacobsen on 2014-05-11

Moving of functionality to its own class from action listeners

[Thomas Stig Jacobsen (tsja10)]

I've pushed a move of the functionality in verify and doInBackground as discussed.

However, the TAPNComposerExtended cannot replace the old TAPNComposer just as is since the constructors differs from each other and just adding a second constructor to the new TAPNComposerExtended would give null pointer exceptions, a lot of if-sentences and a lot less readable code than now.

Essentially the new composer takes a HashMap<TimedArcPetriNet, DataLayer> guiModel in it's constructor so it cannot be used everywhere either since not everywhere a guiModel is available.

[Mathias Grund Sørensen (mathias.grund)]

Bug regarding the way you enable cumulative memory reporting:

Open alternativ-bit-protocol,
change k to 50,
run discrete engine with under-approximation,
interrupt when memory has accumulated some higher number (I interrupted at 50-60MB),
open intro-example and verify.

Memory is now reported as 50-60MB (because the cumulative option is not turned off). I strongly suggest adding cumulative option as a parameter for the attach function call rather than as a separate function call as it is currently implemented (please also keep the function to attach without the flag).

review: Needs Fixing

[Jiri Srba (srba)]

I tried to make a summary of what should be done with suggested solutions so that
we can merge this branch to trunk asap (other branches are waiting on this merge at the moment).

1. Issue with long methods that should be split into more functions.
   (Not essential for merge, could be done in a separate branch and I could put it
    on the bug list unless someone will take a look at this before the merge).

2. s.append issues by Kenneth is in other code as well; I suggest not to fix it in this
   branch and make a separate branch for this (I will make a bug report so that we do not forget).

3. TAPNComposerExtended should be renamed to TAPNComposedWithGUI. Could the normal be
   replaced with the one with GUI or use inheritance as Jakob suggested? Looking forward
   to hear options on this.

4. The memory monitor is buggy at the moment and should be changed according to Mathias' suggestion
   (extra argument that would signal that it is a commulative memory monitor). See the
   issue in the comment just above.

Please, react to those comments so that we can merge it asap. Thanks.

[Thomas Stig Jacobsen (tsja10)]

There is a problem doing the solution that Mathias suggested. Both solutions (the one that is now and Mathias’) are possible but there are tradeoffs.
Doing it the way it is now, it is possible to turn off the cumulative mode on and off from anywhere in the problem. For example as now, in the code for approximations and event listeners for when an verification is aborted (I’ve fixed that bug, just to see how easy it was).
In the way that Mathias’ suggested, it is “prettier”, I totally agree that – first off. I’ve implemented the solution and it works, but there is a but. The ProcessRunner class which attaches the MemoryMonitor to the verification process do not know if the cumulative mode should be turned on or off since it does not get the query of the verification passed on, and I don’t think that it should.
So there is a tradeoff here, so what solution do people think would be the best?

[Mathias Grund Sørensen (mathias.grund)]

> There is a problem doing the solution that Mathias suggested. Both solutions
> (the one that is now and Mathias’) are possible but there are tradeoffs.
> Doing it the way it is now, it is possible to turn off the cumulative mode on
> and off from anywhere in the problem. For example as now, in the code for
> approximations and event listeners for when an verification is aborted (I’ve
> fixed that bug, just to see how easy it was).
> In the way that Mathias’ suggested, it is “prettier”, I totally agree that –
> first off. I’ve implemented the solution and it works, but there is a but. The
> ProcessRunner class which attaches the MemoryMonitor to the verification
> process do not know if the cumulative mode should be turned on or off since it
> does not get the query of the verification passed on, and I don’t think that
> it should.
> So there is a tradeoff here, so what solution do people think would be the
> best?

I see. I agree that it can be a function call by itself then (as we don't want to refactor too much of the existing code at the moment). I then suggest changing setCumulativePeakMemory to a function cumulateMemory() which means that on _the next_ attach, memory is not reset, but the flag is returned to off by the end of the attach method. Having to always remember to turn it off is not good (we will surely forget it somewhere) IMO...

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

936. By Jiri Srba on 2014-05-22

merged with trunk

937. By Jiri Srba on 2014-05-24

merged with trunk

938. By Thomas Stig Jacobsen on 2014-05-25

Commit of the new MemoryMonitor as suggested by Mathias

[Thomas Stig Jacobsen (tsja10)]

Just pushed a commit to fix this.

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

939. By Jiri Srba on 2014-05-25

Query was resolved using over-approximation
is renamed to
Query was resolved using state equations.

[Mathias Grund Sørensen (mathias.grund)]

Cumulative memory implementation nok looks as expected. I have not run the code or considered other parts of the code in this review.

review: Approve (code)

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

940. By Christoffer Moesgaard on 2014-05-27

Splitting up large methods into smaller functions

[Thomas Stig Jacobsen (tsja10)]

Sine and Christoffer have now tried to split up both makeTraceTAPN and modifyTAPN, please review these changes.

[Jiri Srba (srba)]

Thomas, has it been pushed 16 hours ago by Christoffer or is it something new that has not been pushed yet?

review: Needs Information

[Thomas Stig Jacobsen (tsja10)]

Yes it is the commit by Christoffer (#940).

[lp:~tapaal-approx/tapaal/tapaal-approx-new]

941. By Jiri Srba on 2014-05-28

renamed TAPNComposerExtended to TAPNComposerWithGUI

[Jiri Srba (srba)]

I have renamed TAPNComposerExtended to TAPNComposerGUI.

We should take a look if we need both composers or only one, I will make a separate bug report.

Otherwise the rest should be fixed now. The s.append tests in batch processing cannot be
simply replaced by if block due to delimiters. I think it is ok as it is.

review: Approve

[Jiri Srba (srba)]

review: Needs Resubmitting

[Jiri Srba (srba)]

review: Approve

[Jakob Taankvist (jakob-taankvist)]

review: Approve

=== added directory 'src/dk/aau/cs/approximation'
=== added file 'src/dk/aau/cs/approximation/ApproximationWorker.java'
--- src/dk/aau/cs/approximation/ApproximationWorker.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/approximation/ApproximationWorker.java	2014-05-28 18:52:41 +0000
@@ -0,0 +1,671 @@
+package dk.aau.cs.approximation;
+
+import java.math.BigDecimal;
+
+import javax.swing.SwingWorker.StateValue;
+
+import pipe.dataLayer.TAPNQuery.SearchOption;
+import pipe.dataLayer.TAPNQuery.TraceOption;
+import pipe.gui.FileFinderImpl;
+import pipe.gui.MessengerImpl;
+import pipe.gui.RunVerificationBase;
+import pipe.gui.widgets.InclusionPlaces;
+import dk.aau.cs.Messenger;
+import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
+import dk.aau.cs.model.tapn.TAPNQuery;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
+import dk.aau.cs.model.tapn.TimedToken;
+import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
+import dk.aau.cs.model.tapn.simulation.TimeDelayStep;
+import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetStep;
+import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
+import dk.aau.cs.model.tapn.simulation.TimedTransitionStep;
+import dk.aau.cs.translations.ReductionOption;
+import dk.aau.cs.util.MemoryMonitor;
+import dk.aau.cs.util.Tuple;
+import dk.aau.cs.verification.ITAPNComposer;
+import dk.aau.cs.verification.ModelChecker;
+import dk.aau.cs.verification.NameMapping;
+import dk.aau.cs.verification.QueryResult;
+import dk.aau.cs.verification.QueryType;
+import dk.aau.cs.verification.TAPNComposer;
+import dk.aau.cs.verification.TAPNTraceDecomposer;
+import dk.aau.cs.verification.VerificationOptions;
+import dk.aau.cs.verification.VerificationResult;
+import dk.aau.cs.verification.UPPAAL.Verifyta;
+import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
+import dk.aau.cs.verification.VerifyTAPN.ModelReduction;
+import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
+import dk.aau.cs.verification.VerifyTAPN.VerifyPNOptions;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
+import dk.aau.cs.verification.batchProcessing.BatchProcessingWorker;
+
+public class ApproximationWorker {
+	public VerificationResult<TAPNNetworkTrace> normalWorker(VerificationOptions options, ModelChecker modelChecker,
+			Tuple<TimedArcPetriNet, NameMapping> transformedModel, ITAPNComposer composer, TAPNQuery clonedQuery,
+			RunVerificationBase verificationBase, TimedArcPetriNetNetwork model) throws Exception {
+		
+		// If options is of an instance of VerifyTAPNOptions then save the inclusion places before verify alters them
+		InclusionPlaces oldInclusionPlaces = null;
+		if (options instanceof VerifyTAPNOptions)
+			oldInclusionPlaces = ((VerifyTAPNOptions) options).inclusionPlaces();
+		
+		// Enable SOME_TRACE if not already
+		TraceOption oldTraceOption = options.traceOption();
+		if ((options.enableOverApproximation() || options.enableUnderApproximation()) && !(options instanceof VerifytaOptions)) {
+			options.setTraceOption(TraceOption.SOME);
+		}
+		
+		VerificationResult<TAPNNetworkTrace> value = null;
+		VerificationResult<TimedArcPetriNetTrace> result = modelChecker.verify(options, transformedModel, clonedQuery);
+		if (verificationBase.isCancelled()) {
+			verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
+		}
+		if (result.error()) {
+			options.setTraceOption(oldTraceOption);
+			return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime());
+		}
+		else if (options.enableOverApproximation()) {
+			// Over-approximation
+			if (options.approximationDenominator() == 1) {
+				// If r = 1
+				// No matter what it answered -> return that answer
+				QueryResult queryResult = result.getQueryResult();
+				value =  new VerificationResult<TAPNNetworkTrace>(
+						queryResult,
+						decomposeTrace(result.getTrace(), transformedModel.value2(), model),
+						decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+						result.verificationTime(),
+						result.stats(),
+						result.isOverApproximationResult());
+				value.setNameMapping(transformedModel.value2());
+			} else {
+				// If r > 1
+				if (result.getTrace() != null && (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && result.getQueryResult().isQuerySatisfied())
+					|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && !result.getQueryResult().isQuerySatisfied()))) {
+						// If we have a trace AND ((EF OR EG) AND satisfied) OR ((AG OR AF) AND not satisfied)
+						// The results are inconclusive, but we get a trace and can use trace TAPN for verification.
+					
+						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
+						value = new VerificationResult<TAPNNetworkTrace>(
+								approxResult.getQueryResult(),
+								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime(),
+								approxResult.stats(),
+								approxResult.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+						
+						OverApproximation overaprx = new OverApproximation();
+			
+						//Create trace TAPN from the trace
+						Tuple<TimedArcPetriNet, NameMapping> transformedOriginalModel = composer.transformModel(model);
+						overaprx.makeTraceTAPN(transformedOriginalModel, value, clonedQuery);
+						
+						// Reset the inclusion places in order to avoid NullPointerExceptions
+						if (options instanceof VerifyTAPNOptions && oldInclusionPlaces != null)
+							((VerifyTAPNOptions) options).setInclusionPlaces(oldInclusionPlaces);
+			
+						// run model checker again for trace TAPN
+						MemoryMonitor.cumulateMemory();
+						result = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+						if (verificationBase.isCancelled()) {
+							verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
+						}
+						if (result.error()) {
+							options.setTraceOption(oldTraceOption);
+							// if the old trace option was none, we need to set the results traces to null so GUI doesn't try to display the traces later
+							if (oldTraceOption == TraceOption.NONE && value != null){
+								value.setTrace(null);
+								value.setSecondaryTrace(null);
+							}
+							return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime());
+						}
+						//Create the result from trace TAPN
+						renameTraceTransitions(result.getTrace());
+						renameTraceTransitions(result.getSecondaryTrace());
+						QueryResult queryResult = result.getQueryResult();
+						
+						// If ((EG OR EG) AND not satisfied trace) OR ((AG OR AF) AND satisfied trace) -> inconclusive
+						if (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && !queryResult.isQuerySatisfied()) 
+								|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && queryResult.isQuerySatisfied())){
+							queryResult.setApproximationInconclusive(true);
+						}
+						
+						// If satisfied trace -> Return result
+						// This is satisfied for EF and EG and not satisfied for AG and AF
+						value = new VerificationResult<TAPNNetworkTrace>(
+								queryResult,
+								decomposeTrace(result.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime() + result.verificationTime(),
+								approxResult.stats(),
+								approxResult.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+					} 
+					else if (((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && !result.getQueryResult().isQuerySatisfied())
+							|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && result.getQueryResult().isQuerySatisfied())) {
+						// If ((EF OR EG) AND not satisfied) OR ((AG OR AF) AND satisfied)
+						
+						QueryResult queryResult = result.getQueryResult();
+						
+						if(queryResult.hasDeadlock() || result.getQueryResult().queryType() == QueryType.EG || result.getQueryResult().queryType() == QueryType.AF){
+							queryResult.setApproximationInconclusive(true);
+						}
+						
+						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
+						value = new VerificationResult<TAPNNetworkTrace>(
+								approxResult.getQueryResult(),
+								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime(),
+								approxResult.stats(),
+								approxResult.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+					} else {
+						// We cannot use the result directly, and did not get a trace.
+						
+						QueryResult queryResult = result.getQueryResult();
+						queryResult.setApproximationInconclusive(true);
+						
+						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
+						value = new VerificationResult<TAPNNetworkTrace>(
+								approxResult.getQueryResult(),
+								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime(),
+								approxResult.stats(),
+								approxResult.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+						
+					}
+			}
+		} 
+		else if (options.enableUnderApproximation()) {
+			// Under-approximation
+			
+			if (result.getTrace() != null) {
+				for (TimedArcPetriNetStep k : result.getTrace()) {
+					if (k instanceof TimeDelayStep){
+						((TimeDelayStep) k).setDelay(((TimeDelayStep) k).delay().multiply(new BigDecimal(options.approximationDenominator())));
+					}
+					else if (k instanceof TimedTransitionStep) {
+						for (TimedToken a : ((TimedTransitionStep) k).consumedTokens()){
+							a.setAge(a.age().multiply(new BigDecimal(options.approximationDenominator())));
+						}
+					}
+				}
+			}
+			
+			if (options.approximationDenominator() == 1) { 
+				// If r = 1
+				// No matter it answered -> return that answer
+				QueryResult queryResult= result.getQueryResult();
+				value =  new VerificationResult<TAPNNetworkTrace>(
+						queryResult,
+						decomposeTrace(result.getTrace(), transformedModel.value2(), model),
+						decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+						result.verificationTime(),
+						result.stats(),
+						result.isOverApproximationResult());
+				value.setNameMapping(transformedModel.value2());
+			}
+			else {
+				// If r > 1
+				if ((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && ! result.getQueryResult().isQuerySatisfied()
+				|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && result.getQueryResult().isQuerySatisfied())) {
+					// If ((EF OR EG) AND not satisfied) OR ((AG OR AF) and satisfied) -> Inconclusive
+					QueryResult queryResult= result.getQueryResult();
+					queryResult.setApproximationInconclusive(true);
+					value =  new VerificationResult<TAPNNetworkTrace>(
+							queryResult,
+							decomposeTrace(result.getTrace(), transformedModel.value2(), model),
+							decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+							result.verificationTime(),
+							result.stats(),
+							result.isOverApproximationResult());
+					value.setNameMapping(transformedModel.value2());
+				} else if ((result.getQueryResult().queryType() == QueryType.EF || result.getQueryResult().queryType() == QueryType.EG) && result.getQueryResult().isQuerySatisfied()
+						|| ((result.getQueryResult().queryType() == QueryType.AG || result.getQueryResult().queryType() == QueryType.AF) && ! result.getQueryResult().isQuerySatisfied())) {
+										
+					if (result.getTrace() != null){
+						// If query does have deadlock or EG or AF a trace -> create trace TAPN
+						//Create the verification satisfied result for the approximation
+						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
+						value = new VerificationResult<TAPNNetworkTrace>(
+								approxResult.getQueryResult(),
+								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime(),
+								approxResult.stats(),
+								result.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+						
+						OverApproximation overaprx = new OverApproximation();
+						
+			
+						//Create trace TAPN from the trace
+						Tuple<TimedArcPetriNet, NameMapping> transformedOriginalModel = composer.transformModel(model);
+						overaprx.makeTraceTAPN(transformedOriginalModel, value, clonedQuery);
+						
+						// Reset the inclusion places in order to avoid NullPointerExceptions
+						if (options instanceof VerifyTAPNOptions && oldInclusionPlaces != null)
+							((VerifyTAPNOptions) options).setInclusionPlaces(oldInclusionPlaces);
+			
+						//run model checker again for trace TAPN
+						MemoryMonitor.cumulateMemory();
+						result = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+						if (verificationBase.isCancelled()) {
+							verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
+						}
+						if (result.error()) {
+							options.setTraceOption(oldTraceOption);
+							// if the old trace option was none, we need to set the results traces to null so GUI doesn't try to display the traces later
+							if (oldTraceOption == TraceOption.NONE && value != null){
+								value.setTrace(null);
+								value.setSecondaryTrace(null);
+							}
+							return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime());
+						}
+						//Create the result from trace TAPN
+						renameTraceTransitions(result.getTrace());
+						renameTraceTransitions(result.getSecondaryTrace());
+						QueryResult queryResult = result.getQueryResult();
+						
+						
+						// If (EF or EG AND not satisfied trace) OR (AG or AF AND satisfied trace) -> inconclusive
+						if ((result.getQueryResult().queryType() == QueryType.EF && !queryResult.isQuerySatisfied())
+							|| (result.getQueryResult().queryType() == QueryType.AG && queryResult.isQuerySatisfied())
+							|| (result.getQueryResult().queryType() == QueryType.EG && !queryResult.isQuerySatisfied())
+							|| (result.getQueryResult().queryType() == QueryType.AF && queryResult.isQuerySatisfied())) {
+							queryResult.setApproximationInconclusive(true);
+						}
+						
+						// If satisfied trace) -> Return result
+						// This is satisfied for EF and EG and not satisfied for AG and AF
+						value = new VerificationResult<TAPNNetworkTrace>(
+								queryResult,
+								decomposeTrace(result.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime() + result.verificationTime(),
+								approxResult.stats(),
+								approxResult.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+					}
+					else {
+						// the query contains deadlock, but we do not have a trace.
+						QueryResult queryResult = result.getQueryResult();
+						queryResult.setApproximationInconclusive(true);
+						
+						VerificationResult<TimedArcPetriNetTrace> approxResult = result;
+						value = new VerificationResult<TAPNNetworkTrace>(
+								approxResult.getQueryResult(),
+								decomposeTrace(approxResult.getTrace(), transformedModel.value2(), model),
+								decomposeTrace(approxResult.getSecondaryTrace(), transformedModel.value2(), model),
+								approxResult.verificationTime(),
+								approxResult.stats(),
+								approxResult.isOverApproximationResult());
+						value.setNameMapping(transformedModel.value2());
+					}
+				}
+			}
+		} 
+		else {
+			value =  new VerificationResult<TAPNNetworkTrace>(
+					result.getQueryResult(),
+					decomposeTrace(result.getTrace(), transformedModel.value2(), model),
+					decomposeTrace(result.getSecondaryTrace(), transformedModel.value2(), model),
+					result.verificationTime(),
+					result.stats(),
+					result.isOverApproximationResult());
+			value.setNameMapping(transformedModel.value2());
+		}
+		
+		options.setTraceOption(oldTraceOption);
+		// if the old traceoption was none, we need to set the results traces to null so GUI doesn't try to display the traces later
+		if (oldTraceOption == TraceOption.NONE){
+			value.setTrace(null);
+			value.setSecondaryTrace(null);
+		}
+		
+		return value;
+	}
+
+	public VerificationResult<TimedArcPetriNetTrace> batchWorker(Tuple<TimedArcPetriNet, NameMapping> composedModel,
+			VerificationOptions options, pipe.dataLayer.TAPNQuery query, LoadedBatchProcessingModel model,
+			ModelChecker modelChecker, TAPNQuery queryToVerify, TAPNQuery clonedQuery, BatchProcessingWorker verificationBase) throws Exception {
+		InclusionPlaces oldInclusionPlaces = null;
+		if (options instanceof VerifyTAPNOptions)
+			oldInclusionPlaces = ((VerifyTAPNOptions) options).inclusionPlaces();
+		
+		Tuple<TimedArcPetriNet, NameMapping> transformedOriginalModel = new Tuple<TimedArcPetriNet, NameMapping>(composedModel.value1().copy(), composedModel.value2());
+		
+		TraceOption oldTraceOption = options.traceOption();
+		if (query != null && query.isOverApproximationEnabled()) {
+			// Create a fresh model
+			composedModel = composeModel(model);
+			OverApproximation overaprx = new OverApproximation();
+			overaprx.modifyTAPN(composedModel.value1(), query.approximationDenominator());
+			options.setTraceOption(TraceOption.SOME);
+		} else if (query != null && query.isUnderApproximationEnabled()) {
+			// Create a fresh model
+			composedModel = composeModel(model);
+			UnderApproximation underaprx = new UnderApproximation();
+			underaprx.modifyTAPN(composedModel.value1(), query.approximationDenominator());
+			options.setTraceOption(TraceOption.SOME);
+		}
+		
+		VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify);		
+		
+		VerificationResult<TAPNNetworkTrace> valueNetwork = null;	//The final result is meant to be a PetriNetTrace but to make traceTAPN we make a networktrace
+		VerificationResult<TimedArcPetriNetTrace> value = null;
+		if (verificationResult.error()) {
+			options.setTraceOption(oldTraceOption);
+			return new VerificationResult<TimedArcPetriNetTrace>(verificationResult.errorMessage(), verificationResult.verificationTime());
+		}
+		else if (query != null && query.isOverApproximationEnabled()) {		
+			//Create the verification satisfied result for the approximation
+            
+            // Over-approximation
+			if (query.approximationDenominator() == 1) {
+                // If r = 1
+                // No matter what EF and AG answered -> return that answer
+               QueryResult queryResult = verificationResult.getQueryResult();
+               value =  new VerificationResult<TimedArcPetriNetTrace>(
+					queryResult,
+					verificationResult.getTrace(),
+					verificationResult.getSecondaryTrace(),
+					verificationResult.verificationTime(),
+					verificationResult.stats(),
+					verificationResult.isOverApproximationResult());
+				value.setNameMapping(composedModel.value2());
+	        } else {
+	            // If r > 1
+				if (verificationResult.getTrace() != null && (((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG ) && verificationResult.getQueryResult().isQuerySatisfied())
+						|| ((verificationResult.getQueryResult().queryType() == QueryType.AG || verificationResult.getQueryResult().queryType() == QueryType.AF) && !verificationResult.getQueryResult().isQuerySatisfied()))) {
+					// If ((EF OR EG) AND satisfied) OR ((AG OR AF) AND not satisfied)
+					//Create the verification satisfied result for the approximation
+	                VerificationResult<TimedArcPetriNetTrace> approxResult = verificationResult;
+	                valueNetwork = new VerificationResult<TAPNNetworkTrace>(
+	                            approxResult.getQueryResult(),
+	                            decomposeTrace(approxResult.getTrace(), composedModel.value2(), model.network()),
+	                            decomposeTrace(approxResult.getSecondaryTrace(), composedModel.value2(), model.network()),
+	                            approxResult.verificationTime(),
+	                            approxResult.stats(),
+	        					verificationResult.isOverApproximationResult());
+	                valueNetwork.setNameMapping(composedModel.value2());
+	                
+	                OverApproximation overaprx = new OverApproximation();
+	                
+	                //Create trace TAPN from the network trace
+	                overaprx.makeTraceTAPN(transformedOriginalModel, valueNetwork, clonedQuery);
+	                
+	                // Reset the inclusion places in order to avoid NullPointerExceptions
+	                if (options instanceof VerifyTAPNOptions && oldInclusionPlaces != null){
+	                    ((VerifyTAPNOptions) options).setInclusionPlaces(oldInclusionPlaces);
+	                }
+
+	                //run model checker again for trace TAPN
+	                MemoryMonitor.cumulateMemory();
+	                verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+	                if (verificationBase.isCancelled()) {
+	                	verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
+	                }
+	                if (verificationResult.error()) {
+	                	options.setTraceOption(oldTraceOption);
+	                    return new VerificationResult<TimedArcPetriNetTrace>(
+	                    		verificationResult.errorMessage(),
+	                    		verificationResult.verificationTime() + approxResult.verificationTime());
+	                }
+	                //Create the result from trace TAPN
+	                renameTraceTransitions(verificationResult.getTrace());
+	                renameTraceTransitions(verificationResult.getSecondaryTrace());
+	                QueryResult queryResult = verificationResult.getQueryResult();
+	                
+	                // If ((EF OR EG) AND not satisfied trace) OR ((AG OR AF) AND satisfied trace) -> inconclusive
+					if (((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && !queryResult.isQuerySatisfied()) 
+							|| ((verificationResult.getQueryResult().queryType() == QueryType.AG || verificationResult.getQueryResult().queryType() == QueryType.AF) && queryResult.isQuerySatisfied())){
+						queryResult.setApproximationInconclusive(true);
+					}
+	                // If satisfied trace -> Return result
+	                // This is satisfied for EF and EG and not satisfied for AG and AF
+	                value = new VerificationResult<TimedArcPetriNetTrace>(
+	                        queryResult,
+	                        approxResult.getTrace(),
+	                        approxResult.getSecondaryTrace(),
+	                        approxResult.verificationTime() + verificationResult.verificationTime(),
+	                        approxResult.stats(),
+	    					verificationResult.isOverApproximationResult());
+	                value.setNameMapping(composedModel.value2());
+	            }
+				else if (((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && !verificationResult.getQueryResult().isQuerySatisfied())
+						|| ((verificationResult.getQueryResult().queryType() == QueryType.AG || verificationResult.getQueryResult().queryType() == QueryType.AF) && verificationResult.getQueryResult().isQuerySatisfied())) {
+	                // If (EF AND EG not satisfied) OR (AG AND AF satisfied)
+	               
+	                QueryResult queryResult = verificationResult.getQueryResult();
+	              
+	                if(queryResult.hasDeadlock() || queryResult.queryType() == QueryType.EG || queryResult.queryType() == QueryType.AF){
+						queryResult.setApproximationInconclusive(true);
+					}
+	                
+	                value =  new VerificationResult<TimedArcPetriNetTrace>(
+						queryResult,
+						verificationResult.getTrace(),
+						verificationResult.getSecondaryTrace(),
+						verificationResult.verificationTime(),
+						verificationResult.stats(),
+						verificationResult.isOverApproximationResult());
+				    value.setNameMapping(composedModel.value2());
+	            }
+				else {
+					// We cannot use the result directly, and did not get a trace.
+					
+					QueryResult queryResult = verificationResult.getQueryResult();
+					
+					queryResult.setApproximationInconclusive(true);
+	                
+	                value =  new VerificationResult<TimedArcPetriNetTrace>(
+						queryResult,
+						verificationResult.getTrace(),
+						verificationResult.getSecondaryTrace(),
+						verificationResult.verificationTime(),
+						verificationResult.stats(),
+						verificationResult.isOverApproximationResult());
+				    value.setNameMapping(composedModel.value2());
+					
+				}
+	        }
+	    } 
+	    else if (query != null && query.isUnderApproximationEnabled()) {
+	        // Under-approximation
+			
+	        if (query.approximationDenominator() == 1) { 
+	            // If r = 1
+	            // No matter what EF and AG answered -> return that answer
+	            QueryResult queryResult= verificationResult.getQueryResult();
+	            value =  new VerificationResult<TimedArcPetriNetTrace>(
+                    queryResult,
+                    verificationResult.getTrace(),
+                    verificationResult.getSecondaryTrace(),
+                    verificationResult.verificationTime(),
+                    verificationResult.stats(),
+					verificationResult.isOverApproximationResult());
+                value.setNameMapping(composedModel.value2());
+	        }
+	        else {
+	            // If r > 1
+				if ((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && ! verificationResult.getQueryResult().isQuerySatisfied()
+				|| ((verificationResult.getQueryResult().queryType() == QueryType.AG || verificationResult.getQueryResult().queryType() == QueryType.AF) && verificationResult.getQueryResult().isQuerySatisfied())) {
+					// If ((EF OR EG) AND not satisfied) OR ((AG OR AF) and satisfied) -> Inconclusive
+                    
+                    QueryResult queryResult = verificationResult.getQueryResult();
+                    queryResult.setApproximationInconclusive(true);
+                    value =  new VerificationResult<TimedArcPetriNetTrace>(
+                            queryResult,
+                            verificationResult.getTrace(),
+                            verificationResult.getSecondaryTrace(),
+                            verificationResult.verificationTime(),
+                            verificationResult.stats(),
+        					verificationResult.isOverApproximationResult());
+                    value.setNameMapping(composedModel.value2());
+	                    
+				} else if ((verificationResult.getQueryResult().queryType() == QueryType.EF || verificationResult.getQueryResult().queryType() == QueryType.EG) && verificationResult.getQueryResult().isQuerySatisfied()
+						|| ((verificationResult.getQueryResult().queryType() == QueryType.AG || verificationResult.getQueryResult().queryType() == QueryType.AF) && ! verificationResult.getQueryResult().isQuerySatisfied())) {
+					// ((EF OR EG) AND satisfied) OR ((AG OR AF) and not satisfied) -> Check for deadlock
+	                    
+					if(verificationResult.getTrace() != null) {
+	                    // If query does have deadlock -> create trace TAPN
+	                    //Create the verification satisfied result for the approximation
+						VerificationResult<TimedArcPetriNetTrace> approxResult = verificationResult;
+	                    valueNetwork = new VerificationResult<TAPNNetworkTrace>(
+	                    		approxResult.getQueryResult(),
+	                        decomposeTrace(approxResult.getTrace(), composedModel.value2(), model.network()),
+	                        decomposeTrace(approxResult.getSecondaryTrace(), composedModel.value2(), model.network()),
+	                        approxResult.verificationTime(),
+	                        approxResult.stats(),
+	                        approxResult.isOverApproximationResult());
+	                    valueNetwork.setNameMapping(composedModel.value2());
+	                    
+	                    OverApproximation overaprx = new OverApproximation();
+	        
+	                    //Create trace TAPN from the trace
+	                    overaprx.makeTraceTAPN(transformedOriginalModel, valueNetwork, clonedQuery);
+	                    
+	                    // Reset the inclusion places in order to avoid NullPointerExceptions
+	                    if (options instanceof VerifyTAPNOptions && oldInclusionPlaces != null)
+	                        ((VerifyTAPNOptions) options).setInclusionPlaces(oldInclusionPlaces);
+	        
+	                    //run model checker again for trace TAPN
+	                    MemoryMonitor.cumulateMemory();
+	                    verificationResult = modelChecker.verify(options, transformedOriginalModel, clonedQuery);
+	                    if (verificationBase.isCancelled()) {
+	                    	verificationBase.firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
+	                    }
+	                    if (verificationResult.error()) {
+	                    	options.setTraceOption(oldTraceOption);
+	        				return new VerificationResult<TimedArcPetriNetTrace>(
+	        						verificationResult.errorMessage(),
+	        						verificationResult.verificationTime() + approxResult.verificationTime());
+	        			}
+	                    
+	                    //Create the result from trace TAPN
+	                    renameTraceTransitions(verificationResult.getTrace());
+	                    renameTraceTransitions(verificationResult.getSecondaryTrace());
+	                    QueryResult queryResult = verificationResult.getQueryResult();
+	                    
+	                    // If (EF or EG AND not satisfied trace) OR (AG or AF AND satisfied trace) -> inconclusive
+	                    if ((verificationResult.getQueryResult().queryType() == QueryType.EF && !queryResult.isQuerySatisfied())
+	                        || (verificationResult.getQueryResult().queryType() == QueryType.AG && queryResult.isQuerySatisfied())
+	                        || (verificationResult.getQueryResult().queryType() == QueryType.EG && !queryResult.isQuerySatisfied())
+							|| (verificationResult.getQueryResult().queryType() == QueryType.AF && queryResult.isQuerySatisfied())) {
+	                        queryResult.setApproximationInconclusive(true);
+	                    }
+	                    
+	                    // If satisfied trace -> Return result
+	                    // This is satisfied for EF and EG and not satisfied for AG and AF
+	                   value =  new VerificationResult<TimedArcPetriNetTrace>(
+	                		    queryResult,
+	                            verificationResult.getTrace(),
+	                            verificationResult.getSecondaryTrace(),
+	                            verificationResult.verificationTime() + approxResult.verificationTime(),
+	                            verificationResult.stats(),
+	        					verificationResult.isOverApproximationResult());
+	                    value.setNameMapping(composedModel.value2());
+	                }
+	                else {
+	                	QueryResult queryResult = verificationResult.getQueryResult();
+						
+						queryResult.setApproximationInconclusive(true);
+		                
+		                value =  new VerificationResult<TimedArcPetriNetTrace>(
+							queryResult,
+							verificationResult.getTrace(),
+							verificationResult.getSecondaryTrace(),
+							verificationResult.verificationTime(),
+							verificationResult.stats(),
+							verificationResult.isOverApproximationResult());
+					    value.setNameMapping(composedModel.value2());
+	                }
+	            }
+	        }
+	    } else {
+	        value =  new VerificationResult<TimedArcPetriNetTrace>(
+	                verificationResult.getQueryResult(),
+	                verificationResult.getTrace(),
+	                verificationResult.getSecondaryTrace(),
+	                verificationResult.verificationTime(),
+	                verificationResult.stats(),
+					verificationResult.isOverApproximationResult());
+	        value.setNameMapping(composedModel.value2());
+	    }
+		
+		options.setTraceOption(oldTraceOption);
+		return value;
+	}
+	
+	private TAPNNetworkTrace decomposeTrace(TimedArcPetriNetTrace trace, NameMapping mapping, TimedArcPetriNetNetwork model) {
+		if (trace == null)
+			return null;
+
+		TAPNTraceDecomposer decomposer = new TAPNTraceDecomposer(trace, model, mapping);
+		return decomposer.decompose();
+	}
+	
+	private void renameTraceTransitions(TimedArcPetriNetTrace trace) {
+		if (trace != null){
+			trace.reduceTraceForOriginalNet("_traceNet_", "PTRACE");
+			trace.removeTokens("PBLOCK");
+		}
+	}
+	
+	private Tuple<TimedArcPetriNet, NameMapping> composeModel(LoadedBatchProcessingModel model) {
+		ITAPNComposer composer = new TAPNComposer(new Messenger(){
+			public void displayInfoMessage(String message) { }
+			public void displayInfoMessage(String message, String title) {}
+			public void displayErrorMessage(String message) {}
+			public void displayErrorMessage(String message, String title) {}
+			public void displayWrappedErrorMessage(String message, String title) {}
+			
+		});
+		Tuple<TimedArcPetriNet, NameMapping> composedModel = composer.transformModel(model.network());
+		return composedModel;
+	}
+	
+	private ModelChecker getModelChecker(pipe.dataLayer.TAPNQuery query) {
+		if(query.getReductionOption() == ReductionOption.VerifyTAPN)
+			return getVerifyTAPN();
+		else if(query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification)
+			return getVerifyTAPNDiscreteVerification();
+		else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
+			return getVerifyPN();
+		else
+			return getVerifyta();
+	}
+	
+	private Verifyta getVerifyta() {
+		Verifyta verifyta = new Verifyta(new FileFinderImpl(), new MessengerImpl());
+		verifyta.setup();
+		return verifyta;
+	}
+
+	private static VerifyTAPN getVerifyTAPN() {
+		VerifyTAPN verifytapn = new VerifyTAPN(new FileFinderImpl(), new MessengerImpl());
+		verifytapn.setup();
+		return verifytapn;
+	}
+	
+	private static VerifyPN getVerifyPN() {
+		VerifyPN verifypn = new VerifyPN(new FileFinderImpl(), new MessengerImpl());
+		verifypn.setup();
+		return verifypn;
+	}
+	
+	private static VerifyTAPNDiscreteVerification getVerifyTAPNDiscreteVerification() {
+		VerifyTAPNDiscreteVerification verifytapnDiscreteVerification = new VerifyTAPNDiscreteVerification(new FileFinderImpl(), new MessengerImpl());
+		verifytapnDiscreteVerification.setup();
+		return verifytapnDiscreteVerification;
+	}
+}

=== added file 'src/dk/aau/cs/approximation/ITAPNApproximation.java'
--- src/dk/aau/cs/approximation/ITAPNApproximation.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/approximation/ITAPNApproximation.java	2014-05-28 18:52:41 +0000
@@ -0,0 +1,9 @@
+package dk.aau.cs.approximation;
+
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.verification.VerificationOptions;
+
+public interface ITAPNApproximation {
+	//Returns a copy of a network which is the approximated network
+	public void modifyTAPN(TimedArcPetriNet net, int approximationDenominator);
+}

=== added file 'src/dk/aau/cs/approximation/OverApproximation.java'
--- src/dk/aau/cs/approximation/OverApproximation.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/approximation/OverApproximation.java	2014-05-28 18:52:41 +0000
@@ -0,0 +1,264 @@
+package dk.aau.cs.approximation;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Map.Entry;
+
+import dk.aau.cs.TCTL.TCTLAFNode;
+import dk.aau.cs.TCTL.TCTLAGNode;
+import dk.aau.cs.TCTL.TCTLAbstractProperty;
+import dk.aau.cs.TCTL.TCTLAndListNode;
+import dk.aau.cs.TCTL.TCTLAtomicPropositionNode;
+import dk.aau.cs.TCTL.TCTLConstNode;
+import dk.aau.cs.TCTL.TCTLEFNode;
+import dk.aau.cs.TCTL.TCTLEGNode;
+import dk.aau.cs.TCTL.TCTLNotNode;
+import dk.aau.cs.TCTL.TCTLOrListNode;
+import dk.aau.cs.TCTL.TCTLPlaceNode;
+import dk.aau.cs.model.tapn.*;
+import dk.aau.cs.model.tapn.simulation.*;
+import dk.aau.cs.util.Tuple;
+import dk.aau.cs.verification.NameMapping;
+import dk.aau.cs.verification.VerificationOptions;
+import dk.aau.cs.verification.VerificationResult;
+import pipe.dataLayer.TAPNQuery;
+
+public class OverApproximation implements ITAPNApproximation {
+	@Override
+	public void modifyTAPN(TimedArcPetriNet net, int approximationDenominator) {
+		// Fix input arcs
+		for (TimedInputArc arc : net.inputArcs()) {
+			TimeInterval oldInterval = arc.interval();
+			TimeInterval newInterval = modifyIntervals(oldInterval, approximationDenominator);
+			
+			arc.setTimeInterval(newInterval);
+		}
+		 
+		// Fix transport arcs
+		for (TransportArc arc : net.transportArcs()) {
+			TimeInterval oldInterval = arc.interval();
+			TimeInterval newInterval = modifyIntervals(oldInterval, approximationDenominator);
+			
+			arc.setTimeInterval(newInterval);
+		}
+		 
+		// Fix invariants in places
+		for (TimedPlace place : net.places()) {
+			if ( ! (place.invariant().upperBound() instanceof Bound.InfBound) && place.invariant().upperBound().value() > 0) {					
+				TimeInvariant oldInvariant = place.invariant();
+				place.setInvariant(new TimeInvariant(oldInvariant.isUpperNonstrict(), new IntBound((int) Math.ceil(oldInvariant.upperBound().value() / (double)approximationDenominator))));
+			}
+		}
+	}
+	
+	//Returns a copy of an approximated interval
+	private TimeInterval modifyIntervals(TimeInterval oldInterval, int denominator){
+		Bound newUpperBound;
+		// Do not calculate upper bound for infinite
+		if ( ! (oldInterval.upperBound() instanceof Bound.InfBound)) {
+			 // Calculate the new upper bound value. E.g. if the value is 22, the new value needs to be 3 given that r = 10
+			int oldUpperBoundValue = oldInterval.upperBound().value();
+			newUpperBound = new IntBound((int) Math.ceil((double)oldUpperBoundValue /  denominator));
+		} else {
+			newUpperBound = Bound.Infinity;
+		}
+		 
+		// Calculate the new lower bound
+		IntBound newLowerBound = new IntBound((int) Math.floor(oldInterval.lowerBound().value() / denominator));
+
+		return new TimeInterval(
+			 oldInterval.IsLowerBoundNonStrict(),
+			 newLowerBound,
+			 newUpperBound,
+			 oldInterval.IsUpperBoundNonStrict()
+			 );
+	}
+	
+	public void makeTraceTAPN(Tuple<TimedArcPetriNet, NameMapping> transformedModel, VerificationResult<TAPNNetworkTrace> result, dk.aau.cs.model.tapn.TAPNQuery query) {
+		TimedArcPetriNet net = transformedModel.value1();
+                
+		LocalTimedPlace currentPlace = new LocalTimedPlace("PTRACE0");
+		TimedToken currentToken = new TimedToken(currentPlace);
+		net.add(currentPlace);
+		currentPlace.addToken(currentToken);
+		
+		// Block place, which secures the net makes at most one transition not in the trace.
+		LocalTimedPlace blockPlace = new LocalTimedPlace("PBLOCK", TimeInvariant.LESS_THAN_INFINITY);
+		TimedToken blockToken = new TimedToken(blockPlace);
+		net.add(blockPlace);
+		blockPlace.addToken(blockToken);
+		
+		// Copy the original transitions
+		ArrayList<TimedTransition> originalTransitions = new ArrayList<TimedTransition>();
+		for (TimedTransition transition : net.transitions()) {
+			originalTransitions.add(transition);
+		}
+		
+		// Copy the original input arcs
+		ArrayList<TimedInputArc> originalInput = new ArrayList<TimedInputArc>();
+		for (TimedInputArc inputarc : net.inputArcs()) {
+			originalInput.add(inputarc);
+		}
+		
+		// Copy the original output arcs
+		ArrayList<TimedOutputArc> originalOutput = new ArrayList<TimedOutputArc>();
+		for (TimedOutputArc outputarc : net.outputArcs()) {
+			originalOutput.add(outputarc);
+		}
+		
+		// Copy the original inhibitor arcs
+		ArrayList<TimedInhibitorArc> originalInhibitor = new ArrayList<TimedInhibitorArc>();
+		for (TimedInhibitorArc inhibitor : net.inhibitorArcs()) {
+			originalInhibitor.add(inhibitor);
+		}
+		
+		// Copy the original transport arcs
+		ArrayList<TransportArc> originalTransport = new ArrayList<TransportArc>();
+		for (TransportArc transport : net.transportArcs()) {
+			originalTransport.add(transport);
+		}
+
+		int placeInteger = 0;
+		int transitionInteger = 0;
+		TimedOutputArc next = null;
+		boolean traceHasTransitionStep = false;
+		
+		TAPNNetworkTrace trace = result.getTrace();
+		HashMap<Tuple<String, String>, String> nameMap = transformedModel.value2().getOrgToMapped();
+		LocalTimedPlace loopStep = null;
+		boolean delayIsLoopStep = false;
+		
+		for(TAPNNetworkTraceStep step : trace) {
+			if (step instanceof TAPNNetworkTimeDelayStep){
+				// Skip if delay step, but check if this step is a delayStep
+				if(step.isLoopStep())
+				{
+					delayIsLoopStep = true;
+				}				
+			}
+			if (step instanceof TAPNNetworkTimedTransitionStep) {
+				//TimedTransition firedTransition = net.getTransitionByName(reversedNameMap.get(((TAPNNetworkTimedTransitionStep) step).getTransition().name()));
+				TAPNNetworkTimedTransitionStep tmpStep = (TAPNNetworkTimedTransitionStep)step;
+				//If the transition in step is shared, use "" as model for lookup in namemap
+				Tuple<String, String> key = new Tuple<String, String>(
+						(((TAPNNetworkTimedTransitionStep) step).getTransition().sharedTransition() == null ? tmpStep.getTransition().model().name() : ""), 
+						tmpStep.getTransition().name()); 
+				TimedTransition firedTransition = net.getTransitionByName(nameMap.get(key));
+				TimedTransition copyTransition = new TimedTransition(firedTransition.name() + "_traceNet_" + Integer.toString(++transitionInteger), firedTransition.isUrgent());
+				
+				net.add(copyTransition);
+				net.add(new TimedInputArc(currentPlace, copyTransition, TimeInterval.ZERO_INF));
+				
+				net.add(new TimedInputArc(blockPlace, copyTransition, TimeInterval.ZERO_INF));
+				net.add(new TimedOutputArc(copyTransition, blockPlace));
+				
+				// EG queries, where there is a loopStep, we need to store it for later use.
+				if(step.isLoopStep() || delayIsLoopStep)
+				{
+					loopStep = currentPlace;
+					delayIsLoopStep = false;
+				}
+				
+				currentPlace = new LocalTimedPlace("PTRACE" + Integer.toString(++placeInteger));
+				net.add(currentPlace);
+				next = new TimedOutputArc(copyTransition, currentPlace);
+				net.add(next);
+				
+				
+				for (TimedInputArc arc : originalInput) {
+					if (arc.destination() == firedTransition) {
+						net.add(new TimedInputArc(arc.source(), copyTransition, arc.interval(), arc.getWeight()));
+					}
+				}
+				for (TimedOutputArc arc : originalOutput) {
+					if (arc.source() == firedTransition) {
+						net.add(new TimedOutputArc(copyTransition, arc.destination(), arc.getWeight()));
+					}
+				}
+				for (TimedInhibitorArc arc : originalInhibitor) {
+					if (arc.destination() == firedTransition) {
+						net.add(new TimedInhibitorArc(arc.source(), copyTransition, arc.interval(), arc.getWeight()));
+					}
+				}
+				for (TransportArc arc : originalTransport) {
+					if (arc.transition() == firedTransition) {
+						net.add(new TransportArc(arc.source(), copyTransition, arc.destination(), arc.interval(), arc.getWeight()));
+					}
+				}
+				
+				traceHasTransitionStep = true;
+			}
+		}
+		
+		// If the trace is a EG trace with a loop, we need to incorporate the loop in traceTAPN
+		if(loopStep != null){
+			net.add(new TimedOutputArc(next.source(), loopStep));
+		}
+		
+		if(traceHasTransitionStep){
+			net.remove(next);
+			net.remove(currentPlace);
+		}
+		
+		modifyQuery(query, blockPlace);
+		
+		// An input arc from pBlock to all original transitions makes sure, that we can do deadlock checks.
+		for (TimedTransition transition : originalTransitions) {
+			net.add(new TimedInputArc(blockPlace, transition, TimeInterval.ZERO_INF));	
+		}           
+	}
+
+
+	private void modifyQuery(dk.aau.cs.model.tapn.TAPNQuery query, LocalTimedPlace blockPlace) {
+		TCTLAbstractProperty topNode = query.getProperty();
+		TCTLAtomicPropositionNode pBlock = new TCTLAtomicPropositionNode(new TCTLPlaceNode(blockPlace.name()), "=", new TCTLConstNode(1));
+		
+		// We need to modify the query to also have pBlock = 1. 
+		if(topNode instanceof TCTLEFNode)
+		{
+			if(((TCTLEFNode) topNode).getProperty() instanceof TCTLAndListNode){
+				((TCTLAndListNode) ((TCTLEFNode) topNode).getProperty()).addConjunct(pBlock);
+			}
+			else{
+				TCTLAndListNode andList = new TCTLAndListNode((((TCTLEFNode) topNode).getProperty()), pBlock);
+				((TCTLEFNode) topNode).setProperty(andList);
+			}
+				
+		}
+		else if(topNode instanceof TCTLAGNode)
+		{
+			TCTLNotNode notNode = new TCTLNotNode(pBlock);
+			
+			if(((TCTLAGNode) topNode).getProperty() instanceof TCTLOrListNode){
+				((TCTLOrListNode) ((TCTLAGNode) topNode).getProperty()).addDisjunct(notNode);;
+			}
+			else{
+				TCTLOrListNode orList = new TCTLOrListNode((((TCTLAGNode) topNode).getProperty()), notNode);
+				((TCTLAGNode) topNode).setProperty(orList);
+			}
+	
+		}
+		else if(topNode instanceof TCTLEGNode)
+		{
+			if(((TCTLEGNode) topNode).getProperty() instanceof TCTLAndListNode){
+				((TCTLAndListNode) ((TCTLEGNode) topNode).getProperty()).addConjunct(pBlock);
+			}
+			else{
+				TCTLAndListNode andList = new TCTLAndListNode((((TCTLEGNode) topNode).getProperty()), pBlock);
+				((TCTLEGNode) topNode).setProperty(andList);
+			}
+		}
+		else if(topNode instanceof TCTLAFNode)
+		{
+			TCTLNotNode notNode = new TCTLNotNode(pBlock);
+			
+			if(((TCTLAFNode) topNode).getProperty() instanceof TCTLOrListNode){
+				((TCTLOrListNode) ((TCTLAFNode) topNode).getProperty()).addDisjunct(notNode);;
+			}
+			else{
+				TCTLOrListNode orList = new TCTLOrListNode((((TCTLAFNode) topNode).getProperty()), notNode);
+				((TCTLAFNode) topNode).setProperty(orList);
+			}
+		}
+	}
+}

=== added file 'src/dk/aau/cs/approximation/UnderApproximation.java'
--- src/dk/aau/cs/approximation/UnderApproximation.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/approximation/UnderApproximation.java	2014-05-28 18:52:41 +0000
@@ -0,0 +1,191 @@
+package dk.aau.cs.approximation;
+
+import java.lang.reflect.Array;
+import java.util.ArrayList;
+
+import dk.aau.cs.model.tapn.Bound;
+import dk.aau.cs.model.tapn.IntBound;
+import dk.aau.cs.model.tapn.TAPNElement;
+import dk.aau.cs.model.tapn.TimeInterval;
+import dk.aau.cs.model.tapn.TimeInvariant;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedInhibitorArc;
+import dk.aau.cs.model.tapn.TimedInputArc;
+import dk.aau.cs.model.tapn.TimedOutputArc;
+import dk.aau.cs.model.tapn.TimedPlace;
+import dk.aau.cs.model.tapn.TimedTransition;
+import dk.aau.cs.model.tapn.TransportArc;
+import dk.aau.cs.verification.VerificationOptions;
+import pipe.dataLayer.DataLayer;
+import pipe.dataLayer.TAPNQuery;
+import pipe.gui.graphicElements.Arc;
+import pipe.gui.graphicElements.Place;
+import pipe.gui.graphicElements.Transition;
+import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
+import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
+import pipe.gui.graphicElements.tapn.TimedTransportArcComponent;
+
+public class UnderApproximation implements ITAPNApproximation {
+	@Override
+	public void modifyTAPN(TimedArcPetriNet net, int approximationDenominator) {
+		modifyTAPN(net, approximationDenominator, null);
+	}
+	
+	public void modifyTAPN(TimedArcPetriNet net, int approximationDenominator, DataLayer guiModel) {	
+		// Fix input arcs
+		ArrayList<TimedTransition> transitionsToDelete = new ArrayList<TimedTransition>();
+		
+		for (TimedInputArc arc : net.inputArcs()) {
+			 //Fix input arcs
+			TimeInterval oldInterval = arc.interval();
+			
+			TimeInterval newInterval = modifyIntervals(oldInterval, approximationDenominator);
+			
+			//New interval can be null if lower bound surpassed upper bound in rounding
+			if (newInterval != null){
+				arc.setTimeInterval(newInterval);
+			}
+			else{
+				//If an arcs interval became invalid we need to delete it, as well as the destination transition and any other arcs that transition has
+				//otherwise we could enable behavior which is not allowed for under approximation
+				if(!transitionsToDelete.contains(arc.destination())){
+					transitionsToDelete.add(arc.destination());
+				}
+			}
+		}
+
+		for (TransportArc arc : net.transportArcs()) {
+			//fix transport arcs
+			TimeInterval oldInterval = arc.interval();
+			
+			TimeInterval newInterval = modifyIntervals(oldInterval, approximationDenominator);
+			
+			//New interval can be null if lower bound surpassed upper bound in rounding
+			if (newInterval != null)
+				arc.setTimeInterval(newInterval);
+			else{
+				if(!transitionsToDelete.contains(arc.transition())){
+					transitionsToDelete.add(arc.transition());
+				}
+			}
+		}
+
+		for(TimedTransition transitionToDelete : transitionsToDelete){
+			if(guiModel != null){
+				deleteTransitionFromGuiModel(transitionToDelete, guiModel);
+			}
+			else{
+				deleteArcsFromTransition(transitionToDelete);
+			}
+			transitionToDelete.delete();
+		}	
+		
+		// Fix invariants in places
+		for (TimedPlace place1 : net.places()) {
+			if ( ! (place1.invariant().upperBound() instanceof Bound.InfBound) && place1.invariant().upperBound().value() > 0) {					
+				TimeInvariant oldInvariant = place1.invariant();
+				
+				int newInvariantBound = (int) Math.floor(oldInvariant.upperBound().value() / (double)approximationDenominator);
+				if(newInvariantBound != 0){
+					place1.setInvariant(new TimeInvariant(oldInvariant.isUpperNonstrict(), new IntBound(newInvariantBound)));
+				}
+				else{
+					place1.setInvariant(new TimeInvariant(true, new IntBound(0)));
+				}
+			}
+		}
+	}
+	
+	private void deleteTransitionFromGuiModel(TimedTransition transitionToDelete, DataLayer guiModel) {
+		// We assert here that deletions in the guimodel will also delete underlying model elements
+		Transition guiTransition = guiModel.getTransitionByName(transitionToDelete.name());
+		
+		for (Arc arc1 : guiModel.getArcs()){
+			if (arc1.getTarget() instanceof Place && arc1.getSource() == guiTransition) //If arc1 is an output arc
+			{ 
+				arc1.delete();
+			}
+			else if (arc1.getTarget() instanceof Transition && arc1.getTarget() == guiTransition){ //Else if arc1 is an input arc
+				arc1.delete();
+			}
+		}
+		guiTransition.delete();
+	}
+	
+	private void deleteArcsFromTransition(TimedTransition transitionToDelete) {
+		ArrayList<TimedInputArc> inputArcs = new ArrayList<TimedInputArc>();
+		//Add all did not work properly, so we do it manually.
+		for(TimedInputArc arc : transitionToDelete.getInputArcs()){
+			inputArcs.add(arc);
+		}
+		for(TimedInputArc arc : inputArcs){
+			arc.delete();
+		}
+		
+		ArrayList<TimedOutputArc> outputArcs = new ArrayList<TimedOutputArc>();
+		for(TimedOutputArc arc : transitionToDelete.getOutputArcs()){
+			outputArcs.add(arc);
+		}
+		for(TimedOutputArc arc : outputArcs){
+			arc.delete();
+		}
+		
+		ArrayList<TransportArc> transportArcs = new ArrayList<TransportArc>();
+		for(TransportArc arc : transitionToDelete.getTransportArcsGoingThrough()){
+			transportArcs.add(arc);
+		}
+		for(TransportArc arc : transportArcs){
+			arc.delete();
+		}
+		
+		ArrayList<TimedInhibitorArc> inhibitorArcs = new ArrayList<TimedInhibitorArc>();
+		for(TimedInhibitorArc arc : transitionToDelete.getInhibitorArcs()){
+			inhibitorArcs.add(arc);
+		}
+		for(TimedInhibitorArc arc : inhibitorArcs){
+			arc.delete();
+		}
+	}
+	
+	//Returns a copy of an approximated interval
+	private TimeInterval modifyIntervals(TimeInterval oldInterval, int denominator){
+		Bound newUpperBound;
+		// Do not calculate upper bound for infinite
+		if ( ! (oldInterval.upperBound() instanceof Bound.InfBound)) {
+			
+			 // Calculate the new upper bound value.
+			int oldUpperBoundValue = oldInterval.upperBound().value();
+			newUpperBound = new IntBound((int) Math.floor((double)oldUpperBoundValue /  denominator));
+		}
+		else
+			newUpperBound = Bound.Infinity;
+		 
+		// Calculate the new lower bound
+		IntBound newLowerBound = new IntBound((int) Math.ceil((double)oldInterval.lowerBound().value() / denominator));
+		 
+		// if the lower bound has become greater than the upper bound by rounding
+				if ( ! (oldInterval.upperBound() instanceof Bound.InfBound) && newLowerBound.value() > newUpperBound.value())
+				{
+					newLowerBound = new IntBound((int) Math.floor((double)oldInterval.lowerBound().value() / denominator));
+					newUpperBound = new IntBound((int) Math.floor((double)oldInterval.upperBound().value() / denominator));
+				}
+				
+				boolean isLowerBoundNonStrict = oldInterval.IsLowerBoundNonStrict();
+				boolean isUpperBoundNonStrict = oldInterval.IsUpperBoundNonStrict();
+				
+				// if the interval becomes too small we make it a bit bigger to secure, that we do not have to delete the arc
+				if ( (newUpperBound.value() == newLowerBound.value()) && !(oldInterval.IsLowerBoundNonStrict() && oldInterval.IsUpperBoundNonStrict()))
+				{
+					isUpperBoundNonStrict = true;
+					isLowerBoundNonStrict = true;
+				}
+
+				return new TimeInterval(
+					 isLowerBoundNonStrict,
+					 newLowerBound,
+					 newUpperBound,
+					 isUpperBoundNonStrict
+					 );
+	}
+
+}

=== modified file 'src/dk/aau/cs/gui/BatchProcessingDialog.java'
--- src/dk/aau/cs/gui/BatchProcessingDialog.java	2014-02-26 20:07:09 +0000
+++ src/dk/aau/cs/gui/BatchProcessingDialog.java	2014-05-28 18:52:41 +0000
@@ -76,6 +76,7 @@
 import dk.aau.cs.util.StringComparator;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingListener;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions;
+import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.ApproximationMethodOption;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.QueryPropertyOption;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.SymmetryOption;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationResult;
@@ -99,7 +100,7 @@
 	private static final String name_BROADCAST = "UPPAAL: Broadcast Reduction";
 	private static final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction";
 	private static final String name_UNTIMED = "TAPAAL Untimed Engine (verifypn)";
-	private static final String name_UNTIMED_APPROX = "TAPAAL Untimed Engine Over-Approximation Only";
+	private static final String name_UNTIMED_APPROX = "TAPAAL Untimed Engine w. State-Equations Check Only";
 	private static final String name_UNTIMED_REDUCE = "TAPAAL Untimed Engine w. Net Reductions";
 	private static final String name_verifyTAPNWithLegend = "A: "
 			+ name_verifyTAPN;
@@ -137,6 +138,9 @@
 	private static final String name_SEARCHWHOLESTATESPACE = "Search whole state space";
 	private static final String name_SYMMETRY = "Yes";
 	private static final String name_NOSYMMETRY = "No";
+	private static final String name_NONE_APPROXIMATION = "None";
+	private static final String name_OVER_APPROXIMATION = "Over-approximation";
+	private static final String name_UNDER_APPROXIMATION = "Under-approximation";
 
 	//Tool tip strings
 	//Tool tips for model panel
@@ -162,6 +166,14 @@
 	private final static String TOOL_TIP_OOMLabel = null;
 	private final static String TOOL_TIP_OOMValue = "<html>Enter the maximum amount of available memory to the verification.<br>Verification is skipped as soon as it is detected that this amount of memory is exceeded.</html>";
 	private final static String TOOL_TIP_NoOOMCheckBox = "Choose whether to use memory restrictions";
+	private final static String TOOL_TIP_Approximation_method = null;
+	private final static String TOOL_TIP_Approximation_Method_Option_Keep = "Do not override the default approximation method.";
+	private final static String TOOL_TIP_Approximation_Method_Option_None = "No approximation method is used.";
+	private final static String TOOL_TIP_Approximation_Method_Option_Over = "Approximate by dividing all intervals with the approximation constant and enlarging the intervals.";
+	private final static String TOOL_TIP_Approximation_Method_Option_Under = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";
+	private final static String TOOL_TIP_ApproximationDenominatorLabel = null;
+	private final static String TOOL_TIP_ApproximationDenominator = "Choose the approximation constant.";
+	private final static String TOOL_TIP_ApproximationDenominatorCheckbox = "Check to override the default approximation constant.";
 	
 	//Tool tips for monitor panel
 	private final static String TOOL_TIP_FileLabel = "Currently verified net";
@@ -214,6 +226,10 @@
 	private JCheckBox noOOMCheckbox;
 	private CustomJSpinner timeoutValue;
 	private CustomJSpinner oomValue;
+	private JComboBox approximationMethodOption;
+	private CustomJSpinner approximationDenominator;
+	private JCheckBox approximationDenominatorCheckbox;
+	
 	private Timer timeoutTimer = new Timer(30000, new ActionListener() {
 		public void actionPerformed(ActionEvent e) {
 			timeoutCurrentVerificationTask();
@@ -384,7 +400,6 @@
 		addFilesButton = new JButton("Add models");
 		addFilesButton.setToolTipText(TOOL_TIP_AddFilesButton);
 		addFilesButton.addActionListener(new ActionListener() {
-
 			public void actionPerformed(ActionEvent arg0) {
 				addFiles();
 			}
@@ -489,6 +504,7 @@
 		initCapacityComponents();
 		initTimeoutComponents();
 		initOOMComponents();
+		initApproximationMethodOptionsComponents();
 		
 		GridBagConstraints gbc = new GridBagConstraints();
 		gbc.gridx = 1;
@@ -526,6 +542,92 @@
 		gbc.insets = new Insets(0, 0, 5, 0);
 		verificationOptionsPanel.add(queryPropertyOption, gbc);
 	}
+	
+	private void initApproximationMethodOptionsComponents() {
+		JLabel approximationLabel = new JLabel("Approximation method:");
+		approximationLabel.setToolTipText(TOOL_TIP_Approximation_method);
+		GridBagConstraints gbc = new GridBagConstraints();
+		gbc.fill = GridBagConstraints.VERTICAL;
+		gbc.gridx = 0;
+		gbc.gridy = 8;
+		gbc.insets = new Insets(0, 0, 5, 0);
+		gbc.anchor = GridBagConstraints.WEST;
+		verificationOptionsPanel.add(approximationLabel, gbc);
+
+		String[] options = new String[] { 
+				name_KeepQueryOption,
+				name_NONE_APPROXIMATION,
+				name_OVER_APPROXIMATION,
+				name_UNDER_APPROXIMATION
+				};
+		approximationMethodOption = new JComboBox(options);
+		approximationMethodOption.setToolTipText(TOOL_TIP_Approximation_Method_Option_Keep);
+		approximationMethodOption.addActionListener(new ActionListener() {
+			@Override
+			public void actionPerformed(ActionEvent arg0) {
+				if (approximationMethodOption.getSelectedItem() == name_NONE_APPROXIMATION) {
+					approximationMethodOption.setToolTipText(TOOL_TIP_Approximation_Method_Option_None);
+				} else if (approximationMethodOption.getSelectedItem() == name_OVER_APPROXIMATION) {
+					approximationMethodOption.setToolTipText(TOOL_TIP_Approximation_Method_Option_Over);
+				} else if (approximationMethodOption.getSelectedItem() == name_UNDER_APPROXIMATION) {
+					approximationMethodOption.setToolTipText(TOOL_TIP_Approximation_Method_Option_Under);
+				} else {
+					approximationMethodOption.setToolTipText(TOOL_TIP_Approximation_Method_Option_Keep);
+				}
+			}
+		});
+		
+		gbc = new GridBagConstraints();
+		gbc.fill = GridBagConstraints.HORIZONTAL;
+		gbc.gridx = 1;
+		gbc.gridy = 8;
+		gbc.anchor = GridBagConstraints.WEST;
+		gbc.gridwidth = 2;
+		gbc.insets = new Insets(0, 0, 5, 0);
+		verificationOptionsPanel.add(approximationMethodOption, gbc);
+		
+		JLabel approximationDenominatorLabel = new JLabel("Approximation constant: ");
+		approximationDenominatorLabel.setToolTipText(TOOL_TIP_ApproximationDenominatorLabel);
+		gbc = new GridBagConstraints();
+		gbc.gridx = 0;
+		gbc.gridy = 9;
+		gbc.anchor = GridBagConstraints.WEST;
+		gbc.insets = new Insets(0, 0, 5, 0);
+		verificationOptionsPanel.add(approximationDenominatorLabel, gbc);
+
+		approximationDenominator = new CustomJSpinner(2, 1,Integer.MAX_VALUE);
+		approximationDenominator.setToolTipText(TOOL_TIP_ApproximationDenominator);
+		approximationDenominator.setMaximumSize(new Dimension(70, 30));
+		approximationDenominator.setMinimumSize(new Dimension(70, 30));
+		approximationDenominator.setPreferredSize(new Dimension(70, 30));
+		approximationDenominator.setEnabled(false);
+
+		gbc = new GridBagConstraints();
+		gbc.gridx = 1;
+		gbc.gridy = 9;
+		gbc.anchor = GridBagConstraints.WEST;
+		gbc.insets = new Insets(0, 0, 5, 10);
+		verificationOptionsPanel.add(approximationDenominator, gbc);
+		
+		approximationDenominatorCheckbox = new JCheckBox("Do not override");
+		approximationDenominatorCheckbox.setToolTipText(TOOL_TIP_ApproximationDenominatorCheckbox);
+		approximationDenominatorCheckbox.setSelected(true);
+		approximationDenominatorCheckbox.addActionListener(new ActionListener() {
+			public void actionPerformed(ActionEvent e) {
+				if (approximationDenominatorCheckbox.isSelected())
+					approximationDenominator.setEnabled(false);
+				else
+					approximationDenominator.setEnabled(true);
+			}
+		});
+
+		gbc = new GridBagConstraints();
+		gbc.gridx = 2;
+		gbc.gridy = 9;
+		gbc.anchor = GridBagConstraints.WEST;
+		gbc.insets = new Insets(0, 0, 5, 0);
+		verificationOptionsPanel.add(approximationDenominatorCheckbox, gbc);
+	}
 
 	private void initCapacityComponents() {
 		JLabel capacityLabel = new JLabel("Extra tokens:");
@@ -734,6 +836,7 @@
 			c.setEnabled(true);
 
 		numberOfExtraTokensInNet.setEnabled(!keepQueryCapacity.isSelected());
+		approximationDenominator.setEnabled(!approximationDenominatorCheckbox.isSelected());
 		timeoutValue.setEnabled(useTimeout());
 	}
 	
@@ -744,7 +847,7 @@
 				keepQueryCapacity.isSelected(), getNumberOfExtraTokens(),
 				getSearchOption(), getSymmetryOption(), reductionOption,
 				reductionOptionChooser.isDiscreteInclusion(), reductionOptionChooser.useTimeDartsPTrie(), reductionOptionChooser.useTimeDarts(), 
-				reductionOptionChooser.usePTrie(), reductionOptionChooser.getChoosenOptions());
+				reductionOptionChooser.usePTrie(), getApproximationMethodOption(), getApproximationDenominator(), reductionOptionChooser.getChoosenOptions());
 	}
 
 	private int getNumberOfExtraTokens() {
@@ -762,13 +865,29 @@
 	}
 
 	private QueryPropertyOption getQueryPropertyOption() {
-		String propertyOptionString = (String) queryPropertyOption
-				.getSelectedItem();
+		String propertyOptionString = (String) queryPropertyOption.getSelectedItem();
 		if (propertyOptionString.equals(name_SEARCHWHOLESTATESPACE))
 			return QueryPropertyOption.SearchWholeStateSpace;
 		else
 			return QueryPropertyOption.KeepQueryOption;
 	}
+	
+	private ApproximationMethodOption getApproximationMethodOption() {
+		String ApproximationMethodOptionString = (String) approximationMethodOption.getSelectedItem();
+		if(ApproximationMethodOptionString.equals(name_OVER_APPROXIMATION)) {
+			return ApproximationMethodOption.OverApproximation;
+		} else if (ApproximationMethodOptionString.equals(name_UNDER_APPROXIMATION)) {
+			return ApproximationMethodOption.UnderApproximation;
+		} else if (ApproximationMethodOptionString.equals(name_NONE_APPROXIMATION)) {
+			return ApproximationMethodOption.None;
+		} else {
+			return ApproximationMethodOption.KeepQueryOption;
+		}
+	}
+	
+	private int getApproximationDenominator() {
+		return (approximationDenominatorCheckbox.isSelected()) ? 0 : (Integer) approximationDenominator.getValue();
+	}
 
 	private void initSearchOptionsComponents() {
 		JLabel searchLabel = new JLabel("Search order:");
@@ -1106,8 +1225,7 @@
 
 	private void process() {
 		tableModel.clear();
-		currentWorker = new BatchProcessingWorker(files, tableModel,
-				getVerificationOptions());
+		currentWorker = new BatchProcessingWorker(files, tableModel, getVerificationOptions());
 		currentWorker.addPropertyChangeListener(new PropertyChangeListener() {
 
 			public void propertyChange(PropertyChangeEvent evt) {
@@ -1329,8 +1447,10 @@
 								"Not Satisfied"))
 								|| (isQueryColumn && value.toString().equals(
 										"FALSE")))
-							setBackground(new Color(255, 91, 91)); // light
-																	// green
+							setBackground(new Color(255, 91, 91)); // light  green
+						else if (isResultColumn && value.toString().equals(
+								"Inconclusive"))
+							setBackground(new Color(255, 255, 120)); // light yellow
 						else
 							setBackground(table.getBackground());
 					} else {
@@ -1445,6 +1565,19 @@
 				s.append(name_SEARCHWHOLESTATESPACE);
 			else
 				s.append(query.getProperty().toString());
+			
+			s.append("\n\n");
+			s.append("Approximation method: ");
+			if (query.isOverApproximationEnabled()) {
+				s.append(name_OVER_APPROXIMATION);
+			} else if (query.isUnderApproximationEnabled()) {
+				s.append(name_UNDER_APPROXIMATION);
+			} else {
+				s.append(name_NONE_APPROXIMATION);
+			}
+			s.append("\n");
+			s.append("Approximation Constant: ");
+			s.append(query.approximationDenominator());
 
 			return s.toString();
 		}

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2014-02-25 12:56:09 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2014-05-28 18:52:41 +0000
@@ -239,6 +239,10 @@
 	public DataLayer getModel() {
 		return drawingSurface.getGuiModel();
 	}
+	
+	public HashMap<TimedArcPetriNet, DataLayer> getGuiModels() {
+		return this.guiModels;
+	}
 
 	public void setDrawingSurface(DrawingSurfaceImpl drawingSurface) {
 		this.drawingSurface = drawingSurface;

=== modified file 'src/dk/aau/cs/io/TapnXmlLoader.java'
--- src/dk/aau/cs/io/TapnXmlLoader.java	2014-02-22 23:21:12 +0000
+++ src/dk/aau/cs/io/TapnXmlLoader.java	2014-05-28 18:52:41 +0000
@@ -792,6 +792,9 @@
 		boolean timeDarts = getReductionOption(queryElement, "timeDarts", true);
 		boolean pTrie = getReductionOption(queryElement, "pTrie", true);
 		boolean overApproximation = getReductionOption(queryElement, "overApproximation", true);
+		boolean isOverApproximationEnabled = getApproximationOption(queryElement, "enableOverApproximation", false);
+		boolean isUnderApproximationEnabled = getApproximationOption(queryElement, "enableUnderApproximation", false);
+		int approximationDenominator = getApproximationValue(queryElement, "approximationDenominator", 2);
 		boolean discreteInclusion = getDiscreteInclusionOption(queryElement);
 		boolean active = getActiveStatus(queryElement);
 		InclusionPlaces inclusionPlaces = getInclusionPlaces(queryElement, network);
@@ -801,8 +804,7 @@
 		query = parseQueryProperty(queryElement.getAttribute("query"));
 
 		if (query != null) {
-			TAPNQuery parsedQuery = new TAPNQuery(comment, capacity, query, traceOption,
-					searchOption, reductionOption, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, hashTableSize, extrapolationOption, inclusionPlaces);
+			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);
 			return parsedQuery;
@@ -864,6 +866,34 @@
 		return result;	
 	}
 	
+	private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
+	{
+		if(!queryElement.hasAttribute(attributeName)){
+			return defaultValue;
+		}
+		int result;
+		try {
+			result = Integer.parseInt(queryElement.getAttribute(attributeName));
+		} catch(Exception e) {
+			result = defaultValue;
+		}
+		return result;
+	}
+	
+	private boolean getApproximationOption(Element queryElement, String attributeName, boolean defaultValue)
+	{
+		if(!queryElement.hasAttribute(attributeName)){
+			return defaultValue;
+		}
+		boolean result;
+		try {
+			result = queryElement.getAttribute(attributeName).equals("true");
+		} catch(Exception e) {
+			result = defaultValue;
+		}
+		return result;	
+	}
+	
 	private boolean getDiscreteInclusionOption(Element queryElement) {
 		boolean discreteInclusion;
 		try {

=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2014-02-22 23:21:12 +0000
+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java	2014-05-28 18:52:41 +0000
@@ -268,6 +268,9 @@
 		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());
 		
 		return queryElement;
 	}

=== modified file 'src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java'
--- src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java	2014-02-22 23:21:12 +0000
+++ src/dk/aau/cs/io/batchProcessing/BatchProcessingLoader.java	2014-05-28 18:52:41 +0000
@@ -494,18 +494,21 @@
 		boolean timeDarts = getReductionOption(queryElement, "timeDarts", true);
 		boolean pTrie = getReductionOption(queryElement, "pTrie", true);
 		boolean overApproximation = getReductionOption(queryElement, "overApproximation", false);
+		boolean isOverApproximationEnabled = getApproximationOption(queryElement, "enableOverApproximation", false);
+		boolean isUnderApproximationEnabled = getApproximationOption(queryElement, "enableUnderApproximation", false);
+		int approximationDenominator = getApproximationValue(queryElement, "approximationDenominator", 2);
 		boolean active = getActiveStatus(queryElement);
 		boolean discreteInclusion = getDiscreteInclusionOption(queryElement);
 		boolean reduction = getReductionOption(queryElement, "reduction", true);
 		InclusionPlaces inclusionPlaces = getInclusionPlaces(queryElement, network);
 		
-		
 		TCTLAbstractProperty query;
 		query = parseQueryProperty(queryElement.getAttribute("query"));
 
 		if (query != null) {
 			TAPNQuery parsedQuery = new TAPNQuery(comment, capacity, query, traceOption,
-					searchOption, reductionOption, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, hashTableSize, extrapolationOption, inclusionPlaces);
+					searchOption, reductionOption, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, hashTableSize, 
+					extrapolationOption, inclusionPlaces, isOverApproximationEnabled, isUnderApproximationEnabled, approximationDenominator);
 			parsedQuery.setActive(active);
 			parsedQuery.setDiscreteInclusion(discreteInclusion);
 			return parsedQuery;
@@ -513,6 +516,34 @@
 			return null;
 	}
 	
+	private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
+	{
+		if(!queryElement.hasAttribute(attributeName)){
+			return defaultValue;
+		}
+		int result;
+		try {
+			result = Integer.parseInt(queryElement.getAttribute(attributeName));
+		} catch(Exception e) {
+			result = defaultValue;
+		}
+		return result;
+	}
+	
+	private boolean getApproximationOption(Element queryElement, String attributeName, boolean defaultValue)
+	{
+		if(!queryElement.hasAttribute(attributeName)){
+			return defaultValue;
+		}
+		boolean result;
+		try {
+			result = queryElement.getAttribute(attributeName).equals("true");
+		} catch(Exception e) {
+			result = defaultValue;
+		}
+		return result;	
+	}
+	
 	private boolean getDiscreteInclusionOption(Element queryElement) {
 		boolean discreteInclusion;
 		try {

=== modified file 'src/dk/aau/cs/io/batchProcessing/BatchProcessingResultsExporter.java'
--- src/dk/aau/cs/io/batchProcessing/BatchProcessingResultsExporter.java	2014-02-26 20:07:09 +0000
+++ src/dk/aau/cs/io/batchProcessing/BatchProcessingResultsExporter.java	2014-05-28 18:52:41 +0000
@@ -21,12 +21,15 @@
 	private static final String name_BROADCAST = "J: UPPAAL: Broadcast Reduction";
 	private static final String name_BROADCASTDEG2 = "K: UPPAAL: Broadcast Degree 2 Reduction";
 	private static final String name_UNTIMED = "L: TAPAAL Untimed Engine";
-	private static final String name_UNTIMEDAPPROX = "M: TAPAAL Untimed Engine, Over-Approximation Only";	
+	private static final String name_UNTIMEDAPPROX = "M: TAPAAL Untimed Engine, State-Equations Check Only";	
 	private static final String name_UNTIMEDREDUCE = "N: TAPAAL Untimed engine w. Net Reductions";
 	private static final String name_BFS = "Breadth First Search";
 	private static final String name_DFS = "Depth First Search";
 	private static final String name_RandomDFS = "Random Depth First Search";
-	private static final String DELIMITER = ";";
+	private static final String name_NONE_APPROXIMATION = "None";
+	private static final String name_OVER_APPROXIMATION = "Over-approximation";
+	private static final String name_UNDER_APPROXIMATION = "Under-approximation";
+	private static final String DELIMITER = ";";	
 	
 	public void exportToCSV(Iterable<BatchProcessingVerificationResult> results, File outputFile) throws Exception {
 		PrintStream writer = new PrintStream(outputFile);
@@ -43,7 +46,9 @@
 				       "Extra Tokens" + DELIMITER + 
 				       "Verification Method" + DELIMITER + 
 				       "Symmetry" + DELIMITER + 
-				       "Search Order");
+				       "Search Order" + DELIMITER + 
+				       "Approximation Method" + DELIMITER +
+				       "Approximation Constant");
 		
 		for(BatchProcessingVerificationResult result : results) {
 			TAPNQuery query = result.query();
@@ -77,6 +82,10 @@
 			s.append((query != null) ? (query.useSymmetry() ? "Yes" : "No") : "");
 			s.append(DELIMITER);
 			s.append((query != null) ? getVerificationMethod(query) : "");
+			s.append(DELIMITER);
+			s.append((query != null) ? getApproximationMethod(query) : "");
+			s.append(DELIMITER);
+			s.append((query != null) ? query.approximationDenominator() : "");
 			
 			writer.println(s.toString());
 		}
@@ -93,6 +102,15 @@
 			return name_BFS;
 		
 	}
+	
+	private String getApproximationMethod(TAPNQuery query) {
+		if (query.isOverApproximationEnabled()) {
+			return name_OVER_APPROXIMATION;
+		} else if (query.isUnderApproximationEnabled()) {
+			return name_UNDER_APPROXIMATION;
+		}
+		return name_NONE_APPROXIMATION;
+	}
 
 	private Object getSearchOrder(TAPNQuery query) {
 		ReductionOption reduction = query.getReductionOption();

=== modified file 'src/dk/aau/cs/model/tapn/TAPNQuery.java'
--- src/dk/aau/cs/model/tapn/TAPNQuery.java	2013-09-28 12:16:32 +0000
+++ src/dk/aau/cs/model/tapn/TAPNQuery.java	2014-05-28 18:52:41 +0000
@@ -39,4 +39,8 @@
 	public String toString() {
 		return property.toString();
 	}
+	
+	public void setProperty(TCTLAbstractProperty newProperty){
+		this.property = newProperty;
+	}
 }

=== modified file 'src/dk/aau/cs/model/tapn/TimeInterval.java'
--- src/dk/aau/cs/model/tapn/TimeInterval.java	2013-04-11 18:06:16 +0000
+++ src/dk/aau/cs/model/tapn/TimeInterval.java	2014-05-28 18:52:41 +0000
@@ -95,10 +95,18 @@
 	public Bound lowerBound() {
 		return lower;
 	}
+	
+	public void setLowerBound(Bound lower) {
+		this.lower = lower;
+	}
 
 	public Bound upperBound() {
 		return upper;
 	}
+	
+	public void setUpperBound(Bound upper) {
+		this.upper = upper;
+	}
 
 	public boolean IsLowerBoundNonStrict() {
 		return isLowerIncluded;

=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java'
--- src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java	2013-11-14 21:32:09 +0000
+++ src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java	2014-05-28 18:52:41 +0000
@@ -15,6 +15,7 @@
 import dk.aau.cs.util.Require;
 import dk.aau.cs.util.StringComparator;
 import dk.aau.cs.util.Tuple;
+import dk.aau.cs.verification.ITAPNComposer;
 import dk.aau.cs.verification.NameMapping;
 import dk.aau.cs.verification.TAPNComposer;
 
@@ -467,7 +468,7 @@
 	}
 	
 	public boolean isDegree2(){
-		TAPNComposer composer = new TAPNComposer(new MessengerImpl());
+		ITAPNComposer composer = new TAPNComposer(new MessengerImpl());
 		Tuple<TimedArcPetriNet,NameMapping> composedModel = composer.transformModel(this);
 
 		return composedModel.value1().isDegree2();

=== modified file 'src/dk/aau/cs/model/tapn/TimedToken.java'
--- src/dk/aau/cs/model/tapn/TimedToken.java	2014-02-05 15:13:50 +0000
+++ src/dk/aau/cs/model/tapn/TimedToken.java	2014-05-28 18:52:41 +0000
@@ -26,6 +26,10 @@
 		return age;
 	}
 	
+	public void setAge(BigDecimal age) {
+		this.age = age;		
+	}
+	
 	public TimedToken clone() {
 		return new TimedToken(place, age); // age is immutable so ok to pass it
 											// to constructor

=== modified file 'src/dk/aau/cs/model/tapn/TransportArc.java'
--- src/dk/aau/cs/model/tapn/TransportArc.java	2013-04-22 07:35:47 +0000
+++ src/dk/aau/cs/model/tapn/TransportArc.java	2014-05-28 18:52:41 +0000
@@ -90,7 +90,8 @@
 
 	@Override
 	public void delete() {
-		model().remove(this);
+		if (model() != null)
+			model().remove(this);
 	}
 
 	public TransportArc copy(TimedArcPetriNet tapn) {

=== modified file 'src/dk/aau/cs/model/tapn/simulation/TAPNNetworkTimeDelayStep.java'
--- src/dk/aau/cs/model/tapn/simulation/TAPNNetworkTimeDelayStep.java	2013-09-23 15:42:38 +0000
+++ src/dk/aau/cs/model/tapn/simulation/TAPNNetworkTimeDelayStep.java	2014-05-28 18:52:41 +0000
@@ -21,6 +21,10 @@
 	public BigDecimal getDelay(){
 		return delay;
 	}
+	
+	public void setDelay(BigDecimal delay){
+		this.delay = delay;
+	}
 
 	@Override
 	public String toString() {

=== modified file 'src/dk/aau/cs/model/tapn/simulation/TimeDelayStep.java'
--- src/dk/aau/cs/model/tapn/simulation/TimeDelayStep.java	2012-06-27 15:30:31 +0000
+++ src/dk/aau/cs/model/tapn/simulation/TimeDelayStep.java	2014-05-28 18:52:41 +0000
@@ -21,6 +21,10 @@
 	public BigDecimal delay() {
 		return delay;
 	}
+	
+	public void setDelay(BigDecimal delay) {
+		this.delay = delay;
+	}
 
 	@Override
 	public String toString() {

=== modified file 'src/dk/aau/cs/model/tapn/simulation/TimedArcPetriNetTrace.java'
--- src/dk/aau/cs/model/tapn/simulation/TimedArcPetriNetTrace.java	2012-07-05 13:51:28 +0000
+++ src/dk/aau/cs/model/tapn/simulation/TimedArcPetriNetTrace.java	2014-05-28 18:52:41 +0000
@@ -4,6 +4,8 @@
 import java.util.Iterator;
 import java.util.List;
 
+import dk.aau.cs.model.tapn.TimedOutputArc;
+import dk.aau.cs.model.tapn.TimedToken;
 import dk.aau.cs.verification.VerifyTAPN.TraceType;
 
 public class TimedArcPetriNetTrace implements Iterable<TimedArcPetriNetStep> {
@@ -60,4 +62,37 @@
 	public void setTraceType(TraceType traceType){
 		this.traceType = traceType;
 	}
+	
+	public void reduceTraceForOriginalNet(String matchForTransition, String matchTokenRemoval) {
+		for (TimedArcPetriNetStep step : steps){
+			if (step instanceof TimedTransitionStep) {
+				if (((TimedTransitionStep) step).transition().name().contains(matchForTransition)) {
+					((TimedTransitionStep) step).transition().setName(((TimedTransitionStep) step).transition().name().substring(0, ((TimedTransitionStep) step).transition().name().indexOf(matchForTransition)));
+				}
+				if(((TimedTransitionStep) step).consumedTokens() != null){
+					for (TimedToken token : ((TimedTransitionStep) step).consumedTokens()){
+						if(token.place().name().contains(matchTokenRemoval)){
+							((TimedTransitionStep) step).consumedTokens().remove(token);
+							break;
+						}
+					}
+				}
+			}
+		}
+	}
+	
+	public void removeTokens(String matchTokenRemoval){
+		for (TimedArcPetriNetStep step : steps){
+			if (step instanceof TimedTransitionStep){
+				if(((TimedTransitionStep) step).consumedTokens() != null){
+					for (TimedToken token : ((TimedTransitionStep) step).consumedTokens()){
+						if(token.place().name().contains(matchTokenRemoval)){
+							((TimedTransitionStep) step).consumedTokens().remove(token);
+							break;
+						}
+					}
+				}
+			}
+		}
+	}
 }

=== modified file 'src/dk/aau/cs/util/MemoryMonitor.java'
--- src/dk/aau/cs/util/MemoryMonitor.java	2013-11-12 13:08:42 +0000
+++ src/dk/aau/cs/util/MemoryMonitor.java	2014-05-28 18:52:41 +0000
@@ -31,6 +31,7 @@
 	private static int PID = -1;
 	private static Semaphore busy = new Semaphore(1);
 	private static double peakMemory = -1;
+	private static Boolean cumulativePeakMemory = false;
 	private static DecimalFormat formatter = null;
 	
 	private static DecimalFormat getFormatter(){
@@ -44,7 +45,12 @@
 
 	public static void attach(Process p){
 		PID = getPid(p);
-		peakMemory = -1;
+		
+		if( ! cumulativePeakMemory) {
+			peakMemory = -1;
+		}
+		
+		cumulativePeakMemory = false;
 	}
 	
 	public static void detach(){
@@ -55,6 +61,10 @@
 	public static boolean isAttached(){
 		return PID != -1;
 	}
+	
+	public static void cumulateMemory() {
+		cumulativePeakMemory = true;
+	}
 
 	public static String getUsage(){
 		if(busy.tryAcquire()){
@@ -91,7 +101,6 @@
 			}
 
 			busy.release();
-
 			if(memory < 0){
 				return null;
 			}else{

=== added file 'src/dk/aau/cs/verification/ITAPNComposer.java'
--- src/dk/aau/cs/verification/ITAPNComposer.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/verification/ITAPNComposer.java	2014-05-28 18:52:41 +0000
@@ -0,0 +1,12 @@
+package dk.aau.cs.verification;
+
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
+import dk.aau.cs.util.Tuple;
+
+public interface ITAPNComposer {
+
+	public abstract Tuple<TimedArcPetriNet, NameMapping> transformModel(
+			TimedArcPetriNetNetwork model);
+
+}
\ No newline at end of file

=== modified file 'src/dk/aau/cs/verification/NameMapping.java'
--- src/dk/aau/cs/verification/NameMapping.java	2012-05-02 13:40:18 +0000
+++ src/dk/aau/cs/verification/NameMapping.java	2014-05-28 18:52:41 +0000
@@ -35,7 +35,7 @@
 		return originalToMappedNames.get(new Tuple<String, String>(templateName, objectName));
 	}
 	
-	public HashMap<String, Tuple<String, String>> getMappedToOrg(){
-		return mappedNamesToOriginalNames;
+	public HashMap<Tuple<String, String>, String> getOrgToMapped(){
+		return originalToMappedNames;
 	}
 }

=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
--- src/dk/aau/cs/verification/QueryResult.java	2013-10-02 19:52:23 +0000
+++ src/dk/aau/cs/verification/QueryResult.java	2014-05-28 18:52:41 +0000
@@ -5,6 +5,7 @@
 
 public class QueryResult {
 	private boolean satisfied = false;
+	private boolean approximationInconclusive = false;
 	private boolean discreteInclusion = false;
 	private TAPNQuery query;
 	private BoundednessAnalysisResult boundednessAnalysis;
@@ -20,6 +21,14 @@
 		return satisfied;
 	}
 	
+	public boolean isApproximationInconclusive() {
+		return approximationInconclusive;
+	}
+	
+	public void setApproximationInconclusive(boolean result) {
+		approximationInconclusive = result;
+	}
+	
 	public boolean isDiscreteIncludion() {
 		return discreteInclusion;
 	}
@@ -30,8 +39,13 @@
 	
 	@Override
 	public String toString() {
-		StringBuffer buffer = new StringBuffer( "Property is ");
-		buffer.append(satisfied ? "satisfied." : "not satisfied.");
+		StringBuffer buffer = new StringBuffer();
+		if(approximationInconclusive)
+			buffer.append(getInconclusiveString());
+		else {
+			buffer.append("Property is ");
+			buffer.append(satisfied ? "satisfied." : "not satisfied.");
+		}
 		if(shouldAddExplanation())
 			buffer.append(getExplanationString());
 		return buffer.toString();
@@ -54,8 +68,22 @@
 	protected String getExplanationString(){
 		return boundednessAnalysis.toString();
 	}
+	
+	protected String getInconclusiveString(){
+		StringBuffer buffer = new StringBuffer();
+		buffer.append("The result of the approximation was inconclusive.");
+		return buffer.toString();
+	}
+	
+	public TAPNQuery getQuery() {
+		return query;
+	}
 
 	public BoundednessAnalysisResult boundednessAnalysis() {
 		return boundednessAnalysis;
 	}
+	
+	public void flipResult() {
+		this.satisfied = !this.satisfied;
+	}
 }

=== modified file 'src/dk/aau/cs/verification/TAPNComposer.java'
--- src/dk/aau/cs/verification/TAPNComposer.java	2013-11-25 12:16:37 +0000
+++ src/dk/aau/cs/verification/TAPNComposer.java	2014-05-28 18:52:41 +0000
@@ -16,7 +16,7 @@
 import dk.aau.cs.model.tapn.TransportArc;
 import dk.aau.cs.util.Tuple;
 
-public class TAPNComposer {
+public class TAPNComposer implements ITAPNComposer {
 	private static final String PLACE_FORMAT = "P%1$d";
 	private static final String TRANSITION_FORMAT = "T%1$d";
 
@@ -32,6 +32,7 @@
 		this.messenger = messenger;
 	}
 	
+	@Override
 	public Tuple<TimedArcPetriNet, NameMapping> transformModel(TimedArcPetriNetNetwork model) {
 		nextPlaceIndex = -1;
 		nextTransitionIndex = -1;
@@ -48,8 +49,6 @@
 		createTransportArcs(model, tapn, mapping);
 		createInhibitorArcs(model, tapn, mapping);
 
-		//dumpToConsole(tapn, mapping);
-
 		return new Tuple<TimedArcPetriNet, NameMapping>(tapn, mapping);
 	}
 	

=== added file 'src/dk/aau/cs/verification/TAPNComposerWithGUI.java'
--- src/dk/aau/cs/verification/TAPNComposerWithGUI.java	1970-01-01 00:00:00 +0000
+++ src/dk/aau/cs/verification/TAPNComposerWithGUI.java	2014-05-28 18:52:41 +0000
@@ -0,0 +1,599 @@
+package dk.aau.cs.verification;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map.Entry;
+
+import pipe.dataLayer.DataLayer;
+import pipe.gui.graphicElements.Arc;
+import pipe.gui.graphicElements.ArcPath;
+import pipe.gui.graphicElements.ArcPathPoint;
+import pipe.gui.graphicElements.Place;
+import pipe.gui.graphicElements.PlaceTransitionObject;
+import pipe.gui.graphicElements.Transition;
+import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
+import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
+import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
+import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
+import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
+import pipe.gui.graphicElements.tapn.TimedTransportArcComponent;
+import dk.aau.cs.Messenger;
+import dk.aau.cs.model.tapn.Bound;
+import dk.aau.cs.model.tapn.IntBound;
+import dk.aau.cs.model.tapn.LocalTimedPlace;
+import dk.aau.cs.model.tapn.SharedPlace;
+import dk.aau.cs.model.tapn.TimeInterval;
+import dk.aau.cs.model.tapn.TimeInvariant;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
+import dk.aau.cs.model.tapn.TimedInhibitorArc;
+import dk.aau.cs.model.tapn.TimedInputArc;
+import dk.aau.cs.model.tapn.TimedOutputArc;
+import dk.aau.cs.model.tapn.TimedPlace;
+import dk.aau.cs.model.tapn.TimedToken;
+import dk.aau.cs.model.tapn.TimedTransition;
+import dk.aau.cs.model.tapn.TransportArc;
+import dk.aau.cs.util.Tuple;
+
+public class TAPNComposerWithGUI implements ITAPNComposer {
+	private static final String PLACE_FORMAT = "P%1$d";
+	private static final String TRANSITION_FORMAT = "T%1$d";
+
+	private Messenger messenger;
+	private boolean hasShownMessage = false;
+	
+	private int nextPlaceIndex;
+	private int nextTransitionIndex;
+
+	private HashSet<String> processedSharedObjects;
+	private HashMap<TimedArcPetriNet, DataLayer> guiModels;
+	private DataLayer composedGuiModel;
+
+	public TAPNComposerWithGUI(Messenger messenger, HashMap<TimedArcPetriNet, DataLayer> guiModels){
+		this.messenger = messenger;
+		
+		HashMap<TimedArcPetriNet, DataLayer> newGuiModels = new HashMap<TimedArcPetriNet, DataLayer>();
+		for(Entry<TimedArcPetriNet, DataLayer> entry : guiModels.entrySet()) {
+			newGuiModels.put(entry.getKey(), entry.getValue().copy(entry.getKey()));
+		}
+		
+		this.guiModels = newGuiModels;
+	}
+	
+	public Tuple<TimedArcPetriNet, NameMapping> transformModel(TimedArcPetriNetNetwork model) {
+		nextPlaceIndex = -1;
+		nextTransitionIndex = -1;
+		processedSharedObjects = new HashSet<String>();
+		TimedArcPetriNet tapn = new TimedArcPetriNet("ComposedModel");
+		DataLayer guiModel = new DataLayer();
+		NameMapping mapping = new NameMapping();
+		hasShownMessage = false;
+
+		
+		double greatestWidth = 0,
+			   greatestHeight = 0;
+		for (TimedArcPetriNet tapn1 : model.activeTemplates()) {
+			greatestWidth = greatestWidth >= getRightmostObject(guiModels.get(tapn1)).getPositionX() ? greatestWidth : getRightmostObject(guiModels.get(tapn1)).getPositionX();
+			greatestHeight = greatestHeight >= getLowestObject(guiModels.get(tapn1)).getPositionY() ? greatestHeight : getLowestObject(guiModels.get(tapn1)).getPositionY();
+		}
+		
+		createSharedPlaces(model, tapn, mapping, guiModel);
+		createPlaces(model, tapn, mapping, guiModel, greatestWidth, greatestHeight);
+		createTransitions(model, tapn, mapping, guiModel, greatestWidth, greatestHeight);
+		createInputArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight);
+		createOutputArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight);
+		createTransportArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight);
+		createInhibitorArcs(model, tapn, mapping, guiModel, greatestWidth, greatestHeight);
+		
+		// Set composed guiModel in the instance variable
+		this.composedGuiModel = guiModel;
+
+		return new Tuple<TimedArcPetriNet, NameMapping>(tapn, mapping);
+	}
+	
+	public DataLayer getGuiModel() {
+		return this.composedGuiModel;
+	}
+	
+	private Tuple<Integer, Integer> calculateComponentPosition(int netNumber) {
+		Integer x = netNumber % 2;
+		Integer y = (int) Math.floor(netNumber / 2d);
+		
+		return new Tuple<Integer, Integer>(x, y);		
+	}
+	
+	private PlaceTransitionObject getRightmostObject(DataLayer guiModel) {
+		PlaceTransitionObject returnObject = null;
+		
+		for (PlaceTransitionObject currentObject : guiModel.getPlaces()) {
+			if (returnObject == null || returnObject.getPositionX() < currentObject.getPositionX()) {
+				returnObject = currentObject;
+			}
+		}
+		
+		for (PlaceTransitionObject currentObject : guiModel.getTransitions()) {
+			if (returnObject == null || returnObject.getPositionX() < currentObject.getPositionX()) {
+				returnObject = currentObject;
+			}
+		}
+		
+		return returnObject;
+	}
+
+	private PlaceTransitionObject getLowestObject(DataLayer guiModel) {
+		PlaceTransitionObject returnObject = null;
+		
+		for (PlaceTransitionObject currentObject : guiModel.getPlaces()) {
+			if (returnObject == null || returnObject.getPositionY() < currentObject.getPositionY()) {
+				returnObject = currentObject;
+			}
+		}
+		
+		for (PlaceTransitionObject currentObject : guiModel.getTransitions()) {
+			if (returnObject == null || returnObject.getPositionY() < currentObject.getPositionY()) {
+				returnObject = currentObject;
+			}
+		}
+		
+		return returnObject;
+	}
+	
+	private Place getSharedPlace(String name) {
+		for(Entry<TimedArcPetriNet, DataLayer> hashmapEntry : guiModels.entrySet()) {
+			Place findPlace = hashmapEntry.getValue().getPlaceByName(name);
+			if (findPlace != null)
+				return findPlace;
+		}
+		return null;
+	}
+	
+	private void createSharedPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel) {
+		for(SharedPlace place : model.sharedPlaces()){
+			String uniquePlaceName = (model.activeTemplates().size() > 1) ? "Shared_" + place.name() : place.name();
+			
+			LocalTimedPlace constructedPlace = null;
+			if (place.invariant().upperBound() instanceof Bound.InfBound) {					
+				constructedPlace = new LocalTimedPlace(uniquePlaceName, place.invariant());
+			} else {
+				constructedPlace = new LocalTimedPlace(uniquePlaceName, new TimeInvariant(place.invariant().isUpperNonstrict(), new IntBound(place.invariant().upperBound().value())));
+			}
+			constructedModel.add(constructedPlace);
+			mapping.addMappingForShared(place.name(), uniquePlaceName);
+
+			if(model.isSharedPlaceUsedInTemplates(place)){
+				for (TimedToken token : place.tokens()) {
+					constructedPlace.addToken(new TimedToken(constructedPlace, token.age()));
+				}
+			}
+			
+			Place oldPlace = getSharedPlace(place.name());
+			TimedPlaceComponent newPlace = new TimedPlaceComponent(
+					oldPlace.getPositionX(),
+					oldPlace.getPositionY(),
+					oldPlace.getId(),
+					uniquePlaceName,
+					oldPlace.getNameOffsetX(),
+					oldPlace.getNameOffsetY(),
+					0,
+					oldPlace.getMarkingOffsetXObject().doubleValue(),
+					oldPlace.getMarkingOffsetYObject().doubleValue(),
+					0
+					);
+			newPlace.setGuiModel(guiModel);
+			newPlace.setUnderlyingPlace(constructedPlace);
+			newPlace.setName(uniquePlaceName);
+			guiModel.addPlace(newPlace);
+		}
+	}
+
+	private void createPlaces(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) {
+		int i = 0;
+		for (TimedArcPetriNet tapn : model.activeTemplates()) {
+			Tuple<Integer, Integer> offset = this.calculateComponentPosition(i);
+			DataLayer currentGuiModel = this.guiModels.get(tapn);
+			
+			for (TimedPlace timedPlace : tapn.places()) {			
+				if(!timedPlace.isShared()){
+					String uniquePlaceName = (model.activeTemplates().size() > 1) ? ((LocalTimedPlace)timedPlace).model().name() + "_" + timedPlace.name() : timedPlace.name();
+
+					LocalTimedPlace place = null;
+					if (timedPlace.invariant().upperBound() instanceof Bound.InfBound) {					
+						place = new LocalTimedPlace(uniquePlaceName, timedPlace.invariant());
+					} else {
+						place = new LocalTimedPlace(uniquePlaceName, new TimeInvariant(timedPlace.invariant().isUpperNonstrict(), new IntBound(timedPlace.invariant().upperBound().value())));
+					}
+					constructedModel.add(place);
+					mapping.addMapping(tapn.name(), timedPlace.name(), uniquePlaceName);
+
+					for (TimedToken token : timedPlace.tokens()) {
+						place.addToken(new TimedToken(place, token.age()));
+					}
+					
+					Place oldPlace = currentGuiModel.getPlaceByName(timedPlace.name());
+					TimedPlaceComponent newPlace = new TimedPlaceComponent(
+							oldPlace.getPositionX() + offset.value1() * greatestWidth,
+							oldPlace.getPositionY() + offset.value2() * greatestHeight,
+							oldPlace.getId(),
+							uniquePlaceName,
+							oldPlace.getNameOffsetX(),
+							oldPlace.getNameOffsetY(),
+							0,
+							oldPlace.getMarkingOffsetXObject().doubleValue(),
+							oldPlace.getMarkingOffsetYObject().doubleValue(),
+							0
+							);
+					newPlace.setGuiModel(guiModel);
+					newPlace.setUnderlyingPlace(place);
+					newPlace.setName(uniquePlaceName);
+					guiModel.addPlace(newPlace);
+				}
+			}
+			i++;
+		}
+	}
+
+	private String getUniquePlaceName() {
+		nextPlaceIndex++;
+		return String.format(PLACE_FORMAT, nextPlaceIndex);
+	}
+
+	private void createTransitions(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) {
+		int i = 0;
+		for (TimedArcPetriNet tapn : model.activeTemplates()) {
+			Tuple<Integer, Integer> offset = this.calculateComponentPosition(i);
+			DataLayer currentGuiModel = this.guiModels.get(tapn);
+			
+			for (TimedTransition timedTransition : tapn.transitions()) {
+				if(!processedSharedObjects.contains(timedTransition.name())){
+					
+					// CAUTION: This if statement removes orphan transitions.
+					//   This changes answers for e.g. DEADLOCK queries if
+					//   support for such queries are added later.
+					// ONLY THE IF SENTENCE SHOULD BE REMOVED. REST OF CODE SHOULD BE LEFT INTACT
+					if(!timedTransition.isOrphan()){
+						String uniqueTransitionName = "";
+						if (model.activeTemplates().size() > 1) {
+							uniqueTransitionName = ( ! timedTransition.isShared()) ? timedTransition.model().name() + "_" + timedTransition.name() : "Shared_" + timedTransition.name();
+						} else {
+							uniqueTransitionName = timedTransition.name();
+						}
+						
+						TimedTransition transition = new TimedTransition(uniqueTransitionName, timedTransition.isUrgent());
+						constructedModel.add(transition);
+						Transition oldTransition = currentGuiModel.getTransitionByName(timedTransition.name());
+						TimedTransitionComponent newTransition = new TimedTransitionComponent(
+								oldTransition.getPositionX() + offset.value1() * greatestWidth,
+								oldTransition.getPositionY() + offset.value2() * greatestHeight,
+								oldTransition.getId(),
+								uniqueTransitionName,
+								oldTransition.getNameOffsetX(),
+								oldTransition.getNameOffsetY(),
+								true,
+								false,
+								oldTransition.getAngle(),
+								0);
+						newTransition.setGuiModel(guiModel);
+						newTransition.setUnderlyingTransition(transition);
+						newTransition.setName(uniqueTransitionName);
+						guiModel.addTransition(newTransition);
+						
+						if(timedTransition.isShared()){
+							String name = timedTransition.sharedTransition().name();
+							processedSharedObjects.add(name);
+							mapping.addMappingForShared(name, uniqueTransitionName);
+						}else{
+							mapping.addMapping(tapn.name(), timedTransition.name(), uniqueTransitionName);
+						}
+					}else{
+						if(!hasShownMessage){
+							messenger.displayInfoMessage("There are orphan transitions (no incoming and no outgoing arcs) in the model."
+									+ System.getProperty("line.separator") + "They will be removed before the verification.");
+							hasShownMessage = true;
+						}
+					}
+				}
+			}
+			i++;
+		}
+	}
+
+	private String getUniqueTransitionName() {
+		nextTransitionIndex++;
+		return String.format(TRANSITION_FORMAT, nextTransitionIndex);
+	}
+	
+	private ArcPath createArcPath(DataLayer currentGuiModel, PlaceTransitionObject source, PlaceTransitionObject target, Arc arc, double offsetX, double offsetY) {
+		Arc guiArc = currentGuiModel.getArcByEndpoints(source, target);
+		ArcPath arcPath = guiArc.getArcPath();
+		int arcPathPointsNum = arcPath.getNumPoints();
+		
+		// Build ArcPath
+		ArcPath newArcPath = new ArcPath(arc);
+		for(int k = 0; k < arcPathPointsNum; k++) {
+			ArcPathPoint point = arcPath.getArcPathPoint(k);
+			newArcPath.addPoint(
+					point.getPoint().x + offsetX,
+					point.getPoint().y + offsetY,
+					point.getPointType()
+					);
+		}
+		
+		return newArcPath;
+	}
+
+	private void createInputArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) {
+		int i = 0;
+		for (TimedArcPetriNet tapn : model.activeTemplates()) {
+			DataLayer currentGuiModel = this.guiModels.get(tapn);
+			Tuple<Integer, Integer> offset = this.calculateComponentPosition(i);
+			
+			for (TimedInputArc arc : tapn.inputArcs()) {
+				String sourceTemplate = arc.source().isShared() ? "" : tapn.name();
+				TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
+				
+				String targetTemplate = arc.destination().isShared() ? "" : tapn.name();
+				TimedTransition target = constructedModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name()));
+
+				TimeInterval newInterval = new TimeInterval(arc.interval());
+				newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value()));
+				if (newInterval.upperBound() instanceof Bound.InfBound) {
+					newInterval.setUpperBound(newInterval.upperBound());
+				} else {
+					newInterval.setUpperBound(new IntBound(newInterval.upperBound().value()));
+				}
+				TimedInputArc addedArc = new TimedInputArc(source, target, newInterval, arc.getWeight());
+				constructedModel.add(addedArc);
+				
+				Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
+				Transition guiTarget = guiModel.getTransitionByName(mapping.map(targetTemplate, arc.destination().name()));
+				
+				Arc newArc = new TimedInputArcComponent(new TimedOutputArcComponent(
+						0d,
+						0d,
+						0d,
+						0d,
+						guiSource,
+						guiTarget,
+						arc.getWeight().value(),
+						mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(targetTemplate, arc.destination().name()),
+						false
+						));
+				
+				// Build ArcPath
+				Place oldGuiSource = currentGuiModel.getPlaceByName(arc.source().name());
+				Transition oldGuiTarget = currentGuiModel.getTransitionByName(arc.destination().name());
+				ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight);
+				
+				// Set arcPath, guiModel and connectors
+				((TimedInputArcComponent) newArc).setUnderlyingArc(addedArc);
+				newArc.setArcPath(newArcPath);
+				newArc.setGuiModel(guiModel);
+				newArc.updateArcPosition();
+				guiModel.addPetriNetObject(newArc);
+				guiSource.addConnectFrom(newArc);
+				guiTarget.addConnectTo(newArc);
+			}
+			i++;
+		}
+	}
+
+	private void createOutputArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) {
+		int i = 0;
+		for (TimedArcPetriNet tapn : model.activeTemplates()) {
+			DataLayer currentGuiModel = this.guiModels.get(tapn);
+			Tuple<Integer, Integer> offset = this.calculateComponentPosition(i);
+			
+			for (TimedOutputArc arc : tapn.outputArcs()) {
+				String sourceTemplate = arc.source().isShared() ? "" : tapn.name();
+				TimedTransition source = constructedModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name()));
+
+				String destinationTemplate = arc.destination().isShared() ? "" : tapn.name();
+				TimedPlace target = constructedModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name()));
+
+				TimedOutputArc addedArc = new TimedOutputArc(source, target, arc.getWeight());
+				constructedModel.add(addedArc);
+				
+				Transition guiSource = guiModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name()));
+				Place guiTarget = guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name()));
+				
+				TimedOutputArcComponent newArc = new TimedOutputArcComponent(
+						0d,
+						0d,
+						0d,
+						0d,
+						guiModel.getTransitionByName(mapping.map(sourceTemplate, arc.source().name())),
+						guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name())),
+						arc.getWeight().value(),
+						mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()),
+						false
+						);
+				
+				// Build ArcPath
+				Transition oldGuiSource = currentGuiModel.getTransitionByName(arc.source().name());
+				Place oldGuiTarget = currentGuiModel.getPlaceByName(arc.destination().name());
+				ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight);
+				
+				// Set arcPath, guiModel and connectors
+				newArc.setUnderlyingArc(addedArc);
+				newArc.setArcPath(newArcPath);
+				newArc.setGuiModel(guiModel);
+				newArc.updateArcPosition();
+				guiModel.addArc(newArc);
+				guiSource.addConnectTo(newArc);
+				guiTarget.addConnectFrom(newArc);
+			}
+			i++;
+		}
+	}
+
+	private void createTransportArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) {
+		int i = 0;
+		int nextGroupNr = 0;
+		for (TimedArcPetriNet tapn : model.activeTemplates()) {
+			DataLayer currentGuiModel = this.guiModels.get(tapn);
+			Tuple<Integer, Integer> offset = this.calculateComponentPosition(i);
+			
+			for (TransportArc arc : tapn.transportArcs()) {
+				String sourceTemplate = arc.source().isShared() ? "" : tapn.name();
+				String transitionTemplate = arc.transition().isShared() ? "" : tapn.name();
+				String destinationTemplate = arc.destination().isShared() ? "" : tapn.name();
+				
+				TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
+				TimedTransition transition = constructedModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name()));
+				TimedPlace destination = constructedModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name()));
+				
+				TimeInterval newInterval = new TimeInterval(arc.interval());
+				newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value()));
+				if (newInterval.upperBound() instanceof Bound.InfBound) {
+					newInterval.setUpperBound(newInterval.upperBound());
+				} else {
+					newInterval.setUpperBound(new IntBound(newInterval.upperBound().value()));
+				}
+				TransportArc addedArc = new TransportArc(source, transition, destination, newInterval, arc.getWeight());
+				constructedModel.add(addedArc);
+				
+				//Create input transport arc
+				Place guiSourceIn = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
+				Transition guiTargetIn = guiModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name()));
+								
+				TimedTransportArcComponent newInArc = new TimedTransportArcComponent(
+						new TimedInputArcComponent(new TimedOutputArcComponent(
+							0d,
+							0d,
+							0d,
+							0d,
+							guiSourceIn,
+							guiTargetIn,
+							arc.getWeight().value(),
+							mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(transitionTemplate, arc.transition().name()),
+							false
+							)), 
+						nextGroupNr, 
+						true
+						);
+				
+				// Build ArcPath
+				Place oldGuiSourceIn = currentGuiModel.getPlaceByName(arc.source().name());
+				Transition oldGuiTargetIn = currentGuiModel.getTransitionByName(arc.transition().name());
+				ArcPath newArcPathIn = createArcPath(currentGuiModel, oldGuiSourceIn, oldGuiTargetIn, newInArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight);
+							
+				newInArc.setUnderlyingArc(addedArc);
+				newInArc.setArcPath(newArcPathIn);
+				newInArc.setGuiModel(guiModel);
+				newInArc.updateArcPosition();
+				guiModel.addArc(newInArc);
+				
+				guiSourceIn.addConnectTo(newInArc);
+				guiTargetIn.addConnectFrom(newInArc);
+				
+				// Calculate the next group number for this transport arc
+				// By looking at the target of the newInArc -> a transition
+				// Then finding the largest existing group number of outgoing transport arcs from this transition
+				for (Object pt : newInArc.getTarget().getPostset()) {
+					if (pt instanceof TimedTransportArcComponent) {
+						if (((TimedTransportArcComponent) pt).getGroupNr() > nextGroupNr) {
+							nextGroupNr = ((TimedTransportArcComponent) pt).getGroupNr();
+						}
+					}
+				}
+
+				((TimedTransportArcComponent) newInArc).setGroupNr(nextGroupNr + 1);
+				
+				//Create output transport arc
+				Transition guiSourceOut = guiModel.getTransitionByName(mapping.map(transitionTemplate, arc.transition().name()));
+				Place guiTargetOut = guiModel.getPlaceByName(mapping.map(destinationTemplate, arc.destination().name()));
+				
+				TimedTransportArcComponent newOutArc = new TimedTransportArcComponent(
+						new TimedInputArcComponent(new TimedOutputArcComponent(
+							0d,
+							0d,
+							0d,
+							0d,
+							guiSourceOut,
+							guiTargetOut,
+							1,
+							mapping.map(transitionTemplate, arc.transition().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()),
+							false
+							)), 
+						nextGroupNr + 1, 
+						false
+						);
+				
+				// Build ArcPath
+				Transition oldGuiSourceOut = currentGuiModel.getTransitionByName(arc.transition().name());
+				Place oldGuiTargetOut = currentGuiModel.getPlaceByName(arc.destination().name());
+				ArcPath newArcPathOut = createArcPath(currentGuiModel, oldGuiSourceOut, oldGuiTargetOut, newOutArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight);
+			
+				newOutArc.setUnderlyingArc(addedArc);
+				newOutArc.setArcPath(newArcPathOut);
+				newOutArc.setGuiModel(guiModel);
+				newOutArc.updateArcPosition();
+				guiModel.addArc(newOutArc);
+				
+				// Add connection references to the two transport arcs
+				newInArc.setConnectedTo(newOutArc);
+				newOutArc.setConnectedTo(newInArc);
+				
+				guiSourceOut.addConnectTo(newOutArc);
+				guiTargetOut.addConnectFrom(newOutArc);
+			}
+			i++;
+		}
+	}
+
+	
+	
+	private void createInhibitorArcs(TimedArcPetriNetNetwork model, TimedArcPetriNet constructedModel, NameMapping mapping, DataLayer guiModel, double greatestWidth, double greatestHeight) {
+		int i = 0;
+		for (TimedArcPetriNet tapn : model.activeTemplates()) {
+			DataLayer currentGuiModel = this.guiModels.get(tapn);
+			Tuple<Integer, Integer> offset = this.calculateComponentPosition(i);
+			
+			for (TimedInhibitorArc arc : tapn.inhibitorArcs()) {
+				String sourceTemplate = arc.source().isShared() ? "" : tapn.name();
+				String destinationTemplate = arc.destination().isShared() ? "" : tapn.name();
+				
+				TimedPlace source = constructedModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
+				TimedTransition target = constructedModel.getTransitionByName(mapping.map(destinationTemplate, arc.destination().name()));
+
+				TimeInterval newInterval = new TimeInterval(arc.interval());
+				newInterval.setLowerBound(new IntBound(newInterval.lowerBound().value()));
+				if (newInterval.upperBound() instanceof Bound.InfBound) {
+					newInterval.setUpperBound(newInterval.upperBound());
+				} else {
+					newInterval.setUpperBound(new IntBound(newInterval.upperBound().value()));
+				}
+				TimedInhibitorArc addedArc = new TimedInhibitorArc(source, target, newInterval, arc.getWeight());
+				constructedModel.add(addedArc);
+				
+				Place guiSource = guiModel.getPlaceByName(mapping.map(sourceTemplate, arc.source().name()));
+				Transition guiTarget = guiModel.getTransitionByName(mapping.map(destinationTemplate, arc.destination().name()));
+				Arc newArc = new TimedInhibitorArcComponent(new TimedOutputArcComponent(
+						0d,
+						0d,
+						0d,
+						0d,
+						guiSource,
+						guiTarget,
+						arc.getWeight().value(),
+						mapping.map(sourceTemplate, arc.source().name()) + "_to_" + mapping.map(destinationTemplate, arc.destination().name()),
+						false
+						), "");
+				
+				// Build ArcPath
+				Place oldGuiSource = currentGuiModel.getPlaceByName(arc.source().name());
+				Transition oldGuiTarget = currentGuiModel.getTransitionByName(arc.destination().name());
+				ArcPath newArcPath = createArcPath(currentGuiModel, oldGuiSource, oldGuiTarget, newArc, offset.value1() * greatestWidth, offset.value2() * greatestHeight);
+				
+				((TimedInhibitorArcComponent) newArc).setUnderlyingArc(addedArc);
+				newArc.setArcPath(newArcPath);
+				newArc.setGuiModel(guiModel);
+				newArc.updateArcPosition();
+				guiModel.addPetriNetObject(newArc);
+				guiSource.addConnectTo(newArc);
+				guiTarget.addConnectFrom(newArc);
+			}
+			i++;
+		}
+	}
+}

=== modified file 'src/dk/aau/cs/verification/UPPAAL/Verifyta.java'
--- src/dk/aau/cs/verification/UPPAAL/Verifyta.java	2014-02-25 12:29:17 +0000
+++ src/dk/aau/cs/verification/UPPAAL/Verifyta.java	2014-05-28 18:52:41 +0000
@@ -10,6 +10,7 @@
 import java.util.regex.Pattern;
 
 import net.tapaal.Preferences;
+import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.gui.FileFinder;
 import pipe.gui.FileFinderImpl;
@@ -285,6 +286,10 @@
 				}
 		}
 		
+		if (((VerifytaOptions) options).traceOption() == TraceOption.SOME && ((VerifytaOptions) options).symmetry() == true) {
+			return false;
+		}
+		
 		return true;
 	}
 
@@ -363,7 +368,7 @@
 		UppaalTrace trace = traceParser.parseTrace(new BufferedReader(new StringReader(output)), (VerifytaOptions) options);
 
 		if (trace == null) {
-			if (((VerifytaOptions) options).trace() != TraceOption.NONE) {
+			if (((VerifytaOptions) options).traceOption() != TraceOption.NONE) {
 				if((query.getProperty() instanceof TCTLEFNode && !queryResult.isQuerySatisfied()) || (query.getProperty() instanceof TCTLAGNode && queryResult.isQuerySatisfied()) || 
 				   (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) || (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied()))
 					return null;

=== modified file 'src/dk/aau/cs/verification/UPPAAL/VerifytaOptions.java'
--- src/dk/aau/cs/verification/UPPAAL/VerifytaOptions.java	2013-06-25 20:49:54 +0000
+++ src/dk/aau/cs/verification/UPPAAL/VerifytaOptions.java	2014-05-28 18:52:41 +0000
@@ -15,27 +15,33 @@
 	private ReductionOption reduction;
 	private boolean symmetry;
 	private boolean useOverApproximation;
+	private boolean enableOverApproximation;
+	private boolean enableUnderApproximation;
+	private int approximationDenominator;
 
 	private static final Map<TraceOption, String> traceMap = createTraceOptionsMap();
 	private static final Map<SearchOption, String> searchMap = createSearchOptionsMap();
 
 	public VerifytaOptions(TraceOption trace, SearchOption search,
-			boolean untimedTrace, ReductionOption reduction, boolean symmetry, boolean useOverApproximation) {
+			boolean untimedTrace, ReductionOption reduction, boolean symmetry, boolean useOverApproximation, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
 		traceOption = trace;
 		searchOption = search;
 		this.untimedTrace = untimedTrace;
 		this.reduction = reduction;
 		this.symmetry = symmetry;
 		this.useOverApproximation = useOverApproximation;
+		this.enableOverApproximation = enableOverApproximation;
+		this.enableUnderApproximation = enableUnderApproximation;
+		this.approximationDenominator = approximationDenominator;
 	}
 
-	public TraceOption trace() {
-		return traceOption;
-	}
-	
 	public boolean symmetry() {
 		return symmetry;
 	}
+	
+	public void setSymmetry(boolean newOption) {
+		this.symmetry = newOption;
+	}
 
 	@Override
 	public String toString() {
@@ -88,9 +94,28 @@
 	public TraceOption traceOption() {
 		return traceOption;
 	}
+	
+	public void setTraceOption(TraceOption option) {
+		traceOption = option;
+	}
 
 	@Override
 	public SearchOption searchOption() {
 		return searchOption;
 	}
+	
+	@Override
+	public boolean enableOverApproximation() {
+		return enableOverApproximation;
+	}
+
+	@Override
+	public boolean enableUnderApproximation() {
+		return enableUnderApproximation;
+	}
+
+	@Override
+	public int approximationDenominator() {
+		return approximationDenominator;
+	}
 }

=== modified file 'src/dk/aau/cs/verification/VerificationOptions.java'
--- src/dk/aau/cs/verification/VerificationOptions.java	2013-06-25 20:49:54 +0000
+++ src/dk/aau/cs/verification/VerificationOptions.java	2014-05-28 18:52:41 +0000
@@ -2,6 +2,7 @@
 
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
+import pipe.gui.widgets.InclusionPlaces;
 
 public interface VerificationOptions {
 	// Probably need something like this in reality, but for now we dont need it
@@ -11,7 +12,11 @@
 
 	String toString();
 	boolean useOverApproximation();
+	boolean enableOverApproximation();
+	boolean enableUnderApproximation();
+	int approximationDenominator();
 	int extraTokens();
 	TraceOption traceOption();
+	void setTraceOption(TraceOption option);
 	SearchOption searchOption();
 }

=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2014-03-16 19:13:22 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2014-05-28 18:52:41 +0000
@@ -110,6 +110,14 @@
 		return queryResult;
 	}
 
+	public void setTrace(TTrace newTrace){
+		trace = newTrace;
+	}
+	
+	public void setSecondaryTrace(TTrace newTrace){
+		secondaryTrace = newTrace;
+	}
+	
 	public TTrace getTrace() {
 		return trace;
 	}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java	2014-02-19 18:31:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java	2014-05-28 18:52:41 +0000
@@ -16,36 +16,41 @@
 
 	public VerifyDTAPNOptions(int extraTokens, TraceOption traceOption,
 			SearchOption search, boolean symmetry, boolean gcd, boolean timeDarts,
-			boolean pTrie, WorkflowMode workflowMode) {
-		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false);
+			boolean pTrie, WorkflowMode workflowMode,
+			boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, false, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.workflow = workflowMode;
 	}
 	
 	public VerifyDTAPNOptions(int extraTokens, TraceOption traceOption,
 			SearchOption search, boolean symmetry, boolean gcd, boolean timeDarts,
-			boolean pTrie, boolean useOverApproximation) {
-		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, useOverApproximation, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW);
+			boolean pTrie, boolean useOverApproximation,
+			boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, useOverApproximation, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
 	
 	//Only used for boundedness analysis
 	public VerifyDTAPNOptions(boolean dontUseDeadPlaces, int extraTokens, TraceOption traceOption,
 			SearchOption search, boolean symmetry, boolean timeDarts,
-			boolean pTrie) {
-		this(extraTokens, traceOption, search, symmetry, true, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW);
+			boolean pTrie,
+			boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, symmetry, true, timeDarts, pTrie, false, false, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.dontUseDeadPlaces = dontUseDeadPlaces;
 	}
 
 	public VerifyDTAPNOptions(int extraTokens, TraceOption traceOption,
 			SearchOption search, boolean symmetry, boolean discreteInclusion, boolean gcd,
-			boolean timeDarts, boolean pTrie, boolean useOverApproximation) {
-		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, useOverApproximation, discreteInclusion, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW);
+			boolean timeDarts, boolean pTrie, boolean useOverApproximation,
+			boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, symmetry, gcd, timeDarts, pTrie, useOverApproximation, discreteInclusion, new InclusionPlaces(), WorkflowMode.NOT_WORKFLOW, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
 
 	public VerifyDTAPNOptions(int extraTokens, TraceOption traceOption,
 			SearchOption search, boolean symmetry, boolean gcd, boolean timeDarts,
 			boolean pTrie, boolean useOverApproximation, boolean discreteInclusion,
-			InclusionPlaces inclusionPlaces, WorkflowMode workflow) {
-		super(extraTokens, traceOption, search, symmetry, useOverApproximation, discreteInclusion, inclusionPlaces);
+			InclusionPlaces inclusionPlaces, WorkflowMode workflow,
+			boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		super(extraTokens, traceOption, search, symmetry, useOverApproximation, discreteInclusion, inclusionPlaces, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.timeDarts = timeDarts;
 		this.pTrie = pTrie;
 		this.workflow = workflow;

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2014-02-25 11:36:28 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2014-05-28 18:52:41 +0000
@@ -12,13 +12,13 @@
 	private static final Map<SearchOption, String> searchMap = createSearchOptionsMap();
 	private ModelReduction modelReduction;
 	
-	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction) {
-		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces());
+	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.modelReduction = modelReduction;
 	}
 	
-	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction) {
-		this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION);
+	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
 
 	@Override

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2013-11-25 14:26:43 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2014-05-28 18:52:41 +0000
@@ -42,11 +42,11 @@
 			
 			VerifyTAPNOptions options = null;
 			if(dataLayerQuery == null){
-				options = new VerifyTAPNOptions(query.getExtraTokens(), TraceOption.NONE, SearchOption.HEURISTIC, true, true);
+				options = new VerifyTAPNOptions(query.getExtraTokens(), TraceOption.NONE, SearchOption.HEURISTIC, true, true, false, false, 1);
 			}else if(dataLayerQuery.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification){
-				options = new VerifyDTAPNOptions(dataLayerQuery.getCapacity()+model.getNumberOfTokensInNet(), dataLayerQuery.getTraceOption(), dataLayerQuery.getSearchOption(),dataLayerQuery.useSymmetry(), dataLayerQuery.useGCD(), dataLayerQuery.useTimeDarts(), dataLayerQuery.usePTrie(), dataLayerQuery.useOverApproximation());
+				options = new VerifyDTAPNOptions(dataLayerQuery.getCapacity()+model.getNumberOfTokensInNet(), dataLayerQuery.getTraceOption(), dataLayerQuery.getSearchOption(),dataLayerQuery.useSymmetry(), dataLayerQuery.useGCD(), dataLayerQuery.useTimeDarts(), dataLayerQuery.usePTrie(), dataLayerQuery.useOverApproximation(), dataLayerQuery.isOverApproximationEnabled(), dataLayerQuery.isUnderApproximationEnabled(), dataLayerQuery.approximationDenominator());
 			} else {
-				options = new VerifyTAPNOptions(dataLayerQuery.getCapacity()+model.getNumberOfTokensInNet(), dataLayerQuery.getTraceOption(), dataLayerQuery.getSearchOption(),dataLayerQuery.useSymmetry(), dataLayerQuery.useOverApproximation());
+				options = new VerifyTAPNOptions(dataLayerQuery.getCapacity()+model.getNumberOfTokensInNet(), dataLayerQuery.getTraceOption(), dataLayerQuery.getSearchOption(),dataLayerQuery.useSymmetry(), dataLayerQuery.useOverApproximation(), dataLayerQuery.isOverApproximationEnabled(), dataLayerQuery.isUnderApproximationEnabled(), dataLayerQuery.approximationDenominator());
 			}
 		} catch(FileNotFoundException e) {
 			System.err.append("An error occurred while exporting the model to verifytapn. Verification cancelled.");

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java	2013-12-05 13:46:06 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java	2014-05-28 18:52:41 +0000
@@ -11,6 +11,8 @@
 
 	@Override
 	public ImageIcon getIconFor(VerificationResult<?> result) {
+		if (result.getQueryResult().isApproximationInconclusive())
+			return rerunIcon;
 		switch(result.getQueryResult().queryType())
 		{
 		case EF:

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2013-10-02 20:25:38 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2014-05-28 18:52:41 +0000
@@ -20,6 +20,9 @@
 	private boolean useOverApproximation;
 	private boolean discreteInclusion;
 	private InclusionPlaces inclusionPlaces;
+	private boolean enableOverApproximation;
+	private boolean enableUnderApproximation;
+	private int approximationDenominator;
 	
 	//only used for boundedness analysis
 	private boolean dontUseDeadPlaces = false;
@@ -27,21 +30,21 @@
 	private static final Map<TraceOption, String> traceMap = createTraceOptionsMap();
 	private static final Map<SearchOption, String> searchMap = createSearchOptionsMap();
 
-	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation) {
-		this(extraTokens, traceOption, search, symmetry, useOverApproximation, false, new InclusionPlaces());
+	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, symmetry, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
 	
 	//Only used for boundedness analysis
-	public VerifyTAPNOptions(boolean dontUseDeadPLaces, int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation) {
-		this(extraTokens, traceOption, search, symmetry, useOverApproximation, false, new InclusionPlaces());
+	public VerifyTAPNOptions(boolean dontUseDeadPLaces, int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens, traceOption, search, symmetry, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.dontUseDeadPlaces = dontUseDeadPLaces;
 	}
 	
-	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation, boolean discreteInclusion) {
-		this(extraTokens,traceOption, search, symmetry, useOverApproximation, discreteInclusion, new InclusionPlaces());
+	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
+		this(extraTokens,traceOption, search, symmetry, useOverApproximation, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
 	
-	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation, boolean discreteInclusion, InclusionPlaces inclusionPlaces) {
+	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useOverApproximation, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
 		this.extraTokens = extraTokens;
 		this.traceOption = traceOption;
 		searchOption = search;
@@ -49,6 +52,9 @@
 		this.discreteInclusion = discreteInclusion;
 		this.useOverApproximation = useOverApproximation;
 		this.inclusionPlaces = inclusionPlaces;
+		this.enableOverApproximation = enableOverApproximation;
+		this.enableUnderApproximation = enableUnderApproximation;
+		this.approximationDenominator = approximationDenominator;
 	}
 
 	public TraceOption trace() {
@@ -144,9 +150,28 @@
 	public TraceOption traceOption() {
 		return traceOption;
 	}
+	
+	public void setTraceOption(TraceOption option) {
+		traceOption = option;
+	}
 
 	@Override
 	public SearchOption searchOption() {
 		return searchOption;
 	}
+
+	@Override
+	public boolean enableOverApproximation() {
+		return enableOverApproximation;
+	}
+
+	@Override
+	public boolean enableUnderApproximation() {
+		return enableUnderApproximation;
+	}
+
+	@Override
+	public int approximationDenominator() {
+		return approximationDenominator;
+	}
 }

=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java'
--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java	2013-03-03 11:14:15 +0000
+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java	2014-05-28 18:52:41 +0000
@@ -16,11 +16,17 @@
 		KeepQueryOption, Yes, No
 	};
 	
+	public enum ApproximationMethodOption {
+		KeepQueryOption, None, OverApproximation, UnderApproximation
+	}
+	
 	private List<ReductionOption> reductionOptions;
 	private ReductionOption reductionOption;
 	private SearchOption searchOption;
 	private QueryPropertyOption queryPropertyOption;
 	private SymmetryOption symmetryOption;
+	private ApproximationMethodOption approximationMethodOption;
+	private int approximationDenominator = 0;
 	private boolean keepQueryCapacity;
 	private int capacity;
 	private boolean discreteInclusion = false; // only for VerifyTAPN
@@ -29,7 +35,7 @@
 	private boolean usePTrie = false;
 	
 	public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, ReductionOption reductionOption, boolean discreteInclusion,
-			boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, List<ReductionOption> reductionOptions) {
+			boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, ApproximationMethodOption approximationMethodOption, int approximationDenominator, List<ReductionOption> reductionOptions) {
 		Require.that(!(reductionOptions == null && reductionOption == ReductionOption.BatchProcessingUserDefinedReductions), "ReductionOption was given as userdefined but a list of reductionoptions was not given");
 		this.searchOption = searchOption;
 		this.reductionOption = reductionOption;
@@ -42,11 +48,13 @@
 		this.useTimeDart = useTimeDart;
 		this.usePTrie = usePTrie;
 		this.reductionOptions = reductionOptions;
+		this.approximationMethodOption = approximationMethodOption;
+		this.approximationDenominator = approximationDenominator;
 	}
 	
 	public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, ReductionOption reductionOption, boolean discreteInclusion,
-			boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie) {
-		this(queryPropertyOption, keepQueryCapacity, capacity, searchOption, symmetryOption, reductionOption, discreteInclusion, useTimeDartPTrie, useTimeDart, usePTrie, null); 
+			boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, ApproximationMethodOption approximationMethodOption, int approximationRValue) {
+		this(queryPropertyOption, keepQueryCapacity, capacity, searchOption, symmetryOption, reductionOption, discreteInclusion, useTimeDartPTrie, useTimeDart, usePTrie, approximationMethodOption, approximationRValue, null); 
 	}
 	
 	public boolean isReductionOptionUserdefined(){
@@ -93,4 +101,12 @@
 	public int capacity() {
 		return capacity;
 	}
+	
+	public ApproximationMethodOption approximationMethodOption() {
+		return approximationMethodOption;
+	}
+	
+	public int approximationDenominator() {
+		return approximationDenominator;
+	}
 }

=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2014-05-22 19:02:06 +0000
+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2014-05-28 18:52:41 +0000
@@ -1,6 +1,7 @@
 package dk.aau.cs.verification.batchProcessing;
 
 import java.io.File;
+import java.math.BigDecimal;
 import java.util.ArrayList;
 import java.util.List;
 
@@ -10,19 +11,33 @@
 import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.gui.FileFinderImpl;
 import pipe.gui.MessengerImpl;
+import pipe.gui.widgets.InclusionPlaces;
 import dk.aau.cs.Messenger;
 import dk.aau.cs.TCTL.TCTLAGNode;
 import dk.aau.cs.TCTL.TCTLAbstractProperty;
 import dk.aau.cs.TCTL.TCTLTrueNode;
 import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
+import dk.aau.cs.approximation.ApproximationWorker;
+import dk.aau.cs.approximation.OverApproximation;
+import dk.aau.cs.approximation.UnderApproximation;
 import dk.aau.cs.gui.BatchProcessingDialog;
 import dk.aau.cs.gui.components.BatchProcessingResultsTableModel;
 import dk.aau.cs.io.batchProcessing.BatchProcessingModelLoader;
 import dk.aau.cs.io.batchProcessing.LoadedBatchProcessingModel;
 import dk.aau.cs.model.tapn.TAPNQuery;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedInhibitorArc;
+import dk.aau.cs.model.tapn.TimedInputArc;
+import dk.aau.cs.model.tapn.TimedOutputArc;
 import dk.aau.cs.model.tapn.TimedPlace;
+import dk.aau.cs.model.tapn.TimedToken;
+import dk.aau.cs.model.tapn.TimedTransition;
+import dk.aau.cs.model.tapn.TransportArc;
+import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
+import dk.aau.cs.model.tapn.simulation.TimeDelayStep;
+import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetStep;
 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
+import dk.aau.cs.model.tapn.simulation.TimedTransitionStep;
 import dk.aau.cs.translations.ReductionOption;
 import dk.aau.cs.util.MemoryMonitor;
 import dk.aau.cs.util.Require;
@@ -30,6 +45,7 @@
 import dk.aau.cs.util.UnsupportedModelException;
 import dk.aau.cs.util.UnsupportedQueryException;
 import dk.aau.cs.verification.Boundedness;
+import dk.aau.cs.verification.ITAPNComposer;
 import dk.aau.cs.verification.ModelChecker;
 import dk.aau.cs.verification.NameMapping;
 import dk.aau.cs.verification.NullStats;
@@ -37,6 +53,7 @@
 import dk.aau.cs.verification.QueryType;
 import dk.aau.cs.verification.Stats;
 import dk.aau.cs.verification.TAPNComposer;
+import dk.aau.cs.verification.TAPNTraceDecomposer;
 import dk.aau.cs.verification.VerificationOptions;
 import dk.aau.cs.verification.VerificationResult;
 import dk.aau.cs.verification.UPPAAL.Verifyta;
@@ -47,6 +64,7 @@
 import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN;
 import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification;
 import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
+import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.ApproximationMethodOption;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.QueryPropertyOption;
 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.SymmetryOption;
 
@@ -62,7 +80,9 @@
 	private boolean timeoutCurrentVerification = false;
 	private boolean oomCurrentVerification = false;
 	private int verificationTasksCompleted;
-
+	private LoadedBatchProcessingModel model;
+	
+	
 	public BatchProcessingWorker(List<File> files, BatchProcessingResultsTableModel tableModel, BatchProcessingVerificationOptions batchProcessingVerificationOptions) {
 		super();
 		this.files = files;
@@ -107,17 +127,18 @@
 
 			fireFileChanged(file.getName());
 			LoadedBatchProcessingModel model = loadModel(file);
-			if(model != null) {
-				Tuple<TimedArcPetriNet, NameMapping> composedModel = composeModel(model);
-				
+			this.model = model;
+			if(model != null) {			
 				for(pipe.dataLayer.TAPNQuery query : model.queries()) {
-                                        if(exiting()) {
-                                                return null;
-                                        }					
+                    if(exiting()) {
+                        return null;
+                    }			
+                    Tuple<TimedArcPetriNet, NameMapping> composedModel = composeModel(model);
+                                        
 					pipe.dataLayer.TAPNQuery queryToVerify = overrideVerificationOptions(composedModel.value1(), query);
 					
 					if (batchProcessingVerificationOptions.isReductionOptionUserdefined()){
-						processQueryForUserdefinedReductions(file,composedModel, queryToVerify);
+						processQueryForUserdefinedReductions(file, composedModel, queryToVerify);
 					} else {
 						processQuery(file, composedModel, queryToVerify);
 					}
@@ -236,8 +257,24 @@
 			boolean symmetry = batchProcessingVerificationOptions.symmetry() == SymmetryOption.KeepQueryOption ? query.useSymmetry() : getSymmetryFromBatchProcessingOptions();
 			int capacity = batchProcessingVerificationOptions.KeepCapacityFromQuery() ? query.getCapacity() : batchProcessingVerificationOptions.capacity();
 			String name = batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.KeepQueryOption ? query.getName() : "Search Whole State Space";
+			boolean overApproximation = query.isOverApproximationEnabled();
+			boolean underApproximation = query.isUnderApproximationEnabled();
+			int approximationDenominator = query.approximationDenominator();
+			if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) {
+				overApproximation = false;
+				underApproximation = false;
+			} else if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.OverApproximation) {
+				overApproximation = true;
+				underApproximation = false;
+			} else if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.UnderApproximation) {
+				overApproximation = false;
+				underApproximation = true;
+			}
+			if (batchProcessingVerificationOptions.approximationDenominator() != 0) {
+				approximationDenominator = batchProcessingVerificationOptions.approximationDenominator();
+			}
 			
-			pipe.dataLayer.TAPNQuery changedQuery = new pipe.dataLayer.TAPNQuery(name, capacity, property, TraceOption.NONE, search, option, symmetry, false, query.useTimeDarts(), query.usePTrie(), query.useOverApproximation(), query.useReduction(), query.getHashTableSize(), query.getExtrapolationOption(), query.inclusionPlaces());
+			pipe.dataLayer.TAPNQuery changedQuery = new pipe.dataLayer.TAPNQuery(name, capacity, property, TraceOption.NONE, search, option, symmetry, false, query.useTimeDarts(), query.usePTrie(), query.useOverApproximation(), query.useReduction(),  query.getHashTableSize(), query.getExtrapolationOption(), query.inclusionPlaces(), overApproximation, underApproximation, approximationDenominator);
 			
 			if(batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.KeepQueryOption)
 				changedQuery.setActive(query.isActive());
@@ -253,7 +290,7 @@
 	}
 
 	private Tuple<TimedArcPetriNet, NameMapping> composeModel(LoadedBatchProcessingModel model) {
-		TAPNComposer composer = new TAPNComposer(new Messenger(){
+		ITAPNComposer composer = new TAPNComposer(new Messenger(){
 			public void displayInfoMessage(String message) { }
 			public void displayInfoMessage(String message, String title) {}
 			public void displayErrorMessage(String message) {}
@@ -295,16 +332,24 @@
 			publishResult(file.getName(), query, "Skipped - due to OOM", verificationResult.verificationTime(), new NullStats());
 			oomCurrentVerification = false;
 		} else if(!verificationResult.error()) {
-			String queryResult = verificationResult.getQueryResult().isQuerySatisfied() ? "Satisfied" : "Not Satisfied";
-				if (query.discreteInclusion() && !verificationResult.isBounded() && 
-						((query.queryType().equals(QueryType.EF) && !verificationResult.getQueryResult().isQuerySatisfied())
-						||
-						(query.queryType().equals(QueryType.AG) && verificationResult.getQueryResult().isQuerySatisfied())))
-				{queryResult = "Inconclusive answer";}
+			String queryResult = "";
+			if (verificationResult.getQueryResult().isApproximationInconclusive())
+			{
+				queryResult = "Inconclusive";
+			}
+			else
+			{
+				queryResult = verificationResult.getQueryResult().isQuerySatisfied() ? "Satisfied" : "Not Satisfied";
+			}
+			if (query.discreteInclusion() && !verificationResult.isBounded() && 
+					((query.queryType().equals(QueryType.EF) && !verificationResult.getQueryResult().isQuerySatisfied())
+					||
+					(query.queryType().equals(QueryType.AG) && verificationResult.getQueryResult().isQuerySatisfied())))
+			{queryResult = "Inconclusive";}
 				if(query.getReductionOption().equals(ReductionOption.VerifyPNApprox) && 
 						((query.queryType().equals(QueryType.EF) && verificationResult.getQueryResult().isQuerySatisfied()) ||
 						(query.queryType().equals(QueryType.AG) && !verificationResult.getQueryResult().isQuerySatisfied()))){
-					queryResult = "Inconclusive answer";
+					queryResult = "Inconclusive";
 				}
 			publishResult(file.getName(), query, queryResult,	verificationResult.verificationTime(), verificationResult.stats());
 		} else {
@@ -317,15 +362,33 @@
 		publish(result);
 	}
 
-	private VerificationResult<TimedArcPetriNetTrace> verify(Tuple<TimedArcPetriNet, NameMapping> composedModel, pipe.dataLayer.TAPNQuery query) throws Exception {
+	
+	private void renameTraceTransitions(TimedArcPetriNetTrace trace) {
+		if (trace != null)
+			trace.reduceTraceForOriginalNet("_traceNet_", "PTRACE");
+	}
+
+	private TAPNNetworkTrace decomposeTrace(TimedArcPetriNetTrace trace, NameMapping mapping) {
+		if (trace == null)
+			return null;
+
+		TAPNTraceDecomposer decomposer = new TAPNTraceDecomposer(trace, model.network(), mapping);
+		return decomposer.decompose();
+	}
+	
+	private VerificationResult<TimedArcPetriNetTrace> verify(Tuple<TimedArcPetriNet, NameMapping> composedModel, pipe.dataLayer.TAPNQuery query) throws Exception {		
 		TAPNQuery queryToVerify = getTAPNQuery(composedModel.value1(),query);
 		MapQueryToNewNames(queryToVerify, composedModel.value2());
 		
+		TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), queryToVerify.getExtraTokens());
+		MapQueryToNewNames(clonedQuery, composedModel.value2());
+		
 		VerificationOptions options = getVerificationOptionsFromQuery(query);
 		modelChecker = getModelChecker(query);
 		fireVerificationTaskStarted();
-		VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify);
-		return verificationResult;
+		
+		ApproximationWorker worker = new ApproximationWorker();
+		return worker.batchWorker(composedModel, options, query, model, modelChecker, queryToVerify, clonedQuery, this);
 	}
 
 	private TAPNQuery getTAPNQuery(TimedArcPetriNet model, pipe.dataLayer.TAPNQuery query) throws Exception {
@@ -353,13 +416,13 @@
 
 	private VerificationOptions getVerificationOptionsFromQuery(pipe.dataLayer.TAPNQuery query) {
 		if(query.getReductionOption() == ReductionOption.VerifyTAPN)
-			return new VerifyTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), false, query.discreteInclusion(), query.inclusionPlaces());	// XXX DISABLES OverApprox
+			return new VerifyTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), false, query.discreteInclusion(), query.inclusionPlaces(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());	// XXX DISABLES OverApprox
 		else if(query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification)
-			return new VerifyDTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), false,  query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode());
+			return new VerifyDTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), false,  query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 		else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
-			return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction());
+			return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 		else
-			return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false);
+			return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 	}
 	
 	private void MapQueryToNewNames(TAPNQuery query, NameMapping mapping) {

=== modified file 'src/pipe/dataLayer/DataLayer.java'
--- src/pipe/dataLayer/DataLayer.java	2011-09-25 09:35:57 +0000
+++ src/pipe/dataLayer/DataLayer.java	2014-05-28 18:52:41 +0000
@@ -665,7 +665,15 @@
 		return returnArray;
 	}
 
-
+	public Arc getArcByEndpoints(PlaceTransitionObject source, PlaceTransitionObject target) {
+		Arc returnArc = null;
+		for (Arc arc : arcsArray) {
+			if (arc.getSource() == source && arc.getTarget() == target) {
+				returnArc = arc;
+			}
+		}
+		return returnArc;
+	}
 
 	/**
 	 * Return the Transition called transitionName from the Petri-Net

=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java	2014-02-22 23:21:12 +0000
+++ src/pipe/dataLayer/TAPNQuery.java	2014-05-28 18:52:41 +0000
@@ -45,6 +45,10 @@
 	private WorkflowMode workflow;
 	private boolean useReduction;
 	
+	private boolean enableOverApproximation = false;
+	private boolean enableUnderApproximation = false;
+	private int denominator = 2;
+	
 	private boolean discreteInclusion = false; // Only for VerifyTAPN
 
 	private TCTLAbstractProperty property = null;
@@ -64,6 +68,19 @@
 	public String getName() {
 		return name;
 	}
+	
+	public boolean isOverApproximationEnabled() {
+		return this.enableOverApproximation;
+	}
+	
+	public boolean isUnderApproximationEnabled() {
+		return this.enableUnderApproximation;
+	}
+
+	
+	public int approximationDenominator() {
+		return this.denominator;
+	}
 
 	public void setDiscreteInclusion(boolean value){
 		discreteInclusion = value;
@@ -237,6 +254,14 @@
 			TraceOption traceOption, SearchOption searchOption,
 			ReductionOption reductionOption, boolean symmetry, boolean gcd, boolean timeDart, boolean pTrie, boolean overApproximation, boolean reduction, HashTableSize hashTabelSize,
 			ExtrapolationOption extrapolationOption, InclusionPlaces inclusionPlaces) {
+		this(name, capacity, property, traceOption, searchOption, reductionOption, symmetry, gcd, timeDart, pTrie, false, reduction, hashTabelSize, extrapolationOption, new InclusionPlaces(), false, false, 0);
+	}
+	
+	public TAPNQuery(String name, int capacity, TCTLAbstractProperty property,
+			TraceOption traceOption, SearchOption searchOption,
+			ReductionOption reductionOption, boolean symmetry, boolean gcd, boolean timeDart, boolean pTrie, boolean overApproximation, boolean reduction, HashTableSize hashTabelSize,
+			ExtrapolationOption extrapolationOption, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, 
+			int approximationDenominator) {
 		this.setName(name);
 		this.setCapacity(capacity);
 		this.property = property;
@@ -252,8 +277,12 @@
 		this.setExtrapolationOption(extrapolationOption);
 		this.inclusionPlaces = inclusionPlaces;
 		this.useReduction = reduction;
+		this.enableOverApproximation = enableOverApproximation;
+		this.enableUnderApproximation = enableUnderApproximation;
+		this.denominator = approximationDenominator;
 	}
-	
+
+
 	@Override
 	public String toString() {
 		return getName();
@@ -286,7 +315,7 @@
 	}
 
 	public TAPNQuery copy() {
-		TAPNQuery copy = new TAPNQuery(name, capacity, property.copy(), traceOption, searchOption, reductionOption, symmetry, gcd, timeDart, pTrie, overApproximation, useReduction, hashTableSize, extrapolationOption, inclusionPlaces);
+		TAPNQuery copy = new TAPNQuery(name, capacity, property.copy(), traceOption, searchOption, reductionOption, symmetry, gcd, timeDart, pTrie, overApproximation, useReduction, hashTableSize, extrapolationOption, inclusionPlaces, enableOverApproximation, enableUnderApproximation, denominator);
 		copy.setDiscreteInclusion(discreteInclusion);
 		copy.setActive(isActive);
 		

=== modified file 'src/pipe/gui/GuiFrame.java'
--- src/pipe/gui/GuiFrame.java	2014-03-03 23:13:48 +0000
+++ src/pipe/gui/GuiFrame.java	2014-05-28 18:52:41 +0000
@@ -2251,9 +2251,9 @@
 		buffer.append("License information and more is availabe at: www.tapaal.net\n\n");
 		buffer.append("Credits\n\n");
 		buffer.append("TAPAAL GUI and Translations:\n");
-		buffer.append("Mathias Andersen, Joakim Byg, Louise Foshammer, Malte Neve-Graesboell,\n");
-                buffer.append("Lasse Jacobsen, Morten Jacobsen, Peter G. Jensen, ");
-		buffer.append("Kenneth Y. Joergensen,\nMikael H. Moeller, Jiri Srba, Mathias G. Soerensen and Jakob H. Taankvist\n");
+		buffer.append("Mathias Andersen, Sine V. Birch, Joakim Byg, Louise Foshammer, Malte Neve-Graesboell,\n");
+                buffer.append("Lasse Jacobsen, Morten Jacobsen, Thomas S. Jacobsen, Jacob J. Jensen, Peter G. Jensen, ");
+		buffer.append("\nKenneth Y. Joergensen, Mikael H. Moeller, Christoffer Moesgaard, Niels N. Samuelsen,\nJiri Srba, Mathias G. Soerensen and Jakob H. Taankvist\n");
 		buffer.append("Aalborg University 2009-2014\n\n");
 		buffer.append("TAPAAL Continuous Engine (verifytapn):\n");
 		buffer.append("Alexandre David, Lasse Jacobsen, Morten Jacobsen and Jiri Srba\n");

=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
--- src/pipe/gui/KBoundAnalyzer.java	2014-02-25 10:13:00 +0000
+++ src/pipe/gui/KBoundAnalyzer.java	2014-05-28 18:52:41 +0000
@@ -45,17 +45,17 @@
 		RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());
 		dialog.setupListeners(analyzer);
 
-		analyzer.execute(options, tapnNetwork, query);
+		analyzer.execute(options, tapnNetwork, query, null);
 		dialog.setVisible(true);
 	}
 
 	protected VerifyTAPNOptions verificationOptions() {
 		if(modelChecker instanceof VerifyPN){
-			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING);
+			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1);
 		} else if(modelChecker instanceof VerifyTAPN){
-			return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true);
+			return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
 		} else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
-			return new VerifyDTAPNOptions(true, k, TraceOption.NONE, SearchOption.BFS, true, tapnNetwork.hasUrgentTransitions()?false:true, true);
+			return new VerifyDTAPNOptions(true, k, TraceOption.NONE, SearchOption.BFS, true, tapnNetwork.hasUrgentTransitions()?false:true, true, false, false, 1);
 		}
 		return null;
 	}

=== modified file 'src/pipe/gui/RunKBoundAnalysis.java'
--- src/pipe/gui/RunKBoundAnalysis.java	2011-09-08 08:43:34 +0000
+++ src/pipe/gui/RunKBoundAnalysis.java	2014-05-28 18:52:41 +0000
@@ -15,7 +15,7 @@
 	private final JSpinner spinner;
 
 	public RunKBoundAnalysis(ModelChecker modelChecker, Messenger messenger,JSpinner spinner) {
-		super(modelChecker, messenger);
+		super(modelChecker, messenger, null);
 		this.spinner = spinner;
 	}
 

=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java	2014-03-16 20:40:17 +0000
+++ src/pipe/gui/RunVerification.java	2014-05-28 18:52:41 +0000
@@ -19,6 +19,7 @@
 import java.awt.event.HierarchyListener;
 import java.util.ArrayList;
 import java.util.Comparator;
+import java.util.HashMap;
 import java.util.List;
 
 import javax.swing.JButton;
@@ -38,9 +39,11 @@
 import javax.swing.table.TableModel;
 import javax.swing.table.TableRowSorter;
 
+import pipe.dataLayer.DataLayer;
 import pipe.gui.GuiFrame.GUIMode;
 import pipe.gui.widgets.RunningVerificationDialog;
 import dk.aau.cs.Messenger;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
 import dk.aau.cs.util.MemoryMonitor;
 import dk.aau.cs.util.Tuple;
@@ -54,14 +57,14 @@
 public class RunVerification extends RunVerificationBase {
 	private IconSelector iconSelector;
 	private VerificationCallback callback;
-	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {
-		super(modelChecker, messenger);
+	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
+		super(modelChecker, messenger, guiModels);
 		iconSelector = selector;
 		this.callback = callback;
 	}
 	
 	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger) {
-		this(modelChecker, selector, messenger, null);
+		this(modelChecker, selector, messenger, null, null);
 	}
 
 	@Override
@@ -330,7 +333,7 @@
 			gbc.gridy = 4;
 			gbc.insets = new Insets(0,0,15,0);
 			gbc.anchor = GridBagConstraints.WEST;
-			panel.add(new JLabel(toHTML("The query was resolved using the over-approximation.")), gbc);
+			panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
 		}
 		
 		gbc = new GridBagConstraints();

=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java	2014-02-25 10:13:00 +0000
+++ src/pipe/gui/RunVerificationBase.java	2014-05-28 18:52:41 +0000
@@ -1,30 +1,47 @@
 package pipe.gui;
 
+import java.math.BigDecimal;
+import java.util.HashMap;
 import java.util.concurrent.ExecutionException;
 
 import javax.swing.SwingUtilities;
 import javax.swing.SwingWorker;
 
+import pipe.dataLayer.DataLayer;
+import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.dataLayer.TAPNQuery.SearchOption;
+import pipe.gui.widgets.InclusionPlaces;
 import dk.aau.cs.Messenger;
 import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
+import dk.aau.cs.approximation.ApproximationWorker;
+import dk.aau.cs.approximation.OverApproximation;
+import dk.aau.cs.approximation.UnderApproximation;
 import dk.aau.cs.model.tapn.TAPNQuery;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
+import dk.aau.cs.model.tapn.TimedToken;
 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
+import dk.aau.cs.model.tapn.simulation.TimeDelayStep;
+import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetStep;
 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
+import dk.aau.cs.model.tapn.simulation.TimedTransitionStep;
+import dk.aau.cs.util.MemoryMonitor;
 import dk.aau.cs.util.Tuple;
 import dk.aau.cs.util.UnsupportedModelException;
+import dk.aau.cs.verification.ITAPNComposer;
 import dk.aau.cs.verification.ModelChecker;
 import dk.aau.cs.verification.NameMapping;
 import dk.aau.cs.verification.QueryType;
+import dk.aau.cs.verification.QueryResult;
 import dk.aau.cs.verification.TAPNComposer;
 import dk.aau.cs.verification.TAPNTraceDecomposer;
 import dk.aau.cs.verification.VerificationOptions;
 import dk.aau.cs.verification.VerificationResult;
+import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
 import dk.aau.cs.verification.VerifyTAPN.ModelReduction;
 import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
 import dk.aau.cs.verification.VerifyTAPN.VerifyPNOptions;
+import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
 
 public abstract class RunVerificationBase extends SwingWorker<VerificationResult<TAPNNetworkTrace>, Void> {
 
@@ -33,30 +50,47 @@
 	private VerificationOptions options;
 	protected TimedArcPetriNetNetwork model;
 	protected TAPNQuery query;
-
+	protected pipe.dataLayer.TAPNQuery dataLayerQuery;
+	protected HashMap<TimedArcPetriNet, DataLayer> guiModels;
+	
+	
 	protected Messenger messenger;
 
-	public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
+	public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
 		super();
 		this.modelChecker = modelChecker;
 		this.messenger = messenger;
+		this.guiModels = guiModels;
 	}
 
-	public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query) {
+	
+	public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, pipe.dataLayer.TAPNQuery dataLayerQuery) {
 		this.model = model;
 		this.options = options;
 		this.query = query;
+		this.dataLayerQuery = dataLayerQuery;
 		execute();
 	}
 
 	@Override
 	protected VerificationResult<TAPNNetworkTrace> doInBackground() throws Exception {
-		TAPNComposer composer = new TAPNComposer(messenger);
+		ITAPNComposer composer = new TAPNComposer(messenger);
 		Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(model);
+		
+		if (options.enableOverApproximation())
+		{
+			OverApproximation overaprx = new OverApproximation();
+			overaprx.modifyTAPN(transformedModel.value1(), options.approximationDenominator());
+		}
+		else if (options.enableUnderApproximation())
+		{
+			UnderApproximation underaprx = new UnderApproximation();
+			underaprx.modifyTAPN(transformedModel.value1(), options.approximationDenominator());
+		}
 
 		TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), query.getExtraTokens());
 		MapQueryToNewNames(clonedQuery, transformedModel.value2());
-		
+
 		if(options.useOverApproximation() &&
 				(query.queryType() == QueryType.EF || query.queryType() == QueryType.AG) &&
 				!query.hasDeadlock() && !(options instanceof VerifyPNOptions)){
@@ -65,10 +99,12 @@
 				// Skip over-approximation if model is not supported.
 				// Prevents verification from displaying error.
 			}
+
+
 			if(!verifypn.setup()){
 				messenger.displayInfoMessage("Over-approximation check is skipped because VerifyPN is not available.", "VerifyPN unavailable");
 			}else{
-				VerificationResult<TimedArcPetriNetTrace> overapprox_result = verifypn.verify(new VerifyPNOptions(options.extraTokens(), options.traceOption(), SearchOption.OVERAPPROXIMATE, true, ModelReduction.AGGRESSIVE), transformedModel, clonedQuery);
+				VerificationResult<TimedArcPetriNetTrace> overapprox_result = verifypn.verify(new VerifyPNOptions(options.extraTokens(), options.traceOption(), SearchOption.OVERAPPROXIMATE, true, ModelReduction.AGGRESSIVE, options.enableOverApproximation(), options.enableUnderApproximation(), options.approximationDenominator()), transformedModel, clonedQuery);
 				if(!overapprox_result.error() && (
 						(query.queryType() == QueryType.EF && !overapprox_result.getQueryResult().isQuerySatisfied()) ||
 						(query.queryType() == QueryType.AG && overapprox_result.getQueryResult().isQuerySatisfied()))
@@ -83,26 +119,19 @@
 				}
 			}
 		}
+		
+		ApproximationWorker worker = new ApproximationWorker();
+		
+		return worker.normalWorker(options, modelChecker, transformedModel, composer, clonedQuery, this, model);
+	}
+	
+	private void renameTraceTransitions(TimedArcPetriNetTrace trace) {
+		if (trace != null){
+			trace.reduceTraceForOriginalNet("_traceNet_", "PTRACE");
+			trace.removeTokens("PBLOCK");
+		}
+	}
 
-		VerificationResult<TimedArcPetriNetTrace> result = modelChecker.verify(options, transformedModel, clonedQuery);
-		if (isCancelled()) {
-			firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
-		}
-		if (result.error()) {
-			return new VerificationResult<TAPNNetworkTrace>(result.errorMessage(), result.verificationTime());
-		} else {
-			VerificationResult<TAPNNetworkTrace> value =  new VerificationResult<TAPNNetworkTrace>(
-					result.getQueryResult(),
-					decomposeTrace(result.getTrace(), transformedModel.value2()),
-					decomposeTrace(result.getSecondaryTrace(), transformedModel.value2()),
-					result.verificationTime(),
-					result.stats(),
-					result.isOverApproximationResult());
-			value.setNameMapping(transformedModel.value2());
-			return value;
-		}		
-	}
-	
 	protected int kBound(){
 		return model.marking().size() + query.getExtraTokens();
 	}

=== modified file 'src/pipe/gui/Verifier.java'
--- src/pipe/gui/Verifier.java	2014-02-25 10:13:00 +0000
+++ src/pipe/gui/Verifier.java	2014-05-28 18:52:41 +0000
@@ -1,11 +1,15 @@
 package pipe.gui;
 
+import java.util.HashMap;
+
 import javax.swing.JOptionPane;
 import javax.swing.JSpinner;
 
+import pipe.dataLayer.DataLayer;
 import pipe.dataLayer.TAPNQuery;
 import pipe.gui.widgets.RunningVerificationDialog;
 import dk.aau.cs.TCTL.TCTLAbstractProperty;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 import dk.aau.cs.translations.ReductionOption;
 import dk.aau.cs.util.VerificationCallback;
@@ -103,7 +107,7 @@
 
 		TCTLAbstractProperty inputQuery = input.getProperty();
 
-		VerifytaOptions verifytaOptions = new VerifytaOptions(input.getTraceOption(), input.getSearchOption(), untimedTrace, input.getReductionOption(), input.useSymmetry(), input.useOverApproximation());
+		VerifytaOptions verifytaOptions = new VerifytaOptions(input.getTraceOption(), input.getSearchOption(), untimedTrace, input.getReductionOption(), input.useSymmetry(), input.useOverApproximation(), input.isOverApproximationEnabled(), input.isUnderApproximationEnabled(), input.approximationDenominator());
 
 		if (inputQuery == null) {
 			return;
@@ -113,7 +117,7 @@
 			RunVerificationBase thread = new RunVerification(verifyta, new UppaalIconSelector(), new MessengerImpl());
 			RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());
 			dialog.setupListeners(thread);
-			thread.execute(verifytaOptions, timedArcPetriNetNetwork, new dk.aau.cs.model.tapn.TAPNQuery(input.getProperty(), input.getCapacity()));
+			thread.execute(verifytaOptions, timedArcPetriNetNetwork, new dk.aau.cs.model.tapn.TAPNQuery(input.getProperty(), input.getCapacity()), null);
 			dialog.setVisible(true);
 		} else {
 			JOptionPane.showMessageDialog(CreateGui.getApp(),
@@ -127,8 +131,12 @@
 	public static void runVerifyTAPNVerification(TimedArcPetriNetNetwork tapnNetwork, TAPNQuery query) {
 		runVerifyTAPNVerification(tapnNetwork, query, null);		
 	}
-
+	
 	public static void runVerifyTAPNVerification(TimedArcPetriNetNetwork tapnNetwork, TAPNQuery query, VerificationCallback callback) {
+		runVerifyTAPNVerification(tapnNetwork, query, callback, null);
+	}
+
+	public static void runVerifyTAPNVerification(TimedArcPetriNetNetwork tapnNetwork, TAPNQuery query, VerificationCallback callback, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
 		ModelChecker verifytapn = getModelChecker(query);
 
 		if (!verifytapn.isCorrectVersion()) {
@@ -144,11 +152,11 @@
 		
 		VerifyTAPNOptions verifytapnOptions;
 		if(query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification){
-			verifytapnOptions = new VerifyDTAPNOptions(bound, query.getTraceOption(), query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), query.useOverApproximation(), query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode());
+			verifytapnOptions = new VerifyDTAPNOptions(bound, query.getTraceOption(), query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), query.useOverApproximation(), query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 		} else if(query.getReductionOption() == ReductionOption.VerifyPN){
-			verifytapnOptions = new VerifyPNOptions(bound, query.getTraceOption(), query.getSearchOption(), query.useOverApproximation(), query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION);
+			verifytapnOptions = new VerifyPNOptions(bound, query.getTraceOption(), query.getSearchOption(), query.useOverApproximation(), query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 		} else {
-			verifytapnOptions = new VerifyTAPNOptions(bound, query.getTraceOption(), query.getSearchOption(), query.useSymmetry(), query.useOverApproximation(), query.discreteInclusion(), query.inclusionPlaces());
+			verifytapnOptions = new VerifyTAPNOptions(bound, query.getTraceOption(), query.getSearchOption(), query.useSymmetry(), query.useOverApproximation(), query.discreteInclusion(), query.inclusionPlaces(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 		}
 		
 		if (inputQuery == null) {
@@ -156,10 +164,10 @@
 		}
 		
 		if (tapnNetwork != null) {
-			RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
+			RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, guiModels);
 			RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp());
 			dialog.setupListeners(thread);
-			thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound));
+			thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);
 			dialog.setVisible(true);
 		} else {
 			JOptionPane.showMessageDialog(CreateGui.getApp(),

=== modified file 'src/pipe/gui/graphicElements/Arc.java'
--- src/pipe/gui/graphicElements/Arc.java	2012-08-14 20:39:56 +0000
+++ src/pipe/gui/graphicElements/Arc.java	2014-05-28 18:52:41 +0000
@@ -202,6 +202,10 @@
 	public ArcPath getArcPath() {
 		return myPath;
 	}
+	
+	public void setArcPath(ArcPath newPath) {
+		myPath = newPath;
+	}
 
 	@Override
 	public boolean contains(int x, int y) {

=== modified file 'src/pipe/gui/widgets/InclusionPlaces.java'
--- src/pipe/gui/widgets/InclusionPlaces.java	2011-06-28 16:30:37 +0000
+++ src/pipe/gui/widgets/InclusionPlaces.java	2014-05-28 18:52:41 +0000
@@ -31,4 +31,19 @@
 	public void removePlace(TimedPlace place) {
 		inclusionPlaces.remove(place);
 	}
+	
+	/**
+	 * Perform a deep copy of the object and return it
+	 * 
+	 * @return
+	 */
+	public InclusionPlaces copy() {
+		InclusionPlaces copy = new InclusionPlaces();
+		copy.inclusionOption = (this.inclusionOption == InclusionPlacesOption.AllPlaces) ? InclusionPlacesOption.AllPlaces : InclusionPlacesOption.UserSpecified;
+		for (TimedPlace place : this.inclusionPlaces) {
+			copy.inclusionPlaces.add(place.copy());
+		}
+		
+		return copy;
+	}
 }

=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2014-03-17 22:10:21 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2014-05-28 18:52:41 +0000
@@ -19,11 +19,14 @@
 import java.awt.event.MouseAdapter;
 import java.awt.event.MouseEvent;
 import java.awt.event.MouseListener;
+import java.io.ByteArrayInputStream;
+import java.io.ByteArrayOutputStream;
 import java.io.File;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collections;
 import java.util.Comparator;
+import java.util.HashMap;
 import java.util.Vector;
 
 import javax.swing.BorderFactory;
@@ -62,12 +65,18 @@
 import javax.swing.undo.UndoableEdit;
 import javax.swing.undo.UndoableEditSupport;
 
+import pipe.dataLayer.DataLayer;
+import pipe.dataLayer.PNMLWriter;
 import pipe.dataLayer.TAPNQuery;
+import pipe.dataLayer.Template;
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.gui.CreateGui;
+import pipe.gui.FileFinder;
+import pipe.gui.FileFinderImpl;
 import pipe.gui.MessengerImpl;
 import pipe.gui.Verifier;
+import pipe.gui.Zoomer;
 import dk.aau.cs.TCTL.StringPosition;
 import dk.aau.cs.TCTL.TCTLAFNode;
 import dk.aau.cs.TCTL.TCTLAGNode;
@@ -91,6 +100,12 @@
 import dk.aau.cs.TCTL.visitors.HasDeadlockVisitor;
 import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor;
 import dk.aau.cs.TCTL.visitors.VerifyPlaceNamesVisitor;
+import dk.aau.cs.approximation.OverApproximation;
+import dk.aau.cs.approximation.UnderApproximation;
+import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.io.TimedArcPetriNetNetworkWriter;
+import dk.aau.cs.model.tapn.Constant;
+import dk.aau.cs.model.tapn.ConstantStore;
 import dk.aau.cs.model.tapn.SharedPlace;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
@@ -99,8 +114,10 @@
 import dk.aau.cs.util.Tuple;
 import dk.aau.cs.util.UnsupportedModelException;
 import dk.aau.cs.util.UnsupportedQueryException;
+import dk.aau.cs.verification.ITAPNComposer;
 import dk.aau.cs.verification.NameMapping;
 import dk.aau.cs.verification.TAPNComposer;
+import dk.aau.cs.verification.TAPNComposerWithGUI;
 import dk.aau.cs.verification.UPPAAL.UppaalExporter;
 import dk.aau.cs.verification.VerifyTAPN.ModelReduction;
 import dk.aau.cs.verification.VerifyTAPN.VerifyPNExporter;
@@ -115,7 +132,8 @@
 	private static final String EXPORT_UPPAAL_BTN_TEXT = "Export UPPAAL XML";
 	private static final String EXPORT_VERIFYTAPN_BTN_TEXT = "Export TAPAAL XML";
 	private static final String EXPORT_VERIFYPN_BTN_TEXT = "Export PN XML";
-
+	private static final String EXPORT_COMPOSED_BTN_TEXT = "Open composed net";
+	
 	private static final String UPPAAL_SOME_TRACE_STRING = "Some trace       ";
 	private static final String VERIFYTAPN_SOME_TRACE_STRING = "Some trace       ";
 	private static final String SHARED = "Shared";
@@ -204,18 +222,28 @@
 	private JCheckBox useGCD;
 	private JCheckBox useOverApproximation;
 	private JCheckBox useReduction;
-
+	
+	// Approximation options panel
+	private JPanel overApproximationOptionsPanel;
+	private ButtonGroup approximationRadioButtonGroup;
+	private JRadioButton noApproximationEnable;
+	private JRadioButton overApproximationEnable;
+	private JRadioButton underApproximationEnable;
+	private CustomJSpinner overApproximationDenominator;
+	
 	// Buttons in the bottom of the dialogue
 	private JPanel buttonPanel;
 	private JButton cancelButton;
 	private JButton saveButton;
 	private JButton saveAndVerifyButton;
 	private JButton saveUppaalXMLButton;
+	private JButton openComposedNetButton;
 
 	// Private Members
 	private StringPosition currentSelection = null;
 
 	private final TimedArcPetriNetNetwork tapnNetwork;
+	private final HashMap<TimedArcPetriNet, DataLayer> guiModels;
 	private QueryConstructionUndoManager undoManager;
 	private UndoableEditSupport undoSupport;
 	private boolean isNetDegree2;
@@ -313,12 +341,20 @@
 	private final static String TOOL_TIP_SAVE_AND_VERIFY_BUTTON = "Save and verify the query.";
 	private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";
 	private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";
+	private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
 	private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
 	private final static String TOOL_TIP_SAVE_PN_BUTTON = "Export an xml file that can be used as input for the untimed Petri net engine.";
-
+	
+	//Tool tips for approximation panel
+	private final static String TOOL_TIP_APPROXIMATION_METHOD_NONE = "No approximation method is used.";
+	private final static String TOOL_TIP_APPROXIMATION_METHOD_OVER = "Approximate by dividing all intervals with the approximation constant and enlarging the intervals.";
+	private final static String TOOL_TIP_APPROXIMATION_METHOD_UNDER = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";
+	private final static String TOOL_TIP_APPROXIMATION_CONSTANT = "Choose approximation constant";
+	
 	public QueryDialog(EscapableDialog me, QueryDialogueOption option,
-			TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork) {
+			TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
 		this.tapnNetwork = tapnNetwork;
+		this.guiModels = guiModels;
 		inclusionPlaces = queryToCreateFrom == null ? new InclusionPlaces() : queryToCreateFrom.inclusionPlaces();
 		newProperty = queryToCreateFrom == null ? new TCTLPathPlaceHolder() : queryToCreateFrom.getProperty();
 		rootPane = me.getRootPane();
@@ -365,8 +401,9 @@
 		boolean gcd = useGCD.isSelected();
 		boolean overApproximation = useOverApproximation.isSelected();
 		boolean reduction = useReduction.isSelected();
+
+		TAPNQuery query = new TAPNQuery(name, capacity, newProperty.copy(), traceOption, searchOption, reductionOptionToSet, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, /* hashTableSizeToSet */ null, /* extrapolationOptionToSet */null, inclusionPlaces, overApproximationEnable.isSelected(), underApproximationEnable.isSelected(), (Integer) overApproximationDenominator.getValue());
 		
-		TAPNQuery query = new TAPNQuery(name, capacity, newProperty.copy(), traceOption, searchOption, reductionOptionToSet, symmetry, gcd, timeDarts, pTrie, overApproximation, reduction, /* hashTableSizeToSet */ null, /* extrapolationOptionToSet */null, inclusionPlaces);
 		if(reductionOptionToSet.equals(ReductionOption.VerifyTAPN)){
 			query.setDiscreteInclusion(discreteInclusion.isSelected());
 		}
@@ -507,7 +544,13 @@
 		return new HasDeadlockVisitor().hasDeadLock(newProperty);
 	}
 
-	public static TAPNQuery showQueryDialogue(QueryDialogueOption option, TAPNQuery queryToRepresent, TimedArcPetriNetNetwork tapnNetwork) {
+	public static TAPNQuery showQueryDialogue(QueryDialogueOption option, TAPNQuery queryToRepresent, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels) {
+		if(CreateGui.getCurrentTab().network().hasWeights() && !CreateGui.getCurrentTab().network().isNonStrict()){
+			JOptionPane.showMessageDialog(CreateGui.getApp(),
+					"No reduction option supports both strict intervals and weigthed arcs", 
+					"No reduction option", JOptionPane.ERROR_MESSAGE);
+			return null;
+		}
 		guiDialog = new EscapableDialog(CreateGui.getApp(),	"Edit Query", true);
 
 		Container contentPane = guiDialog.getContentPane();
@@ -517,7 +560,7 @@
 		contentPane.setLayout(new GridBagLayout());
 
 		// 2 Add query editor
-		QueryDialog queryDialogue = new QueryDialog(guiDialog, option, queryToRepresent, tapnNetwork);
+		QueryDialog queryDialogue = new QueryDialog(guiDialog, option, queryToRepresent, tapnNetwork, guiModels);
 		contentPane.add(queryDialogue);
 
 		guiDialog.setResizable(false);
@@ -624,10 +667,12 @@
 			existsDiamond.setSelected(true);
 		} else if (currentSelection.getObject() instanceof TCTLEGNode) {
 			existsBox.setSelected(true);
+			noApproximationEnable.setSelected(true);
 		} else if (currentSelection.getObject() instanceof TCTLAGNode) {
 			forAllBox.setSelected(true);
 		} else if (currentSelection.getObject() instanceof TCTLAFNode) {
 			forAllDiamond.setSelected(true);
+			noApproximationEnable.setSelected(true);
 		}
 	}
 
@@ -669,10 +714,12 @@
 			saveButton.setEnabled(isQueryOk);
 			saveAndVerifyButton.setEnabled(isQueryOk);
 			saveUppaalXMLButton.setEnabled(isQueryOk);
+			openComposedNetButton.setEnabled(isQueryOk);
 		} else {
 			saveButton.setEnabled(false);
 			saveAndVerifyButton.setEnabled(false);
 			saveUppaalXMLButton.setEnabled(false);
+			openComposedNetButton.setEnabled(false);
 		}
 	}
 
@@ -948,6 +995,7 @@
 		initQueryPanel();
 		initUppaalOptionsPanel();
 		initReductionOptionsPanel();
+		initOverApproximationPanel();
 		initButtonPanel(option);
 
 		if(queryToCreateFrom != null)
@@ -976,6 +1024,20 @@
 		setupSearchOptionsFromQuery(queryToCreateFrom);		
 		setupReductionOptionsFromQuery(queryToCreateFrom);
 		setupTraceOptionsFromQuery(queryToCreateFrom);
+		setupApproximationOptionsFromQuery(queryToCreateFrom);
+	}
+	
+	private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {
+		if (queryToCreateFrom.isOverApproximationEnabled())
+			overApproximationEnable.setSelected(true);
+		else if (queryToCreateFrom.isUnderApproximationEnabled())
+			underApproximationEnable.setSelected(true);
+		else
+			noApproximationEnable.setSelected(true);
+		
+		if (queryToCreateFrom.approximationDenominator() > 0) {
+			overApproximationDenominator.setValue(queryToCreateFrom.approximationDenominator());
+		}
 	}
 
 	private void setupReductionOptionsFromQuery(TAPNQuery queryToCreateFrom) {
@@ -1045,8 +1107,10 @@
 			existsDiamond.setSelected(true);
 		} else if (queryToCreateFrom.getProperty() instanceof TCTLEGNode) {
 			existsBox.setSelected(true);
+			noApproximationEnable.setSelected(true);
 		} else if (queryToCreateFrom.getProperty() instanceof TCTLAFNode) {
 			forAllDiamond.setSelected(true);
+			noApproximationEnable.setSelected(true);
 		} else if (queryToCreateFrom.getProperty() instanceof TCTLAGNode) {
 			forAllBox.setSelected(true);
 		}
@@ -1185,7 +1249,9 @@
 		searchOptionsPanel.setVisible(advancedView);
 		reductionOptionsPanel.setVisible(advancedView);
 		saveUppaalXMLButton.setVisible(advancedView);
-
+		openComposedNetButton.setVisible(advancedView);
+		overApproximationOptionsPanel.setVisible(advancedView);
+		
 		if(advancedView){
 			advancedButton.setText("Simple view");
 			advancedButton.setToolTipText(TOOL_TIP_SIMPLE_VIEW_BUTTON);
@@ -1206,10 +1272,10 @@
 		boundednessCheckPanel.setLayout(new BoxLayout(boundednessCheckPanel, BoxLayout.X_AXIS));
 		boundednessCheckPanel.add(new JLabel(" Number of extra tokens:  "));
 
-		numberOfExtraTokensInNet = new CustomJSpinner(3, 0, Integer.MAX_VALUE);	
-		numberOfExtraTokensInNet.setMaximumSize(new Dimension(55, 30));
-		numberOfExtraTokensInNet.setMinimumSize(new Dimension(55, 30));
-		numberOfExtraTokensInNet.setPreferredSize(new Dimension(55, 30));
+		numberOfExtraTokensInNet = new CustomJSpinner(4, 0, Integer.MAX_VALUE);	
+		numberOfExtraTokensInNet.setMaximumSize(new Dimension(65, 30));
+		numberOfExtraTokensInNet.setMinimumSize(new Dimension(65, 30));
+		numberOfExtraTokensInNet.setPreferredSize(new Dimension(65, 30));
 		numberOfExtraTokensInNet.setToolTipText(TOOL_TIP_NUMBEROFEXTRATOKENSINNET);
 		boundednessCheckPanel.add(numberOfExtraTokensInNet);
 
@@ -1338,6 +1404,7 @@
 		quantificationPanel = new JPanel(new GridBagLayout());
 		quantificationPanel.setBorder(BorderFactory.createTitledBorder("Quantification"));
 		quantificationRadioButtonGroup = new ButtonGroup();
+		approximationRadioButtonGroup = new ButtonGroup();
 
 		existsDiamond = new JRadioButton("(EF) There exists some reachable marking that satisifies:");
 		existsBox = new JRadioButton("(EG) There exists a trace on which every marking satisfies:");
@@ -2073,6 +2140,62 @@
 		uppaalOptionsPanel.add(traceOptionsPanel, gridBagConstraints);
 
 	}
+	
+	
+	
+	
+	
+	private void initOverApproximationPanel() {
+		overApproximationOptionsPanel = new JPanel(new GridBagLayout());
+		overApproximationOptionsPanel.setVisible(false);
+		overApproximationOptionsPanel.setBorder(BorderFactory.createTitledBorder("Approximation Options"));
+		approximationRadioButtonGroup = new ButtonGroup();
+		
+		noApproximationEnable = new JRadioButton("Exact analysis");
+		noApproximationEnable.setVisible(true);
+		noApproximationEnable.setSelected(true);
+		noApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_NONE);
+		
+		overApproximationEnable = new JRadioButton("Over-approximation");
+		overApproximationEnable.setVisible(true);
+		overApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_OVER);
+		
+		underApproximationEnable = new JRadioButton("Under-approximation");
+		underApproximationEnable.setVisible(true);
+		underApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_UNDER);
+
+		approximationRadioButtonGroup.add(noApproximationEnable);
+		approximationRadioButtonGroup.add(overApproximationEnable);
+		approximationRadioButtonGroup.add(underApproximationEnable);
+		
+		GridBagConstraints gridBagConstraints = new GridBagConstraints();
+		gridBagConstraints.gridy = 0;
+		gridBagConstraints.weightx = 1;
+		gridBagConstraints.anchor = GridBagConstraints.WEST;
+		
+		JLabel approximationDenominatorLabel = new JLabel("Approximation constant: ");	
+		
+		overApproximationDenominator = new CustomJSpinner(2, 2, Integer.MAX_VALUE);	
+		overApproximationDenominator.setMaximumSize(new Dimension(65, 30));
+		overApproximationDenominator.setMinimumSize(new Dimension(65, 30));
+		overApproximationDenominator.setPreferredSize(new Dimension(65, 30));
+		overApproximationDenominator.setToolTipText(TOOL_TIP_APPROXIMATION_CONSTANT);
+		
+		overApproximationOptionsPanel.add(noApproximationEnable, gridBagConstraints);
+		overApproximationOptionsPanel.add(overApproximationEnable, gridBagConstraints);
+		overApproximationOptionsPanel.add(underApproximationEnable, gridBagConstraints);
+		overApproximationOptionsPanel.add(approximationDenominatorLabel, gridBagConstraints);
+		overApproximationOptionsPanel.add(overApproximationDenominator);
+	
+		gridBagConstraints = new GridBagConstraints();
+		gridBagConstraints.gridx = 0;
+		gridBagConstraints.gridy = 5;
+		gridBagConstraints.anchor = GridBagConstraints.WEST;
+		gridBagConstraints.insets = new Insets(5,10,5,10);
+		gridBagConstraints.fill = GridBagConstraints.HORIZONTAL;
+		
+		add(overApproximationOptionsPanel, gridBagConstraints);
+	}
 
 	private void initReductionOptionsPanel() {
 		reductionOptionsPanel = new JPanel(new GridBagLayout());
@@ -2201,7 +2324,7 @@
 		gbc.insets = new Insets(0,5,0,5);
 		reductionOptionsPanel.add(usePTrie, gbc);
 
-		useOverApproximation = new JCheckBox("Use over-approximation check");
+		useOverApproximation = new JCheckBox("Use untimed state-equations check");
 		useOverApproximation.setSelected(true);
 		useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
 
@@ -2293,6 +2416,11 @@
 			useOverApproximation.setVisible(true);
 			useOverApproximation.setSelected(false);
 			useOverApproximation.setEnabled(false);
+			
+			/*noApproximationEnable.setEnabled(false);
+			overApproximationEnable.setEnabled(false);
+			underApproximationEnable.setEnabled(false);
+			overApproximationDenominator.setEnabled(false);*/
 		}
 		else{
 			useOverApproximation.setVisible(true);
@@ -2300,6 +2428,11 @@
 				useOverApproximation.setSelected(true);
 			}
 			useOverApproximation.setEnabled(true);
+					
+			noApproximationEnable.setEnabled(true);
+			overApproximationEnable.setEnabled(true);
+			underApproximationEnable.setEnabled(true);
+			overApproximationDenominator.setEnabled(true);
 		}
 	}
 
@@ -2340,22 +2473,28 @@
 		refreshOverApproximationOption();
 	}
 
+	
 	private void initButtonPanel(QueryDialogueOption option) {
 		buttonPanel = new JPanel(new BorderLayout());
 		if (option == QueryDialogueOption.Save) {
 			saveButton = new JButton("Save");
 			saveAndVerifyButton = new JButton("Save and Verify");
 			cancelButton = new JButton("Cancel");
+			
+			openComposedNetButton = new JButton(EXPORT_COMPOSED_BTN_TEXT);
+			openComposedNetButton.setVisible(false);
+			
 			saveUppaalXMLButton = new JButton(EXPORT_UPPAAL_BTN_TEXT);
 			//Only show in advanced mode
 			saveUppaalXMLButton.setVisible(false);
-
+			
 			//Add tool tips
 			saveButton.setToolTipText(TOOL_TIP_SAVE_BUTTON);
 			saveAndVerifyButton.setToolTipText(TOOL_TIP_SAVE_AND_VERIFY_BUTTON);
 			cancelButton.setToolTipText(TOOL_TIP_CANCEL_BUTTON);
 			saveUppaalXMLButton.setToolTipText(TOOL_TIP_SAVE_UPPAAL_BUTTON);
-
+			openComposedNetButton.setToolTipText(TOOL_TIP_SAVE_COMPOSED_BUTTON);
+			
 			saveButton.addActionListener(new ActionListener() {
 				public void actionPerformed(ActionEvent evt) {
 					// TODO make save 
@@ -2378,7 +2517,7 @@
 						TAPNQuery query = getQuery();
 
 						if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
-							Verifier.runVerifyTAPNVerification(tapnNetwork, query);
+							Verifier.runVerifyTAPNVerification(tapnNetwork, query, null, guiModels);
 						else
 							Verifier.runUppaalVerification(tapnNetwork, query);
 					}}
@@ -2412,8 +2551,19 @@
 					}
 
 					if (xmlFile != null && queryFile != null) {
-						TAPNComposer composer = new TAPNComposer(new MessengerImpl());
+						ITAPNComposer composer = new TAPNComposer(new MessengerImpl());
 						Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(QueryDialog.this.tapnNetwork);
+						
+						if (overApproximationEnable.isSelected())
+						{
+							OverApproximation overaprx = new OverApproximation();
+							overaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator());
+						}
+						else if (underApproximationEnable.isSelected())
+						{
+							UnderApproximation underaprx = new UnderApproximation();
+							underaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator());
+						}						
 
 						TAPNQuery tapnQuery = getQuery();
 						dk.aau.cs.model.tapn.TAPNQuery clonedQuery = new dk.aau.cs.model.tapn.TAPNQuery(tapnQuery.getProperty().copy(), tapnQuery.getCapacity());
@@ -2449,6 +2599,49 @@
 					}
 				}
 			});
+			
+			openComposedNetButton.addActionListener(new ActionListener() {
+				public void actionPerformed(ActionEvent e) {
+					TAPNComposerWithGUI composer = new TAPNComposerWithGUI(new MessengerImpl(), guiModels);
+					Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(tapnNetwork);
+					
+					ArrayList<Template> templates = new ArrayList<Template>(1);
+					querySaved = true;	//Setting this to true will make sure that new values will be used.
+					if (overApproximationEnable.isSelected())
+					{
+						OverApproximation overaprx = new OverApproximation();
+						overaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator());
+					}
+					else if (underApproximationEnable.isSelected())
+					{
+						UnderApproximation underaprx = new UnderApproximation();
+						underaprx.modifyTAPN(transformedModel.value1(), getQuery().approximationDenominator(), ((TAPNComposerWithGUI) composer).getGuiModel());
+					}
+					templates.add(new Template(transformedModel.value1(), ((TAPNComposerWithGUI) composer).getGuiModel(), new Zoomer()));
+					
+					// Create a constant store
+					ConstantStore newConstantStore = new ConstantStore();
+
+					
+					TimedArcPetriNetNetwork network = new TimedArcPetriNetNetwork(newConstantStore);
+					
+					network.add(transformedModel.value1());
+					
+					PNMLWriter tapnWriter = new TimedArcPetriNetNetworkWriter(network, templates, new ArrayList<pipe.dataLayer.TAPNQuery>(0), new ArrayList<Constant>(0));
+			
+					try {
+						ByteArrayOutputStream outputStream = tapnWriter.savePNML();
+						String composedName = "composed-" + CreateGui.getApp().getCurrentTabName();
+						composedName = composedName.replace(".xml", "");
+						CreateGui.getApp().createNewTabFromFile(new ByteArrayInputStream(outputStream.toByteArray()), composedName);
+						exit();
+					} catch (Exception e1) {
+						System.console().printf(e1.getMessage());
+					}
+				}
+			});
+			
+			
 		} else if (option == QueryDialogueOption.Export) {
 			saveButton = new JButton("export");
 			cancelButton = new JButton("Cancel");
@@ -2470,8 +2663,10 @@
 		if (option == QueryDialogueOption.Save) {
 			JPanel leftButtomPanel = new JPanel(new FlowLayout());
 			JPanel rightButtomPanel = new JPanel(new FlowLayout());
+			leftButtomPanel.add(openComposedNetButton, FlowLayout.LEFT);
 			leftButtomPanel.add(saveUppaalXMLButton, FlowLayout.LEFT);
-
+			
+			
 			rightButtomPanel.add(cancelButton);
 
 			rightButtomPanel.add(saveButton);
@@ -2489,7 +2684,7 @@
 
 		GridBagConstraints gridBagConstraints = new GridBagConstraints();
 		gridBagConstraints.gridx = 0;
-		gridBagConstraints.gridy = 5;
+		gridBagConstraints.gridy = 6;
 		gridBagConstraints.anchor = GridBagConstraints.WEST;
 		gridBagConstraints.fill = GridBagConstraints.HORIZONTAL;
 		gridBagConstraints.insets = new Insets(0, 10, 5, 10);

=== modified file 'src/pipe/gui/widgets/QueryPane.java'
--- src/pipe/gui/widgets/QueryPane.java	2013-06-25 20:51:19 +0000
+++ src/pipe/gui/widgets/QueryPane.java	2014-05-28 18:52:41 +0000
@@ -311,7 +311,7 @@
 		addQueryButton.setToolTipText(toolTipNewQuery);
 		addQueryButton.addActionListener(new ActionListener() {
 			public void actionPerformed(ActionEvent e) {
-				TAPNQuery q = QueryDialog.showQueryDialogue(QueryDialogueOption.Save, null, tabContent.network());
+				TAPNQuery q = QueryDialog.showQueryDialogue(QueryDialogueOption.Save, null, tabContent.network(), tabContent.getGuiModels());
 				if (q != null) {
 					undoManager.addNewEdit(new AddQueryCommand(q, tabContent));
 					addQuery(q);
@@ -336,7 +336,7 @@
 		TAPNQuery q = (TAPNQuery) queryList.getSelectedValue();
 		if(q.isActive()) {
 			TAPNQuery newQuery = QueryDialog.showQueryDialogue(
-					QueryDialogueOption.Save, q, tabContent.network());
+					QueryDialogueOption.Save, q, tabContent.network(), tabContent.getGuiModels());
 
 			if (newQuery != null)
 				updateQuery(q, newQuery);
@@ -411,7 +411,7 @@
 		TAPNQuery query = (TAPNQuery) queryList.getSelectedValue();
 
 		if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
-			Verifier.runVerifyTAPNVerification(tabContent.network(), query);
+			Verifier.runVerifyTAPNVerification(tabContent.network(), query, null, this.tabContent.getGuiModels());
 		else
 			Verifier.runUppaalVerification(tabContent.network(), query);
 	}

=== modified file 'src/resources/Images/Ask a question.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/Report bug.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/icon.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/info.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/maybe.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/maybe1.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/notsatisfied.png' (properties changed: +x to -x)
=== modified file 'src/resources/Images/satisfied.png' (properties changed: +x to -x)