Fixed MTL until

imdea-software · Dec 30, 2019 · 9eecfbf · 9eecfbf
1 parent aad78a5
commit 9eecfbf
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git 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
@@ -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