Graded-CTL NuSMV

Test Results for "Dekker"

A≤k G !((pr1.state=critical) ∧ (pr2.state=critical))
k	Time	#BDD
-	0,000	2169
0	0,000	2169
1	0,000	2339
2	0,000	2340
3	0,000	2341
5	0,000	2343
8	0,000	2346
10	0,000	2348
15	0,000	2353
20	0,000	2358
50	0,000	2388

A≤k1 G ((pr1.state=test_bj) ⇒ (A ≤k2 F (pr1.state=critical))
k1	k2	Time	#BDD
-	-	0,004	3940
0	0	0,004	3940
1	0	0,004	4110
2	0	0,004	4111
5	0	0,004	4114
10	0	0,004	4119
0	1	0,004	4110
1	1	0,004	4110
2	1	0,004	4111
5	1	0,004	4114
10	1	0,004	4119
0	2	0,004	4111
1	2	0,004	4111
2	2	0,004	4111
5	2	0,004	4114
10	2	0,004	4119
0	5	0,004	4114
1	5	0,004	4114
2	5	0,004	4114
5	5	0,004	4114
10	5	0,004	4119
0	10	0,004	4119
1	10	0,004	4119
2	10	0,004	4119
5	10	0,004	4119
10	10	0,004	4119
50	10	0,008	4159
50	50	0,008	4159