MITL -> MTL

.gitignore

@@ -0,0 +1,2 @@
+.stack-work/**
+HLola.cabal

package.yaml

@@ -6,9 +6,6 @@ git:              "https://gitlab.software.imdea.org/streamrv/hlola"
 # maintainer:          "[email protected]"
 # copyright:           "2019 Author name here"
 
-extra-source-files:
-- README.md
-
 # Metadata used when publishing your package
 # synopsis:            Short description of your package
 # category:            Web

src/Example/MITLEx.hs → src/Example/MTLEx.hs

@@ -1,14 +1,14 @@
 {-# LANGUAGE RebindableSyntax  #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
-module Example.MITLEx where
+module Example.MTLEx where
 
 import Data.Aeson
 import GHC.Generics
 import Lola
 import Syntax.HLPrelude
 import DecDyn
-import Lib.MITL
+import Lib.MTL
 import Syntax.Booleans
 
 data Event
@@ -28,7 +28,7 @@ property = let
     now x = Now event === Leaf x
     allClear = "allClear" =: now AllClear
     shutdown = "shutdown" =: now Shutdown
-    body = now Alarm `implies` (Now (eventuallyMITL (0,10) allClear) || Now (eventuallyMITL (10,10) shutdown))
+    body = now Alarm `implies` (Now (eventuallyMTL (0,10) allClear) || Now (eventuallyMTL (10,10) shutdown))
   in
     "property" =: body
 
@@ -39,4 +39,4 @@ untilEx = [out p, out q, out theuntil]
   p = Input "p"
   q = Input "q"
   -- Outputs variables
-  theuntil = untilMITL (-1,1) p q
+  theuntil = untilMTL (-1,1) p q

src/Lib/MITL.hs → src/Lib/MTL.hs

@@ -1,5 +1,5 @@
 {-# LANGUAGE RebindableSyntax  #-}
-module Lib.MITL where
+module Lib.MTL where
 
 import Lola
 import Syntax.HLPrelude
@@ -10,23 +10,23 @@ import Lib.Utils
 -- Reference: https://www.cs.ox.ac.uk/people/james.worrell/mtlsurvey08.pdf
 
 -- phi U_{a,b} psi
-untilMITL :: (Int, Int) -> Stream Bool -> Stream Bool -> Stream Bool
-untilMITL (a, b) phi psi = let
+untilMTL :: (Int, Int) -> Stream Bool -> Stream Bool -> Stream Bool
+untilMTL (a, b) phi psi = let
     name = "until_(" ++ show a ++ "," ++ show b ++ ")" <: phi <: psi
   in name =: until' a b phi psi
 
 until' a b phi psi
   | a == b = psi:@(b,False)
   | otherwise = psi:@(a,True) && (phi:@(a, False) || until' (a+1) b phi psi)
 
-notMITL :: Stream Bool -> Stream Bool
-notMITL dec = "not" <: dec =: not (Now dec)
+notMTL :: Stream Bool -> Stream Bool
+notMTL dec = "not" <: dec =: not (Now dec)
 
-andMITL :: Stream Bool -> Stream Bool -> Stream Bool
-andMITL d0 d1 = "and" <: d0 <: d1 =: Now d0 && Now d1
+andMTL :: Stream Bool -> Stream Bool -> Stream Bool
+andMTL d0 d1 = "and" <: d0 <: d1 =: Now d0 && Now d1
 
 -- Phi holds at some point between a and b
-eventuallyMITL :: (Int, Int) -> Stream Bool -> Stream Bool
-eventuallyMITL (a,b) phi = let
+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]]