crdt 6.2 → 7.0

raw patch · 26 files changed

+992/−180 lines, 26 filesdep +Diffdep +QuickCheck-GenTdep +vectordep ~containersPVP ok

version bump matches the API change (PVP)

Dependencies added: Diff, QuickCheck-GenT, vector

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• crdt.cabal +18/−4
• lib/CRDT/Cm.hs +37/−0
• lib/CRDT/Cm/Counter.hs +2/−0
• lib/CRDT/Cm/GSet.hs +3/−1
• lib/CRDT/Cm/ORSet.hs +64/−0
• lib/CRDT/Cm/RGA.hs +181/−0
• lib/CRDT/Cm/TwoPSet.hs +14/−9
• lib/CRDT/Cv/LwwElementSet.hs +2/−2
• lib/CRDT/Cv/RGA.hs +108/−0
• lib/CRDT/Cv/TwoPSet.hs +4/−6
• lib/CRDT/LWW.hs +14/−7
• lib/CRDT/LamportClock.hs +8/−45
• lib/CRDT/LamportClock/Simulation.hs +119/−0
• lib/Data/MultiMap.hs +55/−0
• test/ArbitraryOrphans.hs +50/−8
• test/Cm/ORSet.hs +44/−0
• test/Cm/TwoPSet.hs +9/−3
• test/Cv/ORSet.hs +28/−0
• test/Cv/RGA.hs +27/−0
• test/Cv/TwoPSet.hs +5/−7
• test/LWW.hs +8/−6
• test/Laws.hs +87/−52
• test/LwwElementSet.hs +7/−5
• test/ORSet.hs +0/−25
• test/RGA.hs +81/−0
• test/Util.hs +17/−0

@@ -2,10 +2,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 7021f3e0d6e0f14ccbff42fd8252b25b479ffd645160458d77d1c854912c9698+-- hash: 03da394dee75b1bb3cc8d9b26448adbfe3b32c0f4f91c1f62c6672bb5ab17d04  name:           crdt-version:        6.2+version:        7.0 synopsis:       Conflict-free replicated data types description:    Definitions of CmRDT and CvRDT. Implementations for some classic CRDTs. category:       Distributed Systems@@ -26,7 +26,8 @@   hs-source-dirs:       lib   build-depends:-      base >=4.9 && <4.11+      Diff+    , base >=4.9 && <4.11     , binary     , bytestring     , containers@@ -35,10 +36,13 @@     , safe     , stm     , time+    , vector   exposed-modules:       CRDT.Cm       CRDT.Cm.Counter       CRDT.Cm.GSet+      CRDT.Cm.ORSet+      CRDT.Cm.RGA       CRDT.Cm.TwoPSet       CRDT.Cv       CRDT.Cv.GCounter@@ -47,9 +51,12 @@       CRDT.Cv.Max       CRDT.Cv.ORSet       CRDT.Cv.PNCounter+      CRDT.Cv.RGA       CRDT.Cv.TwoPSet       CRDT.LamportClock+      CRDT.LamportClock.Simulation       CRDT.LWW+      Data.MultiMap       Data.Semilattice   other-modules:       Paths_crdt@@ -62,17 +69,23 @@       test   build-depends:       QuickCheck+    , QuickCheck-GenT     , base >=4.9 && <4.11     , containers     , crdt+    , mtl     , quickcheck-instances     , tasty     , tasty-discover >=4.1     , tasty-quickcheck+    , vector   other-modules:       ArbitraryOrphans+      Cm.ORSet       Cm.TwoPSet       Counter+      Cv.ORSet+      Cv.RGA       Cv.TwoPSet       GCounter       GSet@@ -80,7 +93,8 @@       LWW       LwwElementSet       Max-      ORSet       PNCounter+      RGA+      Util       Paths_crdt   default-language: Haskell2010

@@ -1,13 +1,24 @@+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}  module CRDT.Cm     ( CausalOrd (..)     , CmRDT (..)     , concurrent+    , query+    , makeAndApplyOp+    , makeAndApplyOps     ) where +import           Prelude hiding (fail)++import           Control.Monad.Fail (MonadFail, fail)+import           Control.Monad.State.Strict (MonadState, get, modify)+ import           CRDT.LamportClock (Clock)  -- | Partial order for causal semantics.@@ -61,6 +72,8 @@      type Payload op +    initial :: Payload op+     -- | Generate an update to the local and remote replicas.     --     -- Returns 'Nothing' if the intended operation is not applicable.@@ -77,3 +90,27 @@     -- TODO(Syrovetsky, 2017-12-05) There is no downstream precondition yet.     -- We must make a test for it first.     apply :: op -> Payload op -> Payload op++query :: forall op f. (CmRDT op, Foldable f) => f op -> Payload op+query = foldl (flip apply) (initial @op)++-- | Make op and apply it to the payload -- a common routine at the source node.+makeAndApplyOp+    :: (CmRDT op, Clock m, MonadFail m, MonadState (Payload op) m)+    => Intent op -> m op+makeAndApplyOp intent = do+    payload <- get+    case makeOp intent payload of+        Nothing -> fail "precodition failed"+        Just opAction -> do+            op <- opAction+            modify $ apply op+            pure op++makeAndApplyOps+    :: ( CmRDT op+       , Clock m, MonadFail m, MonadState (Payload op) m+       , Traversable f+       )+    => f (Intent op) -> m (f op)+makeAndApplyOps = traverse makeAndApplyOp

@@ -15,6 +15,8 @@ instance (Num a, Eq a) => CmRDT (Counter a) where     type Payload (Counter a) = a +    initial = 0+     apply = \case         Increment -> (+ 1)         Decrement -> subtract 1

@@ -15,7 +15,9 @@ instance Ord a => CmRDT (GSet a) where     type Payload (GSet a) = Set a +    initial = Set.empty+     apply (Add a) = Set.insert a -instance Eq a => CausalOrd (GSet a) where+instance CausalOrd (GSet a) where     precedes _ _ = False

@@ -0,0 +1,64 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE TypeFamilies #-}++module CRDT.Cm.ORSet+    ( ORSet (..)+    , Intent (..)+    , Payload (..)+    , Tag (..)+    , query+    ) where++import           Data.MultiMap (MultiMap)+import qualified Data.MultiMap as MultiMap+import           Data.Set (Set)+import           Numeric.Natural (Natural)++import           CRDT.Cm (CausalOrd, CmRDT)+import qualified CRDT.Cm as Cm+import           CRDT.LamportClock (Pid (Pid), getPid)++data ORSet a = OpAdd a Tag | OpRemove a (Set Tag)+    deriving Show++data Intent a = Add a | Remove a+    deriving Show++data Payload a = Payload+    { elements :: MultiMap a Tag+    , version  :: Version+    }+    deriving (Eq, Show)++data Tag = Tag Pid Version+    deriving (Eq, Ord)++type Version = Natural++instance Show Tag where+    show (Tag (Pid pid) version) = show pid ++ '-' : show version++instance CausalOrd (ORSet a) where+    precedes _ _ = False++instance Ord a => CmRDT (ORSet a) where+    type Intent  (ORSet a) = Intent  a+    type Payload (ORSet a) = Payload a++    initial = Payload{elements = MultiMap.empty, version = 0}++    makeOp (Add a) Payload{version} = Just $ do+        pid <- getPid+        pure $ OpAdd a $ Tag pid version+    makeOp (Remove a) Payload{elements} =+        Just . pure . OpRemove a $ MultiMap.lookup a elements++    apply op Payload{elements, version} = Payload+        { version  = version + 1+        , elements = case op of+            OpAdd    a tag  -> MultiMap.insert     a tag  elements+            OpRemove a tags -> MultiMap.deleteMany a tags elements+        }++query :: (Ord a, Foldable f) => f (ORSet a) -> Set a+query = MultiMap.keysSet . elements . Cm.query

