{-# 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 {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
(ChoiceType -> ChoiceType -> Bool)
-> (ChoiceType -> ChoiceType -> Bool) -> Eq ChoiceType
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
(Int -> ChoiceType -> ShowS)
-> (ChoiceType -> String)
-> ([ChoiceType] -> ShowS)
-> Show ChoiceType
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 :: DynFormula s
ignore = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (DynLogic s -> Int -> DynLogic s) -> DynLogic s -> DynFormula s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> DynLogic s
forall a b. a -> b -> a
const (DynLogic s -> DynFormula s) -> DynLogic s -> DynFormula s
forall a b. (a -> b) -> a -> b
$ DynLogic s
forall s. DynLogic s
EmptySpec
passTest :: DynFormula s
passTest = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (DynLogic s -> Int -> DynLogic s) -> DynLogic s -> DynFormula s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> DynLogic s
forall a b. a -> b -> a
const (DynLogic s -> DynFormula s) -> DynLogic s -> DynFormula s
forall a b. (a -> b) -> a -> b
$ DynLogic s
forall s. DynLogic s
Stop
afterAny :: (s -> DynFormula s) -> DynFormula s
afterAny s -> DynFormula s
f = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> DynPred s -> DynLogic s
forall s. DynPred s -> DynLogic s
AfterAny (DynPred s -> DynLogic s) -> DynPred s -> DynLogic s
forall a b. (a -> b) -> a -> b
$ \s
s -> DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (s -> DynFormula s
f s
s) Int
n
after :: Action s a -> (s -> DynFormula s) -> DynFormula s
after Action s a
act s -> DynFormula s
f = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> Any (Action s) -> DynPred s -> DynLogic s
forall s. Any (Action s) -> DynPred s -> DynLogic s
After (Action s a -> Any (Action s)
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
act) (DynPred s -> DynLogic s) -> DynPred s -> DynLogic s
forall a b. (a -> b) -> a -> b
$ \s
s -> DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (s -> DynFormula s
f s
s) Int
n
DynFormula Int -> DynLogic s
f ||| :: DynFormula s -> DynFormula s -> DynFormula s
||| DynFormula Int -> DynLogic s
g = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
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 :: q -> (Quantifies q -> DynFormula s) -> DynFormula s
forAllQ q
q Quantifies q -> DynFormula s
f
  | Quantification (Quantifies q) -> Bool
forall a. Quantification a -> Bool
isEmptyQ Quantification (Quantifies q)
q' = DynFormula s
forall s. DynFormula s
ignore
  | Bool
otherwise = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> Quantification (Quantifies q)
-> (Quantifies q -> DynLogic s) -> DynLogic s
forall s a.
(Eq a, Show a, Typeable a) =>
Quantification a -> (a -> DynLogic s) -> DynLogic s
ForAll Quantification (Quantifies q)
q' ((Quantifies q -> DynLogic s) -> DynLogic s)
-> (Quantifies q -> DynLogic s) -> DynLogic s
forall a b. (a -> b) -> a -> b
$ ((Int -> DynLogic s) -> Int -> DynLogic s
forall a b. (a -> b) -> a -> b
$ Int
n) ((Int -> DynLogic s) -> DynLogic s)
-> (Quantifies q -> Int -> DynLogic s)
-> Quantifies q
-> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (DynFormula s -> Int -> DynLogic s)
-> (Quantifies q -> DynFormula s)
-> Quantifies q
-> Int
-> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantifies q -> DynFormula s
f
 where
  q' :: Quantification (Quantifies q)
q' = q -> Quantification (Quantifies q)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify q
q

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

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

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

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

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

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

always :: (s -> DynFormula s) -> s -> DynFormula s
always s -> DynFormula s
p s
s = (Int -> DynFormula s) -> DynFormula s
forall s. (Int -> DynFormula s) -> DynFormula s
withSize ((Int -> DynFormula s) -> DynFormula s)
-> (Int -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s
toStop (s -> DynFormula s
p s
s) DynFormula s -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s -> DynFormula s
||| s -> DynFormula s
p s
s DynFormula s -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s -> DynFormula s
||| Double -> DynFormula s -> DynFormula s
forall s. Double -> DynFormula s -> DynFormula s
weight (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) ((s -> DynFormula s) -> DynFormula s
forall s. (s -> DynFormula s) -> DynFormula s
afterAny ((s -> DynFormula s) -> s -> DynFormula s
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 Step s -> Step s -> Bool
forall a. Eq a => a -> a -> Bool
== Step s
s'
  Witness (a
a :: a) == Witness (a
a' :: a') =
    case (Typeable a, Typeable a) => Maybe (a :~: a)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
      Just a :~: a
Refl -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
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 $ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Step s -> String
forall a. Show a => a -> String
show Step s
step
  show (Witness a
a) = String
"Witness (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
a) String -> ShowS
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 ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
      [String
"BadPrecondition"]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as)
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Any (Action s)] -> String
forall a. Show a => a -> String
show ([Any (Action s)] -> [Any (Action s)]
forall a. Eq a => [a] -> [a]
nub [Any (Action s)]
bads)]
        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 s
