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
(ChoiceType -> ChoiceType -> Bool)
-> (ChoiceType -> ChoiceType -> Bool) -> Eq ChoiceType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ChoiceType -> ChoiceType -> Bool
== :: ChoiceType -> ChoiceType -> Bool
$c/= :: ChoiceType -> ChoiceType -> Bool
/= :: ChoiceType -> ChoiceType -> Bool
Eq, Int -> ChoiceType -> ShowS
[ChoiceType] -> ShowS
ChoiceType -> String
(Int -> ChoiceType -> ShowS)
-> (ChoiceType -> String)
-> ([ChoiceType] -> ShowS)
-> Show ChoiceType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ChoiceType -> ShowS
showsPrec :: Int -> ChoiceType -> ShowS
$cshow :: ChoiceType -> String
show :: ChoiceType -> String
$cshowList :: [ChoiceType] -> ShowS
showList :: [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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (DynLogic s -> Int -> DynLogic s) -> DynLogic s -> DynFormula s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> DynLogic s
forall a b. a -> b -> a
const (DynLogic s -> DynFormula s) -> DynLogic s -> DynFormula s
forall a b. (a -> b) -> a -> b
$ DynLogic s
forall s. DynLogic s
EmptySpec

-- | `True` for DL formulae.
passTest :: DynFormula s
passTest :: forall s. DynFormula s
passTest = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (DynLogic s -> Int -> DynLogic s) -> DynLogic s -> DynFormula s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> DynLogic s
forall a b. a -> b -> a
const (DynLogic s -> DynFormula s) -> DynLogic s -> DynFormula s
forall a b. (a -> b) -> a -> b
$ DynLogic s
forall s. DynLogic s
Stop

-- | 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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> DynPred s -> DynLogic s
forall s. DynPred s -> DynLogic s
AfterAny (DynPred s -> DynLogic s) -> DynPred s -> DynLogic s
forall a b. (a -> b) -> a -> b
$ \Annotated s
s -> DynFormula s -> Int -> DynLogic 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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
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) -> DynLogic s)
-> (Var a -> DynPred s) -> DynLogic s
forall a b. (a -> b) -> a -> b
$ \Var a
x Annotated s
s -> DynFormula s -> Int -> DynLogic 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 = ActionWithPolarity s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
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 (Action s a -> Polarity -> ActionWithPolarity s a
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 = ActionWithPolarity s a
-> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
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 (Action s a -> Polarity -> ActionWithPolarity s a
forall state a.
Eq (Action state a) =>
Action state a -> Polarity -> ActionWithPolarity state a
ActionWithPolarity Action s a
act Polarity
NegPolarity) ((Annotated s -> DynFormula s)
-> Var a -> Annotated s -> DynFormula s
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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
Angelic (Int -> DynLogic s
f Int
n) (Int -> DynLogic s
g Int
n)

-- | 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
  | Quantification (Quantifies q) -> Bool
forall a. Quantification a -> Bool
isEmptyQ Quantification (Quantifies q)
q' = DynFormula s
forall s. DynFormula s
ignore
  | Bool
otherwise = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> Quantification (Quantifies q)
-> (Quantifies q -> DynLogic s) -> DynLogic s
forall s a.
QuantifyConstraints a =>
Quantification a -> (a -> DynLogic s) -> DynLogic s
ForAll Quantification (Quantifies q)
q' ((Quantifies q -> DynLogic s) -> DynLogic s)
-> (Quantifies q -> DynLogic s) -> DynLogic s
forall a b. (a -> b) -> a -> b
$ ((Int -> DynLogic s) -> Int -> DynLogic s
forall a b. (a -> b) -> a -> b
$ Int
n) ((Int -> DynLogic s) -> DynLogic s)
-> (Quantifies q -> Int -> DynLogic s)
-> Quantifies q
-> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (DynFormula s -> Int -> DynLogic s)
-> (Quantifies q -> DynFormula s)
-> Quantifies q
-> Int
-> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantifies q -> DynFormula s
f
  where
    q' :: Quantification (Quantifies q)
q' = q -> Quantification (Quantifies q)
forall q. Quantifiable q => q -> Quantification (Quantifies q)
quantify q
q

-- | 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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ Double -> DynLogic s -> DynLogic s
forall s. Double -> DynLogic s -> DynLogic s
Weight Double
w (DynLogic s -> DynLogic s)
-> (Int -> DynLogic s) -> Int -> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f

-- | 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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula (Int -> DynFormula s
f Int
n) Int
n

-- | 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) = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
Stopping (DynLogic s -> DynLogic s)
-> (Int -> DynLogic s) -> Int -> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DynLogic s
f

-- | Successfully ends the test.
done :: Annotated s -> DynFormula s
done :: forall s. Annotated s -> DynFormula s
done Annotated s
_ = DynFormula 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 = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (DynLogic s -> Int -> DynLogic s) -> DynLogic s -> DynFormula s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> Int -> DynLogic s
forall a b. a -> b -> a
const (DynLogic s -> DynFormula s) -> DynLogic s -> DynFormula s
forall a b. (a -> b) -> a -> b
$ String -> DynPred s -> DynLogic s
forall s. String -> DynPred s -> DynLogic s
Error String
s (DynLogic s -> DynPred s
forall a b. a -> b -> a
const DynLogic s
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) = (Int -> DynLogic s) -> DynFormula s
forall s. (Int -> DynLogic s) -> DynFormula s
DynFormula ((Int -> DynLogic s) -> DynFormula s)
-> (Int -> DynLogic s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ (Property -> Property) -> DynLogic s -> DynLogic s
forall s. (Property -> Property) -> DynLogic s -> DynLogic s
Monitor Property -> Property
m (DynLogic s -> DynLogic s)
-> (Int -> DynLogic s) -> Int -> DynLogic s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DynLogic s
f

-- | 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 = (Int -> DynFormula s) -> DynFormula s
forall s. (Int -> DynFormula s) -> DynFormula s
withSize ((Int -> DynFormula s) -> DynFormula s)
-> (Int -> DynFormula s) -> DynFormula s
forall a b. (a -> b) -> a -> b
$ \Int
n -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s
toStop (Annotated s -> DynFormula s
p Annotated s
s) DynFormula s -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s -> DynFormula s
||| Annotated s -> DynFormula s
p Annotated s
s DynFormula s -> DynFormula s -> DynFormula s
forall s. DynFormula s -> DynFormula s -> DynFormula s
||| Double -> DynFormula s -> DynFormula s
forall s. Double -> DynFormula s -> DynFormula s
weight (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) ((Annotated s -> DynFormula s) -> DynFormula s
forall s. (Annotated s -> DynFormula s) -> DynFormula s
afterAny ((Annotated s -> DynFormula s) -> Annotated s -> DynFormula s
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{} = Set (Any Var)
forall a. Monoid a => a
mempty
  getAllVariables (ActionFail ActionWithPolarity s a
a) = ActionWithPolarity s a -> Set (Any Var)
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 String -> String -> Bool
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @a' = ActionWithPolarity s a
a ActionWithPolarity s a -> ActionWithPolarity s a -> Bool
forall a. Eq a => a -> a -> Bool
== ActionWithPolarity s a
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
  show (ActionFail (ActionWithPolarity Action s a
a Polarity
pol)) = Polarity -> String
forall a. Show a => a -> String
show Polarity
pol String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Action s a -> String
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) = Witnesses r -> r
forall r. Witnesses r -> r
discardWitnesses Witnesses r
k

pattern Witnesses :: Witnesses () -> r -> Witnesses r
pattern $mWitnesses :: forall {r} {r}.
Witnesses r -> (Witnesses () -> r -> r) -> ((# #) -> r) -> r
$bWitnesses :: forall r. Witnesses () -> r -> Witnesses r
Witnesses w r <- ((\Witnesses r
wit -> (Witnesses r -> Witnesses ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Witnesses r
wit, Witnesses r -> r
forall r. Witnesses r -> r
discardWitnesses Witnesses r
wit)) -> (w, r))
  where
    Witnesses Witnesses ()
w r
r = r
r r -> Witnesses () -> Witnesses r
forall a b. a -> Witnesses b -> Witnesses a
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 r -> r -> Bool
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @a' of
      Just a :~: a
Refl -> a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
a' Bool -> Bool -> Bool
&& Witnesses r
k Witnesses r -> Witnesses r -> Bool
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 $ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ r -> String
forall a. Show a => a -> String
show r
r
  show (Witness a
a Witnesses r
k) = String
"Witness (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf a
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Witnesses r -> String
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 $mTestSeqStop :: forall {r} {s}. TestSequence s -> ((# #) -> r) -> ((# #) -> r) -> r
$bTestSeqStop :: forall s. TestSequence s
TestSeqStop = TestSeq (Do ContStop)

pattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s
pattern $mTestSeqStep :: forall {r} {s}.
TestSequence s
-> (Step s -> TestSequence s -> r) -> ((# #) -> r) -> r
$bTestSeqStep :: forall s. Step s -> TestSequence s -> TestSequence s
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 $mTestSeqWitness :: forall {r} {s}.
TestSequence s
-> (forall {a}. QuantifyConstraints a => a -> TestSequence s -> r)
-> ((# #) -> r)
-> r
$bTestSeqWitness :: forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a ss <- TestSeq (Witness a (TestSeq -> ss))
  where
    TestSeqWitness a
a (TestSeq Witnesses (TestContinuation s)
ss) = Witnesses (TestContinuation s) -> TestSequence s
forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq (a
-> Witnesses (TestContinuation s) -> Witnesses (TestContinuation s)
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 = Witnesses (TestContinuation s) -> TestSequence s
forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq (Witnesses (TestContinuation s) -> TestSequence s)
-> Witnesses (TestContinuation s) -> TestSequence s
forall a b. (a -> b) -> a -> b
$ (Step s -> TestSequence s -> TestContinuation s)
-> TestSequence s -> Step s -> TestContinuation s
forall a b c. (a -> b -> c) -> b -> a -> c
flip Step s -> TestSequence s -> TestContinuation s
forall s. Step s -> TestSequence s -> TestContinuation s
ContStep TestSequence s
ss (Step s -> TestContinuation s)
-> TestStep s -> Witnesses (TestContinuation s)
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 Witnesses (TestContinuation s) -> TestContinuation s
forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
ss of
    TestContinuation s
ContStop -> Maybe (TestStep s, TestSequence s)
forall a. Maybe a
Nothing
    ContStep Step s
s TestSequence s
rest -> (TestStep s, TestSequence s) -> Maybe (TestStep s, TestSequence s)
forall a. a -> Maybe a
Just (Step s
s Step s -> Witnesses (TestContinuation s) -> TestStep s
forall a b. a -> Witnesses b -> Witnesses a
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 Witnesses (TestContinuation s) -> TestContinuation s
forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
ss of
    TestContinuation s
ContStop -> Witnesses () -> Maybe (Witnesses ())
forall a. a -> Maybe a
Just (Witnesses () -> Maybe (Witnesses ()))
-> Witnesses () -> Maybe (Witnesses ())
forall a b. (a -> b) -> a -> b
$ () () -> Witnesses (TestContinuation s) -> Witnesses ()
forall a b. a -> Witnesses b -> Witnesses a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Witnesses (TestContinuation s)
ss
    ContStep{} -> Maybe (Witnesses ())
forall a. Maybe a
Nothing

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

pattern (:>) :: TestStep s -> TestSequence s -> TestSequence s
pattern step $m:> :: forall {r} {s}.
TestSequence s
-> (TestStep s -> TestSequence s -> r) -> ((# #) -> r) -> r
$b:> :: forall s. TestStep s -> TestSequence s -> TestSequence s
:> ss <- (unconsSeq -> Just (step, ss))
  where
    TestStep s
step :> TestSequence s
ss = TestStep s -> TestSequence s -> TestSequence s
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = String -> TestSequence s
forall a. HasCallStack => String -> a
error String
"dropSeq: negative number"
dropSeq Int
0 TestSequence s
ss = TestSequence s
ss
dropSeq Int
_ TestSequence s
TestSeqStop = TestSequence s
forall s. TestSequence s
TestSeqStop
dropSeq Int
n (TestSeqWitness a
_ TestSequence s
ss) = Int -> TestSequence s -> TestSequence s
forall s. Int -> TestSequence s -> TestSequence s
dropSeq (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TestSequence s
ss
dropSeq Int
n (TestSeqStep Step s
_ TestSequence s
ss) = Int -> TestSequence s -> TestSequence s
forall s. Int -> TestSequence s -> TestSequence s
dropSeq (Int
n Int -> Int -> Int
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 Witnesses (TestContinuation s) -> TestContinuation s
forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
w of
  TestContinuation s
ContStop -> TestSequence s
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 = ShowS
forall a. HasCallStack => [a] -> [a]
init ShowS -> ShowS
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' ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> ShowS) -> [String] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> ShowS
forall a. [a] -> [a] -> [a]
(++) (String
"do " String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
forall a. a -> [a]
repeat String
"   ") ([String] -> [String]) -> [String] -> [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 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ WithUsedVars (Step s) -> String
forall a. Show a => a -> String
show (VarContext -> Step s -> WithUsedVars (Step s)
forall a. VarContext -> a -> WithUsedVars a
WithUsedVars VarContext
ctx Step s
step) String -> [String] -> [String]
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 $ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a) String -> [String] -> [String]
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) =
    VarContext -> TestSequence s -> String
forall s. VarContext -> TestSequence s -> String
prettyTestSequence (TestSequence s -> VarContext
forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss VarContext -> VarContext -> VarContext
forall a. Semigroup a => a -> a -> a
<> FailingAction s -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables FailingAction s
bad) TestSequence s
ss
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n   -- In state: "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Annotated s -> String
forall a. Show a => a -> String
show Annotated s
s
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n   "
      String -> ShowS
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" False"
      prettyBad (ActionFail (ActionWithPolarity Action s a
a Polarity
p)) = String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" $ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Action s a -> String
forall a. Show a => a -> String
show Action s a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"  -- Failed precondition\n   pure ()"
        where
          f :: String
f
            | Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = String
"action"
            | Bool
otherwise = String
"failingAction"
  show (Looping TestSequence s
ss) = VarContext -> TestSequence s -> String
forall s. VarContext -> TestSequence s -> String
prettyTestSequence (TestSequence s -> VarContext
forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss) TestSequence s
ss String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n   pure ()\n   -- Looping"
  show (Stuck TestSequence s
ss Annotated s
s) = VarContext -> TestSequence s -> String
forall s. VarContext -> TestSequence s -> String
prettyTestSequence (TestSequence s -> VarContext
forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss) TestSequence s
ss String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n   pure ()\n   -- Stuck in state " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Annotated s -> String
forall a. Show a => a -> String
show Annotated s
s
  show (DLScript TestSequence s
ss) = VarContext -> TestSequence s -> String
forall s. VarContext -> TestSequence s -> String
prettyTestSequence (TestSequence s -> VarContext
forall s. StateModel s => TestSequence s -> VarContext
usedVariables TestSequence s
ss) TestSequence s
ss String -> ShowS
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 Annotated s
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 = s -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables (Annotated s -> s
forall state. Annotated state -> state
underlyingState Annotated s
aState)
    go Annotated s
aState (TestSeqWitness a
a TestSequence s
ss) = a -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables a
a VarContext -> VarContext -> VarContext
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) =
      ActionWithPolarity s a -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables ActionWithPolarity s a
act
        VarContext -> VarContext -> VarContext
forall a. Semigroup a => a -> a -> a
<> s -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables (Annotated s -> s
forall state. Annotated state -> state
underlyingState Annotated s
aState)
        VarContext -> VarContext -> VarContext
forall a. Semigroup a => a -> a -> a
<> Annotated s -> TestSequence s -> VarContext
go (Step s -> Annotated s -> Annotated s
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
_) = Action s a -> Bool
forall a. Action s a -> Bool
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 = (DynLogicTest s -> DynLogicTest s)
-> (DynLogicTest s -> DynLogicTest s)
-> DynFormula s
-> (Actions s -> a)
-> Property
forall s a rep.
(DynLogicModel s, Testable a) =>
(rep -> DynLogicTest s)
-> (DynLogicTest s -> rep)
-> DynFormula s
-> (Actions s -> a)
-> Property
forAllMappedScripts DynLogicTest s -> DynLogicTest s
forall a. a -> a
id DynLogicTest s -> DynLogicTest s
forall a. a -> a
id

-- | `Property` function suitable for formulae without choice.
forAllUniqueScripts
  :: (DynLogicModel s, Testable a)
  => 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 =
  (Int -> Property) -> Property
forall prop. Testable prop => (Int -> prop) -> Property
QC.withSize ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
sz ->
    let d :: DynLogic s
d = DynFormula s -> Int -> DynLogic s
forall s. DynFormula s -> Int -> DynLogic s
unDynFormula DynFormula s
f Int
sz
        n :: Int
n = VarContext -> Int
unsafeNextVarIndex (VarContext -> Int) -> VarContext -> Int
forall a b. (a -> b) -> a -> b
$ Annotated s -> VarContext
forall state. Annotated state -> VarContext
vars Annotated s
s
     in case (Annotated s -> Int -> DynLogic s -> Maybe (NextStep s))
-> DynLogic s
-> Int
-> Annotated s
-> Int
-> Maybe (DynLogicTest s)
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 -> Maybe (NextStep s)
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 -> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Generating Non-unique script in forAllUniqueScripts" Bool
False
          Just DynLogicTest s
test -> DynLogic s -> DynLogicTest s -> Property -> Property
forall s.
StateModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
validDLTest DynLogic s
d DynLogicTest s
test (Property -> Property) -> (a -> Property) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> DynLogicTest s -> Property -> Property
forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test (Property -> Property) -> (a -> Property) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property
forall prop. Testable prop => prop -> Property
property (a -> Property) -> a -> Property
forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (DynLogicTest s -> Actions s
forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test)

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

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 =
  DynLogic s -> DynLogicTest s -> Property -> Property
forall s.
StateModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
validDLTest DynLogic s
d DynLogicTest s
test (Property -> Property) -> (a -> Property) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynLogic s -> DynLogicTest s -> Property -> Property
forall s.
DynLogicModel s =>
DynLogic s -> DynLogicTest s -> Property -> Property
applyMonitoring DynLogic s
d DynLogicTest s
test (Property -> Property) -> (a -> Property) -> a -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Property
forall prop. Testable prop => prop -> Property
property (a -> Property) -> a -> Property
forall a b. (a -> b) -> a -> b
$ Actions s -> a
k (DynLogicTest s -> Actions s
forall s. DynLogicTest s -> Actions s
scriptFromDL DynLogicTest s
test)

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

generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest :: forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d Int
size = (Annotated s -> Int -> DynLogic s -> Gen (NextStep s))
-> DynLogic s -> Int -> Annotated s -> Int -> Gen (DynLogicTest s)
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 -> Gen (NextStep s)
forall s.
DynLogicModel s =>
Annotated s -> Int -> DynLogic s -> Gen (NextStep s)
chooseNextStep DynLogic s
d Int
0 (DynLogic s -> Annotated s
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) = TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest 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) = TestSequence s -> DynLogicTest s
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) = TestSequence s -> Annotated s -> DynLogicTest 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) = TestSequence s -> DynLogicTest s
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 = (TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (TestStep s
step TestStep s -> TestSequence s -> TestSequence s
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 = (TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (Witnesses () -> TestSequence s -> TestSequence s
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 = a -> TestSequence s -> TestSequence s
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Int
sizeLimit Int
size
    then DynLogicTest s -> m (DynLogicTest s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ TestSequence s -> DynLogicTest s
forall s. TestSequence s -> DynLogicTest s
Looping TestSequence s
forall s. TestSequence s
TestSeqStop
    else do
      let preferred :: DynLogic s
preferred = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
size then DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
stopping DynLogic s
d else DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noStopping DynLogic s
d
          useStep :: NextStep s -> m (DynLogicTest s) -> m (DynLogicTest s)
useStep (BadAction (Witnesses Witnesses ()
ws FailingAction s
bad)) m (DynLogicTest s)
_ = DynLogicTest s -> m (DynLogicTest s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
forall s.
TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
BadPrecondition (Witnesses () -> TestSequence s
forall s. Witnesses () -> TestSequence s
TestSeqStopW Witnesses ()
ws) FailingAction s
bad Annotated s
s
          useStep NextStep s
StoppingStep m (DynLogicTest s)
_ = DynLogicTest s -> m (DynLogicTest s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ TestSequence s -> DynLogicTest s
forall s. TestSequence s -> DynLogicTest s
DLScript TestSequence s
forall s. TestSequence s
TestSeqStop
          useStep (Stepping Witnesses (Step s)
step DynLogic s
d') m (DynLogicTest s)
_ =
            case Witnesses (Step s) -> Step s
forall r. Witnesses r -> r
discardWitnesses Witnesses (Step s)
step of
              Var a
var := ActionWithPolarity s a
act ->
                Witnesses (Step s) -> DynLogicTest s -> DynLogicTest s
forall s. TestStep s -> DynLogicTest s -> DynLogicTest s
consDLTest Witnesses (Step s)
step
                  (DynLogicTest s -> DynLogicTest s)
-> m (DynLogicTest s) -> m (DynLogicTest s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Annotated s -> Int -> DynLogic s -> m (NextStep s))
-> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s)
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                    (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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)
                    Int
size
          useStep NextStep s
NoStep m (DynLogicTest s)
alt = m (DynLogicTest s)
alt
      (DynLogic s -> m (DynLogicTest s) -> m (DynLogicTest s))
-> m (DynLogicTest s) -> [DynLogic s] -> m (DynLogicTest s)
forall a b. (a -> b -> b) -> b -> [a] -> b
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)
        (DynLogicTest s -> m (DynLogicTest s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DynLogicTest s -> m (DynLogicTest s))
-> DynLogicTest s -> m (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ TestSequence s -> Annotated s -> DynLogicTest s
forall s. TestSequence s -> Annotated s -> DynLogicTest s
Stuck TestSequence s
forall s. TestSequence s
TestSeqStop Annotated s
s)
        [DynLogic s
preferred, DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
preferred, DynLogic s
d, DynLogic s -> DynLogic s
forall s. DynLogic s -> DynLogic s
noAny DynLogic s
d]

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

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

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

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

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

nextSteps :: DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps :: forall s. DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps = (forall a. Quantification a -> Gen a)
-> DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> Gen a
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 = [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
nextSteps' forall a. Quantification a -> m a
_ DynLogic s
Stop = [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, DynLogic s -> Witnesses (DynLogic s)
forall r. r -> Witnesses r
Do (DynLogic s -> Witnesses (DynLogic s))
-> DynLogic s -> Witnesses (DynLogic s)
forall a b. (a -> b) -> a -> b
$ DynLogic s
forall s. DynLogic s
Stop)]
nextSteps' forall a. Quantification a -> m a
_ (After ActionWithPolarity s a
act Var a -> DynPred s
k) = [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, DynLogic s -> Witnesses (DynLogic s)
forall r. r -> Witnesses r
Do (DynLogic s -> Witnesses (DynLogic s))
-> DynLogic s -> Witnesses (DynLogic s)
forall a b. (a -> b) -> a -> b
$ ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
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) = [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, DynLogic s -> Witnesses (DynLogic s)
forall r. r -> Witnesses r
Do (DynLogic s -> Witnesses (DynLogic s))
-> DynLogic s -> Witnesses (DynLogic s)
forall a b. (a -> b) -> a -> b
$ String -> DynPred s -> DynLogic s
forall s. String -> DynPred s -> DynLogic s
Error String
m DynPred s
k)]
nextSteps' forall a. Quantification a -> m a
_ (AfterAny DynPred s
k) = [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
1, DynLogic s -> Witnesses (DynLogic s)
forall r. r -> Witnesses r
Do (DynLogic s -> Witnesses (DynLogic s))
-> DynLogic s -> Witnesses (DynLogic s)
forall a b. (a -> b) -> a -> b
$ DynPred s -> DynLogic s
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') = [(Double, Witnesses (DynLogic s))]
-> [(Double, Witnesses (DynLogic s))]
-> [(Double, Witnesses (DynLogic s))]
forall a. [a] -> [a] -> [a]
(++) ([(Double, Witnesses (DynLogic s))]
 -> [(Double, Witnesses (DynLogic s))]
 -> [(Double, Witnesses (DynLogic s))])
-> m [(Double, Witnesses (DynLogic s))]
-> m ([(Double, Witnesses (DynLogic s))]
      -> [(Double, Witnesses (DynLogic s))])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> m a
forall a. Quantification a -> m a
gen DynLogic s
d m ([(Double, Witnesses (DynLogic s))]
   -> [(Double, Witnesses (DynLogic s))])
-> m [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> m a
forall a. Quantification a -> m a
gen DynLogic s
d'
nextSteps' forall a. Quantification a -> m a
gen (Stopping DynLogic s
d) = (forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> m a
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 a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> m a
forall a. Quantification a -> m a
gen DynLogic s
d
  [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Double
w Double -> Double -> Double
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 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
w' Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double
never]
nextSteps' forall a. Quantification a -> m a
gen (ForAll Quantification a
q a -> DynLogic s
f) = do
  a
x <- Quantification a -> m a
forall a. Quantification a -> m a
gen Quantification a
q
  ((Double, Witnesses (DynLogic s))
 -> (Double, Witnesses (DynLogic s)))
-> [(Double, Witnesses (DynLogic s))]
-> [(Double, Witnesses (DynLogic s))]
forall a b. (a -> b) -> [a] -> [b]
map ((Witnesses (DynLogic s) -> Witnesses (DynLogic s))
-> (Double, Witnesses (DynLogic s))
-> (Double, Witnesses (DynLogic s))
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Witnesses (DynLogic s) -> Witnesses (DynLogic s))
 -> (Double, Witnesses (DynLogic s))
 -> (Double, Witnesses (DynLogic s)))
-> (Witnesses (DynLogic s) -> Witnesses (DynLogic s))
-> (Double, Witnesses (DynLogic s))
-> (Double, Witnesses (DynLogic s))
forall a b. (a -> b) -> a -> b
$ a -> Witnesses (DynLogic s) -> Witnesses (DynLogic s)
forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
x) ([(Double, Witnesses (DynLogic s))]
 -> [(Double, Witnesses (DynLogic s))])
-> m [(Double, Witnesses (DynLogic s))]
-> m [(Double, Witnesses (DynLogic s))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> m a
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 a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' Quantification a -> m a
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 = [(Int, Gen a)] -> Gen a
forall a. [(Int, Gen a)] -> Gen a
frequency [(Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Double
w Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
never), a -> Gen a
forall a. a -> Gen a
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
  DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
forall s. DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps DynLogic s
d Gen [(Double, Witnesses (DynLogic s))]
-> ([(Double, Witnesses (DynLogic s))] -> Gen (NextStep s))
-> Gen (NextStep s)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    [] -> NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
NoStep
    [(Double, Witnesses (DynLogic s))]
steps -> do
      let bads :: [Witnesses (FailingAction s)]
bads = ((Double, Witnesses (DynLogic s)) -> [Witnesses (FailingAction s)])
-> [(Double, Witnesses (DynLogic s))]
-> [Witnesses (FailingAction s)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Witnesses (DynLogic s) -> [Witnesses (FailingAction s)]
findBad (Witnesses (DynLogic s) -> [Witnesses (FailingAction s)])
-> ((Double, Witnesses (DynLogic s)) -> Witnesses (DynLogic s))
-> (Double, Witnesses (DynLogic s))
-> [Witnesses (FailingAction s)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double, Witnesses (DynLogic s)) -> Witnesses (DynLogic s)
forall a b. (a, b) -> b
snd) [(Double, Witnesses (DynLogic s))]
steps
          findBad :: Witnesses (DynLogic s) -> [Witnesses (FailingAction s)]
findBad = (DynLogic s -> [FailingAction s])
-> Witnesses (DynLogic s) -> [Witnesses (FailingAction s)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Witnesses a -> f (Witnesses b)
traverse ((DynLogic s -> [FailingAction s])
 -> Witnesses (DynLogic s) -> [Witnesses (FailingAction s)])
-> (DynLogic s -> [FailingAction s])
-> Witnesses (DynLogic s)
-> [Witnesses (FailingAction s)]
forall a b. (a -> b) -> a -> b
$ (DynLogic s -> Annotated s -> [FailingAction s])
-> Annotated s -> DynLogic s -> [FailingAction s]
forall a b c. (a -> b -> c) -> b -> a -> c
flip DynLogic s -> Annotated s -> [FailingAction s]
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 <- [(Double, Witnesses (DynLogic s))] -> Gen (Witnesses (DynLogic s))
forall a. [(Double, a)] -> Gen a
chooseOneOf [(Double, Witnesses (DynLogic s))]
steps
          let takeStep :: DynLogic s -> Gen (NextStep s)
takeStep = \case
                DynLogic s
Stop -> NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
StoppingStep
                After ActionWithPolarity s a
a Var a -> DynPred s
k ->
                  NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (NextStep s -> Gen (NextStep s)) -> NextStep s -> Gen (NextStep s)
forall a b. (a -> b) -> a -> b
$ Witnesses (Step s) -> DynLogic s -> NextStep s
forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping (Step s -> Witnesses (Step s)
forall r. r -> Witnesses r
Do (Step s -> Witnesses (Step s)) -> Step s -> Witnesses (Step s)
forall a b. (a -> b) -> a -> b
$ Int -> Var a
forall a. Int -> Var a
mkVar Int
n Var a -> ActionWithPolarity s a -> Step s
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 (Int -> Var a
forall a. Int -> Var a
mkVar Int
n) (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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 (Int -> Var a
forall a. Int -> Var a
mkVar Int
n)))
                AfterAny DynPred s
k -> do
                  Maybe (Any (ActionWithPolarity s))
m <- Int
-> Gen (Any (ActionWithPolarity s))
-> (Any (ActionWithPolarity s) -> Bool)
-> Gen (Maybe (Any (ActionWithPolarity s)))
forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil Int
100 (Annotated s -> Gen (Any (ActionWithPolarity s))
forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated s
s) ((Any (ActionWithPolarity s) -> Bool)
 -> Gen (Maybe (Any (ActionWithPolarity s))))
-> (Any (ActionWithPolarity s) -> Bool)
-> Gen (Maybe (Any (ActionWithPolarity s)))
forall a b. (a -> b) -> a -> b
$
                    \case
                      Some ActionWithPolarity s a
act -> Annotated s -> ActionWithPolarity s a -> Bool
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 (ActionWithPolarity s a -> Bool
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 -> NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
NoStep
                    Just (Some a :: ActionWithPolarity s a
a@ActionWithPolarity{}) ->
                      NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (NextStep s -> Gen (NextStep s)) -> NextStep s -> Gen (NextStep s)
forall a b. (a -> b) -> a -> b
$
                        Witnesses (Step s) -> DynLogic s -> NextStep s
forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping
                          (Step s -> Witnesses (Step s)
forall r. r -> Witnesses r
Do (Step s -> Witnesses (Step s)) -> Step s -> Witnesses (Step s)
forall a b. (a -> b) -> a -> b
$ Int -> Var a
forall a. Int -> Var a
mkVar Int
n Var a -> ActionWithPolarity s a -> Step s
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 (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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 (Int -> Var a
forall a. Int -> Var a
mkVar Int
n)))
                DynLogic s
EmptySpec -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: EmptySpec"
                ForAll{} -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: ForAll"
                Error{} -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: Error"
                Alt{} -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: Alt"
                Stopping{} -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: Stopping"
                Weight{} -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: Weight"
                Monitor{} -> String -> Gen (NextStep s)
forall a. HasCallStack => String -> a
error String
"chooseNextStep: Monitor"
              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
                  Gen (NextStep s)
-> (NextStep s -> Gen (NextStep s)) -> Gen (NextStep s)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NextStep s -> Gen (NextStep s))
-> (NextStep s -> NextStep s) -> NextStep s -> Gen (NextStep s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
                    NextStep s
StoppingStep -> NextStep s
forall s. NextStep s
StoppingStep -- TODO: This is a bit fishy
                    Stepping Witnesses (Step s)
step' DynLogic s
dl -> Witnesses (Step s) -> DynLogic s -> NextStep s
forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping (a -> Witnesses (Step s) -> Witnesses (Step s)
forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
a Witnesses (Step s)
step') DynLogic s
dl
                    NextStep s
NoStep -> NextStep s
forall s. NextStep s
NoStep
                    BadAction Witnesses (FailingAction s)
bad -> Witnesses (FailingAction s) -> NextStep s
forall s. Witnesses (FailingAction s) -> NextStep s
BadAction (a -> Witnesses (FailingAction s) -> Witnesses (FailingAction s)
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)]
_ -> NextStep s -> Gen (NextStep s)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (NextStep s -> Gen (NextStep s)) -> NextStep s -> Gen (NextStep s)
forall a b. (a -> b) -> a -> b
$ Witnesses (FailingAction s) -> NextStep s
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 <- ((Double, Witnesses (DynLogic s)) -> Witnesses (DynLogic s))
-> [(Double, Witnesses (DynLogic s))] -> [Witnesses (DynLogic s)]
forall a b. (a -> b) -> [a] -> [b]
map (Double, Witnesses (DynLogic s)) -> Witnesses (DynLogic s)
forall a b. (a, b) -> b
snd ([(Double, Witnesses (DynLogic s))] -> [Witnesses (DynLogic s)])
-> m [(Double, Witnesses (DynLogic s))]
-> m [Witnesses (DynLogic s)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
forall (m :: * -> *) s.
Monad m =>
(forall a. Quantification a -> m a)
-> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
nextSteps' (m a -> Quantification a -> m a
forall a b. a -> b -> a
const m a
forall {a}. m a
bad) DynLogic s
d
  case [Witnesses (DynLogic s)]
steps of
    [] -> NextStep s -> m (NextStep s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
NoStep
    [Do DynLogic s
EmptySpec] -> NextStep s -> m (NextStep s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
NoStep
    [Do DynLogic s
Stop] -> NextStep s -> m (NextStep s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return NextStep s
forall s. NextStep s
StoppingStep
    [Do (After ActionWithPolarity s a
a Var a -> DynPred s
k)] -> NextStep s -> m (NextStep s)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NextStep s -> m (NextStep s)) -> NextStep s -> m (NextStep s)
forall a b. (a -> b) -> a -> b
$ Witnesses (Step s) -> DynLogic s -> NextStep s
forall s. Witnesses (Step s) -> DynLogic s -> NextStep s
Stepping (Step s -> Witnesses (Step s)
forall r. r -> Witnesses r
Do (Step s -> Witnesses (Step s)) -> Step s -> Witnesses (Step s)
forall a b. (a -> b) -> a -> b
$ Int -> Var a
forall a. Int -> Var a
mkVar Int
n Var a -> ActionWithPolarity s a -> Step s
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 (Int -> Var a
forall a. Int -> Var a
mkVar Int
n) (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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 (Int -> Var a
forall a. Int -> Var a
mkVar Int
n)))
    [Witnesses (DynLogic s)]
_ -> m (NextStep s)
forall {a}. m a
bad
  where
    bad :: m a
bad = String -> m a
forall a. String -> m a
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
_ = Maybe a -> Gen (Maybe a)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
keepTryingUntil Int
n Gen a
g a -> Bool
p = do
  a
x <- Gen a
g
  if a -> Bool
p a
x then Maybe a -> Gen (Maybe a)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Gen (Maybe a)) -> Maybe a -> Gen (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x else (Int -> Int) -> Gen (Maybe a) -> Gen (Maybe a)
forall a. (Int -> Int) -> Gen a -> Gen a
scale (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Gen (Maybe a) -> Gen (Maybe a)) -> Gen (Maybe a) -> Gen (Maybe a)
forall a b. (a -> b) -> a -> b
$ Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
forall a. Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
keepTryingUntil (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Gen a
g a -> Bool
p

shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]
shrinkDLTest :: 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' <- DynLogic s -> TestSequence s -> [TestSequence s]
forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> [TestSequence s]
shrinkScript DynLogic s
d (DynLogicTest s -> TestSequence s
forall s. DynLogicTest s -> TestSequence s
getScript DynLogicTest s
tc), let pruned :: TestSequence s
pruned = DynLogic s -> TestSequence s -> TestSequence s
forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> TestSequence s
pruneDLTest DynLogic s
d TestSequence s
as'
                                                     test :: DynLogicTest s
test = DynLogic s -> TestSequence s -> DynLogicTest s
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 = Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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' Annotated s
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 [TestSequence s] -> [TestSequence s] -> [TestSequence s]
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) =
      [ a -> TestSequence s -> TestSequence s
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 TestSequence s -> [TestSequence s] -> [TestSequence s]
forall a. a -> [a] -> [a]
: Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink' Annotated s
s (DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
s (TestSequence s -> DynLogic s) -> TestSequence s -> DynLogic s
forall a b. (a -> b) -> a -> b
$ a -> TestSequence s -> TestSequence s
forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a TestSequence s
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) =
      [Step s -> TestSequence s -> TestSequence s
forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep (Var a -> Var a
forall a b. Var a -> Var b
unsafeCoerceVar Var a
var Var a -> ActionWithPolarity s a -> Step s
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{} <- Annotated s
-> ActionWithPolarity s a -> [Any (ActionWithPolarity s)]
forall state a.
(Typeable a, StateModel state) =>
Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
computeShrinkAction Annotated s
s ActionWithPolarity s a
act]
        [TestSequence s] -> [TestSequence s] -> [TestSequence s]
forall a. [a] -> [a] -> [a]
++ [ Step s -> TestSequence s -> TestSequence s
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'
                (Step s -> Annotated s -> Annotated s
forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep Step s
step Annotated s
s)
                (DynLogic s -> Annotated s -> Step s -> DynLogic 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) =
      TestSequence s
forall s. TestSequence s
TestSeqStop
        TestSequence s -> [TestSequence s] -> [TestSequence s]
forall a. a -> [a] -> [a]
: [TestSequence s] -> [TestSequence s]
forall a. [a] -> [a]
reverse ((TestSequence s -> Bool) -> [TestSequence s] -> [TestSequence s]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool)
-> (TestSequence s -> Bool) -> TestSequence s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestSequence s -> Bool
forall s. TestSequence s -> Bool
nullSeq) [Int -> TestSequence s -> TestSequence s
forall s. Int -> TestSequence s -> TestSequence s
dropSeq (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TestSequence s
rest | Int
n <- (Int -> Int) -> Int -> [Int]
forall a. (a -> a) -> a -> [a]
iterate (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2) Int
1])
        [TestSequence s] -> [TestSequence s] -> [TestSequence s]
forall a. [a] -> [a] -> [a]
++ (TestSequence s -> TestSequence s)
-> [TestSequence s] -> [TestSequence s]
forall a b. (a -> b) -> [a] -> [b]
map (TestStep s
step TestStep s -> TestSequence s -> TestSequence s
forall s. TestStep s -> TestSequence s -> TestSequence s
:>) (Annotated s -> DynLogic s -> TestSequence s -> [TestSequence s]
shrink' (Step s -> Annotated s -> Annotated s
forall s. StateModel s => Step s -> Annotated s -> Annotated s
nextStateStep (TestStep s -> Step s
forall r. Witnesses r -> r
discardWitnesses TestStep s
step) Annotated s
s) (DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
s (TestStep s
step TestStep s -> TestSequence s -> TestSequence s
forall s. TestStep s -> TestSequence 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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl | Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a
a -> Quantification a -> a -> [a]
forall a. Quantification a -> a -> [a]
shrinkQ Quantification a
Quantification a
q a
a
    Maybe (a :~: a)
_ -> []
shrinkWitness (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') a
a = DynLogic s -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d' a
a
shrinkWitness (Stopping DynLogic s
d) a
a = DynLogic s -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a
shrinkWitness (Weight Double
_ DynLogic s
d) a
a = DynLogic s -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a
shrinkWitness (Monitor Property -> Property
_ DynLogic s
d) a
a = DynLogic s -> a -> [a]
forall s a. (StateModel s, Typeable a) => DynLogic s -> a -> [a]
shrinkWitness DynLogic s
d a
a
shrinkWitness 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] Annotated s
forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    prune :: [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [] Annotated s
_ TestSequence s
_ = TestSequence s
forall s. TestSequence s
TestSeqStop
    prune [DynLogic s]
_ Annotated s
_ TestSequence s
TestSeqStop = TestSequence s
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' -> a -> TestSequence s -> TestSequence s
forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a (TestSequence s -> TestSequence s)
-> TestSequence s -> TestSequence s
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)
      | Annotated s -> ActionWithPolarity s a -> Bool
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' <- DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s (Step s -> TestStep 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' -> Step s -> TestSequence s -> TestSequence s
forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step (TestSequence s -> TestSequence s)
-> TestSequence s -> TestSequence s
forall a b. (a -> b) -> a -> b
$ [DynLogic s] -> Annotated s -> TestSequence s -> TestSequence s
prune [DynLogic s]
ds' (Step s -> Annotated s -> Annotated s
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.
  | ActionWithPolarity s a -> Any (ActionWithPolarity s)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
a Any (ActionWithPolarity s) -> Any (ActionWithPolarity s) -> Bool
forall a. Eq a => a -> a -> Bool
== ActionWithPolarity s a -> Any (ActionWithPolarity s)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
act = [Var a -> DynPred s
k (Var a -> Var a
forall a b. Var a -> Var b
unsafeCoerceVar Var a
var) (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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 a
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 (ActionWithPolarity s a -> Bool
forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar ActionWithPolarity s a
act) = [DynPred s
k (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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)]
stepDL (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') Annotated s
s Witnesses (Step s)
step = DynLogic s -> Annotated s -> Witnesses (Step s) -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s Witnesses (Step s)
step [DynLogic s] -> [DynLogic s] -> [DynLogic s]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> Annotated s -> Witnesses (Step s) -> [DynLogic s]
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 = DynLogic s -> Annotated s -> Witnesses (Step s) -> [DynLogic s]
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 = DynLogic s -> Annotated s -> Witnesses (Step s) -> [DynLogic s]
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> [DynLogic s
d | Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a
a, DynLogic s
d <- DynLogic s -> Annotated s -> Witnesses (Step s) -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL (a -> DynLogic s
f a
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 = DynLogic s -> Annotated s -> Witnesses (Step s) -> [DynLogic s]
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> [a -> DynLogic s
k a
a
a | Quantification a -> a -> Bool
forall a. Quantification a -> a -> Bool
isaQ Quantification a
q a
a
a]
    Maybe (a :~: a)
Nothing -> []
stepDLW (Alt ChoiceType
_ DynLogic s
d DynLogic s
d') a
a = DynLogic s -> a -> [DynLogic s]
forall s a.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> [DynLogic s]
stepDLW DynLogic s
d a
a [DynLogic s] -> [DynLogic s] -> [DynLogic s]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> a -> [DynLogic s]
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 = DynLogic s -> a -> [DynLogic s]
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 = DynLogic s -> a -> [DynLogic s]
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 = DynLogic s -> a -> [DynLogic s]
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)) = DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq (DynLogic s -> a -> DynLogic s
forall a s.
(DynLogicModel s, Typeable a) =>
DynLogic s -> a -> DynLogic s
stepDLWitness DynLogic s
d a
a) Annotated s
s (Witnesses () -> TestSequence 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) =
  DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq ([DynLogic s] -> DynLogic s
forall s. [DynLogic s] -> DynLogic s
demonicAlt ([DynLogic s] -> DynLogic s) -> [DynLogic s] -> DynLogic s
forall a b. (a -> b) -> a -> b
$ DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDL DynLogic s
d Annotated s
s TestStep s
step) (Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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) 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 = [DynLogic s] -> DynLogic s
forall s. [DynLogic s] -> DynLogic s
demonicAlt ([DynLogic s] -> DynLogic s) -> [DynLogic s] -> DynLogic s
forall a b. (a -> b) -> a -> b
$ DynLogic s -> a -> [DynLogic s]
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 = DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLSeq DynLogic s
d Annotated s
s (Step s -> TestSequence s -> TestSequence s
forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step TestSequence s
forall s. TestSequence s
TestSeqStop)

demonicAlt :: [DynLogic s] -> DynLogic s
demonicAlt :: forall s. [DynLogic s] -> DynLogic s
demonicAlt [] = DynLogic s
forall s. DynLogic s
EmptySpec
demonicAlt [DynLogic s]
ds = (DynLogic s -> DynLogic s -> DynLogic s)
-> [DynLogic s] -> DynLogic s
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
forall s. ChoiceType -> DynLogic s -> DynLogic s -> DynLogic s
Alt ChoiceType
Demonic) [DynLogic s]
ds

propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property
propPruningGeneratedScriptIsNoop :: forall s. DynLogicModel s => DynLogic s -> Property
propPruningGeneratedScriptIsNoop DynLogic s
d =
  Gen (DynLogicTest s) -> (DynLogicTest s -> Bool) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s))
-> (Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a b. (a -> b) -> a -> b
$ \Int
n -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 Int
n) Gen Int -> (Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= DynLogic s -> Int -> Gen (DynLogicTest s)
forall s.
DynLogicModel s =>
DynLogic s -> Int -> Gen (DynLogicTest s)
generateDLTest DynLogic s
d) ((DynLogicTest s -> Bool) -> Property)
-> (DynLogicTest s -> Bool) -> Property
forall a b. (a -> b) -> a -> b
$ \DynLogicTest s
test ->
    let script :: 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 TestSequence s -> TestSequence s -> Bool
forall a. Eq a => a -> a -> Bool
== DynLogic s -> TestSequence s -> TestSequence s
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 Annotated s
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 = TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
forall s.
TestSequence s -> FailingAction s -> Annotated s -> DynLogicTest s
BadPrecondition TestSequence s
forall s. TestSequence s
TestSeqStop FailingAction s
b Annotated s
s
      | DynLogic s -> Annotated s -> Bool
forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s = TestSequence s -> Annotated s -> DynLogicTest s
forall s. TestSequence s -> Annotated s -> DynLogicTest s
Stuck TestSequence s
forall s. TestSequence s
TestSeqStop Annotated s
s
      | Bool
otherwise = TestSequence s -> DynLogicTest s
forall s. TestSequence s -> DynLogicTest s
DLScript TestSequence s
forall s. TestSequence s
TestSeqStop
    make DynLogic s
d Annotated s
s (TestSeqWitness a
a TestSequence s
ss) =
      (TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (a -> TestSequence s -> TestSequence s
forall s a.
QuantifyConstraints a =>
a -> TestSequence s -> TestSequence s
TestSeqWitness a
a) (DynLogicTest s -> DynLogicTest s)
-> DynLogicTest s -> DynLogicTest s
forall a b. (a -> b) -> a -> b
$
        DynLogic s -> Annotated s -> TestSequence s -> DynLogicTest s
make
          (DynLogic s -> a -> DynLogic s
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) =
      (TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
forall s.
(TestSequence s -> TestSequence s)
-> DynLogicTest s -> DynLogicTest s
onDLTestSeq (Step s -> TestSequence s -> TestSequence s
forall s. Step s -> TestSequence s -> TestSequence s
TestSeqStep Step s
step) (DynLogicTest s -> DynLogicTest s)
-> DynLogicTest s -> DynLogicTest s
forall a b. (a -> b) -> a -> b
$
        DynLogic s -> Annotated s -> TestSequence s -> DynLogicTest s
make
          (DynLogic s -> Annotated s -> Step s -> DynLogic s
forall s.
DynLogicModel s =>
DynLogic s -> Annotated s -> Step s -> DynLogic s
stepDLStep DynLogic s
d Annotated s
s Step s
step)
          (Step s -> Annotated s -> Annotated s
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 = DynLogic s -> TestSequence s -> DynLogicTest s
forall s.
DynLogicModel s =>
DynLogic s -> TestSequence s -> DynLogicTest s
makeTestFromPruned DynLogic s
d (TestSequence s -> DynLogicTest s)
-> TestSequence s -> DynLogicTest s
forall a b. (a -> b) -> a -> b
$ DynLogic s -> TestSequence s -> TestSequence s
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
    Double
-> Gen (Any (ActionWithPolarity s))
-> (Any (ActionWithPolarity s) -> Bool)
-> Bool
forall a. Double -> Gen a -> (a -> Bool) -> Bool
canGenerate
      Double
0.01
      (Annotated s -> Gen (Any (ActionWithPolarity s))
forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated s
s)
      ( \case
          Some ActionWithPolarity s a
act ->
            Annotated s -> ActionWithPolarity s a -> Bool
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 (ActionWithPolarity s a -> Bool
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 = DynLogic s -> Annotated s -> Bool
forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s Bool -> Bool -> Bool
&& DynLogic s -> Annotated s -> 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 = DynLogic s -> Annotated s -> Bool
forall s. DynLogicModel s => DynLogic s -> Annotated s -> Bool
stuck DynLogic s
d Annotated s
s Bool -> Bool -> Bool
|| DynLogic s -> Annotated s -> 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 = DynLogic s -> Annotated s -> Bool
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
never Bool -> Bool -> Bool
|| DynLogic s -> Annotated s -> 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 = DynLogic s -> Annotated s -> Bool
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 Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool
False
validDLTest DynLogic s
_ test :: DynLogicTest s
test@DLScript{} Property
p = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (DynLogicTest s -> String
forall a. Show a => a -> String
show DynLogicTest s
test) Property
p
validDLTest DynLogic s
_ DynLogicTest s
test Property
_ = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (DynLogicTest s -> String
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) = [Step s] -> Actions s
forall state. [Step state] -> Actions state
Actions ([Step s] -> Actions s) -> [Step s] -> Actions s
forall a b. (a -> b) -> a -> b
$ TestSequence s -> [Step s]
forall s. TestSequence s -> [Step s]
sequenceSteps TestSequence s
s
scriptFromDL DynLogicTest s
_ = [Step s] -> Actions 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 Witnesses (TestContinuation s) -> TestContinuation s
forall r. Witnesses r -> r
discardWitnesses Witnesses (TestContinuation s)
ss of
    TestContinuation s
ContStop -> []
    ContStep Step s
s TestSequence s
ss' -> Step s
s Step s -> [Step s] -> [Step s]
forall a. a -> [a] -> [a]
: TestSequence s -> [Step s]
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 a -> Maybe a
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
a of
    Just a
a' -> a -> Witnesses (FailingAction s) -> Witnesses (FailingAction s)
forall a r.
QuantifyConstraints a =>
a -> Witnesses r -> Witnesses r
Witness a
a' (Witnesses (FailingAction s) -> Witnesses (FailingAction s))
-> [Witnesses (FailingAction s)] -> [Witnesses (FailingAction s)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
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 = DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
forall s a.
StateModel s =>
DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActionsGiven DynLogic s
d Annotated s
s Witnesses a
w [Witnesses (FailingAction s)]
-> [Witnesses (FailingAction s)] -> [Witnesses (FailingAction s)]
forall a. [a] -> [a] -> [a]
++ DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
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 = DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
never then [] else DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
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 = DynLogic s
-> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
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
_) = FailingAction s -> Witnesses (FailingAction s)
forall r. r -> Witnesses r
Do (FailingAction s -> Witnesses (FailingAction s))
-> [FailingAction s] -> [Witnesses (FailingAction s)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DynLogic s -> Annotated s -> [FailingAction s]
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
  | Annotated s -> ActionWithPolarity s a -> Bool
forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated s
s ActionWithPolarity s a
a = []
  | Bool
otherwise = [ActionWithPolarity s a -> FailingAction s
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 = [String -> FailingAction 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 = DynLogic s -> Annotated s -> [FailingAction s]
forall s.
StateModel s =>
DynLogic s -> Annotated s -> [FailingAction s]
badActions DynLogic s
d Annotated s
s [FailingAction s] -> [FailingAction s] -> [FailingAction s]
forall a. [a] -> [a] -> [a]
++ DynLogic s -> Annotated s -> [FailingAction s]
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 = DynLogic s -> Annotated s -> [FailingAction 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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
never then [] else DynLogic s -> Annotated s -> [FailingAction s]
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 = DynLogic s -> Annotated s -> [FailingAction 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 DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d Annotated s
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 = (Property -> Property) -> Maybe (Property -> Property)
forall a. a -> Maybe a
Just Property -> Property
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`)
  | ActionWithPolarity s a -> Any (ActionWithPolarity s)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
a Any (ActionWithPolarity s) -> Any (ActionWithPolarity s) -> Bool
forall a. Eq a => a -> a -> Bool
== ActionWithPolarity s a -> Any (ActionWithPolarity s)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity s a
a' = DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring (Var a -> DynPred s
k (Var a -> Var a
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' = Annotated s -> ActionWithPolarity s a -> Var a -> Annotated 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' (Var a -> Var 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 (ActionWithPolarity s a -> Bool
forall s a. DynLogicModel s => ActionWithPolarity s a -> Bool
restrictedPolar ActionWithPolarity s a
a) = DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring (ActionWithPolarity s a -> (Var a -> DynPred s) -> DynLogic s
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 ((Var a -> DynPred s) -> DynLogic s)
-> (Var a -> DynPred s) -> DynLogic s
forall a b. (a -> b) -> a -> b
$ DynPred s -> Var a -> DynPred s
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.
  DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring DynLogic s
d Annotated s
s TestSequence s
as Maybe (Property -> Property)
-> Maybe (Property -> Property) -> Maybe (Property -> Property)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
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 = DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
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 = DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
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)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @a' of
    Just a :~: a
Refl -> DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
forall s.
DynLogicModel s =>
DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
findMonitoring (a -> DynLogic s
k a
a
a) Annotated s
s (Witnesses (TestContinuation s) -> TestSequence s
forall s. Witnesses (TestContinuation s) -> TestSequence s
TestSeq Witnesses (TestContinuation s)
as)
    Maybe (a :~: a)
Nothing -> Maybe (Property -> Property)
forall a. Maybe a
Nothing
findMonitoring (Monitor Property -> Property
m DynLogic s
d) Annotated s
s TestSequence s
as =
  (Property -> Property
m (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Property -> Property) -> Property -> Property)
-> Maybe (Property -> Property) -> Maybe (Property -> Property)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DynLogic s
-> Annotated s -> TestSequence s -> Maybe (Property -> Property)
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
_ = Maybe (Property -> Property)
forall a. Maybe a
Nothing