content: {-# LANGUAGE FlexibleContexts #-}
  {- |
  Module      :  ./Temporal/Mu.hs
  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
  
  
  -- ----------------------------------------------------------------------------
  