{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.QuickCheck.DynamicLogic.Core (
  module Test.QuickCheck.DynamicLogic.Quantify,
  DynLogic,
  DynPred,
  DynFormula,
  DynLogicModel (..),
  DynLogicTest (..),
  TestStep (..),
  ignore,
  passTest,
  afterAny,
  after,
  (|||),
  forAllQ,
  weight,
  withSize,
  toStop,
  done,
  errorDL,
  monitorDL,
  always,
  forAllScripts,
  forAllScripts_,
  withDLScript,
  withDLScriptPrefix,
  forAllMappedScripts,
  forAllMappedScripts_,
  forAllUniqueScripts,
  propPruningGeneratedScriptIsNoop,
) where

import Control.Applicative
import Data.List
import Data.Typeable
import Test.QuickCheck hiding (generate)
import Test.QuickCheck.DynamicLogic.CanGenerate
import Test.QuickCheck.DynamicLogic.Quantify
import Test.QuickCheck.DynamicLogic.SmartShrinking
import Test.QuickCheck.DynamicLogic.Utils qualified as QC
import Test.QuickCheck.StateModel

-- | A `DynFormula` may depend on the QuickCheck size parameter
newtype DynFormula s = DynFormula {forall s. DynFormula s -> Int -> DynLogic s
unDynFormula :: Int -> DynLogic s}

-- | Base Dynamic logic formulae language.
-- Formulae are parameterised
-- over the type of state `s` to which they apply. A `DynLogic` value
-- cannot be constructed directly, one has to use the various "smart
-- constructors" provided, see the /Building formulae/ section.
data DynLogic s
  = -- | False
    EmptySpec
  | -- | True
    Stop
  | -- | After any action the predicate should hold
    AfterAny (DynPred s)
  | -- | Choice (angelic or demonic)
    Alt ChoiceType (DynLogic s) (DynLogic s)
  | -- | Prefer this branch if trying to stop.
    Stopping (DynLogic s)
  | -- | After a specific action the predicate should hold
    After (Any (Action s)) (DynPred s)
  | -- | Adjust the probability of picking a branch
    Weight Double (DynLogic s)
  | -- | Generating a random value
    forall a.
    (Eq a, Show a, Typeable a) =>
    ForAll (Quantification a) (a -> DynLogic s)
  | -- | Apply a QuickCheck property modifier (like `tabulate` or `collect`)
    Monitor (Property -> Property) (DynLogic s)

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

type DynPred s = s -> DynLogic s

-- * Building formulae

-- | `False` for DL formulae.
ignore :: DynFormula s

-- | `True` for DL formulae.
passTest :: DynFormula s

-- | Given `f` must be `True` given /any/ state.
afterAny :: (s -> DynFormula s) -> DynFormula s

-- | Given `f` must be `True` after /some/ action.
-- `f` is passed the state resulting from executing the `Action`.
after ::
  (Show a, Typeable a, Eq (Action s a)) =>
  Action s a ->
  (s -> DynFormula s) ->
  DynFormula s

-- | Disjunction for DL formulae.
-- Is `True` if either formula is `True`. The choice is /angelic/, ie. it is
-- always made by the "caller". This is  mostly important in case a test is
-- `Stuck`.
(|||) :: DynFormula s -> DynFormula s -> DynFormula s

-- | First-order quantification of variables.
-- Formula @f@ is `True` iff. it is `True` /for all/ possible values of `q`. The
-- underlying framework will generate values of `q` and check the formula holds
-- for those values. `Quantifiable` values are thus values that can be generated
-- and checked and the `Test.QuickCheck.DynamicLogic.Quantify` module defines
-- basic combinators to build those from building blocks.
forAllQ ::
  Quantifiable q =>
  q ->
  (Quantifies q -> DynFormula s) ->
  DynFormula s

-- | Adjust weight for selecting formula.
-- This is mostly useful in relation with `(|||)` combinator, in order to tweak the
-- priority for generating the next step(s) of the test that matches the formula.
weight :: Double -> DynFormula s -> DynFormula s
-- ??
withSize :: (Int -> DynFormula s) -> DynFormula s
-- ??
toStop :: DynFormula s -> DynFormula s

-- | Successfully ends the test.
done :: s -> DynFormula s

-- | Ends test with given error message.
errorDL :: String -> DynFormula s

-- | Embed QuickCheck's monitoring functions (eg. `label`, `tabulate`) in
-- a formula.
-- This is useful to improve the reporting from test execution, esp. in the
-- case of failures.
monitorDL :: (Property -> Property) -> DynFormula s -> DynFormula s

-- | Formula should hold at any state.
-- In effect this leads to exploring alternatives from a given state `s` and ensuring
-- formula holds in all those states.
always :: (s -> DynFormula s) -> (s -> DynFormula s)

ignore :: forall s. DynFormula s
ignore = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall s. DynLogic s
EmptySpec
passTest :: forall s. DynFormula s
passTest = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall s. DynLogic s
Stop
afterAny :: forall s. (s -> DynFormula s) -> DynFormula s
afterAny s -> DynFormula s
f = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s. DynPred s -> DynLogic s
AfterAny forall a b. (a -> b) -> a -> b
$ \s
s -> forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (s -> DynFormula s
f s
s) Int
n
after :: forall a s.
(Show a, Typeable a, Eq (Action s a)) =>
Action s a -> (s -> DynFormula s) -> DynFormula s
after Action s a
act s -> DynFormula s
f = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s. Any (Action s) -> DynPred s -> DynLogic s
After (forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
act) forall a b. (a -> b) -> a -> b
$ \s
s -> forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (s -> DynFormula s
f s
s) Int
n
DynFormula Int -> DynLogic s
f ||| :: forall s. DynFormula s -> DynFormula s -> DynFormula s
||| DynFormula Int -> DynLogic s
g = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
Angelic (Int -> DynLogic s
f Int
n) (Int -> DynLogic s
g Int
n)

-- In formulae, we use only angelic
-- choice. But it becomes demonic after one
-- step (that is, the choice has been made).
forAllQ :: forall q s.
Quantifiable q =>
q -> (Quantifies q -> DynFormula s) -> DynFormula s
forAllQ q
q Quantifies q -> DynFormula s
f
  | forall a. Quantification a -> Bool
isEmptyQ Quantification (Quantifies q)
q' = forall s. DynFormula s
ignore
  | Bool
otherwise = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s a.
(Eq a, Show a, Typeable a) =>
Quantification a -> (a -> DynLogic s) -> DynLogic s
ForAll Quantification (Quantifies q)
q' forall a b. (a -> b) -> a -> b
$ (forall a b. (a -> b) -> a -> b
$ Int
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. DynFormula s -> Int -> DynLogic s
unDynFormula forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantifies q -> DynFormula s
f
 where
  q' :: Quantification (Quantifies q)
q' = forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify q
q

weight :: forall s. Double -> DynFormula s -> DynFormula s
weight Double
w DynFormula s
f = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f

withSize :: forall s. (Int -> DynFormula s) -> DynFormula s
withSize Int -> DynFormula s
f = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (Int -> DynFormula s
f Int
n) Int
n

toStop :: forall s. DynFormula s -> DynFormula s
toStop (DynFormula Int -> DynLogic s
f) = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ forall s. DynLogic s -> DynLogic s
Stopping forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DynLogic s
f

done :: forall s. s -> DynFormula s
done s
_ = forall s. DynFormula s
passTest

errorDL :: forall s. String -> DynFormula s
errorDL String
s = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall s. Any (Action s) -> DynPred s -> DynLogic s
After (forall (f :: * -> *). String -> Any f
Error String
s) (forall a b. a -> b -> a
const forall s. DynLogic s
EmptySpec)

monitorDL :: forall s. (Property -> Property) -> DynFormula s -> DynFormula s
monitorDL Property -> Property
m (DynFormula Int -> DynLogic s
f) = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DynLogic s
f

always :: forall s. (s -> DynFormula s) -> s -> DynFormula s
always s -> DynFormula s
p s
s = forall s. (Int -> DynFormula s) -> DynFormula s
withSize forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s. DynFormula s -> DynFormula s
toStop (s -> DynFormula s
p s
s) forall s. DynFormula s -> DynFormula s -> DynFormula s
||| s -> DynFormula s
p s
s forall s. DynFormula s -> DynFormula s -> DynFormula s
||| forall s. Double -> DynFormula s -> DynFormula s
weight (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) (forall s. (s -> DynFormula s) -> DynFormula s
afterAny (forall s. (s -> DynFormula s) -> s -> DynFormula s
always s -> DynFormula s
p))

data DynLogicTest s
  = BadPrecondition [TestStep s] [Any (Action s)] s
  | Looping [TestStep s]
  | Stuck [TestStep s] s
  | DLScript [TestStep s]

data TestStep s
  = Do (Step s)
  | forall a. (Eq a, Show a, Typeable a) => Witness a

instance Eq (TestStep s) where
  Do Step s
s == :: TestStep s -> TestStep s -> Bool
== Do Step s
s' = Step s
s forall a. Eq a => a -> a -> Bool
== Step s
s'
  Witness (a
a :: a) == Witness (a
a' :: a') =
    case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
      Just a :~: a
Refl -> a
a forall a. Eq a => a -> a -> Bool
== a
a'
      Maybe (a :~: a)
Nothing -> Bool
False
  TestStep s
_ == TestStep s
_ = Bool
False

instance StateModel s => Show (TestStep s) where
  show :: TestStep s -> String
show (Do Step s
step) = String
"Do $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Step s
step
  show (Witness a
a) = String
"Witness (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf a
a) forall a. [a] -> [a] -> [a]
++ String
")"

instance StateModel s => Show (DynLogicTest s) where
  show :: DynLogicTest s -> String
show (BadPrecondition [TestStep s]
as [Any (Action s)]
bads s
s) =
    [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
      [String
"BadPrecondition"]
        forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [TestStep s]
as)
        forall a. [a] -> [a] -> [a]
++ [String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Eq a => [a] -> [a]
nub [Any (Action s)]
bads)]
        forall a. [a] -> [a] -> [a]
