/*-------------------------------------------------------------------------*\
** ScalaCheck **
** Copyright (c) 2007-2011 Rickard Nilsson. All rights reserved. **
** http://www.scalacheck.org **
** **
** This software is released under the terms of the Revised BSD License. **
** There is NO WARRANTY. See the file LICENSE for the full text. **
\*------------------------------------------------------------------------ */
package org.scalacheck
import Gen._
import Prop._
import Shrink._
/** See User Guide for usage examples */
trait Commands extends Prop {
/** The abstract state data type. This type must be immutable.
* The state type that encodes the abstract state. The abstract state
* should model all the features we need from the real state, the system
* under test. We should leave out all details that aren't needed for
* specifying our pre- and postconditions. The state type must be called
* State and be immutable. */
type State <: AnyRef
class Binding(private val key: State) {
def get: Any = bindings.find(_._1 eq key) match {
case None => sys.error("No value bound")
case Some(x) => x._2
}
}
/** Abstract commands are defined as subtypes of the traits Command or SetCommand.
* Each command must have a run method and a method that returns the new abstract
* state, as it should look after the command has been run.
* A command can also define a precondition that states how the current
* abstract state must look if the command should be allowed to run.
* Finally, we can also define a postcondition which verifies that the
* system under test is in a correct state after the command exectution. */
trait Command {
/** Used internally. */
protected[Commands] def run_(s: State) = run(s)
def run(s: State): Any
def nextState(s: State): State
/** Returns all preconditions merged into a single function */
def preCondition: (State => Boolean) = s => preConditions.toList.forall(_.apply(s))
/** A precondition is a function that
* takes the current abstract state as parameter and returns a boolean
* that says if the precondition is fulfilled or not. You can add several
* conditions to the precondition list */
val preConditions = new scala.collection.mutable.ListBuffer[State => Boolean]
/** Returns all postconditions merged into a single function */
def postCondition: (State,State,Any) => Prop = (s0,s1,r) => all(postConditions.map(_.apply(s0,s1,r)): _*)
/** A postcondition is a function that
* takes three parameters, s0, s1 and r. s0 is the abstract state before
* the command was run, s1 is the abstract state after the command was
* run, and r is the result from the command's run
* method. The postcondition function should return a Boolean (or
* a Prop instance) that says if the condition holds or not. You can add several
* conditions to the postConditions list. */
val postConditions = new scala.collection.mutable.ListBuffer[(State,State,Any) => Prop]
}
/** A command that binds its result for later use */
trait SetCommand extends Command {
/** Used internally. */
protected[Commands] final override def run_(s: State) = {
val r = run(s)
bindings += ((s,r))
r
}
final def nextState(s: State) = nextState(s, new Binding(s))
def nextState(s: State, b: Binding): State
}
private case class Cmds(cs: List[Command], ss: List[State]) {
override def toString = cs.map(_.toString).mkString(", ")
}
private val bindings = new scala.collection.mutable.ListBuffer[(State,Any)]
private def initState() = {
bindings.clear()
initialState()
}
private def genCmds: Gen[Cmds] = {
def sizedCmds(s: State)(sz: Int): Gen[Cmds] =
if(sz <= 0) value(Cmds(Nil, Nil)) else for {
c <- genCommand(s) suchThat (_.preCondition(s))
Cmds(cs,ss) <- sizedCmds(c.nextState(s))(sz-1)
} yield Cmds(c::cs, s::ss)
for {
s0 <- wrap(value(initialState()))
cmds <- sized(sizedCmds(s0))
} yield cmds
}
private def validCmds(s: State, cs: List[Command]): Option[Cmds] =
cs match {
case Nil => Some(Cmds(Nil, s::Nil))
case c::_ if !c.preCondition(s) => None
case c::cmds => for {
Cmds(_, ss) <- validCmds(c.nextState(s), cmds)
} yield Cmds(cs, s::ss)
}
private def runCommands(cmds: Cmds): Prop = cmds match {
case Cmds(Nil, _) => proved
case Cmds(c::cs, s::ss) =>
c.postCondition(s,c.nextState(s),c.run_(s)) && runCommands(Cmds(cs,ss))
case _ => sys.error("Should not be here")
}
private def commandsProp: Prop = {
def shrinkCmds(cmds: Cmds) = cmds match { case Cmds(cs,_) =>
shrink(cs)(shrinkContainer).flatMap(cs => validCmds(initialState(), cs).toList)
}
forAllShrink(genCmds label "COMMANDS", shrinkCmds)(runCommands _)
}
def apply(p: Prop.Params) = commandsProp(p)
/** initialState should reset the system under test to a well defined
* initial state, and return the abstract version of that state. */
def initialState(): State
/** The command generator. Given an abstract state, the generator
* should return a command that is allowed to run in that state. Note that
* it is still neccessary to define preconditions on the commands if there
* are any. The generator is just giving a hint of which commands that are
* suitable for a given state, the preconditions will still be checked before
* a command runs. Sometimes you maybe want to adjust the distribution of
* your command generator according to the state, or do other calculations
* based on the state. */
def genCommand(s: State): Gen[Command]
}
