#!/bin/sh

# Generate code
java Generate Sample.java 3

# Compile code
javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar Sample.java

# Run JPF with gov.nasa.jpf.search.heuristic.BFSHeuristic
java -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar gov.nasa.jpf.JPF \
+target=Sample \
+classpath=. \
+search.class=gov.nasa.jpf.search.heuristic.BFSHeuristic \
+listener=SearchNotificationRecorder \
+native_classpath=. \
+recorder.file=first.ser \
+cg.enumerate_random=true

# Run JPF with BFSearch
java -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar gov.nasa.jpf.JPF \
+target=Sample \
+classpath=. \
+search.class=BFSearch \
+listener=SearchNotificationRecorder \
+native_classpath=. \
+recorder.file=second.ser \
+cg.enumerate_random=true

# Compare recordings
java CompareSearchRecordings first.ser second.ser