@@ -0,0 +1,181 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE ParallelListComp #-}+{-# LANGUAGE StrictData #-}+{-# LANGUAGE TypeFamilies #-}++-- | Replicated Growable Array (RGA)+module CRDT.Cm.RGA+    ( RGA (..)+    , RgaIntent (..)+    , RgaPayload (..)+    , fromString+    , load+    , toString+    , toVector+    ) where++import           Prelude hiding (lookup)++import           Control.Monad.Fail (MonadFail)+import           Control.Monad.State.Strict (MonadState)+import           Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import           Data.Semigroup ((<>))+import           Data.Vector (Vector, (//))+import qualified Data.Vector as Vector++import           CRDT.Cm (CausalOrd, CmRDT, Intent, Payload, apply, initial,+                          makeAndApplyOp, makeOp, precedes)+import           CRDT.LamportClock (Clock, LamportTime (LamportTime), advance,+                                    getTime)++-- | Using 'LamportTime' as an identifier for vertices+type VertexId = LamportTime++data RgaPayload a = RgaPayload+    { vertices  :: Vector (VertexId, Maybe a) -- TODO(cblp, 2018-02-06) Unbox+    , vertexIxs :: Map VertexId Int+      -- ^ indices in `vertices` vector+    }+    deriving (Eq, Show)++-- | Is added and is not removed.+lookup :: VertexId -> RgaPayload a -> Bool+lookup v RgaPayload{vertices, vertexIxs} =+    case Map.lookup v vertexIxs of+        Just ix -> case vertices Vector.! ix of+            (_, Just _) -> True+            _           -> False+        Nothing -> False++-- before :: Vertex -> Vertex -> Bool+-- before u v = b+--     pre lookup(u) ∧ lookup(v)+--     ∃w_1, ..., w_m ∈ verticesAdded:+--         w_1 = u+--         ∧ w_m = v+--         ∧ ∀j: (w_j, w_{j+1}) ∈ edges++data RgaIntent a+    = AddAfter (Maybe VertexId) a+      -- ^ 'Nothing' means the beginning+    | Remove VertexId+    deriving (Show)++data RGA a+    = OpAddAfter (Maybe VertexId) a VertexId+      -- ^ - id of previous vertex, 'Nothing' means the beginning+      --   - atom+      --   - id of this vertex+    | OpRemove VertexId+    deriving (Eq, Show)++instance CausalOrd (RGA a) where+    precedes _ _ = False++emptyPayload :: RgaPayload a+emptyPayload = RgaPayload+    { vertices = Vector.empty+    , vertexIxs = Map.empty+    }++instance Ord a => CmRDT (RGA a) where+    type Intent  (RGA a) = RgaIntent  a+    type Payload (RGA a) = RgaPayload a++    initial = emptyPayload++    makeOp (AddAfter mOldId atom) payload = case mOldId of+        Nothing -> ok+        Just oldId+            | lookup oldId payload -> ok+            | otherwise            -> Nothing+      where+        RgaPayload{vertexIxs} = payload+        ok = Just $ do+            case Map.lookupMax vertexIxs of+                Just (LamportTime maxKnownTime _, _) ->+                    advance maxKnownTime+                Nothing -> pure ()+            newId <- getTime+            pure $ OpAddAfter mOldId atom newId++    makeOp (Remove w) payload+        | lookup w payload = Just . pure $ OpRemove w+        | otherwise        = Nothing++    apply (OpAddAfter mOldId newAtom newId) payload =+        RgaPayload+            { vertices  = vertices'+            , vertexIxs = vertexIxs'+            }+      where+        RgaPayload{vertices, vertexIxs} = payload+        n = length vertices++        (vertices', newIx)+            | null vertices = case mOldId of+                Nothing    -> (Vector.singleton (newId, Just newAtom), 0)+                Just oldId -> error $ show oldId <> " not delivered"+            | otherwise = (insert ix, ix)+              where+                ix = findWhereToInsert $ case mOldId of+                    Nothing    -> 0+                    Just oldId -> vertexIxs Map.! oldId + 1++        vertexIxs' = Map.insert newId newIx $ Map.map shift vertexIxs++        shift ix+            | ix >= newIx = ix + 1+            | otherwise   = ix++        -- Find an edge (l, r) within which to splice new+        findWhereToInsert ix =+            case vertices Vector.!? ix of+                Just (t', _) | newId < t' -> -- Right position, wrong order+                    findWhereToInsert $ succ ix+                _ -> ix++        insert ix+            | ix < n = left <> Vector.singleton (newId, Just newAtom) <> right+            | otherwise = Vector.snoc vertices (newId, Just newAtom)+          where+            (left, right) = Vector.splitAt ix vertices++    apply (OpRemove vid) payload@RgaPayload{vertices, vertexIxs} =+        -- pre addAfter(_, w) delivered  -- 2P-Set precondition+        payload{vertices = vertices // [(ix, (vid, Nothing))]}+      where+        ix = vertexIxs Map.! vid++fromList+    :: (Ord a, Clock m, MonadFail m, MonadState (RgaPayload a) m)+    => [a] -> m [RGA a]+fromList = go Nothing+  where+    go _      []     = pure []+    go prevId (x:xs) = do+        op@(OpAddAfter _ _ newId) <- makeAndApplyOp (AddAfter prevId x)+        (op :) <$> go (Just newId) xs++toList :: RgaPayload a -> [a]+toList RgaPayload{vertices} = [a | (_, Just a) <- Vector.toList vertices]++toVector :: RgaPayload a -> Vector a+toVector RgaPayload{vertices} = Vector.mapMaybe snd vertices++fromString+    :: (Clock m, MonadFail m, MonadState (RgaPayload Char) m)+    => String -> m [RGA Char]+fromString = fromList++toString :: RgaPayload Char -> String+toString = toList++load :: Vector (VertexId, Maybe a) -> RgaPayload a+load vertices = RgaPayload+    { vertices+    , vertexIxs = Map.fromList+        [(vid, ix) | ix <- [0..] | (vid, _) <- Vector.toList vertices]+    }

