From 134f5147dc47451052587f944acc5039fed5fba5 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 6 Mar 2024 22:37:18 +0100 Subject: [PATCH 01/13] [wip] Circular buffer example --- quickcheck-dynamic/quickcheck-dynamic.cabal | 21 +-- quickcheck-dynamic/test/Spec.hs | 4 + .../test/Spec/CircularBuffer/Buffer.hs | 62 +++++++++ .../test/Spec/CircularBuffer/Model.hs | 126 ++++++++++++++++++ 4 files changed, 204 insertions(+), 9 deletions(-) create mode 100644 quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs create mode 100644 quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal index eabc03f..516755e 100644 --- a/quickcheck-dynamic/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic/quickcheck-dynamic.cabal @@ -91,6 +91,9 @@ test-suite quickcheck-dynamic-test hs-source-dirs: test other-modules: Spec.DynamicLogic.Counters + Spec.CircularBuffer.Model + Spec.CircularBuffer.Buffer + Spec.DynamicLogic.CounterModel Spec.DynamicLogic.Registry Spec.DynamicLogic.RegistryModel Test.QuickCheck.DynamicLogic.QuantifySpec @@ -98,12 +101,12 @@ test-suite quickcheck-dynamic-test ghc-options: -rtsopts build-depends: - , base - , containers - , mtl - , QuickCheck - , quickcheck-dynamic - , stm - , tasty - , tasty-hunit - , tasty-quickcheck + QuickCheck + , base + , containers + , mtl + , quickcheck-dynamic + , stm + , tasty + , tasty-quickcheck + , vector diff --git a/quickcheck-dynamic/test/Spec.hs b/quickcheck-dynamic/test/Spec.hs index 253af4f..db9d036 100644 --- a/quickcheck-dynamic/test/Spec.hs +++ b/quickcheck-dynamic/test/Spec.hs @@ -2,6 +2,8 @@ module Main (main) where +import Spec.CircularBuffer.Model qualified +import Spec.DynamicLogic.CounterModel qualified import Spec.DynamicLogic.RegistryModel qualified import Test.QuickCheck.DynamicLogic.QuantifySpec qualified import Test.QuickCheck.StateModelSpec qualified @@ -15,6 +17,8 @@ tests = testGroup "dynamic logic" [ Spec.DynamicLogic.RegistryModel.tests + , Spec.DynamicLogic.CounterModel.tests + , Spec.CircularBuffer.Model.tests , Test.QuickCheck.DynamicLogic.QuantifySpec.tests , Test.QuickCheck.StateModelSpec.tests ] diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs new file mode 100644 index 0000000..8adc1ea --- /dev/null +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE NamedFieldPuns #-} + +-- | A Reasonably efficient version of a ring buffer. +-- Directly stolen from [q-s-m](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs#L86) +module Spec.CircularBuffer.Buffer where + +import Data.Function (on) +import Data.IORef (IORef, newIORef, readIORef, writeIORef) +import Data.Vector.Unboxed.Mutable ( + IOVector, + ) +import qualified Data.Vector.Unboxed.Mutable as V + +-- | An efficient mutable circular buffer. +data Buffer = Buffer + { top :: IORef Int + -- ^ Index to the top: where to 'Put' the next element + , bot :: IORef Int + -- ^ Index to the bottom: where to 'Get' the next element + , arr :: IOVector Int + -- ^ Array of elements of fixed capacity + } + +-- | Different buffers are assumed to have disjoint memories, +-- so we can use 'V.overlaps' to check equality. +instance Eq Buffer where + (==) = + ((==) `on` top) + `also` ((==) `on` bot) + `also` (V.overlaps `on` arr) + where + also = (liftA2 . liftA2) (&&) + +-- | See 'New'. +newBuffer :: Int -> IO Buffer +newBuffer n = + Buffer + <$> newIORef 0 + <*> newIORef 0 + <*> V.new (n + 1) + +-- | See 'Put'. +putBuffer :: Int -> Buffer -> IO () +putBuffer x Buffer{top, arr} = do + i <- readIORef top + V.write arr i x + writeIORef top $! (i + 1) `mod` V.length arr + +-- | See 'Get'. +getBuffer :: Buffer -> IO Int +getBuffer Buffer{bot, arr} = do + j <- readIORef bot + y <- V.read arr j + writeIORef bot $! (j + 1) `mod` V.length arr + return y + +-- | See 'Len'. +lenBuffer :: Buffer -> IO Int +lenBuffer Buffer{top, bot, arr} = do + i <- readIORef top + j <- readIORef bot + return $ (i - j) `mod` V.length arr diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs new file mode 100644 index 0000000..2a434c5 --- /dev/null +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs @@ -0,0 +1,126 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} + +-- | An classic example of model-checking an implementation of a ring buffer. +-- +-- * Inspired by [q-s-m example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs) +-- * Also described by John Hughes [here](https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf) +module Spec.CircularBuffer.Model where + +import Control.Monad.State (MonadState (..), StateT) +import Control.Monad.Trans (lift) +import Data.Maybe (fromJust) +import GHC.Generics (Generic) +import Spec.CircularBuffer.Buffer (Buffer, getBuffer, lenBuffer, newBuffer, putBuffer) +import Test.QuickCheck (Arbitrary (..), Property, counterexample, getPositive, oneof) +import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), action, anyActions_, assert, assertModel, forAllDL, getModelStateDL, monitorDL) +import Test.QuickCheck.Extras (runPropertyStateT) +import Test.QuickCheck.Monadic (monadicIO) +import Test.QuickCheck.Monadic qualified as QC +import Test.QuickCheck.StateModel (Actions, Any (..), HasVariables (..), RunModel (..), StateModel (..), Var, runActions) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) + +-- * Model + +-- | A simple model of a `CircularBuffer` implemented using a `List`. +data CircularBufferModel + = NoBuffer + | CircularBufferModel + { size :: Int + , buffer :: [Var Int] + } + deriving (Eq, Show, Generic) + +instance StateModel CircularBufferModel where + data Action CircularBufferModel a where + -- Create new buffer of given capacity. + New :: Int -> Action CircularBufferModel () + -- Put an element at the top of the buffer. + Put :: Int -> Action CircularBufferModel Int + -- Get an element out of the bottom of the buffer. + Get :: Action CircularBufferModel Int + -- Get the number of elements in the buffer. + Len :: Action CircularBufferModel Int + + arbitraryAction ctx NoBuffer = Some . New . getPositive <$> arbitrary + arbitraryAction ctx CircularBufferModel{} = + oneof + [ Some . Put <$> arbitrary + , pure $ Some Get + , pure $ Some Len + ] + + initialState = NoBuffer + + nextState NoBuffer (New size) var = + CircularBufferModel{size, buffer = mempty} + nextState buf@CircularBufferModel{size, buffer} Put{} var + | length buffer < size = buf{buffer = var : buffer} + nextState buf@CircularBufferModel{buffer} Get _ + | length buffer > 0 = buf{buffer = init buffer} + nextState st _ _ = st + + precondition NoBuffer New{} = True + precondition CircularBufferModel{size, buffer} Put{} = length buffer < size + precondition CircularBufferModel{buffer} Get{} = length buffer > 0 + precondition _ _ = True + +deriving instance Show (Action CircularBufferModel a) +deriving instance Eq (Action CircularBufferModel a) + +instance HasVariables (Action CircularBufferModel a) where + getAllVariables = const mempty + +instance DynLogicModel CircularBufferModel where + restricted _ = False + +-- * RunModel + +instance RunModel CircularBufferModel (StateT (Maybe Buffer) IO) where + perform _st action _lookup = + case action of + New n -> lift (newBuffer n) >>= put . Just + Put v -> get >>= (lift . putBuffer v . fromJust) >> pure v + Get -> get >>= lift . getBuffer . fromJust + Len -> get >>= lift . lenBuffer . fromJust + + postcondition (CircularBufferModel{buffer}, after) Get lookup res = + let v = lookup (last buffer) + in pure $ v == res + postcondition _ _ _ _ = pure True + +prop_CircularBuffer :: Actions CircularBufferModel -> Property +prop_CircularBuffer s = + monadicIO $ do + runPropertyStateT (runActions @_ @(StateT (Maybe Buffer) IO) s) Nothing + QC.assert True + +propDL :: DL CircularBufferModel () -> Property +propDL d = forAllDL d prop_CircularBuffer + +-- probably not interesting = we are asserting something on the model +prop_NeverGoesOverSize :: DL CircularBufferModel () +prop_NeverGoesOverSize = do + anyActions_ + assertModel "Too many elements" $ \case + NoBuffer -> True + CircularBufferModel{size, buffer} -> length buffer <= size + +prop_GetReturnsFirstPut :: DL CircularBufferModel () +prop_GetReturnsFirstPut = do + anyActions_ + getModelStateDL >>= \case + CircularBufferModel{buffer} | not (null buffer) -> do + let toGet = last buffer + res <- action Get + assert ("wrong element: " <> show toGet <> ", res: " <> show res) $ res == toGet + _ -> pure () + +tests :: TestTree +tests = + testGroup + "Circular Buffer" + [ testProperty "never has more than 'size' elements" $ propDL prop_NeverGoesOverSize + , testProperty "Get first Put" $ propDL prop_GetReturnsFirstPut + ] From c244c84b1e38353c09609cbb75409650921a3329 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 16 Mar 2024 15:00:23 +0100 Subject: [PATCH 02/13] Reproduce bug in model from Quviq paper Require shrinking the actions to ensure the example is minimal => Need to shrink New for buffer size to decrease! --- .../test/Spec/CircularBuffer/Buffer.hs | 48 ++++++++--------- .../test/Spec/CircularBuffer/Model.hs | 51 +++++++------------ 2 files changed, 44 insertions(+), 55 deletions(-) diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs index 8adc1ea..9d04de5 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs @@ -9,15 +9,17 @@ import Data.IORef (IORef, newIORef, readIORef, writeIORef) import Data.Vector.Unboxed.Mutable ( IOVector, ) -import qualified Data.Vector.Unboxed.Mutable as V +import Data.Vector.Unboxed.Mutable qualified as V -- | An efficient mutable circular buffer. data Buffer = Buffer - { top :: IORef Int - -- ^ Index to the top: where to 'Put' the next element - , bot :: IORef Int - -- ^ Index to the bottom: where to 'Get' the next element - , arr :: IOVector Int + { size :: Int + -- ^ Size of buffer + , inp :: IORef Int + -- ^ Index to the next free slot where to 'Put' the next element + , outp :: IORef Int + -- ^ Index to the last occupied slot to 'Get' an element from + , buf :: IOVector Int -- ^ Array of elements of fixed capacity } @@ -25,38 +27,38 @@ data Buffer = Buffer -- so we can use 'V.overlaps' to check equality. instance Eq Buffer where (==) = - ((==) `on` top) - `also` ((==) `on` bot) - `also` (V.overlaps `on` arr) + ((==) `on` inp) + `also` ((==) `on` outp) + `also` (V.overlaps `on` buf) where also = (liftA2 . liftA2) (&&) -- | See 'New'. newBuffer :: Int -> IO Buffer newBuffer n = - Buffer + Buffer n <$> newIORef 0 <*> newIORef 0 - <*> V.new (n + 1) + <*> V.new n -- | See 'Put'. putBuffer :: Int -> Buffer -> IO () -putBuffer x Buffer{top, arr} = do - i <- readIORef top - V.write arr i x - writeIORef top $! (i + 1) `mod` V.length arr +putBuffer x Buffer{size, inp, buf} = do + i <- readIORef inp + V.write buf i x + writeIORef inp $! (i + 1) `mod` size -- | See 'Get'. getBuffer :: Buffer -> IO Int -getBuffer Buffer{bot, arr} = do - j <- readIORef bot - y <- V.read arr j - writeIORef bot $! (j + 1) `mod` V.length arr +getBuffer Buffer{size, outp, buf} = do + j <- readIORef outp + y <- V.read buf j + writeIORef outp $! (j + 1) `mod` size return y -- | See 'Len'. lenBuffer :: Buffer -> IO Int -lenBuffer Buffer{top, bot, arr} = do - i <- readIORef top - j <- readIORef bot - return $ (i - j) `mod` V.length arr +lenBuffer Buffer{inp, outp, size} = do + i <- readIORef inp + j <- readIORef outp + return $ (i - j) `mod` size diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs index 2a434c5..8131447 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE NamedFieldPuns #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} @@ -17,7 +18,7 @@ import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), action, anyActions_ import Test.QuickCheck.Extras (runPropertyStateT) import Test.QuickCheck.Monadic (monadicIO) import Test.QuickCheck.Monadic qualified as QC -import Test.QuickCheck.StateModel (Actions, Any (..), HasVariables (..), RunModel (..), StateModel (..), Var, runActions) +import Test.QuickCheck.StateModel (Actions, Any (..), HasVariables (..), RunModel (..), StateModel (..), Var, counterexamplePost, runActions) import Test.Tasty (TestTree, testGroup) import Test.Tasty.QuickCheck (testProperty) @@ -53,18 +54,21 @@ instance StateModel CircularBufferModel where initialState = NoBuffer - nextState NoBuffer (New size) var = - CircularBufferModel{size, buffer = mempty} - nextState buf@CircularBufferModel{size, buffer} Put{} var - | length buffer < size = buf{buffer = var : buffer} - nextState buf@CircularBufferModel{buffer} Get _ - | length buffer > 0 = buf{buffer = init buffer} - nextState st _ _ = st - precondition NoBuffer New{} = True - precondition CircularBufferModel{size, buffer} Put{} = length buffer < size precondition CircularBufferModel{buffer} Get{} = length buffer > 0 - precondition _ _ = True + precondition CircularBufferModel{} Put{} = True + precondition CircularBufferModel{} Len{} = True + precondition _ _ = False + + nextState NoBuffer (New size) var = CircularBufferModel{size, buffer = mempty} + nextState buf@CircularBufferModel{size, buffer} Put{} var = buf{buffer = var : buffer} + nextState buf@CircularBufferModel{buffer} Get _ = buf{buffer = init buffer} + nextState st _ _ = st + + shrinkAction _ _ = \case + New n -> Some . New <$> [i | i <- shrink n, i > 0] + Put n -> Some . Put <$> shrink n + _ -> [] deriving instance Show (Action CircularBufferModel a) deriving instance Eq (Action CircularBufferModel a) @@ -87,7 +91,9 @@ instance RunModel CircularBufferModel (StateT (Maybe Buffer) IO) where postcondition (CircularBufferModel{buffer}, after) Get lookup res = let v = lookup (last buffer) - in pure $ v == res + in do + counterexamplePost ("Expected: " <> show v <> ", got: " <> show res) + pure $ v == res postcondition _ _ _ _ = pure True prop_CircularBuffer :: Actions CircularBufferModel -> Property @@ -99,28 +105,9 @@ prop_CircularBuffer s = propDL :: DL CircularBufferModel () -> Property propDL d = forAllDL d prop_CircularBuffer --- probably not interesting = we are asserting something on the model -prop_NeverGoesOverSize :: DL CircularBufferModel () -prop_NeverGoesOverSize = do - anyActions_ - assertModel "Too many elements" $ \case - NoBuffer -> True - CircularBufferModel{size, buffer} -> length buffer <= size - -prop_GetReturnsFirstPut :: DL CircularBufferModel () -prop_GetReturnsFirstPut = do - anyActions_ - getModelStateDL >>= \case - CircularBufferModel{buffer} | not (null buffer) -> do - let toGet = last buffer - res <- action Get - assert ("wrong element: " <> show toGet <> ", res: " <> show res) $ res == toGet - _ -> pure () - tests :: TestTree tests = testGroup "Circular Buffer" - [ testProperty "never has more than 'size' elements" $ propDL prop_NeverGoesOverSize - , testProperty "Get first Put" $ propDL prop_GetReturnsFirstPut + [ testProperty "implementation respects its model" prop_CircularBuffer ] From 8f47daa68d59419660d6c006adc653de44e25eed Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 16 Mar 2024 15:12:22 +0100 Subject: [PATCH 03/13] Check postcondition for Len and reproduce 2nd bug from paper --- quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs index 8131447..2dba63a 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs @@ -56,7 +56,7 @@ instance StateModel CircularBufferModel where precondition NoBuffer New{} = True precondition CircularBufferModel{buffer} Get{} = length buffer > 0 - precondition CircularBufferModel{} Put{} = True + precondition CircularBufferModel{buffer, size} Put{} = length buffer < size precondition CircularBufferModel{} Len{} = True precondition _ _ = False @@ -94,6 +94,10 @@ instance RunModel CircularBufferModel (StateT (Maybe Buffer) IO) where in do counterexamplePost ("Expected: " <> show v <> ", got: " <> show res) pure $ v == res + postcondition (CircularBufferModel{buffer}, after) Len lookup res = do + let len = length buffer + counterexamplePost $ "Expected; " <> show len <> ", got: " <> show res + pure $ res == len postcondition _ _ _ _ = pure True prop_CircularBuffer :: Actions CircularBufferModel -> Property From 07fa9cae4e43d173620fb37ec7056e3f64543c30 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 16 Mar 2024 15:23:50 +0100 Subject: [PATCH 04/13] Fix bug by increasing size by 1 It's not possible to reproduce the second bug because `mod` operator in Haskell is implementeed correctly, not like `rem` in C or Erlang. > (-1) `mod` 2 == 1 --- quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs | 8 +++++--- quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs | 7 +++---- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs index 9d04de5..5877de4 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs @@ -36,10 +36,12 @@ instance Eq Buffer where -- | See 'New'. newBuffer :: Int -> IO Buffer newBuffer n = - Buffer n + Buffer size <$> newIORef 0 <*> newIORef 0 - <*> V.new n + <*> V.new size + where + size = n + 1 -- | See 'Put'. putBuffer :: Int -> Buffer -> IO () @@ -61,4 +63,4 @@ lenBuffer :: Buffer -> IO Int lenBuffer Buffer{inp, outp, size} = do i <- readIORef inp j <- readIORef outp - return $ (i - j) `mod` size + pure $ (i - j) `mod` size diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs index 2dba63a..ae9fd20 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs @@ -13,8 +13,8 @@ import Control.Monad.Trans (lift) import Data.Maybe (fromJust) import GHC.Generics (Generic) import Spec.CircularBuffer.Buffer (Buffer, getBuffer, lenBuffer, newBuffer, putBuffer) -import Test.QuickCheck (Arbitrary (..), Property, counterexample, getPositive, oneof) -import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), action, anyActions_, assert, assertModel, forAllDL, getModelStateDL, monitorDL) +import Test.QuickCheck (Arbitrary (..), Property, getPositive, oneof) +import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), forAllDL) import Test.QuickCheck.Extras (runPropertyStateT) import Test.QuickCheck.Monadic (monadicIO) import Test.QuickCheck.Monadic qualified as QC @@ -113,5 +113,4 @@ tests :: TestTree tests = testGroup "Circular Buffer" - [ testProperty "implementation respects its model" prop_CircularBuffer - ] + [testProperty "implementation respects its model" prop_CircularBuffer] From e9a4308e76763bd3b2953e36bd51f4169dc2303e Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 16 Mar 2024 15:32:31 +0100 Subject: [PATCH 05/13] Introduce and fix 3rd bug (using rem) --- quickcheck-dynamic/quickcheck-dynamic.cabal | 1 + quickcheck-dynamic/test/Spec.hs | 2 -- quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs | 2 +- quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs | 5 +++-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal index 516755e..12fea31 100644 --- a/quickcheck-dynamic/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic/quickcheck-dynamic.cabal @@ -108,5 +108,6 @@ test-suite quickcheck-dynamic-test , quickcheck-dynamic , stm , tasty + , tasty-hunit , tasty-quickcheck , vector diff --git a/quickcheck-dynamic/test/Spec.hs b/quickcheck-dynamic/test/Spec.hs index db9d036..c16f1e3 100644 --- a/quickcheck-dynamic/test/Spec.hs +++ b/quickcheck-dynamic/test/Spec.hs @@ -3,7 +3,6 @@ module Main (main) where import Spec.CircularBuffer.Model qualified -import Spec.DynamicLogic.CounterModel qualified import Spec.DynamicLogic.RegistryModel qualified import Test.QuickCheck.DynamicLogic.QuantifySpec qualified import Test.QuickCheck.StateModelSpec qualified @@ -17,7 +16,6 @@ tests = testGroup "dynamic logic" [ Spec.DynamicLogic.RegistryModel.tests - , Spec.DynamicLogic.CounterModel.tests , Spec.CircularBuffer.Model.tests , Test.QuickCheck.DynamicLogic.QuantifySpec.tests , Test.QuickCheck.StateModelSpec.tests diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs index 5877de4..a5b739f 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Buffer.hs @@ -63,4 +63,4 @@ lenBuffer :: Buffer -> IO Int lenBuffer Buffer{inp, outp, size} = do i <- readIORef inp j <- readIORef outp - pure $ (i - j) `mod` size + pure $ (i - j + size) `rem` size diff --git a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs index ae9fd20..6689178 100644 --- a/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs +++ b/quickcheck-dynamic/test/Spec/CircularBuffer/Model.hs @@ -14,7 +14,7 @@ import Data.Maybe (fromJust) import GHC.Generics (Generic) import Spec.CircularBuffer.Buffer (Buffer, getBuffer, lenBuffer, newBuffer, putBuffer) import Test.QuickCheck (Arbitrary (..), Property, getPositive, oneof) -import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), forAllDL) +import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), action, forAllDL) import Test.QuickCheck.Extras (runPropertyStateT) import Test.QuickCheck.Monadic (monadicIO) import Test.QuickCheck.Monadic qualified as QC @@ -113,4 +113,5 @@ tests :: TestTree tests = testGroup "Circular Buffer" - [testProperty "implementation respects its model" prop_CircularBuffer] + [ testProperty "implementation respects its model" prop_CircularBuffer + ] From aec2582c553b1209c28a3474735015d312c76a39 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 1 Apr 2024 10:05:26 +0200 Subject: [PATCH 06/13] Simplified DL for pedagogical purposes --- quickcheck-dynamic/quickcheck-dynamic.cabal | 1 + quickcheck-dynamic/src/Test/QuickCheck/DL.hs | 215 +++++++++++++++++++ 2 files changed, 216 insertions(+) create mode 100644 quickcheck-dynamic/src/Test/QuickCheck/DL.hs diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal index 12fea31..267050b 100644 --- a/quickcheck-dynamic/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic/quickcheck-dynamic.cabal @@ -67,6 +67,7 @@ library import: lang hs-source-dirs: src exposed-modules: + Test.QuickCheck.DL Test.QuickCheck.DynamicLogic Test.QuickCheck.DynamicLogic.CanGenerate Test.QuickCheck.DynamicLogic.Internal diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DL.hs b/quickcheck-dynamic/src/Test/QuickCheck/DL.hs new file mode 100644 index 0000000..ce084cf --- /dev/null +++ b/quickcheck-dynamic/src/Test/QuickCheck/DL.hs @@ -0,0 +1,215 @@ +module Test.QuickCheck.DL where + +import Control.Applicative ((<|>)) +import Control.Monad (foldM) +import Test.QuickCheck ( + Arbitrary (..), + Gen, + Property, + forAllShrink, + (===), + ) + +-- Definition of Propositional Dynamic Logic +-- p.164 +-- f and p are atomic formulas and propositions respectively +-- See also these + +-- | `Prop`ositional logic part of Dynamic Logic. +-- This type is parameterised by the type of atomic propositions and atomic programs, whose +-- semantics is given by a Kripke structure. +data Prop f p where + -- | Atomic propositions + Prop :: f -> Prop f p + -- | Falsity + Zero :: Prop f p + -- | Truth + One :: Prop f p + -- | Basic logic combinator. + -- + -- Classically it's possible to reconstruct all the other usual + -- combinators from implication and falsity. + Imply :: Prop f p -> Prop f p -> Prop f p + -- | Necessity modality + -- + -- This is the only modality in this presentation as /possibility/ + -- is cumbersome to implement. + Always :: Prog f p -> Prop f p -> Prop f p + deriving (Eq, Show) + +-- | `Prog`ams part of Dynamic Logic. +-- +-- This type is parameterised by the type of atomic propositions and atomic programs, whose +-- semantics is typically given by a Kripke structure. +data Prog f p where + -- | Empty program, or /Stop/. + Empty :: Prog f p + -- | Atomic programs. + Prog :: p -> Prog f p + -- | Sequencing of programs. + Seq :: Prog f p -> Prog f p -> Prog f p + -- | Alternation of programs. + Alt :: Prog f p -> Prog f p -> Prog f p + -- | Unbounded repetition of programs. + Star :: Prog f p -> Prog f p + -- | Test of a `Prop`osition. + Test :: Prop f p -> Prog f p + deriving (Eq, Show) + +step + :: (f -> s -> Bool) + -- ^ A function to evaluate atomic formulas + -> (p -> s -> Maybe s) + -- ^ State transition + -> Int + -- ^ Size limit (?) + -> Prog f p + -- ^ Program to interpret + -> s + -- ^ state + -> Maybe s +step ϕ δ k prog s = + case prog of + Empty -> Just s + Prog p -> δ p s + Seq p q -> do + s' <- step ϕ δ k p s + step ϕ δ k q s' + Alt p q -> do + step ϕ δ k p s <|> step ϕ δ k q s + Test f -> + if eval ϕ δ (k - 1) f s + then Just s + else Nothing + Star p -> + foldM (flip $ step ϕ δ (k - 1)) s (replicate k p) + +eval + :: (f -> s -> Bool) + -- ^ A function to evaluate atomic formulas + -> (p -> s -> Maybe s) + -- ^ Transition function for programs + -> Int + -- ^ Size limit (?) + -> Prop f p + -- ^ The proposition to evaluate + -> s + -- ^ Initial state + -> Bool +eval ϕ δ k prop s = + case prop of + Prop f -> ϕ f s + Zero -> False + One -> True + Imply f g -> + not (eval ϕ δ (k - 1) f s) || eval ϕ δ (k - 1) g s + Always p f -> + case step ϕ δ k p s of + Nothing -> False + Just s' -> eval ϕ δ (k - 1) f s' + +data S = U | V | W + deriving (Eq, Show) + +data P = A + deriving (Eq, Show) + +instance Test.QuickCheck.Arbitrary P where + arbitrary = pure A + +type F = [S] + +phi :: F -> S -> Bool +phi = flip elem + +delta :: P -> S -> S +delta A = \case + U -> V + W -> U + V -> W + +-- | Tells whether or not a finite trace from some initial state +-- satisfies the given formula. +satisfy + :: (Eq s, Show p, Show f) + => (f -> s -> Bool) + -- ^ A function to evaluate atomic formulas + -> (p -> s -> Maybe s) + -- ^ Partial transition function for programs + -> s + -- ^ Initial state + -> Prop f p + -- ^ The proposition to evaluate + -> [p] + -- ^ The trace to check satisfaction of proposition against + -> Prop f p +satisfy ϕ δ s prop trace = + case prop of + Prop f -> + if ϕ f s then One else Zero + Zero -> Zero + One -> One + Imply f g -> + let f' = satisfy ϕ δ s f trace + g' = satisfy ϕ δ s g trace + in case (f', g') of + (Zero, _) -> One + (One, One) -> One + (_, _) -> Zero + Always p f -> + case match ϕ δ s trace p of + Right (s', trace') -> satisfy ϕ δ s' f trace' + Left{} -> Zero + +match + :: (Show p, Eq s, Show f) + => (f -> s -> Bool) + -> (p -> s -> Maybe s) + -> s + -> [p] + -> Prog f p + -> Either (String, [p]) (s, [p]) +match _ _ s [] = \case + Empty -> Right (s, []) + Star{} -> Right (s, []) + other -> Left ("empty trace with program " <> show other, []) +match ϕ δ s trace@(a : as) = \case + Empty -> Left ("program should terminate", trace) + Prog b -> + case (δ a s, δ b s) of + (Just t, Just t') + | t == t' -> Right (t', as) + _other -> + Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace) + Seq p q -> do + (s', trace') <- match ϕ δ s trace p + match ϕ δ s' trace' q + Alt p q -> + case match ϕ δ s trace p of + Right v -> Right v + Left{} -> match ϕ δ s trace q + Star p' -> + case match ϕ δ s trace p' of + Right (s', trace') -> match ϕ δ s' trace' (Star p') + Left{} -> Right (s, trace) + Test f -> + case satisfy ϕ δ s f trace of + One -> Right (s, trace) + _other -> Left ("test failed", trace) + +isSatisfiable + :: (Show p, Eq s, Show f, Eq f, Eq p, Test.QuickCheck.Arbitrary p) + => (f -> s -> Bool) + -- ^ The atomic propositions truth value + -> (p -> s -> Maybe s) + -- ^ Transition relation + -> s + -- ^ Initial state + -> Test.QuickCheck.Gen [p] + -- ^ A generator of traces from `s` + -> Prop f p + -- ^ A formula to check + -> Test.QuickCheck.Property +isSatisfiable ϕ δ i gen f = + Test.QuickCheck.forAllShrink gen Test.QuickCheck.shrink $ \trace -> + satisfy ϕ δ i f trace Test.QuickCheck.=== One From 96c3c8c70ea7c4f7e9299d2f207759ed0365b2df Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 1 Apr 2024 12:45:10 +0200 Subject: [PATCH 07/13] Rename functions and give semantics in terms of relations --- quickcheck-dynamic/src/Test/QuickCheck/DL.hs | 63 +++++++++++--------- 1 file changed, 36 insertions(+), 27 deletions(-) diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DL.hs b/quickcheck-dynamic/src/Test/QuickCheck/DL.hs index ce084cf..0aed1b4 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/DL.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/DL.hs @@ -1,7 +1,10 @@ +{-# LANGUAGE FunctionalDependencies #-} + module Test.QuickCheck.DL where import Control.Applicative ((<|>)) import Control.Monad (foldM) +import Data.Kind (Type) import Test.QuickCheck ( Arbitrary (..), Gen, @@ -59,18 +62,19 @@ data Prog f p where step :: (f -> s -> Bool) -- ^ A function to evaluate atomic formulas - -> (p -> s -> Maybe s) - -- ^ State transition + -> (p -> s -> [s]) + -- ^ State transition relation -> Int -- ^ Size limit (?) -> Prog f p -- ^ Program to interpret -> s -- ^ state - -> Maybe s + -> [s] +step _ _ 0 _ _ = [] step ϕ δ k prog s = case prog of - Empty -> Just s + Empty -> [s] Prog p -> δ p s Seq p q -> do s' <- step ϕ δ k p s @@ -78,17 +82,20 @@ step ϕ δ k prog s = Alt p q -> do step ϕ δ k p s <|> step ϕ δ k q s Test f -> - if eval ϕ δ (k - 1) f s - then Just s - else Nothing + [s | satisfy ϕ δ (k - 1) f s] Star p -> foldM (flip $ step ϕ δ (k - 1)) s (replicate k p) -eval +-- | Satisfiability of a given formula in `Prop f p` in a given state `s` against +-- a Kripke structure. +-- +-- The size limit `k` is needed to limit the length of `Star` expressions and +-- the depth of expression analyzed. +satisfy :: (f -> s -> Bool) -- ^ A function to evaluate atomic formulas - -> (p -> s -> Maybe s) - -- ^ Transition function for programs + -> (p -> s -> [s]) + -- ^ Transition relation for programs -> Int -- ^ Size limit (?) -> Prop f p @@ -96,17 +103,19 @@ eval -> s -- ^ Initial state -> Bool -eval ϕ δ k prop s = +satisfy ϕ δ k prop s = case prop of Prop f -> ϕ f s Zero -> False One -> True Imply f g -> - not (eval ϕ δ (k - 1) f s) || eval ϕ δ (k - 1) g s + not (satisfy ϕ δ (k - 1) f s) || satisfy ϕ δ (k - 1) g s Always p f -> case step ϕ δ k p s of - Nothing -> False - Just s' -> eval ϕ δ (k - 1) f s' + [] -> False + states -> all (satisfy ϕ δ (k - 1) f) states + +-- example from p.170 data S = U | V | W deriving (Eq, Show) @@ -122,15 +131,15 @@ type F = [S] phi :: F -> S -> Bool phi = flip elem -delta :: P -> S -> S +delta :: P -> S -> [S] delta A = \case - U -> V - W -> U - V -> W + U -> [V, W] + W -> [V] + V -> [W] --- | Tells whether or not a finite trace from some initial state --- satisfies the given formula. -satisfy +-- | Evaluates some `Prop`osition given some state `s` and a +-- finite /computation sequence/ `[p]`. +eval :: (Eq s, Show p, Show f) => (f -> s -> Bool) -- ^ A function to evaluate atomic formulas @@ -143,22 +152,22 @@ satisfy -> [p] -- ^ The trace to check satisfaction of proposition against -> Prop f p -satisfy ϕ δ s prop trace = +eval ϕ δ s prop trace = case prop of Prop f -> if ϕ f s then One else Zero Zero -> Zero One -> One Imply f g -> - let f' = satisfy ϕ δ s f trace - g' = satisfy ϕ δ s g trace + let f' = eval ϕ δ s f trace + g' = eval ϕ δ s g trace in case (f', g') of (Zero, _) -> One (One, One) -> One (_, _) -> Zero Always p f -> case match ϕ δ s trace p of - Right (s', trace') -> satisfy ϕ δ s' f trace' + Right (s', trace') -> eval ϕ δ s' f trace' Left{} -> Zero match @@ -193,7 +202,7 @@ match ϕ δ s trace@(a : as) = \case Right (s', trace') -> match ϕ δ s' trace' (Star p') Left{} -> Right (s, trace) Test f -> - case satisfy ϕ δ s f trace of + case eval ϕ δ s f trace of One -> Right (s, trace) _other -> Left ("test failed", trace) @@ -212,4 +221,4 @@ isSatisfiable -> Test.QuickCheck.Property isSatisfiable ϕ δ i gen f = Test.QuickCheck.forAllShrink gen Test.QuickCheck.shrink $ \trace -> - satisfy ϕ δ i f trace Test.QuickCheck.=== One + eval ϕ δ i f trace Test.QuickCheck.=== One From f0ade0c3dc0a122d22697141c665261c667be697 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 2 Apr 2024 08:39:16 +0200 Subject: [PATCH 08/13] Introduce docs sub-package to provide, well, documentation The idea is that some of the documentation will be in Literate haskell format and require some "building" to be generated. --- cabal.project | 1 + docs/CircularBuffer/Buffer.lhs | 66 ++++++++ docs/CircularBuffer/Model.lhs | 108 ++++++++++++ docs/DL.lhs | 295 +++++++++++++++++++++++++++++++++ docs/app/Main.hs | 6 + docs/docs.cabal | 86 ++++++++++ 6 files changed, 562 insertions(+) create mode 100644 docs/CircularBuffer/Buffer.lhs create mode 100644 docs/CircularBuffer/Model.lhs create mode 100644 docs/DL.lhs create mode 100644 docs/app/Main.hs create mode 100644 docs/docs.cabal diff --git a/cabal.project b/cabal.project index a68e429..13812e7 100644 --- a/cabal.project +++ b/cabal.project @@ -1,6 +1,7 @@ packages: quickcheck-dynamic quickcheck-dynamic-iosim + docs tests: true diff --git a/docs/CircularBuffer/Buffer.lhs b/docs/CircularBuffer/Buffer.lhs new file mode 100644 index 0000000..04cca9f --- /dev/null +++ b/docs/CircularBuffer/Buffer.lhs @@ -0,0 +1,66 @@ +> {-# LANGUAGE NamedFieldPuns #-} + +> -- | A Reasonably efficient version of a ring buffer. +> -- Directly stolen from [q-s-m](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs#L86) +> module CircularBuffer.Buffer where + +> import Data.Function (on) +> import Data.IORef (IORef, newIORef, readIORef, writeIORef) +> import Data.Vector.Unboxed.Mutable ( +> IOVector, +> ) +> import Data.Vector.Unboxed.Mutable qualified as V + +> -- | An efficient mutable circular buffer. +> data Buffer = Buffer +> { size :: Int +> -- ^ Size of buffer +> , inp :: IORef Int +> -- ^ Index to the next free slot where to 'Put' the next element +> , outp :: IORef Int +> -- ^ Index to the last occupied slot to 'Get' an element from +> , buf :: IOVector Int +> -- ^ Array of elements of fixed capacity +> } + +> -- | Different buffers are assumed to have disjoint memories, +> -- so we can use 'V.overlaps' to check equality. +> instance Eq Buffer where +> (==) = +> ((==) `on` inp) +> `also` ((==) `on` outp) +> `also` (V.overlaps `on` buf) +> where +> also = (liftA2 . liftA2) (&&) + +> -- | See 'New'. +> newBuffer :: Int -> IO Buffer +> newBuffer n = +> Buffer size +> <$> newIORef 0 +> <*> newIORef 0 +> <*> V.new size +> where +> size = n + 1 + +> -- | See 'Put'. +> putBuffer :: Int -> Buffer -> IO () +> putBuffer x Buffer{size, inp, buf} = do +> i <- readIORef inp +> V.write buf i x +> writeIORef inp $! (i + 1) `mod` size + +> -- | See 'Get'. +> getBuffer :: Buffer -> IO Int +> getBuffer Buffer{size, outp, buf} = do +> j <- readIORef outp +> y <- V.read buf j +> writeIORef outp $! (j + 1) `mod` size +> return y + +> -- | See 'Len'. +> lenBuffer :: Buffer -> IO Int +> lenBuffer Buffer{inp, outp, size} = do +> i <- readIORef inp +> j <- readIORef outp +> pure $ (i - j + size) `rem` size diff --git a/docs/CircularBuffer/Model.lhs b/docs/CircularBuffer/Model.lhs new file mode 100644 index 0000000..1ce9519 --- /dev/null +++ b/docs/CircularBuffer/Model.lhs @@ -0,0 +1,108 @@ +> {-# LANGUAGE InstanceSigs #-} +> {-# LANGUAGE NamedFieldPuns #-} +> {-# OPTIONS_GHC -Wno-incomplete-patterns #-} + +> -- | An classic example of model-checking an implementation of a ring buffer. +> -- +> -- * Inspired by [q-s-m example](https://github.com/stevana/quickcheck-state-machine/blob/master/test/CircularBuffer.hs) +> -- * Also described by John Hughes [here](https://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf) +> module CircularBuffer.Model where + +> import Control.Monad.State (MonadState (..), StateT) +> import Control.Monad.Trans (lift) +> import Data.Maybe (fromJust) +> import GHC.Generics (Generic) +> import CircularBuffer.Buffer (Buffer, getBuffer, lenBuffer, newBuffer, putBuffer) +> import Test.QuickCheck (Arbitrary (..), Property, getPositive, oneof) +> import Test.QuickCheck.DynamicLogic (DL, DynLogicModel (..), action, forAllDL) +> import Test.QuickCheck.Extras (runPropertyStateT) +> import Test.QuickCheck.Monadic (monadicIO) +> import Test.QuickCheck.Monadic qualified as QC +> import Test.QuickCheck.StateModel (Actions, Any (..), HasVariables (..), RunModel (..), StateModel (..), Var, counterexamplePost, runActions) + +> -- * Model + +> -- | A simple model of a `CircularBuffer` implemented using a `List`. +> data CircularBufferModel +> = NoBuffer +> | CircularBufferModel +> { size :: Int +> , buffer :: [Var Int] +> } +> deriving (Eq, Show, Generic) + +> instance StateModel CircularBufferModel where +> data Action CircularBufferModel a where +> -- Create new buffer of given capacity. +> New :: Int -> Action CircularBufferModel () +> -- Put an element at the top of the buffer. +> Put :: Int -> Action CircularBufferModel Int +> -- Get an element out of the bottom of the buffer. +> Get :: Action CircularBufferModel Int +> -- Get the number of elements in the buffer. +> Len :: Action CircularBufferModel Int + +> arbitraryAction ctx NoBuffer = Some . New . getPositive <$> arbitrary +> arbitraryAction ctx CircularBufferModel{} = +> oneof +> [ Some . Put <$> arbitrary +> , pure $ Some Get +> , pure $ Some Len +> ] + +> initialState = NoBuffer + +> precondition NoBuffer New{} = True +> precondition CircularBufferModel{buffer} Get{} = length buffer > 0 +> precondition CircularBufferModel{buffer, size} Put{} = length buffer < size +> precondition CircularBufferModel{} Len{} = True +> precondition _ _ = False + +> nextState NoBuffer (New size) var = CircularBufferModel{size, buffer = mempty} +> nextState buf@CircularBufferModel{size, buffer} Put{} var = buf{buffer = var : buffer} +> nextState buf@CircularBufferModel{buffer} Get _ = buf{buffer = init buffer} +> nextState st _ _ = st + +> shrinkAction _ _ = \case +> New n -> Some . New <$> [i | i <- shrink n, i > 0] +> Put n -> Some . Put <$> shrink n +> _ -> [] + +> deriving instance Show (Action CircularBufferModel a) +> deriving instance Eq (Action CircularBufferModel a) + +> instance HasVariables (Action CircularBufferModel a) where +> getAllVariables = const mempty + +> instance DynLogicModel CircularBufferModel where +> restricted _ = False + +> -- * RunModel + +> instance RunModel CircularBufferModel (StateT (Maybe Buffer) IO) where +> perform _st action _lookup = +> case action of +> New n -> lift (newBuffer n) >>= put . Just +> Put v -> get >>= (lift . putBuffer v . fromJust) >> pure v +> Get -> get >>= lift . getBuffer . fromJust +> Len -> get >>= lift . lenBuffer . fromJust + +> postcondition (CircularBufferModel{buffer}, after) Get lookup res = +> let v = lookup (last buffer) +> in do +> counterexamplePost ("Expected: " <> show v <> ", got: " <> show res) +> pure $ v == res +> postcondition (CircularBufferModel{buffer}, after) Len lookup res = do +> let len = length buffer +> counterexamplePost $ "Expected; " <> show len <> ", got: " <> show res +> pure $ res == len +> postcondition _ _ _ _ = pure True + +> prop_CircularBuffer :: Actions CircularBufferModel -> Property +> prop_CircularBuffer s = +> monadicIO $ do +> runPropertyStateT (runActions @_ @(StateT (Maybe Buffer) IO) s) Nothing +> QC.assert True + +> propDL :: DL CircularBufferModel () -> Property +> propDL d = forAllDL d prop_CircularBuffer diff --git a/docs/DL.lhs b/docs/DL.lhs new file mode 100644 index 0000000..f6815eb --- /dev/null +++ b/docs/DL.lhs @@ -0,0 +1,295 @@ +--- +title: Dynamic Logic +--- + +> {-# LANGUAGE FunctionalDependencies #-} +> {-# LANGUAGE InstanceSigs #-} + +> module DL where + +> import Control.Applicative ((<|>)) +> import Control.Monad (foldM) +> import Data.Kind (Type) +> import Test.QuickCheck ( +> Arbitrary (..), +> Gen, +> Property, +> forAllShrink, +> (===), +> ) + += Propositional Dynamic Logic + +This follows the presentation from the book [Dynamic +Logic](https://mitpress.mit.edu/9780262527668/dynamic-logic/) by +Harel, Kozen and Tiuryn, in particular from p.164 on. Those [lecture +notes](https://www.cs.cmu.edu/~fp/courses/15816-s10/lectures/19-PDL.pdf) +have also been useful when preparing these notes. + +== Syntax + +=== Propositions + +This is the `Prop`ositional logic part of _Dynamic Logic_. This type is +parameterised by the type of atomic propositions and atomic programs, +whose semantics is given by a Kripke structure. + +> data Prop f p where + +Atomic propositions are drawn from the type `f`. + +> Prop :: f -> Prop f p + +False and true are propositions. Note that `One` is not strictly necessary but has been added for convenience purpose. + +> Zero :: Prop f p +> One :: Prop f p + + +The main logical combinator is implication. It's well known that it's +possible to reconstruct disjunction and conjunctions from implication. + +> Imply :: Prop f p -> Prop f p -> Prop f p + +The most interesting operator is the modal _necessity_ operator which +informally states that some `Prop`osition must _always_ hold after the +execution of some `Prog`ram. The dual operator, _possibility_, which +states some proposition can hold after some program, could be derived +but is impractical to work with in the context of test case +generations and verification. + +> Always :: Prog f p -> Prop f p -> Prop f p +> deriving (Eq, Show) + +=== Programs + +`Prog`rams are what makes the Dynamic Logic a modal logic, +obviously. This type is also parameterised by atomic propositions `f` +and atomic programs (aka. _actions_) `p`. + +> data Prog f p where + +The empty program, also called _skip_ or represented by the $\emptyset$ symbol, represents termination of a +program execution. We could also define `Abort` or divergence to +represent non-termination or invalid execution. + +> Empty :: Prog f p + +Every atomic program `p` is of course a program. + +> Prog :: p -> Prog f p + +Programs can be run in _sequence_, one after another + +> Seq :: Prog f p -> Prog f p -> Prog f p + +Or one or the other can be run, non deterministically. + +> Alt :: Prog f p -> Prog f p -> Prog f p + +Programs can also be repeated, indefinitely, using an analog to the Kleene star from regular lagnauges. + +> Star :: Prog f p -> Prog f p + +Finally, a program can be a _test_ which does not change the state of +the system but either yields _skip_ or _abort_ depending on the result +of evaluating the given proposition. + +> Test :: Prop f p -> Prog f p +> deriving (Eq, Show) + +=== Deriving constructs + +Standard constructs from imperative programming can be define from the basic combinators, like `if/then/else` or `while` instructions: + +> ifThenElse :: Prop f p -> Prog f p -> Prog f p -> Prog f p +> ifThenElse cond ifTrue ifFalse = +> Alt (Seq (Test cond) ifTrue) +> (Seq (Test (Imply cond Zero)) ifFalse) + +== Semantics + +The semantics of Dynamic Logic formulas is given by a _Kripke_ structure $K = (W, \phi, \delta)$ + +> class Kripke m w | w -> m where +> type Formula w :: Type +> type Program w :: Type + +with $\phi$ giving an interpretation of atomic propositions as a subset of +$W$. Note that this subset is here defined through a characteristic +function `w -> Bool`. + +> ϕ :: Formula w -> w -> Bool + +And $\delta$ giving an interpretation of atomic programs. The usual +presentation is to consider $\delta$ as a relation over $W$, by making +the computation monadic we provide some flexibility of interpretation: +A function is `m = Identity`, a partial function if `m = Maybe`, a +relation if `m = [w]` or anything else. + +> δ :: Program w -> w -> m w + +=== Satisfiability + +> -- | Satisfiability of a given formula in `Prop f p` in a given state `s` against +> -- a Kripke structure. +> -- +> -- The size limit `k` is needed to limit the length of `Star` expressions and +> -- the depth of expression analyzed. +> satisfy +> :: Kripke [] s +> => Int +> -- ^ Size limit (?) +> -> Prop (Formula s) (Program s) +> -- ^ The proposition to evaluate +> -> s +> -- ^ Initial state +> -> Bool +> satisfy k prop s = +> case prop of +> Prop f -> ϕ f s +> Zero -> False +> One -> True +> Imply f g -> +> not (satisfy (k - 1) f s) || satisfy (k - 1) g s +> Always p f -> +> case step k p s of +> [] -> False +> states -> all (satisfy (k - 1) f) states + +> step +> :: Kripke [] s +> => Int +> -- ^ Size limit (?) +> -> Prog (Formula s) (Program s) +> -- ^ Program to interpret +> -> s +> -- ^ state +> -> [s] +> step 0 _ _ = [] +> step k prog s = +> case prog of +> Empty -> [s] +> Prog p -> δ p s +> Seq p q -> do +> s' <- step k p s +> step k q s' +> Alt p q -> do +> step k p s <|> step k q s +> Test f -> +> [s | satisfy (k - 1) f s] +> Star p -> +> foldM (flip $ step (k - 1)) s (replicate k p) + + +> -- example from p.170 + +> data S = U | V | W +> deriving (Eq, Show) + +> data P = A +> deriving (Eq, Show) + +> type F = [S] + +> instance Kripke [] S where +> type Formula S = F +> type Program S = P + +> ϕ :: F -> S -> Bool +> ϕ = flip elem + +> δ :: P -> S -> [S] +> δ A = \case +> U -> [V, W] +> W -> [V] +> V -> [W] + +> instance Test.QuickCheck.Arbitrary P where +> arbitrary = pure A + +> -- | Evaluates some `Prop`osition given some state `s` and a +> -- finite /computation sequence/ `[p]`. +> eval +> :: (Eq s, Show p, Show f) +> => (f -> s -> Bool) +> -- ^ A function to evaluate atomic formulas +> -> (p -> s -> Maybe s) +> -- ^ Partial transition function for programs +> -> s +> -- ^ Initial state +> -> Prop f p +> -- ^ The proposition to evaluate +> -> [p] +> -- ^ The trace to check satisfaction of proposition against +> -> Prop f p +> eval ϕ δ s prop trace = +> case prop of +> Prop f -> +> if ϕ f s then One else Zero +> Zero -> Zero +> One -> One +> Imply f g -> +> let f' = eval ϕ δ s f trace +> g' = eval ϕ δ s g trace +> in case (f', g') of +> (Zero, _) -> One +> (One, One) -> One +> (_, _) -> Zero +> Always p f -> +> case match ϕ δ s trace p of +> Right (s', trace') -> eval ϕ δ s' f trace' +> Left{} -> Zero + +> match +> :: (Show p, Eq s, Show f) +> => (f -> s -> Bool) +> -> (p -> s -> Maybe s) +> -> s +> -> [p] +> -> Prog f p +> -> Either (String, [p]) (s, [p]) +> match _ _ s [] = \case +> Empty -> Right (s, []) +> Star{} -> Right (s, []) +> other -> Left ("empty trace with program " <> show other, []) +> match ϕ δ s trace@(a : as) = \case +> Empty -> Left ("program should terminate", trace) +> Prog b -> +> case (δ a s, δ b s) of +> (Just t, Just t') +> | t == t' -> Right (t', as) +> _other -> +> Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace) +> Seq p q -> do +> (s', trace') <- match ϕ δ s trace p +> match ϕ δ s' trace' q +> Alt p q -> +> case match ϕ δ s trace p of +> Right v -> Right v +> Left{} -> match ϕ δ s trace q +> Star p' -> +> case match ϕ δ s trace p' of +> Right (s', trace') -> match ϕ δ s' trace' (Star p') +> Left{} -> Right (s, trace) +> Test f -> +> case eval ϕ δ s f trace of +> One -> Right (s, trace) +> _other -> Left ("test failed", trace) + +> isSatisfiable +> :: (Show p, Eq s, Show f, Eq f, Eq p, Test.QuickCheck.Arbitrary p) +> => (f -> s -> Bool) +> -- ^ The atomic propositions truth value +> -> (p -> s -> Maybe s) +> -- ^ Transition relation +> -> s +> -- ^ Initial state +> -> Test.QuickCheck.Gen [p] +> -- ^ A generator of traces from `s` +> -> Prop f p +> -- ^ A formula to check +> -> Test.QuickCheck.Property +> isSatisfiable ϕ δ i gen f = +> Test.QuickCheck.forAllShrink gen Test.QuickCheck.shrink $ \trace -> +> eval ϕ δ i f trace Test.QuickCheck.=== One diff --git a/docs/app/Main.hs b/docs/app/Main.hs new file mode 100644 index 0000000..e1de72f --- /dev/null +++ b/docs/app/Main.hs @@ -0,0 +1,6 @@ +import CircularBuffer.Model (prop_CircularBuffer) +import Test.QuickCheck (quickCheck) + +main :: IO () +main = do + quickCheck prop_CircularBuffer diff --git a/docs/docs.cabal b/docs/docs.cabal new file mode 100644 index 0000000..a1f86f2 --- /dev/null +++ b/docs/docs.cabal @@ -0,0 +1,86 @@ +cabal-version: 2.2 +name: docs +version: 3.4.0 +license: Apache-2.0 +license-files: + LICENSE + NOTICE + +maintainer: arnaud.bailly@iohk.io +author: Ulf Norell +category: Testing +synopsis: Documentation for quickcheck-dynamic +homepage: + https://input-output-hk.github.com/quickcheck-dynamic + +bug-reports: + https://github.com/input-output-hk/quickcheck-dynamic/issues + +build-type: Simple + +source-repository head + type: git + location: https://github.com/input-output-hk/quickcheck-dynamic + +common lang + default-language: Haskell2010 + default-extensions: + ConstraintKinds + DataKinds + DefaultSignatures + DeriveDataTypeable + DeriveFoldable + DeriveFunctor + DeriveGeneric + DeriveTraversable + DerivingVia + FlexibleContexts + FlexibleInstances + GADTs + GeneralizedNewtypeDeriving + ImportQualifiedPost + LambdaCase + MultiParamTypeClasses + MultiWayIf + PatternSynonyms + QuantifiedConstraints + RankNTypes + ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeApplications + TypeFamilies + TypeOperators + ViewPatterns + + ghc-options: + -Wall -Wnoncanonical-monad-instances -Wunused-packages + -Wincomplete-uni-patterns -Wincomplete-record-updates + -Wredundant-constraints -Widentities -Wno-unused-do-bind + +library + import: lang + hs-source-dirs: . + exposed-modules: + DL + , CircularBuffer.Model + , CircularBuffer.Buffer + build-depends: + , base >=4.7 && <5 + , containers + , mtl + , QuickCheck + , quickcheck-dynamic + , random + , vector + +executable docs + import: lang + hs-source-dirs: app + main-is: Main.hs + build-depends: + , base >=4.7 && <5 + , containers + , docs + , mtl + , QuickCheck From 3ec35175632ca7c63f901a625051a5ed9dad889b Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 2 Apr 2024 11:46:54 +0200 Subject: [PATCH 09/13] Remove old DL file --- quickcheck-dynamic/src/Test/QuickCheck/DL.hs | 224 ------------------- 1 file changed, 224 deletions(-) delete mode 100644 quickcheck-dynamic/src/Test/QuickCheck/DL.hs diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DL.hs b/quickcheck-dynamic/src/Test/QuickCheck/DL.hs deleted file mode 100644 index 0aed1b4..0000000 --- a/quickcheck-dynamic/src/Test/QuickCheck/DL.hs +++ /dev/null @@ -1,224 +0,0 @@ -{-# LANGUAGE FunctionalDependencies #-} - -module Test.QuickCheck.DL where - -import Control.Applicative ((<|>)) -import Control.Monad (foldM) -import Data.Kind (Type) -import Test.QuickCheck ( - Arbitrary (..), - Gen, - Property, - forAllShrink, - (===), - ) - --- Definition of Propositional Dynamic Logic --- p.164 --- f and p are atomic formulas and propositions respectively --- See also these - --- | `Prop`ositional logic part of Dynamic Logic. --- This type is parameterised by the type of atomic propositions and atomic programs, whose --- semantics is given by a Kripke structure. -data Prop f p where - -- | Atomic propositions - Prop :: f -> Prop f p - -- | Falsity - Zero :: Prop f p - -- | Truth - One :: Prop f p - -- | Basic logic combinator. - -- - -- Classically it's possible to reconstruct all the other usual - -- combinators from implication and falsity. - Imply :: Prop f p -> Prop f p -> Prop f p - -- | Necessity modality - -- - -- This is the only modality in this presentation as /possibility/ - -- is cumbersome to implement. - Always :: Prog f p -> Prop f p -> Prop f p - deriving (Eq, Show) - --- | `Prog`ams part of Dynamic Logic. --- --- This type is parameterised by the type of atomic propositions and atomic programs, whose --- semantics is typically given by a Kripke structure. -data Prog f p where - -- | Empty program, or /Stop/. - Empty :: Prog f p - -- | Atomic programs. - Prog :: p -> Prog f p - -- | Sequencing of programs. - Seq :: Prog f p -> Prog f p -> Prog f p - -- | Alternation of programs. - Alt :: Prog f p -> Prog f p -> Prog f p - -- | Unbounded repetition of programs. - Star :: Prog f p -> Prog f p - -- | Test of a `Prop`osition. - Test :: Prop f p -> Prog f p - deriving (Eq, Show) - -step - :: (f -> s -> Bool) - -- ^ A function to evaluate atomic formulas - -> (p -> s -> [s]) - -- ^ State transition relation - -> Int - -- ^ Size limit (?) - -> Prog f p - -- ^ Program to interpret - -> s - -- ^ state - -> [s] -step _ _ 0 _ _ = [] -step ϕ δ k prog s = - case prog of - Empty -> [s] - Prog p -> δ p s - Seq p q -> do - s' <- step ϕ δ k p s - step ϕ δ k q s' - Alt p q -> do - step ϕ δ k p s <|> step ϕ δ k q s - Test f -> - [s | satisfy ϕ δ (k - 1) f s] - Star p -> - foldM (flip $ step ϕ δ (k - 1)) s (replicate k p) - --- | Satisfiability of a given formula in `Prop f p` in a given state `s` against --- a Kripke structure. --- --- The size limit `k` is needed to limit the length of `Star` expressions and --- the depth of expression analyzed. -satisfy - :: (f -> s -> Bool) - -- ^ A function to evaluate atomic formulas - -> (p -> s -> [s]) - -- ^ Transition relation for programs - -> Int - -- ^ Size limit (?) - -> Prop f p - -- ^ The proposition to evaluate - -> s - -- ^ Initial state - -> Bool -satisfy ϕ δ k prop s = - case prop of - Prop f -> ϕ f s - Zero -> False - One -> True - Imply f g -> - not (satisfy ϕ δ (k - 1) f s) || satisfy ϕ δ (k - 1) g s - Always p f -> - case step ϕ δ k p s of - [] -> False - states -> all (satisfy ϕ δ (k - 1) f) states - --- example from p.170 - -data S = U | V | W - deriving (Eq, Show) - -data P = A - deriving (Eq, Show) - -instance Test.QuickCheck.Arbitrary P where - arbitrary = pure A - -type F = [S] - -phi :: F -> S -> Bool -phi = flip elem - -delta :: P -> S -> [S] -delta A = \case - U -> [V, W] - W -> [V] - V -> [W] - --- | Evaluates some `Prop`osition given some state `s` and a --- finite /computation sequence/ `[p]`. -eval - :: (Eq s, Show p, Show f) - => (f -> s -> Bool) - -- ^ A function to evaluate atomic formulas - -> (p -> s -> Maybe s) - -- ^ Partial transition function for programs - -> s - -- ^ Initial state - -> Prop f p - -- ^ The proposition to evaluate - -> [p] - -- ^ The trace to check satisfaction of proposition against - -> Prop f p -eval ϕ δ s prop trace = - case prop of - Prop f -> - if ϕ f s then One else Zero - Zero -> Zero - One -> One - Imply f g -> - let f' = eval ϕ δ s f trace - g' = eval ϕ δ s g trace - in case (f', g') of - (Zero, _) -> One - (One, One) -> One - (_, _) -> Zero - Always p f -> - case match ϕ δ s trace p of - Right (s', trace') -> eval ϕ δ s' f trace' - Left{} -> Zero - -match - :: (Show p, Eq s, Show f) - => (f -> s -> Bool) - -> (p -> s -> Maybe s) - -> s - -> [p] - -> Prog f p - -> Either (String, [p]) (s, [p]) -match _ _ s [] = \case - Empty -> Right (s, []) - Star{} -> Right (s, []) - other -> Left ("empty trace with program " <> show other, []) -match ϕ δ s trace@(a : as) = \case - Empty -> Left ("program should terminate", trace) - Prog b -> - case (δ a s, δ b s) of - (Just t, Just t') - | t == t' -> Right (t', as) - _other -> - Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace) - Seq p q -> do - (s', trace') <- match ϕ δ s trace p - match ϕ δ s' trace' q - Alt p q -> - case match ϕ δ s trace p of - Right v -> Right v - Left{} -> match ϕ δ s trace q - Star p' -> - case match ϕ δ s trace p' of - Right (s', trace') -> match ϕ δ s' trace' (Star p') - Left{} -> Right (s, trace) - Test f -> - case eval ϕ δ s f trace of - One -> Right (s, trace) - _other -> Left ("test failed", trace) - -isSatisfiable - :: (Show p, Eq s, Show f, Eq f, Eq p, Test.QuickCheck.Arbitrary p) - => (f -> s -> Bool) - -- ^ The atomic propositions truth value - -> (p -> s -> Maybe s) - -- ^ Transition relation - -> s - -- ^ Initial state - -> Test.QuickCheck.Gen [p] - -- ^ A generator of traces from `s` - -> Prop f p - -- ^ A formula to check - -> Test.QuickCheck.Property -isSatisfiable ϕ δ i gen f = - Test.QuickCheck.forAllShrink gen Test.QuickCheck.shrink $ \trace -> - eval ϕ δ i f trace Test.QuickCheck.=== One From 877bf9a715e524b7b27c30680a0f328e633a4046 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 2 Apr 2024 19:25:20 +0200 Subject: [PATCH 10/13] Complete first part --- docs/DL.html | 676 ++++++++++++++++++++ docs/DL.lhs | 307 +++++++-- quickcheck-dynamic/quickcheck-dynamic.cabal | 1 - 3 files changed, 915 insertions(+), 69 deletions(-) create mode 100644 docs/DL.html diff --git a/docs/DL.html b/docs/DL.html new file mode 100644 index 0000000..d2c9e24 --- /dev/null +++ b/docs/DL.html @@ -0,0 +1,676 @@ + + + + + + + DL + + + +
{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE InstanceSigs #-}
+
module DL where
+
import Debug.Trace as Debug
+import Control.Applicative ((<|>))
+import Control.Monad (foldM)
+import Data.Kind (Type)
+import Test.QuickCheck (
+  Arbitrary (..),
+  Gen,
+  Property,
+  forAllShrink,
+  (===),
+ )
+

Propositional Dynamic Logic

+

This follows the presentation from the book Dynamic +Logic by Harel, Kozen and Tiuryn, in particular from p.164 on. Those +lecture +notes have also been useful when preparing these notes.

+

Syntax

+

Propositions

+

This is the Propositional logic part of Dynamic +Logic. This type is parameterised by the type of atomic +propositions and atomic programs, whose semantics is given by a Kripke +structure.

+
data Prop f p where
+

Atomic propositions are drawn from the type f.

+
  Prop :: f -> Prop f p
+

False and true are propositions. Note that One is not +strictly necessary but has been added for convenience purpose.

+
  Zero :: Prop f p
+  One :: Prop f p
+

The main logical combinator is implication. It’s well known that it’s +possible to reconstruct disjunction and conjunctions from +implication.

+
  Imply :: Prop f p -> Prop f p -> Prop f p
+

The most interesting operator is the modal necessity +operator which informally states that some Proposition must +always hold after the execution of some Program. +The dual operator, possibility, which states some proposition +can hold after some program, could be derived but is impractical to work +with in the context of test case generations and verification.

+
  Always :: Prog f p -> Prop f p -> Prop f p
+  deriving (Eq, Show)
+

Programs

+

Programs are what makes the Dynamic Logic a modal logic, +obviously. This type is also parameterised by atomic propositions +f and atomic programs (aka. actions) +p.

+
data Prog f p where
+

The empty program, also called skip or represented by the +∅ symbol, represents termination of a +program execution. We could also define Abort or divergence +to represent non-termination or invalid execution.

+
  Empty :: Prog f p
+

Every atomic program p is of course a program.

+
  Prog :: p -> Prog f p
+

Programs can be run in sequence, one after another

+
  Seq :: Prog f p -> Prog f p -> Prog f p
+

Or one or the other can be run, non deterministically.

+
  Alt :: Prog f p -> Prog f p -> Prog f p
+

Programs can also be repeated, indefinitely, using an analog to the +Kleene star from regular lagnauges.

+
  Star :: Prog f p -> Prog f p
+

Finally, a program can be a test which does not change the +state of the system but either yields skip or abort +depending on the result of evaluating the given proposition.

+
  Test :: Prop f p -> Prog f p
+  deriving (Eq, Show)
+

Deriving constructs

+

Standard constructs from imperative programming can be define from +the basic combinators, like if/then/else or +while instructions:

+
ifThenElse :: Prop f p -> Prog f p -> Prog f p -> Prog f p
+ifThenElse cond ifTrue ifFalse =
+  Alt (Seq (Test cond) ifTrue)
+      (Seq (Test (Imply cond Zero)) ifFalse)
+

Semantics

+

The semantics of Dynamic Logic formulas is given by a Kripke +structure K = (W,ϕ,δ)

+
class Kripke m w | w -> m where
+  type Formula w :: Type
+  type Program w :: Type
+

with ϕ giving an +interpretation of atomic propositions as a subset of W. Note that this subset is here +defined through a characteristic function w -> Bool.

+
  ϕ :: Formula w -> w -> Bool
+

And δ giving an +interpretation of atomic programs. The usual presentation is to consider +δ as a relation over W, by making the computation monadic +we provide some flexibility of interpretation: A function is +m = Identity, a partial function if m = Maybe, +a relation if m = [w] or anything else.

+
  δ :: Program w -> w -> m w
+

Satisfiability

+

Given some Kripke structure K, a formula f is +satisfied in a state s denoted as K, s ⊨ f if the +formula is true in the state s, which is defined +inductively over the structure of f.

+

Note that we need to limit the size of the formula to avoid infinite +recursion.

+
satisfy
+

Note that satisfy is defined here with atomic programs +defining relations over s and not functions, eg. a +given program p can have multiple possible state +outcomes.

+
  :: Kripke [] s
+

The size parameter bounds the depth at which state is explored and +the formula is evaluated.

+
  => Int
+

The formula to evaluate, f is a proposition dependent on +the atomic propositions and programs in K.

+
  -> Prop (Formula s) (Program s)
+

The state in which to evaluate the formula.

+
  -> s
+  -> Bool
+satisfy k prop s =
+  case prop of
+

Atomic propositions are evaluated by the characteristic function +ϕ.

+
    Prop f -> ϕ f s
+

False, true, and implications are evaluated as expected for +propositional logic operators.

+
    Zero -> False
+    One -> True
+    Imply f g ->
+      not (satisfy (k - 1) f s) || satisfy (k - 1) g s
+

The always operator is evaluated by checking that the +proposition holds in all the states reachable from the current +state by executing the program p.

+
    Always p f ->
+      case step k p s of
+        [] -> False
+        states -> all (satisfy (k - 1) f) states
+

The step function computes the set of states reachable +from the current state by executing the program p.

+
step
+  :: Kripke [] s
+  => Int
+  -> Prog (Formula s) (Program s)
+  -> s
+  -> [s]
+

If the size limit is reached, the computation is considered “stuck” +and yields no reachable state.

+
step 0 _ _ = []
+

In other cases, reachable states are defined inductively over the +structure of the program.

+
step k prog s =
+  case prog of
+

If program should stop, simply return the current state.

+
    Empty -> [s]
+

Atomic programs yield the result of the transition relation δ.

+
    Prog p -> δ p s
+

Sequencing of programs is done by executing the first program and +then the second program on the resulting state(s).

+
    Seq p q -> do
+      s' <- step k p s
+      step k q s'
+

Non-deterministic choice is done by executing either the first or the +second program, with a bias towards the first program.

+
    Alt p q -> do
+      step k p s <|> step k q s
+

Test programs are executed by checking if the proposition holds in +the current state and returning the current state if it does.

+
    Test f ->
+      [s | satisfy (k - 1) f s]
+

Finally, repetition of a program is done by iterating over the nested +program k times.

+
    Star p ->
+      foldM (flip $ step (k - 1)) s (replicate k p)
+

A “concrete” Example

+

The following is a concrete example of some simple data types and +Kripke structure to evaluate the satisfaction of a formula, drawn from +p.170 of the book.

+

The system’s state is simply an enumeration of 3 different +states.

+
data S = U | V | W
+  deriving (Eq, Show)
+

There’s a single atomic program, A.

+
data P = A
+  deriving (Eq, Show)
+

The atomic propositions are simply a list of states and a proposition +is true iff reached state is included in the list.

+
type F = [S]
+
instance Kripke [] S where
+  type Formula S = F
+  type Program S = P
+
  ϕ :: F -> S -> Bool
+  ϕ = flip elem
+

The transition relation is the only interesting part of the Kripke +structure.

+
  δ :: P -> S -> [S]
+  δ A = \case
+    U -> [V, W]
+    W -> [V]
+    V -> [W]
+

Now, let’s define a simple formula to check if the state +V is reachable from the state U after +executing the program A.

+
formula :: Prop F P
+formula = Always (Star (Prog A)) (Prop [V,W])
+

We can now check if the formula is satisfied in the state +U of the Kripke structure defined above within GHCi:

+
$ satisfy 10 formula U
+True
+

Property-Based Testing

+

Another way to look at the semantics of Dynamic Logic is to consider +it in the context of traces, that is finite sequences of programs. Here +formula’s meaning is the set of traces that satisfy the formula. This is +particularly useful in the context of property-based testing: Given some +Kripke structure and generators, we can generate traces and check if all +traces satisfy a given formula.

+

Checking satisfiability

+

The basic property we want to check is the satisfiability of some +formula against arbitrary valid traces part of the Kripke structure. In +other words, we want to explore the states of the Kripke structure that +are reachable throughsome sequence of execution of programs, and check +if the formula holds for all of them.

+
isSatisfiable
+  :: ( Eq s, Show s
+     , Eq (Formula s), Show (Formula s)
+     , Eq (Program s), Show (Program s)
+     , Test.QuickCheck.Arbitrary (Program s)
+     , Kripke Maybe s)
+

Given some initial state,

+
   => s
+

A generator for traces,

+
   -> (s -> Test.QuickCheck.Gen [Program s])
+

and a formula to check,

+
   -> Prop (Formula s) (Program s)
+   -> Test.QuickCheck.Property
+isSatisfiable i gen f =
+  Test.QuickCheck.forAllShrink (gen i) Test.QuickCheck.shrink $ \trace ->
+

It should hold that the formula evaluates to True given +the trace and the initial state.

+
    eval i f trace Test.QuickCheck.=== One
+

To do so, we need to evaluate a formula in a given state +against some trace, yielding a simpler formula until we reach atomic +propositions or ground truths.

+
eval
+  :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s))
+   => s
+   -> Prop (Formula s) (Program s)
+   -> [Program s]
+   -> Prop (Formula s) (Program s)
+eval s prop trace =
+

