Graded-CTL NuSMV

Test Results for "Table"

A≤k F (table[1]!=0 ∨ table[2]!=0 ∨ table[3]!=0)
k	Time	#BDD
-	0,008	17542
0	0,008	17542
1	0,008	19363
2	0,008	19481
3	0,008	19604
5	0,008	19827
8	0,008	20170
10	0,008	20400
15	0,012	20973
20	0,012	21530
50	0,020	24936

E>k1 F (table[1]=a ∧ E >k2 X (table[1]=b))
k1	k2	Time	#BDD
-	-	0,008	19275
0	0	0,008	19275
1	0	0,008	25442
2	0	0,012	25594
5	0	0,012	26665
10	0	0,012	27301
0	1	0,008	21149
1	1	0,008	21149
2	1	0,012	21149
5	1	0,012	21152
10	1	0,012	21157
0	2	0,008	21218
1	2	0,008	21218
2	2	0,012	21218
5	2	0,012	21221
10	2	0,012	21226
0	5	0,008	21695
1	5	0,008	21695
2	5	0,012	21695
5	5	0,012	21695
10	5	0,012	21700
0	10	0,008	21746
1	10	0,008	21746
2	10	0,012	21746
5	10	0,012	21746
10	10	0,012	21746
50	10	0,016	21786
50	50	0,016	21772