first release

.gitignore

@@ -14,3 +14,5 @@ cabal.sandbox.config
 *.prof
 *.aux
 *.hp
+BENCHDC
+BENCHMC

BDDREL.hs

@@ -0,0 +1,182 @@
+
+module BDDREL where
+import Control.Arrow
+import Data.HasCacBDD hiding (Top,Bot)
+import Data.List
+import Data.Maybe (fromJust)
+import DELLANG
+import KNSCAC (Scenario,KnState,texBDD)
+import KRIPKEDEL
+import KRIPKEVIS
+import SYMDEL
+
+problemPM :: PointedModel
+problemPM = ( KrM [0,1,2,3]
+  [ (0,[[0],[1,2,3]]), (1,[[0,1,2],[3]]) ]
+  [ (0,[(P 1,True ),(P 2,True )]),
+    (1,[(P 1,True ),(P 2,False)]),
+    (2,[(P 1,False),(P 2,True )]),
+    (3,[(P 1,False),(P 2,False)]) ], 1::State )
+
+problemKNS :: Scenario
+problemKNS = kripkeToKns problemPM
+
+type RelBDD = Bdd
+
+booloutof :: [Prp] -> [Prp] -> Bdd
+booloutof ps qs = conSet $
+  [ var n | (P n) <- ps ] ++
+  [ neg $ var n | (P n) <- qs \\ ps ]
+
+mv :: [Prp] -> [Prp]
+mv = map (fromJust . (`lookup` [ (P n, P  (2*n)      ) | n <- [0..] ])) -- represent p in the double vocabulary
+cp :: [Prp] -> [Prp]
+cp = map (fromJust . (`lookup` [ (P n, P ((2*n) + 1) ) | n <- [0..] ])) -- represent p' in the double vocabulary
+unprime :: [Prp] -> [Prp]
+-- Go from p' in double vocabulary to p in single vocabulary:
+unprime = map f where
+  f (P m) | even m = error "unprime failed: Number is even!"
+	  | otherwise = P $ fromJust (lookup m [ ((2*n) + 1, n) | n <- [0..] ])
+
+cpBdd :: Bdd -> Bdd
+cpBdd b | b == bot  = b
+	| b == top  = b
+	| otherwise = relabel [ (n, (2*n) + 1) | n <- [0..m] ] b where (Just m) = maxVarOf b
+
+unmvBdd :: Bdd -> Bdd
+unmvBdd b | b == bot  = b
+	  | b == top  = b
+	  | otherwise = relabel [ (2 * n, n) | n <- [0..m] ] b where (Just m) = maxVarOf b
+
+propRel2bdd :: [Prp] -> Rel KnState -> RelBDD 
+propRel2bdd voc rel = disSet (map linkbdd rel) where
+  linkbdd (here,there) = con (booloutof (mv here) (mv voc)) (booloutof (cp there) (cp voc))
+
+samplerel :: Rel KnState
+samplerel = [
+  ([],[]), ([],[P 1]), ([],[P 2]), ([],[P 1, P 2]),
+  ([P 1],[P 1]), ([P 1],[P 1, P 2]),
+  ([P 2],[P 2]), ([P 2],[P 1, P 2]),
+  ([P 1, P 2],[P 1, P 2])
+  ]
+
+data GeneralKripkeModel = GenKrM [State] [(Agent,Rel State)] [(State,KRIPKEDEL.Assignment)] deriving (Show)
+
+type GeneralPointedModel = (GeneralKripkeModel,State)
+
+myDispModel :: GeneralPointedModel -> IO ()
+myDispModel (GenKrM states rel val, cur)
+  = dispGenModel show showAgent showVal "" (GenVisModel states rel val cur)
+
+myTexModel :: GeneralPointedModel -> String -> IO String
+myTexModel (GenKrM states rel val, cur)
+  = texGenModel show showAgent showVal "" (GenVisModel states rel val cur)
+
+exampleModel :: GeneralKripkeModel
+exampleModel = GenKrM
+  [1,2]
+  [ (0,[ (1,2),(2,2) ]),
+    (1,[ (1,1),(2,2)       ]) ]
+  [ (1,[(P 0,True) ]),
+    (2,[(P 0,False)])]
+
+examplePointedModel :: GeneralPointedModel
+examplePointedModel = (exampleModel,1::State)
+
+getPropRel :: GeneralKripkeModel -> Agent -> Rel KnState
+getPropRel (GenKrM states rel val) i =
+  if length (nub (map snd val)) /= length states
+    then error "Model does not have distinct valuations."
+    else map (translate *** translate) (fromJust $ lookup i rel) where
+      translate n = map fst (filter snd $ fromJust $ lookup n val)
+
+relBddFor :: GeneralKripkeModel -> Agent -> RelBDD
+relBddFor model@(GenKrM _ _ val) i = propRel2bdd voc (getPropRel model i) where
+  voc = (map fst . snd . head) val
+
+data GenKnowStruct = GenKnS [Prp] Bdd [(Agent,RelBDD)] deriving (Eq,Show)
+
+type GenScenario = (GenKnowStruct,[Prp])
+
+bddOf :: GenKnowStruct -> Form -> Bdd
+bddOf _   Top           = top
+bddOf _   Bot           = bot
+bddOf _   (PrpF (P n))  = var n
+bddOf kns (Neg form)    = neg $ bddOf kns form
+bddOf kns (Conj forms)  = conSet $ map (bddOf kns) forms
+bddOf kns (Disj forms)  = disSet $ map (bddOf kns) forms
+bddOf kns (Xor  forms)  = xorSet $ map (bddOf kns) forms
+bddOf kns (Impl f g)    = imp (bddOf kns f) (bddOf kns g)
+bddOf kns (Equi f g)    = equ (bddOf kns f) (bddOf kns g)
+bddOf kns (Forall ps f) = forallSet (map fromEnum ps) (bddOf kns f)
+bddOf kns (Exists ps f) = existsSet (map fromEnum ps) (bddOf kns f)
+
+bddOf kns@(GenKnS allprops lawbdd obdds) (K i form) = unmvBdd result where
+  result = forallSet ps' (cpBdd lawbdd `imp` (omegai `imp` cpBdd (bddOf kns form)))
+  ps'    = map fromEnum $ cp allprops
+  (Just omegai) = lookup i obdds
+
+bddOf _ (Kw _ _) = error "bddOf failed: Kw not implemented"
+
+bddOf _ (Ck _ _)  = error "bddOf failed: Ck not implemented"
+bddOf _ (Ckw _ _) = error "bddOf failed: Ckw not implemented"
+
+bddOf kns@(GenKnS allprops lawbdd obdds) (PubAnnounce f g) = imp (bddOf kns f) g' where
+  g' = bddOf newkns g
+  newkns = GenKnS allprops (con lawbdd (bddOf kns f)) obdds
+bddOf _ (PubAnnounceW _ _) = error "bddOf failed: PubAnnounceW not implemented"
+
+bddOf _ (AnnounceW{}) = error "bddOf failed: AnnounceW not implemented"
+bddOf kns@(GenKnS allprops lawbdd obdds) (Announce ags f g) = imp (bddOf kns f) g' where
+  (P k)     = freshp allprops
+  newprops  = sort (P k:allprops)
+  newlawbdd = con lawbdd (imp (var k) (bddOf kns f))
+  newobdds  = map changeobdd obdds
+  changeobdd (i,oi) = if i `elem` ags
+    then (i,con oi (equ (var k) (var ((2*k)+1))))
+    else (i,oi)
+  newkns = GenKnS newprops newlawbdd newobdds
+  g'     = restrict (bddOf newkns g) (k,True)
+
+validViaBdd :: GenKnowStruct -> Form -> Bool
+validViaBdd kns@(GenKnS _ lawbdd _) f = top == imp lawbdd (bddOf kns f)
+
+evalViaBdd :: GenScenario -> Form -> Bool
+evalViaBdd (kns@(GenKnS allprops _ _),s) f = let
+    b    = restrictSet (bddOf kns f) list
+    list = [ (n,True) | (P n) <- s ] ++ [ (n,False) | (P n) <- allprops \\ s ]
+  in
+    case (b==top,b==bot) of
+      (True,_) -> True
+      (_,True) -> False
+      _        -> error "evalViaBdd failed: Composite BDD leftover."
+
+texGenStructure :: GenScenario -> String -> IO String
+texGenStructure (GenKnS props lawbdd obdds, state) filename = do
+  let (bddprefix,bddsuffix) = ("\\begin{array}{l} \\scalebox{0.4}{", "} \\end{array} \n")
+  lawbddtex <- texBDD lawbdd
+  obddstringspure <- mapM  (texBDD . snd) obdds
+  let obddstringpairs = zip (map fst obdds) obddstringspure
+  let obddstrings = map ( \(i,os) -> "O_" ++ show i ++ " = " ++ bddprefix ++ os ++ bddsuffix ) obddstringpairs
+  let fullstring = " \\left( \n"
+	++ texPropSet props ++ ", "
+	++ bddprefix ++ lawbddtex ++ bddsuffix
+	++ ", " ++ intercalate ", " obddstrings
+	++ " \\right) , " ++ texPropSet state
+  _ <- writeFile ("tmp/" ++ filename ++ ".tex") fullstring
+  return ("Structure was TeX'd to"++filename)
+
+genKrp2Kns :: GeneralPointedModel -> GenScenario
+genKrp2Kns (pm@(GenKrM states rel val), cur) = (GenKnS voc lawbdd obdds, trAt cur) where
+  voc    = (map fst . snd . head) val
+  lawbdd = disSet [ booloutof (trAt s) voc | s <- states ]
+  obdds  = [ (i, relBddFor pm i ) | i <- agents ]
+  agents = map fst rel
+  trAt s = map fst $ filter snd (fromJust $ lookup s val)
+
+exampleGenScn :: GenScenario
+exampleGenScn = genKrp2Kns examplePointedModel
+
+exampleGenStruct :: GenKnowStruct
+exampleGenState :: KnState
+(exampleGenStruct,exampleGenState) = exampleGenScn

