muddychildren benchmark: include DD lib, automate tex/pdf output

Makefile

@@ -11,10 +11,11 @@ clean:
 	find src/ -iname *.hi -type f -print | xargs /bin/rm -f
 	find src/ -iname *.o -type f -print | xargs /bin/rm -f
 
-MCBENCHMARKS = DEMOS5 CacBDD CUDD Trans Triangle NonS5 NonS5Trans
+MCBENCHMARKS = Triangle CacBDD DD CUDD CUDDz K DEMOS5 Trans TransK
 
-benchmc-results.csv:
-	stack bench :bench-muddychildren --benchmark-arguments "$(MCBENCHMARKS) --csv benchmc-results.csv"
+bench/muddychildren.pdf: Makefile bench/muddychildren.hs bench/muddychildren.tex
+	stack bench :bench-muddychildren --benchmark-arguments "$(MCBENCHMARKS) --csv bench/muddychildren-results.csv"
+	cd bench && latexmk -pdf -quiet -interaction=nonstopmode
 
 todo:
 	@bash -c 'grep -nr "TODO" {src,exec,test,bench}'

bench/.gitignore

@@ -0,0 +1,16 @@
+*.pdf
+*.aux
+*.log
+*.synctex.gz
+*.out
+*.bbl
+*.blg
+*.toc
+*.fls
+*.fdb_latexmk
+*.synctex*
+*.bcf
+*.run.xml
+*.thm
+*.spl
+*.OLD

bench/muddychildren.hs

@@ -22,6 +22,7 @@ import SMCDEL.Internal.MyHaskCUDD
 import qualified SMCDEL.Explicit.DEMO_S5 as DEMO_S5
 import qualified SMCDEL.Explicit.S5
 import qualified SMCDEL.Symbolic.S5
+import qualified SMCDEL.Symbolic.S5_DD
 import qualified SMCDEL.Symbolic.S5_CUDD
 import qualified SMCDEL.Translations.S5
 import qualified SMCDEL.Translations.K
@@ -47,6 +48,10 @@ findNumberCacBDD :: Int -> Int -> Int
 findNumberCacBDD = findNumberWith (cacMudScnInit,SMCDEL.Symbolic.S5.evalViaBdd) where
   cacMudScnInit n m = ( SMCDEL.Symbolic.S5.KnS (mudPs n) (SMCDEL.Symbolic.S5.boolBddOf Top) [ (show i,delete (P i) (mudPs n)) | i <- [1..n] ], mudPs m )
 
+findNumberDD :: Int -> Int -> Int
+findNumberDD = findNumberWith (ddMudScnInit,SMCDEL.Symbolic.S5_DD.evalViaBdd) where
+  ddMudScnInit n m = ( SMCDEL.Symbolic.S5_DD.KnS (mudPs n) (SMCDEL.Symbolic.S5_DD.boolBddOf Top) [ (show i,delete (P i) (mudPs n)) | i <- [1..n] ], mudPs m )
+
 findNumberCUDD :: Manager -> Int -> Int -> Int
 findNumberCUDD mgr n m =
   let cuddMudScnInit = ( SMCDEL.Symbolic.S5_CUDD.KnS mgr (mudPs n) (SMCDEL.Symbolic.S5_CUDD.boolDdOf mgr Top :: Dd B O1 I1) [ (show i, delete (P i) (mudPs n)) | i <- [1..n] ], mudPs m )
@@ -123,26 +128,27 @@ benchMain = do
   defaultMainWith myConfig (map mybench
     [ ("Triangle"  , findNumberTriangle  , [7..40] )
     , ("CacBDD"    , findNumberCacBDD    , [3..40] )
+    , ("DD"        , findNumberDD        , [3..30] )
     , ("CUDD"      , findNumberCUDD mgr  , [3..40] )
     , ("CUDDz"     , findNumberCUDDz mgr , [3..40] )
     , ("K"         , findNumberK         , [3..12] )
     , ("DEMOS5"    , findNumberDemoS5    , [3..12] )
     , ("Trans"     , findNumberTrans     , [3..12] )
-    , ("TransK"    , findNumberTransK    , [3..11] ) ])
+    , ("TransK"    , findNumberTransK    , [3..10] ) ])
   where
     mybench (name,f,range) = bgroup name $ map (run f) range
     run f k = bench (show k) $ whnf (\n -> f n n) k
     myConfig = defaultConfig { Criterion.Types.csvFile = Just theCSVname }
 
 theCSVname :: String
-theCSVname = "muddychildren-results.csv"
+theCSVname = "bench/muddychildren-results.csv"
 
 prepareMain :: IO ()
 prepareMain = do
   oldResults <- doesFileExist theCSVname
   when oldResults $ do
     putStrLn "moving away old results!"
-    renameFile theCSVname ("OLD-results-" ++ theCSVname)
+    renameFile theCSVname (theCSVname ++ ".OLD")
     oldDATfile <- doesFileExist (theCSVname ++ ".dat")
     when oldDATfile $ removeFile (theCSVname ++ ".dat")
 

bench/muddychildren.tex

@@ -0,0 +1,35 @@
+\documentclass{article}
+\usepackage{pgfplots}
+\pgfplotsset{compat=1.17}
+
+\usepackage[margin=2cm]{geometry}
+
+\title{Muddy Children Benchmark}
+\author{SMCDEL}
+
+\begin{document}
+
+\begin{figure}
+  \centering
+  \begin{tikzpicture}
+    \pgfplotstableread{muddychildren-results.csv.dat}
+    \datatable
+    \begin{axis}[legend pos=north east, width=0.95\linewidth, grid=major,
+      ylabel=seconds, ymode=log, ymax=3000,
+      xlabel=no. of children (all muddy),
+      unbounded coords=jump]
+      \addlegendentry{Triangle}        \addplot table[y=Triangle] from \datatable;
+      \addlegendentry{CacBDD}          \addplot table[y=CacBDD] from \datatable;
+      \addlegendentry{DD}              \addplot table[y=DD] from \datatable;
+      \addlegendentry{CUDD}            \addplot table[y=CUDD] from \datatable;
+      \addlegendentry{CUDDz}           \addplot table[y=CUDDz] from \datatable;
+      % \addlegendentry{K (CacBDD)}      \addplot table[y=K] from \datatable;
+      \addlegendentry{DEMO-S5}         \addplot table[y=DEMOS5] from \datatable;
+      \addlegendentry{Trans (CacBDD)}  \addplot table[y=Trans] from \datatable;
+      \addlegendentry{TransK (CacBDD)} \addplot table[y=TransK] from \datatable;
+    \end{axis}
+  \end{tikzpicture}
+  \caption{Results.}
+\end{figure}
+
+\end{document}