smcdel-1.3.0: bench/sumandproduct.hs

{- |

-- * Sum and Product as a Benchmark

We compare the performance of SMCDEL and DEMO-S5 on the Sum \& Product problem.

We use the implementation in the module \texttt{SMCDEL.Examples.SumAndProduct},
see Section~\ref{subsec:exSAP}.
-}

module Main (main) where

import Criterion.Main
import Data.List (groupBy,sortBy)
import Data.Time (getCurrentTime, diffUTCTime)
import System.Environment (getArgs)
import SMCDEL.Explicit.DEMO_S5
import SMCDEL.Examples.SumAndProduct
import SMCDEL.Symbolic.S5

-- * DEMO definitions
-- The following is based on <http://www.cs.otago.ac.nz/staffpriv/hans/sumpro/>.

-- | Two agents
alice, bob :: Agent
(alice,bob) = (Ag 0,Ag 1)

-- | Initial pointed epistemic model with possible pairs 1<x<y, x+y<=100.
msnp :: EpistM (Int,Int)
msnp = Mo pairs [alice,bob] [] rels pairs where
  rels  = [ (alice,partWith (+)) , (bob,partWith (*)) ]
  partWith op = groupBy (\(x,y) (x',y') -> op x y == op x' y') $
    sortBy (\(x,y) (x',y') -> compare (op x y) (op x' y')) pairs

fmrs1e, fmrp2e, fmrs3e :: DemoForm (Int,Int)

-- | Sum says: I knew that you didn't know the two numbers.
fmrs1e = Kn alice (Conj [ Disj [ Ng (Info p)
                               , Ng (Kn bob (Info p))
                               ]
                        | p <- pairs])

-- | Product says: Now I know the two numbers
fmrp2e = Conj [ Disj [ Ng (Info p)
                     , Kn bob (Info p) ] | p <- pairs]

-- | Sum says: Now I know the two numbers too
fmrs3e = Conj [ Disj [ Ng (Info p)
                     , Kn alice (Info p) ] | p <- pairs]

main :: IO ()
main = do
  args <- getArgs
  if args == ["checkingOnly"]
    then do
      putStrLn "Benchmarking only the checking, without model generation."
      benchCheckingOnly
    else do
      putStrLn "Benchmarking the complete run."
      benchAllOnce

benchAllOnce :: IO ()
benchAllOnce = do
  putStrLn "*** Running DEMO_S5 ***"
  start <- getCurrentTime
  print $ updsPa msnp [fmrs1e, fmrp2e, fmrs3e]
  end <- getCurrentTime
  putStrLn $ "This took " ++ show (end `diffUTCTime` start) ++ " seconds.\n"

  putStrLn "*** Running SMCDEL ***"
  start2 <- getCurrentTime
  mapM_ (putStrLn . sapExplainState) sapSolutions
  end2 <- getCurrentTime
  putStrLn $ "This took " ++ show (end2 `diffUTCTime` start2) ++ " seconds.\n"

benchCheckingOnly :: IO ()
benchCheckingOnly = defaultMain [
  bgroup "checkingOnly"
    [ bench "DEMO-S5" $ nf (show . updsPa msnp) [fmrs1e, fmrp2e, fmrs3e]
    , bench "SMCDEL"  $ nf (sapExplainState . head . whereViaBdd sapKnStruct) sapProtocol
    ]
  ]