Merge pull request #10 from sybila/dev-sanitized-bdds

Sanitize BDDs in the result bundle

benchmarks/large_models/README.md

@@ -51,9 +51,10 @@ The standard output should contain the running time for the whole computation.
 The following table gives a summary of the expected results. Naturally, the actual runtime
 will differ based on the performance of your machine.
 
-|   Model   | State space | Parametrisations |  Runtime |
-|:---------:|:-----------:|:----------------:|---------:|
-| Apoptosis |   2.19e12   |      8.61e8      |  39350ms |
-|  Butanol  |   7.37e19   |      8.18e9      |  18310ms |
-|    EGFR   |   2.02e31   |         9        | 209698ms |
-|    MAPK   |    2.62e5   |      1.12e15     |   4949ms |
+|   Model   | State space | Parametrisations |         Runtime |
+|:---------:|:-----------:|:----------------:|----------------:|
+| Apoptosis |   2.19e12   |      8.61e8      |         39350ms |
+|  Butanol  |   7.37e19   |      8.18e9      |         18310ms |
+|   EGFR    |   2.02e31   |        9         |        209698ms |
+|   MAPK    |   2.62e5    |     1.12e15      |          4949ms |
+|  FA BRCA  |   2.68e8    |      1.52e9      |        153120ms |

benchmarks/large_models/[FA-BRCA-pathway]-[28v]-[72p]/fa-brca-fixed.aeon

@@ -0,0 +1,151 @@
+v_BRCA1 -> v_FANCD1N
+v_CHKREC -| v_FANCD1N
+v_ssDNARPA -> v_FANCD1N
+v_FANCD2I -> v_FANCD1N
+v_ATM -> v_BRCA1
+v_CHK2 -> v_BRCA1
+v_DSB -> v_BRCA1
+v_ATR -> v_BRCA1
+v_CHKREC -| v_BRCA1
+v_DSB -> v_ATM
+v_ATR -> v_ATM
+v_CHKREC -| v_ATM
+v_ATM -> v_FANCD2I
+v_FAcore -> v_FANCD2I
+v_DSB -> v_FANCD2I
+v_ATR -> v_FANCD2I
+v_H2AX -> v_FANCD2I
+v_USP1 -| v_FANCD2I
+v_FAcore ->? v_PCNATLS
+v_FAN1 -| v_PCNATLS
+v_ADD -> v_PCNATLS
+v_USP1 -| v_PCNATLS
+v_BRCA1 -> v_HRR
+v_FANCD1N -> v_HRR
+v_DSB -> v_HRR
+v_RAD51 -> v_HRR
+v_CHKREC -| v_HRR
+v_DSB -> v_DNAPK
+v_KU -> v_DNAPK
+v_CHKREC -| v_DNAPK
+v_ATM -> v_MRN
+v_DSB -> v_MRN
+v_KU -| v_MRN
+v_RAD51 -| v_MRN
+v_CHKREC -| v_MRN
+v_FANCD2I -? v_MRN
+v_ATM -| v_NHEJ
+v_DNAPK -> v_NHEJ
+v_DSB -> v_NHEJ
+v_ATR -? v_NHEJ
+v_KU -> v_NHEJ
+v_CHKREC -| v_NHEJ
+v_FANCJBRCA1 -| v_NHEJ
+v_ssDNARPA -? v_NHEJ
+v_XPF -> v_NHEJ
+v_MRN -| v_KU
+v_DSB -> v_KU
+v_CHKREC -| v_KU
+v_FANCD2I -| v_KU
+v_ICL -> v_FANCM
+v_CHKREC -| v_FANCM
+v_ATM -> v_CHK2
+v_DNAPK -> v_CHK2
+v_ATR -> v_CHK2
+v_CHKREC -| v_CHK2
+v_ATM -> v_H2AX
+v_DNAPK -> v_H2AX
+v_DSB -> v_H2AX
+v_ATR -> v_H2AX
+v_CHKREC -| v_H2AX
+v_NHEJ -| v_DSB
+v_HRR -| v_DSB
+v_DSB -> v_DSB
+v_FAN1 -> v_DSB
+v_XPF -> v_DSB
+v_NHEJ -> v_CHKREC
+v_ICL -| v_CHKREC
+v_PCNATLS -> v_CHKREC
+v_HRR -> v_CHKREC
+v_DSB -| v_CHKREC
+v_CHKREC -| v_CHKREC
+v_ADD -| v_CHKREC
+v_MRN -> v_ssDNARPA
+v_DSB -> v_ssDNARPA
+v_KU -| v_ssDNARPA
+v_RAD51 -| v_ssDNARPA
+v_FANCJBRCA1 -> v_ssDNARPA
+v_FANCD2I -> v_ssDNARPA
+v_ATM -> v_FAcore
+v_FANCM -> v_FAcore
+v_ATR -> v_FAcore
+v_CHKREC -| v_FAcore
+v_FANCM -| v_USP1
+v_FANCD1N -> v_USP1
+v_PCNATLS -> v_USP1
+v_FANCD2I -> v_USP1
+v_ATM -> v_FANCJBRCA1
+v_ICL -> v_FANCJBRCA1
+v_ATR -> v_FANCJBRCA1
+v_ssDNARPA -> v_FANCJBRCA1
+v_FANCM -| v_XPF
+v_p53 -> v_XPF
+v_MUS81 -> v_XPF
+v_FAcore -| v_XPF
+v_FAN1 -? v_XPF
+v_FANCD2I -? v_XPF
+v_ICL -> v_MUS81
+v_ATM -> v_CHK1
+v_DNAPK -> v_CHK1
+v_ATR -> v_CHK1
+v_CHKREC -| v_CHK1
+v_ATM -> v_p53
+v_CHK2 -> v_p53
+v_DNAPK -> v_p53
+v_ATR -> v_p53
+v_CHKREC -| v_p53
+v_CHK1 -> v_p53
+v_PCNATLS -| v_ADD
+v_MUS81 -> v_ADD
+v_FAN1 -> v_ADD
+v_ADD -> v_ADD
+v_XPF -> v_ADD
+v_ICL -> v_ICL
+v_DSB -| v_ICL
+v_FANCD1N -> v_RAD51
+v_CHKREC -| v_RAD51
+v_ssDNARPA -> v_RAD51
+v_ATM -> v_ATR
+v_FANCM -> v_ATR
+v_CHKREC -| v_ATR
+v_ssDNARPA -> v_ATR
+v_MUS81 -> v_FAN1
+v_FANCD2I -> v_FAN1
+$v_ADD: ((v_ADD & !v_PCNATLS) | ((v_MUS81 & (v_FAN1 | v_XPF)) & !v_PCNATLS))
+$v_ATM: ((v_DSB & !v_CHKREC) | (v_ATR & !v_CHKREC))
+$v_ATR: (((v_FANCM & !v_CHKREC) | (v_ATM & !v_CHKREC)) | (v_ssDNARPA & !v_CHKREC))
+$v_BRCA1: ((v_DSB & ((v_ATM | v_CHK2) | v_ATR)) & !v_CHKREC)
+$v_CHK1: (((v_ATM & !v_CHKREC) | (v_DNAPK & !v_CHKREC)) | (v_ATR & !v_CHKREC))
+$v_CHK2: (((v_ATM & !v_CHKREC) | (v_DNAPK & !v_CHKREC)) | (v_ATR & !v_CHKREC))
+$v_CHKREC: ((((v_PCNATLS & !v_DSB) | (v_NHEJ & !v_DSB)) | (v_HRR & !v_DSB)) | !((((((v_NHEJ | v_ICL) | v_PCNATLS) | v_HRR) | v_DSB) | v_CHKREC) | v_ADD))
+$v_DNAPK: ((v_DSB & v_KU) & !v_CHKREC)
+$v_DSB: (((v_XPF & !(v_HRR | v_NHEJ)) | (v_DSB & !(v_HRR | v_NHEJ))) | (v_FAN1 & !(v_HRR | v_NHEJ)))
+$v_FAN1: (v_MUS81 & v_FANCD2I)
+$v_FANCD1N: ((v_ssDNARPA & v_BRCA1) | ((v_FANCD2I & v_ssDNARPA) & !v_CHKREC))
+$v_FANCD2I: ((v_FAcore & ((v_ATM | v_ATR) | (v_DSB & v_H2AX))) & !v_USP1)
+$v_FANCJBRCA1: ((v_ssDNARPA & (v_ATM | v_ATR)) | (v_ICL & (v_ATM | v_ATR)))
+$v_FANCM: (v_ICL & !v_CHKREC)
+$v_FAcore: ((v_FANCM & (v_ATM | v_ATR)) & !v_CHKREC)
+$v_H2AX: ((v_DSB & ((v_ATM | v_DNAPK) | v_ATR)) & !v_CHKREC)
+$v_HRR: ((v_DSB & ((v_BRCA1 & v_FANCD1N) & v_RAD51)) & !v_CHKREC)
+$v_ICL: (v_ICL & !v_DSB)
+$v_KU: (v_DSB & !((v_CHKREC | v_MRN) | v_FANCD2I))
+$v_MRN: ((v_DSB & v_ATM) & !((v_RAD51 | (v_KU & v_FANCD2I)) | v_CHKREC))
+$v_MUS81: v_ICL
+$v_NHEJ: (((v_KU & (v_DNAPK & v_DSB)) & !(v_ATM & v_ATR)) | ((v_XPF & (v_DNAPK & v_DSB)) & !((v_FANCJBRCA1 & v_ssDNARPA) | v_CHKREC)))
+$v_PCNATLS: (((v_FAcore & v_ADD) & !(v_FAN1 | v_USP1)) | (v_ADD & !(v_FAN1 | v_USP1)))
+$v_RAD51: ((v_ssDNARPA & v_FANCD1N) & !v_CHKREC)
+$v_USP1: (((v_FANCD1N & v_FANCD2I) & !v_FANCM) | (v_PCNATLS & !v_FANCM))
+$v_XPF: (((v_p53 & v_MUS81) & !(v_FAcore & (v_FAN1 & v_FANCD2I))) | (v_MUS81 & !v_FANCM))
+$v_p53: ((((v_ATM & v_CHK2) & !v_CHKREC) | ((v_ATR & v_CHK1) & !v_CHKREC)) | (v_DNAPK & !v_CHKREC))
+$v_ssDNARPA: ((v_DSB & ((v_FANCJBRCA1 & v_FANCD2I) | v_MRN)) & !(v_KU | v_RAD51))

