{- | Module : ./GMP/GMP-CoLoSS/GMP/Logics/HM.hs

- Description : Implementation of logic instance HML

- Copyright : (c) Daniel Hausmann & Georgel Calin & Lutz Schroeder, DFKI Lab Bremen,

- Rob Myers & Dirk Pattinson, Department of Computing, ICL

- License : GPLv2 or higher, see LICENSE.txt

- Maintainer : hausmann@dfki.de

- Stability : provisional

- Portability : portable

-

- Provides the implementation of the matching functions of Henessy-Milner logic.

-}

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}

module GMP.Logics.HM where

import Data.List

import Data.Ratio

import Data.Maybe

import Debug.Trace

import Text.ParserCombinators.Parsec

import GMP.Logics.Generic

import GMP.Parser

{- ------------------------------------------------------------------------------

instance of feature for Hennessy-Milner logic

------------------------------------------------------------------------------ -}

data HM a = HM Char [Formula a] deriving (Eq, Show)

{- For each positive modal literal, there is a premise containing only one

sequent. This sequent contains the stripped positive literal and all

negated stripped negative literals with the same index.

e.g. seq = [ (M (HM a) p), !(M (HM b) q), (M (HM b) !p), !(M (HM a) !r)]

match seq = [ [[ p, r]], [[ !p, r]] ] -}

instance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature HM b c d where

nefMatch flags seq =

let stripnlits ind = [ Neg (head phi) | Neg (Mod (HM ind phi)) <- seq]

in if flags !! 1

then trace ("\n <HM-matching this:> " ++ pretty_list seq)

[ [[Sequent (head phi : stripnlits ind)]] | Mod (HM ind phi) <- seq]

else [ [[Sequent (head phi : stripnlits ind)]] |

Mod (HM ind phi) <- seq]

nefPretty d = case d of

HM c [] -> "[HM]" ++ show c ++ "nothing contained"

HM c e -> "[HM]" ++ show c ++ pretty (head e)

nefFeatureFromSignature sig = HM 'a'

nefFeatureFromFormula phi = HM 'a'

nefStripFeature (HM a phis) = phis

nefDisj2Conj (Mod (HM c phi)) = Mod (HM c [disj2conj (head phi)])

nefNegNorm (Mod (HM c phi)) = Mod (HM c [negNorm (head phi)])

nefParser sig = do c <- letter

return $ HM c

<?> "Parser.parseHMindex"

{- ------------------------------------------------------------------------------

instance of sigFeature for Hennessy-Milner logic

------------------------------------------------------------------------------ -}

instance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature HM b c d where

neGoOn = genericPGoOn