{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Rank2Types       #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan@advancedtelematic.com>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- The main module for state machine based testing, it contains
-- combinators that help you build sequential and parallel properties.
--
-----------------------------------------------------------------------------

module Test.StateMachine

  ( -- * Sequential property combinators
    Program
  , forAllProgram
  , runAndCheckProgram
  , runAndCheckProgram'

    -- * Parallel property combinators
  , ParallelProgram
  , forAllParallelProgram
  , History
  , runParallelProgram
  , runParallelProgram'
  , checkParallelProgram

    -- * Types
  , module Test.StateMachine.Types
  ) where

import           Control.Monad.State
                   (evalStateT, replicateM_)
import           Test.QuickCheck.Monadic
                   (monadic, monadicIO, run)
import           Test.QuickCheck.Property
                   (Property, forAllShrink, ioProperty)

import           Test.StateMachine.Internal.Parallel
import           Test.StateMachine.Internal.Sequential
import           Test.StateMachine.Internal.Types
import           Test.StateMachine.Internal.Types.Environment
import           Test.StateMachine.Internal.Utils
                   (liftProperty)
import           Test.StateMachine.Types

------------------------------------------------------------------------

-- | This function is like a 'forAllShrink' for sequential programs.
forAllProgram
  :: Show (Untyped act)
  => HFoldable act
  => Generator model act
  -> Shrinker act
  -> Precondition model act
  -> Transition   model act
  -> InitialModel model
  -> (Program act -> Property)  -- ^ Predicate that should hold for all
                                --   programs.
  -> Property
forAllProgram generator shrinker precondition transition model =
  forAllShrink
    (evalStateT (generateProgram generator precondition transition 0) model)
    (shrinkProgram shrinker precondition transition model)

-- | Run a sequential program and check if your model agrees with your
--   semantics.
runAndCheckProgram
  :: Monad m
  => HFunctor act
  => Precondition model act
  -> Transition model act
  -> Postcondition model act
  -> InitialModel model
  -> Semantics act m
  -> (m Property -> Property)  -- ^ Runner
  -> Program act
  -> Property
runAndCheckProgram precond trans postcond m sem runner =
  runAndCheckProgram' precond trans postcond m sem (return ()) (const runner) (const (return ()))

-- | Same as above, except with the possibility to setup some resource
--   for the runner to use. The resource could be a database connection
--   for example.
runAndCheckProgram'
  :: Monad m
  => HFunctor act
  => Precondition model act
  -> Transition model act
  -> Postcondition model act
  -> InitialModel model
  -> Semantics act m
  -> IO setup                           -- ^ Setup a resource.
  -> (setup -> m Property -> Property)
  -> (setup -> IO ())                   -- ^ Tear down the resource.
  -> Program act
  -> Property
runAndCheckProgram' precond trans postcond m sem setup runner cleanup acts =
  monadic (ioProperty . runnerWithSetup)
    (checkProgram precond trans postcond m m sem acts)
  where
  runnerWithSetup mp = do
    s <- setup
    let prop = runner s (evalStateT mp emptyEnvironment)
    cleanup s
    return prop

------------------------------------------------------------------------

-- | This function is like a 'forAllShrink' for parallel programs.
forAllParallelProgram
  :: Show (Untyped act)
  => HFoldable act
  => Generator model act
  -> Shrinker act
  -> Precondition model act
  -> Transition   model act
  -> InitialModel model
  -> (ParallelProgram act -> Property) -- ^ Predicate that should hold
                                       --   for all parallel programs.
  -> Property
forAllParallelProgram generator shrinker precondition transition model =
  forAllShrink
    (generateParallelProgram generator precondition transition model)
    (shrinkParallelProgram shrinker precondition transition model)

-- | Run a parallel program and collect the history of the execution.
runParallelProgram
  :: Show (Untyped act)
  => HTraversable act
  => Semantics act IO
  -> ParallelProgram act
  -> (History act -> Property) -- ^ Predicate that should hold for the
                               --   execution history.
  -> Property
runParallelProgram sem = runParallelProgram' (return ()) (const sem) (const (return ()))

-- | Same as above, but with the possibility of setting up some resource.
runParallelProgram'
  :: Show (Untyped act)
  => HTraversable act
  => IO setup                     -- ^ Setup a resource.
  -> (setup -> Semantics act IO)
  -> (setup -> IO ())             -- ^ Tear down the resource.
  -> ParallelProgram act
  -> (History act -> Property)
  -> Property
runParallelProgram' setup sem clean fork checkhistory = monadicIO $ do
  res <- run setup
  replicateM_ 10 $ do
    hist <- run (executeParallelProgram (sem res) fork)
    run (clean res)
    liftProperty (checkhistory hist)