module Test.QuickCheck.DynamicLogic.Internal where

import Control.Applicative
import Control.Arrow (second)
import Control.Monad
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
    forall a.
    (Eq (Action s a), Show (Action s a), Typeable a) =>
    After (ActionWithPolarity s a) (Var a -> DynPred s)
  | Error String (DynPred s)
  | -- | Adjust the probability of picking a branch
    Weight Double (DynLogic s)
  | -- | Generating a random value
    forall a.
    QuantifyConstraints 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 = Annotated s -> DynLogic s

-- * Building formulae

-- | Ignore this formula, i.e. backtrack and try something else. @forAllScripts ignore (const True)@
--   will discard all test cases (equivalent to @False ==> True@).
ignore :: 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

-- | `True` for DL formulae.
passTest :: DynFormula s
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

-- | Given `f` must be `True` given /any/ state.
afterAny :: (Annotated s -> DynFormula s) -> DynFormula s
afterAny :: forall s. (Annotated s -> DynFormula s) -> DynFormula s
afterAny Annotated 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
$ \Annotated s
s -> forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (Annotated s -> DynFormula s
f Annotated s
s) Int
n

afterPolar
  :: (Typeable a, Eq (Action s a), Show (Action s a))
  => ActionWithPolarity s a
  -> (Var a -> Annotated s -> DynFormula s)
  -> DynFormula s
afterPolar :: forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
ActionWithPolarity s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
afterPolar ActionWithPolarity s a
act Var a -> Annotated s -> DynFormula s
f = forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula forall a b. (a -> b) -> a -> b
$ \Int
n -> forall s a.
(Eq (Action s a), Show (Action s a), Typeable a) =>
ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
After ActionWithPolarity s a
act forall a b. (a -> b) -> a -> b
$ \Var a
x Annotated s
s -> forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (Var a -> Annotated s -> DynFormula s
f Var a
x Annotated s
s) Int
n

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

-- | Given `f` must be `True` after /some/ negative action.
-- `f` is passed the state resulting from executing the `Action`
-- as a negative action.
afterNegative
  :: (Typeable a, Eq (Action s a), Show (Action s a))
  => Action s a
  -> (Annotated s -> DynFormula s)
  -> DynFormula s
afterNegative :: forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
Action s a -> (Annotated s -> DynFormula s) -> DynFormula s
afterNegative Action s a
act Annotated s -> DynFormula s
f = forall a s.
(Typeable a, Eq (Action s a), Show (Action s a)) =>
ActionWithPolarity s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
afterPolar (forall state a.
Eq (Action state a) =>
Action state a -> Polarity -> ActionWithPolarity state a
ActionWithPolarity Action s a
act Polarity
NegPolarity) (forall a b. a -> b -> a
const Annotated s -> DynFormula s
f)

-- | 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
-- In formulae, we use only angelic choice. But it becomes demonic
-- after one step (that is, the choice has been made).
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)

-- | 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
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.
QuantifyConstraints 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

-- | 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
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

-- | Get the current QuickCheck size parameter.
withSize :: (Int -> DynFormula s) -> DynFormula s
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

-- | Prioritise doing this if we are
-- trying to stop generation.
toStop :: DynFormula s -> DynFormula s
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

-- | Successfully ends the test.
done :: Annotated s -> DynFormula s
done :: forall s. Annotated s -> DynFormula s
done Annotated s
_ = forall s. DynFormula s
passTest

-- | Ends test with given error message.
errorDL :: String -> DynFormula s
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. String -> DynPred s -> DynLogic s
Error String
s (forall a b. a -> b -> a
const forall s. DynLogic s
EmptySpec)

-- | 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
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

-- | 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 :: (Annotated s -> DynFormula s) -> (Annotated s -> DynFormula s)
always :: forall s.
(Annotated s -> DynFormula s) -> Annotated s -> DynFormula s
always Annotated s -> DynFormula s
p Annotated 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 (Annotated s -> DynFormula s
p Annotated s
s) forall s. DynFormula s -> DynFormula s -> DynFormula s
||| Annotated s -> DynFormula s
p Annotated 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. (Annotated s -> DynFormula s) -> DynFormula s
afterAny (forall s.
(Annotated s -> DynFormula s) -> Annotated s -> DynFormula s
always Annotated s -> DynFormula s
p))

data FailingAction s
  = ErrorFail String
  | forall a. (Typeable a, Eq (Action s a)) => ActionFail (ActionWithPolarity s a)

instance StateModel s => HasVariables (FailingAction s) where
  getAllVariables :: FailingAction s -> Set (Any Var)
getAllVariables ErrorFail{} = forall a. Monoid a => a
mempty
  getAllVariables (ActionFail ActionWithPolarity s a
a) = forall a. HasVariables a => a -> Set (Any Var)
getAllVariables ActionWithPolarity s a
a

instance StateModel s => Eq (FailingAction s) where
  ErrorFail String
s == :: FailingAction s -> FailingAction s -> Bool
== ErrorFail String
s' = String
s forall a. Eq a => a -> a -> Bool
== String
s'
  ActionFail (ActionWithPolarity s a
a :: ActionWithPolarity s a) == ActionFail (ActionWithPolarity s a
a' :: ActionWithPolarity s a')
    | Just a :~: a
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' = ActionWithPolarity s a
a forall a. Eq a => a -> a -> Bool
== ActionWithPolarity s a
a'
  FailingAction s
_ == FailingAction s
_ = Bool
False

instance StateModel s => Show (FailingAction s) where
  show :: FailingAction s -> String
show (ErrorFail String
s) = String
"Error " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
s
  show (ActionFail (ActionWithPolarity Action s a
a Polarity
pol)) = forall a. Show a => a -> String
show Polarity
pol forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action s a
a

data DynLogicTest s
  = BadPrecondition (TestSequence s) (FailingAction s) (Annotated s)
  | Looping (TestSequence s)
  | Stuck (TestSequence s) (Annotated s)
  | DLScript (TestSequence s)

data Witnesses r where
  Do :: r -> Witnesses r
  Witness :: QuantifyConstraints a => a -> Witnesses r -> Witnesses r

discardWitnesses :: Witnesses r -> r
discardWitnesses :: forall r. Witnesses r -> r
discardWitnesses (Do r
r) = r
r
discardWitnesses (Witness a
_ Witnesses r
k) = forall r. Witnesses r -> r
discardWitnesses Witnesses r
k

