5
\$\begingroup\$

I am trying to implement a monitor for a certain temporal logic. What this means is the following:

  • There is some external source, from which a trace of items are coming. An item looks like a timestamp along with some propositions which holds at that point.
  • There is a property of traces we care about. This is specified in some temporal logic. This could look like "So far, p has been true" or "Since q happened in the last two time units, r has always held since then", or "p always holds when q does"
  • Our task is to build a monitor which is a streaming algorithm whose interface is the operation step which consumes an item from the trace and checks whether the trace fed so far satisfies the given property or not.

Here is the Haskell code:

import Control.Monad.State
import qualified Data.Map
import qualified Data.Set
import Data.Maybe

-- in what follows, `t` stands for some time domain. For most purposes, we assume it is totally ordered and has subtraction defined on it.

data Interval t =
    OpenOpen t t
  | OpenClosed t t
  | ClosedOpen t t
  | ClosedClosed t t
  deriving (Eq, Ord)

inInterval :: Ord t => t -> Interval t -> Bool
inInterval t (OpenOpen       s f) = s < t && t < f
inInterval t (OpenClosed     s f) = s < t && t <= f
inInterval t (ClosedOpen     s f) = s <= t && t < f
inInterval t (ClosedClosed   s f) = s <= t && t <= f

inleqInterval :: Ord t => t -> Interval t -> Bool
inleqInterval t (OpenOpen       s f) = t < f
inleqInterval t (OpenClosed     s f) = t <= f
inleqInterval t (ClosedOpen     s f) = t < f
inleqInterval t (ClosedClosed   s f) = t <= f

-- Below, we use `prop` to denote a domain for the symbols that represent propositions
-- For most purposes, we'd want to use something like int since we'd use formulae based on this symbols as indices of maps

type TruthAssignment prop = Data.Set.Set prop
type Item t prop = (t, TruthAssignment prop)
type Trace t prop = [Item t prop] -- the programmer should ensure that the timestamps are increasing

data TemporalFormula t prop =
  Proposition prop
  | Since (Interval t) (TemporalFormula t prop) (TemporalFormula t prop)
  | Neg (TemporalFormula t prop)
  | And (TemporalFormula t prop) (TemporalFormula t prop)
  deriving (Eq, Ord)

isTemporal :: TemporalFormula t prop -> Bool
isTemporal (Since _ _ _) = True
isTemporal _ = False

getTemporalSubformulas :: TemporalFormula t prop -> [TemporalFormula t prop]
getTemporalSubformulas phi@(Since _ phi1 phi2) = [phi] ++ getTemporalSubformulas phi1 ++ getTemporalSubformulas phi2
getTemporalSubformulas (Neg phi)                 = getTemporalSubformulas phi
getTemporalSubformulas (And phi1 phi2)           = (getTemporalSubformulas phi1) ++ (getTemporalSubformulas phi2)
getTemporalSubformulas _                         = []

type MonitorState t prop = Data.Map.Map (TemporalFormula t prop) [t]

-- the following type signature says that the monitor is a stateful object which when given a stream of items produces a stream of booleans
monitor :: (Ord t, Ord prop, Num t) => TemporalFormula t prop -> Trace t prop -> State (MonitorState t prop) [Bool]
monitor phi stream = do
  iinit phi
  loop stream
  where
    loop (i:is) = do
      b <- step i phi
      bs <- loop is
      return (b:bs)
    loop []     = return []

iinit :: (Ord t, Ord prop) => TemporalFormula t prop -> State (MonitorState t prop) ()
iinit phi = do
  let subformulas = getTemporalSubformulas phi
  put $ foldr (\psi map -> Data.Map.insert psi [] map) Data.Map.empty subformulas

step :: (Num t, Ord t, Ord prop) => Item t prop -> TemporalFormula t prop -> State (MonitorState t prop) Bool
step (_, truths) (Proposition p) = return $ Data.Set.member p truths
step item (Neg formula) = not <$> step item formula
step item (And formula1 formula2) = do
  b1 <- step item formula1
  b2 <- step item formula2
  return $ b1 && b2
step item@(tao, _) phi@(Since inter phi1 phi2) = do
  update item phi
  bufffs <- get
  let lphi = case (Data.Map.lookup phi bufffs) of Just l -> l
  case lphi of
    []    -> return False
    (t:_) -> return $ inInterval (tao - t) inter

