{-# 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 = True
    , configColorMode = ColorAlways
    }

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