++ [String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 s
s String
""]
  show (Looping [TestStep s]
as) =
    [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ String
"Looping" forall a. a -> [a] -> [a]
: [String] -> [String]
bracket (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [TestStep s]
as)
  show (Stuck [TestStep s]
as s
s) =
    [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ [String
"Stuck"] forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [TestStep s]
as) forall a. [a] -> [a] -> [a]
++ [String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 s
s String
""]
  show (DLScript [TestStep s]
as) =
    [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ String
"DLScript" forall a. a -> [a] -> [a]
: [String] -> [String]
bracket (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [TestStep s]
as)

bracket :: [String] -> [String]
bracket :: [String] -> [String]
bracket [] = [String
"  []"]
bracket [String
s] = [String
"  [" forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
"]"]
bracket (String
first : [String]
rest) =
  [String
"  [" forall a. [a] -> [a] -> [a]
++ String
first forall a. [a] -> [a] -> [a]
++ String
", "]
    forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map ((String
"   " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ String
", ")) (forall a. [a] -> [a]
init [String]
rest)
    forall a. [a] -> [a] -> [a]
++ [String
"   " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> a
last [String]
rest forall a. [a] -> [a] -> [a]
++ String
"]"]

-- | Restricted calls are not generated by "AfterAny"; they are included
-- in tests explicitly using "After" in order to check specific
-- properties at controlled times, so they are likely to fail if
-- invoked at other times.
class StateModel s => DynLogicModel s where
  restricted :: Action s a -> Bool
  restricted Action s a
_ = Bool
False

-- * Generate Properties

-- | Simplest "execution" function for `DynFormula`.
-- Turns a given a `DynFormula` paired with an interpreter function to produce some result from an

--- `Actions` sequence into a proper `Property` than can then be run by QuickCheck.
forAllScripts ::
  (DynLogicModel s, Testable a) =>
  DynFormula s ->
  (Actions s -> a) ->
  Property
forAllScripts :: forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
forAllScripts = forall s a rep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
forAllMappedScripts forall a. a -> a
id forall a. a -> a
id

-- | `Property` function suitable for formulae without choice.
forAllUniqueScripts ::
  (DynLogicModel s, Testable a) =>
  Int ->
  s ->
  DynFormula s ->
  (Actions s -> a) ->
  Property
forAllUniqueScripts :: forall s a.
(DynLogicModel s, Testable a) =>
Int -> s -> DynFormula s -> (Actions s -> a) -> Property
forAllUniqueScripts Int
n s
s DynFormula s
f Actions s -> a
k =
  forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize forall a b. (a -> b) -> a -> b
$ \Int
sz ->
    let d :: DynLogic s
d = forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
sz
     in case forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> m (DynLogicTest s)
generate forall (m :: * -> *) s.
(MonadFail m, DynLogicModel s) =>
s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep DynLogic s
d Int
n s
s Int
500 [] of
          Maybe (DynLogicTest s)
Nothing -> forall prop. Testable prop => String -> prop -> Property
counterexample String
"Generating Non-unique script in forAllUniqueScripts" Bool
False
          Just DynLogicTest s
test -> forall s. StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
d DynLogicTest s
test forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test))

