{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Test.QuickCheck.StateModel (
module Test.QuickCheck.StateModel.Variables,
StateModel (..),
RunModel (..),
WithUsedVars (..),
Annotated (..),
Step (..),
LookUp,
Actions (..),
pattern Actions,
EnvEntry (..),
pattern (:=?),
Env,
Realized,
Generic,
stateAfter,
runActions,
lookUpVar,
lookUpVarMaybe,
initialAnnotatedState,
computeNextState,
computePrecondition,
computeArbitraryAction,
computeShrinkAction,
) where
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer (WriterT)
import Data.Data
import Data.Kind
import Data.List
import Data.Set qualified as Set
import GHC.Generics
import Test.QuickCheck as QC
import Test.QuickCheck.DynamicLogic.SmartShrinking
import Test.QuickCheck.Monadic
import Test.QuickCheck.StateModel.Variables
class
( forall a. Show (Action state a)
, forall a. HasVariables (Action state a)
, Show state
, HasVariables state
) =>
StateModel state
where
data Action state a
actionName :: Action state a -> String
actionName = forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
arbitraryAction :: VarContext -> state -> Gen (Any (Action state))
shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]
shrinkAction VarContext
_ state
_ Action state a
_ = []
initialState :: state
nextState :: Typeable a => state -> Action state a -> Var a -> state
nextState state
s Action state a
_ Var a
_ = state
s
precondition :: state -> Action state a -> Bool
precondition state
_ Action state a
_ = Bool
True
deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
type family Realized (m :: Type -> Type) a :: Type
type instance Realized IO a = a
type instance Realized (StateT s m) a = Realized m a
type instance Realized (ReaderT r m) a = Realized m a
type instance Realized (WriterT w m) a = Realized m a
type instance Realized Identity a = a
class Monad m => RunModel state m where
perform :: forall a. Typeable a => state -> Action state a -> LookUp m -> m (Realized m a)
postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> m Bool
postcondition (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
monitoring (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ Property
prop = Property
prop
type LookUp m = forall a. Typeable a => Var a -> Realized m a
type Env m = [EnvEntry m]
data EnvEntry m where
(:==) :: Typeable a => Var a -> Realized m a -> EnvEntry m
infix 5 :==
pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m
pattern v $m:=? :: forall {r} {a} {m :: * -> *}.
Typeable a =>
EnvEntry m -> (Var a -> Realized m a -> r) -> ((# #) -> r) -> r
:=? val <- (viewAtType -> Just (v, val))
viewAtType :: forall a m. Typeable a => EnvEntry m -> Maybe (Var a, Realized m a)
viewAtType :: forall a (m :: * -> *).
Typeable a =>
EnvEntry m -> Maybe (Var a, Realized m a)
viewAtType ((Var a
v :: Var b) :== Realized m a
val)
| Just a :~: a
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b = forall a. a -> Maybe a
Just (Var a
v, Realized m a
val)
| Bool
otherwise = forall a. Maybe a
Nothing
lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe :: forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe [] Var a
_ = forall a. Maybe a
Nothing
lookUpVarMaybe (((Var a
v' :: Var b) :== Realized m a
a) : [EnvEntry m]
env) Var a
v =
case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b of
Just a :~: a
Refl | Var a
v forall a. Eq a => a -> a -> Bool
== Var a
v' -> forall a. a -> Maybe a
Just Realized m a
a
Maybe (a :~: a)
_ -> forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe [EnvEntry m]
env Var a
v
lookUpVar :: Typeable a => Env m -> Var a -> Realized m a
lookUpVar :: forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env Var a
v = case forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe Env m
env Var a
v of
Maybe (Realized m a)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var a
v forall a. [a] -> [a] -> [a]
++ String
" is not bound!"
Just Realized m a
a -> Realized m a
a
data WithUsedVars a = WithUsedVars VarContext a
data Step state where
(:=) ::
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a ->
Action state a ->
Step state
infix 5 :=
instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where
getAllVariables :: Step state -> Set (Any Var)
getAllVariables (Var a
var := Action state a
act) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Var a
var) forall a b. (a -> b) -> a -> b
$ forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Action state a
act
instance Show (Step state) where
show :: Step state -> String
show (Var a
var := Action state a
act) = forall a. Show a => a -> String
show Var a
var forall a. [a] -> [a] -> [a]
++ String
" <- action $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action state a
act
instance Show (WithUsedVars (Step state)) where
show :: WithUsedVars (Step state) -> String
show (WithUsedVars VarContext
ctx (Var a
var := Action state a
act)) =
if forall a. Typeable a => Var a -> VarContext -> Bool
isWellTyped Var a
var VarContext
ctx
then forall a. Show a => a -> String
show Var a
var forall a. [a] -> [a] -> [a]
++ String
" <- action $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action state a
act
else String
"action $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action state a
act
instance Eq (Step state) where
(Var a
v := Action state a
act) == :: Step state -> Step state -> Bool
== (Var a
v' := Action state a
act') =
forall a b. Var a -> Var b
unsafeCoerceVar Var a
v forall a. Eq a => a -> a -> Bool
== Var a
v' Bool -> Bool -> Bool
&& forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action state a
act forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action state a
act'
data Actions state = Actions_ [String] (Smart [Step state])
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x. Rep (Actions state) x -> Actions state
forall state x. Actions state -> Rep (Actions state) x
$cto :: forall state x. Rep (Actions state) x -> Actions state
$cfrom :: forall state x. Actions state -> Rep (Actions state) x
Generic)
pattern Actions :: [Step state] -> Actions state
pattern $bActions :: forall state. [Step state] -> Actions state
$mActions :: forall {r} {state}.
Actions state -> ([Step state] -> r) -> ((# #) -> r) -> r
Actions as <-
Actions_ _ (Smart _ as)
where
Actions [Step state]
as = forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [] (forall a. Int -> a -> Smart a
Smart Int
0 [Step state]
as)
{-# COMPLETE Actions #-}
instance Semigroup (Actions state) where
Actions_ [String]
rs (Smart Int
k [Step state]
as) <> :: Actions state -> Actions state -> Actions state
<> Actions_ [String]
rs' (Smart Int
_ [Step state]
as') = forall state. [String] -> Smart [Step state] -> Actions state
Actions_ ([String]
rs forall a. [a] -> [a] -> [a]
++ [String]
rs') (forall a. Int -> a -> Smart a
Smart Int
k ([Step state]
as forall a. Semigroup a => a -> a -> a
<> [Step state]
as'))
instance Eq (Actions state) where
Actions [Step state]
as == :: Actions state -> Actions state -> Bool
== Actions [Step state]
as' = [Step state]
as forall a. Eq a => a -> a -> Bool
== [Step state]
as'
instance StateModel state => Show (Actions state) where
show :: Actions state -> String
show (Actions [Step state]
as) =
let as' :: [WithUsedVars (Step state)]
as' = forall a. VarContext -> a -> WithUsedVars a
WithUsedVars (forall state. StateModel state => Actions state -> VarContext
usedVariables (forall state. [Step state] -> Actions state
Actions [Step state]
as)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Step state]
as
in forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. [a] -> [a] -> [a]
(++) (String
"do " forall a. a -> [a] -> [a]
: forall a. a -> [a]
repeat String
" ") (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [WithUsedVars (Step state)]
as' forall a. [a] -> [a] -> [a]
++ [String
"pure ()"])
usedVariables :: forall state. StateModel state => Actions state -> VarContext
usedVariables :: forall state. StateModel state => Actions state -> VarContext
usedVariables (Actions [Step state]
as) = Annotated state -> [Step state] -> VarContext
go forall state. StateModel state => Annotated state
initialAnnotatedState [Step state]
as
where
go :: Annotated state -> [Step state] -> VarContext
go :: Annotated state -> [Step state] -> VarContext
go Annotated state
aState [] = forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated state
aState)
go Annotated state
aState ((Var a
var := Action state a
act) : [Step state]
steps) =
forall a. HasVariables a => a -> VarContext
allVariables Action state a
act
forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated state
aState)
forall a. Semigroup a => a -> a -> a
<> Annotated state -> [Step state] -> VarContext
go (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
aState Action state a
act Var a
var) [Step state]
steps
instance StateModel state => Arbitrary (Actions state) where
arbitrary :: Gen (Actions state)
arbitrary = do
([Step state]
as, [String]
rejected) <- Annotated state -> Int -> Gen ([Step state], [String])
arbActions forall state. StateModel state => Annotated state
initialAnnotatedState Int
1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [String]
rejected (forall a. Int -> a -> Smart a
Smart Int
0 [Step state]
as)
where
arbActions :: Annotated state -> Int -> Gen ([Step state], [String])
arbActions :: Annotated state -> Int -> Gen ([Step state], [String])
arbActions Annotated state
s Int
step = forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ \Int
n ->
let w :: Int
w = Int
n forall a. Integral a => a -> a -> a
`div` Int
2 forall a. Num a => a -> a -> a
+ Int
1
in forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (m :: * -> *) a. Monad m => a -> m a
return ([], []))
,
( Int
w
, do
(Maybe (Any (Action state))
mact, [String]
rej) <- Gen (Maybe (Any (Action state)), [String])
satisfyPrecondition
case Maybe (Any (Action state))
mact of
Just (Some Action state a
act) -> do
let var :: Var a
var = forall a. Int -> Var a
mkVar Int
step
([Step state]
as, [String]
rejected) <- Annotated state -> Int -> Gen ([Step state], [String])
arbActions (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) (Int
step forall a. Num a => a -> a -> a
+ Int
1)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action state a
act) forall a. a -> [a] -> [a]
: [Step state]
as, [String]
rej forall a. [a] -> [a] -> [a]
++ [String]
rejected)
Maybe (Any (Action state))
Nothing ->
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
)
]
where
satisfyPrecondition :: Gen (Maybe (Any (Action state)), [String])
satisfyPrecondition = forall a. (Int -> Gen a) -> Gen a
sized forall a b. (a -> b) -> a -> b
$ \Int
n -> Int
-> Int -> [String] -> Gen (Maybe (Any (Action state)), [String])
go Int
n (Int
2 forall a. Num a => a -> a -> a
* Int
n) []
go :: Int
-> Int -> [String] -> Gen (Maybe (Any (Action state)), [String])
go Int
m Int
n [String]
rej
| Int
m forall a. Ord a => a -> a -> Bool
> Int
n = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [String]
rej)
| Bool
otherwise = do
Any (Action state)
a <- forall a. Int -> Gen a -> Gen a
resize Int
m forall a b. (a -> b) -> a -> b
$ forall state.
StateModel state =>
Annotated state -> Gen (Any (Action state))
computeArbitraryAction Annotated state
s
case Any (Action state)
a of
Some Action state a
act ->
if forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
act
then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action state a
act), [String]
rej)
else Int
-> Int -> [String] -> Gen (Maybe (Any (Action state)), [String])
go (Int
m forall a. Num a => a -> a -> a
+ Int
1) Int
n (forall state a. StateModel state => Action state a -> String
actionName Action state a
act forall a. a -> [a] -> [a]
: [String]
rej)
shrink :: Actions state -> [Actions state]
shrink (Actions_ [String]
rs Smart [Step state]
as) =
forall a b. (a -> b) -> [a] -> [b]
map (forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [String]
rs) (forall a. (a -> [a]) -> Smart a -> [Smart a]
shrinkSmart (forall a b. (a -> b) -> [a] -> [b]
map (forall state. StateModel state => [Step state] -> [Step state]
prune forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList forall {state}.
StateModel state =>
(Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates) Smart [Step state]
as)
where
shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker (Var a
v := Action state a
act, Annotated state
s) = [(forall a b. Var a -> Var b
unsafeCoerceVar Var a
v forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action state a
act', Annotated state
s) | Some Action state a
act' <- forall a state.
(Typeable a, StateModel state) =>
Annotated state -> Action state a -> [Any (Action state)]
computeShrinkAction Annotated state
s Action state a
act]
data Annotated state = Metadata
{ forall state. Annotated state -> VarContext
vars :: VarContext
, forall state. Annotated state -> state
underlyingState :: state
}
instance Show state => Show (Annotated state) where
show :: Annotated state -> String
show (Metadata VarContext
ctx state
s) = forall a. Show a => a -> String
show VarContext
ctx forall a. [a] -> [a] -> [a]
++ String
" |- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show state
s
initialAnnotatedState :: StateModel state => Annotated state
initialAnnotatedState :: forall state. StateModel state => Annotated state
initialAnnotatedState = forall state. VarContext -> state -> Annotated state
Metadata forall a. Monoid a => a
mempty forall state. StateModel state => state
initialState
computePrecondition :: StateModel state => Annotated state -> Action state a -> Bool
computePrecondition :: forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
a =
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Some Var a
v) -> Var a
v forall a. Typeable a => Var a -> VarContext -> Bool
`isWellTyped` forall state. Annotated state -> VarContext
vars Annotated state
s) (forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Action state a
a)
Bool -> Bool -> Bool
&& forall state a. StateModel state => state -> Action state a -> Bool
precondition (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a
computeNextState ::
(StateModel state, Typeable a) =>
Annotated state ->
Action state a ->
Var a ->
Annotated state
computeNextState :: forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
a Var a
v = forall state. VarContext -> state -> Annotated state
Metadata (forall a. Typeable a => VarContext -> Var a -> VarContext
extendContext (forall state. Annotated state -> VarContext
vars Annotated state
s) Var a
v) (forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> Var a -> state
nextState (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a Var a
v)
computeArbitraryAction ::
StateModel state =>
Annotated state ->
Gen (Any (Action state))
computeArbitraryAction :: forall state.
StateModel state =>
Annotated state -> Gen (Any (Action state))
computeArbitraryAction Annotated state
s = forall state.
StateModel state =>
VarContext -> state -> Gen (Any (Action state))
arbitraryAction (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state. Annotated state -> state
underlyingState Annotated state
s)
computeShrinkAction ::
(Typeable a, StateModel state) =>
Annotated state ->
Action state a ->
[Any (Action state)]
computeShrinkAction :: forall a state.
(Typeable a, StateModel state) =>
Annotated state -> Action state a -> [Any (Action state)]
computeShrinkAction Annotated state
s = forall state a.
(StateModel state, Typeable a) =>
VarContext -> state -> Action state a -> [Any (Action state)]
shrinkAction (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state. Annotated state -> state
underlyingState Annotated state
s)
prune :: StateModel state => [Step state] -> [Step state]
prune :: forall state. StateModel state => [Step state] -> [Step state]
prune = forall {state}.
StateModel state =>
Annotated state -> [Step state] -> [Step state]
loop forall state. StateModel state => Annotated state
initialAnnotatedState
where
loop :: Annotated state -> [Step state] -> [Step state]
loop Annotated state
_s [] = []
loop Annotated state
s ((Var a
var := Action state a
act) : [Step state]
as)
| forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
act =
(Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action state a
act) forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [Step state]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) [Step state]
as
| Bool
otherwise =
Annotated state -> [Step state] -> [Step state]
loop Annotated state
s [Step state]
as
withStates :: StateModel state => [Step state] -> [(Step state, Annotated state)]
withStates :: forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates = forall {state}.
StateModel state =>
Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop forall state. StateModel state => Annotated state
initialAnnotatedState
where
loop :: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop Annotated state
_s [] = []
loop Annotated state
s ((Var a
var := Action state a
act) : [Step state]
as) =
(Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action state a
act, Annotated state
s) forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) [Step state]
as
stateAfter :: StateModel state => Actions state -> Annotated state
stateAfter :: forall state. StateModel state => Actions state -> Annotated state
stateAfter (Actions [Step state]
actions) = forall {state}.
StateModel state =>
Annotated state -> [Step state] -> Annotated state
loop forall state. StateModel state => Annotated state
initialAnnotatedState [Step state]
actions
where
loop :: Annotated state -> [Step state] -> Annotated state
loop Annotated state
s [] = Annotated state
s
loop Annotated state
s ((Var a
var := Action state a
act) : [Step state]
as) = Annotated state -> [Step state] -> Annotated state
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) [Step state]
as
runActions ::
forall state m.
(StateModel state, RunModel state m) =>
Actions state ->
PropertyM m (Annotated state, Env m)
runActions :: forall state (m :: * -> *).
(StateModel state, RunModel state m) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions (Actions_ [String]
rejected (Smart Int
_ [Step state]
actions)) = Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop forall state. StateModel state => Annotated state
initialAnnotatedState [] [Step state]
actions
where
loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop :: Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop Annotated state
_s Env m
env [] = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
rejected) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions rejected by precondition" [String]
rejected)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annotated state
_s, forall a. [a] -> [a]
reverse Env m
env)
loop Annotated state
s Env m
env ((Var a
v := Action state a
act) : [Step state]
as) = do
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
pre forall a b. (a -> b) -> a -> b
$ forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
act
Realized m a
ret <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (forall state (m :: * -> *) a.
(RunModel state m, Typeable a) =>
state -> Action state a -> LookUp m -> m (Realized m a)
perform (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
act (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env))
let name :: String
name = forall state a. StateModel state => Action state a -> String
actionName Action state a
act
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions" [String
name])
let var :: Var a
var = forall a b. Var a -> Var b
unsafeCoerceVar Var a
v
s' :: Annotated state
s' = forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var
env' :: Env m
env' = (Var a
var forall a (m :: * -> *).
Typeable a =>
Var a -> Realized m a -> EnvEntry m
:== Realized m a
ret) forall a. a -> [a] -> [a]
: Env m
env
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp m
-> Realized m a
-> Property
-> Property
monitoring @state @m (forall state. Annotated state -> state
underlyingState Annotated state
s, forall state. Annotated state -> state
underlyingState Annotated state
s') Action state a
act (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env') Realized m a
ret)
Bool
b <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a -> LookUp m -> Realized m a -> m Bool
postcondition @state @m (forall state. Annotated state -> state
underlyingState Annotated state
s, forall state. Annotated state -> state
underlyingState Annotated state
s') Action state a
act (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env) Realized m a
ret
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
b
Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop Annotated state
s' Env m
env' [Step state]
as