StandardTestControllers.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LambdaCase #-}

{- |
    This module contains building blocks for constructing out-of-the-box 'TestController's.
    
    'TestController's have multiple duties during testing:
    
    * selecting test inputs,
    * deciding whether to continue testing,
    * returning testing results (other than 'Pass' or 'Fail'), and
    * potentially performing side effects during testing.
    
    The building blocks in this module allow composing 'TestController's in a modular way, by combining various choices for these responsibilities.
    Every building block carries its own state. For example, to stop testing after a fixed number of steps, a state in the form of a counter is
    needed, whereas returning the observed trace as test result requires recording the observed trace as state.
-}

module Lattest.Exec.StandardTestControllers (
-- * Test Selectors
selector,
TestSelector,
randomTestSelector,
randomTestSelectorFromSeed,
randomTestSelectorFromGen,
randomDataTestSelector,
randomDataTestSelectorFromSeed,
randomDataTestSelectorFromGen,
randomDataOrWaitForOutputTestSelector,
randomDataOrWaitForOutputTestSelectorFromSeed,
randomDataOrWaitForOutputTestSelectorFromGen,
andThen,
-- * Stop Conditions
StopCondition,
stopCondition,
untilCondition,
stopAfterSteps,
-- * Test Observers
TestObserver,
observer,
andObservingWith,
andObserving,
observingOnly,
traceObserver,
stateObserver,
inconclusiveStateObserver,
-- * Test Side Effects
TestSideEffect,
withSideEffect,
testSideEffect,
printActions,
printState
)
where

import Lattest.Exec.Testing(TestController(..))
import Lattest.Model.Alphabet(TestChoice, IOAct(..), actToChoice, SymInteract(..), IOSymInteract, GateValue(..), IOGateValue, SymGuard, IOSuspGateValue)
import Lattest.Model.Automaton(AutIntrpr(..), StepSemantics, FiniteMenu, specifiedMenu, stateConf, IntrpState(..), STStdest, After)
import Lattest.Model.StandardAutomata(IOSTSIntrp)
import Lattest.Model.BoundedMonad(isConclusive, BoundedConfiguration, BooleanConfiguration)
import Lattest.Model.Symbolic.SolveSTS(solveRandomInteraction)
import Lattest.SMT(runSMT)
import Lattest.Util.Utils(takeRandom, flipCoin)

import Data.Either.Combinators(leftToMaybe, maybeToLeft)
import qualified Lattest.Model.BoundedMonad as BM
import System.Random(RandomGen, StdGen, initStdGen, mkStdGen)
import Data.Maybe (mapMaybe)



{- |
    'Testselector's are test controllers that are only concerned with selecting inputs for testing. They do not return any testing results.
-}
type TestSelector m loc q t tdest act s i = TestController m loc q t tdest act s i ()

{- |
    Create a 'TestSelector'. Requires one function to select an input, also updating the state, and one function to update the state when observing
    an action.
-}
selector ::
    state ->
    (state -> AutIntrpr m loc q t tdest act -> m q -> IO (Maybe (i, state))) ->
    (state -> AutIntrpr m loc q t tdest act -> act -> m q -> IO (Maybe state)) ->
    TestSelector m loc q t tdest act state i
selector state sel upd = TestController {
    testControllerState = state,
    selectTest = \s aut mq -> maybeToLeft () <$> sel s aut mq,
    updateTestController = \s aut act mq -> maybeToLeft () <$> upd s aut act mq,
    handleTestClose = const $ return ()
    }

-- TODO introduce a combinator that adds the 'selector' behaviour to an arbitrary TestController. This is not needed if the selector is always 
-- taken as a basis to combine with stop conditions / test observers, but it would be more flexible to allow turning a composition around.

{- |
    A 'TestSelector' that picks inputs uniformly pseudo-randomly from the outgoing transitions from the current state configuration.
-}
randomTestSelector :: (After m loc q t tdest act, FiniteMenu t act, Foldable m, TestChoice i act, Ord act, Ord q, Ord (m q))
    => IO (TestSelector m loc q t tdest act StdGen i)
randomTestSelector = randomTestSelectorFromGen <$> initStdGen

