D:\mh\examples\bio_pn\levchenko>bddctl levchenko_n1.apnn levchenko.ctl
DSSZCTL Version 2.2
Checking the net: "levchenko_n1.apnn"
(NrP 22 NrT 30 NrMP 7)

Start reachability set computation:
.....
iterations count:5

-> reachability set: #nodes 25 #states 118
RS computation time: 0m0.00 sec

Start checking formula 1:
!EF (Raf * RafP);
.
-> the formula 1 is TRUE
MC time: 0m0.00 sec

Start checking formula 2:
!EF (MEK * MEKP * MEKPP);
.
-> the formula 2 is TRUE
MC time: 0m0.00 sec

Start checking formula 3:
!EF (ERK * ERKP * ERKPP);
.
-> the formula 3 is TRUE
MC time: 0m0.00 sec

Start checking formula 4:
EF ((RafP) * (MEKP + MEKPP));
.....
-> the formula 4 is TRUE
MC time: 0m0.00 sec

Start checking formula 5:
EF ((RafP) * (ERKP + ERKPP));
.........
-> the formula 5 is TRUE
MC time: 0m0.00 sec

Start checking formula 6:
EF ((MEKP + MEKPP) * (ERKP + ERKPP));
.........
-> the formula 6 is TRUE
MC time: 0m0.10 sec

Start checking formula 7:
EF ((RafP) * (MEKP + MEKPP) * (ERKP + ERKPP));
.........
-> the formula 7 is TRUE
MC time: 0m0.00 sec

Start checking formula 8:
!AF (RafP);
..
-> the formula 8 is TRUE
MC time: 0m0.00 sec

Start checking formula 9:
!AF (MEKPP);
.
-> the formula 9 is TRUE
MC time: 0m0.00 sec

Start checking formula 10:
!AF (ERKPP);
.
-> the formula 10 is TRUE
MC time: 0m0.00 sec

Start checking formula 11:
!((Raf * MEK * ERK) -> E [!(RafP) U MEKP]);
....
-> the formula 11 is TRUE
MC time: 0m0.00 sec

Start checking formula 12:
!((Raf * MEK * ERK) -> E [!(MEKP) U MEKPP]);
..
-> the formula 12 is TRUE
MC time: 0m0.00 sec

Start checking formula 13:
!((Raf * MEK * ERK) -> E [!(MEKPP) U ERKP]);
...
-> the formula 13 is TRUE
MC time: 0m0.00 sec

Start checking formula 14:
!((Raf * MEK * ERK) -> E [!(ERKP) U ERKPP]);
..
-> the formula 14 is TRUE
MC time: 0m0.00 sec

Start checking formula 15:
!(E [!RafP U MEKP] + E [!MEKP U MEKPP] + E [!MEKPP U ERKP] + E [!ERKP U ERKPP]);
...........
-> the formula 15 is TRUE
MC time: 0m0.10 sec

Start checking formula 16:
!(E [!RafP U MEKP] * E [!MEKP U MEKPP] * E [!MEKPP U ERKP] * E [!ERKP U ERKPP]);
...........
-> the formula 16 is TRUE
MC time: 0m0.00 sec

Start checking formula 17:
EF (Raf * (ERKP + ERKPP)) * EF (RafP * (ERKP + ERKPP)) * EF (MEK * (ERKP + ERKPP)) * EF ((MEKP + MEKPP) * (ERKP + ERKPP));
..........................................
-> the formula 17 is TRUE
MC time: 0m0.10 sec

Start checking formula 18:
AG ((RafP -> EF (!RafP)) * (!RafP -> EF (RafP)));
......
-> the formula 18 is TRUE
MC time: 0m0.00 sec

Start checking formula 19:
AG ((MEK -> EF (!MEK)) * (!MEK -> EF (MEK)));
...........
-> the formula 19 is TRUE
MC time: 0m0.00 sec

Start checking formula 20:
AG ((ERK -> EF (!ERK)) * (!ERK -> EF (ERK)));
..............
-> the formula 20 is TRUE
MC time: 0m0.00 sec

Start checking formula 21:
AG ((MEKPP -> EF (!MEKPP)) * (!MEKPP -> EF (MEKPP)));
..........
-> the formula 21 is TRUE
MC time: 0m0.00 sec

Total MC time: 0m0.30 sec

Total time: 0m0.100 sec

ZBDD statistic:
overall number of nodes: 4291
number of nodes in nodes-array: 4291
number of garbage collections: 0
fireUnion cache hits/miss/sum: 8569 10502 19071
binOp cache hits/miss/sum: 7786 8632 16418
state number cache hits/miss/sum: 14 25 39

D:\mh\examples\bio_pn\levchenko>