{-# LANGUAGE LambdaCase     #-}
{-# LANGUAGE NamedFieldPuns #-}

module Ouroboros.Network.ConnectionManager.Test.Timeouts
  ( verifyAllTimeouts
  , SimAddr
  , SimAddr_
  , TestAddr (..)
  , TestProperty (..)
  , ArbDataFlow (..)
  , Timeouts (..)
  , ioTimeouts
  , simTimeouts
  , mkProperty
  , mkPropertyPruning
  , groupConns
  , groupConnsEither
  , classifyNegotiatedDataFlow
  , classifyActivityType
  , classifyEffectiveDataFlow
  , classifyTermination
  , classifyPrunings
  , classifyPruning
  , within_
  , ppTransition
  ) where

import Control.Monad.Class.MonadTime.SI (DiffTime, Time, diffTime)
import Control.Monad.IOSim

import Data.Bifoldable (bifoldMap)
import Data.Bitraversable (bimapAccumL)
import Data.List (dropWhileEnd, find, intercalate)
import Data.List.Trace qualified as Trace
import Data.Map.Strict qualified as Map
import Data.Maybe (fromJust, fromMaybe, isJust, isNothing)
import Data.Monoid (Sum (Sum))

import Text.Printf (printf)

import Test.QuickCheck (Arbitrary (..), Property, choose, counterexample, cover,
           frequency, label, property, shrink, tabulate, (.&&.))
import Test.QuickCheck.Monoids (All (..))

import Ouroboros.Network.ConnectionHandler (ConnectionHandlerTrace)
import Ouroboros.Network.ConnectionManager.Core qualified as CM
import Ouroboros.Network.ConnectionManager.Types
import Ouroboros.Network.Driver.Limits (ProtocolTimeLimits (..))
import Ouroboros.Network.Protocol.Handshake.Codec (timeLimitsHandshake)
import Ouroboros.Network.Protocol.Handshake.Type
import Ouroboros.Network.Snocket qualified as Snocket


verifyAllTimeouts :: Show addr
                  => Bool
                  -> Trace (SimResult ()) [(Time, AbstractTransitionTrace addr)]
                  -> All
verifyAllTimeouts :: forall addr.
Show addr =>
Bool
-> Trace (SimResult ()) [(Time, AbstractTransitionTrace addr)]
-> All
verifyAllTimeouts Bool
inDiffusion =
  (SimResult () -> All)
-> ([(Time, AbstractTransitionTrace addr)] -> All)
-> Trace (SimResult ()) [(Time, AbstractTransitionTrace addr)]
-> All
forall m a b. Monoid m => (a -> m) -> (b -> m) -> Trace a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap
   ( \ case
       MainReturn {} -> All
forall a. Monoid a => a
mempty
       SimResult ()
v             -> Property -> All
forall p. Testable p => p -> All
All
                     (Property -> All) -> Property -> All
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (SimResult () -> String
forall a. Show a => a -> String
show SimResult ()
v) Bool
False
   )
   (\ [(Time, AbstractTransitionTrace addr)]
tr ->
     Property -> All
forall p. Testable p => p -> All
All
     (Property -> All) -> Property -> All
forall a b. (a -> b) -> a -> b
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"\nConnection transition trace:\n"
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (((Time, AbstractTransitionTrace addr) -> String)
-> [(Time, AbstractTransitionTrace addr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Time, AbstractTransitionTrace addr) -> String
forall a. Show a => a -> String
show [(Time, AbstractTransitionTrace addr)]
tr)
                     )
     (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
tr)

-- verifyTimeouts checks that in all \tau transition states the timeout is
-- respected. It does so by checking the stream of abstract transitions
-- paired with the time they happened, for a given connection; and checking
-- that transitions from \tau states to any other happens within the correct
-- timeout bounds. One note is that for the example
-- InboundIdleState^\tau -> OutboundState^\tau -> OutboundState sequence
-- The first transition would be fine, but for the second we need the time
-- when we transitioned into InboundIdleState and not OutboundState.
--
verifyTimeouts :: Maybe (AbstractState, Time)
               -- ^ Map of first occurrence of a given \tau state
               -> Bool
               -- ^ If running in Diffusion or not
               -> [(Time , AbstractTransitionTrace addr)]
               -- ^ Stream of abstract transitions for a given connection
               -- paired with the time it occurred
               -> Property
verifyTimeouts :: forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
state Bool
inDiffusion [] =
  String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
    (String
"This state didn't timeout:\n"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe (AbstractState, Time) -> String
forall a. Show a => a -> String
show Maybe (AbstractState, Time)
state
    )
  (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Bool
inDiffusion Bool -> Bool -> Bool
|| Maybe (AbstractState, Time) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (AbstractState, Time)
state
-- If we already seen a \tau transition state
verifyTimeouts st :: Maybe (AbstractState, Time)
st@(Just (AbstractState
state, Time
t')) Bool
inDiffusion
               ((Time
t, TransitionTrace addr
_ tt :: Transition' AbstractState
tt@(Transition AbstractState
_ AbstractState
to)):[(Time, AbstractTransitionTrace addr)]
xs) =
    let newState :: Maybe (AbstractState, Time)
newState  = (AbstractState, Time) -> Maybe (AbstractState, Time)
forall a. a -> Maybe a
Just (AbstractState
to, Time
t)
        idleTimeout :: DiffTime
idleTimeout  =
            DiffTime
1.1 DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* Timeouts -> DiffTime
tProtocolIdleTimeout Timeouts
simTimeouts
        outboundTimeout :: DiffTime
outboundTimeout =
            DiffTime
1.1 DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* Timeouts -> DiffTime
tOutboundIdleTimeout Timeouts
simTimeouts
        timeWaitTimeout :: DiffTime
timeWaitTimeout =
            DiffTime
1.1 DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* Timeouts -> DiffTime
tTimeWaitTimeout Timeouts
simTimeouts
        handshakeTimeout :: DiffTime
handshakeTimeout = case ProtocolTimeLimits (Handshake Any Term)
forall {k} (vNumber :: k).
ProtocolTimeLimits (Handshake vNumber Term)
timeLimitsHandshake of
          (ProtocolTimeLimits forall (st :: Handshake Any Term).
ActiveState st =>
StateToken st -> Maybe DiffTime
stLimit) ->
            -- Should be the same but we bias to the shorter one
            let time :: DiffTime
time = DiffTime -> DiffTime -> DiffTime
forall a. Ord a => a -> a -> a
min (DiffTime -> Maybe DiffTime -> DiffTime
forall a. a -> Maybe a -> a
fromMaybe DiffTime
0 (StateToken 'StPropose -> Maybe DiffTime
forall (st :: Handshake Any Term).
ActiveState st =>
StateToken st -> Maybe DiffTime
stLimit SingHandshake 'StPropose
StateToken 'StPropose
forall {k} {k1} {vNumber :: k} {vParams :: k1}.
SingHandshake 'StPropose
SingPropose))
                           (DiffTime -> Maybe DiffTime -> DiffTime
forall a. a -> Maybe a -> a
fromMaybe DiffTime
0 (StateToken 'StConfirm -> Maybe DiffTime
forall (st :: Handshake Any Term).
ActiveState st =>
StateToken st -> Maybe DiffTime
stLimit SingHandshake 'StConfirm
StateToken 'StConfirm
forall {k} {k1} {vNumber :: k} {vParams :: k1}.
SingHandshake 'StConfirm
SingConfirm))
             in DiffTime
time DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
+ (DiffTime
0.1 DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* DiffTime
time)

     in case AbstractState
state of
       UnnegotiatedSt Provenance
_ -> case AbstractState
to of
         -- Timeout terminating states
         AbstractState
OutboundUniSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
handshakeTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
handshakeTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         InboundIdleSt DataFlow
Unidirectional ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
handshakeTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
handshakeTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
TerminatedSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
handshakeTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
handshakeTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- These states terminate the current timeout
         -- and starts a new one
         OutboundDupSt TimeoutExpired
Ticking ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
handshakeTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
handshakeTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         InboundIdleSt DataFlow
Duplex ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
handshakeTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
handshakeTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Unexpected invalid transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe (AbstractState, Time), Transition' AbstractState) -> String
forall a. Show a => a -> String
show (Maybe (AbstractState, Time)
st, Transition' AbstractState
tt))

       InboundIdleSt DataFlow
Duplex         -> case AbstractState
to of
         -- Should preserve the timeout
         OutboundDupSt TimeoutExpired
Ticking -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
st Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         InboundIdleSt DataFlow
Duplex -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
st Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- Timeout terminating states
         OutboundDupSt TimeoutExpired
Expired ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         InboundSt DataFlow
Duplex ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
DuplexSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
TerminatedSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- This state terminates the current timeout
         -- and starts a new one
         AbstractState
TerminatingSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Unexpected invalid transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe (AbstractState, Time), Transition' AbstractState) -> String
forall a. Show a => a -> String
show (Maybe (AbstractState, Time)
st, Transition' AbstractState
tt))

       InboundIdleSt DataFlow
Unidirectional -> case AbstractState
to of
         -- Timeout terminating states
         InboundSt DataFlow
Unidirectional ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
TerminatedSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- This state terminates the current timeout
         -- and starts a new one
         AbstractState
TerminatingSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
idleTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Unexpected invalid transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe (AbstractState, Time), Transition' AbstractState) -> String
forall a. Show a => a -> String
show (Maybe (AbstractState, Time)
st, Transition' AbstractState
tt))

       OutboundDupSt TimeoutExpired
Ticking        -> case AbstractState
to of
         -- Should preserve the timeout
         InboundIdleSt DataFlow
Duplex -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
st Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         OutboundDupSt TimeoutExpired
Ticking -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
st Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- Timeout terminating states
         OutboundDupSt TimeoutExpired
Expired ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
DuplexSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         InboundSt DataFlow
Duplex ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
TerminatedSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- This state terminates the current timeout
         -- and starts a new one
         AbstractState
TerminatingSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Unexpected invalid transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe (AbstractState, Time), Transition' AbstractState) -> String
forall a. Show a => a -> String
show (Maybe (AbstractState, Time)
st, Transition' AbstractState
tt))

       OutboundIdleSt DataFlow
_             -> case AbstractState
to of
         -- Timeout terminating states
         InboundSt DataFlow
Duplex ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
         AbstractState
TerminatedSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         -- This state terminates the current timeout
         -- and starts a new one
         AbstractState
TerminatingSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
outboundTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Unexpected invalid transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe (AbstractState, Time), Transition' AbstractState) -> String
forall a. Show a => a -> String
show (Maybe (AbstractState, Time)
st, Transition' AbstractState
tt))

       AbstractState
TerminatingSt                -> case AbstractState
to of
         -- Timeout terminating states
         UnnegotiatedSt Provenance
Inbound ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
timeWaitTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
TerminatedSt ->
           String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Transition' AbstractState -> Time -> Time -> DiffTime -> String
forall {a} {a}.
(Show a, Show a) =>
a -> Time -> Time -> a -> String
errorMsg Transition' AbstractState
tt Time
t' Time
t DiffTime
idleTimeout)
           (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Time -> Time -> DiffTime
diffTime Time
t Time
t' DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
<= DiffTime
timeWaitTimeout
           Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

         AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Unexpected invalid transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe (AbstractState, Time), Transition' AbstractState) -> String
forall a. Show a => a -> String
show (Maybe (AbstractState, Time)
st, Transition' AbstractState
tt))

       AbstractState