pattern Witnesses :: Witnesses () -> r -> Witnesses r
pattern $bWitnesses :: forall r. Witnesses () -> r -> Witnesses r
$mWitnesses :: forall {r} {r}.
Witnesses r -> (Witnesses () -> r -> r) -> ((# #) -> r) -> r
Witnesses w r <- ((\Witnesses r
wit -> (forall (f :: * -> *) a. Functor f => f a -> f ()
void Witnesses r
wit, forall r. Witnesses r -> r
discardWitnesses Witnesses r
wit)) -> (w, r))
  where
    Witnesses Witnesses ()
w r
r = r
r forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Witnesses ()
w

{-# COMPLETE Witnesses #-}

deriving instance Functor Witnesses
deriving instance Foldable Witnesses
deriving instance Traversable Witnesses

instance Eq r => Eq (Witnesses r) where
  Do r
r == :: Witnesses r -> Witnesses r -> Bool
== Do r
r' = r
r forall a. Eq a => a -> a -> Bool
== r
r'
  Witness (a
a :: a) Witnesses r
k == Witness (a
a' :: a') Witnesses r
k' =
    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' Bool -> Bool -> Bool
&& Witnesses r
k forall a. Eq a => a -> a -> Bool
== Witnesses r
k'
      Maybe (a :~: a)
Nothing -> Bool
False
  Witnesses r
_ == Witnesses r
_ = Bool
False

instance Show r => Show (Witnesses r) where
  show :: Witnesses r -> String
show (Do r
r) = String
"Do $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show r
r
  show (Witness a
a Witnesses r
k) = 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
")\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Witnesses r
k -- TODO

type TestStep s = Witnesses (Step s)

newtype TestSequence s = TestSeq (Witnesses (TestContinuation s))

deriving instance StateModel s => Show (TestSequence s)
deriving instance StateModel s => Eq (TestSequence s)

data TestContinuation s
  = ContStep (Step s) (TestSequence s)
  | ContStop

pattern TestSeqStop :: TestSequence s
pattern $bTestSeqStop :: forall s. TestSequence s
$mTestSeqStop :: forall {r} {s}. TestSequence s -> ((# #) -> r) -> ((# #) -> r) -> r
TestSeqStop = TestSeq (Do ContStop)

pattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s
pattern $bTestSeqStep :: forall s. Step s -> TestSequence s -> TestSequence s
$mTestSeqStep :: forall {r} {s}.
TestSequence s
-> (Step s -> TestSequence s -> r) -> ((# #) -> r) -> r
TestSeqStep s ss = TestSeq (Do (ContStep s ss))

-- The `()` are the constraints required to use the pattern, and the `(Typeable a, ...)` are the
-- ones provided when you do (including a fresh type variable `a`).
-- See https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html#typing-of-pattern-synonyms
pattern TestSeqWitness :: () => forall a. QuantifyConstraints a => a -> TestSequence s -> TestSequence s
pattern $bTestSeqWitness :: forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
$mTestSeqWitness :: forall {r} {s}.
TestSequence s
-> (forall {a}. QuantifyConstraints a => a -> TestSequence s -> r)
-> ((# #) -> r)
-> r
TestSeqWitness a ss <- TestSeq (Witness a (TestSeq -> ss))
  where
    TestSeqWitness a
a (TestSeq Witnesses (TestContinuation s)
ss) = forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq (forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
a Witnesses (TestContinuation s)
ss)

{-# COMPLETE TestSeqWitness, TestSeqStep, TestSeqStop #-}

deriving instance StateModel s => Show (TestContinuation s)
deriving instance StateModel s => Eq (TestContinuation s)

consSeq :: TestStep s -> TestSequence s -> TestSequence s
consSeq :: forall s. TestStep s -> TestSequence s -> TestSequence s
consSeq TestStep s
step TestSequence s
ss = forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s. Step s -> TestSequence s -> TestContinuation s
ContStep TestSequence s
ss forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestStep s
step

unconsSeq :: TestSequence s -> Maybe (TestStep s, TestSequence s)
unconsSeq :: forall s. TestSequence s -> Maybe (TestStep s, TestSequence s)
unconsSeq (TestSeq Witnesses (TestContinuation s)
ss) =
  case forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
ss of
    TestContinuation s
ContStop -> forall a. Maybe a
Nothing
    ContStep Step s
s TestSequence s
rest -> forall a. a -> Maybe a
Just (Step s
s forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Witnesses (TestContinuation s)
ss, TestSequence s
rest)

unstopSeq :: TestSequence s -> Maybe (Witnesses ())
unstopSeq :: forall s. TestSequence s -> Maybe (Witnesses ())
unstopSeq (TestSeq Witnesses (TestContinuation s)
ss) =
  case forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
ss of
    TestContinuation s
ContStop -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ () forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Witnesses (TestContinuation s)
ss
    ContStep{} -> forall a. Maybe a
Nothing

pattern TestSeqStopW :: Witnesses () -> TestSequence s
pattern $bTestSeqStopW :: forall s. Witnesses () -> TestSequence s
$mTestSeqStopW :: forall {r} {s}.
TestSequence s -> (Witnesses () -> r) -> ((# #) -> r) -> r
TestSeqStopW w <- (unstopSeq -> Just w)
  where
    TestSeqStopW Witnesses ()
w = forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq (forall s. TestContinuation s
ContStop forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Witnesses ()
w)

pattern (:>) :: TestStep s -> TestSequence s -> TestSequence s
pattern step $b:> :: forall s. TestStep s -> TestSequence s -> TestSequence s
$m:> :: forall {r} {s}.
TestSequence s
-> (TestStep s -> TestSequence s -> r) -> ((# #) -> r) -> r
:> ss <- (unconsSeq -> Just (step, ss))
  where
    TestStep s
step :> TestSequence s
ss = forall s. TestStep s -> TestSequence s -> TestSequence s
consSeq TestStep s
step TestSequence s
ss

{-# COMPLETE TestSeqStopW, (:>) #-}

nullSeq :: TestSequence s -> Bool
nullSeq :: forall s. TestSequence s -> Bool
nullSeq TestSequence s
TestSeqStop = Bool
True
nullSeq TestSequence s
_ = Bool
False

dropSeq :: Int -> TestSequence s -> TestSequence s
dropSeq :: forall s. Int -> TestSequence s -> TestSequence s
dropSeq Int
n TestSequence s
_ | Int
n forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. HasCallStack => String -> a
error String
"dropSeq: negative number"
dropSeq Int
0 TestSequence s
ss = TestSequence s
ss
dropSeq Int
_ TestSequence s
TestSeqStop = forall s. TestSequence s
TestSeqStop
dropSeq Int
n (TestSeqWitness a
_ TestSequence s
ss) = forall s. Int -> TestSequence s -> TestSequence s
dropSeq (Int
n forall a. Num a => a -> a -> a
- Int
1) TestSequence s
ss
dropSeq Int
n (TestSeqStep Step s
_ TestSequence s
ss) = forall s. Int -> TestSequence s -> TestSequence s
dropSeq (Int
n forall a. Num a => a -> a -> a
- Int
1) TestSequence s
ss

getContinuation :: TestSequence s -> TestSequence s
getContinuation :: forall s. TestSequence s -> TestSequence s
getContinuation (TestSeq Witnesses (TestContinuation s)
w) = case forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
w of
  TestContinuation s
ContStop -> forall s. TestSequence s
TestSeqStop
  ContStep Step s
_ TestSequence s
s -> TestSequence s
s

unlines' :: [String] -> String
unlines' :: [String] -> String
unlines' [] = String
""
unlines' [String]
xs = forall a. [a] -> [a]
init forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
xs

prettyTestSequence :: VarContext -> TestSequence s -> String
prettyTestSequence :: forall s. VarContext -> TestSequence s -> String
prettyTestSequence VarContext
ctx TestSequence s
ss = [String] -> String
unlines' forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. [a] -> [a] -> [a]
(++) (String
"do " forall a. a -> [a] -> [a]
: forall a. a -> [a]
repeat String
"   ") forall a b. (a -> b) -> a -> b
$ TestSequence s -> [String]
prettySeq TestSequence s
ss
  where
    prettySeq :: TestSequence s -> [String]
prettySeq (TestSeqStopW Witnesses ()
w) = Witnesses () -> [String]
prettyWitnesses Witnesses ()
w
    prettySeq (Witnesses Witnesses ()
w Step s
step :> TestSequence s
ss') = Witnesses () -> [String]
prettyWitnesses Witnesses ()
w forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. VarContext -> a -> WithUsedVars a
WithUsedVars VarContext
ctx Step s
step) forall a. a -> [a] -> [a]
: TestSequence s -> [String]
prettySeq TestSequence s
ss'

prettyWitnesses :: Witnesses () -> [String]
prettyWitnesses :: Witnesses () -> [String]
prettyWitnesses (Witness a
a Witnesses ()
w) = (String
"_ <- forAllQ $ exactlyQ $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a) forall a. a -> [a] -> [a]
: Witnesses () -> [String]
prettyWitnesses Witnesses ()
w
prettyWitnesses Do{} = []

instance StateModel s => Show (DynLogicTest s) where
  show :: DynLogicTest s -> String
show (BadPrecondition TestSequence s
ss FailingAction s
bad Annotated s
s) =
    forall s. VarContext -> TestSequence s -> String
prettyTestSequence (forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> VarContext
allVariables FailingAction s
bad) TestSequence s
ss
      forall a. [a] -> [a] -> [a]
++ String
"\n   -- In state: "
      forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Annotated s
s
      forall a. [a] -> [a] -> [a]
++ String
"\n   "
      forall a. [a] -> [a] -> [a]
++ FailingAction s -> String
prettyBad FailingAction s
bad
    where
      prettyBad :: FailingAction s -> String
      prettyBad :: FailingAction s -> String
prettyBad (ErrorFail String
e) = String
"assert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
e forall a. [a] -> [a] -> [a]
++ String
" False"
      prettyBad (ActionFail (ActionWithPolarity Action s a
a Polarity
p)) = String
f forall a. [a] -> [a] -> [a]
++ String
" $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action s a
a forall a. [a] -> [a] -> [a]
++ String
"  -- Failed precondition\n   pure ()"
        where
          f :: String
f
            | Polarity
p forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = String
"action"
            | Bool
otherwise = String
"failingAction"
  show (Looping TestSequence s
ss) = forall s. VarContext -> TestSequence s -> String
prettyTestSequence (forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss) TestSequence s
ss forall a. [a] -> [a] -> [a]
++ String
"\n   pure ()\n   -- Looping"
  show (Stuck TestSequence s
ss Annotated s
s) = forall s. VarContext -> TestSequence s -> String
prettyTestSequence (forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss) TestSequence s
ss forall a. [a] -> [a] -> [a]
++ String
"\n   pure ()\n   -- Stuck in state " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Annotated s
s
  show (DLScript TestSequence s
ss) = forall s. VarContext -> TestSequence s -> String
prettyTestSequence (forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss) TestSequence s
ss forall a. [a] -> [a] -> [a]
++ String
"\n   pure ()\n"

usedVariables :: forall s. StateModel s => TestSequence s -> VarContext
usedVariables :: forall s. StateModel s => TestSequence s -> VarContext
usedVariables = Annotated s -> TestSequence s -> VarContext
go forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    go :: Annotated s -> TestSequence s -> VarContext
    go :: Annotated s -> TestSequence s -> VarContext
go Annotated s
aState TestSequence s
TestSeqStop = forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated s
aState)
    go Annotated s
aState (TestSeqWitness a
a TestSequence s
ss) = forall a. HasVariables a => a -> VarContext
allVariables a
a forall a. Semigroup a => a -> a -> a
<> Annotated s -> TestSequence s -> VarContext
go Annotated s
aState TestSequence s
ss
    go Annotated s
aState (TestSeqStep step :: Step s
step@(Var a
_ := ActionWithPolarity s a
act) TestSequence s
ss) =
      forall a. HasVariables a => a -> VarContext
allVariables ActionWithPolarity s a
act
        forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated s
aState)
        forall a. Semigroup a => a -> a -> a
<> Annotated s -> TestSequence s -> VarContext
go (forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep Step s
step Annotated s
aState) TestSequence s
ss

-- | 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

restrictedPolar :: DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar :: forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar (ActionWithPolarity Action s a
a Polarity
_) = forall s a. DynLogicModel s => Action s a -> Bool
restricted Action s a
a

-- * 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) =>
(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)
  => Annotated s
  -> DynFormula s
  -> (Actions s -> a)
  -> Property
forAllUniqueScripts :: forall s a.
(DynLogicModel s, Testable a) =>
Annotated s -> DynFormula s -> (Actions s -> a) -> Property
forAllUniqueScripts Annotated 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
        n :: Int
n = VarContext -> Int
unsafeNextVarIndex forall a b. (a -> b) -> a -> b
$ forall state. Annotated state -> VarContext
vars Annotated s
s
     in case forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(Annotated s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s)
generate forall (m :: * -> *) s.
(MonadFail m, DynLogicModel s) =>
Annotated s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep DynLogic s
d Int
n Annotated 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 -> Property
validDLTest DynLogic s
d DynLogicTest s
test forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)

-- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose.
forAllMappedScripts
  :: (DynLogicModel s, Testable a)
  => (rep -> DynLogicTest s)
  -> (DynLogicTest s -> rep)
  -> DynFormula s
  -> (Actions s -> a)
  -> Property
forAllMappedScripts :: forall s a rep.
(DynLogicModel s, Testable a) =>
(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 prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind
          (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)

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 -> Property
validDLTest DynLogic s
d DynLogicTest s
test forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> Property
validDLTest DynLogic s
d DynLogicTest s
test' forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =>
(Annotated s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s)
generate forall s.
DynLogicModel s =>
Annotated s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep DynLogic s
d Int
0 (forall s. StateModel s => DynLogic s -> Annotated s
initialStateFor DynLogic s
d) Int
size

onDLTestSeq :: (TestSequence s -> TestSequence s) -> DynLogicTest s -> DynLogicTest s
onDLTestSeq :: forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq TestSequence s -> TestSequence s
f (BadPrecondition TestSequence s
ss FailingAction s
bad Annotated s
s) = forall s.
TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
BadPrecondition (TestSequence s -> TestSequence s
f TestSequence s
ss) FailingAction s
bad Annotated s
s
onDLTestSeq TestSequence s -> TestSequence s
f (Looping TestSequence s
ss) = forall s. TestSequence s -> DynLogicTest s
Looping (TestSequence s -> TestSequence s
f TestSequence s
ss)
onDLTestSeq TestSequence s -> TestSequence s
f (Stuck TestSequence s
ss Annotated s
s) = forall s. TestSequence s -> Annotated s -> DynLogicTest s
Stuck (TestSequence s -> TestSequence s
f TestSequence s
ss) Annotated s
s
onDLTestSeq TestSequence s -> TestSequence s
f (DLScript TestSequence s
ss) = forall s. TestSequence s -> DynLogicTest s
DLScript (TestSequence s -> TestSequence s
f TestSequence s
ss)

consDLTest :: TestStep s -> DynLogicTest s -> DynLogicTest s
consDLTest :: forall s. TestStep s -> DynLogicTest s -> DynLogicTest s
consDLTest TestStep s
step = forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (TestStep s
step forall s. TestStep s -> TestSequence s -> TestSequence s
:>)

consDLTestW :: Witnesses () -> DynLogicTest s -> DynLogicTest s
consDLTestW :: forall s. Witnesses () -> DynLogicTest s -> DynLogicTest s
consDLTestW Witnesses ()
w = forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (forall {r} {s}. Witnesses r -> TestSequence s -> TestSequence s
addW Witnesses ()
w)
  where
    addW :: Witnesses r -> TestSequence s -> TestSequence s
addW Do{} TestSequence s
ss = TestSequence s
ss
    addW (Witness a
a Witnesses r
w') TestSequence s
ss = forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a (Witnesses r -> TestSequence s -> TestSequence s
addW Witnesses r
w' TestSequence s
ss)

generate
  :: (Monad m, DynLogicModel s)
  => (Annotated s -> Int -> DynLogic s -> m (NextStep s))
  -> DynLogic s
  -> Int
  -> Annotated s
  -> Int
  -> m (DynLogicTest s)
generate :: forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(Annotated s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s)
generate Annotated s -> Int -> DynLogic s -> m (NextStep s)
chooseNextStepFun DynLogic s
d Int
n Annotated s
s Int
size =
  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. TestSequence s -> DynLogicTest s
Looping forall s. TestSequence s
TestSeqStop
    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 (BadAction (Witnesses Witnesses ()
ws FailingAction s
bad)) m (DynLogicTest s)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s.
TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
BadPrecondition (forall s. Witnesses () -> TestSequence s
TestSeqStopW Witnesses ()
ws) FailingAction s
bad Annotated s
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. TestSequence s -> DynLogicTest s
DLScript forall s. TestSequence s
TestSeqStop
          useStep (Stepping Witnesses (Step s)
step DynLogic s
d') m (DynLogicTest s)
_ =
            case forall r. Witnesses r -> r
discardWitnesses Witnesses (Step s)
step of
              Var a
var := ActionWithPolarity s a
act ->
                forall s. TestStep s -> DynLogicTest s -> DynLogicTest s
consDLTest Witnesses (Step s)
step
                  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) s.
(Monad m, DynLogicModel s) =>
(Annotated s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s)
generate
                    Annotated 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, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
act Var a
var)
                    Int
size
          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 <- Annotated s -> Int -> DynLogic s -> m (NextStep s)
chooseNextStepFun Annotated 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. TestSequence s -> Annotated s -> DynLogicTest s
Stuck forall s. TestSequence s
TestSeqStop Annotated 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]

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 -> Annotated s
initialStateFor :: forall s. StateModel s => DynLogic s -> Annotated s
initialStateFor DynLogic s
_ = forall state. StateModel state => Annotated state
initialAnnotatedState

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 ActionWithPolarity s a
act Var a -> DynPred s
k) = forall s a.
(Eq (Action s a), Show (Action s a), Typeable a) =>
ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
After ActionWithPolarity s a
act Var a -> DynPred s
k
stopping (Error String
m DynPred s
k) = forall s. String -> DynPred s -> DynLogic s
Error String
m 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 ActionWithPolarity s a
act Var a -> DynPred s
k) = forall s a.
(Eq (Action s a), Show (Action s a), Typeable a) =>
ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
After ActionWithPolarity s a
act Var a -> DynPred s
k
noStopping (Error String
m DynPred s
k) = forall s. String -> DynPred s -> DynLogic s
Error String
m 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.
QuantifyConstraints 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 ActionWithPolarity s a
act Var a -> DynPred s
k) = forall s a.
(Eq (Action s a), Show (Action s a), Typeable a) =>
ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
After ActionWithPolarity s a
act Var a -> DynPred s
k
noAny (Error String
m DynPred s
k) = forall s. String -> DynPred s -> DynLogic s
Error String
m 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.
QuantifyConstraints 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 -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps :: forall s. DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps = forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> Gen a
generateQ

nextSteps' :: Monad m => (forall a. Quantification a -> m a) -> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' :: forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
_ DynLogic s
EmptySpec = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
nextSteps' forall a. Quantification a -> m a
_ DynLogic s
Stop = forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall s. DynLogic s
Stop)]
nextSteps' forall a. Quantification a -> m a
_ (After ActionWithPolarity s a
act Var a -> DynPred s
k) = forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall s a.
(Eq (Action s a), Show (Action s a), Typeable a) =>
ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
After ActionWithPolarity s a
act Var a -> DynPred s
k)]
nextSteps' forall a. Quantification a -> m a
_ (Error String
m DynPred s
k) = forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall s. String -> DynPred s -> DynLogic s
Error String
m DynPred s
k)]
nextSteps' forall a. Quantification a -> m a
_ (AfterAny DynPred s
k) = forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall s. DynPred s -> DynLogic s
AfterAny DynPred s
k)]
nextSteps' forall a. Quantification a -> m a
gen (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') = forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
gen DynLogic s
d forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
gen DynLogic s
d'
nextSteps' forall a. Quantification a -> m a
gen (Stopping DynLogic s
d) = forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
gen DynLogic s
d
nextSteps' forall a. Quantification a -> m a
gen (Weight Double
w DynLogic s
d) = do
  [(Double, Witnesses (DynLogic s))]
steps <- forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
gen DynLogic s
d
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
w forall a. Num a => a -> a -> a
* Double
w', Witnesses (DynLogic s)
s) | (Double
w', Witnesses (DynLogic s)
s) <- [(Double, Witnesses (DynLogic s))]
steps, Double
w forall a. Num a => a -> a -> a
* Double
w' forall a. Ord a => a -> a -> Bool
> Double
never]
nextSteps' forall a. Quantification a -> m a
gen (ForAll Quantification a
q a -> DynLogic s
f) = do
  a
