Documentation + todo

Author: MaximilianAlgehed

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs

@@ -133,13 +133,16 @@ forAllNonVariableQ q = DL $ \s k -> DL.forAllQ (hasNoVariablesQ q) $ \(HasNoVari
 runDL :: Annotated s -> DL s () -> DL.DynFormula s
 runDL s dl = (unDL dl s $ \_ _ -> DL.passTest)
 
+-- TODO: We probably want versions of these three functions that take an `s` so that you can write DL
+-- properties that are only true in a specific starting state rather than a random starting state.
+
 forAllUniqueDL
   :: (DL.DynLogicModel s, Testable a)
-  => Annotated s
-  -> DL s ()
+  => DL s ()
   -> (Actions s -> a)
   -> Property
-forAllUniqueDL initState d = DL.forAllUniqueScripts initState (runDL initState d)
+forAllUniqueDL d p =
+  forAllBlind initialState $ \st -> DL.forAllUniqueScripts st (runDL (Metadata mempty st) d) p
 
 forAllDL
   :: (DL.DynLogicModel s, Testable a)

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs

@@ -355,6 +355,7 @@ restrictedPolar (ActionWithPolarity a _) = restricted a
 forAllScripts
   :: (DynLogicModel s, Testable a)
   => s
+  -- ^ The initial state
   -> DynFormula s
   -> (Actions s -> a)
   -> Property
@@ -363,15 +364,15 @@ forAllScripts s = forAllMappedScripts s id id
 -- | `Property` function suitable for formulae without choice.
 forAllUniqueScripts
   :: (DynLogicModel s, Testable a)
-  => Annotated s
+  => s
+  -- ^ The initial state
   -> DynFormula s
   -> (Actions s -> a)
   -> Property
 forAllUniqueScripts s f k =
   QC.withSize $ \sz ->
     let d = unDynFormula f sz
-        n = unsafeNextVarIndex $ vars s
-     in case generate chooseUniqueNextStep d n s 500 of
+     in case generate chooseUniqueNextStep d 1 (Metadata mempty s) 500 of
           Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False
           Just test -> validDLTest test . applyMonitoring d test . property $ k (scriptFromDL test)
 
@@ -472,7 +473,8 @@ generate chooseNextStepFun d n s size =
           useStep NoStep alt = alt
       foldr
         (\step k -> do try <- chooseNextStepFun s n step; useStep try k)
-        (return $ Stuck s TestSeqStop s)
+        (return $ Stuck s TestSeqStop s) -- NOTE: we will cons on this `TestSeqStop` so the `s` will not be the same before
+        -- and after state when we get out of this function.
         [preferred, noAny preferred, d, noAny d]
 
 sizeLimit :: Int -> Int