diff --git a/Reverse_Brzozowski/Reverse-Brzozowski.cabal b/Reverse_Brzozowski/Reverse-Brzozowski.cabal index 7227abc9c40d7da9aed7c410f61b1ee9f86f5f30..620f5cf1f6f3f4ceffa43aeb5221cea4c82faf85 100644 --- a/Reverse_Brzozowski/Reverse-Brzozowski.cabal +++ b/Reverse_Brzozowski/Reverse-Brzozowski.cabal @@ -30,6 +30,7 @@ test-suite test build-depends: hedgehog , hedgehog-quickcheck + , lifted-async , base , Derv, containers diff --git a/Reverse_Brzozowski/lib/Derv.hs b/Reverse_Brzozowski/lib/Derv.hs index 7569468d988d24880803f4b2dc68c76862bf6e49..d894a27de6dd91f8991aba60ebe4244e43b60841 100644 --- a/Reverse_Brzozowski/lib/Derv.hs +++ b/Reverse_Brzozowski/lib/Derv.hs @@ -6,7 +6,7 @@ import Data.Set (Set, toList, singleton, empty, map, member, union, cartesianPr import Debug.Trace data RegEx = Empty - | Zero + | Zero String | Push | Pop | Seq RegEx RegEx @@ -14,9 +14,24 @@ data RegEx = Empty | Star RegEx deriving (Show,Eq, Ord) +approx :: Int -> RegEx -> Set String +approx n expr = lang_n n (singleton "") $ norm expr where + lang_n :: Int -> (Set String) -> RegEx -> Set String + lang_n _ acc Empty = acc + lang_n _ acc (Zero _) = empty + lang_n n acc Push = Data.Set.map (\w -> if length w > n then "overflow" else w) $ Data.Set.map (\w -> merge_word (w,"+")) acc + lang_n n acc Pop = Data.Set.map (\w -> if length w > n then "underflow" else w) $ Data.Set.map (\w -> merge_word (w,"-")) acc + lang_n n acc (Seq l r) = lang_n n (lang_n n acc l) r + lang_n n acc (Alt l r) = (lang_n n acc r) `union` (lang_n n acc l) + lang_n n acc (Star e) = fp (\acc' -> lang_n n acc' (Alt e Empty)) acc + +fp :: (Eq a) => (a->a) -> a -> a +fp f a | (f a) == a = a + | otherwise = fp f (f a) + lang :: RegEx -> Set String lang Empty = singleton "" -lang Zero = empty +lang (Zero _) = empty lang Push = singleton "+" lang Pop = singleton "-" -- this doesnt work, Seq Pop Pop -> emptylang (Seq l Pop) = lang (deriv Push l) -- ^-1 operation needed, to do this generaly, since Seq (_) (_ <+> Pop) doesn't work @@ -35,7 +50,7 @@ lang_deriv Pop = Data.Set.map (\word -> if (word == "") then "+" else (if (last --assuming ausmultiplizierte normalform lang2 :: RegEx -> Set String lang2 Empty = singleton "" -lang2 Zero = empty +lang2 (Zero _) = empty lang2 Push = singleton "+" lang2 Pop = singleton "-" lang2 (Seq l Pop) = Data.Set.map (\word -> ( @@ -48,6 +63,10 @@ lang2 (Alt l r) = (lang2 l) `union` (lang2 r) merge_word :: (String, String) -> String -- assume normal form +merge_word ("underflow", _ ) = "underflow" -- underflow +merge_word ("overflow", _ ) = "overflow" -- underflow +merge_word (_, "underflow" ) = "underflow" -- underflow +merge_word (_, "overflow" ) = "overflow" -- underflow merge_word ([], r) = r merge_word (l, ('-':rest)) | last l == '+' = merge_word (init l, rest) | otherwise = l ++ ('-':rest) @@ -55,7 +74,7 @@ merge_word (l,r) = l <> r final :: RegEx -> Bool final Empty = True -final Zero = False +final (Zero _) = False final Push = False final Pop = False final (Seq l Push) = False --f rs then final l else rs where rs = final r -- Wrong definition CONTINUE: find real definition @@ -68,10 +87,10 @@ final (Alt l r) = final l || final r final (Star _) = True derPush :: RegEx -> RegEx -derPush Empty = Zero -derPush Zero = Zero +derPush Empty = Zero "Empty/Push" +derPush (Zero m) = Zero m derPush Push = Empty -derPush Pop = Zero +derPush Pop = Zero "Pop/Zero" derPush (Alt l r) = (derPush l) <+> (derPush r) derPush (Seq l r) | final r = (l <.> (derPush r)) <+> (derPush l) | otherwise = l <.> (derPush r) -- @@ -79,7 +98,7 @@ derPush (Star x) = (Star x) <.> (derPush x) -- hmm?? derPop :: RegEx -> RegEx derPop Empty = Push -derPop Zero = Zero +derPop (Zero x) = Zero x derPop Push = Seq Push Push derPop Pop = Empty <+> (Pop <.> Push) -- oof derPop (Alt l r) = (derPop l) <+> (derPop r) @@ -94,14 +113,14 @@ deriv :: RegEx -> (RegEx -> RegEx) deriv Push = derPush deriv Pop = derPop deriv Empty = id -deriv Zero = const Zero +deriv (Zero x) = const (Zero x) deriv (Seq l r) = (deriv l).(deriv r) deriv (Alt l r) = error "not thought about it enough" -- const Zero -- doesn't ALLWAYS exist -- \ word -> (deriv l word)<+>(deriv r word) -- WONG, doesn't exist deriv _ = error "blub" ends_in :: RegEx -> [RegEx] ends_in Empty = [Pop] -- Push.Pop == 1 -ends_in Zero = [] +ends_in (Zero _) = [] ends_in Push = [Push] ends_in Pop = [Pop] ends_in (Alt l r ) = nub $ sort $ ends_in l ++ ends_in r @@ -130,16 +149,17 @@ closure :: [(RegEx, RegEx)] -> [(RegEx, RegEx)] -> Maybe [(RegEx, RegEx)] closure rel [] = Just rel closure rel ((x,y):todo) | x == y = closure rel todo -- symmetry - | (final x) /= (final y) = trace ("finality diff: " <> (show (pp x,pp y)) <> "\nRel: " <> (show rel)) Nothing + | (final x) /= (final y) = --trace ("finality diff: " <> (show (pp x,pp y)) <> "\nRel: " <> (show rel)) + Nothing | (x,y) `elem` (rel ++ todo) = closure rel todo - | length rel > 1000 = trace "non det?" $ Nothing + | length rel > 1000 = trace "non det?" $ Nothing | otherwise = closure ((x,y):rel) ([(norm (deriv a x), norm (deriv a y)) | a <- to_check x y ] ++ todo) naive :: RegEx -> RegEx -> Maybe [(RegEx, RegEx)] naive l r = closure [] [(l,r)] where naive_bisim :: RegEx -> RegEx -> Bool -naive_bisim l r = isJust $ is_bisim <$> naive l r +naive_bisim l r = isJust $ is_bisim <$> naive (norm l) (norm r) -- assuming norm, else nondet (<#) :: RegEx -> RegEx -> Bool @@ -153,7 +173,7 @@ expr `accepts` word = final (deriv word expr) norm :: RegEx -> RegEx norm Empty = Empty -norm Zero = Zero +norm (Zero m) = Zero m norm Push = Push norm Pop = Pop norm (Alt l r) -- | (norm l) <# (norm r) = norm r -- nondet @@ -167,9 +187,14 @@ norm x@(Seq l r) = let normed = norm l <.> norm r in -- > only 1 evaluation step norm (Star (Star x)) = norm $ Star x norm (Star x) | (norm x) == Empty = Empty - | (norm x) == Zero = Empty - | otherwise = Star $ norm $ x + | is_Zero (norm x) = Empty + | idempotent x = norm (x <+> Empty) -- this solves some issues, but is it premature optim? + | otherwise = case (norm x) of + (Alt Empty nx) -> Star $ nx + alt -> Star alt +idempotent :: RegEx -> Bool +idempotent x = (norm x) `naive_bisim` (norm (x <.> x)) class SemiRing a where one :: a @@ -179,18 +204,21 @@ class SemiRing a where pp :: RegEx -> String pp Empty = "1" -pp Zero = "0" +pp (Zero _) = "0" pp Pop = "-" pp Push = "x" pp (Seq l r) = "(" <> (pp l) <> " " <> (pp r) <> ")" pp (Alt l r) = "(" <> (pp l) <> " | " <> (pp r) <> ")" pp (Star x) = "(" <> (pp x) <> ")*" +is_Zero (Zero _) = True +is_Zero _ = False + instance SemiRing RegEx where one = Empty - zero = Zero - Zero <.> _ = Zero - _ <.> Zero = Zero + zero = Zero "default" + (Zero m) <.> _ = Zero m + _ <.> (Zero m) = Zero m Empty <.> r = r l <.> Empty = l -- (Star l) <.> r = ---- @@ -200,8 +228,8 @@ instance SemiRing RegEx where l <.> (Alt s t) = (l <.> s) <+> (l <.> t) -- slows down performance, makes other steps easier (Alt r s) <.> t = (r <.> t) <+> (s <.> t) -- same. custom hinzugefügt. Alternativly could make every other function smarter l <.> r = Seq l r - Zero <+> r = r - l <+> Zero = l + (Zero _) <+> r = r + l <+> (Zero _) = l Empty <+> (Star x) = (Star x) (Star x) <+> Empty = (Star x) (Alt r s) <+> t = r <+> (s <+> t) @@ -212,3 +240,4 @@ instance SemiRing RegEx where | r <= s = Alt r s | otherwise = Alt s r -- depends on arbitrary, derived (<=), scary +--------------------- lexicographic order diff --git a/Reverse_Brzozowski/test/test.hs b/Reverse_Brzozowski/test/test.hs index 4c8e591a4abf8fb15e605055e9c3984f9ce16aa4..f9758f46440fd80b70ec4afc045e4085f266fa54 100644 --- a/Reverse_Brzozowski/test/test.hs +++ b/Reverse_Brzozowski/test/test.hs @@ -4,6 +4,12 @@ import Derv import Debug.Trace +import System.Timeout (timeout) + +import Control.Concurrent (threadDelay) +import Control.Concurrent.Async.Lifted (race) +import Control.Exception (evaluate) + import Data.Set (member) import Control.Applicative (liftA2) @@ -14,11 +20,11 @@ import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range single_expr :: Gen RegEx -single_expr = Gen.element [Empty, Zero, Push, Pop] +single_expr = Gen.element [Empty, zero, Push, Pop] expr :: Gen RegEx expr = Gen.recursive Gen.choice - (Gen.constant <$> [Empty, Zero, Push, Pop]) -- nonrecursives + (Gen.constant <$> [Empty, zero, Push, Pop]) -- nonrecursives (Gen.subterm2 expr expr <$> [Seq, Alt]) -- recursives -- * means works with star expressions @@ -156,15 +162,29 @@ prop_lang_deriv_r_deriv_lang_r = --todo, generate words (== sequences of symbols) --only to check that accepts terminates -prop_accepts_implies_includes :: Property + +{-prop_accepts_implies_includes :: Property prop_accepts_implies_includes = - property $ do + withTests 10000 $ withRetries 0 $ withShrinks 0 $ property $ do matcher <- forAll star_expr w <- forAll word - liftIO $ print (pp matcher <> " accepts " <> (pp w)) - (if ((norm matcher) `accepts` (norm w)) then True else True) === True + liftIO $ print "A" + result <- liftIO $ timeout 2 $ do + pure $ if ((norm matcher) `accepts` (norm w)) then True else True + liftIO $ print "B" + case result of + Nothing -> fail "Timeout" + Just passed -> passed === True +-} +prop_fast_timeout :: Property +prop_fast_timeout = + property $ do + matcher <- forAll star_expr + w <- forAll word + test $ withTimeLimit 10000 $ + assert $ (if ((norm matcher) `accepts` (norm w)) then True else True) == True tests :: IO Bool tests = @@ -172,6 +192,20 @@ tests = main = tests +withTimeLimit :: Int -> TestT IO a -> TestT IO a +withTimeLimit timeout v = do + result <- + race + (liftIO $ threadDelay timeout) + v + case result of + Left () -> fail "Timeout exceeded" + Right x -> pure x + + -- deriv Push ((Star Push) <.> (Pop)) => Zero -- naive (Pop <+> (Star Push)) ((Star Push) <.> (Pop)) -- this gives the wrong answer +-- final $ deriv Push $ Star (Seq Pop (Alt Push Pop)) :: Nondet +------ but don't know why +