diff --git a/tlatools/.classpath b/tlatools/.classpath
index 291e0fbfbba1d9cf4b93def65b357039d1bc9269..5df2c0e31ace0682e9abd3d638adafa4534c24fa 100644
--- a/tlatools/.classpath
+++ b/tlatools/.classpath
@@ -7,6 +7,8 @@
 	<classpathentry kind="src" path="test"/>
 	<classpathentry kind="src" path="test-long"/>
 	<classpathentry kind="src" path="test-concurrent"/>
+	<classpathentry kind="src" path="test-verify"/>
 	<classpathentry kind="lib" path="lib/javax.mail.jar"/>
+	<classpathentry kind="lib" path="lib/jpf.jar"/>
 	<classpathentry kind="output" path="class"/>
 </classpath>
diff --git a/tlatools/customBuild.xml b/tlatools/customBuild.xml
index e603b3b1a96654d6003b364d4192391e2d8b6339..633a81188e827bdda5b3b55d9babb59e87e7378b 100644
--- a/tlatools/customBuild.xml
+++ b/tlatools/customBuild.xml
@@ -18,9 +18,9 @@
 	</tstamp>
 
 	<!-- JaCoCo code coverage -->
-    <taskdef uri="antlib:org.jacoco.ant" resource="org/jacoco/ant/antlib.xml">
-        <classpath path="lib/jacocoant.jar"/>
-    </taskdef>
+	<taskdef uri="antlib:org.jacoco.ant" resource="org/jacoco/ant/antlib.xml">
+		<classpath path="lib/jacocoant.jar"/>
+	</taskdef>
 
 	<taskdef resource="org/aspectj/tools/ant/taskdefs/aspectjTaskdefs.properties">
 		<classpath>
@@ -91,7 +91,7 @@
 			</fileset>
 		</copy>
 	</target>
-	
+
 	<target name="compile-aj" depends="compile" if="withaj">
 		<echo>
 			====================================================================
@@ -104,7 +104,7 @@
 		<iajc destdir="${class.dir}" sourceRoots="${src-aj.dir}" debug="true" source="1.5" target="1.5">
 			<classpath refid="project.classpath" />
 			<classpath>
-					<pathelement location="lib/aspectjrt-1.8.5.jar" />
+				<pathelement location="lib/aspectjrt-1.8.5.jar" />
 				<pathelement location="lib/aspectjtools-1.8.5.jar" />
 				<pathelement path="${class.dir}" />
 			</classpath>
@@ -135,15 +135,15 @@
 		<!-- The javax.mail dependency as well as javax.activation is also depended upon -->
 		<!-- by the tla2tools OSGi bundle and is expected to be the same version. -->
 		<unzip src="lib/javax.mail.jar" dest="${class.dir}"/>
-		
+
 		<!-- Extract javax.mail to maven classes folder. This script is triggered by -->
 		<!-- maven. However, maven compiles the code again to target/classes from -->
 		<!-- where it creates the plugin -->
 		<unzip src="lib/javax.mail.jar" dest="target/classes"/>
-		
+
 		<!-- TODO: add javax.activation to lib/ and extract it here too. Otherwise we have a -->
 		<!-- runtime dependency on Java 6. -->
-		
+
 		<!-- create a JAR file for the users -->
 		<mkdir dir="${dist.dir}" />
 		<jar destfile="${dist.file}">
@@ -200,7 +200,7 @@
 					<pathelement path="${test.class.dir}" />
 				</classpath>
 				<formatter type="xml" />
-	
+
 				<!-- Pass the base path of the tlatools project to unit tests in case they need it to locate TLA+ specs or configs -->
 				<sysproperty key="basedir" value="${basedir}/"/>
 				<batchtest fork="yes" todir="${test.reports}">
@@ -311,7 +311,7 @@
 			<batchtest fork="yes" todir="${test.reports}/onJarLong">
 				<fileset dir="${test.dir}-long">
 					<exclude name="**/MultiThreadedSpecTest.java"/>
-					
+
 					<!-- The following tests take way too long (hours). -->
 					<!-- Reactivate when you start working on the fingerprint sets! -->
 					<exclude name="**/DiskFPSetTest.java"/>
