Graded-CTL NuSMV

Test Results for "Robot"

A≤k1 G (pT1.start ⇒ A≤k2 G !pT1.finish)
k1	k2	Time	#BDD
-	-	0,072	59240
0	0	0,072	59449
1	0	0,116	113878
2	0	0,116	114968
5	0	0,128	116059
10	0	0,156	122762
0	1	0,116	114476
1	1	0,116	114476
2	1	0,144	121194
5	1	0,154	122285
10	1	0,176	128988
0	2	0,124	115566
1	2	0,128	121194
2	2	0,128	115560
5	2	0,168	122285
10	2	0,188	128988
0	5	0,132	116657
1	5	0,156	122285
2	5	0,156	122285
5	5	0,156	116657
10	5	0,196	123360
0	10	0,164	123360
1	10	0,176	128988
2	10	0,192	128988
5	10	0,200	123360
10	10	0,192	123360
50	10	0,448	176984
50	50	0,532	170281