forAllScripts_ ::
  (DynLogicModel s, Testable a) =>
  DynFormula s ->
  (Actions s -> a) ->
  Property
forAllScripts_ :: forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> Property
forAllScripts_ DynFormula s
f Actions s -> a
k =
  forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
     in forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) forall a b. (a -> b) -> a -> b
$
          forall s a.
(DynLogicModel s, Testable a) =>
DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScript DynLogic s
d Actions s -> a
k

-- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose.
-- ??
forAllMappedScripts ::
  (DynLogicModel s, Testable a, Show rep) =>
  (rep -> DynLogicTest s) ->
  (DynLogicTest s -> rep) ->
  DynFormula s ->
  (Actions s -> a) ->
  Property
forAllMappedScripts :: forall s a rep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
forAllMappedScripts rep -> DynLogicTest s
to DynLogicTest s -> rep
from DynFormula s
f Actions s -> a
k =
  forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
     in forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink
          (forall a. Int -> a -> Smart a
Smart Int
0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (Int -> Gen a) -> Gen a
sized ((DynLogicTest s -> rep
from forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d))
          (forall a. (a -> [a]) -> Smart a -> [Smart a]
shrinkSmart ((DynLogicTest s -> rep
from forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> [DynLogicTest s]
shrinkDLTest DynLogic s
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep -> DynLogicTest s
to))
          forall a b. (a -> b) -> a -> b
$ \(Smart Int
_ rep
script) ->
            forall s a.
(DynLogicModel s, Testable a) =>
DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScript DynLogic s
d Actions s -> a
k (rep -> DynLogicTest s
to rep
script)

forAllMappedScripts_ ::
  (DynLogicModel s, Testable a, Show rep) =>
  (rep -> DynLogicTest s) ->
  (DynLogicTest s -> rep) ->
  DynFormula s ->
  (Actions s -> a) ->
  Property
forAllMappedScripts_ :: forall s a rep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
forAllMappedScripts_ rep -> DynLogicTest s
to DynLogicTest s -> rep
from DynFormula s
f Actions s -> a
k =
  forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
     in forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ (DynLogicTest s -> rep
from forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) forall a b. (a -> b) -> a -> b
$
          forall s a.
(DynLogicModel s, Testable a) =>
DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScript DynLogic s
d Actions s -> a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep -> DynLogicTest s
to

withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScript :: forall s a.
(DynLogicModel s, Testable a) =>
DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScript DynLogic s
d Actions s -> a
k DynLogicTest s
test =
  forall s. StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
d DynLogicTest s
test forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test))

withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScriptPrefix :: forall s a.
(DynLogicModel s, Testable a) =>
DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScriptPrefix DynFormula s
f Actions s -> a
k DynLogicTest s
test =
  forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
        test' :: DynLogicTest s
test' = forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> DynLogicTest s
unfailDLTest DynLogic s
d DynLogicTest s
test
     in forall s. StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
d DynLogicTest s
test' forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test'))

generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest :: forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d Int
size = forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> m (DynLogicTest s)
generate forall s.
DynLogicModel s =>
s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep DynLogic s
d Int
0 (forall s. StateModel s => DynLogic s -> s
initialStateFor DynLogic s
d) Int
size []

generate ::
  (Monad m, DynLogicModel s) =>
  (s -> Int -> DynLogic s -> m (NextStep s)) ->
  DynLogic s ->
  Int ->
  s ->
  Int ->
  [TestStep s] ->
  m (DynLogicTest s)
generate :: forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> m (DynLogicTest s)
generate s -> Int -> DynLogic s -> m (NextStep s)
chooseNextStepFun DynLogic s
d Int
n s
s Int
size [TestStep s]
as =
  case forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s of
    [] ->
      if Int
n forall a. Ord a => a -> a -> Bool
> Int -> Int
sizeLimit Int
size
        then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. [TestStep s] -> DynLogicTest s
Looping (forall a. [a] -> [a]
reverse [TestStep s]
as)
        else do
          let preferred :: DynLogic s
preferred = if Int
n forall a. Ord a => a -> a -> Bool
> Int
size then forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d else forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d
              useStep :: NextStep s -> m (DynLogicTest s) -> m (DynLogicTest s)