Evaluation proceeds recursively over the structure of the formula and +the trace.

+
  case prop of
+

Atomic propositions should hold in the current state

+
    Prop f ->
+      if ϕ f s then One else Zero
+    Zero -> Zero
+    One -> One
+

Implications follow the usual rules of logic

+
    Imply f g ->
+      let f' = eval s f trace
+          g' = eval s g trace
+       in case (f', g') of
+            (Zero, _) -> One
+            (One, One) -> One
+            (_, _) -> Zero
+

The always operator requires advancing the state by +executing the program p and evaluating the formula +f in the resulting state, agains the resulting trace.

+
    Always p f ->
+      case match s trace p of
+        Right (s', trace') -> eval s' f trace'
+        Left{} -> Zero
+

The match function advances the state by executing the program +p:

+
match
+  :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s))
+   => s
+   -> [Program s]
+   -> Prog (Formula s) (Program s)
+

Note match can fail if the program is not executable in the current +state, in which case it returns some error message and the remaining +trace.

+
   -> Either (String, [Program s]) (s, [Program s])
+

The base case is when the trace is empty, in which case the program +should terminate which is only possible if the program is empty, or it +can be repeated indefinitely which includes the case where it’s not +repeated at all.

+
match s [] = \case
+  Empty -> Right (s, [])
+  Star{} -> Right (s, [])
+  other -> Left ("empty trace with program " <> show other, [])
+

