R/state.R

In hedgehog: Property-Based Testing

#' A symbolic value.
#'
#' These values are the outputs of a computation
#' during the calculations' construction, and
#' allow a value to use the results of a previous
#' function.
#'
#' Really, this is just an integer, which we use
#' as a name for a value which will exist later
#' in the computation.
#'
#' @param var the integer output indicator.
symbolic <- function(var) {
  structure (var, class = c(class(var), "hedgehog.internal.symbolic"))
}

#' @export
print.hedgehog.internal.symbolic <- function ( x, ... ) {
  cat ( paste( "Var", x, "(symbolic)" ))
}

#' @export
print.action <- function ( x, ... ) {
  cat (x$title, "\n")
  if (length(x$input) > 0) {
    cat ("inputs:\n")
    print(x$input)
  }
  cat(paste("output variable:", x$output, "\n"))
}


#' State based testing commands
#'
#' This helper function assists one in creating commands
#' for state machine testing in hedgehog.
#'
#' @export
#'
#' @param title the name of this command, to be shown when
#'   reporting any failing test cases.
#' @param generator A generator which provides random arguments
#'   for the command, given the current (symbolic) state.
#'   If nothing can be done with the current state, one
#'   should preclude the situation with a requires and
#'   return NULL. Otherwise, it should be a list of
#'   arguments (the empty list is ok for functions which
#'   take no arguments).
#' @param execute A function from the concrete input,
#'   which executes the true function and returns
#'   concrete output.
#'   Function takes the (possibly named) arguments given
#'   by the generator.
#' @param require A function from the current (symbolic)
#'   state to a bool, indicating if action is currently
#'   applicable.
#'   Function also takes the (possibly named) arguments
#'   given by the generator (this is mostly used in
#'   shrinking, to ensure after a shrink its still
#'   something which could have been generated by the
#'   function generator).
#' @param update A function from state to state, which is
#'   polymorphic over symbolic and concrete inputs and
#'   outputs (as it is used in both action generation and
#'   command execution).
#'   It's critical that one doesn't "inspect" the output
#'   and input values when writing this function.
#' @param ensure A post-condition for a command that must be
#'   verified for the command to be considered a success.
#'   This should be a set of testthat expectations.
#' @return a command structure.
command  <- function( title
                    , generator
                    , execute
                    , require = function(state, ...) T
                    , update  = function(state, output, ...) state
                    , ensure  = function(state, output, ...) NULL
                    ) {
  gen_     <- match.fun(generator)
  execute_ <- match.fun(execute)
  require_ <- match.fun(require)
  update_  <- match.fun(update)
  ensure_  <- match.fun(ensure)
  structure (
    list(
        title   = title
      , gen     = gen_
      , execute = execute_
      , require = require_
      , update  = update_
      , ensure  = ensure_
    )
    , class = "command"
  )
}

# Reify command inputs
#
# Converts a symbolic structure to a concrete one,
# using the provided environment.
#
# @param x A structure potentially holding symbolic
#   variables, which will be replaced with concrete
#   values from the environment.
# @param env a map from symbolic to concrete
#   values.
# @return a reified structure holding concrete
#   values.
reify <- function(x, env) {
  if ( inherits(x, "hedgehog.internal.symbolic") ) {
    # We have a single symbolic variable
    # Find it in the environment.
    env[[x]]
  } else if (is.list( x )) {
    # We have a list which may contain
    # symbolic values.
    # Traverse over it, returning the
    # concrete version.
    lapply (x , function(x_) reify(x_, env))
  } else {
    # Let constants be.
    x
  }
}

