content: {-# LANGUAGE DeriveAnyClass       #-}
  {-# LANGUAGE DeriveGeneric        #-}
  {-# LANGUAGE DerivingStrategies   #-}
  {-# LANGUAGE ExplicitNamespaces   #-}
  {-# LANGUAGE FlexibleContexts     #-}
  {-# LANGUAGE FlexibleInstances    #-}
  {-# LANGUAGE MonoLocalBinds       #-}
  {-# LANGUAGE PolyKinds            #-}
  {-# LANGUAGE ScopedTypeVariables  #-}
  {-# LANGUAGE StandaloneDeriving   #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  
  module Overflow
    ( prop_sequential_overflow
    , prop_parallel_overflow
    , prop_nparallel_overflow
    ) where
  
  import           Control.Concurrent
                     (threadDelay)
  import           Control.Concurrent.MVar
  import           Control.Monad
  import           Data.Int
  import           GHC.Generics
                     (Generic, Generic1)
  import           Prelude
  import           System.Random
                     (randomRIO)
  import           Test.QuickCheck
  import           Test.QuickCheck.Monadic
                     (monadicIO)
  import           Test.StateMachine
  import           Test.StateMachine.DotDrawing
  import qualified Test.StateMachine.Types.Rank2 as Rank2
  
  ------------------------------------------------------------------------
  
  -- The Model is a set of references of Int8. Command BackAndForth picks a random reference and adds a
  -- constant number (in an atomic way) and then substract the same number (in an atomic way).
  -- If there are enough threads (4 in this case) the result can overflow.
  
  data Command r
    = Create
    | Check (Reference (Opaque (MVar Int8)) r)
    | BackAndForth Int (Reference (Opaque (MVar Int8)) r)
    deriving stock (Eq, Generic1)
    deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
  
  deriving stock instance Show (Command Symbolic)
  deriving stock instance Read (Command Symbolic)
  deriving stock instance Show (Command Concrete)
  
  data Response r
      = Created (Reference (Opaque (MVar Int8)) r)
      | IsNegative Bool
      | Unit
      deriving stock (Eq, Generic1)
      deriving anyclass (Rank2.Foldable)
  
  deriving stock instance Show (Response Symbolic)
  deriving stock instance Read (Response Symbolic)
  deriving stock instance Show (Response Concrete)
  
  newtype Model r = Model [(Reference (Opaque (MVar Int8)) r, Int8)]
    deriving stock (Generic, Show)
  
  getVars :: Model r -> [Reference (Opaque (MVar Int8)) r]
  getVars (Model ls) = fst <$> ls
  
  instance ToExpr (Model Symbolic)
  instance ToExpr (Model Concrete)
  
  initModel :: Model r
  initModel = Model []
  
  transition :: Model r -> Command r -> Response r -> Model r
  transition m@(Model model) cmd resp = case (cmd, resp) of
    (Create, Created var)    -> Model ((var, 0) : model)
    (Check _, IsNegative _)  -> m
    (BackAndForth _ _, Unit) -> m
    _                        -> error "impossible to transition!"
  
  precondition :: Model Symbolic -> Command Symbolic -> Logic
  precondition m cmd = case cmd of
    Create             -> Top
    Check var          -> var `member` getVars m
    BackAndForth _ var -> var `member` getVars m
  
  postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
  postcondition _ cmd resp = case (cmd, resp) of
    (Create, Created _)      -> Top
    (Check _, IsNegative bl) -> bl .== False
    (BackAndForth _ _, Unit) -> Top
    _                        -> Bot
  
  semantics :: Command Concrete -> IO (Response Concrete)
  semantics cmd = case cmd of
    Create        -> Created <$> (reference . Opaque <$> newMVar 0)
    Check var     -> do
      val <- readMVar (opaque var)
      return $ IsNegative $ val < 0
    BackAndForth n var -> do
      modifyMVar_ (opaque var) $ \x -> return $ x + fromIntegral n
      threadDelay =<< randomRIO (0, 5000)
      modifyMVar_ (opaque var) $ \x -> return $ x - fromIntegral n
      return Unit
  
  mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
  mock _ cmd = case cmd of
    Create           -> Created <$> genSym
    Check _var       -> return $ IsNegative False
    BackAndForth _ _ -> return $ Unit
  
  generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
  generator (Model []) = Just (return Create)
  generator m          = Just $ frequency
                  [ (1, return Create)
                  , (3, genBackAndForth m)
                  , (3, genCheck m)
                  ]
  
  genCheck :: Model Symbolic -> Gen (Command Symbolic)
  genCheck m =
    Check <$> elements (getVars m)
  
  genBackAndForth :: Model Symbolic -> Gen (Command Symbolic)
  genBackAndForth m = do
    -- The upper limit here must have the property 2 * n < 128 <= 3 * n, so that
    -- there is a counter example for >= 4 threads.
    -- The lower limit only affects how fast a counterexample will be found.
    n <- choose (30,60)
    BackAndForth n <$> elements (getVars m)
  
  shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
  shrinker _ (BackAndForth n var) = [ BackAndForth n' var | n' <- shrink n ]
  shrinker _ _                    = []
  
  sm :: StateMachine Model Command IO Response
  sm = StateMachine initModel transition precondition postcondition
             Nothing generator shrinker semantics mock noCleanup
  
  prop_sequential_overflow :: Property
  prop_sequential_overflow = forAllCommands sm Nothing $ \cmds -> monadicIO $ do
    (hist, _model, res) <- runCommands sm cmds
    prettyCommands sm hist (res === Ok)
  
  prop_parallel_overflow :: Property
  prop_parallel_overflow = forAllParallelCommands sm Nothing $ \cmds -> monadicIO $
      prettyParallelCommandsWithOpts cmds opts =<< runParallelCommands sm cmds
        where opts = Just $ GraphOptions "overflow-test-output.png" Png
  
  prop_nparallel_overflow :: Int -> Property
  prop_nparallel_overflow np = forAllNParallelCommands sm np $ \cmds -> monadicIO $
      prettyNParallelCommandsWithOpts cmds opts =<< runNParallelCommands sm cmds
        where opts = Just $ GraphOptions ("overflow-" ++ show np ++ "-test-output.png") Png
  