@@ -6,9 +6,8 @@     ( TwoPSet (..)     ) where -import           Control.Monad (guard)-import           Data.Set (Set)-import qualified Data.Set as Set+import           Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map  import           CRDT.Cm (CausalOrd (..), CmRDT (..)) @@ -16,15 +15,21 @@     deriving (Eq, Show)  instance Ord a => CmRDT (TwoPSet a) where-    type Payload (TwoPSet a) = Set a+    type Payload (TwoPSet a) = Map a Bool -    makeOp op s = case op of-        Add _     -> Just (pure op)-        Remove a  -> guard (Set.member a s) *> Just (pure op)+    initial = Map.empty +    makeOp op payload = case op of+        Add    _ -> Just $ pure op+        Remove a+            | isKnown a -> Just $ pure op+            | otherwise -> Nothing+      where+        isKnown a = Map.member a payload+     apply = \case-        Add a     -> Set.insert a-        Remove a  -> Set.delete a+        Add    a -> Map.insertWith (&&) a True+        Remove a -> Map.insert          a False  instance Eq a => CausalOrd (TwoPSet a) where     Add b `precedes` Remove a = a == b -- `Remove e` can occur only after `Add e`

@@ -35,13 +35,13 @@ add :: (Ord a, Clock m) => a -> LwwElementSet a -> m (LwwElementSet a) add value old@(LES m) = do     advanceFromLES old-    tag <- LWW.initial True+    tag <- LWW.initialize True     pure . LES $ Map.insertWith (<>) value tag m  remove :: (Ord a, Clock m) => a -> LwwElementSet a -> m (LwwElementSet a) remove value old@(LES m) = do     advanceFromLES old-    tag <- LWW.initial False+    tag <- LWW.initialize False     pure . LES $ Map.insertWith (<>) value tag m  lookup :: Ord a => a -> LwwElementSet a -> Bool

@@ -0,0 +1,108 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ParallelListComp #-}+{-# LANGUAGE TupleSections #-}++module CRDT.Cv.RGA+    ( RGA (..)+    , fromList+    , toList+    , edit+    , RgaString+    , fromString+    , toString+    -- * Packed representation+    , RgaPacked+    , pack+    , unpack+    ) where++import           Data.Algorithm.Diff (Diff (Both, First, Second), getDiffBy)+import           Data.Function (on)+import           Data.Semigroup (Semigroup, (<>))+import           Data.Semilattice (Semilattice)+import           Data.Traversable (for)++import           CRDT.LamportClock (Clock, LamportTime (LamportTime), getTime)++type VertexId = LamportTime++-- | TODO(cblp, 2018-02-06) Vector.Unboxed+newtype RGA a = RGA [(VertexId, Maybe a)]+    deriving (Eq, Show)++type RgaString = RGA Char++merge :: Eq a => RGA a -> RGA a -> RGA a+merge (RGA vertices1) (RGA vertices2) =+    RGA $ mergeVertexLists vertices1 vertices2+  where+    mergeVertexLists []                   vs2                  = vs2+    mergeVertexLists vs1                  []                   = vs1+    mergeVertexLists (v1@(id1, a1) : vs1) (v2@(id2, a2) : vs2) =+        case compare id1 id2 of+            LT -> v2                      : mergeVertexLists (v1:vs1) vs2+            GT -> v1                      : mergeVertexLists vs1      (v2:vs2)+            EQ -> (id1, mergeAtoms a1 a2) : mergeVertexLists vs1      vs2++    mergeAtoms (Just a1) (Just a2)+        | a1 == a2 = Just a1+    mergeAtoms _ _ = Nothing++instance Eq a => Semigroup (RGA a) where+    (<>) = merge++instance Eq a => Semilattice (RGA a)++-- Why not?+instance Eq a => Monoid (RGA a) where+    mempty = RGA []+    mappend = (<>)++toList :: RGA a -> [a]+toList (RGA rga) = [a | (_, Just a) <- rga]++toString :: RgaString -> String+toString = toList++fromList :: Clock m => [a] -> m (RGA a)+fromList = fmap RGA . traverse makeVertex+  where+    makeVertex a = do+        t <- getTime+        pure (t, Just a)++fromString :: Clock m => String -> m RgaString+fromString = fromList++-- | Replace content with specified,+-- applying changed found by the diff algorithm+edit :: (Eq a, Clock m) => [a] -> RGA a -> m (RGA a)+edit newList (RGA oldRga) =+    fmap RGA $ for diff $ \case+        First  (vid, _)        -> pure (vid, Nothing)+        Both   v        _      -> pure v+        Second          (_, a) -> (, a) <$> getTime+  where+    newList' = [(undefined, Just a) | a <- newList]+    diff = getDiffBy ((==) `on` snd) oldRga newList' -- TODO(cblp, 2018-02-07) getGroupedDiffBy++-- | Compact version of 'RGA'.+-- For each 'VertexId', the corresponding sequence of vetices has the same 'Pid'+-- and sequentially growing 'LocalTime', starting with the specified one.+type RgaPacked a = [(VertexId, [Maybe a])]++pack :: RGA a -> RgaPacked a+pack (RGA []) = []+pack (RGA ((first, atom):vs)) = go first [atom] 1 vs+  where+    -- TODO(cblp, 2018-02-08) buf :: DList+    go vid buf _ [] = [(vid, buf)]+    go vid buf dt ((wid, a):ws)+        | wid == next dt vid = go vid (buf ++ [a]) (succ dt) ws+        | otherwise = (vid, buf) : go wid [a] 1 ws+    next dt (LamportTime t p) = LamportTime (t + dt) p++unpack :: RgaPacked a -> RGA a+unpack packed = RGA $ do+    (LamportTime time pid, atoms) <- packed+    [(LamportTime (time + i) pid, atom) | i <- [0..] | atom <- atoms]

@@ -2,14 +2,12 @@     ( TwoPSet (..)     , add     , initial-    , lookup+    , member     , remove     , singleton     , isKnown     ) where -import           Prelude hiding (lookup)- import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import           Data.Maybe (fromMaybe)@@ -31,8 +29,8 @@ initial :: TwoPSet a initial = TwoPSet Map.empty -lookup :: Ord a => a -> TwoPSet a -> Bool-lookup e (TwoPSet m) = fromMaybe False $ Map.lookup e m+member :: Ord a => a -> TwoPSet a -> Bool+member e (TwoPSet m) = fromMaybe False $ Map.lookup e m  remove :: Ord a => a -> TwoPSet a -> TwoPSet a remove e (TwoPSet m) = TwoPSet $ Map.adjust (const False) e m@@ -40,6 +38,6 @@ singleton :: Ord a => a -> TwoPSet a singleton a = add a initial --- | XXX Internal TODO remove+-- | XXX Internal isKnown :: Ord a => a -> TwoPSet a -> Bool isKnown e (TwoPSet m) = Map.member e m

