{-# 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 qualified Test.Cardano.Base.QuickCheck as BaseQC
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)

data SUM

data NoFailure = NoFailure deriving (NoFailure -> NoFailure -> Bool
(NoFailure -> NoFailure -> Bool)
-> (NoFailure -> NoFailure -> Bool) -> Eq NoFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NoFailure -> NoFailure -> Bool
== :: NoFailure -> NoFailure -> Bool
$c/= :: NoFailure -> NoFailure -> Bool
/= :: NoFailure -> NoFailure -> Bool
Eq, Int -> NoFailure -> ShowS
[NoFailure] -> ShowS
NoFailure -> String
(Int -> NoFailure -> ShowS)
-> (NoFailure -> String)
-> ([NoFailure] -> ShowS)
-> Show NoFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NoFailure -> ShowS
showsPrec :: Int -> NoFailure -> ShowS
$cshow :: NoFailure -> String
show :: NoFailure -> String
$cshowList :: [NoFailure] -> ShowS
showList :: [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 = [Int -> F (Clause SUM 'Initial) Int
forall a. a -> F (Clause SUM 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0]

  transitionRules :: [TransitionRule SUM]
transitionRules =
    [ do
        TRC ((), st, xs) <- Rule SUM 'Transition (RuleContext 'Transition SUM)
F (Clause SUM 'Transition) (TRC SUM)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        return $! st + sum xs
    ]

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

  sigGen :: SignalGenerator SUM
sigGen Environment SUM
_ State SUM
_ =
    Range Int -> GenT Identity Int -> GenT Identity [Int]
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list (Int -> Int -> Range Int
forall a. a -> a -> Range a
Range.constant Int
1 Int
100) (Range Int -> GenT Identity Int
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Int -> Int -> Range Int
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
    ()
    ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
10) (Int -> Bool) -> (Trace SUM -> Int) -> Trace SUM -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace SUM -> Int
Trace SUM -> State SUM
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 =
  Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
BaseQC.withNumTests Int
300 (Property -> Property) -> Property -> Property
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 ()
_ = () -> Gen ()
forall a. a -> Gen a
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 = Gen [Int]
Gen (Signal SUM)
forall a. Arbitrary a => Gen a
arbitrary

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