{-# LANGUAGE FlexibleInstances #-}
module DCLabel.QC_Core where


import Test.QuickCheck hiding (label) 
import Control.Monad (liftM)
import DCLabel.Core
import DCLabel.Lattice 
import Data.List

instance Arbitrary Principal where 
     arbitrary = do p <- oneof $ map return ["A", "B", "C"]
                    return $ principal p


instance Arbitrary a => Arbitrary (Disj a) where 
     arbitrary = sized disjunction 
                 where disjunction 0 = return $ MkDisj { disj = [] }
                       disjunction n = do a  <- arbitrary
                                          m  <- choose (0, n-1) 
                                          djs <- disjunction m
                                          return $ MkDisj $ a:(disj djs)     
     shrink (MkDisj ls) = [MkDisj l | l <- tails ls]


instance Arbitrary a => Arbitrary (Conj (Disj a)) where 
     arbitrary = sized conjunction 
                 where conjunction 0 = oneof [return $ MkConj { conj = [] } , 
                                              return $ MkConj { conj = [MkDisj []] },
                                              return $ MkConj { conj = [MkDisj [], MkDisj []] } ] 
                       conjunction n = do a  <- arbitrary
                                          m  <- choose (0, n-1) 
                                          cjs <- conjunction m
                                          return $ MkConj $ a:(conj cjs)     
     shrink (MkConj ls) = [MkConj ll | l <- tails ls, ll <- shrink l]


instance Arbitrary a => Arbitrary (Label a) where
  arbitrary = mkArbLbl arbitrary
    where mkArbLbl :: Gen (Conj (Disj a)) -> Gen (Label a)
          mkArbLbl = liftM MkLabel
          
instance Arbitrary a => Arbitrary (DCLabel a) where
  arbitrary = do s <- arbitrary
                 i <- arbitrary 
                 return $ MkDCLabel { secrecy = s, integrity = i }


-- nubLabel does not modify the semantics of the label 
prop_nubLabel :: Ord a => Label a -> Bool
prop_nubLabel l = let l' = nubLabel l 
                  in l `implies` l' && l' `implies` l

--  Reduce does not modify the semantics of the label
--  Ale: I will keep the original label as it is, without nubLabel.
prop_reduce :: Ord a => Label a -> Bool
prop_reduce l = let l' = reduceLabel l 
                in  l `implies` l' && l' `implies` l 
--                   let l1 = nubLabel ul1
--                       l2  = reduceLabel l1
--                   in l1 `implies` l2 && l2 `implies` l1

prop_reduce_idem :: Ord a => Label a -> Bool 
prop_reduce_idem l = let l'  = reduceLabel l 
                         l'' = reduceLabel l' 
                     in l' == l''

-- Partial order for DCLabels
prop_dc_porder :: Ord a => (DCLabel a, DCLabel a) -> Bool
prop_dc_porder (l1,l2) = let l1' = reduceDC l1
                             l2' = reduceDC l2
                             ge = l1' `canflowto` l2'
                             le = l2' `canflowto` l1'
                             eq = l2' == l1'
                         in (eq && ge && le) ||  -- ==
                            ((not eq) && (ge || le) && (ge /= le)) || -- < or >
                            (not (eq || ge || le)) -- incomparable

-- Check that labels flow to their join for DCLabels
prop_DC_join :: Ord a => (DCLabel a, DCLabel a) -> Bool
prop_DC_join (l1,l2) = let l3 = l1 `join` l2
                           t1 = l1 `canflowto` l3
                           t2 = l2 `canflowto` l3
                       in t1 && t2

-- Check that join is the least upper bound for DCLabels
-- Ale: we need to fix this since it is difficult to satisfy the hypothesis. Need to think about it.
prop_dc_join_lub :: (Ord a, Show a, Arbitrary a)
                 => (DCLabel a, DCLabel a) -> Property
prop_dc_join_lub (l1,l2) = forAll (gen l1) $ \l3' ->
 (l1 `canflowto` l3') && (l2 `canflowto` l3') ==> (l1 `join` l2) `canflowto` l3'
    where gen :: Arbitrary a => DCLabel a -> Gen (DCLabel a)
          gen _ = arbitrary
                  

-- Check that meet flows to the labels making it, for DCLabels
prop_dc_meet :: Ord a => (DCLabel a, DCLabel a) -> Bool
prop_dc_meet (l1,l2) = let l3 = l1 `meet` l2
                           t1 = l3 `canflowto` l1
                           t2 = l3 `canflowto` l2
                       in t1 && t2

-- Check that meet the greatest lower bound for DCLabels
prop_dc_meet_glb :: (Ord a, Show a, Arbitrary a)
                 => (DCLabel a, DCLabel a) -> Property
prop_dc_meet_glb (l1,l2) = forAll (gen l1) $ \l3' ->
 (l3' `canflowto` l1) && (l3' `canflowto` l2) ==> l3' `canflowto` (l1 `meet` l2)
    where gen :: Arbitrary a => DCLabel a -> Gen (DCLabel a)
          gen _ = arbitrary


type DCLabelPair a = (DCLabel a, DCLabel a)
checks n = do 
  let args = stdArgs { maxSuccess = n, maxSize = n, maxDiscard = 10000}
  putStrLn "Checking function nubLabel..."
  quickCheckWith args (prop_nubLabel :: Label Principal -> Bool)
  putStrLn "Checking function reduce..."
  quickCheckWith args (prop_reduce :: Label Principal -> Bool)
  putStrLn "Checking idempotence of function reduce..."
  quickCheckWith args (prop_reduce_idem :: Label Principal -> Bool)
  putStrLn "Checking the join operation..."
  quickCheckWith args (prop_DC_join ::  DCLabelPair Principal -> Bool)
  putStrLn "Checking the join operation is indeed the least upper bound..."
  quickCheckWith args (prop_dc_join_lub :: DCLabelPair Principal -> Property)
  putStrLn "Checking the meet operation..."
  quickCheckWith args (prop_dc_meet :: DCLabelPair Principal -> Bool)
  putStrLn "Checking the meet operation is indeed the greatest lower bound..."
  quickCheckWith args (prop_dc_meet_glb :: DCLabelPair Principal -> Property)
  putStrLn "Checking DC labels form a partial order..."
  quickCheckWith args (prop_dc_porder :: DCLabelPair Principal -> Bool)


l1 = MkDCLabel {secrecy = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "B"}]},MkDisj {disj = []},MkDisj {disj = []}]}}, integrity = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "A"}]},MkDisj {disj = []},MkDisj {disj = []}]}}}
l2 = MkDCLabel {secrecy = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "C"}]},MkDisj {disj = []}]}}, integrity = MkLabel {label = MkConj {conj = [MkDisj {disj = [MkPrincipal {name = "B"}]}]}}}