If the trace is not empty, we need to inductively walk through the +trace and the program structure:

+
match s trace@(a : as) = \case
+  Empty -> Left ("program should terminate", trace)
+

For atomic programs, we could check equality of the atomic programs +and advance the state if they matched, but we choose instead to check +equality of observational behaviors of the programs, eg. +whether or not the two programs yield the same state:

+
  Prog b ->
+    case (δ a s, δ b s) of
+      (Just t, Just t')
+        | t == t' -> Right (t', as)
+      _other ->
+        Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace)
+

Sequential execution is straightforward, simply feeding the new state +and trace to the next program

+
  Seq p q -> do
+    (s', trace') <- match s trace p
+    match s' trace' q
+

Non-deterministic choice is also straightforward, trying to match the +first program and if it fails, trying the second program. Note that we +cannot here use the Alternative operator +(<|>) as Either e is, somewhat +surprisingly in the case of an “error” monad, not an instance of +Alternative.

+
  Alt p q ->
+    case match s trace p of
+      Right v -> Right v
+      Left{} -> match s trace q
+

Repetition is also quite simple and terminates because the base case +(Prog p) consumes the head of the trace.

+
  Star p' ->
+    case match s trace p' of
+      Right (s', trace') -> match s' trace' (Star p')
+      Left{} -> Right (s, trace)
+

Finally, we can Test a formula whose result depends on +call to eval with current state and trace.

+
  Test f ->
+    case eval s f trace of
+      One -> Right (s, trace)
+      _other -> Left ("test failed", trace)
+

Example

+

The generator for our simple model is quite simple as there’s a +single action.

+
instance Test.QuickCheck.Arbitrary P where
+  arbitrary = pure A
+

However we need a different Kripke structure because we want it to +work in the Maybe monad, so let’s wrap S and +create the structure:

+
newtype S' = S' { unS :: S }
+  deriving (Eq, Show)
+
instance Kripke Maybe S' where
+  type Formula S' = F
+  type Program S' = P
+
  ϕ f = ϕ f . unS
+
  δ A = \case
+    S' U -> Just $ S' W
+    S' V -> Just $ S' W
+    S' W -> Just $ S' V
+

Then we can run QuickCheck over our example formula:

+
$ quickCheck $ isSatisfiable (S' U)  (const arbitrary) formula
+*** Failed! Falsified (after 1 test):
+[]
+Zero /= One
+

Of course, the formula is wrong on an empty sequence of actions as we +are in state U, but if we start from state V +we can verify the property holds:

+
quickCheck $ isSatisfiable (S' V)  (const arbitrary) formula
++++ OK, passed 100 tests.
+

Generating valid traces

+

In practice, what we are interested in with Dynamic Logic formulas is +rather the converse of what we have done so far: Inferring the subset of +Kripke structure that’s a model for a given formula, for a given +“universe of discourse” consisting of the atomic propositions and +programs.

+ + diff --git a/docs/DL.lhs b/docs/DL.lhs index f6815eb..f822bb5 100644 --- a/docs/DL.lhs +++ b/docs/DL.lhs @@ -1,12 +1,10 @@ ---- -title: Dynamic Logic ---- > {-# LANGUAGE FunctionalDependencies #-} > {-# LANGUAGE InstanceSigs #-} > module DL where +> import Debug.Trace as Debug > import Control.Applicative ((<|>)) > import Control.Monad (foldM) > import Data.Kind (Type) @@ -131,67 +129,121 @@ relation if `m = [w]` or anything else. === Satisfiability -> -- | Satisfiability of a given formula in `Prop f p` in a given state `s` against -> -- a Kripke structure. -> -- -> -- The size limit `k` is needed to limit the length of `Star` expressions and -> -- the depth of expression analyzed. +Given some Kripke structure $K$, a formula `f` is _satisfied_ in a +state `s` denoted as $K, s\models f$ if the formula is true in the +state `s`, which is defined inductively over the structure of `f`. + +Note that we need to limit the size of the formula to avoid infinite recursion. + > satisfy + +Note that `satisfy` is defined here with atomic programs defining _relations_ over `s` and not functions, eg. a given program `p` can have multiple possible state outcomes. + > :: Kripke [] s + +The size parameter bounds the depth at which state is explored and the formula is evaluated. + > => Int -> -- ^ Size limit (?) + +The formula to evaluate, `f` is a proposition dependent on the atomic propositions and programs in $K$. + > -> Prop (Formula s) (Program s) -> -- ^ The proposition to evaluate + +The state in which to evaluate the formula. + > -> s -> -- ^ Initial state > -> Bool > satisfy k prop s = > case prop of + +Atomic propositions are evaluated by the characteristic function $\phi$. + > Prop f -> ϕ f s + +False, true, and implications are evaluated as expected for propositional logic operators. + > Zero -> False > One -> True > Imply f g -> > not (satisfy (k - 1) f s) || satisfy (k - 1) g s + +The _always_ operator is evaluated by checking that the proposition +holds in _all_ the states reachable from the current state by +executing the program `p`. + > Always p f -> > case step k p s of > [] -> False > states -> all (satisfy (k - 1) f) states +The `step` function computes the set of states reachable from the current state by executing the program `p`. + > step > :: Kripke [] s > => Int -> -- ^ Size limit (?) > -> Prog (Formula s) (Program s) -> -- ^ Program to interpret > -> s -> -- ^ state > -> [s] + +If the size limit is reached, the computation is considered "stuck" and yields no reachable state. + > step 0 _ _ = [] + +In other cases, reachable states are defined inductively over the structure of the program. + > step k prog s = > case prog of + +If program should stop, simply return the current state. + > Empty -> [s] + +Atomic programs yield the result of the transition relation $\delta$. + > Prog p -> δ p s + +Sequencing of programs is done by executing the first program and then the second program on the resulting state(s). + > Seq p q -> do > s' <- step k p s > step k q s' + +Non-deterministic choice is done by executing either the first or the second program, with a bias towards the first program. + > Alt p q -> do > step k p s <|> step k q s + +Test programs are executed by checking if the proposition holds in the current state and returning the current state if it does. + > Test f -> > [s | satisfy (k - 1) f s] + +Finally, repetition of a program is done by iterating over the nested program `k` times. + > Star p -> > foldM (flip $ step (k - 1)) s (replicate k p) +=== A "concrete" Example -> -- example from p.170 +The following is a concrete example of some simple data types and +Kripke structure to evaluate the satisfaction of a formula, drawn from p.170 of the book. + +The system's state is simply an enumeration of 3 different states. > data S = U | V | W > deriving (Eq, Show) +There's a single atomic program, `A`. + > data P = A > deriving (Eq, Show) +The atomic propositions are simply a list of states and a proposition +is true iff reached state is included in the list. + > type F = [S] + > instance Kripke [] S where > type Formula S = F > type Program S = P @@ -199,97 +251,216 @@ relation if `m = [w]` or anything else. > ϕ :: F -> S -> Bool > ϕ = flip elem +The transition relation is the only interesting part of the Kripke structure. + > δ :: P -> S -> [S] > δ A = \case > U -> [V, W] > W -> [V] > V -> [W] -> instance Test.QuickCheck.Arbitrary P where -> arbitrary = pure A +Now, let's define a simple formula to check if the state `V` is reachable from the state `U` after executing the program `A`. + +> formula :: Prop F P +> formula = Always (Star (Prog A)) (Prop [V,W]) + +We can now check if the formula is satisfied in the state `U` of the Kripke structure defined above within GHCi: + +``` +$ satisfy 10 formula U +True +``` + += Property-Based Testing + +Another way to look at the semantics of Dynamic Logic is to consider it in the context of traces, that is finite sequences of programs. Here formula's meaning is the set of traces that satisfy the formula. +This is particularly useful in the context of property-based testing: Given some Kripke structure and generators, we can generate traces and check if all traces satisfy a given formula. + +== Checking satisfiability + +The basic property we want to check is the satisfiability of some +formula against arbitrary valid traces part of the Kripke +structure. In other words, we want to explore the states of the Kripke +structure that are reachable throughsome sequence of execution of +programs, and check if the formula holds for all of them. + +> isSatisfiable +> :: ( Eq s, Show s +> , Eq (Formula s), Show (Formula s) +> , Eq (Program s), Show (Program s) +> , Test.QuickCheck.Arbitrary (Program s) +> , Kripke Maybe s) + +Given some initial state, + +> => s + +A generator for traces, + +> -> (s -> Test.QuickCheck.Gen [Program s]) + +and a formula to check, + +> -> Prop (Formula s) (Program s) +> -> Test.QuickCheck.Property +> isSatisfiable i gen f = +> Test.QuickCheck.forAllShrink (gen i) Test.QuickCheck.shrink $ \trace -> + +It should hold that the formula evaluates to `True` given the trace and the initial state. + +> eval i f trace Test.QuickCheck.=== One + +To do so, we need to `eval`uate a formula in a given state against some trace, yielding a simpler formula until we reach atomic propositions or ground truths. -> -- | Evaluates some `Prop`osition given some state `s` and a -> -- finite /computation sequence/ `[p]`. > eval -> :: (Eq s, Show p, Show f) -> => (f -> s -> Bool) -> -- ^ A function to evaluate atomic formulas -> -> (p -> s -> Maybe s) -> -- ^ Partial transition function for programs -> -> s -> -- ^ Initial state -> -> Prop f p -> -- ^ The proposition to evaluate -> -> [p] -> -- ^ The trace to check satisfaction of proposition against -> -> Prop f p -> eval ϕ δ s prop trace = +> :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s)) +> => s +> -> Prop (Formula s) (Program s) +> -> [Program s] +> -> Prop (Formula s) (Program s) +> eval s prop trace = + +Evaluation proceeds recursively over the structure of the formula and the trace. + > case prop of + +Atomic propositions should hold in the current state + > Prop f -> > if ϕ f s then One else Zero > Zero -> Zero > One -> One + +Implications follow the usual rules of logic + > Imply f g -> -> let f' = eval ϕ δ s f trace -> g' = eval ϕ δ s g trace +> let f' = eval s f trace +> g' = eval s g trace > in case (f', g') of > (Zero, _) -> One > (One, One) -> One > (_, _) -> Zero + +The _always_ operator requires advancing the state by executing the +program `p` and evaluating the formula `f` in the resulting state, +agains the resulting trace. + > Always p f -> -> case match ϕ δ s trace p of -> Right (s', trace') -> eval ϕ δ s' f trace' +> case match s trace p of +> Right (s', trace') -> eval s' f trace' > Left{} -> Zero +The match function advances the state by executing the program `p`: + > match -> :: (Show p, Eq s, Show f) -> => (f -> s -> Bool) -> -> (p -> s -> Maybe s) -> -> s -> -> [p] -> -> Prog f p -> -> Either (String, [p]) (s, [p]) -> match _ _ s [] = \case +> :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s)) +> => s +> -> [Program s] +> -> Prog (Formula s) (Program s) + +Note match can fail if the program is not executable in the current +state, in which case it returns some error message and the remaining +trace. + +> -> Either (String, [Program s]) (s, [Program s]) + +The base case is when the trace is empty, in which case the program +should terminate which is only possible if the program is empty, or it +can be repeated indefinitely which includes the case where it's not +repeated at all. + +> match s [] = \case > Empty -> Right (s, []) > Star{} -> Right (s, []) > other -> Left ("empty trace with program " <> show other, []) -> match ϕ δ s trace@(a : as) = \case + +If the trace is not empty, we need to inductively walk through the trace and the program structure: + +> match s trace@(a : as) = \case > Empty -> Left ("program should terminate", trace) + +For atomic programs, we could check equality of the atomic programs and advance the state if they matched, but we choose instead to check equality of _observational behaviors_ of the programs, eg. whether or not the two programs yield the same state: + > Prog b -> > case (δ a s, δ b s) of > (Just t, Just t') > | t == t' -> Right (t', as) > _other -> > Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace) + +Sequential execution is straightforward, simply feeding the new state and trace to the next program + > Seq p q -> do -> (s', trace') <- match ϕ δ s trace p -> match ϕ δ s' trace' q +> (s', trace') <- match s trace p +> match s' trace' q + +Non-deterministic choice is also straightforward, trying to match the +first program and if it fails, trying the second program. Note that +we cannot here use the `Alternative` operator `(<|>)` as `Either e` +is, somewhat surprisingly in the case of an "error" monad, not an +instance of `Alternative`. + > Alt p q -> -> case match ϕ δ s trace p of +> case match s trace p of > Right v -> Right v -> Left{} -> match ϕ δ s trace q +> Left{} -> match s trace q + +Repetition is also quite simple and terminates because the base case (`Prog p`) consumes the head of the trace. + > Star p' -> -> case match ϕ δ s trace p' of -> Right (s', trace') -> match ϕ δ s' trace' (Star p') +> case match s trace p' of +> Right (s', trace') -> match s' trace' (Star p') > Left{} -> Right (s, trace) + +Finally, we can `Test` a formula whose result depends on call to `eval` with current state and trace. + > Test f -> -> case eval ϕ δ s f trace of +> case eval s f trace of > One -> Right (s, trace) > _other -> Left ("test failed", trace) -> isSatisfiable -> :: (Show p, Eq s, Show f, Eq f, Eq p, Test.QuickCheck.Arbitrary p) -> => (f -> s -> Bool) -> -- ^ The atomic propositions truth value -> -> (p -> s -> Maybe s) -> -- ^ Transition relation -> -> s -> -- ^ Initial state -> -> Test.QuickCheck.Gen [p] -> -- ^ A generator of traces from `s` -> -> Prop f p -> -- ^ A formula to check -> -> Test.QuickCheck.Property -> isSatisfiable ϕ δ i gen f = -> Test.QuickCheck.forAllShrink gen Test.QuickCheck.shrink $ \trace -> -> eval ϕ δ i f trace Test.QuickCheck.=== One +=== Example + +The generator for our simple model is quite simple as there's a single action. + +> instance Test.QuickCheck.Arbitrary P where +> arbitrary = pure A + +However we need a different Kripke structure because we want it to work in the `Maybe` monad, so let's wrap `S` and create the structure: + +> newtype S' = S' { unS :: S } +> deriving (Eq, Show) + +> instance Kripke Maybe S' where +> type Formula S' = F +> type Program S' = P + +> ϕ f = ϕ f . unS + +> δ A = \case +> S' U -> Just $ S' W +> S' V -> Just $ S' W +> S' W -> Just $ S' V + +Then we can run QuickCheck over our example formula: + +``` +$ quickCheck $ isSatisfiable (S' U) (const arbitrary) formula +*** Failed! Falsified (after 1 test): +[] +Zero /= One +``` + +Of course, the formula is wrong on an empty sequence of actions as we are in state `U`, but if we start from state `V` we can verify the property holds: + +``` +quickCheck $ isSatisfiable (S' V) (const arbitrary) formula ++++ OK, passed 100 tests. +``` + +== Generating valid traces + +In practice, what we are interested in with Dynamic Logic formulas is +rather the converse of what we have done so far: Inferring the subset of Kripke +structure that's a model for a given formula, for a given "universe of +discourse" consisting of the atomic propositions and programs. diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal index 267050b..12fea31 100644 --- a/quickcheck-dynamic/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic/quickcheck-dynamic.cabal @@ -67,7 +67,6 @@ library import: lang hs-source-dirs: src exposed-modules: - Test.QuickCheck.DL Test.QuickCheck.DynamicLogic Test.QuickCheck.DynamicLogic.CanGenerate Test.QuickCheck.DynamicLogic.Internal From f7ae1a47c255520db1f817c919f1013ccede050d Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 3 Apr 2024 11:03:55 +0200 Subject: [PATCH 11/13] Add section on test generation --- docs/DL.lhs | 146 ++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 137 insertions(+), 9 deletions(-) diff --git a/docs/DL.lhs b/docs/DL.lhs index f822bb5..07d7adb 100644 --- a/docs/DL.lhs +++ b/docs/DL.lhs @@ -1,20 +1,29 @@ + > {-# LANGUAGE FunctionalDependencies #-} > {-# LANGUAGE InstanceSigs #-} +> {-# LANGUAGE ScopedTypeVariables #-} > module DL where -> import Debug.Trace as Debug > import Control.Applicative ((<|>)) > import Control.Monad (foldM) > import Data.Kind (Type) > import Test.QuickCheck ( -> Arbitrary (..), -> Gen, -> Property, -> forAllShrink, -> (===), -> ) +> Arbitrary (..), +> Gen, +> Property, +> forAllShrink, +> (===), discard, forAllShrinkShow, +> ) + +The goal of this document is to provide a gentle introduction to +_Dynamic Logic_ which is a form of modal logic that is used within +`quickcheck-dynamic` to give the user the ability to express and tests +stateful properties about their code. The intention is to provide an +intuition of how things work within the library on a simpler version +of the logic. + = Propositional Dynamic Logic @@ -178,8 +187,7 @@ executing the program `p`. The `step` function computes the set of states reachable from the current state by executing the program `p`. -> step -> :: Kripke [] s +> step :: Kripke [] s > => Int > -> Prog (Formula s) (Program s) > -> s @@ -464,3 +472,123 @@ In practice, what we are interested in with Dynamic Logic formulas is rather the converse of what we have done so far: Inferring the subset of Kripke structure that's a model for a given formula, for a given "universe of discourse" consisting of the atomic propositions and programs. + +Our generator thus takes an initial state, a formula and output a list +of `Program` that satisfy this formula. If there's no such list, for +example because some proposition is not valid in some state, then the +generated sequence is `discard`ed. + +> generate :: +> forall s. +> Kripke Maybe s +> => s +> -> Prop (Formula s) (Program s) +> -> Gen [Program s] +> generate i = go i [] +> where + +As expected, the generator proceeds recursively on the structure of +the proposition, accumulating a trace as it walks through the syntax +tree. + +> go :: s -> [Program s] -> Prop (Formula s) (Program s) -> Gen [Program s] +> go s acc = \case + +A formula that's not verified in the current state discards its +accumulated trace, otherwise it yields it. + +> Prop f -> if ϕ f s +> then pure acc +> else discard + +False and True and logical implications are handled as expected, +respectively discarding their trace, returning it or testing both +formulas with the same state. + +> Zero -> discard +> One -> pure acc +> Imply f g -> do +> tr <- go s acc f +> go s (acc <> tr) g + +Modal necessity tries to make some progress from given program and +checks the result formula in the new state. + +> Always p f -> do +> (s', prog) <- progress s p +> go s' (acc <> prog) f + +Progress proceeds also structurally through a program's structure: + +> progress :: s -> Prog (Formula s) (Program s) -> Gen (s, [Program s]) +> progress s = \case + +Empty program succeeds yielding an empty trace and unchanged state. + +> Empty -> pure (s, []) + +An atomic program updates state and trace iff $\delta$ is defined in +the Kripke structure for the current state and program. + +> Prog p -> +> case δ p s of +> Nothing -> discard +> Just s' -> pure (s', [p]) + +Sequence of programs accumulate state change and trace for both executed programs. + +> Seq p q -> do +> (s', p') <- progress s p +> (s'', q') <- progress s' q +> pure (s'', p' <> q') + +Choice is handled non-deterministically, flipping a coin and selecting +one of the branches to make progress. This assumes that should one +branch fail, the other one will ultimately be selected. + +> Alt p q -> do +> b <- arbitrary +> if b +> then progress s p +> else progress s q + +A test leaves the state unchanged and depends on the result of evaluating the formula. + +> Test f -> +> (s,) <$> go s [] f + +Finally, iterative execution also flips a coin: If it fails, an empty +trace and unchanged state is returned, otherwise it progresses through +one step of the program and recursively calls itself with the result. + +> Star p -> do +> b <- arbitrary +> if b +> then do +> (s', p') <- progress s p +> (s'', p'') <- progress s' (Star p) +> pure (s'', p' <> p'') +> else +> pure (s, []) + +We can actually verify our generator is consistent with the given formula, expressing that as a `Property`: + +> generateConsistentWithEval :: +> ( Eq s, Show s +> , Eq (Formula s), Show (Formula s) +> , Eq (Program s), Show (Program s) +> , Test.QuickCheck.Arbitrary (Program s) +> , Kripke Maybe s) +> => s +> -> Prop (Formula s) (Program s) +> -> Property +> generateConsistentWithEval i f = +> forAllShrinkShow (generate i f) shrink show $ \ trace -> +> eval i f trace Test.QuickCheck.=== One + +Running this property gives us: + +``` +$ Test.QuickCheck.quickCheck $ generateConsistentWithEval (S' U) formula ++++ OK, passed 100 tests; 78 discarded. +``` From 33b740f5f9ce90c9051536c0fa3732263b12da5d Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 3 Apr 2024 16:57:22 +0200 Subject: [PATCH 12/13] Add some motivating section --- docs/DL.html | 493 ++++++++++++++++++++++++++++++++------------------- docs/DL.lhs | 34 +++- 2 files changed, 337 insertions(+), 190 deletions(-) diff --git a/docs/DL.html b/docs/DL.html index d2c9e24..ab57638 100644 --- a/docs/DL.html +++ b/docs/DL.html @@ -60,10 +60,6 @@ img { max-width: 100%; } - svg { - height: auto; - max-width: 100%; - } h1, h2, h3, h4, h5, h6 { margin-top: 1.4em; } @@ -156,11 +152,8 @@ div.columns{display: flex; gap: min(4vw, 1.5em);} div.column{flex: auto; overflow-x: auto;} div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} - /* The extra [class] is a hack that increases specificity enough to - override a similar rule in reveal.js */ - ul.task-list[class]{list-style: none;} + ul.task-list{list-style: none;} ul.task-list li input[type="checkbox"] { - font-size: inherit; width: 0.8em; margin: 0 0.8em 0.2em -1.6em; vertical-align: middle; @@ -168,7 +161,7 @@ .display.math{display: block; text-align: center; margin: 0.5rem auto;} /* CSS for syntax highlighting */ pre > code.sourceCode { white-space: pre; position: relative; } - pre > code.sourceCode > span { line-height: 1.25; } + pre > code.sourceCode > span { display: inline-block; line-height: 1.25; } pre > code.sourceCode > span:empty { height: 1.2em; } .sourceCode { overflow: visible; } code.sourceCode > span { color: inherit; text-decoration: inherit; } @@ -231,25 +224,45 @@ code span.vs { color: #4070a0; } /* VerbatimString */ code span.wa { color: #60a0b0; font-weight: bold; font-style: italic; } /* Warning */ + 
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE InstanceSigs #-}
+class="sourceCode literatehaskell literate">> {-# LANGUAGE FunctionalDependencies #-} +> {-# LANGUAGE InstanceSigs #-} +> {-# LANGUAGE ScopedTypeVariables #-} 
module DL where
+class="sourceCode literatehaskell literate">> module DL where 
import Debug.Trace as Debug
-import Control.Applicative ((<|>))
-import Control.Monad (foldM)
-import Data.Kind (Type)
-import Test.QuickCheck (
-  Arbitrary (..),
-  Gen,
-  Property,
-  forAllShrink,
-  (===),
- )
+class="sourceCode literatehaskell literate">> import Control.Applicative ((<|>)) +> import Control.Monad (foldM) +> import Data.Kind (Type) +> import Test.QuickCheck ( +> Arbitrary (..), +> Gen, +> Property, +> forAllShrink, +> (===), discard, forAllShrinkShow, +> ) +

The goal of this document is to provide a gentle introduction to +Dynamic Logic, a form of modal logic that is used within +quickcheck-dynamic. The intention is to provide an +intuition of how things work within the library on a simpler version of +the logic.

+

Dynamic Logic DL – for short – formulas give users the ability to +express and tests liveness and safety properties about +their code independently from the actual state-machine model +and implementation. Put it differently, DL formulas allow a user to +restrict the state space of a model and provide an Embedded +Domain Specific Language to define composable expressions +representing some fragment of a larger state.

+

In quickcheck-dynamic, DynamicLogic +is exposed through a monadic interface which makes it simpler to write +formulas, and, more importantly, provides variables and universal +quantification over values.

Propositional Dynamic Logic

This follows the presentation from the book Dynamic @@ -264,20 +277,20 @@

Propositions

propositions and atomic programs, whose semantics is given by a Kripke structure.

data Prop f p where
+class="sourceCode literatehaskell literate">> data Prop f p where

Atomic propositions are drawn from the type f.

  Prop :: f -> Prop f p
+class="sourceCode literatehaskell literate">> Prop :: f -> Prop f p

False and true are propositions. Note that One is not strictly necessary but has been added for convenience purpose.

  Zero :: Prop f p
-  One :: Prop f p
+class="sourceCode literatehaskell literate">> Zero :: Prop f p +> One :: Prop f p

The main logical combinator is implication. It’s well known that it’s possible to reconstruct disjunction and conjunctions from implication.

  Imply :: Prop f p -> Prop f p -> Prop f p
+class="sourceCode literatehaskell literate">> Imply :: Prop f p -> Prop f p -> Prop f p

The most interesting operator is the modal necessity operator which informally states that some Proposition must always hold after the execution of some Program. @@ -285,63 +298,63 @@

Propositions

can hold after some program, could be derived but is impractical to work with in the context of test case generations and verification.

  Always :: Prog f p -> Prop f p -> Prop f p
-  deriving (Eq, Show)
+class="sourceCode literatehaskell literate">> Always :: Prog f p -> Prop f p -> Prop f p +> deriving (Eq, Show)

Programs

Programs are what makes the Dynamic Logic a modal logic, obviously. This type is also parameterised by atomic propositions f and atomic programs (aka. actions) p.

data Prog f p where
+class="sourceCode literatehaskell literate">> data Prog f p where

The empty program, also called skip or represented by the ∅ symbol, represents termination of a program execution. We could also define Abort or divergence to represent non-termination or invalid execution.

  Empty :: Prog f p
+class="sourceCode literatehaskell literate">> Empty :: Prog f p

Every atomic program p is of course a program.

  Prog :: p -> Prog f p
+class="sourceCode literatehaskell literate">> Prog :: p -> Prog f p

Programs can be run in sequence, one after another

  Seq :: Prog f p -> Prog f p -> Prog f p
+class="sourceCode literatehaskell literate">> Seq :: Prog f p -> Prog f p -> Prog f p

Or one or the other can be run, non deterministically.

  Alt :: Prog f p -> Prog f p -> Prog f p
+class="sourceCode literatehaskell literate">> Alt :: Prog f p -> Prog f p -> Prog f p

Programs can also be repeated, indefinitely, using an analog to the Kleene star from regular lagnauges.

  Star :: Prog f p -> Prog f p
+class="sourceCode literatehaskell literate">> Star :: Prog f p -> Prog f p

Finally, a program can be a test which does not change the state of the system but either yields skip or abort depending on the result of evaluating the given proposition.

  Test :: Prop f p -> Prog f p
-  deriving (Eq, Show)
+class="sourceCode literatehaskell literate">> Test :: Prop f p -> Prog f p +> deriving (Eq, Show)

Deriving constructs

Standard constructs from imperative programming can be define from the basic combinators, like if/then/else or while instructions:

ifThenElse :: Prop f p -> Prog f p -> Prog f p -> Prog f p
-ifThenElse cond ifTrue ifFalse =
-  Alt (Seq (Test cond) ifTrue)
-      (Seq (Test (Imply cond Zero)) ifFalse)
+class="sourceCode literatehaskell literate">> ifThenElse :: Prop f p -> Prog f p -> Prog f p -> Prog f p +> ifThenElse cond ifTrue ifFalse = +> Alt (Seq (Test cond) ifTrue) +> (Seq (Test (Imply cond Zero)) ifFalse)

Semantics

The semantics of Dynamic Logic formulas is given by a Kripke structure K = (W,ϕ,δ)

class Kripke m w | w -> m where
-  type Formula w :: Type
-  type Program w :: Type
+class="sourceCode literatehaskell literate">> class Kripke m w | w -> m where +> type Formula w :: Type +> type Program w :: Type

with ϕ giving an interpretation of atomic propositions as a subset of W. Note that this subset is here defined through a characteristic function w -> Bool.

  ϕ :: Formula w -> w -> Bool
+class="sourceCode literatehaskell literate">> ϕ :: Formula w -> w -> Bool

And δ giving an interpretation of atomic programs. The usual presentation is to consider δ as a relation over Semantics m = Identity, a partial function if m = Maybe, a relation if m = [w] or anything else.

  δ :: Program w -> w -> m w
+class="sourceCode literatehaskell literate">> δ :: Program w -> w -> m w

Satisfiability

Given some Kripke structure K, a formula f is @@ -361,93 +374,92 @@

Satisfiability

Note that we need to limit the size of the formula to avoid infinite recursion.

satisfy
+class="sourceCode literatehaskell literate">> satisfy

Note that satisfy is defined here with atomic programs defining relations over s and not functions, eg. a given program p can have multiple possible state outcomes.

  :: Kripke [] s
+class="sourceCode literatehaskell literate">> :: Kripke [] s

The size parameter bounds the depth at which state is explored and the formula is evaluated.

  => Int
+class="sourceCode literatehaskell literate">> => Int

The formula to evaluate, f is a proposition dependent on the atomic propositions and programs in K.

  -> Prop (Formula s) (Program s)
+class="sourceCode literatehaskell literate">> -> Prop (Formula s) (Program s)

The state in which to evaluate the formula.

  -> s
-  -> Bool
-satisfy k prop s =
-  case prop of
+class="sourceCode literatehaskell literate">> -> s +> -> Bool +> satisfy k prop s = +> case prop of

Atomic propositions are evaluated by the characteristic function ϕ.

    Prop f -> ϕ f s
+class="sourceCode literatehaskell literate">> Prop f -> ϕ f s

False, true, and implications are evaluated as expected for propositional logic operators.

    Zero -> False
-    One -> True
-    Imply f g ->
-      not (satisfy (k - 1) f s) || satisfy (k - 1) g s
+class="sourceCode literatehaskell literate">> Zero -> False +> One -> True +> Imply f g -> +> not (satisfy (k - 1) f s) || satisfy (k - 1) g s

The always operator is evaluated by checking that the proposition holds in all the states reachable from the current state by executing the program p.

    Always p f ->
-      case step k p s of
-        [] -> False
-        states -> all (satisfy (k - 1) f) states
+class="sourceCode literatehaskell literate">> Always p f -> +> case step k p s of +> [] -> False +> states -> all (satisfy (k - 1) f) states

The step function computes the set of states reachable from the current state by executing the program p.

step
-  :: Kripke [] s
-  => Int
-  -> Prog (Formula s) (Program s)
-  -> s
-  -> [s]
+class="sourceCode literatehaskell literate">> step :: Kripke [] s +> => Int +> -> Prog (Formula s) (Program s) +> -> s +> -> [s]

If the size limit is reached, the computation is considered “stuck” and yields no reachable state.

step 0 _ _ = []
+class="sourceCode literatehaskell literate">> step 0 _ _ = []

In other cases, reachable states are defined inductively over the structure of the program.

step k prog s =
-  case prog of
+class="sourceCode literatehaskell literate">> step k prog s = +> case prog of

If program should stop, simply return the current state.

    Empty -> [s]
+class="sourceCode literatehaskell literate">> Empty -> [s]

Atomic programs yield the result of the transition relation δ.

    Prog p -> δ p s
+class="sourceCode literatehaskell literate">> Prog p -> δ p s

Sequencing of programs is done by executing the first program and then the second program on the resulting state(s).

    Seq p q -> do
-      s' <- step k p s
-      step k q s'
+class="sourceCode literatehaskell literate">> Seq p q -> do +> s' <- step k p s +> step k q s'

Non-deterministic choice is done by executing either the first or the second program, with a bias towards the first program.

    Alt p q -> do
-      step k p s <|> step k q s
+class="sourceCode literatehaskell literate">> Alt p q -> do +> step k p s <|> step k q s

Test programs are executed by checking if the proposition holds in the current state and returning the current state if it does.

    Test f ->
-      [s | satisfy (k - 1) f s]
+class="sourceCode literatehaskell literate">> Test f -> +> [s | satisfy (k - 1) f s]

Finally, repetition of a program is done by iterating over the nested program k times.

    Star p ->
-      foldM (flip $ step (k - 1)) s (replicate k p)
+class="sourceCode literatehaskell literate">> Star p -> +> foldM (flip $ step (k - 1)) s (replicate k p)

A “concrete” Example

The following is a concrete example of some simple data types and Kripke structure to evaluate the satisfaction of a formula, drawn from @@ -455,37 +467,37 @@

A “concrete” Example

The system’s state is simply an enumeration of 3 different states.

data S = U | V | W
-  deriving (Eq, Show)
+class="sourceCode literatehaskell literate">> data S = U | V | W +> deriving (Eq, Show)

There’s a single atomic program, A.

data P = A
-  deriving (Eq, Show)
+class="sourceCode literatehaskell literate">> data P = A +> deriving (Eq, Show)

The atomic propositions are simply a list of states and a proposition is true iff reached state is included in the list.

type F = [S]
+class="sourceCode literatehaskell literate">> type F = [S] 
instance Kripke [] S where
-  type Formula S = F
-  type Program S = P
+class="sourceCode literatehaskell literate">> instance Kripke [] S where +> type Formula S = F +> type Program S = P 
  ϕ :: F -> S -> Bool
-  ϕ = flip elem
+class="sourceCode literatehaskell literate">> ϕ :: F -> S -> Bool +> ϕ = flip elem

The transition relation is the only interesting part of the Kripke structure.

  δ :: P -> S -> [S]
-  δ A = \case
-    U -> [V, W]
-    W -> [V]
-    V -> [W]
+class="sourceCode literatehaskell literate">> δ :: P -> S -> [S] +> δ A = \case +> U -> [V, W] +> W -> [V] +> V -> [W]

Now, let’s define a simple formula to check if the state V is reachable from the state U after executing the program A.

formula :: Prop F P
-formula = Always (Star (Prog A)) (Prop [V,W])
+class="sourceCode literatehaskell literate">> formula :: Prop F P +> formula = Always (Star (Prog A)) (Prop [V,W])

We can now check if the formula is satisfied in the state U of the Kripke structure defined above within GHCi:

$ satisfy 10 formula U
@@ -504,110 +516,110 @@ 
Checking satisfiability

 are reachable throughsome sequence of execution of programs, and check
 if the formula holds for all of them.

 
isSatisfiable
-  :: ( Eq s, Show s
-     , Eq (Formula s), Show (Formula s)
-     , Eq (Program s), Show (Program s)
-     , Test.QuickCheck.Arbitrary (Program s)
-     , Kripke Maybe s)

+class="sourceCode literatehaskell literate">> isSatisfiable
+>   :: ( Eq s, Show s
+>      , Eq (Formula s), Show (Formula s)
+>      , Eq (Program s), Show (Program s)
+>      , Test.QuickCheck.Arbitrary (Program s)
+>      , Kripke Maybe s)

Given some initial state,

   => s
+class="sourceCode literatehaskell literate">> => s

A generator for traces,

   -> (s -> Test.QuickCheck.Gen [Program s])
+class="sourceCode literatehaskell literate">> -> (s -> Test.QuickCheck.Gen [Program s])

and a formula to check,

   -> Prop (Formula s) (Program s)
-   -> Test.QuickCheck.Property
-isSatisfiable i gen f =
-  Test.QuickCheck.forAllShrink (gen i) Test.QuickCheck.shrink $ \trace ->
+class="sourceCode literatehaskell literate">> -> Prop (Formula s) (Program s) +> -> Test.QuickCheck.Property +> isSatisfiable i gen f = +> Test.QuickCheck.forAllShrink (gen i) Test.QuickCheck.shrink $ \trace ->

It should hold that the formula evaluates to True given the trace and the initial state.

    eval i f trace Test.QuickCheck.=== One
+class="sourceCode literatehaskell literate">> eval i f trace Test.QuickCheck.=== One

To do so, we need to evaluate a formula in a given state against some trace, yielding a simpler formula until we reach atomic propositions or ground truths.

eval
-  :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s))
-   => s
-   -> Prop (Formula s) (Program s)
-   -> [Program s]
-   -> Prop (Formula s) (Program s)
-eval s prop trace =
+class="sourceCode literatehaskell literate">> eval +> :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s)) +> => s +> -> Prop (Formula s) (Program s) +> -> [Program s] +> -> Prop (Formula s) (Program s) +> eval s prop trace =

Evaluation proceeds recursively over the structure of the formula and the trace.

  case prop of
+class="sourceCode literatehaskell literate">> case prop of

Atomic propositions should hold in the current state

    Prop f ->
-      if ϕ f s then One else Zero
-    Zero -> Zero
-    One -> One
+class="sourceCode literatehaskell literate">> Prop f -> +> if ϕ f s then One else Zero +> Zero -> Zero +> One -> One

Implications follow the usual rules of logic

    Imply f g ->
-      let f' = eval s f trace
-          g' = eval s g trace
-       in case (f', g') of
-            (Zero, _) -> One
-            (One, One) -> One
-            (_, _) -> Zero
+class="sourceCode literatehaskell literate">> Imply f g -> +> let f' = eval s f trace +> g' = eval s g trace +> in case (f', g') of +> (Zero, _) -> One +> (One, One) -> One +> (_, _) -> Zero

The always operator requires advancing the state by executing the program p and evaluating the formula f in the resulting state, agains the resulting trace.

    Always p f ->
-      case match s trace p of
-        Right (s', trace') -> eval s' f trace'
-        Left{} -> Zero
+class="sourceCode literatehaskell literate">> Always p f -> +> case match s trace p of +> Right (s', trace') -> eval s' f trace' +> Left{} -> Zero

The match function advances the state by executing the program p:

match
-  :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s))
-   => s
-   -> [Program s]
-   -> Prog (Formula s) (Program s)
+class="sourceCode literatehaskell literate">> match +> :: (Kripke Maybe s, Eq s, Show s, Show (Program s), Show (Formula s)) +> => s +> -> [Program s] +> -> Prog (Formula s) (Program s)

