Initial import

[jpf-core.git] / src / examples / RobotManager-replay-ot.jpf

diff --git a/src/examples/RobotManager-replay-ot.jpf b/src/examples/RobotManager-replay-ot.jpf
new file mode 100644 (file)
index 0000000..67aa617
--- /dev/null
+++ b/src/examples/RobotManager-replay-ot.jpf
@@ -0,0 +1,10 @@
+target = RobotManager
+
+listener=.listener.ChoiceSelector,.listener.ObjectTracker
+
+choice.use_trace=trace
+
+ot.refs = 0x160,0x185
+ot.log_fields = false
+
+cg.enumerate_random=true