update :: (Num t, Ord t, Ord prop) => Item t prop -> TemporalFormula t prop -> State (MonitorState t prop) ()
update (time, truths) phi@(Since inter phi1 phi2) = do
  bufffs <- get
  let lphi = case (Data.Map.lookup phi bufffs) of Just l -> l
  b1 <- step (time, truths) phi1
  b2 <- step (time, truths) phi2
  let l = if b1 then (ddrop lphi inter time) else []
  let lphi' = if b2 then l ++ [time] else l
  put (Data.Map.insert phi lphi' bufffs)


ddrop :: (Ord t, Num t) => [t] -> Interval t -> t -> [t]
ddrop [] _ _             = []
ddrop (kappa:ls) inter tao
  | inleqInterval (tao - kappa) inter   = ddrop' kappa ls inter tao
  | otherwise                       = ddrop ls inter tao

ddrop' :: (Ord t, Num t) => t -> [t] -> Interval t -> t -> [t]
ddrop' kappa [] _ _          = [kappa]
ddrop' kappa (kappa':ls) inter tao
  | inInterval (tao - kappa') inter    = ddrop' kappa' ls inter tao
  | otherwise                          = (kappa:kappa':ls)

For comparison, here is a Java implementation of the same idea.

I would like some feedback on my Haskell code:

  • I would like to be able to extend this code with a main and test it on a large stream to see how well it performs. Is the State Monad appropriate for the purpose of performance? Is my way of modelling streams as lists appropriate for this purpose?
  • As implemented, the "monitor state" and the Formula looks like independent objects. Is there a better way to tie them together than to define a seperate MonitorState and initalize it everytime? I think the idea of modelling MonitorState as a Map is ugly and not very haskell-y. What are some better ways of structuring my code so that I can avoid the Map and/or show that there is some relation between the state of the monitor and a formula?
  • Other general comments on improving the code quality.
\$\endgroup\$
0

1 Answer 1

2
\$\begingroup\$

I can't comment on performance implications of state monad usage, but it seems like list concatenation may be a bottleneck (e.g. in getTemporalSubformulas or l ++ [time] in update).

Minor style notes

It is common practice to import Data.Map and Data.Set with alias and to import main type unqualified. This makes type signatures a bit more concise.

import qualified Data.Map as Map
import Data.Map (Map)

foo :: Int -> Map Int String
foo x = Map.singleton x "hello"

In isTemporal you can use {} to match on data constructor without matching its fields. This is potentially future-proof in case of changing number of fields in data constructor.

isTemporal Since{} = True
isTemporal _       = False

It may be a bit easier to encode intervals as a pair of bounds:

data EndPoint t = Open t | Closed t
type Interval t = (EndPoint t, EndPoint t)

afterStart, beforeEnd :: Ord t => t -> Interval t -> Bool
afterStart t (Open start)   = t >  start
afterStart t (Closed start) = t >= start
beforeEnd  t (Open end)     = t <  end
beforeEnd  t (Closed end)   = t <= end

inInterval, inleqInterval :: Ord t => t -> Interval t -> Bool
inInterval t int = afterStart t int && beforeEnd t int
inleqInterval = beforeEnd

It is also may be beneficial to reuse intervals from data-interval package.


In iinint

foldr (\psi map -> Data.Map.insert psi [] map) Data.Map.empty subformulas

can be rewritten as

Map.fromList $ map (,[]) subformulas

Try to compile with -Wall flag, seems like you have a lot of non-exhaustive pattern matches, which is bad.

For example:

  let lphi = case (Data.Map.lookup phi bufffs) of Just l -> l

If you are absolutely sure that lookup won't fail here, you can rewrite it with Data.Map.!:

  let lphi = bufffs `Map.!` phi

ddrop can be rewritten to make it more explicit what parts of the list you are removing:

ddrop ls inter tao = case dropWhile f ls of
  [] -> []
  kappa:ls' -> kappa : dropWhile g ls'
  where
     f kappa = not $ inleqInterval (tao - kappa) inter
     g kappa = inInterval (tao - kappa) inter

or a bit shorter with the ViewPatterns extension

ddrop ls inter tao = case dropWhile f ls of
  | dropWhile f ls -> kappa:ls' = kappa : dropWhile g ls'
  | otherwise = []
  where
     f kappa = not $ inleqInterval (tao - kappa) inter
     g kappa = inInterval (tao - kappa) inter
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.