CoCASL/LTS/lts.hs

{- |
Module      :  ./CoCASL/LTS/lts.hs
Copyright   :  (c) Daniel Hausmann, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  hausmann@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Functions which allow to compute
- satisfaction of a Hennessy-Milner-Logic formula for a LTS
- simulations and bisimulations between two LTSs.

-}


import qualified Data.List as List

type Node = Char
type Action = Char

data Edge = Edge
    { leftNode :: Node
    , action :: Action
    , rightNode :: Node
    } deriving (Show, Eq, Ord)

data LTS = LTS
    { nodeList :: [Node]
    , edgeList :: [Edge]
    , actionList :: [Action]
    } deriving (Show, Eq, Ord)

data LogOp = AndOp
           | OrOp
           | ImpliesOp
             deriving (Show, Eq, Ord)

data ModOp = BoxOp
           | DiamondOp
             deriving (Show, Eq, Ord)

data HML = Top
         | Bot
         | Neg HML
         | Bin LogOp HML HML
         | Modal ModOp HML Action
           deriving (Show, Eq, Ord)

equal :: [(Node, Node)] -> [(Node, Node)] -> Bool
equal l1 l2 = case l1 of
              [] -> case l2 of
                  [] -> True
                  _ : _ -> False
              (n, m) : l1t -> elem (n, m) l2
                  && equal l1t (List.delete (n, m) l2)

-- functions for hml-formulas

satisfy :: LTS -> HML -> [(Node, ([(Node, HML, Bool)], Bool))]
satisfy lts f = case nodeList lts of
    [] -> []
    n : nt -> (n, ltshml lts f n $ edgeList lts) :
              satisfy lts { nodeList = nt } f

ltshml :: LTS -> HML -> Node -> [Edge] -> ([(Node, HML, Bool)], Bool)
ltshml lts f n ed1 = case f of
    Bot -> ([(n, Bot, False)], False)
    Top -> ([(n, Top, True)], True)
    Neg g -> case ltshml lts g n ed1 of
        (l, b1) -> ((n, Neg g, not b1) : l, not b1)
    Bin op g h -> case ltshml lts g n ed1 of
        (l, b1) -> case ltshml lts h n ed1 of
            (k, b2) -> case op of
                AndOp -> ((n, f, b1 && b2) : l ++ k, b1 && b2)
                OrOp -> ((n, f, b1 || b2) : l ++ k, b1 || b2)
                ImpliesOp -> ((n, f, not b1 || b2) : l ++ k, not b1 || b2)
    Modal op g a -> case ed1 of
        [] -> case op of
            BoxOp -> ([(n, f, True)], True)
            DiamondOp -> ([(n, f, False)], False)
        ed : et ->
            if leftNode ed == n && action ed == a then
                    case ltshml lts g (rightNode ed) (edgeList lts) of
                        (l, b1) -> case ltshml lts f n et of
                            (k, b2) -> case op of
                              BoxOp -> if b1 then
                                (List.nub ((n, f, b2) : l ++ k), b2)
                                else (List.nub ((n, f, False) : l), False)
                              DiamondOp -> if b1 then
                                (List.nub ((n, f, True) : l), True)
                                else (List.nub ((n, f, b2) : l ++ k), b2)
                else ltshml lts f n et

-- functions for bisimulations

bisimulations :: LTS -> LTS -> [((Node, Node), [(Node, Node)])]
bisimulations lts1 lts2 = bisims lts1 lts2 $ simulations lts1 lts2

bisims :: LTS -> LTS -> [((Node, Node), [(Node, Node)])] ->
                                         [((Node, Node), [(Node, Node)])]
bisims lts1 lts2 l = case l of
                         [] -> []
                         ((n, m), ls) : lt -> if bisimulates lts1 lts2 n m
                              then ((n, m), ls) : bisims lts1 lts2 lt
                              else bisims lts1 lts2 lt

bisimulation :: LTS -> LTS -> Node -> Node -> [(Node, Node)]
bisimulation lts1 lts2 n m = if bisimulates lts1 lts2 n m
                             then simulation lts1 lts2 n m
                             else []

bisimulates :: LTS -> LTS -> Node -> Node -> Bool
bisimulates lts1 lts2 n m = simulates lts1 lts2 n m &&
                            equal (simulation lts2 lts1 m n)
                            (map (\ (p, q) -> (q, p)) (simulation lts1 lts2 n m))


-- functions for simulations

simulations :: LTS -> LTS -> [((Node, Node), [(Node, Node)])]
simulations lts1 lts2 = sims lts1 lts2 (nodeList lts1) (nodeList lts2)

sims :: LTS -> LTS -> [Node] -> [Node] -> [((Node, Node), [(Node, Node)])]
sims lts1 lts2 nd1 nd2 = case nd1 of
    [] -> []
    n : nt -> case nd2 of
        [] -> sims lts1 lts2 nt (nodeList lts2)
        m : mt -> if simulates lts1 lts2 n m then
                  ((n, m), simulation lts1 lts2 n m) : sims lts1 lts2 nd1 mt
                  else sims lts1 lts2 nd1 mt

simulation :: LTS -> LTS -> Node -> Node -> [(Node, Node)]
simulation lts1 lts2 n m = fst $ sim lts1 lts2 n m
                                     (edgeList lts1) (edgeList lts2) []

simulates :: LTS -> LTS -> Node -> Node -> Bool
simulates lts1 lts2 n m = snd $ sim lts1 lts2 n m
                                    (edgeList lts1) (edgeList lts2) []


sim :: LTS -> LTS -> Node -> Node -> [Edge] -> [Edge] -> [(Node, Node)] ->
                                                      ([(Node, Node)], Bool)
sim lts1 lts2 n m ed1 ed2 l = if elem (n, m) l then (l, True) else
    case ed1 of
    [] -> (List.nub ((n, m) : l), True)
    ed : e1t ->
        if leftNode ed == n then
            case ed2 of
                [] -> ([], False)
                ee : e2t ->
                    if leftNode ee == m && action ed == action ee then
                            case sim lts1 lts2 (rightNode ed) (rightNode ee)
                                             (edgeList lts1) (edgeList lts2)
                                                     (List.nub ((n, m) : l)) of
                                    (k, True) -> case sim lts1 lts2 n m
                                                      e1t (edgeList lts2) l of
                                        (o, True) -> (List.nub (k ++ o), True)
                                        (_, False) -> ([], False)
                                    (_, False) -> sim lts1 lts2 n m ed1 e2t l
                        else sim lts1 lts2 n m ed1 e2t l
        else sim lts1 lts2 n m e1t (edgeList lts2) l