sybila / biodivine-lib-param-bn

Rust library for working with parametrised Boolean networks.
MIT License
2 stars 2 forks source link

Reachability method with less overhead #55

Closed daemontus closed 7 months ago

daemontus commented 7 months ago

This PR introduces a better reachability algorithm which uses structural information about the BN to eliminate certain transition checks and thus reduces overhead.

This is mostly a "constant factor" improvement, and in certain edge cases can be even slower (produces slightly larger BDDs), but overall seems to be worth it:

ID Basic Structural
002 DNF DNF
004 DNF DNF
012 28s 12s
016 27s 9s
019 1.5s 0.3s
039 141s 222s
050 2154s 1843s
051 8s 7s
059 0.7s 1.4s
078 8783s 2477s
079 DNF DNF
080 35s 14s
082 DNF DNF
083 DNF DNF
092 9s 6s
143 1.5s 0.5s
148 4s 2s
151 2314s 307s
160 24s 4s
179 4s 1s
192 DNF DNF
195 DNF DNF
204 34s 13s
207 4s 2s
209 DNF DNF
210 DNF DNF
211 DNF DNF
220 DNF DNF
222 DNF DNF
223 213s 4s
224 5s 3s
codecov[bot] commented 7 months ago

Codecov Report

Attention: 8 lines in your changes are missing coverage. Please review.

Comparison is base (2503d58) 80.36% compared to head (27c3442) 80.42%.

Files Patch % Lines
src/symbolic_async_graph/reachability.rs 89.04% 8 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## master #55 +/- ## ========================================== + Coverage 80.36% 80.42% +0.06% ========================================== Files 71 72 +1 Lines 4827 4890 +63 ========================================== + Hits 3879 3933 +54 - Misses 948 957 +9 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.