BENCHDC.hs

@@ -0,0 +1,50 @@
+
+module Main (main) where
+import Control.Monad (when)
+import Data.Time (diffUTCTime,getCurrentTime,NominalDiffTime)
+import System.Environment (getArgs)
+import System.IO (hSetBuffering,BufferMode(NoBuffering),stdout)
+import DELLANG
+import KNSCAC
+import EXAMPLES (genDcKnsInit,genDcReveal)
+
+genDcCheckForm :: Int -> Form
+genDcCheckForm n = Impl (Neg (PrpF $ P 1)) $
+  PubAnnounceW (Xor [genDcReveal n i | i<-[1..n] ]) $
+    Disj [ K 1 (Conj [Neg $ PrpF $ P k | k <- [1..n]  ])
+	 , Conj [ K 1 (Disj [ PrpF $ P k | k <- [2..n] ])
+		, Conj [ Neg $ K 1 (PrpF $ P k) | k <- [2..n] ] ] ]
+
+genDcValid :: Int -> Bool
+genDcValid n = validViaBdd (genDcKnsInit n) (genDcCheckForm n)
+
+dcTimeThis :: Int -> IO NominalDiffTime
+dcTimeThis n = do
+  start <- getCurrentTime
+  let mykns@(KnS props _ _) = genDcKnsInit n
+  putStr $ show (length props) ++ "\t"
+  putStr $ show (length $ show mykns) ++ "\t"
+  putStr $ show (length $ show $ genDcCheckForm n) ++ "\t"
+  if genDcValid n then do
+    end <- getCurrentTime
+    return (end `diffUTCTime` start)
+  else
+    error "Wrong result."
+
+mainLoop :: [Int] -> Int -> IO ()
+mainLoop [] _ = putStrLn ""
+mainLoop (n:ns) limit = do
+  putStr $ show n ++ "\t"
+  result <- dcTimeThis n
+  print result
+  when (result <= fromIntegral limit) $ mainLoop ns limit
+
+main :: IO ()
+main = do
+  args <- getArgs
+  hSetBuffering stdout NoBuffering
+  case args of
+    [aInteger] | [(n,_)] <- reads aInteger -> do
+      putStrLn $ "n" ++ "\tn(prps)"++ "\tsz(KNS)"++ "\tsz(frm)" ++ "\ttime"
+      mainLoop (3:(5 : map (10*) [1..])) n
+    _ -> error "Please give a maximum runtime as an argument."