s String
""]
  show (Looping [TestStep s]
as) =
    [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"Looping" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as)
  show (Stuck [TestStep s]
as s
s) =
    [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
"Stuck"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> s -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 s
s String
""]
  show (DLScript [TestStep s]
as) =
    [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"DLScript" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
bracket ((TestStep s -> String) -> [TestStep s] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TestStep s -> String
forall a. Show a => a -> String
show [TestStep s]
as)

bracket :: [String] -> [String]
bracket :: [String] -> [String]
bracket [] = [String
"  []"]
bracket [String
s] = [String
"  [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"]
bracket (String
first : [String]
rest) =
  [String
"  [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
first String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", "]
    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ")) ([String] -> [String]
forall a. [a] -> [a]
init [String]
rest)
    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. [a] -> a
last [String]
rest String -> ShowS
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 :: DynFormula s -> (Actions s -> a) -> Property
forAllScripts = (DynLogicTest s -> DynLogicTest s)
-> (DynLogicTest s -> DynLogicTest s)
-> DynFormula s
-> (Actions s -> a)
-> Property
forall s a rep.
(DynLogicModel s, Testable a, Show rep) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
forAllMappedScripts DynLogicTest s -> DynLogicTest s
forall a. a -> a
id DynLogicTest s -> DynLogicTest s
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 :: Int -> s -> DynFormula s -> (Actions s -> a) -> Property
forAllUniqueScripts Int
n s
s DynFormula s
f Actions s -> a
k =
  (Int -> Property) -> Property
forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
sz ->
    let d :: DynLogic s
d = DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
sz
     in case (s -> Int -> DynLogic s -> Maybe (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> Maybe (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 -> Maybe (NextStep s)
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 -> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Generating Non-unique script in forAllUniqueScripts" Bool
False
          Just DynLogicTest s
test -> DynLogic s -> DynLogicTest s -> Property
forall s. StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
d DynLogicTest s
test Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (DynLogic s -> DynLogicTest s -> Property -> Property
forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test (Property -> Property) -> (a -> Property) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property
forall prop. Testable prop => prop -> Property
property (a -> Property) -> a -> Property
forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (DynLogicTest s -> Actions s
forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test))

forAllScripts_ ::
  (DynLogicModel s, Testable a) =>
  DynFormula s ->
  (Actions s -> a) ->
  Property
forAllScripts_ :: DynFormula s -> (Actions s -> a) -> Property
forAllScripts_ DynFormula s
f Actions s -> a
k =
  (Int -> Property) -> Property
forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
     in Gen (DynLogicTest s) -> (DynLogicTest s -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s))
-> (Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ DynLogic s -> Int -> Gen (DynLogicTest s)
forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) ((DynLogicTest s -> Property) -> Property)
-> (DynLogicTest s -> Property) -> Property
forall a b. (a -> b) -> a -> b
$
          DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
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 :: (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 =
  (Int -> Property) -> Property
forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
     in Gen (Smart rep)
-> (Smart rep -> [Smart rep])
-> (Smart rep -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink
          (Int -> rep -> Smart rep
forall a. Int -> a -> Smart a
Smart Int
0 (rep -> Smart rep) -> Gen rep -> Gen (Smart rep)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Gen rep) -> Gen rep
forall a. (Int -> Gen a) -> Gen a
sized ((DynLogicTest s -> rep
from (DynLogicTest s -> rep) -> Gen (DynLogicTest s) -> Gen rep
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Gen (DynLogicTest s) -> Gen rep)
-> (Int -> Gen (DynLogicTest s)) -> Int -> Gen rep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> Gen (DynLogicTest s)
forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d))
          ((rep -> [rep]) -> Smart rep -> [Smart rep]
forall a. (a -> [a]) -> Smart a -> [Smart a]
shrinkSmart ((DynLogicTest s -> rep
from (DynLogicTest s -> rep) -> [DynLogicTest s] -> [rep]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([DynLogicTest s] -> [rep])
-> (rep -> [DynLogicTest s]) -> rep -> [rep]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> DynLogicTest s -> [DynLogicTest s]
forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> [DynLogicTest s]
shrinkDLTest DynLogic s
d (DynLogicTest s -> [DynLogicTest s])
-> (rep -> DynLogicTest s) -> rep -> [DynLogicTest s]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep -> DynLogicTest s
to))
          ((Smart rep -> Property) -> Property)
-> (Smart rep -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(Smart Int
_ rep
script) ->
            DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
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_ :: (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 =
  (Int -> Property) -> Property
forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let d :: DynLogic s
d = DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
n
     in Gen rep -> (rep -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen rep) -> Gen rep
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen rep) -> Gen rep) -> (Int -> Gen rep) -> Gen rep
forall a b. (a -> b) -> a -> b
$ (DynLogicTest s -> rep
from (DynLogicTest s -> rep) -> Gen (DynLogicTest s) -> Gen rep
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Gen (DynLogicTest s) -> Gen rep)
-> (Int -> Gen (DynLogicTest s)) -> Int -> Gen rep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> Gen (DynLogicTest s)
forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) ((rep -> Property) -> Property) -> (rep -> Property) -> Property
forall a b. (a -> b) -> a -> b
$
          DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
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 -> Property)
-> (rep -> DynLogicTest s) -> rep -> Property
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 :: DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScript DynLogic s
d Actions s -> a
k DynLogicTest s
test =
  DynLogic s -> DynLogicTest s -> Property
forall s. StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
d DynLogicTest s
test Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (DynLogic s -> DynLogicTest s -> Property -> Property
forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test (Property -> Property) -> (a -> Property) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property
forall prop. Testable prop => prop -> Property
property (a -> Property) -> a -> Property
forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (DynLogicTest s -> Actions s
forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test))

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

generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest :: DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d Int
size = (s -> Int -> DynLogic s -> Gen (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> Gen (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 -> Gen (NextStep s)
forall s.
DynLogicModel s =>
s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep DynLogic s
d Int
0 (DynLogic s -> s
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 :: (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 DynLogic s -> s -> [Any (Action s)]
forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s of
    [] ->
      if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Int
sizeLimit Int
size
        then DynLogicTest s -> m (DynLogicTest s)
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ [TestStep s] -> DynLogicTest s
forall s. [TestStep s] -> DynLogicTest s
Looping ([TestStep s] -> [TestStep s]
forall a. [a] -> [a]
reverse [TestStep s]
as)
        else do
          let preferred :: DynLogic s
preferred = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
size then DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d else DynLogic s -> DynLogic s
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)
_ = DynLogicTest s -> m (DynLogicTest s)
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ [TestStep s] -> DynLogicTest s
forall s. [TestStep s] -> DynLogicTest s
DLScript ([TestStep s] -> [TestStep s]
forall a. [a] -> [a]
reverse [TestStep s]
as)
              useStep (Stepping (Do (Var a
var := Action s a
act)) DynLogic s
d') m (DynLogicTest s)
_ =
                (s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> 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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                  (s -> Action s a -> Var a -> s
forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
act Var a
var)
                  Int
size
                  (Step s -> TestStep s
forall s. Step s -> TestStep s
Do (Var a
var Var a -> Action s a -> Step s
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) TestStep s -> [TestStep s] -> [TestStep s]
forall a. a -> [a] -> [a]
: [TestStep s]
as)
              useStep (Stepping (Witness a
a) DynLogic s
d') m (DynLogicTest s)
_ =
                (s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s
-> Int
-> s
-> Int
-> [TestStep s]
-> 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
                  (a -> TestStep s
forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a TestStep s -> [TestStep s] -> [TestStep s]
forall a. a -> [a] -> [a]
: [TestStep s]
as)
              useStep NextStep s
NoStep m (DynLogicTest s)
alt = m (DynLogicTest s)
alt
          (DynLogic s -> m (DynLogicTest s) -> m (DynLogicTest s))
-> m (DynLogicTest s) -> [DynLogic s] -> m (DynLogicTest s)
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)
            (DynLogicTest s -> m (DynLogicTest s)
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ [TestStep s] -> s -> DynLogicTest s
forall s. [TestStep s] -> s -> DynLogicTest s
Stuck ([TestStep s] -> [TestStep s]
forall a. [a] -> [a]
reverse [TestStep s]
as) s
s)
            [DynLogic s
preferred, DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
preferred, DynLogic s
d, DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d]
    [Any (Action s)]
bs -> DynLogicTest s -> m (DynLogicTest s)
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
forall s. [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
BadPrecondition ([TestStep s] -> [TestStep s]
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
20

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

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

noStopping :: DynLogic s -> DynLogic s
noStopping :: DynLogic s -> DynLogic s
noStopping DynLogic s
EmptySpec = DynLogic s
forall s. DynLogic s
EmptySpec
noStopping DynLogic s
Stop = DynLogic s
forall s. DynLogic s
EmptySpec
noStopping (After Any (Action s)
act DynPred s
k) = Any (Action s) -> DynPred s -> DynLogic s
forall s. Any (Action s) -> DynPred s -> DynLogic s
After Any (Action s)
act DynPred s
k
noStopping (AfterAny DynPred s
k) = DynPred s -> DynLogic s
forall s. DynPred s -> DynLogic s
AfterAny DynPred s
k
noStopping (Alt ChoiceType
b DynLogic s
d DynLogic s
d') = ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
b (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d) (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d')
noStopping (Stopping DynLogic s
_) = DynLogic s
forall s. DynLogic s
EmptySpec
noStopping (Weight Double
w DynLogic s
d) = Double -> DynLogic s -> DynLogic s
forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d)
noStopping (ForAll Quantification a
q a -> DynLogic s
f) = Quantification a -> (a -> DynLogic s) -> DynLogic s
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) = (Property -> Property) -> DynLogic s -> DynLogic s
forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
f (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d)

noAny :: DynLogic s -> DynLogic s
noAny :: DynLogic s -> DynLogic s
noAny DynLogic s
EmptySpec = DynLogic s
forall s. DynLogic s
EmptySpec
noAny DynLogic s
Stop = DynLogic s
forall s. DynLogic s
Stop
noAny (After Any (Action s)
act DynPred s
k) = Any (Action s) -> DynPred s -> DynLogic s
forall s. Any (Action s) -> DynPred s -> DynLogic s
After Any (Action s)
act DynPred s
k
noAny (AfterAny DynPred s
_) = DynLogic s
forall s. DynLogic s
EmptySpec
noAny (Alt ChoiceType
b DynLogic s
d DynLogic s
d') = ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
b (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d) (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d')
noAny (Stopping DynLogic s
d) = DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
Stopping (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d)
noAny (Weight Double
w DynLogic s
d) = Double -> DynLogic s -> DynLogic s
forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d)
noAny (ForAll Quantification a
q a -> DynLogic s
f) = Quantification a -> (a -> DynLogic s) -> DynLogic s
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) = (Property -> Property) -> DynLogic s -> DynLogic s
forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
f (DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d)

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

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

chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep :: s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep s
s Int
n DynLogic s
d =
  case (Double, DynLogic s) -> DynLogic s
forall a b. (a, b) -> b
snd ((Double, DynLogic s) -> DynLogic s)
-> [(Double, DynLogic s)] -> [DynLogic s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DynLogic s -> [(Double, DynLogic s)]
forall s. DynLogic s -> [(Double, DynLogic s)]
nextSteps DynLogic s
d of
    [] -> NextStep s -> m (NextStep s)
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
NoStep
    [DynLogic s
EmptySpec] -> NextStep s -> m (NextStep s)
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
NoStep
    [DynLogic s
Stop] -> NextStep s -> m (NextStep s)
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
StoppingStep
    [After (Some Action s a
a) DynPred s
k] -> NextStep s -> m (NextStep s)
forall (m :: * -> *) a. Monad m => a -> m a
return (NextStep s -> m (NextStep s)) -> NextStep s -> m (NextStep s)
forall a b. (a -> b) -> a -> b
$ TestStep s -> DynLogic s -> NextStep s
forall s. TestStep s -> DynLogic s -> NextStep s
Stepping (Step s -> TestStep s
forall s. Step s -> TestStep s
Do (Step s -> TestStep s) -> Step s -> TestStep s
forall a b. (a -> b) -> a -> b
$ Int -> Var a
forall a. Int -> Var a
Var Int
n Var a -> Action s a -> Step s
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 (s -> Action s a -> Var a -> s
forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState s
s Action s a
a (Int -> Var a
forall a. Int -> Var a
Var Int
n)))
    [DynLogic s]
_ -> String -> m (NextStep 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 :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil Int
0 Gen a
_ a -> Bool
_ = Maybe a -> Gen (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
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 Maybe a -> Gen (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Gen (Maybe a)) -> Maybe a -> Gen (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x else (Int -> Int) -> Gen (Maybe a) -> Gen (Maybe a)
forall a. (Int -> Int) -> Gen a -> Gen a
scale (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Gen (Maybe a) -> Gen (Maybe a)) -> Gen (Maybe a) -> Gen (Maybe a)
forall a b. (a -> b) -> a -> b
$ Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil (Int
n Int -> Int -> Int
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 :: 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' <- DynLogic s -> [TestStep s] -> [[TestStep s]]
forall t.
DynLogicModel t =>
DynLogic t -> [TestStep t] -> [[TestStep t]]
shrinkScript DynLogic s
d (DynLogicTest s -> [TestStep s]
forall s. DynLogicTest s -> [TestStep s]
getScript DynLogicTest s
tc), let test :: DynLogicTest s
test = DynLogic s -> [TestStep s] -> DynLogicTest s
forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned DynLogic s
d (DynLogic s -> [TestStep s] -> [TestStep s]
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 :: DynLogic t -> [TestStep t] -> [[TestStep t]]
shrinkScript DynLogic t
dl [TestStep t]
steps = DynLogic t -> [TestStep t] -> t -> [[TestStep t]]
forall t.
DynLogicModel t =>
DynLogic t -> [TestStep t] -> t -> [[TestStep t]]
shrink' DynLogic t
dl [TestStep t]
steps t
forall state. StateModel state => state
initialState
 where
  shrink' :: DynLogic t -> [TestStep t] -> t -> [[TestStep t]]
shrink' DynLogic t
_ [] t
_ = []
  shrink' DynLogic t
d (TestStep t
step : [TestStep t]
as) t
s =
    [] [TestStep t] -> [[TestStep t]] -> [[TestStep t]]
forall a. a -> [a] -> [a]
:
    [[TestStep t]] -> [[TestStep t]]
forall a. [a] -> [a]
reverse (([TestStep t] -> Bool) -> [[TestStep t]] -> [[TestStep t]]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> ([TestStep t] -> Bool) -> [TestStep t] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TestStep t] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [Int -> [TestStep t] -> [TestStep t]
forall a. Int -> [a] -> [a]
drop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [TestStep t]
as | Int
n <- (Int -> Int) -> Int -> [Int]
forall a. (a -> a) -> a -> [a]
iterate (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2) Int
1])
      [[TestStep t]] -> [[TestStep t]] -> [[TestStep t]]
forall a. [a] -> [a] -> [a]
++ case TestStep t
step of
        Do (Var Int
i := Action t a
act) ->
          [Step t -> TestStep t
forall s. Step s -> TestStep s
Do (Int -> Var a
forall a. Int -> Var a
Var Int
i Var a -> Action t a -> Step t
forall a state.
(Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action t a
act') TestStep t -> [TestStep t] -> [TestStep t]
forall a. a -> [a] -> [a]
: [TestStep t]
as | Some Action t a
act' <- t -> Action t a -> [Any (Action t)]
forall state a.
(StateModel state, Show a, Typeable a) =>
state -> Action state a -> [Any (Action state)]
shrinkAction t
s Action t 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.
          [ a -> TestStep t
forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a' TestStep t -> [TestStep t] -> [TestStep t]
forall a. a -> [a] -> [a]
: [TestStep t]
as' | a
a' <- DynLogic t -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic t
d a
a, [TestStep t]
as' <- [TestStep t]
as [TestStep t] -> [[TestStep t]] -> [[TestStep t]]
forall a. a -> [a] -> [a]
: DynLogic t -> [TestStep t] -> t -> [[TestStep t]]
shrink' (DynLogic t -> t -> TestStep t -> DynLogic t
forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic t
d t
s (a -> TestStep t
forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a')) [TestStep t]
as t
s
          ]
      [[TestStep t]] -> [[TestStep t]] -> [[TestStep t]]
forall a. [a] -> [a] -> [a]
++ [ TestStep t
step TestStep t -> [TestStep t] -> [TestStep t]
forall a. a -> [a] -> [a]
: [TestStep t]
as'
         | [TestStep t]
as' <- DynLogic t -> [TestStep t] -> t -> [[TestStep t]]
shrink' (DynLogic t -> t -> TestStep t -> DynLogic t
forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic t
d t
s TestStep t
step) [TestStep t]
as (t -> [[TestStep t]]) -> t -> [[TestStep t]]
forall a b. (a -> b) -> a -> b
$
            case TestStep t
step of
              Do (Var a
var := Action t a
act) -> t -> Action t a -> Var a -> t
forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState t
s Action t a
act Var a
var
              Witness a
_ -> t
s
         ]

shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness :: DynLogic s -> a -> [a]
shrinkWitness (ForAll (Quantification a
q :: Quantification a) a -> DynLogic s
_) (a
a :: a') =
  case (Typeable a, Typeable a) => Maybe (a :~: a)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl | Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a
a -> Quantification a -> a -> [a]
forall a. Quantification a -> a -> [a]
shrinkQ Quantification a
q a
a
a
    Maybe (a :~: a)
_ -> []
shrinkWitness (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') a
a = DynLogic s -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> 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 = DynLogic s -> 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 = DynLogic s -> 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 = DynLogic s -> 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 :: DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest DynLogic s
dl = [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
forall s.
DynLogicModel s =>
[DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s
dl] s
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)
    | s -> Action s a -> Bool
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' <- DynLogic s -> s -> TestStep s -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s (Step s -> TestStep s
forall s. Step s -> TestStep s
Do (Step s -> TestStep s) -> Step s -> TestStep s
forall a b. (a -> b) -> a -> b
$ Var a
var Var a -> Action s a -> Step s
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' ->
          Step s -> TestStep s
forall s. Step s -> TestStep s
Do (Var a
var Var a -> Action s a -> Step s
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) TestStep s -> [TestStep s] -> [TestStep s]
forall a. a -> [a] -> [a]
:
          [DynLogic s] -> s -> [TestStep s] -> [TestStep s]
prune [DynLogic s]
ds' (s -> Action s a -> Var a -> s
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' <- DynLogic s -> s -> TestStep s -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s (a -> TestStep 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' -> a -> TestStep s
forall s a. (Eq a, Show a, Typeable a) => a -> TestStep s
Witness a
a TestStep s -> [TestStep s] -> [TestStep s]
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 :: 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 Any (Action s) -> Any (Action s) -> Bool
forall a. Eq a => a -> a -> Bool
== Action s a -> Any (Action s)
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
act = [DynPred s
k (s -> Action s a -> Var a -> s
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 (Action s a -> Bool
forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
act) = [DynPred s
k (s -> Action s a -> Var a -> s
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 = DynLogic s -> s -> TestStep s -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step [DynLogic s] -> [DynLogic s] -> [DynLogic s]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> s -> TestStep s -> [DynLogic s]
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 = DynLogic s -> s -> TestStep s -> [DynLogic s]
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 = DynLogic s -> s -> TestStep s -> [DynLogic s]
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 (Typeable a, Typeable a) => Maybe (a :~: a)
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
a | Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a
a]
    Maybe (a :~: a)
Nothing -> []
stepDL (Monitor Property -> Property
_f DynLogic s
d) s
s TestStep s
step = DynLogic s -> s -> TestStep s -> [DynLogic s]
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 :: DynLogic s -> s -> TestStep s -> DynLogic s
stepDLtoDL DynLogic s
d s
s TestStep s
step = case DynLogic s -> s -> TestStep s -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d s
s TestStep s
step of
  [] -> DynLogic s
forall s. DynLogic s
EmptySpec
  [DynLogic s]
ds -> (DynLogic s -> DynLogic s -> DynLogic s)
-> [DynLogic s] -> DynLogic s
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
Demonic) [DynLogic s]
ds

propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property
propPruningGeneratedScriptIsNoop :: DynLogic s -> Property
propPruningGeneratedScriptIsNoop DynLogic s
d =
  Gen (DynLogicTest s) -> (DynLogicTest s -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s))
-> (Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ \Int
n -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 Int
n) Gen Int -> (Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= DynLogic s -> Int -> Gen (DynLogicTest s)
forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) ((DynLogicTest s -> Bool) -> Property)
-> (DynLogicTest s -> Bool) -> Property
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 [TestStep s] -> [TestStep s] -> Bool
forall a. Eq a => a -> a -> Bool
== DynLogic s -> [TestStep s] -> [TestStep s]
forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> [TestStep s]
pruneDLTest DynLogic s
d [TestStep s]
script

getScript :: DynLogicTest s -> [TestStep s]
getScript :: 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 :: DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned DynLogic s
dl = DynLogic s -> s -> [TestStep s] -> DynLogicTest s
forall t.
DynLogicModel t =>
DynLogic t -> t -> [TestStep t] -> DynLogicTest t
make DynLogic s
dl s
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 ([Any (Action t)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Any (Action t)]
bad) = [TestStep t] -> [Any (Action t)] -> t -> DynLogicTest t
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 = DynLogic t -> t -> [Any (Action t)]
forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic t
d t
s
  make DynLogic t
d t
s []
    | DynLogic t -> t -> Bool
forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic t
d t
s = [TestStep t] -> t -> DynLogicTest t
forall s. [TestStep s] -> s -> DynLogicTest s
Stuck [] t
s
    | Bool
otherwise = [TestStep t] -> DynLogicTest t
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
      (DynLogic t -> t -> TestStep t -> DynLogic t
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) -> t -> Action t a -> Var a -> t
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 -> [TestStep t] -> [Any (Action t)] -> t -> DynLogicTest t
forall s. [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s
BadPrecondition (TestStep t
step TestStep t -> [TestStep t] -> [TestStep t]
forall a. a -> [a] -> [a]
: [TestStep t]
as) [Any (Action t)]
bad t
s
      Stuck [TestStep t]
as t
s -> [TestStep t] -> t -> DynLogicTest t
forall s. [TestStep s] -> s -> DynLogicTest s
Stuck (TestStep t
step TestStep t -> [TestStep t] -> [TestStep t]
forall a. a -> [a] -> [a]
: [TestStep t]
as) t
s
      DLScript [TestStep t]
as -> [TestStep t] -> DynLogicTest t
forall s. [TestStep s] -> DynLogicTest s
DLScript (TestStep t
step TestStep t -> [TestStep t] -> [TestStep t]
forall a. a -> [a] -> [a]
: [TestStep t]
as)
      Looping{} -> String -> DynLogicTest t
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 :: DynLogic s -> DynLogicTest s -> DynLogicTest s
unfailDLTest DynLogic s
d DynLogicTest s
test = DynLogic s -> [TestStep s] -> DynLogicTest s
forall s.
DynLogicModel s =>
DynLogic s -> [TestStep s] -> DynLogicTest s
makeTestFromPruned DynLogic s
d ([TestStep s] -> DynLogicTest s) -> [TestStep s] -> DynLogicTest s
forall a b. (a -> b) -> a -> b
$ DynLogic s -> [TestStep s] -> [TestStep s]
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 :: 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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    Double -> Gen (Any (Action s)) -> (Any (Action s) -> Bool) -> Bool
forall a. Double -> Gen a -> (a -> Bool) -> Bool
canGenerate
      Double
0.01
      (s -> Gen (Any (Action s))
forall state. StateModel state => state -> Gen (Any (Action state))
arbitraryAction s
s)
      ( \case
          Some Action s a
act ->
            s -> Action s a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition s
s Action s a
act
              Bool -> Bool -> Bool
&& Bool -> Bool
not (Action s a -> Bool
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 = DynLogic s -> s -> Bool
forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s Bool -> Bool -> Bool
&& DynLogic s -> s -> 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 = DynLogic s -> s -> Bool
forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s Bool -> Bool -> Bool
|| DynLogic s -> s -> Bool
forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d' s
s
stuck (Stopping DynLogic s
d) s
s = DynLogic s -> s -> Bool
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
never Bool -> Bool -> Bool
|| DynLogic s -> s -> 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 = DynLogic s -> s -> Bool
forall s. DynLogicModel s => DynLogic s -> s -> Bool
stuck DynLogic s
d s
s

validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property
validDLTest :: DynLogic s -> DynLogicTest s -> Property
validDLTest DynLogic s
_ (DLScript [TestStep s]
_) = Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
validDLTest DynLogic s
_ (Stuck [TestStep s]
as s
_) = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Stuck\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([String] -> String
unlines ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [TestStep s] -> String
forall a. Show a => a -> String
show [TestStep s]
as)) Bool
False
validDLTest DynLogic s
_ (Looping [TestStep s]
as) = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Looping\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([String] -> String
unlines ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [TestStep s] -> String
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) = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"BadPrecondition\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [TestStep s] -> String
forall a. Show a => a -> String
show [TestStep s]
as String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (Any (Action s) -> String
forall (f :: * -> *). Show (Any f) => Any f -> String
showBad (Any (Action s) -> String) -> [Any (Action s)] -> [String]
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 = Any f -> String
forall a. Show a => a -> String
show Any f
a

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

badActions :: StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions :: 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
  | s -> Action s a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition s
s Action s a
a = []
  | Bool
otherwise = [Action s a -> Any (Action s)
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 = [String -> Any (Action 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 = DynLogic s -> s -> [Any (Action s)]
forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d s
s [Any (Action s)] -> [Any (Action s)] -> [Any (Action s)]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> s -> [Any (Action s)]
forall s. StateModel s => DynLogic s -> s -> [Any (Action s)]
badActions DynLogic s
d' s
s
badActions (Stopping DynLogic s
d) s
s = DynLogic s -> s -> [Any (Action 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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
never then [] else DynLogic s -> s -> [Any (Action s)]
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 = DynLogic s -> s -> [Any (Action 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 :: DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d (DLScript [TestStep s]
s) Property
p =
  case DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d s
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 :: DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
Stop s
_s [] = (Property -> Property) -> Maybe (Property -> Property)
forall a. a -> Maybe a
Just Property -> Property
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)
  | Action s a -> Any (Action s)
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
a Any (Action s) -> Any (Action s) -> Bool
forall a. Eq a => a -> a -> Bool
== Action s a -> Any (Action s)
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action s a
a' = DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
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' = s -> Action s a -> Var a -> 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 (Action s a -> Bool
forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
a) = DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring (Any (Action s) -> DynPred s -> DynLogic s
forall s. Any (Action s) -> DynPred s -> DynLogic s
After (Action s a -> Any (Action s)
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.
  DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring DynLogic s
d s
s [TestStep s]
as Maybe (Property -> Property)
-> Maybe (Property -> Property) -> Maybe (Property -> Property)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
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 = DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
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 = DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
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 (Typeable a, Typeable a) => Maybe (a :~: a)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
findMonitoring (a -> DynLogic s
k a
a
a) s
s [TestStep s]
as
    Maybe (a :~: a)
Nothing -> Maybe (Property -> Property)
forall a. Maybe a
Nothing
findMonitoring (Monitor Property -> Property
m DynLogic s
d) s
s [TestStep s]
as =
  (Property -> Property
m (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Property -> Property) -> Property -> Property)
-> Maybe (Property -> Property) -> Maybe (Property -> Property)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)
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]
_ = Maybe (Property -> Property)
forall a. Maybe a
Nothing