no dependency on leon List

testcases/verification/xlang/DataRacing.scala

@@ -12,29 +12,32 @@ object DataRacing {
 
   implicit def toInstr(instr: (SharedState) => Unit): AtomicInstr = AtomicInstr(instr)
 
+  abstract class Runnable
+  case class RunnableCons(instr: AtomicInstr, tail: Runnable) extends Runnable
+  case class RunnableNil() extends Runnable
 
-  def execute(t1: List[AtomicInstr], t2: List[AtomicInstr], state: SharedState): Unit = (t1, t2) match {
-    case (x::xs, y::ys) =>
+  def execute(t1: Runnable, t2: Runnable, state: SharedState): Unit = (t1, t2) match {
+    case (RunnableCons(x,xs), RunnableCons(y,ys)) =>
       if(Random.nextBoolean) {
         x.instr(state)
-        execute(xs, y::ys, state)
+        execute(xs, RunnableCons(y,ys), state)
       } else {
         y.instr(state)
-        execute(x::xs, ys, state)
+        execute(RunnableCons(x,xs), ys, state)
       }
-    case (Nil(), y::ys) =>
+    case (RunnableNil(), RunnableCons(y,ys)) =>
       y.instr(state)
-      execute(Nil(), ys, state)
-    case (x::xs, Nil()) =>
+      execute(RunnableNil(), ys, state)
+    case (RunnableCons(x,xs), RunnableNil()) =>
       x.instr(state)
-      execute(xs, Nil(), state)
-    case (Nil(), Nil()) => ()
+      execute(xs, RunnableNil(), state)
+    case (RunnableNil(), RunnableNil()) => ()
   }
 
   def main(): Unit = {
     val state = SharedState(0)
-    val t1 = List[AtomicInstr]((s: SharedState) => s.i = s.i + 1)
-    val t2 = List[AtomicInstr]((s: SharedState) => s.i = s.i * 2)
+    val t1 = RunnableCons((s: SharedState) => s.i = s.i + 1, RunnableNil())
+    val t2 = RunnableCons((s: SharedState) => s.i = s.i * 2, RunnableNil())
     execute(t1, t2, state)
     assert(state.i == 2)
   }