_ -> String -> Property
forall a. HasCallStack => String -> a
error (String
"Should be a \tau state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe (AbstractState, Time) -> String
forall a. Show a => a -> String
show Maybe (AbstractState, Time)
st)
  where
    errorMsg :: a -> Time -> Time -> a -> String
errorMsg a
trans Time
time' Time
time a
maxDiffTime =
      String
"\nAt transition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
trans String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"First happened at: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Time -> String
forall a. Show a => a -> String
show Time
time' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Second happened at: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Time -> String
forall a. Show a => a -> String
show Time
time String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Should only take: "
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
maxDiffTime
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", but took:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DiffTime -> String
forall a. Show a => a -> String
show (Time -> Time -> DiffTime
diffTime Time
time Time
time')
-- If we haven't seen a \tau transition state
verifyTimeouts Maybe (AbstractState, Time)
Nothing Bool
inDiffusion ((Time
t, TransitionTrace addr
_ (Transition AbstractState
_ AbstractState
to)):[(Time, AbstractTransitionTrace addr)]
xs) =
    let newState :: Maybe (AbstractState, Time)
newState = (AbstractState, Time) -> Maybe (AbstractState, Time)
forall a. a -> Maybe a
Just (AbstractState
to, Time
t)
     in case AbstractState
to of
       InboundIdleSt DataFlow
_       -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
       OutboundDupSt TimeoutExpired
Ticking -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
       OutboundIdleSt DataFlow
_      -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
       AbstractState
TerminatingSt         -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
newState Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs
       AbstractState
_                     -> Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
forall addr.
Maybe (AbstractState, Time)
-> Bool -> [(Time, AbstractTransitionTrace addr)] -> Property
verifyTimeouts Maybe (AbstractState, Time)
forall a. Maybe a
Nothing  Bool
inDiffusion [(Time, AbstractTransitionTrace addr)]
xs

-- | Configurable timeouts.  We use different timeouts for 'IO' and 'IOSim' property tests.
--
data Timeouts = Timeouts {
    Timeouts -> DiffTime
tProtocolIdleTimeout :: DiffTime,
    Timeouts -> DiffTime
tOutboundIdleTimeout :: DiffTime,
    Timeouts -> DiffTime
tTimeWaitTimeout     :: DiffTime
  }

-- | Timeouts for 'IO' tests.
--
ioTimeouts :: Timeouts
ioTimeouts :: Timeouts
ioTimeouts = Timeouts {
    tProtocolIdleTimeout :: DiffTime
tProtocolIdleTimeout = DiffTime
0.1,
    tOutboundIdleTimeout :: DiffTime
tOutboundIdleTimeout = DiffTime
0.1,
    tTimeWaitTimeout :: DiffTime
tTimeWaitTimeout     = DiffTime
0.1
  }

-- | Timeouts for 'IOSim' tests.
--
simTimeouts :: Timeouts
simTimeouts :: Timeouts
simTimeouts = Timeouts {
    tProtocolIdleTimeout :: DiffTime
tProtocolIdleTimeout = DiffTime
5,
    tOutboundIdleTimeout :: DiffTime
tOutboundIdleTimeout = DiffTime
5,
    tTimeWaitTimeout :: DiffTime
tTimeWaitTimeout     = DiffTime
30
  }

-- | Groups 'TransitionTrace' to the same peerAddr.
--
groupConns :: Ord addr
           => (a -> TransitionTrace' addr st)
           -> (Transition' st -> Bool)
           -> Trace r a
           -> Trace r [a]
groupConns :: forall addr a st r.
Ord addr =>
(a -> TransitionTrace' addr st)
-> (Transition' st -> Bool) -> Trace r a -> Trace r [a]
groupConns a -> TransitionTrace' addr st
getTransition Transition' st -> Bool
isFinalTransition =
    (Maybe [a] -> [a]) -> Trace r (Maybe [a]) -> Trace r [a]
forall a b. (a -> b) -> Trace r a -> Trace r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe [a] -> [a]
forall a. HasCallStack => Maybe a -> a
fromJust
  (Trace r (Maybe [a]) -> Trace r [a])
-> (Trace r a -> Trace r (Maybe [a])) -> Trace r a -> Trace r [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe [a] -> Bool) -> Trace r (Maybe [a]) -> Trace r (Maybe [a])
forall b a. (b -> Bool) -> Trace a b -> Trace a b
Trace.filter Maybe [a] -> Bool
forall a. Maybe a -> Bool
isJust
  -- there might be some connections in the state, push them onto the 'Trace'
  (Trace r (Maybe [a]) -> Trace r (Maybe [a]))
-> (Trace r a -> Trace r (Maybe [a]))
-> Trace r a
-> Trace r (Maybe [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Map addr [a]
s, Trace r (Maybe [a])
o) -> ([a] -> Trace r (Maybe [a]) -> Trace r (Maybe [a]))
-> Trace r (Maybe [a]) -> [[a]] -> Trace r (Maybe [a])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\[a]
a Trace r (Maybe [a])
as -> Maybe [a] -> Trace r (Maybe [a]) -> Trace r (Maybe [a])
forall a b. b -> Trace a b -> Trace a b
Trace.Cons ([a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
a)) Trace r (Maybe [a])
as) Trace r (Maybe [a])
o (Map addr [a] -> [[a]]
forall k a. Map k a -> [a]
Map.elems Map addr [a]
s))
  ((Map addr [a], Trace r (Maybe [a])) -> Trace r (Maybe [a]))
-> (Trace r a -> (Map addr [a], Trace r (Maybe [a])))
-> Trace r a
-> Trace r (Maybe [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map addr [a] -> r -> (Map addr [a], r))
-> (Map addr [a] -> a -> (Map addr [a], Maybe [a]))
-> Map addr [a]
-> Trace r a
-> (Map addr [a], Trace r (Maybe [a]))
forall (t :: * -> * -> *) a b c d e.
Bitraversable t =>
(a -> b -> (a, c))
-> (a -> d -> (a, e)) -> a -> t b d -> (a, t c e)
bimapAccumL
      ( \ Map addr [a]
s r
a -> (Map addr [a]
s, r
a))
      ( \ Map addr [a]
s a
a ->
          let TransitionTrace { addr
ttPeerAddr :: addr
ttPeerAddr :: forall id state. TransitionTrace' id state -> id
ttPeerAddr, Transition' st
ttTransition :: Transition' st
ttTransition :: forall id state. TransitionTrace' id state -> Transition' state
ttTransition } = a -> TransitionTrace' addr st
getTransition a
a
           in if Transition' st -> Bool
isFinalTransition Transition' st
ttTransition
                 then case addr
ttPeerAddr addr -> Map addr [a] -> Maybe [a]
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map addr [a]
s of
                        Maybe [a]
Nothing  -> ( addr -> [a] -> Map addr [a] -> Map addr [a]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert addr
ttPeerAddr [a
a] Map addr [a]
s
                                    , Maybe [a]
forall a. Maybe a
Nothing
                                    )
                        Just [a]
trs -> ( addr -> Map addr [a] -> Map addr [a]
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete addr
ttPeerAddr Map addr [a]
s
                                    , [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
trs)
                                    )
                 else ( (Maybe [a] -> Maybe [a]) -> addr -> Map addr [a] -> Map addr [a]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (\case
                                     Maybe [a]
Nothing -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
a]
                                     Just [a]
as -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as)
                                  )
                                  addr
ttPeerAddr Map addr [a]
s
                      , Maybe [a]
forall a. Maybe a
Nothing)
      )
      Map addr [a]
forall k a. Map k a
Map.empty

-- | Like 'groupConns' but can be used to also interleave other types of events.
--
groupConnsEither :: Ord addr
                 => (a -> TransitionTrace' addr st)
                 -> (Transition' st -> Bool)
                 -> Trace r (Either a b)
                 -> Trace r (Either [a] b)
groupConnsEither :: forall addr a st r b.
Ord addr =>
(a -> TransitionTrace' addr st)
-> (Transition' st -> Bool)
-> Trace r (Either a b)
-> Trace r (Either [a] b)
groupConnsEither a -> TransitionTrace' addr st
getTransition Transition' st -> Bool
isFinalTransition =
    (Maybe (Either [a] b) -> Either [a] b)
-> Trace r (Maybe (Either [a] b)) -> Trace r (Either [a] b)
forall a b. (a -> b) -> Trace r a -> Trace r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe (Either [a] b) -> Either [a] b
forall a. HasCallStack => Maybe a -> a
fromJust
  (Trace r (Maybe (Either [a] b)) -> Trace r (Either [a] b))
-> (Trace r (Either a b) -> Trace r (Maybe (Either [a] b)))
-> Trace r (Either a b)
-> Trace r (Either [a] b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (Either [a] b) -> Bool)
-> Trace r (Maybe (Either [a] b)) -> Trace r (Maybe (Either [a] b))
forall b a. (b -> Bool) -> Trace a b -> Trace a b
Trace.filter Maybe (Either [a] b) -> Bool
forall a. Maybe a -> Bool
isJust
  -- there might be some connections in the state, push them onto the 'Trace'
  (Trace r (Maybe (Either [a] b)) -> Trace r (Maybe (Either [a] b)))
-> (Trace r (Either a b) -> Trace r (Maybe (Either [a] b)))
-> Trace r (Either a b)
-> Trace r (Maybe (Either [a] b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Map addr [a]
s, Trace r (Maybe (Either [a] b))
o) -> ([a]
 -> Trace r (Maybe (Either [a] b))
 -> Trace r (Maybe (Either [a] b)))
-> Trace r (Maybe (Either [a] b))
-> [[a]]
-> Trace r (Maybe (Either [a] b))
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\[a]
a Trace r (Maybe (Either [a] b))
as -> Maybe (Either [a] b)
-> Trace r (Maybe (Either [a] b)) -> Trace r (Maybe (Either [a] b))
forall a b. b -> Trace a b -> Trace a b
Trace.Cons (Either [a] b -> Maybe (Either [a] b)
forall a. a -> Maybe a
Just ([a] -> Either [a] b
forall a b. a -> Either a b
Left ([a] -> Either [a] b) -> [a] -> Either [a] b
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
a)) Trace r (Maybe (Either [a] b))
as) Trace r (Maybe (Either [a] b))
o (Map addr [a] -> [[a]]
forall k a. Map k a -> [a]
Map.elems Map addr [a]
s))
  ((Map addr [a], Trace r (Maybe (Either [a] b)))
 -> Trace r (Maybe (Either [a] b)))
-> (Trace r (Either a b)
    -> (Map addr [a], Trace r (Maybe (Either [a] b))))
-> Trace r (Either a b)
-> Trace r (Maybe (Either [a] b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map addr [a] -> r -> (Map addr [a], r))
-> (Map addr [a]
    -> Either a b -> (Map addr [a], Maybe (Either [a] b)))
-> Map addr [a]
-> Trace r (Either a b)
-> (Map addr [a], Trace r (Maybe (Either [a] b)))
forall (t :: * -> * -> *) a b c d e.
Bitraversable t =>
(a -> b -> (a, c))
-> (a -> d -> (a, e)) -> a -> t b d -> (a, t c e)
bimapAccumL
      ( \ Map addr [a]
s r
a -> (Map addr [a]
s, r
a))
      ( \ Map addr [a]
s Either a b
x -> case Either a b
x of
          Left a
a ->
            let TransitionTrace { addr
ttPeerAddr :: forall id state. TransitionTrace' id state -> id
ttPeerAddr :: addr
ttPeerAddr, Transition' st
ttTransition :: forall id state. TransitionTrace' id state -> Transition' state
ttTransition :: Transition' st
ttTransition } = a -> TransitionTrace' addr st
getTransition a
a
             in if Transition' st -> Bool
isFinalTransition Transition' st
ttTransition
                   then case addr
ttPeerAddr addr -> Map addr [a] -> Maybe [a]
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map addr [a]
s of
                          Maybe [a]
Nothing  -> ( addr -> [a] -> Map addr [a] -> Map addr [a]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert addr
ttPeerAddr [a
a] Map addr [a]
s
                                      , Maybe (Either [a] b)
forall a. Maybe a
Nothing
                                      )
                          Just [a]
trs -> ( addr -> Map addr [a] -> Map addr [a]
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete addr
ttPeerAddr Map addr [a]
s
                                      , Either [a] b -> Maybe (Either [a] b)
forall a. a -> Maybe a
Just ([a] -> Either [a] b
forall a b. a -> Either a b
Left ([a] -> Either [a] b) -> [a] -> Either [a] b
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
trs)
                                      )
                   else ( (Maybe [a] -> Maybe [a]) -> addr -> Map addr [a] -> Map addr [a]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (\case
                                       Maybe [a]
Nothing -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
a]
                                       Just [a]
as -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as)
                                    )
                                    addr
ttPeerAddr Map addr [a]
s
                        , Maybe (Either [a] b)
forall a. Maybe a
Nothing)
          Right b
b -> ( Map addr [a]
s, Either [a] b -> Maybe (Either [a] b)
forall a. a -> Maybe a
Just (b -> Either [a] b
forall a b. b -> Either a b
Right b
b) )
      )
      Map addr [a]
forall k a. Map k a
Map.empty

-- | The concrete address type used by simulations.
--
type SimAddr  = Snocket.TestAddress SimAddr_
type SimAddr_ = Int

-- | We use a wrapper for test addresses since the Arbitrary instance for Snocket.TestAddress only
--   generates addresses between 1 and 4.
newtype TestAddr = TestAddr { TestAddr -> SimAddr
unTestAddr :: SimAddr }
  deriving (Int -> TestAddr -> String -> String
[TestAddr] -> String -> String
TestAddr -> String
(Int -> TestAddr -> String -> String)
-> (TestAddr -> String)
-> ([TestAddr] -> String -> String)
-> Show TestAddr
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> TestAddr -> String -> String
showsPrec :: Int -> TestAddr -> String -> String
$cshow :: TestAddr -> String
show :: TestAddr -> String
$cshowList :: [TestAddr] -> String -> String
showList :: [TestAddr] -> String -> String
Show, TestAddr -> TestAddr -> Bool
(TestAddr -> TestAddr -> Bool)
-> (TestAddr -> TestAddr -> Bool) -> Eq TestAddr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TestAddr -> TestAddr -> Bool
== :: TestAddr -> TestAddr -> Bool
$c/= :: TestAddr -> TestAddr -> Bool
/= :: TestAddr -> TestAddr -> Bool
Eq, Eq TestAddr
Eq TestAddr =>
(TestAddr -> TestAddr -> Ordering)
-> (TestAddr -> TestAddr -> Bool)
-> (TestAddr -> TestAddr -> Bool)
-> (TestAddr -> TestAddr -> Bool)
-> (TestAddr -> TestAddr -> Bool)
-> (TestAddr -> TestAddr -> TestAddr)
-> (TestAddr -> TestAddr -> TestAddr)
-> Ord TestAddr
TestAddr -> TestAddr -> Bool
TestAddr -> TestAddr -> Ordering
TestAddr -> TestAddr -> TestAddr
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TestAddr -> TestAddr -> Ordering
compare :: TestAddr -> TestAddr -> Ordering
$c< :: TestAddr -> TestAddr -> Bool
< :: TestAddr -> TestAddr -> Bool
$c<= :: TestAddr -> TestAddr -> Bool
<= :: TestAddr -> TestAddr -> Bool
$c> :: TestAddr -> TestAddr -> Bool
> :: TestAddr -> TestAddr -> Bool
$c>= :: TestAddr -> TestAddr -> Bool
>= :: TestAddr -> TestAddr -> Bool
$cmax :: TestAddr -> TestAddr -> TestAddr
max :: TestAddr -> TestAddr -> TestAddr
$cmin :: TestAddr -> TestAddr -> TestAddr
min :: TestAddr -> TestAddr -> TestAddr
Ord)

instance Arbitrary TestAddr where
  arbitrary :: Gen TestAddr
arbitrary = SimAddr -> TestAddr
TestAddr (SimAddr -> TestAddr) -> (Int -> SimAddr) -> Int -> TestAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SimAddr
forall addr. addr -> TestAddress addr
Snocket.TestAddress (Int -> TestAddr) -> Gen Int -> Gen TestAddr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)


-- | Test property together with classification.
--
data TestProperty = TestProperty {
    TestProperty -> Property
tpProperty            :: !Property,
    -- ^ 'True' if property is true

    TestProperty -> Sum Int
tpNumberOfTransitions :: !(Sum Int),
    -- ^ number of all transitions

    TestProperty -> Sum Int
tpNumberOfConnections :: !(Sum Int),
    -- ^ number of all connections

    TestProperty -> Sum Int
tpNumberOfPrunings    :: !(Sum Int),
    -- ^ number of all connections

    --
    -- classification of connections
    --
    TestProperty -> [NegotiatedDataFlow]
tpNegotiatedDataFlows :: ![NegotiatedDataFlow],
    TestProperty -> [EffectiveDataFlow]
tpEffectiveDataFlows  :: ![EffectiveDataFlow],
    TestProperty -> [Maybe TerminationType]
tpTerminationTypes    :: ![Maybe TerminationType],
    TestProperty -> [ActivityType]
tpActivityTypes       :: ![ActivityType],

    TestProperty -> [Transition' AbstractState]
tpTransitions         :: ![AbstractTransition]

  }

instance Show TestProperty where
    show :: TestProperty -> String
show TestProperty
tp =
      [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"TestProperty "
             , String
"{ tpNumberOfTransitions = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sum Int -> String
forall a. Show a => a -> String
show (TestProperty -> Sum Int
tpNumberOfTransitions TestProperty
tp)
             , String
", tpNumberOfConnections = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sum Int -> String
forall a. Show a => a -> String
show (TestProperty -> Sum Int
tpNumberOfConnections TestProperty
tp)
             , String
", tpNumberOfPrunings = "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sum Int -> String
forall a. Show a => a -> String
show (TestProperty -> Sum Int
tpNumberOfPrunings TestProperty
tp)
             , String
", tpNegotiatedDataFlows = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [NegotiatedDataFlow] -> String
forall a. Show a => a -> String
show (TestProperty -> [NegotiatedDataFlow]
tpNegotiatedDataFlows TestProperty
tp)
             , String
", tpTerminationTypes = "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Maybe TerminationType] -> String
forall a. Show a => a -> String
show (TestProperty -> [Maybe TerminationType]
tpTerminationTypes TestProperty
tp)
             , String
", tpActivityTypes = "       String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ActivityType] -> String
forall a. Show a => a -> String
show (TestProperty -> [ActivityType]
tpActivityTypes TestProperty
tp)
             , String
", tpTransitions = "         String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Transition' AbstractState] -> String
forall a. Show a => a -> String
show (TestProperty -> [Transition' AbstractState]
tpTransitions TestProperty
tp)
             , String
"}"
             ]

instance Semigroup TestProperty where
  <> :: TestProperty -> TestProperty -> TestProperty
(<>) (TestProperty Property
a0 Sum Int
a1 Sum Int
a2 Sum Int
a3 [NegotiatedDataFlow]
a4 [EffectiveDataFlow]
a5 [Maybe TerminationType]
a6 [ActivityType]
a7 [Transition' AbstractState]
a8)
       (TestProperty Property
b0 Sum Int
b1 Sum Int
b2 Sum Int
b3 [NegotiatedDataFlow]
b4 [EffectiveDataFlow]
b5 [Maybe TerminationType]
b6 [ActivityType]
b7 [Transition' AbstractState]
b8) =
      Property
-> Sum Int
-> Sum Int
-> Sum Int
-> [NegotiatedDataFlow]
-> [EffectiveDataFlow]
-> [Maybe TerminationType]
-> [ActivityType]
-> [Transition' AbstractState]
-> TestProperty
TestProperty (Property
a0 Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Property
b0)
                   (Sum Int
a1 Sum Int -> Sum Int -> Sum Int
forall a. Semigroup a => a -> a -> a
<> Sum Int
b1)
                   (Sum Int
a2 Sum Int -> Sum Int -> Sum Int
forall a. Semigroup a => a -> a -> a
<> Sum Int
b2)
                   (Sum Int
a3 Sum Int -> Sum Int -> Sum Int
forall a. Semigroup a => a -> a -> a
<> Sum Int
b3)
                   ([NegotiatedDataFlow]
a4 [NegotiatedDataFlow]
-> [NegotiatedDataFlow] -> [NegotiatedDataFlow]
forall a. Semigroup a => a -> a -> a
<> [NegotiatedDataFlow]
b4)
                   ([EffectiveDataFlow]
a5 [EffectiveDataFlow] -> [EffectiveDataFlow] -> [EffectiveDataFlow]
forall a. Semigroup a => a -> a -> a
<> [EffectiveDataFlow]
b5)
                   ([Maybe TerminationType]
a6 [Maybe TerminationType]
-> [Maybe TerminationType] -> [Maybe TerminationType]
forall a. Semigroup a => a -> a -> a
<> [Maybe TerminationType]
b6)
                   ([ActivityType]
a7 [ActivityType] -> [ActivityType] -> [ActivityType]
forall a. Semigroup a => a -> a -> a
<> [ActivityType]
b7)
                   ([Transition' AbstractState]
a8 [Transition' AbstractState]
-> [Transition' AbstractState] -> [Transition' AbstractState]
forall a. Semigroup a => a -> a -> a
<> [Transition' AbstractState]
b8)

instance Monoid TestProperty where
    mempty :: TestProperty
mempty = Property
-> Sum Int
-> Sum Int
-> Sum Int
-> [NegotiatedDataFlow]
-> [EffectiveDataFlow]
-> [Maybe TerminationType]
-> [ActivityType]
-> [Transition' AbstractState]
-> TestProperty
TestProperty (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True)
                          Sum Int
forall a. Monoid a => a
mempty Sum Int
forall a. Monoid a => a
mempty Sum Int
forall a. Monoid a => a
mempty [NegotiatedDataFlow]
forall a. Monoid a => a
mempty
                          [EffectiveDataFlow]
forall a. Monoid a => a
mempty [Maybe TerminationType]
forall a. Monoid a => a
mempty [ActivityType]
forall a. Monoid a => a
mempty [Transition' AbstractState]
forall a. Monoid a => a
mempty

mkProperty :: TestProperty -> Property
mkProperty :: TestProperty -> Property
mkProperty TestProperty { Property
tpProperty :: TestProperty -> Property
tpProperty :: Property
tpProperty
                        , tpNumberOfTransitions :: TestProperty -> Sum Int
tpNumberOfTransitions = Sum Int
numberOfTransitions_
                        , tpNumberOfConnections :: TestProperty -> Sum Int
tpNumberOfConnections = Sum Int
numberOfConnections_
                        , tpNumberOfPrunings :: TestProperty -> Sum Int
tpNumberOfPrunings = Sum Int
numberOfPrunings_
                        , [NegotiatedDataFlow]
tpNegotiatedDataFlows :: TestProperty -> [NegotiatedDataFlow]
tpNegotiatedDataFlows :: [NegotiatedDataFlow]
tpNegotiatedDataFlows
                        , [EffectiveDataFlow]
tpEffectiveDataFlows :: TestProperty -> [EffectiveDataFlow]
tpEffectiveDataFlows :: [EffectiveDataFlow]
tpEffectiveDataFlows
                        , [Maybe TerminationType]
tpTerminationTypes :: TestProperty -> [Maybe TerminationType]
tpTerminationTypes :: [Maybe TerminationType]
tpTerminationTypes
                        , [ActivityType]
tpActivityTypes :: TestProperty -> [ActivityType]
tpActivityTypes :: [ActivityType]
tpActivityTypes
                        , [Transition' AbstractState]
tpTransitions :: TestProperty -> [Transition' AbstractState]
tpTransitions :: [Transition' AbstractState]
tpTransitions
                        } =
     String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
label (String
"Number of transitions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Int -> String
within_ Int
10 Int
numberOfTransitions_
           )
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
label (String
"Number of connections: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numberOfConnections_
           )
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Pruning"             [Int -> String
forall a. Show a => a -> String
show Int
numberOfPrunings_]
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Negotiated DataFlow" ((NegotiatedDataFlow -> String) -> [NegotiatedDataFlow] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NegotiatedDataFlow -> String
forall a. Show a => a -> String
show [NegotiatedDataFlow]
tpNegotiatedDataFlows)
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Effective DataFLow"  ((EffectiveDataFlow -> String) -> [EffectiveDataFlow] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map EffectiveDataFlow -> String
forall a. Show a => a -> String
show [EffectiveDataFlow]
tpEffectiveDataFlows)
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Termination"         ((Maybe TerminationType -> String)
-> [Maybe TerminationType] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Maybe TerminationType -> String
forall a. Show a => a -> String
show [Maybe TerminationType]
tpTerminationTypes)
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Activity Type"       ((ActivityType -> String) -> [ActivityType] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ActivityType -> String
forall a. Show a => a -> String
show [ActivityType]
tpActivityTypes)
   (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Transitions"         ((Transition' AbstractState -> String)
-> [Transition' AbstractState] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Transition' AbstractState -> String
ppTransition [Transition' AbstractState]
tpTransitions)
   (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Property
tpProperty

mkPropertyPruning :: TestProperty -> Property
mkPropertyPruning :: TestProperty -> Property
mkPropertyPruning tp :: TestProperty
tp@TestProperty { tpNumberOfPrunings :: TestProperty -> Sum Int
tpNumberOfPrunings = Sum Int
numberOfPrunings_ } =
     Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
35 (Int
numberOfPrunings_ Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) String
"Prunings"
   (Property -> Property)
-> (TestProperty -> Property) -> TestProperty -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestProperty -> Property
mkProperty
   (TestProperty -> Property) -> TestProperty -> Property
forall a b. (a -> b) -> a -> b
$ TestProperty
tp

-- classify negotiated data flow
classifyNegotiatedDataFlow :: [AbstractTransition] -> NegotiatedDataFlow
classifyNegotiatedDataFlow :: [Transition' AbstractState] -> NegotiatedDataFlow
classifyNegotiatedDataFlow [Transition' AbstractState]
as =
  case (Transition' AbstractState -> Bool)
-> [Transition' AbstractState] -> Maybe (Transition' AbstractState)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ( \ Transition' AbstractState
tr
             -> case Transition' AbstractState -> AbstractState
forall state. Transition' state -> state
toState Transition' AbstractState
tr of
                  AbstractState
OutboundUniSt    -> Bool
True
                  OutboundDupSt {} -> Bool
True
                  InboundIdleSt {} -> Bool
True
                  AbstractState
_                -> Bool
False
            ) [Transition' AbstractState]
as of
     Maybe (Transition' AbstractState)
Nothing -> NegotiatedDataFlow
NotNegotiated
     Just Transition' AbstractState
tr ->
       case Transition' AbstractState -> AbstractState
forall state. Transition' state -> state
toState Transition' AbstractState
tr of
         AbstractState
OutboundUniSt      -> DataFlow -> NegotiatedDataFlow
NegotiatedDataFlow DataFlow
Unidirectional
         OutboundDupSt {}   -> DataFlow -> NegotiatedDataFlow
NegotiatedDataFlow DataFlow
Duplex
         (InboundIdleSt DataFlow
df) -> DataFlow -> NegotiatedDataFlow
NegotiatedDataFlow DataFlow
df
         AbstractState
_                  -> String -> NegotiatedDataFlow
forall a. HasCallStack => String -> a
error String
"impossible happened!"

-- classify effective data flow
classifyEffectiveDataFlow :: [AbstractTransition] -> EffectiveDataFlow
classifyEffectiveDataFlow :: [Transition' AbstractState] -> EffectiveDataFlow
classifyEffectiveDataFlow [Transition' AbstractState]
as =
  case (Transition' AbstractState -> Bool)
-> [Transition' AbstractState] -> Maybe (Transition' AbstractState)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((AbstractState -> AbstractState -> Bool
forall a. Eq a => a -> a -> Bool
== AbstractState
DuplexSt) (AbstractState -> Bool)
-> (Transition' AbstractState -> AbstractState)
-> Transition' AbstractState
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition' AbstractState -> AbstractState
forall state. Transition' state -> state
toState) [Transition' AbstractState]
as of
    Maybe (Transition' AbstractState)
Nothing -> DataFlow -> EffectiveDataFlow
EffectiveDataFlow DataFlow
Unidirectional
    Just Transition' AbstractState
_  -> DataFlow -> EffectiveDataFlow
EffectiveDataFlow DataFlow
Duplex

-- classify termination
classifyTermination :: [AbstractTransition] -> Maybe TerminationType
classifyTermination :: [Transition' AbstractState] -> Maybe TerminationType
classifyTermination [Transition' AbstractState]
as =
    case [Transition' AbstractState] -> Maybe (Transition' AbstractState)
forall a. [a] -> Maybe a
maybeLast ([Transition' AbstractState] -> Maybe (Transition' AbstractState))
-> [Transition' AbstractState] -> Maybe (Transition' AbstractState)
forall a b. (a -> b) -> a -> b
$ (Transition' AbstractState -> Bool)
-> [Transition' AbstractState] -> [Transition' AbstractState]
forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd
                  (Transition' AbstractState -> Transition' AbstractState -> Bool
forall a. Eq a => a -> a -> Bool
== AbstractState -> AbstractState -> Transition' AbstractState
forall state. state -> state -> Transition' state
Transition AbstractState
TerminatedSt AbstractState
TerminatedSt)
              ([Transition' AbstractState] -> [Transition' AbstractState])
-> [Transition' AbstractState] -> [Transition' AbstractState]
forall a b. (a -> b) -> a -> b
$ (Transition' AbstractState -> Bool)
-> [Transition' AbstractState] -> [Transition' AbstractState]
forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd
                  (Transition' AbstractState -> Transition' AbstractState -> Bool
forall a. Eq a => a -> a -> Bool
== AbstractState -> AbstractState -> Transition' AbstractState
forall state. state -> state -> Transition' state
Transition AbstractState
TerminatedSt AbstractState
UnknownConnectionSt) [Transition' AbstractState]
as of
      Just Transition { fromState :: forall state. Transition' state -> state
fromState = AbstractState
TerminatingSt
                      , toState :: forall state. Transition' state -> state
toState   = AbstractState
TerminatedSt
                      } -> TerminationType -> Maybe TerminationType
forall a. a -> Maybe a
Just TerminationType
CleanTermination
      Just Transition' AbstractState
_            -> TerminationType -> Maybe TerminationType
forall a. a -> Maybe a
Just TerminationType
ErroredTermination
      Maybe (Transition' AbstractState)
Nothing           -> Maybe TerminationType
forall a. Maybe a
Nothing
  where
    maybeLast :: [a] -> Maybe a
    maybeLast :: forall a. [a] -> Maybe a
maybeLast []         = Maybe a
forall a. Maybe a
Nothing
    maybeLast xs :: [a]
xs@(a
_ : [a]
_) = a -> Maybe a
forall a. a -> Maybe a
Just ([a] -> a
forall a. HasCallStack => [a] -> a
last [a]
xs)

-- classify if a connection is active or not
classifyActivityType :: [AbstractTransition] -> ActivityType
classifyActivityType :: [Transition' AbstractState] -> ActivityType
classifyActivityType [Transition' AbstractState]
as =
  case (Transition' AbstractState -> Bool)
-> [Transition' AbstractState] -> Maybe (Transition' AbstractState)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ( \ Transition' AbstractState
tr
             -> case Transition' AbstractState -> AbstractState
forall state. Transition' state -> state
toState Transition' AbstractState
tr of
                  InboundSt     {} -> Bool
True
                  AbstractState
OutboundUniSt    -> Bool
True
                  OutboundDupSt {} -> Bool
True
                  DuplexSt      {} -> Bool
True
                  AbstractState
_                -> Bool
False
            ) [Transition' AbstractState]
as of
    Maybe (Transition' AbstractState)
Nothing -> ActivityType
IdleConn
    Just {} -> ActivityType
ActiveConn

-- classify negotiated data flow
classifyPrunings :: [CM.Trace
                      addr
                      (ConnectionHandlerTrace
                        prctl
                        dataflow)]
                 -> Sum Int
classifyPrunings :: forall addr prctl dataflow.
[Trace addr (ConnectionHandlerTrace prctl dataflow)] -> Sum Int
classifyPrunings =
  Int -> Sum Int
forall a. a -> Sum a
Sum
  (Int -> Sum Int)
-> ([Trace addr (ConnectionHandlerTrace prctl dataflow)] -> Int)
-> [Trace addr (ConnectionHandlerTrace prctl dataflow)]
-> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Trace addr (ConnectionHandlerTrace prctl dataflow)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
  ([Trace addr (ConnectionHandlerTrace prctl dataflow)] -> Int)
-> ([Trace addr (ConnectionHandlerTrace prctl dataflow)]
    -> [Trace addr (ConnectionHandlerTrace prctl dataflow)])
-> [Trace addr (ConnectionHandlerTrace prctl dataflow)]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Trace addr (ConnectionHandlerTrace prctl dataflow) -> Bool)
-> [Trace addr (ConnectionHandlerTrace prctl dataflow)]
-> [Trace addr (ConnectionHandlerTrace prctl dataflow)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ case
               CM.TrPruneConnections {} -> Bool
True
               Trace addr (ConnectionHandlerTrace prctl dataflow)
_                        -> Bool
False
           )


classifyPruning
  :: CM.Trace addr (ConnectionHandlerTrace prctl dataflow)
  -> Sum Int
classifyPruning :: forall addr prctl dataflow.
Trace addr (ConnectionHandlerTrace prctl dataflow) -> Sum Int
classifyPruning CM.TrPruneConnections {} = Int -> Sum Int
forall a. a -> Sum a
Sum Int
1
classifyPruning Trace addr (ConnectionHandlerTrace prctl dataflow)
_                        = Int -> Sum Int
forall a. a -> Sum a
Sum Int
0

newtype ArbDataFlow = ArbDataFlow DataFlow
  deriving Int -> ArbDataFlow -> String -> String
[ArbDataFlow] -> String -> String
ArbDataFlow -> String
(Int -> ArbDataFlow -> String -> String)
-> (ArbDataFlow -> String)
-> ([ArbDataFlow] -> String -> String)
-> Show ArbDataFlow
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ArbDataFlow -> String -> String
showsPrec :: Int -> ArbDataFlow -> String -> String
$cshow :: ArbDataFlow -> String
show :: ArbDataFlow -> String
$cshowList :: [ArbDataFlow] -> String -> String
showList :: [ArbDataFlow] -> String -> String
Show

instance Arbitrary ArbDataFlow where
    arbitrary :: Gen ArbDataFlow
arbitrary = DataFlow -> ArbDataFlow
ArbDataFlow (DataFlow -> ArbDataFlow) -> Gen DataFlow -> Gen ArbDataFlow
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, Gen DataFlow)] -> Gen DataFlow
forall a. [(Int, Gen a)] -> Gen a
frequency [ (Int
3, DataFlow -> Gen DataFlow
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DataFlow
Duplex)
                                          , (Int
1, DataFlow -> Gen DataFlow
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DataFlow
Unidirectional)
                                          ]
    shrink :: ArbDataFlow -> [ArbDataFlow]
shrink (ArbDataFlow DataFlow
Duplex)         = [DataFlow -> ArbDataFlow
ArbDataFlow DataFlow
Unidirectional]
    shrink (ArbDataFlow DataFlow
Unidirectional) = []

data ActivityType
    = IdleConn

    -- | Active connections are once that reach any of the state:
    --
    -- - 'InboundSt'
    -- - 'OutobundUniSt'
    -- - 'OutboundDupSt'
    -- - 'DuplexSt'
    --
    | ActiveConn
    deriving (ActivityType -> ActivityType -> Bool
(ActivityType -> ActivityType -> Bool)
-> (ActivityType -> ActivityType -> Bool) -> Eq ActivityType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ActivityType -> ActivityType -> Bool
== :: ActivityType -> ActivityType -> Bool
$c/= :: ActivityType -> ActivityType -> Bool
/= :: ActivityType -> ActivityType -> Bool
Eq, Int -> ActivityType -> String -> String
[ActivityType] -> String -> String
ActivityType -> String
(Int -> ActivityType -> String -> String)
-> (ActivityType -> String)
-> ([ActivityType] -> String -> String)
-> Show ActivityType
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ActivityType -> String -> String
showsPrec :: Int -> ActivityType -> String -> String
$cshow :: ActivityType -> String
show :: ActivityType -> String
$cshowList :: [ActivityType] -> String -> String
showList :: [ActivityType] -> String -> String
Show)

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

data NegotiatedDataFlow
    = NotNegotiated

    -- | Negotiated value of 'DataFlow'
    | NegotiatedDataFlow DataFlow
    deriving (NegotiatedDataFlow -> NegotiatedDataFlow -> Bool
(NegotiatedDataFlow -> NegotiatedDataFlow -> Bool)
-> (NegotiatedDataFlow -> NegotiatedDataFlow -> Bool)
-> Eq NegotiatedDataFlow
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NegotiatedDataFlow -> NegotiatedDataFlow -> Bool
== :: NegotiatedDataFlow -> NegotiatedDataFlow -> Bool
$c/= :: NegotiatedDataFlow -> NegotiatedDataFlow -> Bool
/= :: NegotiatedDataFlow -> NegotiatedDataFlow -> Bool
Eq, Int -> NegotiatedDataFlow -> String -> String
[NegotiatedDataFlow] -> String -> String
NegotiatedDataFlow -> String
(Int -> NegotiatedDataFlow -> String -> String)
-> (NegotiatedDataFlow -> String)
-> ([NegotiatedDataFlow] -> String -> String)
-> Show NegotiatedDataFlow
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> NegotiatedDataFlow -> String -> String
showsPrec :: Int -> NegotiatedDataFlow -> String -> String
$cshow :: NegotiatedDataFlow -> String
show :: NegotiatedDataFlow -> String
$cshowList :: [NegotiatedDataFlow] -> String -> String
showList :: [NegotiatedDataFlow] -> String -> String
Show)

data EffectiveDataFlow
    -- | Unlike the negotiated 'DataFlow' this indicates if the connection has
    -- ever been in 'DuplexSt'
    --
    = EffectiveDataFlow DataFlow
    deriving (EffectiveDataFlow -> EffectiveDataFlow -> Bool
(EffectiveDataFlow -> EffectiveDataFlow -> Bool)
-> (EffectiveDataFlow -> EffectiveDataFlow -> Bool)
-> Eq EffectiveDataFlow
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EffectiveDataFlow -> EffectiveDataFlow -> Bool
== :: EffectiveDataFlow -> EffectiveDataFlow -> Bool
$c/= :: EffectiveDataFlow -> EffectiveDataFlow -> Bool
/= :: EffectiveDataFlow -> EffectiveDataFlow -> Bool
Eq, Int -> EffectiveDataFlow -> String -> String
[EffectiveDataFlow] -> String -> String
EffectiveDataFlow -> String
(Int -> EffectiveDataFlow -> String -> String)
-> (EffectiveDataFlow -> String)
-> ([EffectiveDataFlow] -> String -> String)
-> Show EffectiveDataFlow
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> EffectiveDataFlow -> String -> String
showsPrec :: Int -> EffectiveDataFlow -> String -> String
$cshow :: EffectiveDataFlow -> String
show :: EffectiveDataFlow -> String
$cshowList :: [EffectiveDataFlow] -> String -> String
showList :: [EffectiveDataFlow] -> String -> String
Show)

within_ :: Int -> Int -> String
within_ :: Int -> Int -> String
within_ Int
_ Int
0 = String
"0"
within_ Int
a Int
b = let x :: Int
x = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
a in
              [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ if Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
a
                         then String
"1"
                         else Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
a
                     , String
" - "
                     , Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
                     ]

ppTransition :: AbstractTransition -> String
ppTransition :: Transition' AbstractState -> String
ppTransition Transition {AbstractState
fromState :: forall state. Transition' state -> state
fromState :: AbstractState
fromState, AbstractState
toState :: forall state. Transition' state -> state
toState :: AbstractState
toState} =
    String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%-30s → %s" (AbstractState -> String
forall a. Show a => a -> String
show AbstractState
fromState) (AbstractState -> String
forall a. Show a => a -> String
show AbstractState
toState)