@@ -319,7 +319,7 @@
 					<exclude name="**/MSBDiskFPSetTest.java"/>
 					<exclude name="**/OffHeapDiskFPSetTest.java"/>
 					<exclude name="**/DiskStateQueueTest.java"/>
-					
+
 					<include name="**/*Test*.java" />
 				</fileset>
 			</batchtest>
@@ -329,6 +329,40 @@
 		<delete dir="${ws.class.dir}" deleteonexit="true"/>
 	</target>
 
+	<!-- -->
+	<target name="test-verify" description="Verifies TLC parts with NASA's pathfinder model checker">
+		<!-- Compile our boilerplate code needed to verify TLC. E.g. the StateQueueVerify creates -->
+		<!-- examplary produces & consumers and a dummy implementation of StateQueue. -->
+		<javac srcdir="${test.dir}-verify" destdir="${test.class.dir}" debug="true" verbose="false">
+			<classpath refid="project.classpath" />
+			<classpath>
+				<pathelement path="${class.dir}" />
+				<pathelement location="lib/jpf.jar" />
+			</classpath>
+		</javac>
+
+		<mkdir dir="${test.reports}/verify" />
+		<junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="4096m" forkmode="perTest" fork="yes" 
+			dir="${basedir}/test-verify" >
+			<classpath refid="project.classpath" />
+			<classpath>
+				<pathelement location="lib/junit-4.8.2.jar" />
+				<pathelement location="lib/jpf.jar" />
+				<pathelement location="lib/jpf-classes.jar" />
+				<pathelement path="${class.dir}" />
+				<pathelement path="${test.class.dir}" />
+			</classpath>
+
+			<formatter type="xml" />
+
+			<batchtest fork="yes" todir="${test.reports}/verify">
+				<fileset dir="${test.dir}-verify">
+					<include name="**/*Test*.java" />
+				</fileset>
+			</batchtest>
+		</junit>
+	</target>
+
 	<target name="dist-mixed-jar" description="Build a distribution" depends="default">
 		<!-- create a JAR file for the users -->
 		<jar destfile="${dist-mixed.file.jar}">
