Scaludita is based on Udita system but adapted to Scala by Tihomir Gvero

  def assume(p : Boolean) = Verify.ignoreIf(!p)
  def choose = Verify.getInt(1,20)
 
  val y = 11
  val x = choose
  assume(10 < y && x < 5 && y < 3*x)
  println("x = " + x)

package redblacktree
 
import gov.nasa.jpf.jvm.Verify;
import gov.nasa.jpf.jvm.generators.StructureCounter;
 
object RedBlackTreeTest extends Application { 
  val MAXTREESIZE = 4
 
  abstract class Color
  case class RED extends Color
  case class BLACK extends Color
 
  sealed abstract class Tree
  case class Empty extends Tree
  case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
 
 
  def member(x: Int, t:Tree): Boolean = t match {
    case Empty() => false
    case Node(_,a,y,b) => 
      if (x < y) member(x,a)
      else if (x > y) member(x,b)
      else true
  }
 
  def insert(x: Int, t: Tree): Tree = {
    def ins(t: Tree): Tree = t match {
      case Empty() => Node(RED(),Empty(),x,Empty())
      case Node(c,a,y,b) =>
        if      (x < y)  balance(c, ins(a), y, b)
        else if (x == y) Node(c,a,y,b)
        else             // balance(c,a,y,ins(b))
	  Node(c,a,y,ins(b))
    }
    makeBlack(ins(t))
  }
 
  def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = (c,a,x,b) match {
    case (BLACK(),Node(RED(),Node(RED(),a,xV,b),yV,c),zV,d) => 
      Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
    case (BLACK(),Node(RED(),a,xV,Node(RED(),b,yV,c)),zV,d) => 
      Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
    case (BLACK(),a,xV,Node(RED(),Node(RED(),b,yV,c),zV,d)) => 
      Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
    case (BLACK(),a,xV,Node(RED(),b,yV,Node(RED(),c,zV,d))) => 
      Node(RED(),Node(BLACK(),a,xV,b),yV,Node(BLACK(),c,zV,d))
    case (c,a,xV,b) => Node(c,a,xV,b)
  }
 
  /** makeBLACK: Turn a node BLACK. */
  def makeBlack(n: Tree): Tree = n match {
    case Node(RED(),l,v,r) => Node(BLACK(),l,v,r)
    case _ => n
  }
 
  /* global invariants: 
   * RED-BLACK trees are binary search trees obeying two key invariants:
   *
   * (1) Any path from a root node to a leaf node contains the same number
   *     of BLACK nodes. (A balancing condition.)
   *
   * (2) RED nodes always have BLACK children.
   *
   */
 
  /* Empty tree are consideRED to be BLACK */
  def isBLACK(t: Tree): Boolean = t match {
    case Node(RED(),_,_,_) => false
    case _ => true
  }
 
  private def getSubTree(size:Int, min:Int, max:Int): Tree = {
    if (size == 0) Empty()
    else if (size == 1) 
      Node(if (Verify.getBoolean()) RED() 
	   else BLACK(), Empty(), Verify.getInt(min,max), Empty())
    else {
      val value = Verify.getInt(min,max)
      val leftSize = value - min
      val rightSize = size - 1 - leftSize
      Node(if (Verify.getBoolean()) RED() else BLACK(), 
	   getSubTree(leftSize, min, value - 1), value, getSubTree(rightSize, value + 1, max))
    }
  }
 
  private def generateBinarySearchTree(treeSize:Int): Tree = {
    val size = Verify.getInt(1, treeSize)
    val maxNodeValue = size - 1
    val t = getSubTree(size, 0, maxNodeValue)
    t
  }
 
  // declarative, naive representation
  def anyPathsContainsSameNumberOfBlackNodes(t: Tree): Boolean = {
    def blackNodeNos(t: Tree, acc: Int): List[Int] = t match {
      case Empty() => List(acc + 1) // because Empty are assumed to be BLACK
      case Node(_,l,_,r) => {
        val upAcc = if(isBLACK(t)) acc + 1 else acc 
        blackNodeNos(l,upAcc) ::: blackNodeNos(r,upAcc) }
    }
    val paths = blackNodeNos(t, 0)
 
    paths.forall(_ == paths.head)
  } 
 
  def areRedNodeChildrenBlack(t: Tree): Boolean = t match {
    case Node(RED(),l,_,r) =>
      isBLACK(l) && isBLACK(r) &&
      areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
    case Node(BLACK(),l,_,r) =>
      areRedNodeChildrenBlack(l) && areRedNodeChildrenBlack(r)
    case _ => true
  }
 
  def generateRedBlackTree(treeSize:Int): Tree = {
    val t = generateBinarySearchTree(treeSize)
    Verify.ignoreIf(!(anyPathsContainsSameNumberOfBlackNodes(t) && areRedNodeChildrenBlack(t)))
    t
  }
 
  def content(t:Tree):Set[Int] = t match {
    case Empty() => Set.empty
    case Node(_,left,value,right) => (content(left) ++ Set(value) ++ content(right))
  }
 
  def forAllrbt(property: (Tree,Int) => Boolean){     
    val size = Verify.getInt(1,MAXTREESIZE+1)
    val t = generateRedBlackTree(size)
    val x = Verify.getInt(0,size)
    val prop = property(t,x)
    StructureCounter.incCounters(prop)
    if (!prop) {
      System.out.println("____________________________________________________________________")
      System.out.println("| Found counterexample: " + t+" "+x)
      System.out.println("--------------------------------------------------------------------")
      assert(false)
    }
    //System.out.println(t+" "+x)
  }
 
  forAllrbt((t:Tree, x:Int)  => ({
    val t1 = insert(x,t)
    anyPathsContainsSameNumberOfBlackNodes(t1) && areRedNodeChildrenBlack(t1)}))
}