{- |
    A 'TestSelector' that picks inputs uniformly pseudo-randomly from the outgoing transitions from the current state configuration, starting with
    the given random seed.
-}
randomTestSelectorFromSeed :: (After m loc q t tdest act, FiniteMenu t act, Foldable m, TestChoice i act, Ord act, Ord q, Ord (m q))
    => Int -> TestSelector m loc q t tdest act StdGen i
randomTestSelectorFromSeed i = randomTestSelectorFromGen $ mkStdGen i

{- |
    A 'TestSelector' that picks inputs uniformly pseudo-randomly from the outgoing transitions from the current state configuration, based on the
    given random generator.
-}
randomTestSelectorFromGen :: (After m loc q t tdest act, FiniteMenu t act, Foldable m, TestChoice i act, RandomGen g, Ord act, Ord q, Ord (m q))
    => g -> TestSelector m loc q t tdest act g i
randomTestSelectorFromGen g = selector g randomSelectTest (\s _ _ _ -> return $ Just s)
    where
    randomSelectTest g' aut _ =
        let ins = mapMaybe actToChoice (specifiedMenu aut)
        in if null ins
            then error "random test selector found an empty menu"
            else return $ Just $ takeRandom g' ins

{- |
    A 'TestSelector' that picks inputs uniformly pseudo-randomly from the outgoing transitions from the current state configuration.
-}
randomDataTestSelector :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o), BooleanConfiguration m, Ord i, Ord o, Ord (m SymGuard))
    => IO (TestSelector m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o) StdGen (GateValue i))
randomDataTestSelector = randomDataTestSelectorFromGen <$> initStdGen

{- |
    A 'TestSelector' that picks inputs uniformly pseudo-randomly from the outgoing transitions from the current state configuration, starting with
    the given random seed.
-}
randomDataTestSelectorFromSeed :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o), BooleanConfiguration m, Ord i, Ord o, Ord (m SymGuard))
    => Int -> TestSelector m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o) StdGen (GateValue i)
randomDataTestSelectorFromSeed i = randomDataTestSelectorFromGen (mkStdGen i)

{- |
    A 'TestSelector' that picks input gates uniformly pseudo-randomly from the outgoing transitions from the current state configuration, based on the
    given random generator, with arbitrary data values as picked by the given SMT solver. Will immediately stop if it cannot find any possible data values for any input gate.
-}
randomDataTestSelectorFromGen :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o), BooleanConfiguration m, Ord i, Ord o, Ord (m SymGuard), RandomGen g)
    => g -> TestSelector m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o) g (GateValue i)
randomDataTestSelectorFromGen g = selector g solveRandomIfPossible (\s _ _ _ -> return $ Just s)
    where
    solveRandomIfPossible :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOGateValue i o), BooleanConfiguration m, Ord i, Ord o, Ord (m SymGuard), RandomGen g)
        => g -> IOSTSIntrp m loc i o -> m (IntrpState loc) -> IO (Maybe (GateValue i, g))
    solveRandomIfPossible g'' intrpr _ = do
        (maybeGateValue, g') <- solveRandomInput g'' maybeFromIOAct intrpr
        return $ case maybeGateValue of
            Nothing -> Nothing
            Just value -> Just (value, g')
    maybeFromIOAct :: SymInteract (IOAct i1 o1) -> Maybe (SymInteract i1)
    maybeFromIOAct = error ""

{- |
    A 'TestSelector' that picks input gates uniformly pseudo-randomly from the outgoing transitions from the current state configuration, with arbitrary
    data values as picked by the given SMT solver. See 'randomDataOrWaitForOutputTestSelectorFromGen' for details.
-}
randomDataOrWaitForOutputTestSelector :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o), BooleanConfiguration m, Ord i, Ord o, Ord (m SymGuard))
    => Double -> IO (TestSelector m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o) StdGen (Maybe (GateValue i)))
randomDataOrWaitForOutputTestSelector pWait = do
    r <- initStdGen
    return $ randomDataOrWaitForOutputTestSelectorFromGen r pWait

{- |
    A 'TestSelector' that picks input gates uniformly pseudo-randomly from the outgoing transitions from the current state configuration, starting with
    the given random seed., with arbitrary data values as picked by the given SMT solver. See 'randomDataOrWaitForOutputTestSelectorFromGen' for details.
-}
randomDataOrWaitForOutputTestSelectorFromSeed :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o), BooleanConfiguration m, Ord i, Ord o, Ord (m SymGuard))
    => Int -> Double -> TestSelector m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o) StdGen (Maybe (GateValue i))
