Bellow is the efforts for reducing the run time of modelchecker (After removing PKT DROP and REORDER options):
Normal case
depths 1, 2 in 0
depths 2, 14 in 0
depths 3, 54 in 0
depths 4, 153 in 0
depths 5, 394 in 1
depths 6, 939 in 2
depths 7, 2187 in 4
depths 8, 5074 in 11
depths 9, 11837 in 29
depths 10, 27630 in 74
depths 11, 64300 in 189
depths 12, 148919 in 472
directly start from depth 10
depths 10, 18155 in ???
depths 11, 50621 in 100
depths 12, 127010 in 357
removing ES_CONSEQUENCES
Here speed up is in the form of improving the effective depth at which we can find the bug. e.g. If a bug happens normally at depth 10 and we enable CONSIDER_ES_ACTION_CONSEQUENCES and this path to bug includes 5 events run my myNode, then the effective depths will be increased to 10+5=15 because we adds 5 branch points to modelchecker tree corresponding to ES specific actions in myNode. Here, the first bug which happened after depth 10 in normal case (74s) happens after depth 8 (28s)
depths 1, 2 in 0
depths 2, 17 in 1
depths 3, 77 in 1
depths 4, 231 in 1
depths 5, 626 in 2
depths 6, 1610 in 4
depths 7, 4149 in 10
depths 8, 10835 in 28
depths 9, 27935 in 77
depths 10, 71099 in 212
depths 11, 178306 in 579
pruning all the sch and app events after depth 1
That works perfect
depths 1, 2 in 0
depths 2, 12 in 0
depths 3, 39 in 0
depths 4, 96 in 1
depths 5, 195 in 1
depths 6, 338 in 1
depths 7, 519 in 1
depths 8, 739 in 2
depths 9, 1022 in 2
depths 10, 1430 in 3
depths 11, 2085 in 5
depths 12, 3204 in 9
removing timed entries from states
I was too violent and removed most of the entries. It is practically equal to the case where APP and SCH almost will not happen 2 times along the path.
depths 1, 2 in 0
depths 2, 14 in 0
depths 3, 50 in 0
depths 4, 125 in 0
depths 5, 273 in 0
depths 6, 525 in 0
depths 7, 938 in 1
depths 8, 1616 in 2
depths 9, 2706 in 5
depths 10, 4436 in 8
depths 11, 7018 in 14
depths 12, 10774 in 23
depths 13, 15982 in 37