benchmarks/large_models/[FA-BRCA-pathway]-[28v]-[72p]/fa-brca-parametrized-annotated.aeon

@@ -0,0 +1,190 @@
+# Properties
+
+# existence of a "checkpoint" state
+#! dynamic_property: p1: #`3{x}: @{x}: (AX (~{x} & AF {x}))`#
+
+# existence of a "checkpoint" state that lies on at least two different cycles
+#! dynamic_property: p2: #`3{x}: @{x}: ((AX (~{x} & AF {x})) & (EF (!{y}: EX ~AF {y})))`#
+
+# existence of a pair of steady states
+#! dynamic_property: p3: #`3{x}: 3{y}: ((@{x}: ~{y} & AX {x}) & (@{y}: AX {y}))`#
+
+# existence of "fork" states in the system (states where system decides which terminal steady state to visit)
+#! dynamic_property: p4: #`3{x}: 3{y}: ((@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & (!{z}: AX {z})) & EF ({y} & (!{z}: AX {z})) & AX (EF ({x} & (!{z}: AX {z})) ^ EF ({y} & (!{z}: AX {z}))))`#
+
+## Model
+
+#position:v_ATM:0,0
+$v_ATM:((v_DSB & !v_CHKREC) | (v_ATR & !v_CHKREC))
+v_DSB -> v_ATM
+v_ATR -> v_ATM
+v_CHKREC -| v_ATM
+#position:v_BRCA1:0,0
+$v_BRCA1:((v_DSB & ((v_ATM | v_CHK2) | v_ATR)) & !v_CHKREC)
+v_ATM -> v_BRCA1
+v_CHK2 -> v_BRCA1
+v_DSB -> v_BRCA1
+v_ATR -> v_BRCA1
+v_CHKREC -| v_BRCA1
+#position:v_CHK2:0,0
+v_ATM -> v_CHK2
+v_DNAPK -> v_CHK2
+v_ATR -> v_CHK2
+v_CHKREC -| v_CHK2
+#position:v_DSB:0,0
+$v_DSB:(((v_XPF & !(v_HRR | v_NHEJ)) | (v_DSB & !(v_HRR | v_NHEJ))) | (v_FAN1 & !(v_HRR | v_NHEJ)))
+v_NHEJ -| v_DSB
+v_HRR -| v_DSB
+v_DSB -> v_DSB
+v_FAN1 -> v_DSB
+v_XPF -> v_DSB
+#position:v_ATR:0,0
+v_ATM -> v_ATR
+v_FANCM -> v_ATR
+v_CHKREC -| v_ATR
+v_ssDNARPA -> v_ATR
+#position:v_CHKREC:0,0
+$v_CHKREC:((((v_PCNATLS & !v_DSB) | (v_NHEJ & !v_DSB)) | (v_HRR & !v_DSB)) | !((((((v_NHEJ | v_ICL) | v_PCNATLS) | v_HRR) | v_DSB) | v_CHKREC) | v_ADD))
+v_NHEJ -> v_CHKREC
+v_ICL -| v_CHKREC
+v_PCNATLS -> v_CHKREC
+v_HRR -> v_CHKREC
+v_DSB -| v_CHKREC
+v_CHKREC -| v_CHKREC
+v_ADD -| v_CHKREC
+#position:v_FANCD1N:0,0
+v_BRCA1 -> v_FANCD1N
+v_CHKREC -| v_FANCD1N
+v_ssDNARPA -> v_FANCD1N
+v_FANCD2I -> v_FANCD1N
+#position:v_ssDNARPA:0,0
+$v_ssDNARPA:((v_DSB & ((v_FANCJBRCA1 & v_FANCD2I) | v_MRN)) & !(v_KU | v_RAD51))
+v_MRN -> v_ssDNARPA
+v_DSB -> v_ssDNARPA
+v_KU -| v_ssDNARPA
+v_RAD51 -| v_ssDNARPA
+v_FANCJBRCA1 -> v_ssDNARPA
+v_FANCD2I -> v_ssDNARPA
+#position:v_FANCD2I:0,0
+$v_FANCD2I:((v_FAcore & ((v_ATM | v_ATR) | (v_DSB & v_H2AX))) & !v_USP1)
+v_ATM -> v_FANCD2I
+v_FAcore -> v_FANCD2I
+v_DSB -> v_FANCD2I
+v_ATR -> v_FANCD2I
+v_H2AX -> v_FANCD2I
+v_USP1 -| v_FANCD2I
+#position:v_NHEJ:0,0
+$v_NHEJ:(((v_KU & (v_DNAPK & v_DSB)) & !(v_ATM & v_ATR)) | ((v_XPF & (v_DNAPK & v_DSB)) & !((v_FANCJBRCA1 & v_ssDNARPA) | v_CHKREC)))
+v_ATM -| v_NHEJ
+v_DNAPK -> v_NHEJ
+v_DSB -> v_NHEJ
+v_ATR -? v_NHEJ
+v_KU -> v_NHEJ
+v_CHKREC -| v_NHEJ
+v_FANCJBRCA1 -| v_NHEJ
+v_ssDNARPA -? v_NHEJ
+v_XPF -> v_NHEJ
+#position:v_ICL:0,0
+$v_ICL:(v_ICL & !v_DSB)
+v_ICL -> v_ICL
+v_DSB -| v_ICL
+#position:v_PCNATLS:0,0
+$v_PCNATLS:(((v_FAcore & v_ADD) & !(v_FAN1 | v_USP1)) | (v_ADD & !(v_FAN1 | v_USP1)))
+v_FAcore ->? v_PCNATLS
+v_FAN1 -| v_PCNATLS
+v_ADD -> v_PCNATLS
+v_USP1 -| v_PCNATLS
+#position:v_HRR:0,0
+$v_HRR:((v_DSB & ((v_BRCA1 & v_FANCD1N) & v_RAD51)) & !v_CHKREC)
+v_BRCA1 -> v_HRR
+v_FANCD1N -> v_HRR
+v_DSB -> v_HRR
+v_RAD51 -> v_HRR
+v_CHKREC -| v_HRR
+#position:v_ADD:0,0
+$v_ADD:((v_ADD & !v_PCNATLS) | ((v_MUS81 & (v_FAN1 | v_XPF)) & !v_PCNATLS))
+v_PCNATLS -| v_ADD
+v_MUS81 -> v_ADD
+v_FAN1 -> v_ADD
+v_ADD -> v_ADD
+v_XPF -> v_ADD
+#position:v_MRN:0,0
+$v_MRN:((v_DSB & v_ATM) & !((v_RAD51 | (v_KU & v_FANCD2I)) | v_CHKREC))
+v_ATM -> v_MRN
+v_DSB -> v_MRN
+v_KU -| v_MRN
+v_RAD51 -| v_MRN
+v_CHKREC -| v_MRN
+v_FANCD2I -? v_MRN
+#position:v_KU:0,0
+v_MRN -| v_KU
+v_DSB -> v_KU
+v_CHKREC -| v_KU
+v_FANCD2I -| v_KU
+#position:v_RAD51:0,0
+v_FANCD1N -> v_RAD51
+v_CHKREC -| v_RAD51
+v_ssDNARPA -> v_RAD51
+#position:v_FANCJBRCA1:0,0
+$v_FANCJBRCA1:((v_ssDNARPA & (v_ATM | v_ATR)) | (v_ICL & (v_ATM | v_ATR)))
+v_ATM -> v_FANCJBRCA1
+v_ICL -> v_FANCJBRCA1
+v_ATR -> v_FANCJBRCA1
+v_ssDNARPA -> v_FANCJBRCA1
+#position:v_FAcore:0,0
+$v_FAcore:((v_FANCM & (v_ATM | v_ATR)) & !v_CHKREC)
+v_ATM -> v_FAcore
+v_FANCM -> v_FAcore
+v_ATR -> v_FAcore
+v_CHKREC -| v_FAcore
+#position:v_H2AX:0,0
+$v_H2AX:((v_DSB & ((v_ATM | v_DNAPK) | v_ATR)) & !v_CHKREC)
+v_ATM -> v_H2AX
+v_DNAPK -> v_H2AX
+v_DSB -> v_H2AX
+v_ATR -> v_H2AX
+v_CHKREC -| v_H2AX
+#position:v_USP1:0,0
+$v_USP1:(((v_FANCD1N & v_FANCD2I) & !v_FANCM) | (v_PCNATLS & !v_FANCM))
+v_FANCM -| v_USP1
+v_FANCD1N -> v_USP1
+v_PCNATLS -> v_USP1
+v_FANCD2I -> v_USP1
+#position:v_DNAPK:0,0
+$v_DNAPK:((v_DSB & v_KU) & !v_CHKREC)
+v_DSB -> v_DNAPK
+v_KU -> v_DNAPK
+v_CHKREC -| v_DNAPK
+#position:v_FAN1:0,0
+$v_FAN1:(v_MUS81 & v_FANCD2I)
+v_MUS81 -> v_FAN1
+v_FANCD2I -> v_FAN1
+#position:v_XPF:0,0
+$v_XPF:(((v_p53 & v_MUS81) & !(v_FAcore & (v_FAN1 & v_FANCD2I))) | (v_MUS81 & !v_FANCM))
+v_FANCM -| v_XPF
+v_p53 -> v_XPF
+v_MUS81 -> v_XPF
+v_FAcore -| v_XPF
+v_FAN1 -? v_XPF
+v_FANCD2I -? v_XPF
+#position:v_FANCM:0,0
+$v_FANCM:(v_ICL & !v_CHKREC)
+v_ICL -> v_FANCM
+v_CHKREC -| v_FANCM
+#position:v_MUS81:0,0
+$v_MUS81:v_ICL
+v_ICL -> v_MUS81
+#position:v_p53:0,0
+$v_p53:((((v_ATM & v_CHK2) & !v_CHKREC) | ((v_ATR & v_CHK1) & !v_CHKREC)) | (v_DNAPK & !v_CHKREC))
+v_ATM -> v_p53
+v_CHK2 -> v_p53
+v_DNAPK -> v_p53
+v_ATR -> v_p53
+v_CHKREC -| v_p53
+v_CHK1 -> v_p53
+#position:v_CHK1:0,0
+$v_CHK1:(((v_ATM & !v_CHKREC) | (v_DNAPK & !v_CHKREC)) | (v_ATR & !v_CHKREC))
+v_ATM -> v_CHK1
+v_DNAPK -> v_CHK1
+v_ATR -> v_CHK1
+v_CHKREC -| v_CHK1