module Test.QuickCheck.DynamicLogic.Internal where

import Control.Applicative
import Control.Arrow (second)
import Control.Monad
import Data.Typeable
import Test.QuickCheck (Gen, Property, Testable)
import Test.QuickCheck qualified as QC
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
QC.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
QC.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
QC.forAllShrinkBlind
          (Int -> rep -> Smart rep
forall a. Int -> a -> Smart a
QC.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
QC.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
$ \(QC.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
QC.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
QC.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
QC.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
QC.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
QC.forAll ((Int -> Gen (DynLogicTest s)) -> Gen (DynLogicTest s)
forall a. (Int -> Gen a) -> Gen a
QC.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
QC.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
QC.==> Bool
False
validDLTest DynLogic s
_ test :: DynLogicTest s
test@DLScript{} Property
p = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.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
QC.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