{-# LANGUAGE OverloadedStrings #-}

import System.IO (BufferMode (LineBuffering), hSetBuffering, hSetEncoding, stdout, utf8)
import qualified Test.Control.State.Transition.Examples.CommitReveal as CommitReveal
import qualified Test.Control.State.Transition.Examples.GlobalSum as GSum
import qualified Test.Control.State.Transition.Examples.Sum as Sum
import Test.Hspec
import Test.Hspec.QuickCheck
import Test.Hspec.Runner
import Test.QuickCheck (expectFailure)

conf :: Config
conf :: Config
conf =
  Config
defaultConfig
    { configTimes :: Bool
configTimes = Bool
True
    , configColorMode :: ColorMode
configColorMode = ColorMode
ColorAlways
    }

spec :: Spec
spec :: Spec
spec = forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"All" forall a b. (a -> b) -> a -> b
$ do
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Sum" forall a b. (a -> b) -> a -> b
$ do
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"it allows to inspect generated trace counterexamples" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
expectFailure Property
Sum.prop_qc_Bounded
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Only valid traces are generated" Property
Sum.prop_qc_onlyValidSignalsAreGenerated
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"Classified" Property
Sum.prop_qc_Classified
  forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"CommitReveal" forall a b. (a -> b) -> a -> b
$ do
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"we're inspecting generated counterexamples" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
expectFailure Property
CommitReveal.prop_qc_UniqueData
    forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"a counterexample of an invalid signal should be found" forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => prop -> Property
expectFailure Property
CommitReveal.prop_qc_OnlyValidSignals
  Spec
GSum.spec

main :: IO ()
IO ()
main = do
  Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdout BufferMode
LineBuffering
  Handle -> TextEncoding -> IO ()
hSetEncoding Handle
stdout TextEncoding
utf8
  Config -> Spec -> IO ()
hspecWith Config
conf Spec
spec