Commands

commands.scala

package com.pulseenergy.lassie.translations

import org.scalacheck.{Arbitrary, Gen, Commands}
import org.scalacheck.Arbitrary.arbitrary
import org.scalacheck.Gen._

import org.scalatest.{Matchers, FlatSpec}
import org.scalatest.prop.{PropertyChecks, Checkers}

class Counter {
  private var n = 0
  def inc = n += 1
//  def dec = if(n > 10) n -= 2 else n -= 1  // Bug!
  def dec = n -= 1  // No bug!
  def get = n
  def reset = n = 0
}

class MySpecificationSpec extends FlatSpec with PropertyChecks with Matchers {


  it should "have the right state transitions" in {
    Checkers.check(new StackS[Int])
  }
//  it should "do the right thing" in {
//    Checkers.check(Specs)
//  }
}

object MySpecification extends Commands {

  val counter = new Counter

  case class State(n: Int)

  def initialState() = {
    counter.reset
    State(counter.get)
  }

  case object Inc extends Command {
    def run(s: State) = counter.inc
    def nextState(s: State) = State(s.n + 1)
    preConditions += (s => true)
  }

  case object Dec extends Command {
    def run(s: State) = counter.dec
    def nextState(s: State) = State(s.n - 1)
  }

  case object Get extends Command {
    def run(s: State) = counter.get
    def nextState(s: State) = s

    postConditions += {
      case (s0, s1, r:Int) =>
        assert(r == s0.n, s"s0.n should be: $r, but was ${s0.n}")
        r == s0.n
      case _ => false
    }
  }

  def genCommand(s: State): Gen[Command] = Gen.oneOf(Inc, Dec, Get)
}
class Stack[T] {
  private var items = List.empty[T]

  def push(item: T) = items = item :: items

  // Bug!
//  def popOption(): Option[T] = {
//    val result = items.headOption
//    if(items.length > 10) items = items.tail.tail
//    else if(items.nonEmpty) items = items.tail
//    result
//  }

//  No bug!
  def popOption(): Option[T] = {
    val result = items.headOption
    if (items.nonEmpty) items = items.tail
    result
  }

  def reset() = items = List.empty[T]
}
class StackS[T](implicit arbT: Arbitrary[T]) extends Commands {

  val stack = new Stack[T]

  case class State(items: List[T])

  def initialState() = {
    stack.reset()
    State(List.empty)
  }

  case class Push(n: T) extends Command {
    def run(s: State) = stack.push(n)
    def nextState(s: State) = State(n :: s.items)
    preConditions += (s => true)
  }

  case object PopOption extends Command {
    def run(s: State): Option[T] = stack.popOption()
    def nextState(s: State) = State(if(s.items.nonEmpty) s.items.tail else s.items)

    postConditions += {
      case (s0, s1, r:Option[T]) =>
        val result = s0.items.headOption == r
        assert(result, s"s0.items.headOption should be $r, but was ${s0.items.headOption}")
        result
      case _ => false
    }
  }

  def genCommand(s: State): Gen[Command] = Gen.oneOf( for(i <- arbitrary[T]) yield Push(i), Gen.const(PopOption))
}