x <- forall a. Quantification a -> m a
gen Quantification a
q
  forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
gen (a -> DynLogic s
f a
x)
nextSteps' forall a. Quantification a -> m a
gen (Monitor Property -> Property
_f DynLogic s
d) = forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' forall a. Quantification a -> m a
gen DynLogic s
d

chooseOneOf :: [(Double, a)] -> Gen a
chooseOneOf :: forall a. [(Double, a)] -> Gen a
chooseOneOf [(Double, a)]
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 a
s) | (Double
w, a
s) <- [(Double, a)]
steps]

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

data NextStep s
  = StoppingStep
  | Stepping (Witnesses (Step s)) (DynLogic s)
  | NoStep
  | BadAction (Witnesses (FailingAction s))

chooseNextStep :: DynLogicModel s => Annotated s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep :: forall s.
DynLogicModel s =>
Annotated s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep Annotated s
s Int
n DynLogic s
d = do
  forall s. DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps DynLogic s
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
    [(Double, Witnesses (DynLogic s))]
steps -> do
      let bads :: [Witnesses (FailingAction s)]
bads = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Witnesses (DynLogic s) -> [Witnesses (FailingAction s)]
findBad forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Double, Witnesses (DynLogic s))]
steps
          findBad :: Witnesses (DynLogic s) -> [Witnesses (FailingAction s)]