@@ -1,10 +1,11 @@+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE TypeFamilies #-}  module CRDT.LWW     ( LWW (..)       -- * CvRDT-    , initial+    , initialize     , assign     , query       -- * Implementation detail@@ -47,15 +48,15 @@ instance Eq a => Semilattice (LWW a)  -- | Initialize state-initial :: Clock m => a -> m (LWW a)-initial value = LWW value <$> getTime+initialize :: Clock m => a -> m (LWW a)+initialize value = LWW value <$> getTime  -- | Change state as CvRDT operation. -- Current value is ignored, because new timestamp is always greater. assign :: Clock m => a -> LWW a -> m (LWW a) assign value old = do     advanceFromLWW old-    initial value+    initialize value  -- | Query state query :: LWW a -> a@@ -69,11 +70,17 @@  instance Eq a => CmRDT (LWW a) where     type Intent  (LWW a) = a-    type Payload (LWW a) = LWW a+    type Payload (LWW a) = Maybe (LWW a) -    makeOp value = Just . assign value+    initial = Nothing -    apply = (<>)+    makeOp value = Just . \case+        Just payload -> assign value payload+        Nothing      -> initialize value++    apply op = Just . \case+        Just payload -> op <> payload+        Nothing      -> op  advanceFromLWW :: Clock m => LWW a -> m () advanceFromLWW LWW{time = LamportTime time _} = advance time

@@ -1,4 +1,7 @@+{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE StrictData #-}  module CRDT.LamportClock     ( Pid (..)@@ -7,11 +10,6 @@     , LamportTime (..)     , LocalTime     , Process (..)-    -- * Lamport clock simulation-    , LamportClockSim (..)-    , ProcessSim (..)-    , runLamportClockSim-    , runProcessSim     -- * Real Lamport clock     , LamportClock     , runLamportClock@@ -23,13 +21,9 @@                                          readTVar, writeTVar) import           Control.Monad.IO.Class (MonadIO, liftIO) import           Control.Monad.Reader (ReaderT, ask, runReaderT)-import           Control.Monad.State.Strict (State, evalState, modify, state) import           Control.Monad.Trans (lift) import           Data.Binary (decode) import qualified Data.ByteString.Lazy as BSL-import           Data.Map.Strict (Map)-import qualified Data.Map.Strict as Map-import           Data.Maybe (fromMaybe) import           Data.Time.Clock.POSIX (getPOSIXTime) import           Data.Word (Word64) import           Network.Info (MAC (MAC), getNetworkInterfaces, mac)@@ -39,37 +33,19 @@ -- | Unix time in 10^{-7} seconds (100 ns), as in RFC 4122 and Swarm RON. type LocalTime = Natural -data LamportTime = LamportTime !LocalTime !Pid-    deriving (Eq, Ord, Show)+data LamportTime = LamportTime LocalTime Pid+    deriving (Eq, Ord) +instance Show LamportTime where+    show (LamportTime time (Pid pid)) = show time ++ '.' : show pid+ -- | Unique process identifier newtype Pid = Pid Word64     deriving (Eq, Ord, Show) --- | Lamport clock simpulation. Key is 'Pid'.--- Non-present value is equivalent to 0.-newtype LamportClockSim a = LamportClockSim (State (Map Pid LocalTime) a)-    deriving (Applicative, Functor, Monad)---- | ProcessSim inside Lamport clock simpulation.-newtype ProcessSim a = ProcessSim (ReaderT Pid LamportClockSim a)-    deriving (Applicative, Functor, Monad)- class Monad m => Process m where     getPid :: m Pid -runLamportClockSim :: LamportClockSim a -> a-runLamportClockSim (LamportClockSim action) = evalState action mempty--runProcessSim :: Pid -> ProcessSim a -> LamportClockSim a-runProcessSim pid (ProcessSim action) = runReaderT action pid--preIncrementAt :: Pid -> LamportClockSim LocalTime-preIncrementAt pid =-    LamportClockSim . state $ \m -> let-        lt' = succ . fromMaybe 0 $ Map.lookup pid m-        in (lt', Map.insert pid lt' m)- getRealLocalTime :: IO LocalTime getRealLocalTime = round . (* 10000000) <$> getPOSIXTime @@ -90,19 +66,6 @@ class Process m => Clock m where     getTime :: m LamportTime     advance :: LocalTime -> m ()--instance Process ProcessSim where-    getPid = ProcessSim ask--instance Clock ProcessSim where-    getTime = ProcessSim $ do-        pid <- ask-        time <- lift $ preIncrementAt pid-        pure $ LamportTime time pid--    advance time = ProcessSim $ do-        pid <- ask-        lift . LamportClockSim . modify $ Map.insertWith max pid time  -- TODO(cblp, 2018-01-06) benchmark and compare with 'atomicModifyIORef' newtype LamportClock a = LamportClock (ReaderT (TVar LocalTime) IO a)

@@ -0,0 +1,119 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}++module CRDT.LamportClock.Simulation+    (+    -- * Lamport clock simulation+      LamportClockSim+    , LamportClockSimT (..)+    , ProcessSim+    , ProcessSimT (..)+    , runLamportClockSim+    , runLamportClockSimT+    , runProcessSim+    , runProcessSimT+    ) where++import           Control.Monad.Except (ExceptT, MonadError, runExceptT,+                                       throwError)+import           Control.Monad.Fail (MonadFail, fail)+import           Control.Monad.Reader (ReaderT, ask, runReaderT)+import           Control.Monad.RWS.Strict (RWST, evalRWS, evalRWST)+import           Control.Monad.State.Strict (MonadState, get, gets, modify, put,+                                             state)+import           Control.Monad.Trans (MonadTrans, lift)+import           Data.Functor.Identity (Identity)+import           Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map++import           CRDT.LamportClock (Clock, LamportTime (LamportTime), LocalTime,+                                    Pid, Process, advance, getPid, getTime)++-- | Lamport clock simulation. Key is 'Pid'.+-- Non-present value is equivalent to (0, initial).+newtype LamportClockSimT s m a =+    LamportClockSim (ExceptT String (RWST s () (Map Pid (ProcessState s)) m) a)+    deriving (Applicative, Functor, Monad, MonadError String)++instance MonadTrans (LamportClockSimT s) where+    lift = LamportClockSim . lift . lift++instance Monad m => MonadFail (LamportClockSimT s m) where+    fail = throwError++type LamportClockSim s = LamportClockSimT s Identity++data ProcessState s = ProcessState+    { time :: LocalTime+    , var  :: s+    }++-- | ProcessSim inside Lamport clock simulation.+newtype ProcessSimT s m a = ProcessSim (ReaderT Pid (LamportClockSimT s m) a)+    deriving (Applicative, Functor, Monad, MonadFail)++type ProcessSim s = ProcessSimT s Identity++instance MonadTrans (ProcessSimT s) where+    lift = ProcessSim . lift . lift++instance Monad m => Process (ProcessSimT s m) where+    getPid = ProcessSim ask++instance Monad m => Clock (ProcessSimT s m) where+    getTime = ProcessSim $ do+        pid <- ask+        time <- lift $ preIncrementTime pid+        pure $ LamportTime time pid++    advance time = ProcessSim $ do+        pid <- ask+        lift . LamportClockSim $ do+            initial <- ask+            modify $ Map.alter (Just . advancePS initial) pid+      where+        advancePS initial Nothing = ProcessState{time, var = initial}+        advancePS _       (Just ProcessState{time = current, var}) =+            ProcessState{time = max time current, var}++instance Monad m => MonadState s (ProcessSimT s m) where+    get = ProcessSim $ do+        pid <- ask+        lift . LamportClockSim $ do+            initial <- ask+            gets $ maybe initial var . Map.lookup pid+    put var = ProcessSim $ do+        pid <- ask+        lift . LamportClockSim . modify $ Map.alter (Just . putPS) pid+      where+        putPS Nothing                   = ProcessState{time = 0, var}+        putPS (Just ProcessState{time}) = ProcessState{time,     var}++runLamportClockSim :: s -> LamportClockSim s a -> Either String a+runLamportClockSim initial (LamportClockSim action) =+    fst $ evalRWS (runExceptT action) initial mempty++runLamportClockSimT+    :: Monad m => s -> LamportClockSimT s m a -> m (Either String a)+runLamportClockSimT initial (LamportClockSim action) =+    fst <$> evalRWST (runExceptT action) initial mempty++runProcessSim :: Pid -> ProcessSim s a -> LamportClockSim s a+runProcessSim pid (ProcessSim action) = runReaderT action pid++runProcessSimT :: Pid -> ProcessSimT s m a -> LamportClockSimT s m a+runProcessSimT pid (ProcessSim action) = runReaderT action pid++preIncrementTime :: Monad m => Pid -> LamportClockSimT s m LocalTime+preIncrementTime pid = LamportClockSim $ do+    initial <- ask+    state $ \pss -> let+        ps@ProcessState{time} =+            case Map.lookup pid pss of+                Nothing -> ProcessState{time = 1, var = initial}+                Just ProcessState{time = current, var} ->+                    ProcessState{time = succ current, var}+        in+        (time, Map.insert pid ps pss)