BENCHMC.hs

@@ -0,0 +1,111 @@
+
+module Main (main) where
+import Control.Monad
+import Data.List
+import Data.Time (getCurrentTime, NominalDiffTime, diffUTCTime)
+import System.Environment (getArgs)
+import System.IO (stdout, hSetBuffering, BufferMode(NoBuffering))
+import DELLANG
+import EXAMPLES
+import qualified DEMO_S5
+import qualified KNSCAC
+import qualified KNSCUDD
+import qualified KNSROB
+import qualified KNSNOO
+import qualified MCTRIANGLE
+
+checkForm :: Int -> Int -> Form
+checkForm n 0 = nobodyknows n
+checkForm n k = PubAnnounce (nobodyknows n) (checkForm n (k-1))
+
+findNumberWith :: (Int -> Int -> a, a -> Form -> Bool) -> Int -> Int -> Int
+findNumberWith (start,evalfunction) n m = loop 0 where
+  loop count = if evalfunction (start n m) (PubAnnounce (father n) (checkForm n count))
+    then loop (count+1)
+    else count
+
+mudPs :: Int -> [Prp]
+mudPs n = [P 1 .. P n]
+
+findNumberCacBdd :: Int -> Int -> Int
+findNumberCacBdd = findNumberWith (cacMudScnInit,KNSCAC.evalViaBdd) where
+  cacMudScnInit n m = ( KNSCAC.KnS (mudPs n) (KNSCAC.boolBddOf Top) [ (i,delete (P i) (mudPs n)) | i <- [1..n] ], [P 1 .. P m] )
+
+findNumberCUDD :: Int -> Int -> Int
+findNumberCUDD = findNumberWith (cuddMudScnInit,KNSCUDD.evalViaBdd) where
+  cuddMudScnInit n m = ( KNSCUDD.KnS (mudPs n) (KNSCUDD.boolBddOf Top) [ (i,delete (P i) (mudPs n)) | i <- [1..n] ], [P 1 .. P m] )
+
+findNumberRobBdd :: Int -> Int -> Int
+findNumberRobBdd = findNumberWith (robMudScnInit,KNSROB.evalViaBdd) where
+  robMudScnInit n m = ( KNSROB.KnS (mudPs n) (KNSROB.boolBddOf Top) [ (i,delete (P i) (mudPs n)) | i <- [1..n] ], [P 1 .. P m] )
+
+findNumberNooBdd :: Int -> Int -> Int
+findNumberNooBdd = findNumberWith (nooMudScnInit,KNSNOO.evalViaBdd) where
+  nooMudScnInit n m = ( KNSNOO.KnS (mudPs n) (KNSNOO.boolBddOf Top) [ (i,delete (P i) (mudPs n)) | i <- [1..n] ], [P 1 .. P m] )
+
+mudDemoKrpInit :: Int -> Int -> DEMO_S5.EpistM [Bool]
+mudDemoKrpInit n m = DEMO_S5.Mo states agents [] rels points where
+  states = DEMO_S5.bTables n
+  agents = map DEMO_S5.Ag [1..n]
+  rels = [(DEMO_S5.Ag i, [[tab1++[True]++tab2,tab1++[False]++tab2] |
+                   tab1 <- DEMO_S5.bTables (i-1),
+                   tab2 <- DEMO_S5.bTables (n-i) ]) | i <- [1..n] ]
+  points = [replicate (n-m) False ++ replicate m True]
+
+findNumberDemo :: Int -> Int -> Int
+findNumberDemo n m = findNumberDemoLoop n m 0 start where
+  start = DEMO_S5.upd_pa (mudDemoKrpInit n m) (DEMO_S5.fatherN n)
+
+findNumberDemoLoop :: Int -> Int -> Int -> DEMO_S5.EpistM [Bool] -> Int
+findNumberDemoLoop n m count curMod =
+  if DEMO_S5.isTrue curMod (DEMO_S5.dont n)
+    then findNumberDemoLoop n m (count+1) (DEMO_S5.upd_pa curMod (DEMO_S5.dont n))
+    else count
+
+findNumberTriangle :: Int -> Int -> Int
+findNumberTriangle n m = findNumberTriangleLoop 0 start where
+  start = MCTRIANGLE.update (MCTRIANGLE.mcModel (n-m,m)) (MCTRIANGLE.Qf MCTRIANGLE.some)
+
+findNumberTriangleLoop :: Int -> MCTRIANGLE.McModel -> Int
+findNumberTriangleLoop count curMod =
+  if MCTRIANGLE.eval curMod MCTRIANGLE.nobodyknows
+    then findNumberTriangleLoop (count+1) (MCTRIANGLE.update curMod MCTRIANGLE.nobodyknows)
+    else count
+
+timeWith :: Int -> Int -> (Int -> Int -> Int) -> IO NominalDiffTime
+timeWith n m function = do
+  start <- getCurrentTime
+  if function n m == (m - 1)
+    then do end <- getCurrentTime
+	    return (end `diffUTCTime` start)
+    else error "Wrong result."
+
+mainLoop :: [(Bool, Int -> Int -> Int)] -> [Int] -> Int -> IO ()
+mainLoop _  [] _ = putStrLn ""
+mainLoop fs (n:ns) limit = do
+  putStr $ show n ++ "\t"
+  results <- mapM (\(bit,f) ->
+    if bit then do
+      result <- timeWith n n f
+      putStr $ init (show result) ++ replicate (9 - length (show result)) '0' ++ "\t"
+      return result
+    else do
+      putStr "nan      \t"
+      return 0
+    ) fs
+  putStrLn ""
+  let newfs = map (\((bit,f),t) -> (bit && (t<= fromIntegral limit), f)) (zip fs results)
+  when (any fst newfs) $ mainLoop newfs ns limit
+
+main :: IO ()
+main = do
+  hSetBuffering stdout NoBuffering
+  putStrLn $ "Initializing CacBDD: 40==" ++ show (findNumberCacBdd 41 41)
+  putStrLn $ "Initializing CUDD: 40==" ++ show (findNumberCUDD 41 41)
+  putStrLn $ "n\t" ++ concatMap (++ "\t") ["TRIANGLE","KNSCAC  ","KNSCUDD ", "KNSROB  ","KNSNOO  ","DEMO-S5 "]
+  let allfs = [findNumberTriangle, findNumberCacBdd, findNumberCUDD, findNumberRobBdd, findNumberNooBdd, findNumberDemo]
+  args <- getArgs
+  case args of
+    [aInteger] | [(n,_)] <- reads aInteger ->
+      mainLoop (zip (repeat True) allfs) ([3..40]++[50,60,70,80,90,100]) n
+    _ -> error "Please give a maximum runtime as an argument."