packages feed

quickcheck-dynamic (empty) → 1.0.0

raw patch · 11 files changed

+1608/−0 lines, 11 filesdep +QuickCheckdep +basedep +random

Dependencies added: QuickCheck, base, random

Files

+ LICENSE view
@@ -0,0 +1,53 @@+Apache License++Version 2.0, January 2004++http://www.apache.org/licenses/++TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION++1. Definitions.++"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document.++"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License.++"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity.++"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License.++"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files.++"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types.++"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below).++"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof.++"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution."++"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work.++2. Grant of Copyright License. Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form.++3. Grant of Patent License. Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed.++4. Redistribution. You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions:++You must give any other recipients of the Work or Derivative Works a copy of this License; and+You must cause any modified files to carry prominent notices stating that You changed the files; and+You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and+If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License. ++You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License.+5. Submission of Contributions. Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions.++6. Trademarks. This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file.++7. Disclaimer of Warranty. Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License.++8. Limitation of Liability. In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages.++9. Accepting Warranty or Additional Liability. While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability.++END OF TERMS AND CONDITIONS
+ NOTICE view
@@ -0,0 +1,14 @@+Copyright 2019 Input Output (Hong Kong) Ltd.++   Licensed under the Apache License, Version 2.0 (the "License");+   you may not use this file except in compliance with the License.+   You may obtain a copy of the License at++       http://www.apache.org/licenses/LICENSE-2.0++   Unless required by applicable law or agreed to in writing, software+   distributed under the License is distributed on an "AS IS" BASIS,+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+   See the License for the specific language governing permissions and+   limitations under the License.+
+ README.md view
@@ -0,0 +1,27 @@+# quickcheck-dynamic++A library for testing stateful programs using [QuickCheck](https://hackage.haskell.org/package/QuickCheck) and [dynamic logic](https://en.wikipedia.org/wiki/Dynamic_logic_(modal_logic)).++## Background++This library was initially designed by [QuviQ](http://www.quviq.com/) in collaboration with+[IOG](https://iohk.io/) to provide a dedicated test framework for [Plutus](https://docs.cardano.org/plutus/learn-about-plutus) "Smart+contracts". As the need of a _Model-Based Testing_ framework arises in+quite a lot of contexts, it was deemed useful to extract the most+generic part as a standalone package with no strings attached to+Plutus or Cardano.++## Usage++* Documentation is currenly mostly provided inline as Haddock+  comments. Checkout [StateModel](src/Test/QuickCheck/StateModel.hs)+  and [DynamicLogic](src/Test/QuickCheck/DynamicLogic.hs) modules for+  some usage instructions.+* For a concrete standalone example, have a look at [Registry](../quickcheck-io-sim-compat/test/Spec/DynamicLogic/Registry.hs), a multithreaded Thread registry.+* For more documentation on how to quickcheck-dynamic is used to test+  Plutus DApps, check this+  [tutorial](https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html).+* Apart from Plutus, this library is now in use in the+  [Hydra](https://github.com/input-output-hk/hydra-poc) project to+  verify the _Head Protocol_ implementation with respect to the+  original research paper.
+ quickcheck-dynamic.cabal view
@@ -0,0 +1,63 @@+cabal-version:   2.2+name:            quickcheck-dynamic+version:         1.0.0+license:         Apache-2.0+license-files:+  LICENSE+  NOTICE+  +maintainer:      arnaud.bailly@iohk.io+author:          Ulf Norell+category:        Testing+synopsis:+  A library for stateful property-based testing   +homepage:+  https://github.com/input-output-hk/quickcheck-dynamic#readme++bug-reports:+  https://github.com/input-output-hk/quickcheck-dynamic/issues++description:+  Please see the README on GitHub at <https://github.com/input-output-hk/quickcheck-dynamic#readme>++build-type:      Simple+extra-doc-files: README.md++source-repository head+  type:     git+  location: https://github.com/input-output-hk/quickcheck-dynamic++common lang+  default-language:   Haskell2010+  default-extensions:+    DeriveFoldable+    DeriveFunctor+    DeriveGeneric+    DeriveLift+    DeriveTraversable+    ExplicitForAll+    GeneralizedNewtypeDeriving+    ImportQualifiedPost+    ScopedTypeVariables+    StandaloneDeriving++  ghc-options:+    -Wall -Wnoncanonical-monad-instances -Wunused-packages+    -Wincomplete-uni-patterns -Wincomplete-record-updates+    -Wredundant-constraints -Widentities++library+    import: lang+    hs-source-dirs: src+    exposed-modules:+        Test.QuickCheck.DynamicLogic+        Test.QuickCheck.DynamicLogic.CanGenerate+        Test.QuickCheck.DynamicLogic.Core+        Test.QuickCheck.DynamicLogic.Quantify+        Test.QuickCheck.DynamicLogic.SmartShrinking+        Test.QuickCheck.DynamicLogic.Utils+        Test.QuickCheck.StateModel+    build-depends:+        QuickCheck -any,+        base >=4.7 && <5,+        random -any
+ src/Test/QuickCheck/DynamicLogic.hs view
@@ -0,0 +1,170 @@+{-# LANGUAGE FlexibleContexts #-}++-- | Monadic interface for writing /Dynamic Logic/ properties.+--+-- This interface offers a much nicer experience than manipulating the+-- expressions it is implemented on top of, especially as it improves+-- readability. It's still possible to express properties as pure+-- expressions using the `Test.QuickCheck.DynamicLogic.Core` module+-- and it might make sense depending on the context and the kind of+-- properties one wants to express.+module Test.QuickCheck.DynamicLogic (+  DL,+  action,+  anyAction,+  anyActions,+  anyActions_,+  stopping,+  weight,+  getSize,+  getModelStateDL,+  assert,+  assertModel,+  monitorDL,+  forAllQ,+  forAllDL,+  forAllDL_,+  forAllMappedDL,+  forAllMappedDL_,+  forAllUniqueDL,+  withDLTest,+  DL.DynLogic,+  DL.DynLogicModel (..),+  DL.DynLogicTest (..),+  DL.TestStep (..),+  module Test.QuickCheck.DynamicLogic.Quantify,+) where++import Control.Applicative+import Control.Monad+import Data.Typeable+import Test.QuickCheck hiding (getSize)+import Test.QuickCheck.DynamicLogic.Core qualified as DL+import Test.QuickCheck.DynamicLogic.Quantify+import Test.QuickCheck.StateModel++-- | The `DL` monad provides a nicer interface to dynamic logic formulae than the plain API.+--   It's a continuation monad producing a `DL.DynFormula` formula, with a state component threaded+--   through.+newtype DL s a = DL {unDL :: s -> (a -> s -> DL.DynFormula s) -> DL.DynFormula s}+  deriving (Functor)++instance Applicative (DL s) where+  pure x = DL $ \s k -> k x s+  (<*>) = ap++instance Alternative (DL s) where+  empty = DL $ \_ _ -> DL.ignore+  DL h <|> DL j = DL $ \s k -> h s k DL.||| j s k++instance Monad (DL s) where+  return = pure+  DL h >>= j = DL $ \s k -> h s $ \x s1 -> unDL (j x) s1 k++instance MonadFail (DL s) where+  fail = errorDL++action :: (Show a, Typeable a, Eq (Action s a)) => Action s a -> DL s ()+action cmd = DL $ \_ k -> DL.after cmd $ k ()++anyAction :: DL s ()+anyAction = DL $ \_ k -> DL.afterAny $ k ()++anyActions :: Int -> DL s ()+anyActions n =+  stopping+    <|> pure ()+    <|> (weight (fromIntegral n) >> anyAction >> anyActions n)++-- average number of actions same as average length of a list+anyActions_ :: DL s ()+anyActions_ = do+  n <- getSize+  anyActions (n `div` 2 + 1)++stopping :: DL s ()+stopping = DL $ \s k -> DL.toStop (k () s)++weight :: Double -> DL s ()+weight w = DL $ \s k -> DL.weight w (k () s)++getSize :: DL s Int+getSize = DL $ \s k -> DL.withSize $ \n -> k n s++getModelStateDL :: DL s s+getModelStateDL = DL $ \s k -> k s s++errorDL :: String -> DL s a+errorDL name = DL $ \_ _ -> DL.errorDL name++-- | Fail if the boolean is @False@.+--+--   Equivalent to+--+-- @+-- assert msg b = unless b (fail msg)+-- @+assert :: String -> Bool -> DL s ()+assert name b = if b then return () else errorDL name++assertModel :: String -> (s -> Bool) -> DL s ()+assertModel name p = assert name . p =<< getModelStateDL++monitorDL :: (Property -> Property) -> DL s ()+monitorDL f = DL $ \s k -> DL.monitorDL f (k () s)++-- | Generate a random value using the given `Quantification` (or list/tuple of quantifications).+--   Generated values will only shrink to smaller values that could also have been generated.+forAllQ :: Quantifiable q => q -> DL s (Quantifies q)+forAllQ q = DL $ \s k -> DL.forAllQ q $ \x -> k x s++runDL :: s -> DL s () -> DL.DynFormula s+runDL s dl = unDL dl s $ \_ _ -> DL.passTest++forAllUniqueDL ::+  (DL.DynLogicModel s, Testable a) =>+  Int ->+  s ->+  DL s () ->+  (Actions s -> a) ->+  Property+forAllUniqueDL nextVar initState d = DL.forAllUniqueScripts nextVar initState (runDL initState d)++forAllDL ::+  (DL.DynLogicModel s, Testable a) =>+  DL s () ->+  (Actions s -> a) ->+  Property+forAllDL d = DL.forAllScripts (runDL initialState d)++forAllDL_ ::+  (DL.DynLogicModel s, Testable a) =>+  DL s () ->+  (Actions s -> a) ->+  Property+forAllDL_ d = DL.forAllScripts_ (runDL initialState d)++forAllMappedDL ::+  (DL.DynLogicModel s, Testable a, Show rep) =>+  (rep -> DL.DynLogicTest s) ->+  (DL.DynLogicTest s -> rep) ->+  (Actions s -> srep) ->+  DL s () ->+  (srep -> a) ->+  Property+forAllMappedDL to from fromScript d prop =+  DL.forAllMappedScripts to from (runDL initialState d) (prop . fromScript)++forAllMappedDL_ ::+  (DL.DynLogicModel s, Testable a, Show rep) =>+  (rep -> DL.DynLogicTest s) ->+  (DL.DynLogicTest s -> rep) ->+  (Actions s -> srep) ->+  DL s () ->+  (srep -> a) ->+  Property+forAllMappedDL_ to from fromScript d prop =+  DL.forAllMappedScripts_ to from (runDL initialState d) (prop . fromScript)++withDLTest :: (DL.DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> DL.DynLogicTest s -> Property+withDLTest d = DL.withDLScriptPrefix (runDL initialState d)
+ src/Test/QuickCheck/DynamicLogic/CanGenerate.hs view
@@ -0,0 +1,21 @@+module Test.QuickCheck.DynamicLogic.CanGenerate (canGenerate) where++import System.IO.Unsafe+import Test.QuickCheck++-- | @canGenerate prob g p@+--   returns @False@ if we are sure @Prob(g generates x satisfying p) >= prob@+--   otherwise @True@ (and we know such an x can be generated).+canGenerate :: Double -> Gen a -> (a -> Bool) -> Bool+canGenerate prob g p = unsafePerformIO $ tryToGenerate 1+ where+  tryToGenerate luck+    | luck < eps = return False+    | otherwise = do+        x <- generate g+        if p x+          then return True+          else tryToGenerate (luck * (1 - prob))++  -- Our confidence level is 1-eps+  eps = 1.0e-9
+ src/Test/QuickCheck/DynamicLogic/Core.hs view
@@ -0,0 +1,675 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Test.QuickCheck.DynamicLogic.Core (+  module Test.QuickCheck.DynamicLogic.Quantify,+  DynLogic,+  DynPred,+  DynFormula,+  DynLogicModel (..),+  DynLogicTest (..),+  TestStep (..),+  ignore,+  passTest,+  afterAny,+  after,+  (|||),+  forAllQ,+  weight,+  withSize,+  toStop,+  done,+  errorDL,+  monitorDL,+  always,+  forAllScripts,+  forAllScripts_,+  withDLScript,+  withDLScriptPrefix,+  forAllMappedScripts,+  forAllMappedScripts_,+  forAllUniqueScripts,+  propPruningGeneratedScriptIsNoop,+) where++import Control.Applicative+import Data.List+import Data.Typeable+import Test.QuickCheck hiding (generate)+import Test.QuickCheck.DynamicLogic.CanGenerate+import Test.QuickCheck.DynamicLogic.Quantify+import Test.QuickCheck.DynamicLogic.SmartShrinking+import Test.QuickCheck.DynamicLogic.Utils qualified as QC+import Test.QuickCheck.StateModel++-- | A `DynFormula` may depend on the QuickCheck size parameter+newtype DynFormula s = DynFormula {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+    After (Any (Action s)) (DynPred s)+  | -- | Adjust the probability of picking a branch+    Weight Double (DynLogic s)+  | -- | Generating a random value+    forall a.+    (Eq a, Show a, Typeable 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 (Eq, Show)++type DynPred s = s -> DynLogic s++-- * Building formulae++-- | `False` for DL formulae.+ignore :: DynFormula s++-- | `True` for DL formulae.+passTest :: DynFormula s++-- | Given `f` must be `True` given /any/ state.+afterAny :: (s -> DynFormula s) -> DynFormula s++-- | Given `f` must be `True` after /some/ action.+-- `f` is passed the state resulting from executing the `Action`.+after ::+  (Show a, Typeable a, Eq (Action s a)) =>+  Action s a ->+  (s -> DynFormula s) ->+  DynFormula s++-- | 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++-- | 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++-- | 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+-- ??+withSize :: (Int -> DynFormula s) -> DynFormula s+-- ??+toStop :: DynFormula s -> DynFormula s++-- | Successfully ends the test.+done :: s -> DynFormula s++-- | Ends test with given error message.+errorDL :: String -> DynFormula s++-- | 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++-- | 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 :: (s -> DynFormula s) -> (s -> DynFormula s)++ignore = DynFormula . const $ EmptySpec+passTest = DynFormula . const $ Stop+afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n+after act f = DynFormula $ \n -> After (Some act) $ \s -> unDynFormula (f s) n+DynFormula f ||| DynFormula g = DynFormula $ \n -> Alt Angelic (f n) (g n)++-- In formulae, we use only angelic+-- choice. But it becomes demonic after one+-- step (that is, the choice has been made).+forAllQ q f+  | isEmptyQ q' = ignore+  | otherwise = DynFormula $ \n -> ForAll q' $ ($ n) . unDynFormula . f+ where+  q' = quantify q++weight w f = DynFormula $ Weight w . unDynFormula f++withSize f = DynFormula $ \n -> unDynFormula (f n) n++toStop (DynFormula f) = DynFormula $ Stopping . f++done _ = passTest++errorDL s = DynFormula . const $ After (Error s) (const EmptySpec)++monitorDL m (DynFormula f) = DynFormula $ Monitor m . f++always p s = withSize $ \n -> toStop (p s) ||| p s ||| weight (fromIntegral n) (afterAny (always p))++data DynLogicTest s+  = BadPrecondition [TestStep s] [Any (Action s)] s+  | Looping [TestStep s]+  | Stuck [TestStep s] s+  | DLScript [TestStep s]++data TestStep s+  = Do (Step s)+  | forall a. (Eq a, Show a, Typeable a) => Witness a++instance Eq (TestStep s) where+  Do s == Do s' = s == s'+  Witness (a :: a) == Witness (a' :: a') =+    case eqT @a @a' of+      Just Refl -> a == a'+      Nothing -> False+  _ == _ = False++instance StateModel s => Show (TestStep s) where+  show (Do step) = "Do $ " ++ show step+  show (Witness a) = "Witness (" ++ show a ++ " :: " ++ show (typeOf a) ++ ")"++instance StateModel s => Show (DynLogicTest s) where+  show (BadPrecondition as bads s) =+    unlines $+      ["BadPrecondition"]+        ++ bracket (map show as)+        ++ ["  " ++ show (nub bads)]+        ++ ["  " ++ showsPrec 11 s ""]+  show (Looping as) =+    unlines $ "Looping" : bracket (map show as)+  show (Stuck as s) =+    unlines $ ["Stuck"] ++ bracket (map show as) ++ ["  " ++ showsPrec 11 s ""]+  show (DLScript as) =+    unlines $ "DLScript" : bracket (map show as)++bracket :: [String] -> [String]+bracket [] = ["  []"]+bracket [s] = ["  [" ++ s ++ "]"]+bracket (first : rest) =+  ["  [" ++ first ++ ", "]+    ++ map (("   " ++) . (++ ", ")) (init rest)+    ++ ["   " ++ last rest ++ "]"]++-- | 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 _ = False++-- * 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 = forAllMappedScripts id id++-- | `Property` function suitable for formulae without choice.+forAllUniqueScripts ::+  (DynLogicModel s, Testable a) =>+  Int ->+  s ->+  DynFormula s ->+  (Actions s -> a) ->+  Property+forAllUniqueScripts n s f k =+  QC.withSize $ \sz ->+    let d = unDynFormula f sz+     in case generate chooseUniqueNextStep d n s 500 [] of+          Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False+          Just test -> validDLTest d test .&&. (applyMonitoring d test . property $ k (scriptFromDL test))++forAllScripts_ ::+  (DynLogicModel s, Testable a) =>+  DynFormula s ->+  (Actions s -> a) ->+  Property+forAllScripts_ f k =+  QC.withSize $ \n ->+    let d = unDynFormula f n+     in forAll (sized $ generateDLTest d) $+          withDLScript d k++-- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose.+-- ??+forAllMappedScripts ::+  (DynLogicModel s, Testable a, Show rep) =>+  (rep -> DynLogicTest s) ->+  (DynLogicTest s -> rep) ->+  DynFormula s ->+  (Actions s -> a) ->+  Property+forAllMappedScripts to from f k =+  QC.withSize $ \n ->+    let d = unDynFormula f n+     in forAllShrink+          (Smart 0 <$> sized ((from <$>) . generateDLTest d))+          (shrinkSmart ((from <$>) . shrinkDLTest d . to))+          $ \(Smart _ script) ->+            withDLScript d k (to script)++forAllMappedScripts_ ::+  (DynLogicModel s, Testable a, Show rep) =>+  (rep -> DynLogicTest s) ->+  (DynLogicTest s -> rep) ->+  DynFormula s ->+  (Actions s -> a) ->+  Property+forAllMappedScripts_ to from f k =+  QC.withSize $ \n ->+    let d = unDynFormula f n+     in forAll (sized $ (from <$>) . generateDLTest d) $+          withDLScript d k . to++withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property+withDLScript d k test =+  validDLTest d test .&&. (applyMonitoring d test . property $ k (scriptFromDL test))++withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property+withDLScriptPrefix f k test =+  QC.withSize $ \n ->+    let d = unDynFormula f n+        test' = unfailDLTest d test+     in validDLTest d test' .&&. (applyMonitoring d test' . property $ k (scriptFromDL test'))++generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)+generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size []++generate ::+  (Monad m, DynLogicModel s) =>+  (s -> Int -> DynLogic s -> m (NextStep s)) ->+  DynLogic s ->+  Int ->+  s ->+  Int ->+  [TestStep s] ->+  m (DynLogicTest s)+generate chooseNextStepFun d n s size as =+  case badActions d s of+    [] ->+      if n > sizeLimit size+        then return $ Looping (reverse as)+        else do+          let preferred = if n > size then stopping d else noStopping d+              useStep StoppingStep _ = return $ DLScript (reverse as)+              useStep (Stepping (Do (var := act)) d') _ =+                generate+                  chooseNextStepFun+                  d'+                  (n + 1)+                  (nextState s act var)+                  size+                  (Do (var := act) : as)+              useStep (Stepping (Witness a) d') _ =+                generate+                  chooseNextStepFun+                  d'+                  n+                  s+                  size+                  (Witness a : as)+              useStep NoStep alt = alt+          foldr+            (\step k -> do try <- chooseNextStepFun s n step; useStep try k)+            (return $ Stuck (reverse as) s)+            [preferred, noAny preferred, d, noAny d]+    bs -> return $ BadPrecondition (reverse as) bs s++sizeLimit :: Int -> Int+sizeLimit size = 2 * size + 20++initialStateFor :: StateModel s => DynLogic s -> s+initialStateFor _ = initialState++stopping :: DynLogic s -> DynLogic s+stopping EmptySpec = EmptySpec+stopping Stop = Stop+stopping (After act k) = After act k+stopping (AfterAny _) = EmptySpec+stopping (Alt b d d') = Alt b (stopping d) (stopping d')+stopping (Stopping d) = d+stopping (Weight w d) = Weight w (stopping d)+stopping (ForAll _ _) = EmptySpec+stopping (Monitor f d) = Monitor f (stopping d)++noStopping :: DynLogic s -> DynLogic s+noStopping EmptySpec = EmptySpec+noStopping Stop = EmptySpec+noStopping (After act k) = After act k+noStopping (AfterAny k) = AfterAny k+noStopping (Alt b d d') = Alt b (noStopping d) (noStopping d')+noStopping (Stopping _) = EmptySpec+noStopping (Weight w d) = Weight w (noStopping d)+noStopping (ForAll q f) = ForAll q f+noStopping (Monitor f d) = Monitor f (noStopping d)++noAny :: DynLogic s -> DynLogic s+noAny EmptySpec = EmptySpec+noAny Stop = Stop+noAny (After act k) = After act k+noAny (AfterAny _) = EmptySpec+noAny (Alt b d d') = Alt b (noAny d) (noAny d')+noAny (Stopping d) = Stopping (noAny d)+noAny (Weight w d) = Weight w (noAny d)+noAny (ForAll q f) = ForAll q f+noAny (Monitor f d) = Monitor f (noAny d)++nextSteps :: DynLogic s -> [(Double, DynLogic s)]+nextSteps EmptySpec = []+nextSteps Stop = [(1, Stop)]+nextSteps (After act k) = [(1, After act k)]+nextSteps (AfterAny k) = [(1, AfterAny k)]+nextSteps (Alt _ d d') = nextSteps d ++ nextSteps d'+nextSteps (Stopping d) = nextSteps d+nextSteps (Weight w d) = [(w * w', s) | (w', s) <- nextSteps d, w * w' > never]+nextSteps (ForAll q f) = [(1, ForAll q f)]+nextSteps (Monitor _f d) = nextSteps d++chooseOneOf :: [(Double, DynLogic s)] -> Gen (DynLogic s)+chooseOneOf steps = frequency [(round (w / never), return s) | (w, s) <- steps]++never :: Double+never = 1.0e-9++data NextStep s+  = StoppingStep+  | Stepping (TestStep s) (DynLogic s)+  | NoStep++chooseNextStep :: DynLogicModel s => s -> Int -> DynLogic s -> Gen (NextStep s)+chooseNextStep s n d =+  case nextSteps d of+    [] -> return NoStep+    steps -> do+      chosen <- chooseOneOf steps+      case chosen of+        EmptySpec -> return NoStep+        Stop -> return StoppingStep+        After (Some a) k ->+          return $ Stepping (Do $ Var n := a) (k (nextState s a (Var n)))+        AfterAny k -> do+          m <- keepTryingUntil 100 (arbitraryAction s) $+            \case+              Some act -> precondition s act && not (restricted act)+              Error _ -> False+          case m of+            Nothing -> return NoStep+            Just (Some a) ->+              return $+                Stepping+                  (Do $ Var n := a)+                  (k (nextState s a (Var n)))+            Just Error{} -> error "impossible"+        ForAll q f -> do+          x <- generateQ q+          return $ Stepping (Witness x) (f x)+        After Error{} _ -> error "chooseNextStep: After Error"+        Alt{} -> error "chooseNextStep: Alt"+        Stopping{} -> error "chooseNextStep: Stopping"+        Weight{} -> error "chooseNextStep: Weight"+        Monitor{} -> error "chooseNextStep: Monitor"++chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => s -> Int -> DynLogic s -> m (NextStep s)+chooseUniqueNextStep s n d =+  case snd <$> nextSteps d of+    [] -> return NoStep+    [EmptySpec] -> return NoStep+    [Stop] -> return StoppingStep+    [After (Some a) k] -> return $ Stepping (Do $ Var n := a) (k (nextState s a (Var n)))+    _ -> fail "chooseUniqueNextStep: non-unique action in DynLogic"++keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)+keepTryingUntil 0 _ _ = return Nothing+keepTryingUntil n g p = do+  x <- g+  if p x then return $ Just x else scale (+ 1) $ keepTryingUntil (n - 1) g p++shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]+shrinkDLTest _ (Looping _) = []+shrinkDLTest d tc =+  [ test | as' <- shrinkScript d (getScript tc), let test = makeTestFromPruned d (pruneDLTest d as'),+  -- Don't shrink a non-executable test case to an executable one.+  case (tc, test) of+    (DLScript _, _) -> True+    (_, DLScript _) -> False+    _ -> True+  ]++shrinkScript :: DynLogicModel t => DynLogic t -> [TestStep t] -> [[TestStep t]]+shrinkScript dl steps = shrink' dl steps initialState+ where+  shrink' _ [] _ = []+  shrink' d (step : as) s =+    [] :+    reverse (takeWhile (not . null) [drop (n - 1) as | n <- iterate (* 2) 1])+      ++ case step of+        Do (Var i := act) ->+          [Do (Var i := act') : as | Some act' <- shrinkAction s act]+        Witness a ->+          -- When we shrink a witness, allow one shrink of the+          -- rest of the script... so assuming the witness may be+          -- used once to construct the rest of the test. If used+          -- more than once, we may need double shrinking.+          [ Witness a' : as' | a' <- shrinkWitness d a, as' <- as : shrink' (stepDLtoDL d s (Witness a')) as s+          ]+      ++ [ step : as'+         | as' <- shrink' (stepDLtoDL d s step) as $+            case step of+              Do (var := act) -> nextState s act var+              Witness _ -> s+         ]++shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a]+shrinkWitness (ForAll (q :: Quantification a) _) (a :: a') =+  case eqT @a @a' of+    Just Refl | isaQ q a -> shrinkQ q a+    _ -> []+shrinkWitness (Alt _ d d') a = shrinkWitness d a ++ shrinkWitness d' a+shrinkWitness (Stopping d) a = shrinkWitness d a+shrinkWitness (Weight _ d) a = shrinkWitness d a+shrinkWitness (Monitor _ d) a = shrinkWitness d a+shrinkWitness _ _ = []++-- The result of pruning a list of actions is a list of actions that+-- could have been generated by the dynamic logic.+pruneDLTest :: DynLogicModel s => DynLogic s -> [TestStep s] -> [TestStep s]+pruneDLTest dl = prune [dl] initialState+ where+  prune [] _ _ = []+  prune _ _ [] = []+  prune ds s (Do (var := act) : rest)+    | precondition s act =+      case [d' | d <- ds, d' <- stepDL d s (Do $ var := act)] of+        [] -> prune ds s rest+        ds' ->+          Do (var := act) :+          prune ds' (nextState s act var) rest+    | otherwise =+      prune ds s rest+  prune ds s (Witness a : rest) =+    case [d' | d <- ds, d' <- stepDL d s (Witness a)] of+      [] -> prune ds s rest+      ds' -> Witness a : prune ds' s rest++stepDL :: DynLogicModel s => DynLogic s -> s -> TestStep s -> [DynLogic s]+stepDL (After a k) s (Do (var := act))+  | a == Some act = [k (nextState s act var)]+stepDL (AfterAny k) s (Do (var := act))+  | not (restricted act) = [k (nextState s act var)]+stepDL (Alt _ d d') s step = stepDL d s step ++ stepDL d' s step+stepDL (Stopping d) s step = stepDL d s step+stepDL (Weight _ d) s step = stepDL d s step+stepDL (ForAll (q :: Quantification a) f) _ (Witness (a :: a')) =+  case eqT @a @a' of+    Just Refl -> [f a | isaQ q a]+    Nothing -> []+stepDL (Monitor _f d) s step = stepDL d s step+stepDL _ _ _ = []++stepDLtoDL :: DynLogicModel s => DynLogic s -> s -> TestStep s -> DynLogic s+stepDLtoDL d s step = case stepDL d s step of+  [] -> EmptySpec+  ds -> foldr1 (Alt Demonic) ds++propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property+propPruningGeneratedScriptIsNoop d =+  forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest d) $ \test ->+    let script = case test of+          BadPrecondition s _ _ -> s+          Looping s -> s+          Stuck s _ -> s+          DLScript s -> s+     in script == pruneDLTest d script++getScript :: DynLogicTest s -> [TestStep s]+getScript (BadPrecondition s _ _) = s+getScript (Looping s) = s+getScript (Stuck s _) = s+getScript (DLScript s) = s++makeTestFromPruned :: DynLogicModel s => DynLogic s -> [TestStep s] -> DynLogicTest s+makeTestFromPruned dl = make dl initialState+ where+  make d s as | not (null bad) = BadPrecondition as bad s+   where+    bad = badActions d s+  make d s []+    | stuck d s = Stuck [] s+    | otherwise = DLScript []+  make d curStep (step : steps) =+    case make+      (stepDLtoDL d curStep step)+      ( case step of+          Do (var := act) -> nextState curStep act var+          Witness _ -> curStep+      )+      steps of+      BadPrecondition as bad s -> BadPrecondition (step : as) bad s+      Stuck as s -> Stuck (step : as) s+      DLScript as -> DLScript (step : as)+      Looping{} -> error "makeTestFromPruned: Looping"++-- | 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 d test = makeTestFromPruned d $ pruneDLTest d steps+ where+  steps = case test of+    BadPrecondition as _ _ -> as+    Stuck as _ -> as+    DLScript as -> as+    Looping as -> as++stuck :: DynLogicModel s => DynLogic s -> s -> Bool+stuck EmptySpec _ = True+stuck Stop _ = False+stuck (After _ _) _ = False+stuck (AfterAny _) s =+  not $+    canGenerate+      0.01+      (arbitraryAction s)+      ( \case+          Some act ->+            precondition s act+              && not (restricted act)+          Error _ -> False+      )+stuck (Alt Angelic d d') s = stuck d s && stuck d' s+stuck (Alt Demonic d d') s = stuck d s || stuck d' s+stuck (Stopping d) s = stuck d s+stuck (Weight w d) s = w < never || stuck d s+stuck (ForAll _ _) _ = False+stuck (Monitor _ d) s = stuck d s++validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property+validDLTest _ (DLScript _) = property True+validDLTest _ (Stuck as _) = counterexample ("Stuck\n" ++ (unlines . map ("  " ++) . lines $ show as)) False+validDLTest _ (Looping as) = counterexample ("Looping\n" ++ (unlines . map ("  " ++) . lines $ show as)) False+validDLTest _ (BadPrecondition as bads _s) = counterexample ("BadPrecondition\n" ++ show as ++ "\n" ++ unlines (showBad <$> bads)) False+ where+  showBad (Error s) = s+  showBad a = show a++scriptFromDL :: DynLogicTest s -> Actions s+scriptFromDL (DLScript s) = Actions [a | Do a <- s]+scriptFromDL _ = Actions []++badActions :: StateModel s => DynLogic s -> s -> [Any (Action s)]+badActions EmptySpec _ = []+badActions Stop _ = []+badActions (After (Some a) _) s+  | precondition s a = []+  | otherwise = [Some a]+badActions (After (Error m) _) _s = [Error m]+badActions (AfterAny _) _ = []+badActions (Alt _ d d') s = badActions d s ++ badActions d' s+badActions (Stopping d) s = badActions d s+badActions (Weight w d) s = if w < never then [] else badActions d s+badActions (ForAll _ _) _ = []+badActions (Monitor _ d) s = badActions d s++applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property+applyMonitoring d (DLScript s) p =+  case findMonitoring d initialState s of+    Just f -> f p+    Nothing -> p+applyMonitoring _ Stuck{} p = p+applyMonitoring _ Looping{} p = p+applyMonitoring _ BadPrecondition{} p = p++findMonitoring :: DynLogicModel s => DynLogic s -> s -> [TestStep s] -> Maybe (Property -> Property)+findMonitoring Stop _s [] = Just id+findMonitoring (After (Some a) k) s (Do (var := a') : as)+  | Some a == Some a' = findMonitoring (k s') s' as+ where+  s' = nextState s a' var+findMonitoring (AfterAny k) s as@(Do (_var := a) : _)+  | not (restricted a) = findMonitoring (After (Some a) k) s as+findMonitoring (Alt _b d d') s as =+  -- Give priority to monitoring matches to the left. Combining both+  -- results in repeated monitoring from always, which is unexpected.+  findMonitoring d s as <|> findMonitoring d' s as+findMonitoring (Stopping d) s as = findMonitoring d s as+findMonitoring (Weight _ d) s as = findMonitoring d s as+findMonitoring (ForAll (_q :: Quantification a) k) s (Witness (a :: a') : as) =+  case eqT @a @a' of+    Just Refl -> findMonitoring (k a) s as+    Nothing -> Nothing+findMonitoring (Monitor m d) s as =+  (m .) <$> findMonitoring d s as+findMonitoring _ _ _ = Nothing
+ src/Test/QuickCheck/DynamicLogic/Quantify.hs view
@@ -0,0 +1,222 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}++-- | This module defines Quantifications, which are used together with+--   forAllQ in DynamicLogic. A `Quantification t` can be used to generate+--   a `t`, shrink a `t`, and recognise a generated `t`.+module Test.QuickCheck.DynamicLogic.Quantify (+  Quantification (isaQ),+  isEmptyQ,+  generateQ,+  shrinkQ,+  arbitraryQ,+  exactlyQ,+  elementsQ,+  oneofQ,+  frequencyQ,+  mapQ,+  whereQ,+  chooseQ,+  withGenQ,+  validQuantification,+  Quantifiable (..),+) where++import Control.Monad+import Data.Maybe+import Data.Typeable+import System.Random+import Test.QuickCheck+import Test.QuickCheck.DynamicLogic.CanGenerate++-- | A `Quantification` over a type @a@ is a generator that can be used with+--   `Plutus.Contract.Test.ContractModel.forAllQ` to generate random values in+--   DL scenarios. In addition to a QuickCheck generator a `Quantification` contains a shrinking+--   strategy that ensures that shrunk values stay in the range of the generator.+data Quantification a = Quantification+  { genQ :: Maybe (Gen a)+  , isaQ :: a -> Bool+  , shrQ :: a -> [a]+  }++isEmptyQ :: Quantification a -> Bool+isEmptyQ = isNothing . genQ++generateQ :: Quantification a -> Gen a+generateQ q = fromJust (genQ q) `suchThat` isaQ q++shrinkQ :: Quantification a -> a -> [a]+shrinkQ q a = filter (isaQ q) (shrQ q a)++-- | Wrap a `Gen a` generator in a `Quantification a`.+-- Uses given shrinker.+withGenQ :: Gen a -> (a -> [a]) -> Quantification a+withGenQ gen = Quantification (Just gen) (const True)++-- | Pack up an `Arbitrary` instance as a `Quantification`. Treats all values as being in range.+arbitraryQ :: Arbitrary a => Quantification a+arbitraryQ = Quantification (Just arbitrary) (const True) shrink++-- | Generates exactly the given value. Does not shrink.+exactlyQ :: Eq a => a -> Quantification a+exactlyQ a =+  Quantification+    (Just $ return a)+    (== a)+    (const [])++-- | Generate a random value in a given range (inclusive).+chooseQ :: (Arbitrary a, Random a, Ord a) => (a, a) -> Quantification a+chooseQ r@(a, b) =+  Quantification+    (guard (a <= b) >> Just (choose r))+    is+    (filter is . shrink)+ where+  is x = a <= x && x <= b++-- | Pick a random value from a list. Treated as an empty choice if the list is empty:+--+-- @+-- `Plutus.Contract.Test.ContractModel.forAllQ` (`elementsQ` []) == `Control.Applicative.empty`+-- @+elementsQ :: Eq a => [a] -> Quantification a+elementsQ as = Quantification g (`elem` as) (\a -> takeWhile (/= a) as)+ where+  g+    | null as = Nothing+    | otherwise = Just (elements as)++-- | Choose from a weighted list of quantifications. Treated as an `Control.Applicative.empty`+--   choice if no quantification has weight > 0.+frequencyQ :: [(Int, Quantification a)] -> Quantification a+frequencyQ iqs =+  Quantification+    ( case [(i, g) | (i, q) <- iqs, i > 0, Just g <- [genQ q]] of+        [] -> Nothing+        igs -> Just (frequency igs)+    )+    (isa iqs)+    (shr iqs)+ where+  isa [] _ = False+  isa ((i, q) : iqs) a = (i > 0 && isaQ q a) || isa iqs a+  shr [] _ = []+  shr ((i, q) : iqs) a =+    [a' | i > 0, isaQ q a, a' <- shrQ q a]+      ++ shr iqs a++-- | Choose from a list of quantifications. Same as `frequencyQ` with all weights the same (and >+--   0).+oneofQ :: [Quantification a] -> Quantification a+oneofQ qs = frequencyQ $ map (1,) qs++-- | `Quantification` is not a `Functor`, since it also keeps track of the range of the generators.+--   However, if you have two functions+-- @+-- to   :: a -> b+-- from :: b -> a+-- @+--   satisfying @from . to = id@ you can go from a quantification over @a@ to one over @b@. Note+--   that the @from@ function need only be defined on the image of @to@.+mapQ :: (a -> b, b -> a) -> Quantification a -> Quantification b+mapQ (f, g) q =+  Quantification+    ((f <$>) <$> genQ q)+    (isaQ q . g)+    (map f . shrQ q . g)++-- | Restrict the range of a quantification.+whereQ :: Quantification a -> (a -> Bool) -> Quantification a+whereQ q p =+  Quantification+    ( case genQ q of+        Just g | canGenerate 0.01 g p -> Just (g `suchThat` p)+        _ -> Nothing+    )+    (\a -> p a && isaQ q a)+    (\a -> if p a then filter p (shrQ q a) else [])++pairQ :: Quantification a -> Quantification b -> Quantification (a, b)+pairQ q q' =+  Quantification+    (liftM2 (,) <$> genQ q <*> genQ q')+    (\(a, a') -> isaQ q a && isaQ q' a')+    (\(a, a') -> map (,a') (shrQ q a) ++ map (a,) (shrQ q' a'))++-- | Generalization of `Quantification`s, which lets you treat lists and tuples of quantifications+--   as quantifications. For instance,+--+-- @+--   ...+--   (die1, die2) <- `Plutus.Contract.Test.ContractModel.forAllQ` (`chooseQ` (1, 6), `chooseQ` (1, 6))+--   ...+-- @+class+  (Eq (Quantifies q), Show (Quantifies q), Typeable (Quantifies q)) =>+  Quantifiable q+  where+  -- | The type of values quantified over.+  --+  -- @+  -- `Quantifies` (`Quantification` a) = a+  -- @+  type Quantifies q++  -- | Computing the actual `Quantification`.+  quantify :: q -> Quantification (Quantifies q)++instance (Eq a, Show a, Typeable a) => Quantifiable (Quantification a) where+  type Quantifies (Quantification a) = a+  quantify = id++instance (Quantifiable a, Quantifiable b) => Quantifiable (a, b) where+  type Quantifies (a, b) = (Quantifies a, Quantifies b)+  quantify (a, b) = pairQ (quantify a) (quantify b)++instance (Quantifiable a, Quantifiable b, Quantifiable c) => Quantifiable (a, b, c) where+  type Quantifies (a, b, c) = (Quantifies a, Quantifies b, Quantifies c)+  quantify (a, b, c) = mapQ (to, from) (quantify a `pairQ` (quantify b `pairQ` quantify c))+   where+    to (a, (b, c)) = (a, b, c)+    from (a, b, c) = (a, (b, c))++instance (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d) => Quantifiable (a, b, c, d) where+  type+    Quantifies (a, b, c, d) =+      (Quantifies a, Quantifies b, Quantifies c, Quantifies d)+  quantify (a, b, c, d) =+    mapQ (to, from) (quantify a `pairQ` (quantify b `pairQ` (quantify c `pairQ` quantify d)))+   where+    to (a, (b, (c, d))) = (a, b, c, d)+    from (a, b, c, d) = (a, (b, (c, d)))++instance+  (Quantifiable a, Quantifiable b, Quantifiable c, Quantifiable d, Quantifiable e) =>+  Quantifiable (a, b, c, d, e)+  where+  type+    Quantifies (a, b, c, d, e) =+      (Quantifies a, Quantifies b, Quantifies c, Quantifies d, Quantifies e)+  quantify (a, b, c, d, e) =+    mapQ (to, from) (quantify a `pairQ` (quantify b `pairQ` (quantify c `pairQ` (quantify d `pairQ` quantify e))))+   where+    to (a, (b, (c, (d, e)))) = (a, b, c, d, e)+    from (a, b, c, d, e) = (a, (b, (c, (d, e))))++instance Quantifiable a => Quantifiable [a] where+  type Quantifies [a] = [Quantifies a]+  quantify [] = Quantification (Just $ return []) null (const [])+  quantify (a : as) =+    mapQ (to, from) (pairQ (quantify a) (quantify as))+      `whereQ` (not . null)+   where+    to (x, xs) = x : xs+    from (x : xs) = (x, xs)+    from [] = error "quantify: impossible"++validQuantification :: Show a => Quantification a -> Property+validQuantification q =+  forAllShrink (fromJust $ genQ q) (shrinkQ q) $ isaQ q
+ src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs view
@@ -0,0 +1,14 @@+module Test.QuickCheck.DynamicLogic.SmartShrinking (shrinkSmart) where++import Test.QuickCheck++-- | This combinator captures the 'smart shrinking' implemented for the+-- Smart type wrapper in Test.QuickCheck.Modifiers.+shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a]+shrinkSmart shr (Smart i x) = take i' ys `ilv` drop i' ys+ where+  ys = [Smart j y | (j, y) <- [0 ..] `zip` shr x]+  i' = 0 `max` (i - 2)+  [] `ilv` bs = bs+  as `ilv` [] = as+  (a : as) `ilv` (b : bs) = a : b : (as `ilv` bs)
+ src/Test/QuickCheck/DynamicLogic/Utils.hs view
@@ -0,0 +1,7 @@+module Test.QuickCheck.DynamicLogic.Utils where++import Test.QuickCheck+import Test.QuickCheck.Property++withSize :: Testable prop => (Int -> prop) -> Property+withSize f = MkProperty . sized $ unProperty . property . f
+ src/Test/QuickCheck/StateModel.hs view
@@ -0,0 +1,342 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE RecordWildCards #-}++-- | Simple (stateful) Model-Based Testing library for use with Haskell QuickCheck.+--+-- This module provides the basic machinery to define a `StateModel` from which /traces/ can+-- be generated and executed against some /actual/ implementation code to define monadic `Property`+-- to be asserted by QuickCheck.+module Test.QuickCheck.StateModel (+  StateModel (..),+  RunModel (..),+  Any (..),+  Step (..),+  LookUp,+  Var (..), -- we export the constructors so that users can construct test cases+  Actions (..),+  pattern Actions,+  EnvEntry (..),+  Env,+  stateAfter,+  runActions,+  runActionsInState,+  lookUpVar,+  lookUpVarMaybe,+  invertLookupVarMaybe,+) where++import Control.Monad+import Data.Data+import Test.QuickCheck as QC+import Test.QuickCheck.DynamicLogic.SmartShrinking+import Test.QuickCheck.Monadic++-- | The typeclass users implement to define a model against which to validate some implementation.+--+-- To implement a `StateModel`, user needs to provide at least the following:+--+--   * A datatype for `Action`s: Each test case is a sequence of `Action`s that's supposed to lead from+--     some `initialState` to some end state,+--   * A generator for traces of `Action`s, the `arbitraryAction` function,+--   * An `initialState`,+--   * A /transition/ function, `nextState`, that "interprets" each `Action` and producing some new `state`.+--+-- For finer grained control over the testing process, one can also define:+--+--  * `shrinkAction`: Shrinking is an important part of MBT as it allows QuickCheck engine to look for simpler+--    test cases when something goes wrong which makes troubleshooting easier,+--  * `precondition`: Filters generated `Action` depending on the `state`. When `precondition` is False then+--    the action is /rejected/ and a new one is tried. This is also useful when shrinking a trace+--    in order to ensure that removing some `Action` still produces a valid trace. The `precondition` can be+--    somewhat redundant with the generator's conditions,+--  * `postcondition`: This function is evaluated during test execution after `perform`ing the action, it allows+--    the model to express expectations about the output of actual code given some "transition".+class+  ( forall a. Show (Action state a)+  , Show state+  ) =>+  StateModel state+  where+  -- | The type of `Action` relevant for this `state`.+  --+  -- This is expected to be defined as a GADT where the `a` parameter is instantiated to some+  -- observable output from the SUT a given action is expected to produce. For example, here+  -- is a fragment of the `Action RegState` (taken from the `Spec.Dynamic.RegistryModel`  module) :+  --+  -- @+  --   data Action RegState a where+  --     Spawn      ::                           Action RegState ThreadId+  --     Register   :: String -> Var ThreadId -> Action RegState (Either ErrorCall ())+  --     KillThread :: Var ThreadId           -> Action RegState ()+  -- @+  --+  -- The @Spawn@ action should produce a @ThreadId@, whereas the @KillThread@ action does not return+  -- anything.+  data Action state a++  -- | Display name for `Action`.+  -- This is useful to provide sensible statistics about the distribution of `Action`s run+  -- when checking a property.+  --+  -- Default implementation uses a poor-man's string manipulation method to extract the+  -- constructor name from the value.+  actionName :: Action state a -> String+  actionName = head . words . show++  -- | Generator for `Action` depending on `state`.+  -- The generated values are wrapped in `Any` type to allow the model to /not/ generate an action under+  -- some circumstances: Any generated  `Error` value will be ignored when generating a trace for testing.+  arbitraryAction :: state -> Gen (Any (Action state))++  -- | Shrinker for `Action`.+  -- Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness+  -- of property-based testing.+  shrinkAction :: (Show a, Typeable a) => state -> Action state a -> [Any (Action state)]+  shrinkAction _ _ = []++  -- | Initial state of generated traces.+  initialState :: state++  -- | Transition function for the model.+  -- The `Var a` parameter is useful to keep reference to actual value of type `a` produced+  -- by `perform`ing the `Action` inside the `state` so that further actions can use `Lookup`+  -- to retrieve that data. This allows the model to be ignorant of those values yet maintain+  -- some references that can be compared and looked for.+  nextState :: state -> Action state a -> Var a -> state+  nextState s _ _ = s++  -- | Precondition for filtering generated `Action`.+  -- This function is applied before the action is performed, it is useful to refine generators that+  -- can produce more values than are useful.+  precondition :: state -> Action state a -> Bool+  precondition _ _ = True++  -- | Postcondition on the `a` value produced at some step.+  -- The result is `assert`ed and will make the property fail should it be `False`. This is useful+  -- to check the implementation produces expected values.+  postcondition :: state -> Action state a -> LookUp -> a -> Bool+  postcondition _ _ _ _ = True++  -- | Allows the user to attach information to the `Property` at each step of the process.+  -- This function is given the full transition that's been executed, including the start and ending+  -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`+  -- while executing this step.+  monitoring :: (state, state) -> Action state a -> LookUp -> a -> Property -> Property+  monitoring _ _ _ _ = id++-- | Perform an `Action` in some `state` in the `Monad` `m`.  This+-- is the function that's used to exercise the actual stateful+-- implementation, usually through various side-effects as permitted+-- by `m`. It produces a value of type `a`, eg. some observable+-- output from the `Action` that should later be kept in the+-- environment through a `Var a` also passed to the `nextState`+-- function.+--+-- The `Lookup` parameter provides an /environment/ to lookup `Var+-- a` instances from previous steps.+newtype RunModel state m = RunModel {perform :: forall a. state -> Action state a -> LookUp -> m a}++type LookUp = forall a. Typeable a => Var a -> a++type Env = [EnvEntry]++data EnvEntry where+  (:==) :: (Show a, Typeable a) => Var a -> a -> EnvEntry++infix 5 :==++deriving instance Show EnvEntry++lookUpVarMaybe :: Typeable a => Env -> Var a -> Maybe a+lookUpVarMaybe [] _ = Nothing+lookUpVarMaybe ((v' :== a) : env) v =+  case cast (v', a) of+    Just (v'', a') | v == v'' -> Just a'+    _ -> lookUpVarMaybe env v++lookUpVar :: Typeable a => Env -> Var a -> a+lookUpVar env v = case lookUpVarMaybe env v of+  Nothing -> error $ "Variable " ++ show v ++ " is not bound!"+  Just a -> a++invertLookupVarMaybe :: (Typeable a, Eq a) => Env -> a -> Maybe (Var a)+invertLookupVarMaybe [] _ = Nothing+invertLookupVarMaybe ((v :== a) : env) a' =+  case cast (v, a) of+    Just (v', a'') | a' == a'' -> Just v'+    _ -> invertLookupVarMaybe env a'++data Any f where+  Some :: (Show a, Typeable a, Eq (f a)) => f a -> Any f+  Error :: String -> Any f++deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))++instance Eq (Any f) where+  Some (a :: f a) == Some (b :: f b) =+    case eqT @a @b of+      Just Refl -> a == b+      Nothing -> False+  Error s == Error s' = s == s'+  _ == _ = False++data Step state where+  (:=) ::+    (Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>+    Var a ->+    Action state a ->+    Step state++infix 5 :=++deriving instance (forall a. Show (Action state a)) => Show (Step state)++newtype Var a = Var Int+  deriving (Eq, Ord, Show, Typeable, Data)++instance Eq (Step state) where+  (Var i := act) == (Var j := act') =+    i == j && Some act == Some act'++-- Action sequences use Smart shrinking, but this is invisible to+-- client code because the extra Smart constructor is concealed by a+-- pattern synonym.++-- We also collect a list of names of actions which were generated,+-- but were then rejected by their precondition.++data Actions state = Actions_ [String] (Smart [Step state])++pattern Actions :: [Step state] -> Actions state+pattern Actions as <-+  Actions_ _ (Smart _ as)+  where+    Actions as = Actions_ [] (Smart 0 as)++{-# COMPLETE Actions #-}++instance Semigroup (Actions state) where+  Actions_ rs (Smart k as) <> Actions_ rs' (Smart _ as') = Actions_ (rs ++ rs') (Smart k (as <> as'))++instance Eq (Actions state) where+  Actions as == Actions as' = as == as'++instance (forall a. Show (Action state a)) => Show (Actions state) where+  showsPrec d (Actions as)+    | d > 10 = ("(" ++) . shows (Actions as) . (")" ++)+    | null as = ("Actions []" ++)+    | otherwise =+      ("Actions \n [" ++)+        . foldr+          (.)+          (shows (last as) . ("]" ++))+          [shows a . (",\n  " ++) | a <- init as]++instance (StateModel state) => Arbitrary (Actions state) where+  arbitrary = do+    (as, rejected) <- arbActions initialState 1+    return $ Actions_ rejected (Smart 0 as)+   where+    arbActions :: state -> Int -> Gen ([Step state], [String])+    arbActions s step = sized $ \n ->+      let w = n `div` 2 + 1+       in frequency+            [ (1, return ([], []))+            ,+              ( w+              , do+                  (mact, rej) <- satisfyPrecondition+                  case mact of+                    Just (Some act) -> do+                      (as, rejected) <- arbActions (nextState s act (Var step)) (step + 1)+                      return ((Var step := act) : as, rej ++ rejected)+                    Just Error{} -> error "impossible"+                    Nothing ->+                      return ([], [])+              )+            ]+     where+      satisfyPrecondition = sized $ \n -> go n (2 * n) [] -- idea copied from suchThatMaybe+      go m n rej+        | m > n = return (Nothing, rej)+        | otherwise = do+          a <- resize m $ arbitraryAction s+          case a of+            Some act ->+              if precondition s act+                then return (Just (Some act), rej)+                else go (m + 1) n (actionName act : rej)+            Error _ ->+              go (m + 1) n rej++  shrink (Actions_ rs as) =+    map (Actions_ rs) (shrinkSmart (map (prune . map fst) . shrinkList shrinker . withStates) as)+   where+    shrinker (Var i := act, s) = [(Var i := act', s) | Some act' <- shrinkAction s act]++prune :: StateModel state => [Step state] -> [Step state]+prune = loop initialState+ where+  loop _s [] = []+  loop s ((var := act) : as)+    | precondition s act =+      (var := act) : loop (nextState s act var) as+    | otherwise =+      loop s as++withStates :: StateModel state => [Step state] -> [(Step state, state)]+withStates = loop initialState+ where+  loop _s [] = []+  loop s ((var := act) : as) =+    (var := act, s) : loop (nextState s act var) as++stateAfter :: StateModel state => Actions state -> state+stateAfter (Actions actions) = loop initialState actions+ where+  loop s [] = s+  loop s ((var := act) : as) = loop (nextState s act var) as++runActions ::+  forall state m.+  (StateModel state, Monad m) =>+  RunModel state m ->+  Actions state ->+  PropertyM m (state, Env)+runActions = runActionsInState @_ @m initialState++runActionsInState ::+  forall state m.+  (StateModel state, Monad m) =>+  state ->+  RunModel state m ->+  Actions state ->+  PropertyM m (state, Env)+runActionsInState state RunModel{..} (Actions_ rejected (Smart _ actions)) = loop state [] actions+ where+  loop _s env [] = do+    unless (null rejected) $+      monitor (tabulate "Actions rejected by precondition" rejected)+    return (_s, reverse env)+  loop s env ((Var n := act) : as) = do+    pre $ precondition s act+    ret <- run (perform s act (lookUpVar env))+    let name = actionName act+    monitor (tabulate "Actions" [name])+    let s' = nextState s act (Var n)+        env' = (Var n :== ret) : env+    monitor (monitoring (s, s') act (lookUpVar env') ret)+    assert $ postcondition s act (lookUpVar env) ret+    loop s' env' as