@@ -0,0 +1,55 @@+module Data.MultiMap+    ( MultiMap (..)+    , assocs+    , delete+    , deleteMany+    , empty+    , insert+    , keysSet+    , lookup+    , singleton+    ) where++import           Prelude hiding (lookup)++import           Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import           Data.Maybe (fromMaybe)+import           Data.Semigroup ((<>))+import           Data.Set (Set)+import qualified Data.Set as Set++newtype MultiMap k v = MultiMap (Map k (Set v))+    deriving (Eq, Show)++assocs :: MultiMap k v -> [(k, [v])]+assocs (MultiMap m) = Map.assocs $ Set.toList <$> m++delete :: (Ord k, Ord v) => k -> v -> MultiMap k v -> MultiMap k v+delete k v (MultiMap m) = MultiMap $ Map.update delete' k m+  where+    delete' s = let s' = Set.delete v s in if null s' then Nothing else Just s'++deleteMany ::+    (Ord k, Ord v) => k -> Set v -> MultiMap k v -> MultiMap k v+deleteMany k vs (MultiMap m) = MultiMap $ Map.update deleteMany' k m+  where+    deleteMany' s =+        let s' = Set.difference s vs in if null s' then Nothing else Just s'++empty :: MultiMap k v+empty = MultiMap Map.empty++insert :: (Ord k, Ord v) => k -> v -> MultiMap k v -> MultiMap k v+insert k v (MultiMap m) =+    MultiMap $ Map.insertWith (<>) k (Set.singleton v) m++keysSet :: MultiMap k v -> Set k+keysSet (MultiMap m) = Map.keysSet m++-- | If no key in the map then the result is empty.+lookup :: Ord k => k -> MultiMap k v -> Set v+lookup k (MultiMap m) = fromMaybe Set.empty $ Map.lookup k m++singleton :: k -> v -> MultiMap k v+singleton k v = MultiMap $ Map.singleton k $ Set.singleton v