Note match can fail if the program is not executable in the current state, in which case it returns some error message and the remaining trace.

   -> Either (String, [Program s]) (s, [Program s])
+class="sourceCode literatehaskell literate">> -> Either (String, [Program s]) (s, [Program s])

The base case is when the trace is empty, in which case the program should terminate which is only possible if the program is empty, or it can be repeated indefinitely which includes the case where it’s not repeated at all.

match s [] = \case
-  Empty -> Right (s, [])
-  Star{} -> Right (s, [])
-  other -> Left ("empty trace with program " <> show other, [])
+class="sourceCode literatehaskell literate">> match s [] = \case +> Empty -> Right (s, []) +> Star{} -> Right (s, []) +> other -> Left ("empty trace with program " <> show other, [])

If the trace is not empty, we need to inductively walk through the trace and the program structure:

match s trace@(a : as) = \case
-  Empty -> Left ("program should terminate", trace)
+class="sourceCode literatehaskell literate">> match s trace@(a : as) = \case +> Empty -> Left ("program should terminate", trace)

For atomic programs, we could check equality of the atomic programs and advance the state if they matched, but we choose instead to check equality of observational behaviors of the programs, eg. whether or not the two programs yield the same state:

  Prog b ->
-    case (δ a s, δ b s) of
-      (Just t, Just t')
-        | t == t' -> Right (t', as)
-      _other ->
-        Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace)
+class="sourceCode literatehaskell literate">> Prog b -> +> case (δ a s, δ b s) of +> (Just t, Just t') +> | t == t' -> Right (t', as) +> _other -> +> Left ("unmatched atomic program, expected" <> show b <> ", found " <> show a, trace)

Sequential execution is straightforward, simply feeding the new state and trace to the next program

  Seq p q -> do
-    (s', trace') <- match s trace p
-    match s' trace' q
+class="sourceCode literatehaskell literate">> Seq p q -> do +> (s', trace') <- match s trace p +> match s' trace' q

Non-deterministic choice is also straightforward, trying to match the first program and if it fails, trying the second program. Note that we cannot here use the Alternative operator @@ -615,47 +627,47 @@

Checking satisfiability

surprisingly in the case of an “error” monad, not an instance of Alternative.

  Alt p q ->
-    case match s trace p of
-      Right v -> Right v
-      Left{} -> match s trace q
+class="sourceCode literatehaskell literate">> Alt p q -> +> case match s trace p of +> Right v -> Right v +> Left{} -> match s trace q

Repetition is also quite simple and terminates because the base case (Prog p) consumes the head of the trace.

  Star p' ->
-    case match s trace p' of
-      Right (s', trace') -> match s' trace' (Star p')
-      Left{} -> Right (s, trace)
+class="sourceCode literatehaskell literate">> Star p' -> +> case match s trace p' of +> Right (s', trace') -> match s' trace' (Star p') +> Left{} -> Right (s, trace)

Finally, we can Test a formula whose result depends on call to eval with current state and trace.

  Test f ->
-    case eval s f trace of
-      One -> Right (s, trace)
-      _other -> Left ("test failed", trace)
+class="sourceCode literatehaskell literate">> Test f -> +> case eval s f trace of +> One -> Right (s, trace) +> _other -> Left ("test failed", trace)

Example

The generator for our simple model is quite simple as there’s a single action.

instance Test.QuickCheck.Arbitrary P where
-  arbitrary = pure A
+class="sourceCode literatehaskell literate">> instance Test.QuickCheck.Arbitrary P where +> arbitrary = pure A

However we need a different Kripke structure because we want it to work in the Maybe monad, so let’s wrap S and create the structure:

newtype S' = S' { unS :: S }
-  deriving (Eq, Show)
+class="sourceCode literatehaskell literate">> newtype S' = S' { unS :: S } +> deriving (Eq, Show) 
instance Kripke Maybe S' where
-  type Formula S' = F
-  type Program S' = P
+class="sourceCode literatehaskell literate">> instance Kripke Maybe S' where +> type Formula S' = F +> type Program S' = P 
  ϕ f = ϕ f . unS
+class="sourceCode literatehaskell literate">> ϕ f = ϕ f . unS 
  δ A = \case
-    S' U -> Just $ S' W
-    S' V -> Just $ S' W
-    S' W -> Just $ S' V
+class="sourceCode literatehaskell literate">> δ A = \case +> S' U -> Just $ S' W +> S' V -> Just $ S' W +> S' W -> Just $ S' V

Then we can run QuickCheck over our example formula:

$ quickCheck $ isSatisfiable (S' U)  (const arbitrary) formula
 *** Failed! Falsified (after 1 test):
@@ -672,5 +684,122 @@ 
Generating valid traces

 Kripke structure that’s a model for a given formula, for a given
 “universe of discourse” consisting of the atomic propositions and
 programs.

+
NOTE: This implementation relies on
+discard from the QuickCheck library to prune sequence of
+programs which is annoying. It would be better to wrap generation in
+some result type and keep generating upon failures, until some timeout
+or limit is reached.

+
Our generator thus takes an initial state, a formula and output a
+list of Program that satisfy this formula. If there’s no
+such list, for example because some proposition is not valid in some
+state, then the generated sequence is discarded.

+
> generate ::
+>      forall s.
+>      Kripke Maybe s
+>      => s
+>      -> Prop (Formula s) (Program s)
+>      -> Gen [Program s]
+> generate i = go i []
+>   where

+
As expected, the generator proceeds recursively on the structure of
+the proposition, accumulating a trace as it walks through the syntax
+tree.

+
>    go :: s -> [Program s] -> Prop (Formula s) (Program s) ->  Gen [Program s]
+>    go s acc = \case

+
A formula that’s not verified in the current state discards its
+accumulated trace, otherwise it yields it.

+
>      Prop f -> if ϕ f s
+>                 then pure acc
+>                 else discard

+
False and True and logical implications are handled as expected,
+respectively discarding their trace, returning it or testing both
+formulas with the same state.

+
NOTE: Imply implementation is most
+probably wrong…

+
>      Zero -> discard
+>      One -> pure acc
+>      Imply f g -> do
+>        tr <- go s acc f
+>        go s (acc <> tr) g

+
Modal necessity tries to make some progress from given program and
+checks the result formula in the new state.

+
>      Always p f -> do
+>        (s', prog) <- progress s p
+>        go s' (acc <> prog) f

+
Progress proceeds also structurally through a program’s
+structure:

+
>    progress :: s -> Prog (Formula s) (Program s) -> Gen (s, [Program s])
+>    progress s = \case

+
Empty program succeeds yielding an empty trace and unchanged
+state.

+
>      Empty -> pure (s, [])

+
An atomic program updates state and trace iff δ is defined in the Kripke structure
+for the current state and program.

+
>      Prog p ->
+>        case δ p s of
+>          Nothing -> discard
+>          Just s' -> pure (s', [p])

+
Sequence of programs accumulate state change and trace for both
+executed programs.

+
>      Seq p q -> do
+>        (s', p') <- progress s p
+>        (s'', q') <- progress s' q
+>        pure (s'', p' <> q')

+
Choice is handled non-deterministically, flipping a coin and
+selecting one of the branches to make progress. This assumes that should
+one branch fail, the other one will ultimately be selected.

+
>      Alt p q -> do
+>        b <- arbitrary
+>        if b
+>         then progress s p
+>         else progress s q

+
A test leaves the state unchanged and depends on the result of
+evaluating the formula.

+
>      Test f ->
+>        (s,) <$> go s [] f

+
Finally, iterative execution also flips a coin: If it fails, an empty
+trace and unchanged state is returned, otherwise it progresses through
+one step of the program and recursively calls itself with the
+result.

+
>      Star p -> do
+>        b <- arbitrary
+>        if b
+>          then do
+>            (s', p') <- progress s p
+>            (s'', p'') <- progress s' (Star p)
+>            pure (s'', p' <> p'')
+>          else
+>            pure (s, [])

+
We can actually verify our generator is consistent with the given
+formula, expressing that as a Property:

+
> generateConsistentWithEval ::
+>         ( Eq s, Show s
+>         , Eq (Formula s), Show (Formula s)
+>         , Eq (Program s), Show (Program s)
+>         , Test.QuickCheck.Arbitrary (Program s)
+>         , Kripke Maybe s)
+>         => s
+>         -> Prop (Formula s) (Program s)
+>         -> Property
+> generateConsistentWithEval i f =
+>   forAllShrinkShow (generate i f) shrink show $ \ trace ->
+>      eval i f trace Test.QuickCheck.=== One

+
Running this property gives us:

+
$ Test.QuickCheck.quickCheck $ generateConsistentWithEval (S' U) formula
++++ OK, passed 100 tests; 78 discarded.

 
 
diff --git a/docs/DL.lhs b/docs/DL.lhs
index 07d7adb..c212548 100644
--- a/docs/DL.lhs
+++ b/docs/DL.lhs
@@ -18,12 +18,23 @@
 >    )
 
 The goal of this document is to provide a gentle introduction to
-_Dynamic Logic_ which is a form of modal logic that is used within
-`quickcheck-dynamic` to give the user the ability to express and tests
-stateful properties about their code. The intention is to provide an
-intuition of how things work within the library on a simpler version
-of the logic.
-
+_Dynamic Logic_, a form of modal logic that is used within
+`quickcheck-dynamic`.  The intention is to provide an intuition of how
+things work within the library on a simpler version of the logic.
+
+Dynamic Logic DL -- for short -- formulas give users the ability to
+express and tests _liveness_ and _safety_ properties about their code
+_independently_ from the actual state-machine model and
+implementation. Put it differently, DL formulas allow a user to
+_restrict_ the state space of a model and provide an _Embedded Domain
+Specific Language_ to define composable expressions representing some
+fragment of a larger state.
+
+In `quickcheck-dynamic`,
+[`DynamicLogic`](https://github.com/input-output-hk/quickcheck-dynamic/blob/f7ae1a47c255520db1f817c919f1013ccede050d/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs#L9)
+is exposed through a monadic interface which makes it simpler to write
+formulas, and, more importantly, provides variables and universal
+quantification over values.
 
 = Propositional Dynamic Logic
 
@@ -473,6 +484,11 @@ rather the converse of what we have done so far: Inferring the subset of Kripke
 structure that's a model for a given formula, for a given "universe of
 discourse" consisting of the atomic propositions and programs.
 
+**NOTE**: This implementation relies on `discard` from the QuickCheck
+  library to prune sequence of programs which is annoying. It would be
+  better to wrap generation in some result type and keep generating
+  upon failures, until some timeout or limit is reached.
+
 Our generator thus takes an initial state, a formula and output a list
 of `Program` that satisfy this formula. If there's no such list, for
 example because some proposition is not valid in some state, then the
@@ -505,6 +521,8 @@ False and True and logical implications are handled as expected,
 respectively discarding their trace, returning it or testing both
 formulas with the same state.
 
+**NOTE**: `Imply` implementation is wrong...
+
 >      Zero -> discard
 >      One -> pure acc
 >      Imply f g -> do
@@ -573,7 +591,7 @@ one step of the program and recursively calls itself with the result.
 
 We can actually verify our generator is consistent with the given formula, expressing that as a `Property`:
 
-> generateConsistentWithEval ::
+> isGenerateConsistentWithEval ::
 >         ( Eq s, Show s
 >         , Eq (Formula s), Show (Formula s)
 >         , Eq (Program s), Show (Program s)
@@ -582,7 +600,7 @@ We can actually verify our generator is consistent with the given formula, expre
 >         => s
 >         -> Prop (Formula s) (Program s)
 >         -> Property
-> generateConsistentWithEval i f =
+> isGenerateConsistentWithEval i f =
 >   forAllShrinkShow (generate i f) shrink show $ \ trace ->
 >      eval i f trace Test.QuickCheck.=== One
 

From 76a3260c3bd5b84a2ecee80ee7d553802b4c6d1c Mon Sep 17 00:00:00 2001
From: Arnaud Bailly 
Date: Wed, 3 Apr 2024 17:05:52 +0200
Subject: [PATCH 13/13] Added README for docs/

---
 docs/README.md | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/README.md

diff --git a/docs/README.md b/docs/README.md
new file mode 100644
index 0000000..dee5280
--- /dev/null
+++ b/docs/README.md
@@ -0,0 +1 @@
+This "package" is meant to contain the source of the documentation for quickcheck-dynamic which is deployed to https://input-output-hk.github.io/quickcheck-dynamic