diff --git a/src/MA/Algorithm/Split.hs b/src/MA/Algorithm/Split.hs index 736d0d8776cc1a343b892d0d4001069991f2a81b..e9e220f49719e4749688a00367f66fd1fb01c3c4 100644 --- a/src/MA/Algorithm/Split.hs +++ b/src/MA/Algorithm/Split.hs @@ -3,8 +3,9 @@ module MA.Algorithm.Split ( SplitM , split - -- * Internal functions + -- * Internal functions, exported only for testing , collectTouchedBlocks + , updateBlock ) where import Prelude hiding (pred) @@ -47,6 +48,14 @@ split blockS = do whenM (lift $ Partition.hasMarked (partition as) b) $ splitBlock 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 @@ -61,7 +70,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) -> diff --git a/src/MA/Functors/MonoidValued.hs b/src/MA/Functors/MonoidValued.hs index 15f66a1fd979b83e02107055a7a92339427cf370..64ca17ffff9c81c6dad4921ba66a4dd40dd6885e 100644 --- a/src/MA/Functors/MonoidValued.hs +++ b/src/MA/Functors/MonoidValued.hs @@ -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) diff --git a/tests/MA/Algorithm/SplitSpec.hs b/tests/MA/Algorithm/SplitSpec.hs index 6066ac2fdf0dcecb987f1a89ff3f3e7131e5101d..2b1786d7e572a33c1cdde61a3faa0bade3e2573a 100644 --- a/tests/MA/Algorithm/SplitSpec.hs +++ b/tests/MA/Algorithm/SplitSpec.hs @@ -3,6 +3,7 @@ module MA.Algorithm.SplitSpec (spec) where import Test.Hspec import Control.Monad.ST +import Data.STRef import Control.Monad.Reader import qualified Data.Vector as V @@ -22,11 +23,13 @@ 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 spec :: Spec spec = do collectTouchedBlocksSpec + updateBlockSpec collectTouchedBlocksSpec :: Spec collectTouchedBlocksSpec = describe "collectTouchedBlocks" $ do @@ -72,6 +75,81 @@ collectTouchedBlocksSpec = describe "collectTouchedBlocks" $ do 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) + + withState :: RefinementInterface h => Encoding (Label h) (H1 h)