{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | Simple example of a transition system whose states contain the sum of the
-- integers seen in the signals.
module Test.Control.State.Transition.Examples.Sum where

import Control.State.Transition
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Test.Control.State.Transition.Generator
import Test.Control.State.Transition.Trace
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as STS.Gen
import Test.QuickCheck (Property, arbitrary, shrink, withMaxSuccess)

data SUM

data NoFailure = NoFailure deriving (NoFailure -> NoFailure -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NoFailure -> NoFailure -> Bool
$c/= :: NoFailure -> NoFailure -> Bool
== :: NoFailure -> NoFailure -> Bool
$c== :: NoFailure -> NoFailure -> Bool
Eq, Int -> NoFailure -> ShowS
[NoFailure] -> ShowS
NoFailure -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NoFailure] -> ShowS
$cshowList :: [NoFailure] -> ShowS
show :: NoFailure -> String
$cshow :: NoFailure -> String
showsPrec :: Int -> NoFailure -> ShowS
$cshowsPrec :: Int -> NoFailure -> ShowS
Show)

instance STS SUM where
  type Environment SUM = ()

  type State SUM = Int

  type Signal SUM = [Int]

  type PredicateFailure SUM = NoFailure

  initialRules :: [InitialRule SUM]
initialRules = [forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0]

  transitionRules :: [TransitionRule SUM]
transitionRules =
    [ do
        TRC ((), State SUM
st, Signal SUM
xs) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! State SUM
st forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Signal SUM
xs
    ]

instance HasTrace SUM where
  envGen :: Word64 -> Gen (Environment SUM)
envGen Word64
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  sigGen :: SignalGenerator SUM
sigGen Environment SUM
_ State SUM
_ =
    forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list (forall a. a -> a -> Range a
Range.constant Int
1 Int
100) (forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. a -> a -> Range a
Range.constant (-Int
3) Int
3))

-- | This property is intended to be used to manually inspect the
-- counterexamples that we get.
prop_qc_Bounded :: Property
prop_qc_Bounded :: Property
prop_qc_Bounded =
  forall sts traceGenEnv prop.
(HasTrace sts traceGenEnv, Testable prop,
 Show (Environment sts)) =>
BaseEnv sts
-> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property
STS.Gen.forAllTrace @SUM @()
    ()
    Word64
100
    ()
    ((forall a. Ord a => a -> a -> Bool
< Int
10) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Trace s -> State s
lastState)

-- | Property that simply classifies the trace length distribution.
prop_qc_Classified :: Property
prop_qc_Classified :: Property
prop_qc_Classified =
  forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts)) =>
BaseEnv sts -> Word64 -> Word64 -> traceGenEnv -> Property
STS.Gen.traceLengthsAreClassified @SUM () Word64
100 Word64
10 ()

prop_qc_onlyValidSignalsAreGenerated :: Property
prop_qc_onlyValidSignalsAreGenerated :: Property
prop_qc_onlyValidSignalsAreGenerated =
  forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
300 forall a b. (a -> b) -> a -> b
$
    forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts),
 Show (Signal sts)) =>
BaseEnv sts -> Word64 -> traceGenEnv -> Property
STS.Gen.onlyValidSignalsAreGenerated @SUM @() () Word64
100 ()

instance STS.Gen.HasTrace SUM () where
  envGen :: HasCallStack => () -> Gen (Environment SUM)
envGen ()
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  sigGen :: HasCallStack =>
() -> Environment SUM -> State SUM -> Gen (Signal SUM)
sigGen ()
_traceEnv Environment SUM
_env State SUM
_st = forall a. Arbitrary a => Gen a
arbitrary

  shrinkSignal :: HasCallStack => Signal SUM -> [Signal SUM]
shrinkSignal = forall a. Arbitrary a => a -> [a]
shrink