findBad = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions Annotated s
s
      case [Witnesses (FailingAction s)]
bads of
        [] -> do
          Witnesses (DynLogic s)
chosen <- forall a. [(Double, a)] -> Gen a
chooseOneOf [(Double, Witnesses (DynLogic s))]
steps
          let takeStep :: DynLogic s -> Gen (NextStep s)
takeStep = \case
                DynLogic s
Stop -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
StoppingStep
                After ActionWithPolarity s a
a Var a -> DynPred s
k ->
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping (forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall a. Int -> Var a
mkVar Int
n forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity s a
a) (Var a -> DynPred s
k (forall a. Int -> Var a
mkVar Int
n) (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
a (forall a. Int -> Var a
mkVar Int
n)))
                AfterAny DynPred s
k -> do
                  Maybe (Any (ActionWithPolarity s))
m <- forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil Int
100 (forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated s
s) forall a b. (a -> b) -> a -> b
$
                    \case
                      Some ActionWithPolarity s a
act -> forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated s
s ActionWithPolarity s a
act Bool -> Bool -> Bool
&& Bool -> Bool
not (forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar ActionWithPolarity s a
act)
                  case Maybe (Any (ActionWithPolarity s))
m of
                    Maybe (Any (ActionWithPolarity s))
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
                    Just (Some a :: ActionWithPolarity s a
a@ActionWithPolarity{}) ->
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                        forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping
                          (forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall a. Int -> Var a
mkVar Int
n forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity s a
a)
                          (DynPred s
k (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
a (forall a. Int -> Var a
mkVar Int
n)))
                DynLogic s
