Tool Performance Data for Chiron OD Property p08

Property p08a
Problem INCA INCA-Spin INCA-SMV NuSMV Native Spin FLAVERS
Property Artists Events a2s Derive analyze flo cyc Cplex Prom Never Spin Cc Pan Trans SMV NuSMV Never Spin Cc Pan LP Java MHP SP
p08a 02 02 24.7 0.4 0.1 0.1
 
 
 0.1 0.0 0.1 1.7 0.8 0.3 0.2 0.3
 
 0.0 1.5 0.8 25.9 3.4 0.1 0.2
p08a 02 03 25.3 1.1 0.3
 
 
 
 0.3 0.1 0.3 2.3 0.9 0.7 0.6 0.9
 
 0.1 1.8 0.9 33.0 3.7 0.1 0.4
p08a 02 04 26.2 7.7 1.0
 
 
 
 1.9 0.1 8.3 9.5 1.0 4.1 12.6 12.5
 
 0.2 2.0 0.9 41.1 4.2 0.1 0.6
p08a 02 05 26.8 19.4 4.1
 
 
 
 4.3 0.0 40.4 23.5 1.0 9.7 48.9 66.0
 
 0.2 2.2 0.9 50.3 4.3 0.1 0.9
p08a 02 06 27.6 49.2 22.6
 
 
 
 10.0 0.1 202.3 98.4 1.2 22.6 233.1 341.6
 
 0.2 2.4 0.9 59.5 4.6 0.2 1.1
p08a 02 07 28.5 470.4 567.0
 
 
 
 67.5 0.1 error
 
 
 
 
 
 
 0.2 2.7 1.0 69.9 4.9 0.2 1.6
p08a 02 08 29.4 2513.3 3259.1
 
 
 
 
 
 
 
 
 
 
 
 
 0.3 2.8 1.0 81.3 5.2 0.3 1.9
p08a 02 09
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.3 3.1 1.1 95.2 5.5 0.3 2.3
p08a 02 10
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.4 3.3 1.3 106.3 5.8 0.4 2.9
p08a 02 11
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.4 3.7 1.4 119.9 6.2 0.5 3.4
p08a 02 12
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.5 4.0 1.5 134.6 6.4 0.6 3.9
p08a 02 13
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.5 4.1 2.0 150.0 6.8 0.7 4.5
p08a 02 14
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.6 4.4 2.1 166.6 7.1 0.8 5.1
p08a 02 15
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.6 4.7 2.3 183.2 7.3 0.8 5.9
p08a 02 16
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.7 5.0 3.9 200.2 7.8 1.0 6.7
p08a 02 17
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.7 5.4 4.1 222.6 8.0 1.1 7.4
p08a 02 18
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.8 5.7 4.4 248.8 8.2 1.3 8.1
p08a 02 19
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.8 6.1 8.3 265.6 8.4 1.5 9.2
p08a 02 20
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.9 6.4 9.0 283.8 8.8 1.6 10.0
p08a 02 21
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.0 6.9 9.7 304.5 9.3 1.8 11.4
p08a 02 22
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.1 7.1 19.2 327.6 9.8 2.0 12.2
p08a 02 23
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.1 7.5 20.4 352.3 9.9 2.2 13.1
p08a 02 24
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.2 7.9 23.7 376.6 10.4 2.5 14.2
p08a 02 25
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.3 8.3 44.6 401.2 10.5 2.8 15.4
p08a 02 26
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.4 8.8 49.7 438.9 11.1 3.0 16.4
Problem INCA INCA-Spin INCA-SMV NuSMV Native Spin FLAVERS
Property Artists Events a2s Derive analyze flo cyc Cplex Prom Never Spin Cc Pan Trans SMV NuSMV Never Spin Cc Pan LP Java MHP SP
p08a 02 27
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.5 9.2 53.5 471.9 11.3 3.3 17.5
p08a 02 28
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.6 9.7 106.1 500.5 11.6 3.6 19.1
p08a 02 29
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.7 10.2 112.2 523.5 12.4 4.0 20.3
p08a 02 30
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.8 11.0 122.8 548.4 12.4 4.2 21.6
p08a 02 31
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.8 10.8 251.2 575.7 12.7 4.6 23.3
p08a 02 32
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1.9 12.3 272.4 605.1 12.9 5.0 24.6
p08a 02 33
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.0 11.8 284.9 639.6 13.2 5.5 25.8
p08a 02 34
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.2 12.9 586.5 679.2 13.5 6.0 27.6
p08a 02 35
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.3 13.3 635.8 735.6 13.7 6.4 29.1
p08a 02 36
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.4 13.8 676.1 777.5 14.1 6.7 30.6
p08a 02 37
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.5 14.8 1373.1 816.6 15.2 7.3 32.9
p08a 02 38
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.6 15.3 1443.5 844.1 15.3 8.0 34.0
p08a 02 39
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.8 14.8 1574.7 877.5 15.6 8.5 35.7
p08a 02 40
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 2.9 16.1 3278.5 903.1 15.9 9.2 38.5
p08a 02 41
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 3.0 16.4 3599.8 937.2 16.4 9.7 40.0
p08a 02 42
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 3.1 17.4 3868.9 976.6 16.9 10.2 41.0
p08a 02 43
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 3.3 17.8
 
 1039.5 17.1 11.1 43.4
p08a 02 44
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 3.4 20.9
 
 1103.7 17.4 11.8 45.7
p08a 02 45
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1155.2 17.9 12.6 47.6
p08a 02 46
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1203.3 19.0 13.6 49.8
p08a 02 47
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1246.2 19.1 14.4 51.6
p08a 02 48
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1284.0 19.7 15.3 53.9
p08a 02 49
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1319.6 19.9 16.4 56.4
p08a 02 50
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1357.2 20.0 16.7 58.2
p08a 02 51
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1410.0 21.2 18.0 60.3
Problem INCA INCA-Spin INCA-SMV NuSMV Native Spin FLAVERS
Property Artists Events a2s Derive analyze flo cyc Cplex Prom Never Spin Cc Pan Trans SMV NuSMV Never Spin Cc Pan LP Java MHP SP
p08a 02 52
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1497.9 21.2 19.1 63.4
p08a 02 53
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1559.4 21.3 20.0 66.3
p08a 02 54
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 error error
 
 
p08a 02 55
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 error error
 
 
p08a 02 60
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 error error
 
 
p08a 03 02 25.6 5.4 1.0
 
 
 
 1.2 0.0 3.9 6.1 0.9 2.5 6.3 6.2
 
 0.1 1.7 0.9 62.6 5.4 0.2 7.7
p08a 04 02 26.1 30.5 9.8
 
 
 
 5.4 0.0 79.0 40.3 1.6 11.0 141.6 181.7
 
 0.1 1.9 1.2 202.8 9.8 0.8 297.8
p08a 05 02 26.9 9126.4 4304.2
 
 
 
 113.8 0.0 0.7
 
 
 254.9
 
 
 
 0.1 2.0 6.5 770.5 19.9 3.2
 
p08a 06 02 27.2
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.1 2.1 43.4 3054.4 40.6 12.2
 
p08a 07 02
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.2 2.3 1315.0 error
 
 
 
p08a 08 02
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 0.2 2.6