randomDataOrWaitForOutputTestSelectorFromSeed i = randomDataOrWaitForOutputTestSelectorFromGen (mkStdGen i)

{- |
    A 'TestSelector' that picks input gates uniformly pseudo-randomly from the outgoing transitions from the current state configuration, based on the
    given random generator, with arbitrary data values as picked by the given SMT solver. It may instead also omit picking an input gate, and wait 
    for an output value instead, with the givene probability (clamped to [0,1]). Will always wait for an output if it cannot find any possible data
    values for any input gate.
-}
randomDataOrWaitForOutputTestSelectorFromGen :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o), BooleanConfiguration m, Ord i, Ord o, RandomGen g, Ord (m SymGuard))
    => g -> Double -> TestSelector m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o) g (Maybe (GateValue i))
randomDataOrWaitForOutputTestSelectorFromGen g pWait = selector g (solveRandomOrWait pWait) (\s _ _ _ -> return $ Just s)
    where
    solveRandomOrWait :: (StepSemantics m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o), BooleanConfiguration m, Ord i, Ord o, RandomGen g, Ord (m SymGuard))
        => Double -> g -> AutIntrpr m loc (IntrpState loc) (IOSymInteract i o) STStdest (IOSuspGateValue i' o) -> m (IntrpState loc) -> IO (Maybe (Maybe (GateValue i), g))
    solveRandomOrWait pWait' g'' intrpr _ =
        let (doWait, g') = flipCoin g'' pWait'
        in if doWait
            then return $ Just (Nothing, g')
            else Just <$> solveRandomInput g' maybeFromIFInteraction intrpr
    maybeFromIFInteraction :: IOSymInteract i o -> Maybe (SymInteract i)
    maybeFromIFInteraction (SymInteract (In i) vars) = Just $ SymInteract i vars
    maybeFromIFInteraction (SymInteract _ _) = Nothing

solveRandomInput :: (BM.OrdMonad m, BooleanConfiguration m, Ord g, Ord (m SymGuard), RandomGen r)
    => r -> (SymInteract g -> Maybe (SymInteract i)) -> AutIntrpr m loc (IntrpState loc) (SymInteract g) STStdest (GateValue g') -> IO (Maybe (GateValue i), r)
solveRandomInput g f intrpr = do
    (maybeGateValue, g') <- runSMT $ solveRandomInteraction intrpr f g
    return (maybeGateValue, g') -- append the new state to the solved value, if any
{-        maybeFromIFInteraction' (SymInteract gate vars) = case maybeFromInput gate of
            Just i -> Just $ SymInteract i vars
            Nothing -> Nothing
-}

{- |
    Creates a TestController that first selects inputs according to the first provided TestController, and when that first TestController is finished, selects inputs according to the second provided TestController

    Note: the result from the first tester is currently dropped.
-}
andThen :: (TestChoice i act) => TestController m loc q t tdest act state1 i r1 -> TestController m loc q t tdest act state2 i r2 -> TestController m loc q t tdest act (Either state1 state2) i r2
andThen tester1 tester2 =
    TestController {
        testControllerState = Left $ testControllerState tester1,
        selectTest = andThenSelect,
        updateTestController = andThenUpdate,
        handleTestClose = \case
            (Left _) -> handleTestClose tester2 (testControllerState tester2)
            (Right s) -> handleTestClose tester2 s
    }
    where
        andThenSelect testState specState mq = case testState of
            (Left s) -> do
                res <- selectTest tester1 s specState mq
                case res of
                    Left (i1,s1) -> return $ Left (i1, Left s1)
                    Right _ -> do -- TODO: propagate results from first TestController to resulting TestController
                        res2 <- selectTest tester2 (testControllerState tester2) specState mq
                        return $ case res2 of
                            Left (i2,s2) -> Left (i2, Right s2)
                            Right r2 -> Right r2
            (Right s) -> do
                res2 <- selectTest tester2 s specState mq
                return $ case res2 of
                    Left (i2,s2) -> Left (i2, Right s2)
                    Right r2 -> Right r2
        andThenUpdate testState specState ioact mq = case testState of
            Left s -> do
                res1 <- updateTestController tester1 s specState ioact mq
                return $ case res1 of
                    Left s1 ->  Left $ Left s1
                    Right _ -> Left $ Right $ testControllerState tester2
            Right s -> do
                res2 <- updateTestController tester2 s specState ioact mq
                return $ case res2 of
                    Left s2 ->  Left $ Right s2
                    Right r2 -> Right r2


{- |
    'StopCondition's are test controllers that are only concerned with deciding whether to continue testing after observing an action. They do not
    select inputs or return any testing results.
-}
type StopCondition m loc q t tdest act s = TestController m loc q t tdest act s () ()

{- |
    Create a state-based stop condition, starting in the given initial state. The provided function should provide either 'Just' a new state to continue
    testing, or 'Nothing' to stop testing.
-}
stopCondition :: s -> (s -> AutIntrpr m loc q t tdest act -> act -> m q -> IO (Maybe s)) -> StopCondition m loc q t tdest act s
stopCondition state upd = TestController {
    testControllerState = state,
    selectTest = \s _ _  -> return $ Left ((), s), -- no state change, continue testing
    updateTestController = \s aut act q -> do
        maybeS' <- upd s aut act q
        case maybeS' of
            Just s' -> return $ Left s'
            Nothing -> return $ Right (),
    handleTestClose = const $ return ()
    }

{- |
    Apply a stop condition: run the (first) test controller until it returns a result, or until the stop condition is reached. The selected inputs and returned result come from the test controller.
-}
untilCondition :: TestController m loc q t tdest act state1 i1 r1 -> TestController m loc q t tdest act state2 i2 r2 -> TestController m loc q t tdest act (state1,state2) i1 r1
untilCondition controller condition = TestController {
    testControllerState = (testControllerState controller, testControllerState condition),
    selectTest = \s aut mq -> do
        next <- selectTest controller (fst s) aut mq
        return $ case next of
            Left (i,s') -> Left (i,(s',snd s))
            Right r -> Right r,
    updateTestController = \s aut act q -> do
        stateOrResult <- updateTestController controller (fst s) aut act q
        maybeCondState <- updateStopCondition condition (snd s) aut act q
        case stateOrResult of
            Left state -> case maybeCondState of
                Just condState -> return $ Left (state, condState)
                Nothing -> Right <$> handleTestClose controller state
            Right result -> return $ Right result,
    handleTestClose = handleTestClose controller . fst
    }
    where
    updateStopCondition :: TestController m loc q t tdest act state i r -> state -> AutIntrpr m loc q t tdest act -> act -> m q -> IO (Maybe state)
    updateStopCondition condition' state aut act q = leftToMaybe <$> updateTestController condition' state aut act q


{- |
    Observe a fixed number of actions, and then stop testing.
    
    Note: since stop conditions only decide whether to stop testing after observing an action, the minimum number of actions to observe is 1.
-}
stopAfterSteps :: Int -> StopCondition m loc q t tdest act Int
stopAfterSteps n = stopCondition n (\n' _ _ _ -> return $ if n' <= 1 then Nothing else Just (n'-1))

{- |
    'TestObserver's are only concerned with returning a result after testing. They do not select inputs or decide whether to continue testing.
-}
type TestObserver m loc q t tdest act s r = TestController m loc q t tdest act s () r

{- |
    Create a 'TestObserver'.
-}
observer :: s -> (s -> AutIntrpr m loc q t tdest act -> act -> m q -> IO s) -> (s -> IO r) -> TestObserver m loc q t tdest act s r
observer state upd finish = TestController {
    testControllerState = state,
    selectTest = \s _ _ -> return $ Left ((), s), -- no state change, continue testing
    updateTestController = \s aut act q -> Left <$> upd s aut act q,
    handleTestClose = finish
    }

{- |
    Apply an observer: Use the (former) test controller, but also returning the result of the (latter) observer. Combine the two results using the given function.
-}
andObservingWith :: TestController m loc q t tdest act state1 i1 r1 -> (r1 -> r2 -> r) -> TestController m loc q t tdest act state2 i2 r2 -> TestController m loc q t tdest act (state1,state2) i1 r
andObservingWith controller f obs = TestController {
    testControllerState = (testControllerState controller, testControllerState obs),
    selectTest = \s aut mq -> do
        next <- selectTest controller (fst s) aut mq
        case next of
            Left (i,s') -> return $ Left (i,(s',snd s))
            Right r1 -> do
                r2 <- handleTestClose obs (snd s)
                return $ Right $ f r1 r2,
    updateTestController = \s aut act q -> do
        stateOrResult1 <- updateTestController controller (fst s) aut act q
        stateOrResult2 <- updateTestController obs (snd s) aut act q
        case stateOrResult1 of
            Left s1 -> case stateOrResult2 of
                Left s2 -> return $ Left (s1, s2)
                Right r2 -> do
                    r1 <- handleTestClose controller s1
                    return $ Right $ f r1 r2
            Right r1 -> case stateOrResult2 of
                Left s2 -> do
                    r2 <- handleTestClose obs s2
                    return $ Right $ f r1 r2
                Right r2 -> return $ Right $ f r1 r2,
    handleTestClose = \(s1,s2) -> do
        r1 <- handleTestClose controller s1
        r2 <- handleTestClose obs s2
        return $ f r1 r2
    }

{- |
    Apply an observer: use the (former) test controller, but also returning the result of the (latter) observer in a tuple.
-}
andObserving :: TestController m loc q t tdest act state1 i1 r1 -> TestController m loc q t tdest act state2 i2 r2 -> TestController m loc q t tdest act (state1,state2) i1 (r1,r2)
andObserving controller = andObservingWith controller (,)

{- |
    Apply an observer: use the (former) test controller, but only return the result of the (latter) observer.
-}
observingOnly :: TestController m loc q t tdest act state1 i1 r1 -> TestController m loc q t tdest act state2 i2 r2 -> TestController m loc q t tdest act (state1,state2) i1 r2
observingOnly controller = andObservingWith controller (\_ r2 -> r2)

{- |
    A 'TestObserver' that returns the trace of all observed actions
-}
traceObserver :: TestObserver m loc q t tdest act [act] [act]
traceObserver = observer [] (\trace _ act _ -> return $ act : trace) (pure . reverse)

-- FIXME get rid of the Maybe
{- |
    A 'TestObserver' that returns the last state configuration of the specification model. This may be a conclusive state. For example,
    during a failed test, this observer returns 'forbidden'.
-}
stateObserver :: TestObserver m loc q t tdest act (Maybe (m q)) (Maybe (m q))
stateObserver = observer Nothing (\_ aut _ _ -> return $ Just (stateConf aut)) return

{- |
    A 'TestObserver' that returns the last inconclusive state configuration of the specification model. For example, during a failing test,
    this observer returns the last state before the failure.
    
-}
inconclusiveStateObserver :: BoundedConfiguration m => TestObserver m loc q t tdest act (Maybe (m q)) (Maybe (m q))
inconclusiveStateObserver = observer Nothing makeSelection return
    where
    makeSelection _ aut _ mq =
        let mq' = stateConf aut
        in return $ Just $ if isConclusive mq' then mq else mq'

{- |
    'TestSideEffect's perform side effects during testing, but have no impact on the testing itself, nor on the result.
-}
type TestSideEffect m loc q t tdest act s = TestController m loc q t tdest act s () ()

{- |
    Apply a side effect: Use the (former) test controller, but also perform the side effect of the (latter) observer.
-}
withSideEffect :: TestController m loc q t tdest act state1 i1 r1 -> TestController m loc q t tdest act state2 i2 r2 -> TestController m loc q t tdest act (state1,state2) i1 r1
withSideEffect controller = andObservingWith controller const


{- |
    Create a 'TestSideEffect'. The provided function returns the new state in an 'IO' monad that can also perform the side effects.
-}
testSideEffect :: s -> (s -> AutIntrpr m loc q t tdest act -> act -> m q -> IO s) -> TestSideEffect m loc q t tdest act s
testSideEffect s f = observer s f (const $ pure ())

{- |
    Print observed to stdin actions during testing.
-}
printActions :: Show act => TestSideEffect m loc q t tdest act ()
printActions = testSideEffect () (\_ _ act _ -> print act)

{- |
    Print the state configuration of the specification during testing.
-}
printState :: Show (m q) => TestSideEffect m loc q t tdest act ()
printState = testSideEffect () (\_ _ _ mq -> print mq)