{-# LANGUAGE FlexibleContexts #-}
{- |
Module      :  $Header$
Copyright   :  (c) Klaus Hartke, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  non-portable (FlexibleContexts)

-}

module Mu where

import Control.Monad as Monad
import Data.Set as Set
import Kripke


{- ----------------------------------------------------------------------------
Formulas of the µ-Calculus
---------------------------------------------------------------------------- -}

--
{- Given a finite set of variables, the set of µ-calculus pre-formulas is the
set of formulas that can be derived from the following definitions: -}
--

data StateFormula a = Var a
                    | Snot (StateFormula a)
                    | Sand (StateFormula a) (StateFormula a)
                    | Sor (StateFormula a) (StateFormula a)
                    | E (PathFormula a)
                    | A (PathFormula a)
                    | Diamond (StateFormula a)
                    | Box (StateFormula a)
                    | DiamondPast (StateFormula a)
                    | BoxPast (StateFormula a)
                    | Mu a (StateFormula a)
                    | Nu a (StateFormula a)
                     deriving (Show)


data PathFormula a = SF (StateFormula a)
                   | Pnot (PathFormula a)
                   | Pand (PathFormula a) (PathFormula a)
                   | Por (PathFormula a) (PathFormula a)
                   | X (PathFormula a)
                    deriving (Show)

--
{- The set of µ-calculus formulas is the subset of pre-formulas where each
subformula of the form (Mu x phi) or (Nu x phi) statisfies the constraint
that all occurrences of x in phi occur under an even number of negation
symbols. -}
--
{- A subformula, where all X operators occur in the scope of a path quantifier
(E or A) is a state formula, otherwise it is a path formula. The semantics
of state formulas is defined on states, while the semantics of path formulas
is defined on paths of the Kripke structure. -}
--


{- ----------------------------------------------------------------------------
Negation Normal Form
---------------------------------------------------------------------------- -}

nnfS :: StateFormula a -> StateFormula a

nnfS (Snot (Var x )) = Snot (Var x)
nnfS (Snot (Snot phi )) = nnfS phi
nnfS (Snot (Sand phi psi)) = Sor (nnfS (Snot phi)) (nnfS (Snot psi))
nnfS (Snot (Sor phi psi)) = Sand (nnfS (Snot phi)) (nnfS (Snot psi))
nnfS (Snot (A phi )) = E (nnfP (Pnot phi))
nnfS (Snot (E phi )) = A (nnfP (Pnot phi))
nnfS (Snot (Box phi )) = Diamond (nnfS (Snot phi))
nnfS (Snot (Diamond phi )) = Box (nnfS (Snot phi))
nnfS (Snot (BoxPast phi )) = DiamondPast (nnfS (Snot phi))
nnfS (Snot (DiamondPast phi )) = BoxPast (nnfS (Snot phi))
nnfS (Snot (Mu x phi )) = Nu x (nnfS (Snot phi))
nnfS (Snot (Nu x phi )) = Mu x (nnfS (Snot phi))

nnfS (Var x ) = Var x
nnfS (Sand phi psi) = Sand (nnfS phi) (nnfS psi)
nnfS (Sor phi psi) = Sor (nnfS phi) (nnfS psi)
nnfS (A phi ) = A (nnfP phi)
nnfS (E phi ) = E (nnfP phi)
nnfS (Box phi ) = Box (nnfS phi)
nnfS (Diamond phi ) = Diamond (nnfS phi)
nnfS (BoxPast phi ) = BoxPast (nnfS phi)
nnfS (DiamondPast phi ) = DiamondPast (nnfS phi)
nnfS (Mu x phi ) = Mu x (nnfS phi)
nnfS (Nu x phi ) = Nu x (nnfS phi)


nnfP :: PathFormula a -> PathFormula a

nnfP (Pnot (Pnot phi )) = nnfP phi
nnfP (Pnot (Pand phi psi)) = Por (nnfP (Pnot phi)) (nnfP (Pnot psi))
nnfP (Pnot (Por phi psi)) = Pand (nnfP (Pnot phi)) (nnfP (Pnot psi))
nnfP (Pnot (X phi )) = X (nnfP (Pnot phi))
nnfP (Pnot (SF phi )) = SF (nnfS (Snot phi))

nnfP (Pand phi psi) = Pand (nnfP phi) (nnfP psi)
nnfP (Por phi psi) = Por (nnfP phi) (nnfP psi)
nnfP (X phi ) = X (nnfP phi)
nnfP (SF phi ) = SF (nnfS phi)


{- ----------------------------------------------------------------------------
Normal Form of µ-Calculus Formulas
---------------------------------------------------------------------------- -}

--
{- For every formula of the µ-calculus, there is an equivalent formula of the
µ-calculus where neither path quantifiers E, A nor X operators occur. -}
--
{- We ensure that the given formula is in negation normal form. Hence, negation
symbols only occur in front of variables, which means that we can neglect
Pnot. -}
--

munf :: Set a -> StateFormula a -> StateFormula a

munf vars phi = munf' (nnfS phi)
    where
        munf' (Var x) = Var x
        munf' (Snot (Var x)) = Snot (Var x)
        munf' (Sand phi psi) = Sand (munf' phi) (munf' psi)
        munf' (Sor phi psi) = Sor (munf' phi) (munf' psi)
        munf' (Mu x phi) = Mu x (munf' phi)
        munf' (Nu x phi) = Nu x (munf' phi)
        munf' (Diamond phi) = Diamond (munf' phi)
        munf' (Box phi) = Box (munf' phi)
        munf' (DiamondPast phi) = DiamondPast (munf' phi)
        munf' (BoxPast phi) = BoxPast (munf' phi)
        munf' (A phi) = Snot (munf' (E (nnfP (Pnot phi))))
        munf' (E (SF phi)) = Sand (munf' phi) phiinf
        munf' (E (Por phi psi)) = Sor (munf' (E phi)) (munf' (E psi))
        munf' (E (X phi)) = Sand (Diamond (munf' (E phi))) phiinf
        munf' (E (Pand phi psi)) = error "Read the fucking book, pg. 100"

        phiinf = Nu (Set.findMin vars) (Diamond (Var (Set.findMin vars)))


