module Main where 

import LIO
import LIO.TCB
import LIO.DCLabel

-- | Simple secrecy component example
s :: CNF
s =  ("Alice" \/ "Bob") /\  "Carla"

-- | Simple integrity component example
i :: CNF
i = "Alice" /\ "Carla"

-- | Simple label
l1 :: DCLabel
l1 = s %% i

-- | Simple label
l2 :: DCLabel
l2 = "Djon" %% "Alice"

-- | Creating privilege using constructor from TCB
p :: DCPriv
p = PrivTCB  $ "Alice" /\ "Carla"

main = do
  putStrLn $ "Label 1: " ++ show l1
  putStrLn $ "Label 2: " ++ show l2
  putStrLn $ "Join of labels: " ++ show (l1 `lub` l2)
  putStrLn $ "Meet of labels: " ++ show (l1 `glb` l2)
  putStrLn $ "Privileges: " ++ show p
  putStrLn $ "Label 1 flows to Label 2? " ++ (show $ canFlowTo l1 l2)
  putStrLn $ "Label 1 flows to Label 2 given privileges? " ++
             (show $ canFlowToP p l1 l2)
{-
Output:
ghci> main
Label 1: "Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"
Label 2: "Djon" %% "Alice"
Join of labels: "Carla" /\ "Djon" /\ ("Alice" \/ "Bob") %% "Alice"
Meet of labels: ("Carla" \/ "Djon") /\ ("Alice" \/ "Bob" \/ "Djon") %% "Alice" /\ "Carla"
Privileges: PrivTCB ("Alice" /\ "Carla")
Label 1 flows to Label 2? False
Label 1 flows to Label 2 given privileges? True
-}