useStep NextStep s
StoppingStep m (DynLogicTest s)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. [TestStep s] -> DynLogicTest s
DLScript (forall a. [a] -> [a]
reverse [TestStep s]
as)
              useStep (Stepping (Do (Var a
var := Action s a
act)) DynLogic s
d') m (DynLogicTest s)
_ =
                forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> m (DynLogicTest s)
generate
                  s -> Int -> DynLogic s -> m (NextStep s)
chooseNextStepFun
                  DynLogic s
d'
                  (Int
n forall a. Num a => a -> a -> a
+ Int
1)
                  (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
act Var a
var)
                  Int
size
                  (forall s. Step s -> TestStep s
Do (Var a
var forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action s a
act) forall a. a -> [a] -> [a]
: [TestStep s]
as)
              useStep (Stepping (Witness a
a) DynLogic s
d') m (DynLogicTest s)
_ =
                forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> m (DynLogicTest s)
generate
                  s -> Int -> DynLogic s -> m (NextStep s)
chooseNextStepFun
                  DynLogic s
d'
                  Int
n
                  s
s
                  Int
size
                  (forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a forall a. a -> [a] -> [a]
: [TestStep s]
as)
              useStep NextStep s
NoStep m (DynLogicTest s)
alt = m (DynLogicTest s)
alt
          forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
            (\DynLogic s
step m (DynLogicTest s)
k -> do NextStep s
try <- s -> Int -> DynLogic s -> m (NextStep s)
chooseNextStepFun s
s Int
n DynLogic s
step; NextStep s -> m (DynLogicTest s) -> m (DynLogicTest s)
useStep NextStep s
try m (DynLogicTest s)
k)
            (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. [TestStep s] -> s -> DynLogicTest s
Stuck (forall a. [a] -> [a]
reverse [TestStep s]
as) s
s)
            [DynLogic s
preferred, forall s. DynLogic s -> DynLogic s
noAny DynLogic s
preferred, DynLogic s
d, forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d]
    [Any (Action s)]
bs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
BadPrecondition (forall a. [a] -> [a]
reverse [TestStep s]
as) [Any (Action s)]
bs s
s

sizeLimit :: Int -> Int
sizeLimit :: Int -> Int
sizeLimit Int
size = Int
2 forall a. Num a => a -> a -> a
* Int
size forall a. Num a => a -> a -> a
+ Int
20

initialStateFor :: StateModel s => DynLogic s -> s
initialStateFor :: forall s. StateModel s => DynLogic s -> s
initialStateFor DynLogic s
_ = forall state. StateModel state => state
initialState

stopping :: DynLogic s -> DynLogic s
stopping :: forall s. DynLogic s -> DynLogic s
stopping DynLogic s
EmptySpec = forall s. DynLogic s
EmptySpec
stopping DynLogic s
Stop = forall s. DynLogic s
Stop
stopping (After Any (Action s)
act DynPred s
k) = forall s. Any (Action s) -> DynPred s -> DynLogic s
After Any (Action s)
act DynPred s
k
stopping (AfterAny DynPred s
_) = forall s. DynLogic s
EmptySpec
stopping (Alt ChoiceType
b DynLogic s
d DynLogic s
d') = forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
b (forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d) (forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d')
stopping (Stopping DynLogic s
d) = DynLogic s
d
stopping (Weight Double
w DynLogic s
d) = forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w (forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d)
stopping (ForAll Quantification a
_ a -> DynLogic s
_) = forall s. DynLogic s
EmptySpec
stopping (Monitor Property -> Property
f DynLogic s
d) = forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
f (forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d)

noStopping :: DynLogic s -> DynLogic s
noStopping :: forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
EmptySpec = forall s. DynLogic s
EmptySpec
noStopping DynLogic s
Stop = forall s. DynLogic s
EmptySpec
noStopping (After Any (Action s)
act DynPred s
k) = forall s. Any (Action s) -> DynPred s -> DynLogic s
After Any (Action s)
act DynPred s
k
noStopping (AfterAny DynPred s
k) = forall s. DynPred s -> DynLogic s
AfterAny DynPred s
k
noStopping (Alt ChoiceType
b DynLogic s
d DynLogic s
d') = forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
b (forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d) (forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d')
noStopping (Stopping DynLogic s
_) = forall s. DynLogic s
EmptySpec
noStopping (Weight Double
w DynLogic s
d) = forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w (forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d)
noStopping (ForAll Quantification a
q a -> DynLogic s
f) = forall s a.
(Eq a, Show a, Typeable a) =>
Quantification a -> (a -> DynLogic s) -> DynLogic s
ForAll Quantification a
q a -> DynLogic s
f
noStopping (Monitor Property -> Property
f DynLogic s
d) = forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
f (forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d)

noAny :: DynLogic s -> DynLogic s
noAny :: forall s. DynLogic s -> DynLogic s
noAny DynLogic s
EmptySpec = forall s. DynLogic s
EmptySpec
noAny DynLogic s
Stop = forall s. DynLogic s
Stop
noAny (After Any (Action s)
act DynPred s
k) = forall s. Any (Action s) -> DynPred s -> DynLogic s
After Any (Action s)
act DynPred s
k
noAny (AfterAny DynPred s
_) = forall s. DynLogic s
EmptySpec
noAny (Alt ChoiceType
b DynLogic s
d DynLogic s
d') = forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
b (forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d) (forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d')
noAny (Stopping DynLogic s
d) = forall s. DynLogic s -> DynLogic s
Stopping (forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d)
noAny (Weight Double
w DynLogic s
d) = forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w (forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d)
noAny (ForAll Quantification a
q a -> DynLogic s
f) = forall s a.
(Eq a, Show a, Typeable a) =>
Quantification a -> (a -> DynLogic s) -> DynLogic s
ForAll Quantification a
q a -> DynLogic s
f
noAny (Monitor Property -> Property
f DynLogic s
d) = forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
f (forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d)

nextSteps :: DynLogic s -> [(Double, DynLogic s)]
nextSteps :: forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
EmptySpec = []
nextSteps DynLogic s
Stop = [(Double
1, forall s. DynLogic s
Stop)]
nextSteps (After Any (Action s)
act DynPred s
k) = [(Double
1, forall s. Any (Action s) -> DynPred s -> DynLogic s
After Any (Action s)
act DynPred s
k)]
nextSteps (AfterAny DynPred s
k) = [(Double
1, forall s. DynPred s -> DynLogic s
AfterAny DynPred s
k)]
nextSteps (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') = forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d forall a. [a] -> [a] -> [a]
++ forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d'
nextSteps (Stopping DynLogic s
d) = forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d
nextSteps (Weight Double
w DynLogic s
d) = [(Double
w forall a. Num a => a -> a -> a
* Double
w', DynLogic s
s) | (Double
w', DynLogic s
s) <- forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d, Double
w forall a. Num a => a -> a -> a
* Double
w' forall a. Ord a => a -> a -> Bool
> Double
never]
nextSteps (ForAll Quantification a
q a -> DynLogic s
f) = [(Double
1, forall s a.
(Eq a, Show a, Typeable a) =>
Quantification a -> (a -> DynLogic s) -> DynLogic s
ForAll Quantification a
q a -> DynLogic s
f)]
nextSteps (Monitor Property -> Property
_f DynLogic s
d) = forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d

chooseOneOf :: [(Double, DynLogic s)] -> Gen (DynLogic s)
chooseOneOf :: forall s. [(Double, DynLogic s)] -> Gen (DynLogic s)
chooseOneOf [(Double, DynLogic s)]
steps = forall a. [(Int, Gen a)] -> Gen a
frequency [(forall a b. (RealFrac a, Integral b) => a -> b
round (Double
w forall a. Fractional a => a -> a -> a
/ Double
never), forall (m :: * -> *) a. Monad m => a -> m a
return DynLogic s
s) | (Double
w, DynLogic s
s) <- [(Double, DynLogic s)]
steps]

never :: Double
never :: Double
never = Double
1.0e-9

data NextStep s
  = StoppingStep
  | Stepping (TestStep s) (DynLogic s)
  | NoStep

chooseNextStep :: DynLogicModel s => s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep :: forall s.
DynLogicModel s =>
s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep s
s Int
n DynLogic s
d =
  case forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
    [(Double, DynLogic s)]
steps -> do
      DynLogic s
chosen <- forall s. [(Double, DynLogic s)] -> Gen (DynLogic s)
chooseOneOf [(Double, DynLogic s)]
steps
      case DynLogic s
chosen of
        DynLogic s
EmptySpec -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
        DynLogic s
Stop -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
StoppingStep
        After (Some Action s a
a) DynPred s
k ->
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. TestStep s -> DynLogic s -> NextStep s
Stepping (forall s. Step s -> TestStep s
Do forall a b. (a -> b) -> a -> b
$ forall a. Int -> Var a
Var Int
n forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action s a
a) (DynPred s
k (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
a (forall a. Int -> Var a
Var Int
n)))
        AfterAny DynPred s
k -> do
          Maybe (Any (Action s))
m <- forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil Int
100 (forall state. StateModel state => state -> Gen (Any (Action state))
arbitraryAction s
s) forall a b. (a -> b) -> a -> b
$
            \case
              Some Action s a
act -> forall state a. StateModel state => state -> Action state a -> Bool
precondition s
s Action s a
act Bool -> Bool -> Bool
&& Bool -> Bool
not (forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
act)
              Error String
_ -> Bool
False
          case Maybe (Any (Action s))
m of
            Maybe (Any (Action s))
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
            Just (Some Action s a
a) ->
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                forall s. TestStep s -> DynLogic s -> NextStep s
Stepping
                  (forall s. Step s -> TestStep s
Do forall a b. (a -> b) -> a -> b
$ forall a. Int -> Var a
Var Int
n forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action s a
a)
                  (DynPred s
k (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
a (forall a. Int -> Var a
Var Int
n)))
            Just Error{} -> forall a. HasCallStack => String -> a
error String
"impossible"
        ForAll Quantification a
q a -> DynLogic s
f -> do
          a
x <- forall a. Quantification a -> Gen a
generateQ Quantification a
q
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. TestStep s -> DynLogic s -> NextStep s
Stepping (forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
x) (a -> DynLogic s
f a
x)
        After Error{} DynPred s
_ -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: After Error"
        Alt{} -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: Alt"
        Stopping{} -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: Stopping"
        Weight{} -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: Weight"
        Monitor{} -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: Monitor"

chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep :: forall (m :: * -> *) s.
(MonadFail m, DynLogicModel s) =>
s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep s
s Int
n DynLogic s
d =
  case forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
    [DynLogic s
EmptySpec] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
    [DynLogic s
Stop] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
StoppingStep
    [After (Some Action s a
a) DynPred s
k] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. TestStep s -> DynLogic s -> NextStep s
Stepping (forall s. Step s -> TestStep s
Do forall a b. (a -> b) -> a -> b
$ forall a. Int -> Var a
Var Int
n forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action s a
a) (DynPred s
k (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
a (forall a. Int -> Var a
Var Int
n)))
    [DynLogic s]
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"chooseUniqueNextStep: non-unique action in DynLogic"

keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil :: forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil Int
0 Gen a
_ a -> Bool
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
keepTryingUntil Int
n Gen a
g a -> Bool
p = do
  a
x <- Gen a
g
  if a -> Bool
p a
x then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just a
x else forall a. (Int -> Int) -> Gen a -> Gen a
scale (forall a. Num a => a -> a -> a
+ Int
1) forall a b. (a -> b) -> a -> b
$ forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil (Int
n forall a. Num a => a -> a -> a
- Int
1) Gen a
g a -> Bool
p

shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]
shrinkDLTest :: forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> [DynLogicTest s]
shrinkDLTest DynLogic s
_ (Looping [TestStep s]
_) = []
shrinkDLTest DynLogic s
d DynLogicTest s
tc =
  [ DynLogicTest s
test | [TestStep s]
as' <- forall t.
DynLogicModel t =>
DynLogic t -> [TestStep t] -> [[TestStep t]]
shrinkScript DynLogic s
d (forall s. DynLogicTest s -> [TestStep s]
getScript DynLogicTest s
tc), let test :: DynLogicTest s
test = forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned DynLogic s
d (forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest DynLogic s
d [TestStep s]
as'),
  -- Don't shrink a non-executable test case to an executable one.
  case (DynLogicTest s
tc, DynLogicTest s
test) of
    (DLScript [TestStep s]
_, DynLogicTest s
_) -> Bool
True
    (DynLogicTest s
_, DLScript [TestStep s]
_) -> Bool
False
    (DynLogicTest s, DynLogicTest s)
_ -> Bool
True
  ]

shrinkScript :: DynLogicModel t => DynLogic t -> [TestStep t] -> [[TestStep t]]
shrinkScript :: forall t.
DynLogicModel t =>
DynLogic t -> [TestStep t] -> [[TestStep t]]
shrinkScript DynLogic t
dl [TestStep t]
steps = forall {a}.
DynLogicModel a =>
DynLogic a -> [TestStep a] -> a -> [[TestStep a]]
shrink' DynLogic t
dl [TestStep t]
steps forall state. StateModel state => state
initialState
 where
  shrink' :: DynLogic a -> [TestStep a] -> a -> [[TestStep a]]
shrink' DynLogic a
_ [] a
_ = []
  shrink' DynLogic a
d (TestStep a
step : [TestStep a]
as) a
s =
    [] forall a. a -> [a] -> [a]
:
    forall a. [a] -> [a]
reverse (forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [forall a. Int -> [a] -> [a]
drop (Int
n forall a. Num a => a -> a -> a
- Int
1) [TestStep a]
as | Int
n <- forall a. (a -> a) -> a -> [a]
iterate (forall a. Num a => a -> a -> a
* Int
2) Int
1])
      forall a. [a] -> [a] -> [a]
++ case TestStep a
step of
        Do (Var Int
i := Action a a
act) ->
          [forall s. Step s -> TestStep s
Do (forall a. Int -> Var a
Var Int
i forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action a a
act') forall a. a -> [a] -> [a]
: [TestStep a]
as | Some Action a a
act' <- forall state a.
(StateModel state, Show a, Typeable a) =>
state -> Action state a -> [Any (Action state)]
shrinkAction a
s Action a a
act]
        Witness a
a ->
          -- When we shrink a witness, allow one shrink of the
          -- rest of the script... so assuming the witness may be
          -- used once to construct the rest of the test. If used
          -- more than once, we may need double shrinking.
          [ forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a' forall a. a -> [a] -> [a]
: [TestStep a]
as' | a
a' <- forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic a
d a
a, [TestStep a]
as' <- [TestStep a]
as forall a. a -> [a] -> [a]
: DynLogic a -> [TestStep a] -> a -> [[TestStep a]]
shrink' (forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic a
d a
s (forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a')) [TestStep a]
as a
s
          ]
      forall a. [a] -> [a] -> [a]
++ [ TestStep a
step forall a. a -> [a] -> [a]
: [TestStep a]
as'
         | [TestStep a]
as' <- DynLogic a -> [TestStep a] -> a -> [[TestStep a]]
shrink' (forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic a
d a
s TestStep a
step) [TestStep a]
as forall a b. (a -> b) -> a -> b
$
            case TestStep a
step of
              Do (Var a
var := Action a a
act) -> forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState a
s Action a a
act Var a
var
              Witness a
_ -> a
s
         ]

shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness :: forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness (ForAll (Quantification a
q :: Quantification a) a -> DynLogic s
_) (a
a :: a') =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl | forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a -> forall a. Quantification a -> a -> [a]
shrinkQ Quantification a
q a
a
    Maybe (a :~: a)
_ -> []
shrinkWitness (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') a
a = forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a forall a. [a] -> [a] -> [a]
++ forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d' a
a
shrinkWitness (Stopping DynLogic s
d) a
a = forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a
shrinkWitness (Weight Double
_ DynLogic s
d) a
a = forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a
shrinkWitness (Monitor Property -> Property
_ DynLogic s
d) a
a = forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a
shrinkWitness DynLogic s
_ a
_ = []

-- The result of pruning a list of actions is a list of actions that
-- could have been generated by the dynamic logic.
pruneDLTest :: DynLogicModel s => DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest :: forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest DynLogic s
dl = forall {s}.
DynLogicModel s =>
[DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s
dl] forall state. StateModel state => state
initialState
 where
  prune :: [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [] s
_ [TestStep s]
_ = []
  prune [DynLogic s]
_ s
_ [] = []
  prune [DynLogic s]
ds s
s (Do (Var a
var := Action s a
act) : [TestStep s]
rest)
    | forall state a. StateModel state => state -> Action state a -> Bool
precondition s
s Action s a
act =
      case [DynLogic s
d' | DynLogic s
d <- [DynLogic s]
ds, DynLogic s
d' <- forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s (forall s. Step s -> TestStep s
Do forall a b. (a -> b) -> a -> b
$ Var a
var forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action s a
act)] of
        [] -> [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s]
ds s
s [TestStep s]
rest
        [DynLogic s]
ds' ->
          forall s. Step s -> TestStep s
Do (Var a
var forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action s a
act) forall a. a -> [a] -> [a]
:
          [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s]
ds' (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
act Var a
var) [TestStep s]
rest
    | Bool
otherwise =
      [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s]
ds s
s [TestStep s]
rest
  prune [DynLogic s]
ds s
s (Witness a
a : [TestStep s]
rest) =
    case [DynLogic s
d' | DynLogic s
d <- [DynLogic s]
ds, DynLogic s
d' <- forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s (forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a)] of
      [] -> [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s]
ds s
s [TestStep s]
rest
      [DynLogic s]
ds' -> forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a forall a. a -> [a] -> [a]
: [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s]
ds' s
s [TestStep s]
rest

stepDL :: DynLogicModel s => DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL :: forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL (After Any (Action s)
a DynPred s
k) s
s (Do (Var a
var := Action s a
act))
  | Any (Action s)
a forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
act = [DynPred s
k (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
act Var a
var)]
stepDL (AfterAny DynPred s
k) s
s (Do (Var a
var := Action s a
act))
  | Bool -> Bool
not (forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
act) = [DynPred s
k (forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
act Var a
var)]
stepDL (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') s
s TestStep s
step = forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step forall a. [a] -> [a] -> [a]
++ forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d' s
s TestStep s
step
stepDL (Stopping DynLogic s
d) s
s TestStep s
step = forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step
stepDL (Weight Double
_ DynLogic s
d) s
s TestStep s
step = forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step
stepDL (ForAll (Quantification a
q :: Quantification a) a -> DynLogic s
f) s
_ (Witness (a
a :: a')) =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> [a -> DynLogic s
f a
a | forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a]
    Maybe (a :~: a)
Nothing -> []
stepDL (Monitor Property -> Property
_f DynLogic s
d) s
s TestStep s
step = forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step
stepDL DynLogic s
_ s
_ TestStep s
_ = []

stepDLtoDL :: DynLogicModel s => DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL :: forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic s
d s
s TestStep s
step = case forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step of
  [] -> forall s. DynLogic s
EmptySpec
  [DynLogic s]
ds -> forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
Demonic) [DynLogic s]
ds

propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property
propPruningGeneratedScriptIsNoop :: forall s. DynLogicModel s => DynLogic s -> Property
propPruningGeneratedScriptIsNoop DynLogic s
d =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ \Int
n -> forall a. Random a => (a, a) -> Gen a
choose (Int
1, forall a. Ord a => a -> a -> a
max Int
1 Int
n) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) forall a b. (a -> b) -> a -> b
$ \DynLogicTest s
test ->
    let script :: [TestStep s]
script = case DynLogicTest s
test of
          BadPrecondition [TestStep s]
s [Any (Action s)]
_ s
_ -> [TestStep s]
s
          Looping [TestStep s]
s -> [TestStep s]
s
          Stuck [TestStep s]
s s
_ -> [TestStep s]
s
          DLScript [TestStep s]
s -> [TestStep s]
s
     in [TestStep s]
script forall a. Eq a => a -> a -> Bool
== forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest DynLogic s
d [TestStep s]
script

getScript :: DynLogicTest s -> [TestStep s]
getScript :: forall s. DynLogicTest s -> [TestStep s]
getScript (BadPrecondition [TestStep s]
s [Any (Action s)]
_ s
_) = [TestStep s]
s
getScript (Looping [TestStep s]
s) = [TestStep s]
s
getScript (Stuck [TestStep s]
s s
_) = [TestStep s]
s
getScript (DLScript [TestStep s]
s) = [TestStep s]
s

makeTestFromPruned :: DynLogicModel s => DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned :: forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned DynLogic s
dl = forall {t}.
DynLogicModel t =>
DynLogic t -> t -> [TestStep t] -> DynLogicTest t
make DynLogic s
dl forall state. StateModel state => state
initialState
 where
  make :: DynLogic t -> t -> [TestStep t] -> DynLogicTest t
make DynLogic t
d t
s [TestStep t]
as | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Any (Action t)]
bad) = forall s. [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
BadPrecondition [TestStep t]
as [Any (Action t)]
bad t
s
   where
    bad :: [Any (Action t)]
bad = forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic t
d t
s
  make DynLogic t
d t
s []
    | forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic t
d t
s = forall s. [TestStep s] -> s -> DynLogicTest s
Stuck [] t
s
    | Bool
otherwise = forall s. [TestStep s] -> DynLogicTest s
DLScript []
  make DynLogic t
d t
curStep (TestStep t
step : [TestStep t]
steps) =
    case DynLogic t -> t -> [TestStep t] -> DynLogicTest t
make
      (forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic t
d t
curStep TestStep t
step)
      ( case TestStep t
step of
          Do (Var a
var := Action t a
act) -> forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState t
curStep Action t a
act Var a
var
          Witness a
_ -> t
curStep
      )
      [TestStep t]
steps of
      BadPrecondition [TestStep t]
as [Any (Action t)]
bad t
s -> forall s. [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
BadPrecondition (TestStep t
step forall a. a -> [a] -> [a]
: [TestStep t]
as) [Any (Action t)]
bad t
s
      Stuck [TestStep t]
as t
s -> forall s. [TestStep s] -> s -> DynLogicTest s
Stuck (TestStep t
step forall a. a -> [a] -> [a]
: [TestStep t]
as) t
s
      DLScript [TestStep t]
as -> forall s. [TestStep s] -> DynLogicTest s
DLScript (TestStep t
step forall a. a -> [a] -> [a]
: [TestStep t]
as)
      Looping{} -> forall a. HasCallStack => String -> a
error String
"makeTestFromPruned: Looping"

-- | If failed, return the prefix up to the failure. Also prunes the test in case the model has
--   changed.
unfailDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> DynLogicTest s
unfailDLTest :: forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> DynLogicTest s
unfailDLTest DynLogic s
d DynLogicTest s
test = forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned DynLogic s
d forall a b. (a -> b) -> a -> b
$ forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest DynLogic s
d [TestStep s]
steps
 where
  steps :: [TestStep s]
steps = case DynLogicTest s
test of
    BadPrecondition [TestStep s]
as [Any (Action s)]
_ s
_ -> [TestStep s]
as
    Stuck [TestStep s]
as s
_ -> [TestStep s]
as
    DLScript [TestStep s]
as -> [TestStep s]
as
    Looping [TestStep s]
as -> [TestStep s]
as

stuck :: DynLogicModel s => DynLogic s -> s -> Bool
stuck :: forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
EmptySpec s
_ = Bool
True
stuck DynLogic s
Stop s
_ = Bool
False
stuck (After Any (Action s)
_ DynPred s
_) s
_ = Bool
False
stuck (AfterAny DynPred s
_) s
s =
  Bool -> Bool
not forall a b. (a -> b) -> a -> b
$
    forall a. Double -> Gen a -> (a -> Bool) -> Bool
canGenerate
      Double
0.01
      (forall state. StateModel state => state -> Gen (Any (Action state))
arbitraryAction s
s)
      ( \case
          Some Action s a
act ->
            forall state a. StateModel state => state -> Action state a -> Bool
precondition s
s Action s a
act
              Bool -> Bool -> Bool
&& Bool -> Bool
not (forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
act)
          Error String
_ -> Bool
False
      )
stuck (Alt ChoiceType
Angelic DynLogic s
d DynLogic s
d') s
s = forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s Bool -> Bool -> Bool
&& forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d' s
s
stuck (Alt ChoiceType
Demonic DynLogic s
d DynLogic s
d') s
s = forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s Bool -> Bool -> Bool
|| forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d' s
s
stuck (Stopping DynLogic s
d) s
s = forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s
stuck (Weight Double
w DynLogic s
d) s
s = Double
w forall a. Ord a => a -> a -> Bool
< Double
never Bool -> Bool -> Bool
|| forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s
stuck (ForAll Quantification a
_ a -> DynLogic s
_) s
_ = Bool
False
stuck (Monitor Property -> Property
_ DynLogic s
d) s
s = forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s

validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest :: forall s. StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
_ (DLScript [TestStep s]
_) = forall prop. Testable prop => prop -> Property
property Bool
True
validDLTest DynLogic s
_ (Stuck [TestStep s]
as s
_) = forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Stuck\n" forall a. [a] -> [a] -> [a]
++ ([String] -> String
unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (String
"  " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show [TestStep s]
as)) Bool
False
validDLTest DynLogic s
_ (Looping [TestStep s]
as) = forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Looping\n" forall a. [a] -> [a] -> [a]
++ ([String] -> String
unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (String
"  " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show [TestStep s]
as)) Bool
False
validDLTest DynLogic s
_ (BadPrecondition [TestStep s]
as [Any (Action s)]
bads s
_s) = forall prop. Testable prop => String -> prop -> Property
counterexample (String
"BadPrecondition\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [TestStep s]
as forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (forall {f :: * -> *}. Show (Any f) => Any f -> String
showBad forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Any (Action s)]
bads)) Bool
False
 where
  showBad :: Any f -> String
showBad (Error String
s) = String
s
  showBad Any f
a = forall a. Show a => a -> String
show Any f
a

scriptFromDL :: DynLogicTest s -> Actions s
scriptFromDL :: forall s. DynLogicTest s -> Actions s
scriptFromDL (DLScript [TestStep s]
s) = forall state. [Step state] -> Actions state
Actions [Step s
a | Do Step s
a <- [TestStep s]
s]
scriptFromDL DynLogicTest s
_ = forall state. [Step state] -> Actions state
Actions []

badActions :: StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions :: forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
EmptySpec s
_ = []
badActions DynLogic s
Stop s
_ = []
badActions (After (Some Action s a
a) DynPred s
_) s
s
  | forall state a. StateModel state => state -> Action state a -> Bool
precondition s
s Action s a
a = []
  | Bool
otherwise = [forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
a]
badActions (After (Error String
m) DynPred s
_) s
_s = [forall (f :: * -> *). String -> Any f
Error String
m]
badActions (AfterAny DynPred s
_) s
_ = []
badActions (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') s
s = forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s forall a. [a] -> [a] -> [a]
++ forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d' s
s
badActions (Stopping DynLogic s
d) s
s = forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s
badActions (Weight Double
w DynLogic s
d) s
s = if Double
w forall a. Ord a => a -> a -> Bool
< Double
never then [] else forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s
badActions (ForAll Quantification a
_ a -> DynLogic s
_) s
_ = []
badActions (Monitor Property -> Property
_ DynLogic s
d) s
s = forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s

applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring :: forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d (DLScript [TestStep s]
s) Property
p =
  case forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d forall state. StateModel state => state
initialState [TestStep s]
s of
    Just Property -> Property
f -> Property -> Property
f Property
p
    Maybe (Property -> Property)
Nothing -> Property
p
applyMonitoring DynLogic s
_ Stuck{} Property
p = Property
p
applyMonitoring DynLogic s
_ Looping{} Property
p = Property
p
applyMonitoring DynLogic s
_ BadPrecondition{} Property
p = Property
p

findMonitoring :: DynLogicModel s => DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring :: forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
Stop s
_s [] = forall a. a -> Maybe a
Just forall a. a -> a
id
findMonitoring (After (Some Action s a
a) DynPred s
k) s
s (Do (Var a
var := Action s a
a') : [TestStep s]
as)
  | forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
a forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
a' = forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring (DynPred s
k s
s') s
s' [TestStep s]
as
 where
  s' :: s
s' = forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
a' Var a
var
findMonitoring (AfterAny DynPred s
k) s
s as :: [TestStep s]
as@(Do (Var a
_var := Action s a
a) : [TestStep s]
_)
  | Bool -> Bool
not (forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
a) = forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring (forall s. Any (Action s) -> DynPred s -> DynLogic s
After (forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
a) DynPred s
k) s
s [TestStep s]
as
findMonitoring (Alt ChoiceType
_b DynLogic s
d DynLogic s
d') s
s [TestStep s]
as =
  -- Give priority to monitoring matches to the left. Combining both
  -- results in repeated monitoring from always, which is unexpected.
  forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d s
s [TestStep s]
as forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d' s
s [TestStep s]
as
findMonitoring (Stopping DynLogic s
d) s
s [TestStep s]
as = forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d s
s [TestStep s]
as
findMonitoring (Weight Double
_ DynLogic s
d) s
s [TestStep s]
as = forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d s
s [TestStep s]
as
findMonitoring (ForAll (Quantification a
_q :: Quantification a) a -> DynLogic s
k) s
s (Witness (a
a :: a') : [TestStep s]
as) =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring (a -> DynLogic s
k a
a) s
s [TestStep s]
as
    Maybe (a :~: a)
Nothing -> forall a. Maybe a
Nothing
findMonitoring (Monitor Property -> Property
m DynLogic s
d) s
s [TestStep s]
as =
  (Property -> Property
m forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d s
s [TestStep s]
as
findMonitoring DynLogic s
_ s
_ [TestStep s]
_ = forall a. Maybe a
Nothing