Commit ba44d2dc authored by Hans-Peter Deifel's avatar Hans-Peter Deifel 🐢
Browse files

Fix whitespace

parent 39ad81b7
......@@ -70,7 +70,7 @@ stateInBlockToBDD varsPartition stateBitSize state block =
encBlock = encodeInteger stateBitSize (fromBlock block)
polarities = encState ++ encBlock
in cube varsPartition polarities
blocksToBDD :: PrimMonad m => P.Partition -> BDD -> Int -> V.Vector State -> Int -> m BDD
blocksToBDD partition varsPartition stateBitSize statesVec 0 = return sylvanFalse
blocksToBDD partition varsPartition stateBitSize statesVec statesVecSize = do
......@@ -87,7 +87,7 @@ partitionToBDD partition varsPartition stateBitSize statesVec = blocksToBDD part
-- res1 <- band transitionBDD partitionBDD
-- exists res1 varsTo
-- We have to somehow assign numbers to all edge labels, which could be anything.
-- We have to somehow assign numbers to all edge labels, which could be anything.
-- Therefore we take a list (in the form of a vector) of all edge labels and filter out duplicates,
-- so we can assign a unique number (their position in the vector) to each.
createLabelsVec :: Eq a => Encoding a f1 -> V.Vector a
......@@ -103,7 +103,7 @@ calculateLabelBitSizes :: V.Vector a -> Int
calculateLabelBitSizes labelsVec = ceiling (logBase 2 (fromIntegral (max 1 (V.length labelsVec))))
createVarsEdges :: PrimMonad m => (Int, Int) -> m BDD
createVarsEdges (stateBitSize, labelBitSize) = setFromArray (Data.List.take (2 * stateBitSize) [(10::BDDVar),(11::BDDVar)..]
createVarsEdges (stateBitSize, labelBitSize) = setFromArray (Data.List.take (2 * stateBitSize) [(10::BDDVar),(11::BDDVar)..]
++ Data.List.take labelBitSize [((fromIntegral (10 + 3 * stateBitSize))::BDDVar),
((fromIntegral ((10 + 3 * stateBitSize)+1))::BDDVar)..])
createVarsPartition :: PrimMonad m => Int -> m BDD
......@@ -151,7 +151,7 @@ createVarsTo stateBitSize = setFromArray ((Data.List.take (stateBitSize) [(fromI
-- tail <- decodeBlock low
-- return (Negative : tail)
---- Goes through the state encodings to get to the block encoding. We can do this the easy way,
---- Goes through the state encodings to get to the block encoding. We can do this the easy way,
---- since states and blocks are cubes, therefore we can just walk along the nodes that are not
---- sylvanFalse and we will end up at a sylvanTrue or in this case at the root of the block encoding.
--decodeBlockHelper :: PrimMonad m => BDD -> Int -> m [Polarity]
......@@ -161,7 +161,7 @@ createVarsTo stateBitSize = setFromArray ((Data.List.take (stateBitSize) [(fromI
-- then do
-- low <- getlow partition
-- high <- gethigh partition
-- if low == sylvanFalse
-- if low == sylvanFalse
-- then decodeBlockHelper high stateBitSize
-- else decodeBlockHelper low stateBitSize
-- else decodeBlock partition
......@@ -240,7 +240,7 @@ class (Ord (F1 f), Ord (Label f)) => SymbolicInterface f where
symbolicSig :: PrimMonad m => Proxy f -> BDD -> BDD -> BDD -> m BDD
--instance SymbolicInterface SomeFunctor where
-- encodeEdges proxy
-- encodeEdges proxy
instance SymbolicInterface Powerset where
encodeEdges proxy coalgebra = do
......@@ -285,7 +285,7 @@ instance SymbolicInterface RationalValued where
symbolicSig proxy varsTo transitionBDD partitionBDD = mtbddAndExists transitionBDD partitionBDD varsTo
-- Sadly I do not really know how to make Complex valued leaves in Sylvan. Maybe mtbdd_makeleaf with a custom type could be used,
-- Sadly I do not really know how to make Complex valued leaves in Sylvan. Maybe mtbdd_makeleaf with a custom type could be used,
-- but I don't know how good custom Types are supported in this version of Sylvan.
instance SymbolicInterface Bag where
......@@ -354,7 +354,7 @@ instance SymbolicInterface f => SymbolicInterface (Desorted f) where
encodeEdges proxy coalgebra = encodeEdges @f (Proxy :: Proxy f) (desortCoalgebra (Proxy :: Proxy f) coalgebra)
symbolicSig proxy = symbolicSig @f (Proxy :: Proxy f)
refinenementStep :: PrimMonad m => BDD -> BDD -> Int -> Int -> M.Map (BDD, BDD) BDD -> M.Map BDD BDD
refinenementStep :: PrimMonad m => BDD -> BDD -> Int -> Int -> M.Map (BDD, BDD) BDD -> M.Map BDD BDD
-> m (BDD, Int, M.Map (BDD, BDD) BDD, M.Map BDD BDD)
refinenementStep signature partition stateBitSize currentNewBlockNum cache blocks =
let result = M.lookup (partition, signature) cache
......@@ -381,15 +381,15 @@ refinenementStep signature partition stateBitSize currentNewBlockNum cache block
let block = M.lookup partition blocks
in case block of
Just blockSign ->
if blockSign == signature
then return (partition, currentNewBlockNum, cache, blocks)
if blockSign == signature
then return (partition, currentNewBlockNum, cache, blocks)
else insertNewBlock signature partition stateBitSize currentNewBlockNum cache blocks
_ ->
let cache' = M.insert (partition, signature) partition cache
blocks' = M.insert partition signature blocks
in return (partition, currentNewBlockNum, cache', blocks')
insertNewBlock :: PrimMonad m => BDD -> BDD -> Int -> Int -> M.Map (BDD, BDD) BDD -> M.Map BDD BDD
insertNewBlock :: PrimMonad m => BDD -> BDD -> Int -> Int -> M.Map (BDD, BDD) BDD -> M.Map BDD BDD
-> m (BDD, Int, M.Map (BDD, BDD) BDD, M.Map BDD BDD)
insertNewBlock signature partition stateBitSize currentNewBlockNum cache blocks = do
let polarities = encodeInteger stateBitSize currentNewBlockNum
......@@ -398,7 +398,7 @@ insertNewBlock signature partition stateBitSize currentNewBlockNum cache blocks
let cache' = M.insert (partition, signature) newBlock cache
blocks' = M.insert newBlock signature blocks
return (newBlock, currentNewBlockNum+1, cache', blocks')
-- Returns the initial partition, grouping states by their F1 value
initializeSymbolic :: forall f . SymbolicInterface f => Proxy f -> Encoding (Label f) (F1 f) -> P.Partition
initializeSymbolic proxy coalgebra = runST $ do
......@@ -508,10 +508,12 @@ refineRecurse proxy varsTo stateBitSize currentNewBlockNum transitionBDD partiti
signatureBDD <- symbolicSig proxy varsTo transitionBDD partitionBDD
-- sig <- bddToArray signatureBDD --debug: output signature
(partitionBDD', currentNewBlockNum', cache, blocks) <- refinenementStep signatureBDD partitionBDD stateBitSize currentNewBlockNum M.empty M.empty --`debug` (show sig)
if partitionBDD' == partitionBDD
if partitionBDD' == partitionBDD
then decodePartition partitionBDD' stateBitSize
else refineRecurse proxy varsTo stateBitSize currentNewBlockNum' transitionBDD partitionBDD'
bddToArray :: PrimMonad m => BDD -> m [Int]
bddToArray bdd =
if bdd == sylvanFalse
......@@ -526,4 +528,4 @@ bddToArray bdd =
high <- bddToArray v2
return ([(fromIntegral c)] ++ low ++ high)
--debug = flip trace
\ No newline at end of file
--debug = flip trace
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment