Tool Performance Data for Chiron DD Property p04

Property p04a
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
p04a 02 02 25.4 0.3 0.4 0.1
 
 0.0 0.3 0.0 0.1 2.8 0.9 0.3 0.4 0.4 0.0 0.1 1.7 0.9 32.2 3.2 0.1 0.3
p04a 02 03 26.2 0.3 0.6
 
 
 0.1 0.4 0.1 0.3 3.3 0.9 0.5 0.6 0.6 0.1 0.1 2.2 0.9 43.4 3.5 0.1 0.7
p04a 02 04 27.3 0.4 0.8
 
 
 0.1 0.5 0.1 0.3 4.4 1.1 0.7 0.9 1.0 0.1 0.2 2.5 1.1 57.1 3.9 0.2 1.4
p04a 02 05 28.4 0.5 0.9
 
 
 0.1 0.7 0.1 0.4 4.9 1.2 0.5 1.2 1.1 0.1 0.2 2.8 1.1 71.8 4.3 0.2 2.2
p04a 02 06 30.0 0.7 0.9
 
 
 0.1 0.4 0.1 0.5 5.4 1.3 0.6 1.5 1.4 0.1 0.2 3.2 1.3 88.8 4.7 0.4 3.3
p04a 02 07 30.6 1.4 1.0
 
 
 0.2 0.5 0.1 0.6 6.6 2.0 0.7 2.2 2.0 0.1 0.3 3.6 1.7 108.0 5.1 0.5 4.7
p04a 02 08 31.7 1.5 1.1
 
 
 0.2 0.5 0.1 0.6 7.2 2.3 0.9 2.8 2.3 0.1 0.3 4.0 1.9 127.8 5.5 0.6 6.2
p04a 02 09 32.7 1.6 1.4
 
 
 0.2 0.5 0.1 0.7 7.9 2.7 0.9 3.2 2.6 0.1 0.3 4.5 2.2 150.2 5.9 0.8 7.9
p04a 02 10 34.0 1.7 1.5
 
 
 0.3 0.6 0.1 0.8 9.3 5.0 1.0 5.0 3.6 0.1 0.3 4.9 3.7 177.2 6.3 1.0 9.9
p04a 02 11 35.2 1.7 1.6
 
 
 0.3 0.6 0.1 0.9 10.4 5.9 1.2 6.2 4.3 0.1 0.4 5.5 4.1 201.1 6.7 1.3 12.2
p04a 02 12 36.4 1.8 1.7
 
 
 0.3 0.7 0.1 1.0 10.7 6.9 1.2 7.4 5.2 0.1 0.4 5.7 4.7 225.5 7.1 1.5 14.6
p04a 02 13 37.8 2.0 2.1
 
 
 0.3 0.8 0.1 1.1 12.3 14.0 1.4 10.1 7.2 0.1 0.5 6.4 8.8 254.3 7.2 1.9 17.4
p04a 02 14 39.0 2.1 2.0
 
 
 0.4 0.8 0.1 1.2 13.3 16.2 1.5 11.7 7.9 0.1 0.5 6.9 10.5 287.4 8.0 2.2 20.1
p04a 02 15 40.2 2.1 2.1
 
 
 0.4 0.9 0.1 1.3 13.9 19.1 1.5 14.4 8.9 0.1 0.6 7.5 12.2 316.1 8.3 2.6 23.1
p04a 02 16 41.5 2.5 3.1
 
 
 0.4 0.9 0.1 1.5 17.1 40.9 1.7 20.9 10.8 0.1 0.6 7.9 24.6 352.3 8.6 3.1 26.5
p04a 02 17 43.1 2.7 2.7
 
 
 0.5 1.0 0.1 1.6 16.1 45.6 1.8 25.0 11.9 0.1 0.7 8.5 27.6 386.4 9.1 3.6 30.2
p04a 02 18 44.1 3.0 2.7
 
 
 0.5 1.0 0.1 1.7 17.0 54.3 1.9 29.2 13.2 0.1 0.7 9.0 30.5 424.1 9.3 4.1 34.0
p04a 02 19 45.8 3.1 3.6
 
 
 0.5 1.5 0.1 1.9 18.8 113.4 2.0 42.8 16.4 0.1 0.7 10.3 64.5 464.7 9.8 4.8 38.3
p04a 02 20 47.2 3.4 3.3
 
 
 0.6 1.1 0.1 2.0 20.1 129.5 2.0 53.1 18.0 0.1 0.8 10.7 71.4 513.2 10.1 5.4 42.5
p04a 02 21 48.4 3.7 3.2
 
 
 0.6 1.2 0.1 2.2 21.5 146.1 2.2 67.8 19.7 0.0 0.8 11.2 78.0 563.1 10.6 6.1 46.7
p04a 02 22 49.9 3.9 3.8
 
 
 0.7 1.5 0.1 2.4 23.9 316.5 2.3 129.7 24.1 0.1 0.9 11.8 167.6 607.4 10.9 7.0 51.7
p04a 02 23 51.6 4.1 4.3
 
 
 0.7 1.3 0.1 2.5 24.4 348.9 2.5 151.2 26.1 0.1 0.9 12.8 187.2 649.1 11.8 8.0 56.2
p04a 02 24 52.7 4.4 4.2
 
 
 0.7 1.3 0.1 2.6 25.8 394.3 2.5 197.5 28.7 0.1 1.0 14.7 196.6 692.5 12.1 8.8 61.6
p04a 02 25 54.6 4.9 4.5
 
 
 0.8 1.4 0.1 2.9 31.3 844.5 2.8 265.0 33.7 0.1 1.0 14.5 419.3 737.2 12.7 10.2 67.4
p04a 02 26 56.0 5.3 4.0
 
 
 0.9 1.4 0.1 3.0 29.7 909.7 2.8 359.0 36.5 0.1 1.1 16.2 485.5 786.8 13.4 11.2 72.8
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
p04a 02 27 57.7 5.6 4.9
 
 
 0.9 1.5 0.1 3.2 31.1 1008.4 3.0 337.2 39.6 0.1 1.1 15.6 500.9 839.1 13.7 12.4 78.4
p04a 02 28 59.0 6.0 4.6
 
 
 1.0 1.6 0.1 3.5 35.0 2194.9 3.0 425.4 44.7 0.1 1.2 16.8 1070.8 894.4 14.7 14.1 84.8
p04a 02 29 60.9 6.1 4.9
 
 
 1.0 1.6 0.1 3.6 35.2 2423.1 3.2 523.0 49.0 0.1 1.2 17.5 1153.4 952.6 14.6 15.4 91.7
p04a 02 30 62.2 6.6 5.2
 
 
 1.0 1.6 0.1 3.8 37.5 2665.8 3.3 564.2 51.6 0.1 1.3 18.1 1250.0 1026.8 15.4 16.8 97.1
p04a 02 31 64.1 7.0 6.0
 
 
 1.1 1.7 0.1 4.1 41.1 5926.2 3.4 713.7 58.1 0.1 1.4 19.6 2608.3 1102.4 15.6 18.8 104.8
p04a 02 32 65.6 7.4 5.2
 
 
 1.1 1.8 0.1 4.3 50.3 6709.6 3.5 813.8 62.5 0.1 1.4 20.8 2852.7 1170.0 16.4 20.3 112.7
p04a 02 33 67.1 7.8 5.4
 
 
 1.2 1.8 0.1 4.5 42.8 6763.5 3.9 932.6 71.2 0.1 1.5 24.7 3001.7 1232.4 16.6 22.1 119.3
p04a 02 34 69.0 8.3 6.1
 
 
 1.3 2.0 0.1 4.8 48.1 15220.1 4.5 1079.8 74.1 0.1 1.5 21.7 6681.3 1290.4 17.4 24.4 126.7
p04a 02 35 70.8 9.2 5.4
 
 
 1.3 2.0 0.1 4.9 48.7 16821.8 4.1 1073.2 78.5 0.1 1.6 23.5 7043.8 1352.3 18.8 26.6 134.4
p04a 02 36 72.5 9.3 6.5
 
 
 1.4 2.0 0.1 5.1 50.5 18404.8 4.1 1236.9 82.8 0.1 1.7 24.4 8050.7 1403.8 19.1 28.5 142.2
p04a 02 37 74.3 9.5 7.1
 
 
 1.5 2.2 0.1 5.5 53.0 38301.9 4.3 1377.6 92.1 0.1 1.7 33.4
 
 1469.8 20.6 31.3 150.6
p04a 02 38 76.2 9.9 7.0
 
 
 1.6 2.1 0.1 5.6 57.4 40434.3 4.6 1645.1 98.7
 
 
 
 
 1537.4 21.3 33.8 158.1
p04a 02 39 78.0 10.6 7.3
 
 
 1.6 2.2 0.1 5.9 71.8 43363.6 4.4 1814.7 104.1
 
 
 
 
 1617.5 19.8 36.1 168.3
p04a 02 40 79.9 11.8 7.9
 
 
 1.7 2.3 0.1 6.3 61.0
 
 4.6 2184.6 115.5
 
 
 
 
 1708.0 20.1 39.6 176.4
p04a 02 41 81.6 11.8 7.5
 
 
 1.7
 
 
 
 
 
 5.0 2290.0 121.1
 
 
 
 
 1810.2 20.8 42.0 186.1
p04a 02 42 83.8 12.8 7.5
 
 
 1.7
 
 
 
 
 
 5.3 2504.9 128.6
 
 
 
 
 1904.0 21.7 44.9 194.7
p04a 02 43 85.6 13.2 7.3
 
 
 1.9
 
 
 
 
 
 5.1 2825.8 142.5
 
 
 
 
 1986.8 22.3 49.2 204.6
p04a 02 44 87.5 14.4 8.2
 
 
 1.9
 
 
 
 
 
 5.2 2793.6 148.5
 
 
 
 
 2064.1 22.9 52.2 214.9
p04a 02 45 89.6 14.8 8.4
 
 
 2.0
 
 
 
 
 
 5.4 3076.5 157.5
 
 
 
 
 2155.6 23.1 55.4 225.2
p04a 02 46 91.6 16.6 7.9
 
 
 2.1
 
 
 
 
 
 5.5 3656.1 171.3
 
 
 
 
 2229.6 24.0 59.6 239.7
p04a 02 47 93.7 17.5 7.9
 
 
 2.1
 
 
 
 
 
 6.6 4075.9 181.7
 
 
 
 
 2309.1 24.2 63.1 250.7
p04a 02 48 95.5 17.8 9.8
 
 
 2.2
 
 
 
 
 
 5.9 4556.2 191.9
 
 
 
 
 2375.6 24.9 68.0 255.6
p04a 02 49 97.6 18.1 9.3
 
 
 2.3
 
 
 
 
 
 5.9 5581.1 208.0
 
 
 
 
 2466.6 25.6 72.0 270.0
p04a 02 50 99.8 19.7 8.6
 
 
 2.4
 
 
 
 
 
 6.7 6853.1 221.8
 
 
 
 
 2578.4 26.2 77.0 279.8
p04a 02 51 101.7 20.6 8.8
 
 
 2.4
 
 
 
 
 
 6.3 7692.1 231.3
 
 
 
 
 2700.2 27.0 80.4 293.2
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
p04a 02 52 104.0 20.7 8.7
 
 
 2.6
 
 
 
 
 
 6.5 8961.8 252.0
 
 
 
 
 2823.1 27.4 85.2 305.1
p04a 02 53 105.8 23.0 9.9
 
 
 2.7
 
 
 
 
 
 6.7 9604.3 264.2
 
 
 
 
 2931.1 27.1 89.9 317.9
p04a 02 54 107.9 22.1 9.3
 
 
 2.7
 
 
 
 
 
 7.7 10427.5 276.1
 
 
 
 
 error
 
 
 
p04a 02 55 110.5 23.8 11.2
 
 
 2.8
 
 
 
 
 
 7.7 12104.2 301.7
 
 
 
 
 
 
 
 
p04a 02 56 112.7 23.8 11.7
 
 
 2.9
 
 
 
 
 
 7.6 11488.4 318.2
 
 
 
 
 
 
 
 
p04a 02 57 114.8 24.6 11.0
 
 
 2.9
 
 
 
 
 
 7.1 13168.9 332.1
 
 
 
 
 
 
 
 
p04a 02 58 117.1 25.3 10.7
 
 
 3.1
 
 
 
 
 
 7.5 14169.5 364.9
 
 
 
 
 
 
 
 
p04a 02 59 119.3 26.9 11.3
 
 
 3.1
 
 
 
 
 
 7.9 15051.3 382.3
 
 
 
 
 
 
 
 
p04a 02 60 121.5 28.4 12.6
 
 
 3.2
 
 
 
 
 
 8.1 16050.9 393.2
 
 
 
 
 error
 
 
 
p04a 02 61 123.8 30.1 12.3
 
 
 3.4
 
 
 
 
 
 9.1
 
 420.8
 
 
 
 
 
 
 
 
p04a 02 62 126.3 28.9 11.9
 
 
 3.4
 
 
 
 
 
 8.1
 
 446.3
 
 
 
 
 
 
 
 
p04a 02 63 128.6 31.7 12.4
 
 
 3.5
 
 
 
 
 
 8.2
 
 461.3
 
 
 
 
 
 
 
 
p04a 02 64 131.1 31.9 14.7
 
 
 3.7
 
 
 
 
 
 8.3
 
 502.1
 
 
 
 
 
 
 
 
p04a 02 65 133.4 33.4 14.6
 
 
 3.7
 
 
 
 
 
 8.4
 
 518.7
 
 
 
 
 
 
 
 
p04a 02 66 135.5 34.9 14.4
 
 
 3.8
 
 
 
 
 
 8.7
 
 540.2
 
 
 
 
 
 
 
 
p04a 02 67 138.2 36.3 15.4
 
 
 4.0
 
 
 
 
 
 9.0
 
 574.2
 
 
 
 
 
 
 
 
p04a 02 68 141.0 37.5 15.2
 
 
 4.2
 
 
 
 
 
 9.1
 
 599.5
 
 
 
 
 
 
 
 
p04a 02 69 143.1 38.5 15.9
 
 
 4.1
 
 
 
 
 
 9.2
 
 630.6
 
 
 
 
 
 
 
 
p04a 02 70 145.7 39.5 14.3
 
 
 4.3
 
 
 
 
 
 9.7
 
 674.7
 
 
 
 
 
 
 
 
p04a 02 71 148.9 40.1 16.0
 
 
 4.4
 
 
 
 
 
 9.7
 
 695.7
 
 
 
 
 
 
 
 
p04a 02 72 151.5 41.8 15.5
 
 
 4.4
 
 
 
 
 
 9.8
 
 726.4
 
 
 
 
 
 
 
 
p04a 02 73 155.0 44.2 13.9
 
 
 4.7
 
 
 
 
 
 10.2
 
 771.9
 
 
 
 
 
 
 
 
p04a 02 74 158.1 46.8 16.4
 
 
 4.8
 
 
 
 
 
 10.4
 
 805.3
 
 
 
 
 
 
 
 
p04a 02 75 161.6 47.9 16.6
 
 
 4.9
 
 
 
 
 
 10.4
 
 829.5
 
 
 
 
 
 
 
 
p04a 02 76 163.7 53.7 18.3
 
 
 5.0
 
 
 
 
 
 11.6
 
 889.9
 
 
 
 
 
 
 
 
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
p04a 02 77 166.2 52.0 17.3
 
 
 5.2
 
 
 
 
 
 10.9
 
 924.2
 
 
 
 
 
 
 
 
p04a 02 78 168.7 52.8 17.7
 
 
 5.2
 
 
 
 
 
 11.2
 
 954.9
 
 
 
 
 
 
 
 
p04a 02 79 171.3 54.7 17.0
 
 
 5.4
 
 
 
 
 
 11.2
 
 1019.9
 
 
 
 
 
 
 
 
p04a 02 80 175.5 61.5 19.0
 
 
 5.5
 
 
 
 
 
 11.7
 
 1052.5
 
 
 
 
 
 
 
 
p04a 02 81 178.2 56.6 19.1
 
 
 5.6
 
 
 
 
 
 12.4
 
 1122.2
 
 
 
 
 
 
 
 
p04a 02 82 180.3 60.1 16.7
 
 
 5.8
 
 
 
 
 
 12.0
 
 1171.9
 
 
 
 
 
 
 
 
p04a 02 83 183.2 60.2 22.1
 
 
 5.8
 
 
 
 
 
 12.0
 
 1211.2
 
 
 
 
 
 
 
 
p04a 02 84 185.3 62.2 19.5
 
 
 6.0
 
 
 
 
 
 12.8
 
 1255.8
 
 
 
 
 
 
 
 
p04a 02 85 187.5 62.9 20.3
 
 
 6.2
 
 
 
 
 
 12.6
 
 1322.6
 
 
 
 
 
 
 
 
p04a 02 86 190.5 68.2 19.5
 
 
 6.2
 
 
 
 
 
 12.6
 
 1357.4
 
 
 
 
 
 
 
 
p04a 02 87 194.0 73.3 21.7
 
 
 6.3
 
 
 
 
 
 12.7
 
 1438.3
 
 
 
 
 
 
 
 
p04a 02 88 196.8 71.7 22.2
 
 
 6.5
 
 
 
 
 
 13.4
 
 1497.8
 
 
 
 
 
 
 
 
p04a 02 89 199.1 77.8 18.0
 
 
 6.7
 
 
 
 
 
 13.3
 
 1540.2
 
 
 
 
 
 
 
 
p04a 02 90 201.9 77.0 20.6
 
 
 6.7
 
 
 
 
 
 14.4
 
 1593.7
 
 
 
 
 
 
 
 
p04a 02 91 206.6 81.5 18.4
 
 
 7.0
 
 
 
 
 
 13.7
 
 1673.4
 
 
 
 
 
 
 
 
p04a 02 92 209.4 81.3 18.5
 
 
 7.0
 
 
 
 
 
 13.9
 
 1836.9
 
 
 
 
 
 
 
 
p04a 02 93 212.3 85.8 18.9
 
 
 7.1
 
 
 
 
 
 13.9
 
 1886.2
 
 
 
 
 
 
 
 
p04a 02 94 216.7 85.4 21.0
 
 
 7.4
 
 
 
 
 
 14.7
 
 1974.1
 
 
 
 
 
 
 
 
p04a 02 95 217.7 86.0 21.6
 
 
 7.6
 
 
 
 
 
 14.7
 
 2091.0
 
 
 
 
 
 
 
 
p04a 02 96 223.4 88.9 23.7
 
 
 7.6
 
 
 
 
 
 15.0
 
 2106.5
 
 
 
 
 
 
 
 
p04a 02 97 226.7 93.5 21.0
 
 
 7.8
 
 
 
 
 
 15.0
 
 2166.9
 
 
 
 
 
 
 
 
p04a 02 98 227.7 98.2 20.8
 
 
 8.0
 
 
 
 
 
 15.1
 
 2242.9
 
 
 
 
 
 
 
 
p04a 02 99 231.3 97.7 23.4
 
 
 8.0
 
 
 
 
 
 15.6
 
 2294.9
 
 
 
 
 
 
 
 
p04a 03 02 26.3 1.0 0.9
 
 
 0.2 0.5 0.0 0.6 6.1 1.1 0.8 1.3 1.5 0.1 0.1 2.0 1.1 72.8 4.2 0.2 1.5
p04a 04 02 26.8 4.8 6.6
 
 
 0.6 1.5 0.0 9.6 28.3 2.4 2.8 7.2 6.2 0.1 0.1 2.1 2.1 219.1 6.1 0.4 5.9
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
p04a 05 02 27.4 33.3 127.2
 
 
 7.8 9.5 0.0 342.8
 
 
 19.4 221.5 161.7 0.1 0.2 2.3 19.8 808.7 10.3 0.9 19.7
p04a 06 02 28.0 2042.3 6998.4
 
 
 260.8 61.4 0.0 error
 
 
 339.4 7267.8 7931.0 0.1 0.2 2.4 142.7 3007.9 18.6 2.2 53.2
p04a 07 02 27.9 14298.0
 
 
 
 
 
 
 
 
 
 16801.8
 
 
 0.1 0.2 2.6 4194.4 error