# Generator for actions
#
# @param commands the list of commands which
#   we can select choose from. Only commands
#   appropriate for the state will actually be
#   selected.
# @param state the current state of the system
# @param counter the output variable this action
#   can write to.
#
# @return a list, acc is the new state and counter
#   as well as the action generated.
gen.action <- function(commands, state, counter) {
  possible <- Filter(function(command) {
    !is.null ( command$gen(state) )
  }, commands)
  gen.and_then(gen.element( possible ), function (command) {
    # The (symbolic) input for the command.
    # Essentially this says which values it
    # will read from.
    gen.map(function(input) {
      # Check the requires condition make sense.
      # These requires functions are needed to
      # ensure we have a good shrink.
      if (!do.call(command$require, c(list(state = state), as.list(input))))
        stop("Command generation arguments voilate requirements")

      # Get a variable name we'll use for the output
      # We just use sequential values, as we'll add
      # them to the environment list here.
      output   <- symbolic (counter)

      # Build a new state which we can work with
      state_   <- do.call(command$update , c(list(state = state, output = output), as.list( input )))

      # Build the action which can be run.
      action_  <- structure(list(
          title   = command$title
        , input   = input
        , output  = output
        , execute = command$execute
        , require = command$require
        , update  = command$update
        , ensure  = command$ensure
      ), class = "action")

      # Return the new symbolic state and the action to run.
      list(acc = list(state = state_, counter = counter + 1), action = action_)
    }, command$gen(state))
  })
}

# Returns the actions and it's updates to the state
# only if they're currently valid.
check.valid  <- function(ok, state, action) {
  if (do.call(action$require, c(list(state = state), as.list(action$input)))) {
    state_  <- do.call(action$update, c(list(state = state, output = action$output), as.list(action$input)))
    list(ok = snoc(ok, action), state = state_)
  } else {
    list(ok = ok, state = state)
  }
}

# After shrinking we may have an inconsistent state.
# Run the state, ensuring the requirements are still
# good.
drop.invalid <- function(actions, initial.state) {
  result <- Reduce(function(acc, action) {
    check.valid( acc$ok, acc$state, action )
  }, actions, init = list(ok = list(), state = initial.state))
  result$ok
}

#' Generate a list of possible actions.
#'
#' @export
#' @param initial.state the starting state to
#'   build from which is appropriate for this
#'   state machine generator.
#' @param commands the list of commands which
#'   we can select choose from. Only commands
#'   appropriate for the state will actually be
#'   selected.
#'
#' @return a list of actions to run during testing
gen.actions <- function(initial.state, commands) {
  gen.map(
    function(actions) drop.invalid(actions, initial.state)
  , { g <-  gen(function(size) {
              tree.bind(function(num) {
                tree.replicateS(num, function(x) {
                  gen.action(commands, x$state, x$counter)$unGen(size)
                }, list(state = initial.state, counter = 1))
              }, gen.int(size)$unGen(size) )
            })
      gen.shrink(shrink.list, g)
    }
  )
}

# Execute an action in an environment.
#
# Executes the action in an environment, ensuring
# all postconditions are met.
#
# @param state the current state of the system
# @param env the environment list (list of values
#   output so far by the computation.
# @param action the action to execute and check the
#   results from.
execute <- function(state, env, action) {
  input   <- reify( action$input, env )
  output  <- do.call( action$execute, as.list(input))
  state_  <- do.call( action$update, c(list(state = state, output = output), as.list( input )))
  env[[action$output]] <- output

  do.call( action$ensure, c(list(state = state_, output = output), as.list( input )))
  list( state = state_
      , environment = env
      )
}

#' Execute a state machine model
#'
#' Executes the list of commands sequentially,
#' ensuring that all postconditions hold.
#'
#' @export
#' @param initial.state the starting state to
#'   build from which is appropriate for this
#'   state machine generator.
#' @param actions the list of actions which
#'   are to be run.
#' @return an expectation.
expect_sequential <- function(initial.state, actions) {
  # Succeed ensures there is always at
  # least one expectation. If there wasn't
  # we could cause a "No expectations in
  # property" error and shrink to 0 elements
  # in the counterexample. This has to go first
  # so any real expectations have their error
  # message shown instead of "as expected".
  testthat::succeed()

  Reduce(
    function(acc, action) execute(acc$state, acc$environment, action)
  , init = list(state = initial.state, environment = list())
  , actions
  )
}