-- | Monadic interface for writing /Dynamic Logic/ properties.
--
-- This interface offers a much nicer experience than manipulating the
-- expressions it is implemented on top of, especially as it improves
-- readability. It's still possible to express properties as pure
-- expressions using the `Test.QuickCheck.DynamicLogic.Internal` module
-- and it might make sense depending on the context and the kind of
-- properties one wants to express.
module Test.QuickCheck.DynamicLogic (
  DL,
  action,
  failingAction,
  anyAction,
  anyActions,
  anyActions_,
  stopping,
  weight,
  getSize,
  getModelStateDL,
  getVarContextDL,
  forAllVar,
  assert,
  assertModel,
  monitorDL,
  forAllQ,
  forAllNonVariableQ,
  forAllDL,
  forAllMappedDL,
  forAllUniqueDL,
  DL.DynLogicModel (..),
  module Test.QuickCheck.DynamicLogic.Quantify,
) where

import Control.Applicative
import Control.Monad
import Data.Typeable
import Test.QuickCheck hiding (getSize)
import Test.QuickCheck.DynamicLogic.Internal qualified as DL
import Test.QuickCheck.DynamicLogic.Quantify
import Test.QuickCheck.StateModel

-- | The `DL` monad provides a nicer interface to dynamic logic formulae than the plain API.
--   It's a continuation monad producing a `DL.DynFormula` formula, with a state component (with
--   variable context) threaded through.
newtype DL s a = DL {forall s a.
DL s a
-> Annotated s
-> (a -> Annotated s -> DynFormula s)
-> DynFormula s
unDL :: Annotated s -> (a -> Annotated s -> DL.DynFormula s) -> DL.DynFormula s}
  deriving ((forall a b. (a -> b) -> DL s a -> DL s b)
-> (forall a b. a -> DL s b -> DL s a) -> Functor (DL s)
forall a b. a -> DL s b -> DL s a
forall a b. (a -> b) -> DL s a -> DL s b
forall s a b. a -> DL s b -> DL s a
forall s a b. (a -> b) -> DL s a -> DL s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall s a b. (a -> b) -> DL s a -> DL s b
fmap :: forall a b. (a -> b) -> DL s a -> DL s b
$c<$ :: forall s a b. a -> DL s b -> DL s a
<$ :: forall a b. a -> DL s b -> DL s a
Functor)

instance Applicative (DL s) where
  pure :: forall a. a -> DL s a
