Commit 4beb07b6 authored by Hans-Peter Deifel's avatar Hans-Peter Deifel
Browse files

Merge branch 'test-split'

parents fe73de51 145dda57
......@@ -138,6 +138,7 @@ test-suite spec
, MA.Coalgebra.ParserSpec
, MA.Parser.LexerSpec
, MA.Algorithm.InitializeSpec
, MA.Algorithm.SplitSpec
default-language: Haskell2010
default-extensions: GADTs
, StandaloneDeriving
......@@ -163,6 +164,7 @@ test-suite spec
, microlens-platform
, unordered-containers
, containers
, mtl
, ma
test-suite doctests
......
......@@ -15,11 +15,15 @@ module Data.BlockQueue
, enqueue
, dequeue
, elem
, delete
, clear
, toList
) where
import Prelude hiding (null, elem)
import Control.Monad.ST
import qualified Data.Foldable as Foldable
import Data.Primitive.MutVar
import Data.Sequence (Seq)
......@@ -68,7 +72,7 @@ enqueue q block = unlessM (elem block q) $ do
modifyMutVar (q^.queue) $ \s -> s Seq.|> block
UnboxedV.write (q^.presence) (fromBlock block) True
-- | Read and delete the first element in the queue
-- | Read and delete the first element in the queue.
--
-- Returns 'Nothing' and doesn't modify the queue if it was empty.
--
......@@ -81,8 +85,40 @@ dequeue q = Seq.viewl <$> readMutVar (q^.queue) >>= \case
writeMutVar (q^.queue) rest
return (Just x)
-- | Tests whether an element is in the queue
-- | Tests whether an element is in the queue.
--
-- Runtime: O(1)
elem :: Block -> BlockQueue s -> ST s Bool
elem (Block block) !q = UnboxedV.read (q^.presence) block
-- | Removes all items from the queue.
--
-- Runtime: O(max size of queue)
clear :: BlockQueue s -> ST s ()
clear q = do
writeMutVar (q^.queue) Seq.empty
UnboxedV.set (q^.presence) False
-- | Return a list of currently queued items in the order in which they were
-- added to the queue.
--
-- Runtime: O(n)
toList :: BlockQueue s -> ST s [Block]
toList q = Foldable.toList <$> readMutVar (q^.queue)
-- | Delete the given block from the queue if it is queued or do nothing
-- otherwise.
--
-- The block id must be smaller than the maximum size of the queue.
--
-- Runtime: O(current size of queue)
delete :: Block -> BlockQueue s -> ST s ()
delete (Block b) q = do
UnboxedV.write (q ^. presence) b False
modifyMutVar (q ^. queue) deleteFromSeq
where
deleteFromSeq s = case Seq.elemIndexL (Block b) s of
Nothing -> s
Just idx -> Seq.deleteAt idx s
{-# LANGUAGE BangPatterns #-}
module MA.Algorithm.Split
( SplitM
(
-- * Main interface
SplitM
, split
-- * Internal functions
-- | These are mainly exported for testing and benchmarking. Use 'split' or
-- even better: 'MA.Algorithm.refine'.
, collectTouchedBlocks
, updateBlock
, splitBlock
, addBlocksToQueue
) where
import Prelude hiding (pred)
......@@ -14,7 +26,7 @@ import Data.Maybe (maybeToList)
import Data.STRef
import System.IO.Unsafe (unsafeDupablePerformIO)
import Control.Monad.Extra (unlessM, whenM, ifM)
import Control.Monad.Extra (unlessM, whenM)
import Control.Monad.Reader
import Data.Tuple.Extra (snd3)
import qualified Data.Vector as V
......@@ -43,8 +55,16 @@ split blockS = do
forM_ touchedBlocks $ \(b, v0) -> do
updateBlock b v0
whenM (lift $ Partition.hasMarked (partition as) b) $
splitBlock b
splitBlock b >>= addBlocksToQueue b
-- | Update weights for all marked states in the given block @b@.
--
-- This calls 'update' for all marked states in the block with @[labels to S]@
-- and @weightToC@ as parameters and saves the resulting weight to S in @lastW@.
-- @toSub@ in reset to an empty list for all marked states. Also, the @H3@
-- values returned from 'update' are saved in @h3Cache@.
--
-- As a precondition, toSub must not be empty for marked states.
updateBlock :: forall s h. RefinementInterface h => Block -> H3 h -> SplitM s h ()
updateBlock b v0 = ask >>= \(as, _) -> lift $ do
markB <- Partition.markedStates (partition as) b
......@@ -59,7 +79,7 @@ updateBlock b v0 = ask >>= \(as, _) -> lift $ do
return $! lab)
(!wxS, !vx, !wxCwithoutS) <- RI.update @h labelsToS <$> readSTRef pc
writeSTRef pc wxCwithoutS
writeSTRef pc wxCwithoutS
!ps <- newSTRef wxS
VM.read (toSub as) x >>= \(!edges) -> forM_ edges $ \(EdgeRef !e) ->
......@@ -71,9 +91,13 @@ updateBlock b v0 = ask >>= \(as, _) -> lift $ do
then Partition.unmark (partition as) x
else VM.write (h3Cache as) x $! vx
-- b must have at least one marked state
splitBlock :: RefinementInterface h => Block -> SplitM s h ()
splitBlock b = ask >>= \(as, queue) -> lift $ do
-- | Split block according to marked/unmarked status and saved H3s.
--
-- @b@ must have at least one marked state
--
-- Returns a list of new sub-blocks of @b@
splitBlock :: RefinementInterface h => Block -> SplitM s h [Block]
splitBlock b = ask >>= \(as, _) -> lift $ do
-- b has marked states, so b1 is guaranteed to be non-empty
(Just b1, bunmarked) <- Partition.splitMarked (partition as) b
......@@ -92,15 +116,33 @@ splitBlock b = ask >>= \(as, queue) -> lift $ do
(Just b1', b2) <- Partition.splitBy (partition as) b1
((==pmc) . unsafeH3)
blocks <- ((b1':maybeToList bunmarked) ++) <$> case b2 of
((b1':maybeToList bunmarked) ++) <$> case b2 of
Nothing -> return []
Just b2' -> Partition.groupBy (partition as) b2' unsafeH3
let enqueue = Queue.enqueue queue
ifM (b `Queue.elem` queue) (mapM_ enqueue blocks) $
deleteLargestM (Partition.blockSize (partition as)) (maybeAdd b blocks)
>>= mapM_ enqueue
-- | Add sub-blocks that were split off of a super-block to the queue.
--
-- If the original @b@ is already in the queue, we add all sub-blocks except the
-- one that shares its identity with @b@. If @b@ is not in the queue, we add all
-- blocks except a largest one.
--
-- Runtime: @O(|sub-blocks|)@
addBlocksToQueue
:: RefinementInterface h
=> Block -- ^ Original super-block
-> [Block] -- ^ List of split-off sub-blocks
-> SplitM s h ()
addBlocksToQueue b blocks = ask >>= \(as, queue) -> lift $ do
bInQueue <- Queue.elem b queue
blocks' <- if bInQueue
then return blocks
-- FIXME Is this maybeAdd really needed
else deleteLargestM (Partition.blockSize (partition as)) (maybeAdd b blocks)
mapM_ (Queue.enqueue queue) blocks'
-- | Returns a list of blocks that have at least one predecessor state of the
-- given block @S@.
......
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
module MA.Algorithm.Types
( AlgoState(..)
) where
-- * Lenses
, toSubL
, lastWL
, encodingL
, predL
, partitionL
, h3CacheL
)
where
import Data.STRef
import Data.STRef
import Data.Vector (Vector)
import Data.Vector.Mutable (MVector)
import Data.Vector ( Vector )
import Data.Vector.Mutable ( MVector )
import Lens.Micro.TH
import Data.MorphismEncoding
import Data.RefinablePartition (RefinablePartition)
import MA.Coalgebra.RefinementTypes
import Data.MorphismEncoding
import Data.RefinablePartition ( RefinablePartition )
import MA.Coalgebra.RefinementTypes
data AlgoState s h = AlgoState
{ toSub :: MVector s [EdgeRef]
......@@ -21,3 +31,13 @@ data AlgoState s h = AlgoState
, partition :: RefinablePartition s
, h3Cache :: MVector s (H3 h)
}
makeLensesFor
[ ( "toSub", "toSubL" )
, ( "lastW", "lastWL" )
, ( "encoding", "encodingL" )
, ( "pred", "predL")
, ( "partition", "partitionL")
, ( "h3Cache", "h3CacheL")
]
''AlgoState
......@@ -57,6 +57,8 @@ realValued = FunctorDescription
}
data MonoidWeight m = MonoidWeight !m !m
deriving (Eq, Ord, Show)
data MonoidH3 m = MonoidH3 !m !m !m
deriving (Eq, Ord, Show)
......
......@@ -8,7 +8,7 @@ import Test.Hspec
import Test.QuickCheck
import Control.Monad.ST
import Data.List (delete)
import qualified Data.List as List (delete)
import Data.Vector (Vector)
import qualified Data.Vector as V
......@@ -33,28 +33,28 @@ emptySpec = describe "empty" $ do
enqueueSpec :: Spec
enqueueSpec = describe "enqueue" $ do
it "makes an empty queue non-empty" $
runST (empty 2 >>= \q -> enqueue q 0 >> null q) `shouldBe` False
it "is inverse to enqueue" $
let enqdeq a b = do
q <- empty 10
enqueue q a
enqueue q b
(,) <$> dequeue q <*> dequeue q
in
property $ forAll (elements [0..9]) $ \a -> forAll (elements (delete a [0..9])) $ \b ->
runST (enqdeq a b) === (Just a, Just b)
it "doesn't insert blocks twice" $
let enqtwice = do
q <- empty 5
enqueue q 0
enqueue q 0
Just 0 <- dequeue q
null q
in
runST enqtwice `shouldBe` True
it "makes an empty queue non-empty"
$ runST (empty 2 >>= \q -> enqueue q 0 >> null q)
`shouldBe` False
it "is inverse to enqueue"
$ let enqdeq a b = do
q <- empty 10
enqueue q a
enqueue q b
(,) <$> dequeue q <*> dequeue q
in property $ forAll (elements [0 .. 9]) $ \a ->
forAll (elements (List.delete a [0 .. 9]))
$ \b -> runST (enqdeq a b) === (Just a, Just b)
it "doesn't insert blocks twice"
$ let enqtwice = do
q <- empty 5
enqueue q 0
enqueue q 0
Just 0 <- dequeue q
null q
in runST enqtwice `shouldBe` True
instance Arbitrary a => Arbitrary (Vector a) where
arbitrary = V.fromList <$> arbitrary
......
module MA.Algorithm.SplitSpec (spec) where
import Test.Hspec
import Control.Monad.ST
import Data.STRef
import Data.List ( sort )
import Control.Monad.Reader
import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as VU
import Lens.Micro.Platform
import MA.Algorithm.Types
import MA.Algorithm.Split
import Data.BlockQueue ( BlockQueue )
import Data.Partition.Common
import Data.MorphismEncoding ( fromEdgeRef
, Encoding
)
import qualified Data.MorphismEncoding as Encoding
import MA.RefinementInterface
import MA.Coalgebra.RefinementTypes
import MA.Algorithm.Initialize
import qualified Data.BlockQueue as Queue
import MA.Functors.Powerset
import MA.Functors.MonoidValued
import qualified Data.RefinablePartition as Partition
import qualified Data.Partition as Partition
( toBlocks )
spec :: Spec
spec = do
collectTouchedBlocksSpec
updateBlockSpec
splitBlockSpec
addBlocksToQueueSpec
splitSpec
collectTouchedBlocksSpec :: Spec
collectTouchedBlocksSpec = describe "collectTouchedBlocks" $ do
it "returns an empty list when no predecessors exist" $ do
withState @Powerset (enc [True, False] [(0, (), 1)])
(collectTouchedBlocks (Block 0))
`shouldBe` []
it "returns the correct block when predecessors exist" $ do
withState @Powerset (enc [True, False] [(0, (), 1)])
(map fst <$> collectTouchedBlocks (Block 1))
`shouldBe` [Block 0]
it "doesn't return duplicates" $ do
withState @Powerset (enc [True, True, False] [(0, (), 2), (1, (), 2)])
(map fst <$> collectTouchedBlocks (Block 1))
`shouldBe` [Block 0]
it "computes the correct v0" $ do
withState @Powerset (enc [True, True, False] [(0, (), 2), (1, (), 2)])
(map snd <$> collectTouchedBlocks (Block 1))
-- initially, C contains all blocks, so calling update with empty list of
-- edges to S, the result is: No edges to "outside of C", all edges to C
-- and no edges to S.
`shouldBe` [(False, True, False)]
it "marks the correct states" $ do
let res =
withState @Powerset (enc [True, True, False] [(0, (), 2), (1, (), 2)])
$ do
[(b, _)] <- collectTouchedBlocks (Block 1)
p <- view (_1 . partitionL)
VU.toList <$> lift (Partition.markedStates p b)
res `shouldMatchList` [0, 1]
it "adds the correct edges to toSub" $ do
let res =
withState @Powerset (enc [True, True, False] [(0, (), 2), (1, (), 2)])
$ do
_ <- collectTouchedBlocks (Block 1)
ts <- view (_1 . toSubL) >>= V.freeze
return (ts & each . each %~ fromEdgeRef & V.toList)
res `shouldBe` [[0], [1], []]
updateBlockSpec :: Spec
updateBlockSpec = describe "updateBlock" $ do
it "resets toSub to all empty lists"
$ let
res =
withState @Powerset (enc [True, True, False] [(0, (), 2), (1, (), 2)])
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
view (_1 . toSubL)
>>= V.freeze
<&> (each . each %~ fromEdgeRef)
<&> V.toList
in res `shouldBe` [[], [], []]
-- Visualization of the graph. Can be rendered with ditaa.
-- @
-- e1
-- /-\
-- | |
-- v |
-- +---+ e0
-- | 0 +-------\
-- +-+-+ |
-- | v
-- | e2 +---+
-- | | 2 |
-- | +---+
-- v ^
-- +---+ |
-- | 1 |-------/
-- +---+ e3
-- @
it "updates lastW correctly"
$ let res =
withState @Powerset
(enc [True, True, False]
[(0, (), 2), (0, (), 0), (0, (), 1), (1, (), 2)]
)
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
lw <- view (_1 . lastWL) >>= lift . V.freeze
lift (lw & V.toList & mapM readSTRef)
in res `shouldBe` [(2, 1), (1, 2), (1, 2), (0, 1)]
-- The idea here is that the edges from state 0 to block 1 cancel each other
-- out and thus the state has a total weight of 0 and must be unmarked.
it "unmarks states where H3 is v0"
$ let res =
withState @(MonoidValued Integer)
(enc [1, 1, 0, 0]
[(0, 1, 2), (0, (-1), 3), (1, 1, 3), (0, 1, 1)]
)
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
p <- view (_1 . partitionL)
lift (Partition.markedStates p b) <&> VU.toList
in res `shouldBe` [1]
it "caches H3 values for all non-v0 states"
$ let res =
withState @(MonoidValued Integer)
(enc [1, 1, 0, 0]
[(0, 1, 2), (0, (-1), 3), (1, 1, 3), (0, 1, 1)]
)
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
h3 <- view (_1 . h3CacheL) >>= lift . V.freeze
return (h3 V.! 1)
in res `shouldBe` (MonoidH3 0 0 1)
splitBlockSpec :: Spec
splitBlockSpec = describe "splitBlock" $ do
it "handles the simple case of a one-element block"
$ let res = withState @Powerset (enc [True, False] [(0, (), 1)]) $ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
splitBlock b
in res `shouldBe` [0]
it "splits blocks into marked and unmaked"
$ let
res =
withState @Powerset (enc [True, True, False] [(0, (), 2), (1, (), 0)])
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
splitBlock b
in res `shouldMatchList` [Block 0, Block 2]
it "splits different H3s into different blocks"
$ let
res =
withState @(MonoidValued Int)
(enc [3, 3, 3, 0]
[(0, 1, 3), (1, 2, 3), (2, 3, 3), (0, 2, 0), (1, 1, 1)]
)
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
splitBlock b
in res `shouldMatchList` [Block 0, Block 2, Block 3]
it "combines equal H3s into the same block"
$ let
res =
withState @(MonoidValued Int)
(enc [3, 3, 3, 0]
[(0, 1, 3), (1, 1, 3), (2, 3, 3), (0, 2, 0), (1, 2, 1)]
)
$ do
[(b, v0)] <- collectTouchedBlocks (Block 1)
updateBlock b v0
splitBlock b
in res `shouldMatchList` [Block 0, Block 2]
addBlocksToQueueSpec :: Spec
addBlocksToQueueSpec = describe "addBlocksToQueue" $ do
it "doesn't add the largest block to the queue"
$ let res =
withState @(MonoidValued Int)
(enc [1, 1, 2, 3] [(0, 1, 0), (1, 1, 1), (2, 2, 2), (3, 3, 3)])
$ do
lift . Queue.clear =<< view _2
addBlocksToQueue (Block 0) (map Block [0, 1, 2])
q <- lift . Queue.toList =<< view _2
p <- view (_1 . partitionL)
lift $ forM q $ \b -> Partition.blockSize p b
in res `shouldMatchList` ([1, 1])
it "does add all new blocks, if the original was already queued"
$ let res =
withState @(MonoidValued Int)
(enc [1, 1, 2, 3] [(0, 1, 0), (1, 1, 1), (2, 2, 2), (3, 3, 3)])
$ do
queue <- view _2
lift (Queue.clear queue)
lift (Queue.enqueue queue (Block 0))
addBlocksToQueue (Block 0) (map Block [0, 1, 2])
lift (Queue.toList queue)
in res `shouldMatchList` (map Block [0, 1, 2])
splitSpec :: Spec
splitSpec = describe "split" $ do
let encoding =
(enc
[10, 10, 10, 1, 1, 20, 20, 0]
[ (0, 1 , 7)
, (0, 9 , 0)
, (1, 2 , 7)
, (1, 8 , 1)
, (2, 3 , 7)
, (2, 7 , 2)
, (3, 1 , 7)
, (4, 1 , 4)
, (5, 20, 6)
, (6, 20, 5)
]
)
it "splits all touched blocks correctly"
$ let res = withState @(MonoidValued Int) encoding $ do
p <- view (_1 . partitionL)
b <- lift (Partition.blockOfState p 7)
split b
Partition.toBlocks <$> lift (Partition.freeze p)
in (map sort res)
`shouldMatchList` [[0], [1], [2], [3], [4], [5, 6], [7]]
it "adds the correct blocks to the queue"
$ let
res = withState @(MonoidValued Int) encoding $ do
p <- view (_1 . partitionL)
b <- lift (Partition.blockOfState p 7)
b3 <- lift (Partition.blockOfState p 3)
(lift . Queue.delete b) =<< view _2
(lift . Queue.delete b3) =<< view _2
split b
queuedBlocks <- lift . Queue.toList =<< view _2
lift (mapM (fmap VU.toList . Partition.statesOfBlock p) queuedBlocks)
in
res
`shouldSatisfy` (\l ->
([0] `elem` l)
&& ([1] `elem` l)
&& ([2] `elem` l)
&& ([5, 6] `elem` l)
&& ( ([3] `elem` l && not ([4] `elem` l))
|| ([4] `elem` l && not ([3] `elem` l))
)
)
withState
:: RefinementInterface h
=> Encoding (Label h) (H1 h)
-> (forall s . SplitM s h a)
-> a
withState e action = runST $ do
(q, as) <- initialize e