diff --git a/src/Lib/LTL.hs b/src/Lib/LTL.hs index 64d8883..b2c3d09 100644 --- a/src/Lib/LTL.hs +++ b/src/Lib/LTL.hs @@ -19,7 +19,7 @@ once :: Stream Bool -> Stream Bool once = hFoldl "once" (P.||) False since :: Stream Bool -> Stream Bool -> Stream Bool -since p q = "since" <: p <: q =: Now q || ( Now p && since p q :@(-1, False)) +since p q = "since" <: p <: q =: Now q || ( Now p && p `since` q :@(-1, False)) yesterday :: Stream Bool -> Stream Bool yesterday p = "yesterday" <: p =: p:@(-1, False) diff --git a/src/Lib/MTL.hs b/src/Lib/MTL.hs index d4ba311..ecf6f9e 100644 --- a/src/Lib/MTL.hs +++ b/src/Lib/MTL.hs @@ -17,7 +17,7 @@ untilMTL (a, b) phi psi = let until' a b phi psi | a == b = psi:@(b,False) - | otherwise = psi:@(a,True) && (phi:@(a, False) || until' (a+1) b phi psi) + | otherwise = psi:@(a,False) || (phi:@(a, True) && until' (a+1) b phi psi) notMTL :: Stream Bool -> Stream Bool notMTL dec = "not" <: dec =: not (Now dec) @@ -30,3 +30,11 @@ eventuallyMTL :: (Int, Int) -> Stream Bool -> Stream Bool eventuallyMTL (a,b) phi = let name = "eventually_(" ++ show a ++ "," ++ show b ++ ")" <: phi in name =: foldl (||) (Leaf False) [phi :@ (i, False) | i <- [a..b]] + +historicallyMTL :: Int -> Stream Bool -> Stream Bool +historicallyMTL k dec = "historicallyMTL" <: k <: dec =: + Now (consecutiveTrueMTL dec) >= Leaf k + +consecutiveTrueMTL :: Stream Bool -> Stream Int +consecutiveTrueMTL dec = "consecutiveTrueMTL" <: dec =: + if not $ Now dec then 0 else consecutiveTrueMTL dec @: (-1, 0) + 1