@@ -2,27 +2,34 @@  {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE StandaloneDeriving #-}  module ArbitraryOrphans () where  import           Test.QuickCheck (Arbitrary (..), arbitraryBoundedEnum,-                                  elements)+                                  elements, frequency, oneof) import           Test.QuickCheck.Gen (Gen (MkGen)) import           Test.QuickCheck.Instances () import           Test.QuickCheck.Random (mkQCGen)  import           CRDT.Cm.Counter (Counter (..)) import           CRDT.Cm.GSet (GSet (..))-import qualified CRDT.Cm.TwoPSet as Cm+import qualified CRDT.Cm.ORSet as CmORSet+import qualified CRDT.Cm.RGA as CmRGA+import qualified CRDT.Cm.TwoPSet as CmTwoPSet import           CRDT.Cv.GCounter (GCounter (..)) import           CRDT.Cv.LwwElementSet (LwwElementSet (..))-import           CRDT.Cv.ORSet (ORSet (..))+import qualified CRDT.Cv.ORSet as CvORSet import           CRDT.Cv.PNCounter (PNCounter (..))-import qualified CRDT.Cv.TwoPSet as Cv+import qualified CRDT.Cv.RGA as CvRGA+import qualified CRDT.Cv.TwoPSet as CvTwoPSet import           CRDT.LamportClock (LamportTime (..), Pid (..)) import           CRDT.LWW (LWW (..))+import           Data.MultiMap (MultiMap (..)) +import           Util (pattern (:-))+ instance Arbitrary (Counter a) where     arbitrary = arbitraryBoundedEnum @@ -36,19 +43,54 @@  deriving instance Arbitrary a => Arbitrary (GSet a) -instance Arbitrary a => Arbitrary (Cm.TwoPSet a) where-    arbitrary = elements [Cm.Add, Cm.Remove] <*> arbitrary+deriving instance+        (Arbitrary k, Ord k, Arbitrary v, Ord v) => Arbitrary (MultiMap k v) +instance Arbitrary a => Arbitrary (CmORSet.Intent a) where+    arbitrary = elements [CmORSet.Add, CmORSet.Remove] <*> arbitrary++instance Arbitrary a => Arbitrary (CmORSet.ORSet a) where+    arbitrary = oneof+        [ CmORSet.OpAdd    <$> arbitrary <*> arbitrary+        , CmORSet.OpRemove <$> arbitrary <*> arbitrary+        ]++instance (Arbitrary a, Ord a) => Arbitrary (CmORSet.Payload a) where+    arbitrary = CmORSet.Payload <$> arbitrary <*> arbitrary++instance Arbitrary CmORSet.Tag where+    arbitrary = CmORSet.Tag <$> arbitrary <*> arbitrary++instance Arbitrary a => Arbitrary (CmRGA.RGA a) where+    arbitrary = oneof+        [ CmRGA.OpAddAfter <$> arbitrary <*> arbitrary <*> arbitrary+        , CmRGA.OpRemove   <$> arbitrary+        ]++instance Arbitrary a => Arbitrary (CmRGA.RgaIntent a) where+    arbitrary = frequency+        [ 10 :- CmRGA.AddAfter <$> arbitrary <*> arbitrary+        ,  1 :- CmRGA.Remove   <$> arbitrary+        ]++instance (Arbitrary a, Ord a) => Arbitrary (CmRGA.RgaPayload a) where+    arbitrary = CmRGA.load <$> arbitrary++instance Arbitrary a => Arbitrary (CmTwoPSet.TwoPSet a) where+    arbitrary = elements [CmTwoPSet.Add, CmTwoPSet.Remove] <*> arbitrary+ deriving instance Arbitrary a => Arbitrary (GCounter a) -deriving instance (Arbitrary a, Ord a) => Arbitrary (ORSet a)+deriving instance (Arbitrary a, Ord a) => Arbitrary (CvORSet.ORSet a)  deriving instance (Arbitrary a, Ord a) => Arbitrary (LwwElementSet a)  instance Arbitrary a => Arbitrary (PNCounter a) where     arbitrary = PNCounter <$> arbitrary <*> arbitrary -deriving instance (Ord a, Arbitrary a) => Arbitrary (Cv.TwoPSet a)+deriving instance Arbitrary a => Arbitrary (CvRGA.RGA a)++deriving instance (Ord a, Arbitrary a) => Arbitrary (CvTwoPSet.TwoPSet a)  instance Arbitrary LamportTime where     arbitrary = LamportTime <$> arbitrary <*> arbitrary

@@ -0,0 +1,44 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Cm.ORSet where++import qualified Data.MultiMap as MultiMap+import           Test.QuickCheck (counterexample, (.&&.), (===), (==>))++import           CRDT.Cm (initial, makeAndApplyOp, query)+import           CRDT.Cm.ORSet (Intent (Add, Remove), ORSet, Tag (Tag),+                                elements)+import           CRDT.LamportClock.Simulation (runLamportClockSim,+                                               runProcessSim)++import           Laws (cmrdtLaw)+import           Util (pattern (:-), expectRight)++prop_Cm = cmrdtLaw @(ORSet Char)++-- | Example from fig. 14 from "A comprehensive study of CRDTs"+prop_fig14 α β a = expectRight . runLamportClockSim (initial @(ORSet Char)) $ do+    op1 <- runProcessSim β $ makeAndApplyOp (Add (a :: Char))+    op2 <- runProcessSim α $ makeAndApplyOp (Add a)+    op3 <- runProcessSim α $ makeAndApplyOp (Remove a)+    pure $+        α < β ==>+        check "2"   [op2]           [a :- [Tag α 0]]          .&&.+        check "23"  [op2, op3]      []                        .&&.+        check "231" [op2, op3, op1] [a :- [Tag β 0]]          .&&.+        check "1"   [op1]           [a :- [Tag β 0]]          .&&.+        check "12"  [op1, op2]      [a :- [Tag α 0, Tag β 0]] .&&.+        check "123" [op1, op2, op3] [a :- [Tag β 0]]+  where+    check opsLabel ops result =+        counterexample ("ops = " ++ opsLabel) $+        counterexample ("ops = " ++ show ops) $+        query' ops === result++query' :: (Ord a, Foldable f) => f (ORSet a) -> [(a, [Tag])]+query' = MultiMap.assocs . elements . query

@@ -4,10 +4,16 @@  module Cm.TwoPSet where -import           CRDT.Cm.TwoPSet (TwoPSet)+import           Test.QuickCheck (Small) -import           Laws (cmrdtLaw)+import           CRDT.Cm.TwoPSet (TwoPSet (Remove)) +import           Laws (cmrdtLaw, opCommutativity)+ prop_Cm = cmrdtLaw @(TwoPSet Char) --- prop_add =+prop_remove_commutes_with_itself e = opCommutativity intentOp intentOp+  where+    intent = Remove (e :: Small Int)+    op = intent+    intentOp = (intent, op)

@@ -0,0 +1,28 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Cv.ORSet where++import           Prelude hiding (lookup)++import           Data.Semigroup (Semigroup ((<>)))++import           CRDT.Cv.ORSet (ORSet, add, lookup, remove)+import           CRDT.LamportClock.Simulation (runLamportClockSim,+                                               runProcessSim)++import           Laws (cvrdtLaws)+import           Util (expectRight)++test_Cv = cvrdtLaws @(ORSet Int)++prop_add pid (x :: Char) s = expectRight . runLamportClockSim undefined $+    runProcessSim pid $ not . lookup x . remove x <$> add x s++-- | Difference from 'LwwElementSet' --+-- other replica can not accidentally delete x+prop_add_merge (x :: Char) pid s1 s0 = expectRight $+    runLamportClockSim undefined $+        runProcessSim pid $ lookup x . (<> s1) <$> add x s0

@@ -0,0 +1,27 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++{-# LANGUAGE TypeApplications #-}++module Cv.RGA where++import           Test.QuickCheck ((===))++import           CRDT.Cv.RGA (RgaString, edit, fromString, pack, toString,+                              unpack)+import           CRDT.LamportClock.Simulation (runLamportClockSim,+                                               runProcessSim)++import           Laws (cvrdtLaws)+import           Util (expectRight)++prop_fromString_toString s pid = expectRight $ do+    s' <- runLamportClockSim undefined $ runProcessSim pid $ fromString s+    pure $ toString s' === s++test_Cv = cvrdtLaws @RgaString++prop_edit v1 s2 pid = expectRight . runLamportClockSim undefined $ do+    v2 <- runProcessSim pid $ edit s2 v1+    pure $ toString v2 === s2++prop_pack_unpack rga = unpack (pack rga) == (rga :: RgaString)

@@ -5,23 +5,21 @@  module Cv.TwoPSet where -import           Prelude hiding (lookup)- import           Test.QuickCheck ((==>)) -import           CRDT.Cv.TwoPSet (TwoPSet (..), add, isKnown, lookup, remove)+import           CRDT.Cv.TwoPSet (TwoPSet (..), add, isKnown, member, remove)  import           Laws (cvrdtLaws)  -- | Difference from LwwElementSet and ORSet -- removal bias prop_removal_bias (s :: TwoPSet Char) x =-    not . lookup x . add x . remove x $ add x s+    not . member x . add x . remove x $ add x s -prop_add (s :: TwoPSet Char) x = not (isKnown x s) ==> lookup x (add x s)+prop_add (s :: TwoPSet Char) x = not (isKnown x s) ==> member x (add x s) -prop_remove (s :: TwoPSet Char) x = not . lookup x $ remove x s+prop_remove (s :: TwoPSet Char) x = not . member x $ remove x s  prop_add_then_remove (s :: TwoPSet Char) x =-    not . lookup x . remove x $ add x s+    not . member x . remove x $ add x s  test_Cv = cvrdtLaws @(TwoPSet Char)

@@ -14,23 +14,25 @@ import           Data.Semigroup ((<>)) import           Test.QuickCheck ((===)) -import           CRDT.LamportClock (runLamportClockSim, runProcessSim)-import           CRDT.LWW (LWW, assign, initial, query)+import           CRDT.LamportClock.Simulation (runLamportClockSim,+                                               runProcessSim)+import           CRDT.LWW (LWW, assign, initialize, query)  import           Laws (cmrdtLaw, cvrdtLaws)+import           Util (expectRight)  prop_Cm = cmrdtLaw @(LWW Char)  test_Cv = cvrdtLaws @(LWW Char)  prop_assign pid1 pid2 (formerValue :: Char) latterValue =-    runLamportClockSim $ do-        state1 <- runProcessSim pid1 $ initial formerValue+    expectRight . runLamportClockSim undefined $ do+        state1 <- runProcessSim pid1 $ initialize formerValue         state2 <- runProcessSim pid2 $ assign latterValue state1         pure $ query state2 === latterValue  prop_merge_with_former pid1 pid2 (formerValue :: Char) latterValue =-    runLamportClockSim $ do-        state1 <- runProcessSim pid1 $ initial formerValue+    expectRight . runLamportClockSim undefined $ do+        state1 <- runProcessSim pid1 $ initialize formerValue         state2 <- runProcessSim pid2 $ assign latterValue state1         pure $ query (state1 <> state2) === latterValue

@@ -1,6 +1,8 @@+{-# OPTIONS_GHC -Wno-orphans #-}+ {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}@@ -9,24 +11,28 @@ module Laws     ( cmrdtLaw     , cvrdtLaws+    , opCommutativity     ) where -import           Data.Maybe (fromMaybe, isJust)+import           Control.Monad.State.Strict (MonadState, get, modify)+import           Control.Monad.Trans (lift)+import           Data.Functor.Identity (runIdentity)+import           Data.Maybe (isJust) import           Data.Semigroup (Semigroup, (<>))-import           Test.QuickCheck (Arbitrary (..), Property, counterexample,-                                  discard, property, (.&&.), (===), (==>))+import           QuickCheck.GenT (MonadGen, liftGen, runGenT)+import qualified QuickCheck.GenT as GenT+import           Test.QuickCheck (Arbitrary (..), Property, choose,+                                  counterexample, discard, forAll, getSize,+                                  property, (.&&.), (===), (==>)) import           Test.Tasty (TestTree) import           Test.Tasty.QuickCheck (testProperty)  import           CRDT.Cm (CmRDT (..), concurrent)-import           CRDT.Cm.Counter (Counter)-import           CRDT.Cm.GSet (GSet)-import           CRDT.Cm.TwoPSet (TwoPSet) import           CRDT.Cv (CvRDT)-import           CRDT.LamportClock (Clock, ProcessSim, runLamportClockSim,-                                    runProcessSim)-import           CRDT.LWW (LWW)-import qualified CRDT.LWW as LWW+import           CRDT.LamportClock (Clock)+import           CRDT.LamportClock.Simulation (ProcessSim, ProcessSimT,+                                               runLamportClockSimT,+                                               runProcessSimT) import           Data.Semilattice (Semilattice, merge)  import           ArbitraryOrphans ()@@ -50,54 +56,83 @@ cvrdtLaws :: forall a. (Arbitrary a, CvRDT a, Eq a, Show a) => [TestTree] cvrdtLaws = semilatticeLaws @a -class Initialize op where-    type Initial op-    type Initial op = Payload op--    initialize :: Clock m => Initial op -> m (Payload op)-    default initialize-        :: (Applicative m, Initial op ~ Payload op)-        => Initial op -> m (Payload op)-    initialize = pure--instance Initialize (Counter a)--instance Initialize (GSet a)--instance Initialize (LWW a) where-    type Initial (LWW a) = a-    initialize = LWW.initial--instance Initialize (TwoPSet a)- -- | CmRDT law: concurrent ops commute cmrdtLaw     :: forall op.-    ( CmRDT op-    , Arbitrary op, Show op+    ( CmRDT op, Show op     , Arbitrary (Intent  op), Show (Intent  op)     , Arbitrary (Payload op), Show (Payload op)-    , Initialize op-    , Arbitrary (Initial op), Show (Initial op)     )     => Property cmrdtLaw = property concurrentOpsCommute   where-    concurrentOpsCommute st1 st2 seed3 in1 in2 pid1 pid2 pid3 =-        let (op1, op2, state) = runLamportClockSim $ (,,)-                <$> runProcessSim pid1 (makeOp @op in1 st1 `orElse` discard)-                <*> runProcessSim pid2 (makeOp @op in2 st2 `orElse` discard)-                <*> runProcessSim pid3 (initialize @op seed3)-        in  concurrent op1 op2 ==> opCommutativity (in1, op1) (in2, op2) state-    opCommutativity (in1, op1) (in2, op2) state =-        isJust (makeOp @op @ProcessSim in1 state) ==>-        isJust (makeOp @op @ProcessSim in2 state) ==>-            counterexample-                ( show in1 ++ " must be valid after " ++ show op2 ++-                  " applied to " ++ show state )-                (isJust $ makeOp @op @ProcessSim in1 $ apply op2 state)-            .&&.-            (apply op1 . apply op2) state === (apply op2 . apply op1) state+    concurrentOpsCommute payload pid1 pid2 pid3 =+        pid1 < pid2 && pid2 < pid3 ==>+        forAll genOps $ \case+            Right ((in1, op1), (in2, op2), state3) ->+                concurrent op1 op2 ==>+                opCommutativity (in1, op1) (in2, op2) state3+            Left _ -> discard+      where+        genOps = fmap runIdentity $ runGenT $ runLamportClockSimT payload $ (,,)+            <$> runProcessSimT pid1 (do+                    _ <- genAndApplyOps @op+                    genAndApplyOp @op)+            <*> runProcessSimT pid2 (do+                    _ <- genAndApplyOps @op+                    genAndApplyOp @op)+            <*> runProcessSimT pid3 (do+                    _ <- genAndApplyOps @op+                    get) -orElse :: Maybe a -> a -> a-orElse = flip fromMaybe+opCommutativity+    :: forall op.+    (CmRDT op, Show op, Show (Intent  op), Show (Payload op))+    => (Intent op, op) -- ^ the op must be made from the intent+    -> (Intent op, op) -- ^ the op must be made from the intent+    -> Payload op -- ^ any reachable state+    -> Property+opCommutativity (in1, op1) (in2, op2) state =+    isJust (makeOp' in1 state) ==>+    isJust (makeOp' in2 state) ==>+        counterexample+            ( show in2 ++ " must be valid after " ++ show op1 +++              " applied to " ++ show state )+            (isJust $ makeOp' in2 $ apply op1 state)+        .&&.+        (apply op1 . apply op2) state === (apply op2 . apply op1) state+  where+    makeOp' = makeOp @op @(ProcessSim (Payload op))++genAndApplyOp+    :: ( CmRDT op, Arbitrary (Intent op)+       , Clock m, MonadState (Payload op) m, MonadGen m+       , Show op, Show (Intent op), Show (Payload op)+       )+    => m (Intent op, op)+genAndApplyOp = do+    payload <- get+    intent <- liftGen arbitrary+    case makeOp intent payload of+        Nothing -> genAndApplyOp+        Just opAction -> do+            op <- opAction+            modify $ apply op+            pure (intent, op)++genAndApplyOps+    :: ( CmRDT op, Arbitrary (Intent op)+       , Clock m, MonadState (Payload op) m, MonadGen m+       , Show op, Show (Intent op), Show (Payload op)+       )+    => m [(Intent op, op)]+genAndApplyOps = GenT.listOf genAndApplyOp++instance MonadGen m => MonadGen (ProcessSimT s m) where+    liftGen = lift . liftGen+    variant = undefined+    sized f = do+        size <- liftGen getSize+        f size+    resize = undefined+    choose = liftGen . choose

@@ -16,26 +16,28 @@ import           Data.Semigroup ((<>))  import           CRDT.Cv.LwwElementSet (LwwElementSet, add, lookup, remove)-import           CRDT.LamportClock (runLamportClockSim, runProcessSim)+import           CRDT.LamportClock.Simulation (runLamportClockSim,+                                               runProcessSim)  import           Laws (cvrdtLaws)+import           Util (expectRight)  test_Cv = cvrdtLaws @(LwwElementSet Char)  prop_add (s :: LwwElementSet Char) x pid1 =-    runLamportClockSim $ do+    expectRight . runLamportClockSim undefined $ do         s1 <- runProcessSim pid1 $ add x s         pure $ lookup x s1  prop_remove (s :: LwwElementSet Char) x pid1 pid2 =-    runLamportClockSim $ do+    expectRight . runLamportClockSim undefined $ do         s1 <- runProcessSim pid1 $ add x s         s2 <- runProcessSim pid2 $ remove x s1         pure . not $ lookup x s2  -- | Difference from 'TwoPSet' -- no removal bias prop_no_removal_bias (s :: LwwElementSet Char) x pid1 pid2 pid3 =-    runLamportClockSim $ do+    expectRight . runLamportClockSim undefined $ do         s1 <- runProcessSim pid1 $ add x s         s2 <- runProcessSim pid2 $ remove x s1         s3 <- runProcessSim pid3 $ add x s2@@ -43,7 +45,7 @@  -- | Difference from 'ORSet' -- other replica can accidentally delete x prop_they_accidentally_delete_our_value (s :: LwwElementSet Char) x pid1 pid2 =-    runLamportClockSim $ do+    expectRight . runLamportClockSim undefined $ do         s1 <- runProcessSim pid1 $ add x s         s2 <- runProcessSim pid2 $ remove x =<< add x s         pure . not . lookup x $ s1 <> s2

@@ -1,25 +0,0 @@-{-# OPTIONS_GHC -Wno-missing-signatures #-}--{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}--module ORSet where--import           Prelude hiding (lookup)--import           Data.Semigroup (Semigroup ((<>)))--import           CRDT.Cv.ORSet (ORSet, add, lookup, remove)-import           CRDT.LamportClock (runLamportClockSim, runProcessSim)--import           Laws (cvrdtLaws)--test_Cv = cvrdtLaws @(ORSet Int)--prop_add pid (x :: Char) s =-    runLamportClockSim $ runProcessSim pid $ not . lookup x . remove x <$> add x s---- | Difference from 'LwwElementSet' ----- other replica can not accidentally delete x-prop_add_merge (x :: Char) pid s1 s0 =-    runLamportClockSim $ runProcessSim pid $ lookup x . (<> s1) <$> add x s0

@@ -0,0 +1,81 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++{-# LANGUAGE ParallelListComp #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeApplications #-}++module RGA where++import           Control.Monad.State.Strict (get)+import           Data.Maybe (isJust)+import qualified Data.Vector as Vector+import           Test.QuickCheck (conjoin, counterexample, (===))++import           CRDT.Cm (apply, initial, makeAndApplyOp, makeOp)+import           CRDT.Cm.RGA (RGA (OpAddAfter), RgaIntent (AddAfter),+                              fromString, load, toString)+import           CRDT.LamportClock (LamportTime (LamportTime), Pid (Pid),+                                    advance)+import           CRDT.LamportClock.Simulation (ProcessSim, runLamportClockSim,+                                               runProcessSim)++import           Laws (cmrdtLaw)+import           Util (pattern (:-), expectRightK)++prop_makeOp =+    isJust+        (makeOp @(RGA Char) (AddAfter Nothing 'a') (initial @(RGA Char))+        :: Maybe (ProcessSim () (RGA Char)))++prop_makeAndApplyOp = conjoin+    [ counterexample "result3"  $ result3  === Right (op3, payload3)+    , counterexample "result2"  $ result2  === Right (op2, payload2)+    , counterexample "result1"  $ result1  === Right (op1, payload1)+    , counterexample "result12" $ result12 === payload12+    , counterexample "results=" $ result21 === result12+    ]+  where+    time1 = LamportTime 4 $ Pid 1+    time2 = LamportTime 4 $ Pid 2+    time3 = LamportTime 3 $ Pid 3+    op1 = OpAddAfter Nothing '1' time1+    op2 = OpAddAfter Nothing '2' time2+    op3 = OpAddAfter Nothing '3' time3+    payload3 = load $ Vector.singleton (time3 :- Just '3')+    payload1 = load $ Vector.fromList [time1 :- Just '1', time3 :- Just '3']+    payload2 = load $ Vector.fromList [time2 :- Just '2', time3 :- Just '3']+    payload12 = load $ Vector.fromList+        [time2 :- Just '2', time1 :- Just '1', time3 :- Just '3']+    result3 = runLamportClockSim (initial @(RGA Char)) $+        runProcessSim (Pid 3) $ do+            advance 2+            (,) <$> makeAndApplyOp @(RGA Char) (AddAfter Nothing '3')+                <*> get+    result2 = runLamportClockSim payload3 $ runProcessSim (Pid 2) $ do+        advance 1+        (,) <$> makeAndApplyOp @(RGA Char) (AddAfter Nothing '2')+            <*> get+    result1 = runLamportClockSim payload3 $ runProcessSim (Pid 1) $+        (,) <$> makeAndApplyOp @(RGA Char) (AddAfter Nothing '1')+            <*> get+    result12 = apply op2 payload1+    result21 = apply op1 payload2++prop_fromString s pid =+    result ===+    Right (load $ Vector.fromList+        [LamportTime t pid :- Just c | t <- [1..] | c <- s])+  where+    result = runLamportClockSim (initial @(RGA Char)) $+        runProcessSim pid $ do+            _ <- fromString s+            get++prop_fromString_toString s pid =+    expectRightK result $ \s' -> toString s' === s+  where+    result = runLamportClockSim (initial @(RGA Char)) $ runProcessSim pid $ do+        _ <- fromString s+        get++prop_Cm = cmrdtLaw @(RGA Char)

@@ -0,0 +1,17 @@+{-# LANGUAGE PatternSynonyms #-}++module Util where++import           Test.QuickCheck (Property, Testable, counterexample, property)++expectRight :: Testable a => Either String a -> Property+expectRight e = expectRightK e id++expectRightK :: Testable b => Either String a -> (a -> b) -> Property+expectRightK e f = case e of+    Left l  -> counterexample l $ property False+    Right a -> property $ f a++pattern (:-) :: a -> b -> (a, b)+pattern a :- b = (a, b)+infix 0 :-