{- ----------------------------------------------------------------------------
Local Model Checking for the µ-Calculus
---------------------------------------------------------------------------- -}

--
{- We assume that the considered formulas fulfill the following syntactic
requirements, that can be achieved without loss of generality: -}
--
{- * We only consider formulas in guarded normal form, so that every bound
variable occurs in the scope of a modal operator. Moreover, we assume
negation normal form, so that negation symbols only occur before
variables (that are not bound). -}
--
{- * We assume that every bound variable is bound only once and has no free
occurrences, so that we can define for a formula an associated function
that maps a bound variable to the unique subformula where the variable
is bound. -}
--

d :: (Eq a) => StateFormula a -> a -> Maybe (StateFormula a)

d (Snot phi) x = d phi x
d (Sand phi psi) x = Monad.mplus (d phi x) (d psi x)
d (Sor phi psi) x = Monad.mplus (d phi x) (d psi x)
d (Mu x' phi) x = if x' == x then Just (Mu x' phi) else d phi x
d (Nu x' phi) x = if x' == x then Just (Nu x' phi) else d phi x
d (Diamond phi) x = d phi x
d (Box phi) x = d phi x
d (DiamondPast phi) x = d phi x
d (BoxPast phi) x = d phi x
d (Var x') x = Nothing


sucE :: (Kripke m a s, Ord a, Ord s) => m -> Set s -> Set s

sucE k = Set.fold (Set.union . next k) Set.empty


preE :: (Kripke m a s, Ord a, Ord s) => m -> Set s -> Set s

preE k y = Set.filter (not . Set.null . Set.intersection y . next k) (states k)


localCheck :: (Kripke k a s, Ord a, Ord s, Ord (s, StateFormula a)) => (k, s) ->
              StateFormula a -> Bool

localCheck (k, s) phi = localCheck' s phi Set.empty
    where
        localCheck' s (Snot (Var x)) callStack =
            not $ Set.member x (labels k s)
        localCheck' s (Sand phi psi) callStack =
            conj2 callStack $ Set.fromList [ (s, phi), (s, psi) ]
        localCheck' s (Sor phi psi) callStack =
            disj2 callStack $ Set.fromList [ (s, phi), (s, psi) ]
        localCheck' s (Mu x phi ) callStack =
            localCheck' s phi $ Set.insert (s, Mu x phi) callStack
        localCheck' s (Nu x phi ) callStack =
            localCheck' s phi $ Set.insert (s, Nu x phi) callStack
        localCheck' s (Diamond phi ) callStack =
            disj2 callStack $ Set.map (flip (,) phi) $ sucE k (Set.singleton s)
        localCheck' s (Box phi ) callStack =
            conj2 callStack $ Set.map (flip (,) phi) $ sucE k (Set.singleton s)
        localCheck' s (DiamondPast phi ) callStack =
            disj2 callStack $ Set.map (flip (,) phi) $ preE k (Set.singleton s)
        localCheck' s (BoxPast phi ) callStack =
            conj2 callStack $ Set.map (flip (,) phi) $ preE k (Set.singleton s)
        localCheck' s (Var x ) callStack =
            case d phi x of
                Nothing -> Set.member x (labels k s)
                Just d' -> if Set.member (s, d') callStack then
                               case d' of
                                   Mu _ _ -> True
                                   Nu _ _ -> False
                           else
                               localCheck' s d' callStack

        disj2 callStack = flip Set.fold True $ \ (s, phi) b -> b &&
                           localCheck' s phi callStack

        conj2 callStack = flip Set.fold False $ \ (s, phi) b -> b ||
                           localCheck' s phi callStack


-- ----------------------------------------------------------------------------