pure a
x = (Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s a)
-> (Annotated s
    -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall a b. (a -> b) -> a -> b
$ \Annotated s
s a -> Annotated s -> DynFormula s
k -> a -> Annotated s -> DynFormula s
k a
x Annotated s
s
  <*> :: forall a b. DL s (a -> b) -> DL s a -> DL s b
(<*>) = DL s (a -> b) -> DL s a -> DL s b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Alternative (DL s) where
  empty :: forall a. DL s a
empty = (Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s a)
-> (Annotated s
    -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall a b. (a -> b) -> a -> b
$ \Annotated s
_ a -> Annotated s -> DynFormula s
_ -> DynFormula s
forall s. DynFormula s
DL.ignore
  DL Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h <|> :: forall a. DL s a -> DL s a -> DL s a
<|> DL Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
j = (Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s a)
-> (Annotated s
    -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall a b. (a -> b) -> a -> b
$ \Annotated s
s a -> Annotated s -> DynFormula s
k -> Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h Annotated s
s a -> Annotated s -> DynFormula s
k DynFormula s -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s -> DynFormula s
DL.||| Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
j Annotated s
s a -> Annotated s -> DynFormula s
k

instance Monad (DL s) where
  return :: forall a. a -> DL s a
return = a -> DL s a
forall a. a -> DL s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  DL Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h >>= :: forall a b. DL s a -> (a -> DL s b) -> DL s b
>>= a -> DL s b
j = (Annotated s -> (b -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s b
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (b -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s b)
-> (Annotated s
    -> (b -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s b
forall a b. (a -> b) -> a -> b
$ \Annotated s
s b -> Annotated s -> DynFormula s
k -> Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s
h Annotated s
s ((a -> Annotated s -> DynFormula s) -> DynFormula s)
-> (a -> Annotated s -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \a
x Annotated s
s1 -> DL s b
-> Annotated s
-> (b -> Annotated s -> DynFormula s)
-> DynFormula s
forall s a.
DL s a
-> Annotated s
-> (a -> Annotated s -> DynFormula s)
-> DynFormula s
unDL (a -> DL s b
j a
x) Annotated s
s1 b -> Annotated s -> DynFormula s
k

instance MonadFail (DL s) where
  fail :: forall a. String -> DL s a
fail = String -> DL s a
forall s a. String -> DL s a
errorDL

action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
action :: forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s (Var a)
action Action s a
cmd = (Annotated s
 -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s (Var a)
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s (Var a))
-> (Annotated s
    -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s (Var a)
forall a b. (a -> b) -> a -> b
$ \Annotated s
_ Var a -> Annotated s -> DynFormula s
k -> Action s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
DL.after Action s a
cmd Var a -> Annotated s -> DynFormula s
k

failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
failingAction :: forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> DL s ()
failingAction Action s a
cmd = (Annotated s
 -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s ())
-> (Annotated s
    -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall a b. (a -> b) -> a -> b
$ \Annotated s
_ () -> Annotated s -> DynFormula s
k -> Action s a -> (Annotated s -> DynFormula s) -> DynFormula s
forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> (Annotated s -> DynFormula s) -> DynFormula s
DL.afterNegative Action s a
cmd (() -> Annotated s -> DynFormula s
k ())

anyAction :: DL s ()
anyAction :: forall s. DL s ()
anyAction = (Annotated s
 -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s ())
-> (Annotated s
    -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall a b. (a -> b) -> a -> b
$ \Annotated s
_ () -> Annotated s -> DynFormula s
k -> (Annotated s -> DynFormula s) -> DynFormula s
forall s. (Annotated s -> DynFormula s) -> DynFormula s
DL.afterAny ((Annotated s -> DynFormula s) -> DynFormula s)
-> (Annotated s -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ () -> Annotated s -> DynFormula s
k ()

anyActions :: Int -> DL s ()
anyActions :: forall s. Int -> DL s ()
anyActions Int
n =
  DL s ()
forall s. DL s ()
stopping
    DL s () -> DL s () -> DL s ()
forall a. DL s a -> DL s a -> DL s a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> () -> DL s ()
forall a. a -> DL s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    DL s () -> DL s () -> DL s ()
forall a. DL s a -> DL s a -> DL s a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Double -> DL s ()
forall s. Double -> DL s ()
weight (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) DL s () -> DL s () -> DL s ()
forall a b. DL s a -> DL s b -> DL s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DL s ()
forall s. DL s ()
anyAction DL s () -> DL s () -> DL s ()
forall a b. DL s a -> DL s b -> DL s b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> DL s ()
forall s. Int -> DL s ()
anyActions Int
n)

-- average number of actions same as average length of a list
anyActions_ :: DL s ()
anyActions_ :: forall s. DL s ()
anyActions_ = do
  Int
n <- DL s Int
forall s. DL s Int
getSize
  Int -> DL s ()
forall s. Int -> DL s ()
anyActions (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

stopping :: DL s ()
stopping :: forall s. DL s ()
stopping = (Annotated s
 -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s ())
-> (Annotated s
    -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall a b. (a -> b) -> a -> b
$ \Annotated s
s () -> Annotated s -> DynFormula s
k -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s
DL.toStop (() -> Annotated s -> DynFormula s
k () Annotated s
s)

weight :: Double -> DL s ()
weight :: forall s. Double -> DL s ()
weight Double
w = (Annotated s
 -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s ())
-> (Annotated s
    -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall a b. (a -> b) -> a -> b
$ \Annotated s
s () -> Annotated s -> DynFormula s
k -> Double -> DynFormula s -> DynFormula s
forall s. Double -> DynFormula s -> DynFormula s
DL.weight Double
w (() -> Annotated s -> DynFormula s
k () Annotated s
s)

getSize :: DL s Int
getSize :: forall s. DL s Int
getSize = (Annotated s
 -> (Int -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s Int
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (Int -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s Int)
-> (Annotated s
    -> (Int -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s Int
forall a b. (a -> b) -> a -> b
$ \Annotated s
s Int -> Annotated s -> DynFormula s
k -> (Int -> DynFormula s) -> DynFormula s
forall s. (Int -> DynFormula s) -> DynFormula s
DL.withSize ((Int -> DynFormula s) -> DynFormula s)
-> (Int -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> Int -> Annotated s -> DynFormula s
k Int
n Annotated s
s

getModelStateDL :: DL s s
getModelStateDL :: forall s. DL s s
getModelStateDL = (Annotated s -> (s -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s s
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (s -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s s)
-> (Annotated s
    -> (s -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s s
forall a b. (a -> b) -> a -> b
$ \Annotated s
s s -> Annotated s -> DynFormula s
k -> s -> Annotated s -> DynFormula s
k (Annotated s -> s
forall state. Annotated state -> state
underlyingState Annotated s
s) Annotated s
s

getVarContextDL :: DL s VarContext
getVarContextDL :: forall s. DL s VarContext
getVarContextDL = (Annotated s
 -> (VarContext -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s VarContext
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (VarContext -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s VarContext)
-> (Annotated s
    -> (VarContext -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s VarContext
forall a b. (a -> b) -> a -> b
$ \Annotated s
s VarContext -> Annotated s -> DynFormula s
k -> VarContext -> Annotated s -> DynFormula s
k (Annotated s -> VarContext
forall state. Annotated state -> VarContext
vars Annotated s
s) Annotated s
s

forAllVar :: forall a s. Typeable a => DL s (Var a)
forAllVar :: forall a s. Typeable a => DL s (Var a)
forAllVar = do
  [Var a]
xs <- VarContext -> [Var a]
forall a. Typeable a => VarContext -> [Var a]
ctxAtType (VarContext -> [Var a]) -> DL s VarContext -> DL s [Var a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DL s VarContext
forall s. DL s VarContext
getVarContextDL
  Quantification (Var a)
-> DL s (Quantifies (Quantification (Var a)))
forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ (Quantification (Var a)
 -> DL s (Quantifies (Quantification (Var a))))
-> Quantification (Var a)
-> DL s (Quantifies (Quantification (Var a)))
forall a b. (a -> b) -> a -> b
$ [Var a] -> Quantification (Var a)
forall a. Eq a => [a] -> Quantification a
elementsQ [Var a]
xs

errorDL :: String -> DL s a
errorDL :: forall s a. String -> DL s a
errorDL String
name = (Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s a)
-> (Annotated s
    -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall a b. (a -> b) -> a -> b
$ \Annotated s
_ a -> Annotated s -> DynFormula s
_ -> String -> DynFormula s
forall s. String -> DynFormula s
DL.errorDL String
name

-- | Fail if the boolean is @False@.
--
--   Equivalent to
--
-- @
-- assert msg b = unless b (fail msg)
-- @
assert :: String -> Bool -> DL s ()
assert :: forall s. String -> Bool -> DL s ()
assert String
name Bool
b = if Bool
b then () -> DL s ()
forall a. a -> DL s a
forall (m :: * -> *) a. Monad m => a -> m a
return () else String -> DL s ()
forall s a. String -> DL s a
errorDL String
name

assertModel :: String -> (s -> Bool) -> DL s ()
assertModel :: forall s. String -> (s -> Bool) -> DL s ()
assertModel String
name s -> Bool
p = String -> Bool -> DL s ()
forall s. String -> Bool -> DL s ()
assert String
name (Bool -> DL s ()) -> (s -> Bool) -> s -> DL s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Bool
p (s -> DL s ()) -> DL s s -> DL s ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< DL s s
forall s. DL s s
getModelStateDL

monitorDL :: (Property -> Property) -> DL s ()
monitorDL :: forall s. (Property -> Property) -> DL s ()
monitorDL Property -> Property
f = (Annotated s
 -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s ())
-> (Annotated s
    -> (() -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s ()
forall a b. (a -> b) -> a -> b
$ \Annotated s
s () -> Annotated s -> DynFormula s
k -> (Property -> Property) -> DynFormula s -> DynFormula s
forall s. (Property -> Property) -> DynFormula s -> DynFormula s
DL.monitorDL Property -> Property
f (() -> Annotated s -> DynFormula s
k () Annotated s
s)

-- | Generate a random value using the given `Quantification` (or list/tuple of quantifications).
--   Generated values will only shrink to smaller values that could also have been generated.
forAllQ :: Quantifiable q => q -> DL s (Quantifies q)
forAllQ :: forall q s. Quantifiable q => q -> DL s (Quantifies q)
forAllQ q
q = (Annotated s
 -> (Quantifies q -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s (Quantifies q)
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (Quantifies q -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s (Quantifies q))
-> (Annotated s
    -> (Quantifies q -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s (Quantifies q)
forall a b. (a -> b) -> a -> b
$ \Annotated s
s Quantifies q -> Annotated s -> DynFormula s
k -> q -> (Quantifies q -> DynFormula s) -> DynFormula s
forall q s.
Quantifiable q =>
q -> (Quantifies q -> DynFormula s) -> DynFormula s
DL.forAllQ q
q ((Quantifies q -> DynFormula s) -> DynFormula s)
-> (Quantifies q -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Quantifies q
x -> Quantifies q -> Annotated s -> DynFormula s
k Quantifies q
x Annotated s
s

-- | Generate a random value using the given `Quantification` (or list/tuple of quantifications).
--   Generated values will only shrink to smaller values that could also have been generated.
forAllNonVariableQ :: QuantifyConstraints (HasNoVariables a) => Quantification a -> DL s a
forAllNonVariableQ :: forall a s.
QuantifyConstraints (HasNoVariables a) =>
Quantification a -> DL s a
forAllNonVariableQ Quantification a
q = (Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall s a.
(Annotated s -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
DL ((Annotated s
  -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
 -> DL s a)
-> (Annotated s
    -> (a -> Annotated s -> DynFormula s) -> DynFormula s)
-> DL s a
forall a b. (a -> b) -> a -> b
$ \Annotated s
s a -> Annotated s -> DynFormula s
k -> Quantification (HasNoVariables a)
-> (Quantifies (Quantification (HasNoVariables a)) -> DynFormula s)
-> DynFormula s
forall q s.
Quantifiable q =>
q -> (Quantifies q -> DynFormula s) -> DynFormula s
DL.forAllQ (Quantification a -> Quantification (HasNoVariables a)
forall a. Quantification a -> Quantification (HasNoVariables a)
hasNoVariablesQ Quantification a
q) ((Quantifies (Quantification (HasNoVariables a)) -> DynFormula s)
 -> DynFormula s)
-> (Quantifies (Quantification (HasNoVariables a)) -> DynFormula s)
-> DynFormula s
forall a b. (a -> b) -> a -> b
$ \(HasNoVariables a
x) -> a -> Annotated s -> DynFormula s
k a
x Annotated s
s

runDL :: Annotated s -> DL s () -> DL.DynFormula s
runDL :: forall s. Annotated s -> DL s () -> DynFormula s
runDL Annotated s
s DL s ()
dl = DL s ()
-> Annotated s
-> (() -> Annotated s -> DynFormula s)
-> DynFormula s
forall s a.
DL s a
-> Annotated s
-> (a -> Annotated s -> DynFormula s)
-> DynFormula s
unDL DL s ()
dl Annotated s
s ((() -> Annotated s -> DynFormula s) -> DynFormula s)
-> (() -> Annotated s -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \()
_ Annotated s
_ -> DynFormula s
forall s. DynFormula s
DL.passTest

forAllUniqueDL
  :: (DL.DynLogicModel s, Testable a)
  => Annotated s
  -> DL s ()
  -> (Actions s -> a)
  -> Property
forAllUniqueDL :: forall s a.
(DynLogicModel s, Testable a) =>
Annotated s -> DL s () -> (Actions s -> a) -> Property
forAllUniqueDL Annotated s
initState DL s ()
d = Annotated s -> DynFormula s -> (Actions s -> a) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
Annotated s -> DynFormula s -> (Actions s -> a) -> Property
DL.forAllUniqueScripts Annotated s
initState (Annotated s -> DL s () -> DynFormula s
forall s. Annotated s -> DL s () -> DynFormula s
runDL Annotated s
initState DL s ()
d)

forAllDL
  :: (DL.DynLogicModel s, Testable a)
  => DL s ()
  -> (Actions s -> a)
  -> Property
forAllDL :: forall s a.
(DynLogicModel s, Testable a) =>
DL s () -> (Actions s -> a) -> Property
forAllDL DL s ()
d = DynFormula s -> (Actions s -> a) -> Property
forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
DL.forAllScripts (Annotated s -> DL s () -> DynFormula s
forall s. Annotated s -> DL s () -> DynFormula s
runDL Annotated s
forall state. StateModel state => Annotated state
initialAnnotatedState DL s ()
d)

forAllMappedDL
  :: (DL.DynLogicModel s, Testable a)
  => (rep -> DL.DynLogicTest s)
  -> (DL.DynLogicTest s -> rep)
  -> (Actions s -> srep)
  -> DL s ()
  -> (srep -> a)
  -> Property
forAllMappedDL :: forall s a rep srep.
(DynLogicModel s, Testable a) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> (Actions s -> srep)
-> DL s ()
-> (srep -> a)
-> Property
forAllMappedDL rep -> DynLogicTest s
to DynLogicTest s -> rep
from Actions s -> srep
fromScript DL s ()
d srep -> a
prop =
  (rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
forall s a rep.
(DynLogicModel s, Testable a) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
DL.forAllMappedScripts rep -> DynLogicTest s
to DynLogicTest s -> rep
from (Annotated s -> DL s () -> DynFormula s
forall s. Annotated s -> DL s () -> DynFormula s
runDL Annotated s
forall state. StateModel state => Annotated state
initialAnnotatedState DL s ()
d) (srep -> a
prop (srep -> a) -> (Actions s -> srep) -> Actions s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions s -> srep
fromScript)