EmptySpec -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: EmptySpec"
                ForAll{} -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: ForAll"
                Error{} -> forall a. HasCallStack => String -> a
error String
"chooseNextStep: 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"
              go :: Witnesses (DynLogic s) -> Gen (NextStep s)
go (Do DynLogic s
d') = DynLogic s -> Gen (NextStep s)
takeStep DynLogic s
d'
              go (Witness a
a Witnesses (DynLogic s)
step) =
                Witnesses (DynLogic s) -> Gen (NextStep s)
go Witnesses (DynLogic s)
step
                  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                    NextStep s
StoppingStep -> forall s. NextStep s
StoppingStep -- TODO: This is a bit fishy
                    Stepping Witnesses (Step s)
step' DynLogic s
dl -> forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping (forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
a Witnesses (Step s)
step') DynLogic s
dl
                    NextStep s
NoStep -> forall s. NextStep s
NoStep
                    BadAction Witnesses (FailingAction s)
bad -> forall s. Witnesses (FailingAction s) -> NextStep s
BadAction (forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
a Witnesses (FailingAction s)
bad)
          Witnesses (DynLogic s) -> Gen (NextStep s)
go Witnesses (DynLogic s)
chosen
        Witnesses (FailingAction s)
b : [Witnesses (FailingAction s)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. Witnesses (FailingAction s) -> NextStep s
BadAction Witnesses (FailingAction s)
b

chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => Annotated s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep :: forall (m :: * -> *) s.
(MonadFail m, DynLogicModel s) =>
Annotated s -> Int -> DynLogic s -> m (NextStep s)
chooseUniqueNextStep Annotated s
s Int
n DynLogic s
d = do
  [Witnesses (DynLogic s)]
steps <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' (forall a b. a -> b -> a
const forall {a}. m a
bad) DynLogic s
d
  case [Witnesses (DynLogic s)]
steps of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
    [Do DynLogic s
EmptySpec] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
NoStep
    [Do DynLogic s
Stop] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall s. NextStep s
StoppingStep
    [Do (After ActionWithPolarity s a
a Var a -> DynPred s
k)] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping (forall r. r -> Witnesses r
Do forall a b. (a -> b) -> a -> b
$ forall a. Int -> Var a
mkVar Int
n forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity s a
a) (Var a -> DynPred s
k (forall a. Int -> Var a
mkVar Int
n) (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
a (forall a. Int -> Var a
mkVar Int
n)))
    [Witnesses (DynLogic s)]
_ -> forall {a}. m a
bad
  where
    bad :: m a
bad = 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 TestSequence s
_) = []
shrinkDLTest DynLogic s
d DynLogicTest s
tc =
  [ DynLogicTest s
test | TestSequence s
as' <- forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> [TestSequence s]
shrinkScript DynLogic s
d (forall s. DynLogicTest s -> TestSequence s
getScript DynLogicTest s
tc), let pruned :: TestSequence s
pruned = forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> TestSequence s
pruneDLTest DynLogic s
d TestSequence s
as'
                                                     test :: DynLogicTest s
test = forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> DynLogicTest s
makeTestFromPruned DynLogic s
d TestSequence s
pruned,
  -- Don't shrink a non-executable test case to an executable one.
  case (DynLogicTest s
tc, DynLogicTest s
test) of
    (DLScript TestSequence s
_, DynLogicTest s
_) -> Bool
True
    (DynLogicTest s
_, DLScript TestSequence s
_) -> Bool
False
    (DynLogicTest s, DynLogicTest s)
_ -> Bool
True
  ]

nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep :: forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep (Var a
var := ActionWithPolarity s a
act) Annotated s
s = forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
act Var a
var

shrinkScript :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s]
shrinkScript :: forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> [TestSequence s]
shrinkScript = Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink' forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    shrink' :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
    shrink' :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink' Annotated s
s DynLogic s
d TestSequence s
ss = Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
structural Annotated s
s DynLogic s
d TestSequence s
ss forall a. [a] -> [a] -> [a]
++ Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
nonstructural Annotated s
s DynLogic s
d TestSequence s
ss

    nonstructural :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
