search

jrclogic / SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.
https://w4eg.de/malvin/illc/smcdelweb
GNU General Public License v2.0
39 stars 9 forks source link

provide Symbolic.S5_DD using haskell-decision-diagrams as BDD package #26

Closed m4lvin closed 3 months ago

m4lvin commented 1 year ago

See https://github.com/msakai/haskell-decision-diagrams

m4lvin commented 7 months ago

Work in progress since https://github.com/jrclogic/SMCDEL/commit/a7701ca9ee8ce0cca6e455de79c1bfd26dbf9f11

Benchmarks added in https://github.com/jrclogic/SMCDEL/commit/c1720cbfbf2a4d3d9bca90b35fc4b3bb895ef612 - in the plot below "DD" is the version using decision-diagrams.

Screenshot_20231124_172442

m4lvin commented 7 months ago

Some profiling results:

    Tue Nov 28 14:14 2023 Time and Allocation Profiling Report  (Final)

       bench-muddychildren +RTS -p -RTS DD CUDD --csv bench/muddychildren-results.csv

    total time  =     6446.78 secs   (6446778 ticks @ 1000 us, 1 processor)
    total alloc = 7,015,669,765,456 bytes  (excludes profiling overheads)

COST CENTRE       MODULE                                 SRC                                                       %time %alloc

insert'           Data.HashTable.ST.Cuckoo               src/Data/HashTable/ST/Cuckoo.hs:(417,1)-(424,12)           10.4    6.6
lookup            Data.HashTable.ST.Cuckoo               src/Data/HashTable/ST/Cuckoo.hs:135:5-28                    8.8    6.3
lookup#           Data.HashMap.Internal                  Data/HashMap/Internal.hs:609:1-82                           8.2    0.0
hashInt           Data.Hashable.LowLevel                 src/Data/Hashable/LowLevel.hs:(64,1)-(80,31)                5.4    7.8
ghashWithSalt     Data.Hashable.Generic.Instances        src/Data/Hashable/Generic/Instances.hs:43:5-36              5.3   11.1
primitive         Control.Monad.Primitive                Control/Monad/Primitive.hs:211:3-16                         5.1    5.5
mkApplyOp.f       Data.DecisionDiagram.BDD               src/Data/DecisionDiagram/BDD.hs:(266,7)-(279,22)            4.2    5.4
modifyAdvice      Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:104:10-22     3.4    4.2
hashWithSalt      Data.Hashable.Class                    src/Data/Hashable/Class.hs:334:5-26                         3.4    0.0
$mLeaf.\          Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:82:19-36      2.6    0.5
$mBranch.\        Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:92:29-59      2.5    1.7
hashWithSalt      Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:71:3-46       2.4    4.1
grow.rehash.go    Data.HashTable.ST.Cuckoo               src/Data/HashTable/ST/Cuckoo.hs:(735,9)-(747,29)            2.3    2.1
ghashWithSalt     Data.Hashable.Generic.Instances        src/Data/Hashable/Generic/Instances.hs:(34,5)-(35,60)       2.1    3.7
intern            Data.Interned.Internal                 Data/Interned/Internal.hs:(81,1)-(90,33)                    1.8    3.2
liftHashWithSalt2 Data.Hashable.Class                    src/Data/Hashable/Class.hs:553:5-58                         1.7    3.7
hashWithSalt      Data.DecisionDiagram.BDD               src/Data/DecisionDiagram/BDD.hs:171:17-24                   1.7    0.0
ghashWithSalt     Data.Hashable.Generic.Instances        src/Data/Hashable/Generic/Instances.hs:39:5-62              1.5    6.9
from              Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:110:19-25     1.4    7.4
$mT.\             Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:74:14-29      1.4    0.0
hashSum           Data.Hashable.Generic.Instances        src/Data/Hashable/Generic/Instances.hs:111:5-89             1.4    2.8
==                Data.DecisionDiagram.BDD.Internal.Node src/Data/DecisionDiagram/BDD/Internal/Node.hs:110:15-16     1.2    0.0
defaultHash       Data.Hashable.Class                    src/Data/Hashable/Class.hs:308:1-38                         0.9    1.1
insert            Data.HashTable.ST.Cuckoo               src/Data/HashTable/ST/Cuckoo.hs:133:5-28                    0.7    1.2
hashWithSalt      Data.Hashable.Class                    src/Data/Hashable/Class.hs:235:5-38                         0.4    1.4
writeArray        Data.HashTable.Internal.IntArray       src/Data/HashTable/Internal/IntArray.hs:(103,1)-(105,30)    0.3    1.1