syfco-1.1.0.0: src/Data/LTL.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.LTL
-- License : MIT (see the LICENSE file)
-- Maintainer : Felix Klein (klein@react.uni-saarland.de)
--
-- Internal representation of Linear Temporal Logic formulas.
--
-----------------------------------------------------------------------------
module Data.LTL
( Atomic(..)
, Formula(..)
, subFormulas
, applySub
, applyAtomic
, fmlSignals
, fmlInputs
, fmlOutputs
, isBooleanFormula
, isBooleanNextFormula
, simplePrint
, fNot
, fAnd
, fOr
, fGlobally
, fFinally
) where
-----------------------------------------------------------------------------
import qualified Data.Set as S
( toList
, insert
, empty
)
-----------------------------------------------------------------------------
-- | Internal representation of an atomic proposition. Each atomic
-- proposition is either an input or output signal.
data Atomic =
Input String
| Output String
deriving (Eq)
-----------------------------------------------------------------------------
instance Ord Atomic where
compare x y = case (x,y) of
(Input _, Output _) -> LT
(Output _, Input _) -> GT
(Input a, Input b) -> compare a b
(Output a, Output b) -> compare a b
-----------------------------------------------------------------------------
instance Show Atomic where
show a = case a of
Input x -> x
Output x -> x
-----------------------------------------------------------------------------
-- | Internal representation of a Linear Temporal Logic formula.
data Formula =
TTrue
| FFalse
| Atomic Atomic
| Not Formula
| Implies Formula Formula
| Equiv Formula Formula
| And [Formula]
| Or [Formula]
| Next Formula
| Globally Formula
| Finally Formula
| Until Formula Formula
| Release Formula Formula
| Weak Formula Formula
deriving (Eq, Show)
-----------------------------------------------------------------------------
instance Ord Formula where
compare x y = case (x,y) of
(Atomic a, Atomic b) -> compare a b
(Not a, Not b) -> compare a b
(Next a, Next b) -> compare a b
(Globally a, Globally b) -> compare a b
(Finally a, Finally b) -> compare a b
(Implies a b, Implies c d) -> case compare a c of
EQ -> compare b d
v -> v
(Equiv a b, Equiv c d) -> case compare a c of
EQ -> compare b d
v -> v
(Until a b, Until c d) -> case compare a c of
EQ -> compare b d
v -> v
(Release a b, Release c d) -> case compare a c of
EQ -> compare b d
v -> v
(And xs, And ys) -> case foldl lexord EQ $ zip xs ys of
EQ -> compare (length xs) (length ys)
v -> v
(Or xs, Or ys) -> case foldl lexord EQ $ zip xs ys of
EQ -> compare (length xs) (length ys)
v -> v
_ -> compare (num x) (num y)
where
num :: Formula -> Int
num f = case f of
FFalse -> 0
TTrue -> 1
Atomic {} -> 2
Not {} -> 3
Implies {} -> 4
Equiv {} -> 5
And {} -> 6
Or {} -> 7
Next {} -> 8
Globally {} -> 9
Finally {} -> 10
Until {} -> 11
Release {} -> 12
Weak {} -> 13
lexord a (b,c) = case a of
EQ -> compare b c
v -> v
-----------------------------------------------------------------------------
-- | @applySub f fml@ applies the function @f@ to the direct sub-formulas of
-- @fml@, i.e., every sub-formula under the first operator that appears.
-- If @fml@ is a basic term, the formula remains unchanged.
applySub
:: (Formula -> Formula) -> Formula -> Formula
applySub f fml = case fml of
Not x -> Not $ f x
Next x -> Next $ f x
Globally x -> Globally $ f x
Finally x -> Finally $ f x
And xs -> And $ map f xs
Or xs -> Or $ map f xs
Equiv x y -> Equiv (f x) (f y)
Implies x y -> Implies (f x) (f y)
Until x y -> Until (f x) (f y)
Release x y -> Release (f x) (f y)
Weak x y -> Weak (f x) (f y)
_ -> fml
-----------------------------------------------------------------------------
-- | @applyAtomic f fml@ applies the function @f@ to every atomic
-- proposition of @fml@.
applyAtomic
:: (Atomic -> Formula) -> Formula -> Formula
applyAtomic f fml = case fml of
Atomic x -> f x
_ -> applySub (applyAtomic f) fml
-----------------------------------------------------------------------------
-- | Returns the list of Atomic propositions that appear inside the given
-- formula.
fmlSignals
:: Formula -> [Atomic]
fmlSignals = S.toList . signals' S.empty
where
signals' a fml = case fml of
Atomic x -> S.insert x a
_ -> foldl signals' a $ subFormulas fml
-----------------------------------------------------------------------------
-- | Returns the list of input signals that appear inside the given formula.
fmlInputs
:: Formula -> [String]
fmlInputs fml = map (\(Input x) -> x) $ filter isInput $ fmlSignals fml
where
isInput (Input _) = True
isInput (Output _) = False
-----------------------------------------------------------------------------
-- | Returns the list of output signals that appear inside the given formula.
fmlOutputs
:: Formula -> [String]
fmlOutputs fml = map (\(Output x) -> x) $ filter isOutput $ fmlSignals fml
where
isOutput (Output _) = True
isOutput (Input _) =False
-----------------------------------------------------------------------------
-- | Returns all direct sub-formulas of the given formula, i.e., the formulas
-- that appear under the first operator. If the given formula is a basic
-- term, an empty list is returned.
subFormulas
:: Formula -> [Formula]
subFormulas fml = case fml of
TTrue -> []
FFalse -> []
Atomic _ -> []
Not x -> [x]
Next x -> [x]
Globally x -> [x]
Finally x -> [x]
Implies x y -> [x,y]
Equiv x y -> [x,y]
Until x y -> [x,y]
Release x y -> [x,y]
Weak x y -> [x,y]
And xs -> xs
Or xs -> xs
-----------------------------------------------------------------------------
-- | Checks whether a given formula is free of temporal operators.
isBooleanFormula
:: Formula -> Bool
isBooleanFormula fml = case fml of
TTrue -> True
FFalse -> True
Atomic {} -> True
Not x -> isBooleanFormula x
And xs -> all isBooleanFormula xs
Or xs -> all isBooleanFormula xs
_ -> False
-----------------------------------------------------------------------------
-- | Checks whether a given formula contains 'next' as the only temporal
-- operator.
isBooleanNextFormula
:: Formula -> Bool
isBooleanNextFormula fml = case fml of
TTrue -> True
FFalse -> True
Atomic {} -> True
Not x -> isBooleanNextFormula x
And xs -> all isBooleanNextFormula xs
Or xs -> all isBooleanNextFormula xs
Next x -> isBooleanFormula x
_ -> False
-----------------------------------------------------------------------------
-- | Smart 'And' constructur.
fAnd
:: [Formula] -> Formula
fAnd xs =
case filter (/= TTrue) $ warp xs of
[] -> TTrue
[x] -> x
_ -> And xs
where
warp = concatMap wAnd
wAnd fml = case fml of
And x -> x
_ -> [fml]
-----------------------------------------------------------------------------
-- | Smart 'Or' constructur.
fOr
:: [Formula] -> Formula
fOr xs =
case filter (/= FFalse) $ warp xs of
[] -> FFalse
[x] -> x
_ -> Or xs
where
warp = concatMap wOr
wOr fml = case fml of
Or x -> x
_ -> [fml]
-----------------------------------------------------------------------------
-- | Smart 'Not' constructur.
fNot
:: Formula -> Formula
fNot fml = case fml of
TTrue -> FFalse
FFalse -> TTrue
Atomic x -> Not $ Atomic x
Not x -> x
Next x -> Next $ fNot x
Globally x -> Finally $ fNot x
Finally x -> Globally $ fNot x
Implies x y -> And [x, fNot y]
Equiv (Not x) y -> Equiv x y
Equiv x (Not y) -> Equiv x y
Equiv x y -> Equiv (fNot x) y
Until x y -> Release (fNot x) (fNot y)
Release x y -> Until (fNot x) (fNot y)
Weak x y -> Until (fNot y) (And [fNot x, fNot y])
And xs -> Or $ map fNot xs
Or xs -> And $ map fNot xs
-----------------------------------------------------------------------------
-- | Smart 'Globally' constructur.
fGlobally
:: Formula -> Formula
fGlobally fml = case fml of
Globally FFalse -> FFalse
Globally TTrue -> TTrue
Globally _ -> fml
_ -> Globally fml
-----------------------------------------------------------------------------
-- | Smart 'Globally' constructur.
fFinally
:: Formula -> Formula
fFinally fml = case fml of
Finally FFalse -> FFalse
Finally TTrue -> TTrue
Finally _ -> fml
_ -> Finally fml
-----------------------------------------------------------------------------
-- | Simple printing.
simplePrint
:: Formula -> String
simplePrint fml = case fml of
TTrue -> "true"
FFalse -> "false"
Atomic x -> show x
Not x -> '!' : simplePrint x
Next x -> 'X' : ' ' : simplePrint x
Globally x -> 'G' : ' ' : simplePrint x
Finally x -> 'F' : ' ' : simplePrint x
Implies x y -> "(" ++ simplePrint x ++ " -> " ++ simplePrint y ++ ")"
Equiv x y -> "(" ++ simplePrint x ++ " <-> " ++ simplePrint y ++ ")"
Until x y -> "(" ++ simplePrint x ++ " U " ++ simplePrint y ++ ")"
Release x y -> "(" ++ simplePrint x ++ " R " ++ simplePrint y ++ ")"
Weak x y -> "(" ++ simplePrint x ++ " W " ++ simplePrint y ++ ")"
And [] -> simplePrint TTrue
And [x] -> simplePrint x
And (x:xr) -> "(" ++ simplePrint x ++
concatMap ((" && " ++) . simplePrint) xr ++ ")"
Or [] -> simplePrint FFalse
Or (x:xr) -> "(" ++ simplePrint x ++
concatMap ((" || " ++) . simplePrint) xr ++ ")"
-----------------------------------------------------------------------------