diff --git a/tlatools/lib/jpf-classes.jar b/tlatools/lib/jpf-classes.jar
new file mode 100644
index 0000000000000000000000000000000000000000..15a91af503b5aa6c7b016b932c227fb27c68fb76
Binary files /dev/null and b/tlatools/lib/jpf-classes.jar differ
diff --git a/tlatools/lib/jpf.jar b/tlatools/lib/jpf.jar
new file mode 100644
index 0000000000000000000000000000000000000000..28915b7cd4d47aa788cd776e4e1e4542a2263324
Binary files /dev/null and b/tlatools/lib/jpf.jar differ
diff --git a/tlatools/test-verify/README.txt b/tlatools/test-verify/README.txt
new file mode 100644
index 0000000000000000000000000000000000000000..9b796debbc8d6eaffebd0008216e94847b918dd2
--- /dev/null
+++ b/tlatools/test-verify/README.txt
@@ -0,0 +1 @@
+This folder contains code to verify TLC with Java Pathfinder (http://babelfish.arc.nasa.gov/trac/jpf/wiki/WikiStart).
\ No newline at end of file
diff --git a/tlatools/test-verify/jpf.properties b/tlatools/test-verify/jpf.properties
new file mode 100644
index 0000000000000000000000000000000000000000..cf1cbb98c00029aaf7c51ca9ca4d46f24a54f1d8
--- /dev/null
+++ b/tlatools/test-verify/jpf.properties
@@ -0,0 +1,437 @@
+# JPF configuration for "jpf-core" component
+
+# path elements can either be relative to the property file location, or
+# use the JPF component name (e.g. "jpf-core") as a variable prefix
+# (e.g. "jpf-core.sourcepath=${jpf-core}/src/examples").
+# If a jpf.properties is to be used within NB, it has to use the variable prefix
+# (prepending the project root is only done during JPF init)
+
+# we use the ';' separator here because it is recognized by NetBeans (as opposed
+# to ',')
+
+# 'config_path' is set automatically by gov.nasa.jpf.Config during JPF init.
+# If used from within an Ant build system, 'jpf-core' has to be set explicitly
+# (ant does ${..} property expansion, but ignores property redefinition, so the
+# following line will be ignored)
+
+jpf-core = ${config_path}
+
+jpf-core.native_classpath=\
+  ${jpf-core}/../lib/jpf.jar;\
+  ${jpf-core}/../lib/jpf-annotations.jar
+
+jpf-core.classpath=\
+  ${jpf-core}/../lib/jpf-classes.jar
+
+#jpf-core.sourcepath=\
+#  ${jpf-core}/src/examples
+
+#jpf-core.test_classpath=\
+#  ${jpf-core}/build/tests
+
+jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
+
+
+
+# the default jpf-core properties file with keys for which we need mandatory defaults
+
+########################### 0. global part ###############################
+
+# instances that are both search and VM listeners
+#listener = ..
+
+# do we want JPF exceptions to print their stack traces (that's only for
+# debugging)
+jpf.print_exception_stack = true
+
+
+# this is where we can specify additional classpath entries that are
+# not in the system property class.path (e.g. when running JPF from
+# an environment that uses it's own loaders, like Eclipse plugins etc.)
+#jpf.native_classpath = ..
+
+
+########################### 1. Search part ###############################
+search.class = gov.nasa.jpf.search.DFSearch
+
+
+# This flag indicates whether state matching will only be done when a state
+# is revisited at a lower depth. By default this is false. If it is set to
+# true and no error is found in a limited-depth search then it is guaranteed
+# not to have such error below that depth. Note that for traditional
+# depth limited search this does not hold
+search.match_depth = false
+
+# This flag indicates whether JPF should produce more than one error
+# or stop at the first one
+search.multiple_errors = false
+
+# the minimum free memory bounds. If we fall below that threshold, we
+# stop the search
+search.min_free = 1M
+
+# name of the file in which we store error paths. If not set, we don't store
+#search.error_path = error.xml
+
+# the standard properties we want to check for
+search.properties=\
+gov.nasa.jpf.vm.NotDeadlockedProperty,\
+gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
+
+
+# various heuristic parameters
+
+# This number specifies the maximum number of states to keep on the queue
+# during a heuristic search. By default it is set to -1
+search.heuristic.queue_limit = -1
+
+# This flag indicates whether branches with counts less than branch-start
+# are to be ranked according to how many times they have been taken.
+# It is set to true by default. If it is set to false, they are all valued
+# the same
+search.heuristic.branch.count_early = true
+
+# This number determines at what point branches are heuristically valued as worse
+# than non-branching transitions. By default this value is 1.
+branch_start = 1
+
+
+# This number if greater than 0 is returned as the heuristic value for
+# non-branching transitions. By default it is set to -1 in which case the
+# value of branch-start is returned instead
+search.heuristic.branch.no_branch_return = -1
+
+# exclusive search listeners
+# search.listener =
+
+
+############################### 2. VM part ###############################
+
+
+# this is an ordered list of packages from which we try to locate native peers.
+# "<model>" means JPF tries the same package like the model class
+# "<default>" means no package at all
+# (this is going to be extended by jpf.properties files)
+#peer_packages = <model>,<default>
+
+
+vm.class = gov.nasa.jpf.vm.SingleProcessVM
+
+# the ClassLoaderInfo class used for startup
+vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
+
+# class used to hash/store states (if not set, states are not matched)
+vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet
+
+# class used to maintain the backtrack stack
+vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
+
+# serializer to be used by state set (vm.storage.class)
+vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
+#vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer
+#vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer
+
+# the class that models static fields and classes
+vm.statics.class = gov.nasa.jpf.vm.OVStatics
+
+# the class that models the heap
+#vm.heap.class = gov.nasa.jpf.vm.PSIMHeap
+vm.heap.class = gov.nasa.jpf.vm.OVHeap
+
+# the class representing the list of all threads
+vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
+
+# restorer to be used by backtracker such as DefaultBacktracker UNLESS a
+# serializer that is also a restorer (such as CollapsingSerializer) is used.
+# I.e. this is only read if serializer is not used or it's not a StateRestorer
+vm.restorer.class = .vm.DefaultMementoRestorer
+
+# where do we get the standard libraries from?
+# "<system>" is replaced by the host VM sun.boot.class.path setting
+vm.boot_classpath = <system>
+
+# instruction factory
+jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
+
+# fields factory
+vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
+
+# pattern list for assertion enabled/disabled classes
+#vm.enable_assertions = *
+#vm.disable_assertions=
+
+# do we support the Verify.ignorePath() API (to imperatively ignore paths in modeled/instrumented programs)?
+vm.verify.ignore_path = true
+
+
+vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
+vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
+vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
+
+# the following properties can be used to set filters for GenericSharednessPolicy instances
+
+# never break on exposure or shared field access from matching methods.
+# NOTE - this is transitive and hence should only include a minimal set of trusted methods
+vm.shared.never_break_methods=\
+      java.util.concurrent.ThreadPoolExecutor.processWorkerExit,\
+      java.util.concurrent.locks.Abstract*Synchronizer.*,\
+      java.util.concurrent.ThreadPoolExecutor.getTask,\
+      java.util.concurrent.atomic.Atomic*.*,\
+      java.util.concurrent.Exchanger.doExchange,\
+      java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,\
+      java.util.concurrent.TimeUnit.*
+
+vm.shared.never_break_types=\
+      java.util.concurrent.TimeUnit
+
+# never break on shared access of the following fields. While this is less prone to
+# masking defects than never_break_methods, it should also be used sparingly.
+# NOTE - java.lang.Thread* fields should not be excluded if the SUT explicitly uses 
+# Thread or ThreadGroup objects
+vm.shared.never_break_fields=\
+      java.lang.Thread*.*,\
+      java.lang.System.*,\
+      java.lang.Runtime.*,\
+      java.lang.Boolean.*,\
+      java.lang.String.*,\
+      java.lang.*.TYPE,\
+      java.util.HashMap.EMPTY_TABLE,\
+      java.util.HashSet.PRESENT,\
+      java.util.concurrent.ThreadPoolExecutor*.*,\
+      java.util.concurrent.ThreadPoolExecutor*.*,\
+      java.util.concurrent.TimeUnit.*,\
+      java.util.concurrent.Exchanger.CANCEL,\
+      java.util.concurrent.Exchanger.NULL_ITEM,\
+      java.util.concurrent.Executors$DefaultThreadFactory.*,\
+      sun.misc.VM.*,\
+      sun.misc.SharedSecrets.*,\
+      sun.misc.Unsafe.theUnsafe,\
+      gov.nasa.jpf.util.test.TestJPF.*
+
+
+# do we also break transitions on reference field puts that could make the
+# referenced objects shared
+vm.shared.break_on_exposure = true
+
+# do we try to deduce if a field is supposed to be protected by a lock? In this
+# case, we stop to treat this field as a boundary step, but only if we see the lock
+vm.shared.sync_detection = true
+
+# do we assume final fields to be race-safe (not really true, esp. for
+# instance fields with references leaking from a ctor, but a good starting point)
+vm.shared.skip_finals=true
+
+# ClassLoaders synchronize the loading of a class.
+# Thus, static final fields can never be included in a race condition since only 1 thread is allowed to access the class while it is loading.
+# Defaulted to false to maintain backward compatibility in JPF
+vm.shared.skip_static_finals=false
+
+# When an object's constructor has returned, then the final fields can not be changed.
+# Thus, instance final fields can never be included in a race condition (unless the this reference is leaked from a constructor)
+# Defaulted to false to maintain backward compatibility in JPF
+vm.shared.skip_constructed_finals=false
+
+
+# do we ignore explicitly set Thread.UncaughtHandlers
+vm.ignore_uncaught_handler=false
+
+# do we treat returned Thread.UncaughtHandler.uncaughtException() calls as normal thread termination
+vm.pass_uncaught_handler=true
+
+# do we reclaim unused memory (run garbage collection)
+vm.gc = true
+
+# threshold after which number of allocations to perform a garbage collection
+# (even within the same transition, to avoid lots of short living objects)
+# -1 means never
+vm.max_alloc_gc = -1 
+
+# do we run finalizers on collected objects (only makes sense with garbage collection)
+vm.finalize = false
+
+# this is a preemption boundary specifying the max number of instructions after which we
+# break the current transition if there are other runnable threads
+vm.max_transition_length = 50000
+
+# are thread ids of terminated threads with recycled thread objects reused when creating new
+# threads. This is required for programs that sequentially create many short living threads
+vm.reuse_tid = false
+
+# do we want to halt execution on each throw of an exception that matches
+# one of the given classname wildcard patterns w/o looking for exception handlers?
+# (useful for empty handler blocks, over-permissive catches or generally
+# misused exceptions)
+#vm.halt_on_throw = *
+
+# class that is used to create scheduling relevant choice generators.
+# this will replace the scheduler
+vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
+
+# print output as it is generated during the search (for all paths)
+vm.tree_output = true
+
+# collect output inside the stored path (to create program trace outout)
+vm.path_output = false
+
+# do we want to store the whole path no matter if we report them
+vm.store_steps=false
+
+# untracked property
+vm.untracked = true
+
+# from where do we initialize the system properties
+#   SELECTED - keys specified as vm.system.properties, values from host
+#   FILE - Java properties file (key=value pairs)
+#   HOST - all system properties from underlying host VM
+vm.sysprop.source = SELECTED
+
+# pathname of property file with system properties
+#vm.sysprop.file =
+
+# list of key names to load from host VM
+#vm.sysprop.keys =
+
+# class we use to model execution time
+vm.time.class = gov.nasa.jpf.vm.SystemTime
+
+# if this is set to true, we throw an exception if we encounter any orphan native peer methods
+vm.no_orphan_methods = false
+
+# if this is set to true, overriden finalize() methods execute upon objects garbage collections
+vm.process_finalizers = false
+
+
+### jvm specifics
+
+# di=o we model nested locks during class init (to detect possible hotspot dealocks during init)
+# (off by default since it can cause state explosion)
+jvm.nested_init=false
+
+# if so, for which classes (default is to exclude system classes)
+jvm.nested_init.exclude=java.*,javax.*,sun.misc.*
+
+
+############################### 3. CG part ###############################
+
+# choice randomization policy in effect:
+#   "NONE" - choice sets are not randomized
+#   "FIXED_SEED" - choice sets are randomized using a fixed seed for each JPF run (reproducible)
+#   "VAR_SEED" - choice sets are randomized using a variable seed for each JPF run
+cg.randomize_choices = NONE
+
+# the standard seed value used for the FIXED_SEED policy
+cg.seed = 42
+
+
+# if this is set, we create choice generators even if there is only a single
+# choice. This is to ensure state storage/matching at all locations where a
+# choice generator *could* be created. The default should be to turn it off though,
+# since this can produce a lot of additional states (esp. with threads)
+cg.break_single_choice = false
+
+
+# default BooleanChoiceGenerator sequence: do we start with 'false'
+cg.boolean.false_first = true
+
+# do we want java.util.Random. nextXX() enumerate choices, or just return a single value?
+# (isn't implemented for all types yet)
+cg.enumerate_random=false
+
+# maximum number of processors returned by Runtime.availableProcessors(). If this is
+# greater than 1, the call represents a ChoiceGenerator
+cg.max_processors=1
+
+# creates a CG upon Thread.start, i.e. breaks the starting transition. Note this is
+# required for data race detection (which depends on detecting access of shared objects)
+cg.threads.break_start=true
+
+# if this option is set we break the transition on Thread.yield()
+cg.threads.break_yield=true
+
+# if this option is set we break the transition on Thread.sleep()
+cg.threads.break_sleep=true
+
+# set if we shold also break on array instructions, e.g. to detect races
+# for array elements. This is off by default because it can cause serious
+# state explosion
+cg.threads.break_arrays=false
+
+# do we support atomic sections. If set to false, Verify.beginAtomic()/endAtomic()
+# will not do anything
+cg.enable_atomic=true
+
+############################### 3. Report Part ###############################
+log.handler.class=gov.nasa.jpf.util.LogHandler
+
+# Windows seem to have a different default
+log.level=warning
+
+report.class=gov.nasa.jpf.report.Reporter
+report.publisher=console
+
+report.console.class=gov.nasa.jpf.report.ConsolePublisher
+
+# this prints out repository information if the 'jpf' topic is set (for debugging)
+#jpf.report.show_repository=true
+
+#property violation reporting is configured separately
+report.console.start=jpf,sut
+
+report.console.transition=
+report.console.constraint=constraint,snapshot
+
+report.console.probe=statistics
+
+report.console.property_violation=error,snapshot
+report.console.show_steps=true
+report.console.show_method=true
+report.console.show_code=false
+
+report.console.finished=result,statistics
+
+#jpf.report.console.show_steps=true
+#jpf.report.console.show_method=true
+#jpf.report.console.show_code=true
+
+report.xml.class=gov.nasa.jpf.report.XMLPublisher
+
+report.html.class=gov.nasa.jpf.report.HTMLPublisher
+report.html.start=jpf,sut,platform,user,dtg,config
+report.html.constraint=constraint
+report.html.property_violation=
+report.html.finished=result,statistics,error,snapshot,output
+
+
+############################### 4. Listener part #############################
+
+# imperative list of listeners
+#listener=
+
+listener.autoload=\
+  gov.nasa.jpf.NonNull,\
+  gov.nasa.jpf.Const
+
+listener.gov.nasa.jpf.NonNull=gov.nasa.jpf.tools.NonNullChecker
+listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker
+
+
+### PreciseRaceDetector
+
+# we don't check for races in standard libraries
+race.exclude=java.*,javax.*
+
+
+############################### 5. test part #############################
+
+test.report.console.finished=result
+
+###
+### Include both directories created by customBuild.xml as classpath
+### elements. ../class contains the TLC code, ../test-class contains
+### TLC's test code. It's relative to this file jpf.properties to
+### support running the tests from any directory (e.g. via the Eclipse
+### launcher as well as customBuild.xml).
+###
++classpath=${config_path}/../class/;\
+		   ${config_path}/../test-class/
+
diff --git a/tlatools/test-verify/tlc2/tool/queue/StateQueueJPFTest.java b/tlatools/test-verify/tlc2/tool/queue/StateQueueJPFTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..ea4bc80a8bf128715696af493ac21d00eedd1312
--- /dev/null
+++ b/tlatools/test-verify/tlc2/tool/queue/StateQueueJPFTest.java
@@ -0,0 +1,100 @@
+/*******************************************************************************
+ * Copyright (c) 2015 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+
+package tlc2.tool.queue;
+
+import java.io.IOException;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import tlc2.tool.TLCState;
+
+public class StateQueueJPFTest extends TestJPF {
+
+	@Test
+	public void test() {
+		if (verifyNoPropertyViolation()) {
+			final StateQueue queue = new DummyStateQueue();
+			final TLCState tlcState = new DummyTLCState();
+			queue.enqueue(tlcState);
+			
+			Thread main = new Thread(new Runnable() {
+				public void run() {
+					queue.suspendAll();
+					// critical section (taking a checkpoint)
+					queue.resumeAll();
+				}
+			}, "Main");
+			main.start();
+			
+			Thread worker = new Thread(new Runnable() {
+				public void run() {
+					for (int i = 0; i < 10; i++) {
+						TLCState state = queue.dequeue();
+						if (state == null) {
+							queue.finishAll();
+							return;
+						}
+						queue.enqueue(tlcState);
+					}
+					queue.finishAll();
+				}
+			}, "Worker");
+			worker.start();
+		}
+	}
+	
+	/*
+	 * Dummy implementation of StateQueue with minimal functionality compared to
+	 * DiskStateQueue or MemStateQueue. After all, we verify the abstract
+	 * StateQueue and not the implementations (which should be done separately).
+	 */
+	private static class DummyStateQueue extends StateQueue {
+
+		private TLCState state;
+
+		void enqueueInner(TLCState state) {
+			this.state = state;
+		}
+
+		TLCState dequeueInner() {
+			return state;
+		}
+
+		public void beginChkpt() throws IOException {
+			// checkpointing not being verified
+		}
+
+		public void commitChkpt() throws IOException {
+			// checkpointing not being verified
+		}
+
+		public void recover() throws IOException {
+			// checkpointing not being verified
+		}
+	}
+}