nonstructural Annotated s
s DynLogic s
d (TestSeqWitness a
a TestSequence s
ss) =
      [ forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a' TestSequence s
ss'
      | a
a' <- forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness @s DynLogic s
d a
a
      , TestSequence s
ss' <- TestSequence s
ss forall a. a -> [a] -> [a]
: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink' Annotated s
s (forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
s forall a b. (a -> b) -> a -> b
$ forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a forall s. TestSequence s
TestSeqStop) TestSequence s
ss
      ]
    nonstructural Annotated s
s DynLogic s
d (TestSeqStep step :: Step s
step@(Var a
var := ActionWithPolarity s a
act) TestSequence s
ss) =
      [forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep (forall a b. Var a -> Var b
unsafeCoerceVar Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity s a
act') TestSequence s
ss | Some act' :: ActionWithPolarity s a
act'@ActionWithPolarity{} <- forall state a.
(Typeable a, StateModel state) =>
Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
computeShrinkAction Annotated s
s ActionWithPolarity s a
act]
        forall a. [a] -> [a] -> [a]
++ [ forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step TestSequence s
ss'
           | TestSequence s
ss' <-
              Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink'
                (forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep Step s
step Annotated s
s)
                (forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> Step s -> DynLogic s
stepDLStep DynLogic s
d Annotated s
s Step s
step)
                TestSequence s
ss
           ]
    nonstructural Annotated s
_ DynLogic s
_ TestSequence s
TestSeqStop = []

    structural :: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
structural Annotated s
_ DynLogic s
_ TestSeqStopW{} = []
    structural Annotated s
s DynLogic s
d (TestStep s
step :> TestSequence s
rest) =
      forall s. TestSequence s
TestSeqStop
        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 s. TestSequence s -> Bool
nullSeq) [forall s. Int -> TestSequence s -> TestSequence s
dropSeq (Int
n forall a. Num a => a -> a -> a
- Int
1) TestSequence s
rest | 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]
++ forall a b. (a -> b) -> [a] -> [b]
map (TestStep s
step forall s. TestStep s -> TestSequence s -> TestSequence s
:>) (Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink' (forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep (forall r. Witnesses r -> r
discardWitnesses TestStep s
step) Annotated s
s) (forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
s (TestStep s
step forall s. TestStep s -> TestSequence s -> TestSequence s
:> forall s. TestSequence s
TestSeqStop)) TestSequence s
rest)

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 EmptySpec{} a
_ = []
shrinkWitness Stop{} a
_ = []
shrinkWitness Error{} a
_ = []
shrinkWitness After{} a
_ = []
shrinkWitness AfterAny{} a
_ = []

-- The result of pruning a list of actions is a prefix of a list of actions that
-- could have been generated by the dynamic logic.
pruneDLTest :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s
pruneDLTest :: forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> TestSequence s
pruneDLTest DynLogic s
dl = [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s
dl] forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    prune :: [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [] Annotated s
_ TestSequence s
_ = forall s. TestSequence s
TestSeqStop
    prune [DynLogic s]
_ Annotated s
_ TestSequence s
TestSeqStop = forall s. TestSequence s
TestSeqStop
    prune [DynLogic s]
ds Annotated s
s (TestSeqWitness a
a TestSequence s
ss) =
      case [DynLogic s
d' | DynLogic s
d <- [DynLogic s]
ds, DynLogic s
d' <- forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW @s DynLogic s
d a
a] of
        [] -> [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s]
ds Annotated s
s TestSequence s
ss
        [DynLogic s]
ds' -> forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a forall a b. (a -> b) -> a -> b
$ [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s]
ds' Annotated s
s TestSequence s
ss
    prune [DynLogic s]
ds Annotated s
s (TestSeqStep step :: Step s
step@(Var a
_ := ActionWithPolarity s a
act) TestSequence s
ss)
      | forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated s
s ActionWithPolarity s a
act =
          case [DynLogic s
d' | DynLogic s
d <- [DynLogic s]
ds, DynLogic s
d' <- forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s (forall r. r -> Witnesses r
Do Step s
step)] of
            [] -> [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s]
ds Annotated s
s TestSequence s
ss
            [DynLogic s]
ds' -> forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step forall a b. (a -> b) -> a -> b
$ [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s]
ds' (forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep Step s
step Annotated s
s) TestSequence s
ss
      | Bool
otherwise = [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s]
ds Annotated s
s TestSequence s
ss

stepDL :: DynLogicModel s => DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL :: forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL (After ActionWithPolarity s a
a Var a -> DynPred s
k) Annotated s
s (Do (Var a
var := ActionWithPolarity s a
act))
  -- TOOD: make this nicer when we migrate to 9.2 where we can just bind
  -- the type variables cleanly and do `Just Refl <- eqT ...` here instead.
  | forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
a forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
act = [Var a -> DynPred s
k (forall a b. Var a -> Var b
unsafeCoerceVar Var a
var) (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
act (forall a b. Var a -> Var b
unsafeCoerceVar Var a
var))]
stepDL (AfterAny DynPred s
k) Annotated s
s (Do (Var a
var := ActionWithPolarity s a
act))
  | Bool -> Bool
not (forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar ActionWithPolarity s a
act) = [DynPred s
k (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
act Var a
var)]
stepDL (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') Annotated s
s Witnesses (Step s)
step = forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s Witnesses (Step s)
step forall a. [a] -> [a] -> [a]
++ forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d' Annotated s
s Witnesses (Step s)
step
stepDL (Stopping DynLogic s
d) Annotated s
s Witnesses (Step s)
step = forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s Witnesses (Step s)
step
stepDL (Weight Double
_ DynLogic s
d) Annotated s
s Witnesses (Step s)
step = forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s Witnesses (Step s)
step
stepDL (ForAll (Quantification a
q :: Quantification a) a -> DynLogic s
f) Annotated s
s (Witness (a
a :: a') Witnesses (Step s)
step) =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> [DynLogic s
d | forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a, DynLogic s
d <- forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL (a -> DynLogic s
f a
a) Annotated s
s Witnesses (Step s)
step]
    Maybe (a :~: a)
Nothing -> []
stepDL (Monitor Property -> Property
_f DynLogic s
d) Annotated s
s Witnesses (Step s)
step = forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s Witnesses (Step s)
step
stepDL DynLogic s
_ Annotated s
_ Witnesses (Step s)
_ = []

stepDLW :: forall s a. (DynLogicModel s, Typeable a) => DynLogic s -> a -> [DynLogic s]
stepDLW :: forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW (ForAll (Quantification a
q :: Quantification a') a -> DynLogic s
k) 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
k a
a | forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a]
    Maybe (a :~: a)
Nothing -> []
stepDLW (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') a
a = forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d a
a forall a. [a] -> [a] -> [a]
++ forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d' a
a
stepDLW (Monitor Property -> Property
_ DynLogic s
d) a
a = forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d a
a
stepDLW (Weight Double
_ DynLogic s
d) a
a = forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d a
a
stepDLW (Stopping DynLogic s
d) a
a = forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d a
a
stepDLW DynLogic s
_ a
_ = []

stepDLSeq :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq :: forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
_ (TestSeqStopW Do{}) = DynLogic s
d
stepDLSeq DynLogic s
d Annotated s
s (TestSeqStopW (Witness a
a Witnesses ()
w)) = forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq (forall a s.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> DynLogic s
stepDLWitness DynLogic s
d a
a) Annotated s
s (forall s. Witnesses () -> TestSequence s
TestSeqStopW Witnesses ()
w)
stepDLSeq DynLogic s
d Annotated s
s (step :: TestStep s
step@(Witnesses Witnesses ()
_ (Var a
var := ActionWithPolarity s a
act)) :> TestSequence s
ss) =
  forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq (forall s. [DynLogic s] -> DynLogic s
demonicAlt forall a b. (a -> b) -> a -> b
$ forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s TestStep s
step) (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
act Var a
var) TestSequence s
ss

stepDLWitness :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> DynLogic s
stepDLWitness :: forall a s.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> DynLogic s
stepDLWitness DynLogic s
d a
a = forall s. [DynLogic s] -> DynLogic s
demonicAlt forall a b. (a -> b) -> a -> b
$ forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d a
a

stepDLStep :: DynLogicModel s => DynLogic s -> Annotated s -> Step s -> DynLogic s
stepDLStep :: forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> Step s -> DynLogic s
stepDLStep DynLogic s
d Annotated s
s Step s
step = forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
s (forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step forall s. TestSequence s
TestSeqStop)

demonicAlt :: [DynLogic s] -> DynLogic s
demonicAlt :: forall s. [DynLogic s] -> DynLogic s
demonicAlt [] = forall s. DynLogic s
EmptySpec
demonicAlt [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 :: TestSequence s
script = case DynLogicTest s
test of
          BadPrecondition TestSequence s
s FailingAction s
_ Annotated s
_ -> TestSequence s
s
          Looping TestSequence s
s -> TestSequence s
s
          Stuck TestSequence s
s Annotated s
_ -> TestSequence s
s
          DLScript TestSequence s
s -> TestSequence s
s
     in TestSequence s
script forall a. Eq a => a -> a -> Bool
== forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> TestSequence s
pruneDLTest DynLogic s
d TestSequence s
script

getScript :: DynLogicTest s -> TestSequence s
getScript :: forall s. DynLogicTest s -> TestSequence s
getScript (BadPrecondition TestSequence s
s FailingAction s
_ Annotated s
_) = TestSequence s
s
getScript (Looping TestSequence s
s) = TestSequence s
s
getScript (Stuck TestSequence s
s Annotated s
_) = TestSequence s
s
getScript (DLScript TestSequence s
s) = TestSequence s
s

makeTestFromPruned :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s
makeTestFromPruned :: forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> DynLogicTest s
makeTestFromPruned DynLogic s
dl = DynLogic s -> Annotated s -> TestSequence s -> DynLogicTest s
make DynLogic s
dl forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    make :: DynLogic s -> Annotated s -> TestSequence s -> DynLogicTest s
make DynLogic s
d Annotated s
s TestSequence s
TestSeqStop
      | FailingAction s
b : [FailingAction s]
_ <- forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions @s DynLogic s
d Annotated s
s = forall s.
TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
BadPrecondition forall s. TestSequence s
TestSeqStop FailingAction s
b Annotated s
s
      | forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s = forall s. TestSequence s -> Annotated s -> DynLogicTest s
Stuck forall s. TestSequence s
TestSeqStop Annotated s
s
      | Bool
otherwise = forall s. TestSequence s -> DynLogicTest s
DLScript forall s. TestSequence s
TestSeqStop
    make DynLogic s
d Annotated s
s (TestSeqWitness a
a TestSequence s
ss) =
      forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a) forall a b. (a -> b) -> a -> b
$
        DynLogic s -> Annotated s -> TestSequence s -> DynLogicTest s
make
          (forall a s.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> DynLogic s
stepDLWitness DynLogic s
d a
a)
          Annotated s
s
          TestSequence s
ss
    make DynLogic s
d Annotated s
s (TestSeqStep Step s
step TestSequence s
ss) =
      forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step) forall a b. (a -> b) -> a -> b
$
        DynLogic s -> Annotated s -> TestSequence s -> DynLogicTest s
make
          (forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> Step s -> DynLogic s
stepDLStep DynLogic s
d Annotated s
s Step s
step)
          (forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep Step s
step Annotated s
s)
          TestSequence s
ss

-- | 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 -> TestSequence s -> DynLogicTest s
makeTestFromPruned DynLogic s
d forall a b. (a -> b) -> a -> b
$ forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> TestSequence s
pruneDLTest DynLogic s
d TestSequence s
steps
  where
    steps :: TestSequence s
steps = case DynLogicTest s
test of
      BadPrecondition TestSequence s
as FailingAction s
_ Annotated s
_ -> TestSequence s
as
      Stuck TestSequence s
as Annotated s
_ -> TestSequence s
as
      DLScript TestSequence s
as -> TestSequence s
as
      Looping TestSequence s
as -> TestSequence s
as

stuck :: DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck :: forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
EmptySpec Annotated s
_ = Bool
True
stuck DynLogic s
Stop Annotated s
_ = Bool
False
stuck (After ActionWithPolarity s a
_ Var a -> DynPred s
_) Annotated s
_ = Bool
False
stuck (Error String
_ DynPred s
_) Annotated s
_ = Bool
False
stuck (AfterAny DynPred s
_) Annotated 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 =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated s
s)
      ( \case
          Some ActionWithPolarity s a
act ->
            forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated s
s ActionWithPolarity s a
act
              Bool -> Bool -> Bool
&& Bool -> Bool
not (forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar ActionWithPolarity s a
act)
      )
stuck (Alt ChoiceType
Angelic DynLogic s
d DynLogic s
d') Annotated s
s = forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s Bool -> Bool -> Bool
&& forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d' Annotated s
s
stuck (Alt ChoiceType
Demonic DynLogic s
d DynLogic s
d') Annotated s
s = forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s Bool -> Bool -> Bool
|| forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d' Annotated s
s
stuck (Stopping DynLogic s
d) Annotated s
s = forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s
stuck (Weight Double
w DynLogic s
d) Annotated s
s = Double
w forall a. Ord a => a -> a -> Bool
< Double
never Bool -> Bool -> Bool
|| forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s
stuck (ForAll Quantification a
_ a -> DynLogic s
_) Annotated s
_ = Bool
False
stuck (Monitor Property -> Property
_ DynLogic s
d) Annotated s
s = forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s

validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property -> Property
validDLTest :: forall s.
StateModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
validDLTest DynLogic s
_ Stuck{} Property
_ = Bool
False forall prop. Testable prop => Bool -> prop -> Property
==> Bool
False
validDLTest DynLogic s
_ test :: DynLogicTest s
test@DLScript{} Property
p = forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show DynLogicTest s
test) Property
p
validDLTest DynLogic s
_ DynLogicTest s
test Property
_ = forall prop. Testable prop => String -> prop -> Property
counterexample (forall a. Show a => a -> String
show DynLogicTest s
test) Bool
False

scriptFromDL :: DynLogicTest s -> Actions s
scriptFromDL :: forall s. DynLogicTest s -> Actions s
scriptFromDL (DLScript TestSequence s
s) = forall state. [Step state] -> Actions state
Actions forall a b. (a -> b) -> a -> b
$ forall s. TestSequence s -> [Step s]
sequenceSteps TestSequence s
s
scriptFromDL DynLogicTest s
_ = forall state. [Step state] -> Actions state
Actions []

sequenceSteps :: TestSequence s -> [Step s]
sequenceSteps :: forall s. TestSequence s -> [Step s]
sequenceSteps (TestSeq Witnesses (TestContinuation s)
ss) =
  case forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
ss of
    TestContinuation s
ContStop -> []
    ContStep Step s
s TestSequence s
ss' -> Step s
s forall a. a -> [a] -> [a]
: forall s. TestSequence s -> [Step s]
sequenceSteps TestSequence s
ss'

badActionsGiven :: StateModel s => DynLogic s -> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven :: forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
Stop Annotated s
_ Witnesses a
_ = []
badActionsGiven DynLogic s
EmptySpec Annotated s
_ Witnesses a
_ = []
badActionsGiven AfterAny{} Annotated s
_ Witnesses a
_ = []
badActionsGiven (ForAll Quantification a
_ a -> DynLogic s
k) Annotated s
s (Witness a
a Witnesses a
step) =
  case forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
a of
    Just a
a' -> forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
a' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven (a -> DynLogic s
k a
a') Annotated s
s Witnesses a
step
    Maybe a
_ -> []
badActionsGiven (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') Annotated s
s Witnesses a
w = forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
d Annotated s
s Witnesses a
w forall a. [a] -> [a] -> [a]
++ forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
d' Annotated s
s Witnesses a
w
badActionsGiven (Stopping DynLogic s
d) Annotated s
s Witnesses a
w = forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
d Annotated s
s Witnesses a
w
badActionsGiven (Weight Double
k DynLogic s
d) Annotated s
s Witnesses a
w = if Double
k forall a. Ord a => a -> a -> Bool
< Double
never then [] else forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
d Annotated s
s Witnesses a
w
badActionsGiven (Monitor Property -> Property
_ DynLogic s
d) Annotated s
s Witnesses a
w = forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
d Annotated s
s Witnesses a
w
badActionsGiven DynLogic s
d Annotated s
s (Do a
_) = forall r. r -> Witnesses r
Do forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d Annotated s
s
badActionsGiven Error{} Annotated s
_ Witnesses a
_ = []
badActionsGiven After{} Annotated s
_ Witnesses a
_ = []

badActions :: StateModel s => DynLogic s -> Annotated s -> [FailingAction s]
badActions :: forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
EmptySpec Annotated s
_ = []
badActions DynLogic s
Stop Annotated s
_ = []
badActions (After ActionWithPolarity s a
a Var a -> DynPred s
_) Annotated s
s
  | forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated s
s ActionWithPolarity s a
a = []
  | Bool
otherwise = [forall s a.
(Typeable a, Eq (Action s a)) =>
ActionWithPolarity s a -> FailingAction s
ActionFail ActionWithPolarity s a
a]
badActions (Error String
m DynPred s
_) Annotated s
_s = [forall s. String -> FailingAction s
ErrorFail String
m]
badActions (AfterAny DynPred s
_) Annotated s
_ = []
badActions (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') Annotated s
s = forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d Annotated s
s forall a. [a] -> [a] -> [a]
++ forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d' Annotated s
s
badActions (Stopping DynLogic s
d) Annotated s
s = forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d Annotated s
s
badActions (Weight Double
w DynLogic s
d) Annotated s
s = if Double
w forall a. Ord a => a -> a -> Bool
< Double
never then [] else forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d Annotated s
s
badActions (ForAll Quantification a
_ a -> DynLogic s
_) Annotated s
_ = []
badActions (Monitor Property -> Property
_ DynLogic s
d) Annotated s
s = forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d Annotated 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 TestSequence s
s) Property
p =
  case forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d forall state. StateModel state => Annotated state
initialAnnotatedState TestSequence 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 -> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring :: forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
Stop Annotated s
_s TestSequence s
TestSeqStop = forall a. a -> Maybe a
Just forall a. a -> a
id
findMonitoring (After ActionWithPolarity s a
a Var a -> DynPred s
k) Annotated s
s (TestSeqStep (Var a
var := ActionWithPolarity s a
a') TestSequence s
as)
  -- TODO: do nicely with eqT instead (avoids `unsafeCoerceVar`)
  | forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
a forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
a' = forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring (Var a -> DynPred s
k (forall a b. Var a -> Var b
unsafeCoerceVar Var a
var) Annotated s
s') Annotated s
s' TestSequence s
as
  where
    s' :: Annotated s
s' = forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated s
s ActionWithPolarity s a
a' (forall a b. Var a -> Var b
unsafeCoerceVar Var a
var)
findMonitoring (AfterAny DynPred s
k) Annotated s
s as :: TestSequence s
as@(TestSeqStep (Var a
_var := ActionWithPolarity s a
a) TestSequence s
_)
  | Bool -> Bool
not (forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar ActionWithPolarity s a
a) = forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring (forall s a.
(Eq (Action s a), Show (Action s a), Typeable a) =>
ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
After ActionWithPolarity s a
a forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const DynPred s
k) Annotated s
s TestSequence s
as
findMonitoring (Alt ChoiceType
_b DynLogic s
d DynLogic s
d') Annotated s
s TestSequence 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
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d Annotated s
s TestSequence s
as forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d' Annotated s
s TestSequence s
as
findMonitoring (Stopping DynLogic s
d) Annotated s
s TestSequence s
as = forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d Annotated s
s TestSequence s
as
findMonitoring (Weight Double
_ DynLogic s
d) Annotated s
s TestSequence s
as = forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d Annotated s
s TestSequence s
as
findMonitoring (ForAll (Quantification a
_q :: Quantification a) a -> DynLogic s
k) Annotated s
s (TestSeq (Witness (a
a :: a') Witnesses (TestContinuation 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
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring (a -> DynLogic s
k a
a) Annotated s
s (forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq Witnesses (TestContinuation s)
as)
    Maybe (a :~: a)
Nothing -> forall a. Maybe a
Nothing
findMonitoring (Monitor Property -> Property
m DynLogic s
d) Annotated s
s TestSequence 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
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d Annotated s
s TestSequence s
as
findMonitoring DynLogic s
_ Annotated s
_ TestSequence s
_ = forall a. Maybe a
Nothing