PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:28:34 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2,3,4,5,6,7>> R{"common_value"}min=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5, 6, 7]>> R{"common_value"}min=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 94033 202784 285962 394252 508292 572449 677666 783093 889530 991102 1070372 1178951 1286561 1394270 1510341 1620602 1716052 1828288 1935228 2054532 2161577 2281553 2386802 2505841 2612214 2731002 2767595 2876804 2981531 3099049 3216100 3304369 3421150 3509122 3626971 3727488 3835732 3954396 4051125 4170633 4269129 4389458 4509045 4598590 4717192 4834113 4918321 5035685 5153192 5228635 5345203 5461044 5549882 5666257 5782110 5873085 5989565 6105399 6196721 6241312 Reachable states exploration and model construction done in 188.859 secs. Sorting reachable states list... Time for model construction: 210.698 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5, 6, 7]>> R{"common_value"}min=? [ F time=max_time ] Building reward structure... Value in the initial state: 38.1570984134083 Time for model checking: 870.041 seconds. Result: 38.1570984134083 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:46:37 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1>> R{"value1"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1]>> R{"value1"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 99219 206683 287680 395973 501699 564068 671087 785406 902871 1012812 1127763 1239937 1350567 1457730 1574328 1596094 1703419 1814941 1925986 2043987 2151652 2270109 2376011 2482090 2598806 2706954 2823798 2926986 3042925 3043527 3151184 3243281 3358572 3450985 3565679 3662508 3777885 3876062 3981304 4101059 4183048 4301048 4382632 4501476 4595948 4713296 4829338 4914938 5029947 5110165 5226640 5303443 5419062 5422918 5497410 5613106 5680845 5794272 5859476 5974396 6035842 6151166 6207749 6241312 Reachable states exploration and model construction done in 209.017 secs. Sorting reachable states list... Time for model construction: 234.483 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1]>> R{"value1"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 7.415178953621567 Time for model checking: 1028.355 seconds. Result: 7.415178953621567 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 18:07:42 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2>> R{"value12"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 86729 196280 300513 391843 497954 602499 676340 788499 897783 1016718 1049845 1170310 1276870 1396496 1501819 1620692 1729915 1852103 1933372 2043923 2163621 2264694 2382858 2487242 2605362 2708013 2816915 2934545 3031913 3149846 3266561 3364529 3480593 3575152 3686922 3802286 3898177 4016942 4135911 4213932 4324587 4442861 4529738 4649396 4765639 4880835 4998983 5114067 5220012 5335571 5451477 5553694 5669823 5785566 5871719 5988028 6094552 6215484 6241312 Reachable states exploration and model construction done in 189.423 secs. Sorting reachable states list... Time for model construction: 215.222 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 14.391087601221185 Time for model checking: 844.983 seconds. Result: 14.391087601221185 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 18:25:24 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2,3>> R{"value123"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 97946 205814 287402 395867 502827 564358 674085 789543 903143 1012864 1128506 1241768 1352955 1461721 1578726 1596760 1705375 1817510 1929668 2048536 2157152 2276224 2374872 2481729 2600001 2709042 2826863 2930538 3042924 3150335 3241906 3357905 3451059 3566344 3663555 3779745 3876148 3993721 4109907 4230905 4346414 4466377 4583779 4671408 4780894 4856297 4973458 5054489 5171661 5249233 5365424 5415708 5490453 5597538 5667637 5783794 5850446 5966199 6028963 6145497 6200558 6241312 Reachable states exploration and model construction done in 207.282 secs. Sorting reachable states list... Time for model construction: 232.32 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 20.979812052380733 Time for model checking: 1054.799 seconds. Result: 20.979812052380733 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 18:46:53 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2,3,4>> R{"value1234"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 99737 200945 279701 387274 502283 572529 679686 793639 903978 1012925 1127724 1239695 1336713 1449982 1555413 1606593 1716141 1827512 1939458 2048779 2146970 2265708 2371966 2489995 2595923 2704165 2821877 2881317 2990141 3084995 3202305 3298917 3414661 3512352 3627632 3723075 3839048 3945111 4064392 4184426 4284426 4402878 4503314 4620756 4714849 4832507 4949931 5032326 5149339 5249841 5365393 5481738 5555080 5670128 5710725 5783673 5900125 5964410 6079683 6141475 6241312 Reachable states exploration and model construction done in 196.137 secs. Sorting reachable states list... Time for model construction: 223.03 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 27.24664671573934 Time for model checking: 893.012 seconds. Result: 27.24664671573934 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 19:05:31 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2,3,4,5>> R{"value12345"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5]>> R{"value12345"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 82787 195624 277207 386838 495710 570618 677111 794025 904697 1025076 1123990 1237704 1350858 1461171 1579334 1609313 1720395 1831044 1944390 2063789 2168933 2287900 2394979 2503521 2623023 2731159 2850278 2898862 3008263 3100013 3213394 3307653 3423834 3522299 3638458 3743759 3852392 3971058 4068396 4188895 4289797 4409354 4510576 4629701 4748818 4841920 4959879 5051434 5169616 5285696 5362960 5481122 5563235 5670966 5745118 5812939 5929612 6012530 6130796 6217120 6241312 Reachable states exploration and model construction done in 193.296 secs. Sorting reachable states list... Time for model construction: 237.399 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5]>> R{"value12345"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 33.26338980501653 Time for model checking: 1083.119 seconds. Result: 33.26338980501653 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 19:27:34 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2,3,4,5,6>> R{"value123456"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5, 6]>> R{"value123456"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 94551 201435 303100 382648 490594 590544 676110 784818 892815 1008260 1047811 1157569 1262979 1379233 1481086 1595930 1698052 1819605 1895659 2007608 2125753 2225644 2342478 2446316 2565286 2666234 2784730 2901064 3005449 3122426 3220967 3336619 3451531 3485072 3591608 3706206 3788207 3905097 4022816 4118537 4238184 4355740 4447395 4561384 4674594 4746236 4854666 4970835 5034432 5151784 5265236 5344999 5458879 5574638 5652427 5768515 5882816 5963071 6078074 6160784 6241312 Reachable states exploration and model construction done in 193.979 secs. Sorting reachable states list... Time for model construction: 214.645 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5, 6]>> R{"value123456"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 39.10031607761575 Time for model checking: 1069.64 seconds. Result: 39.10031607761575 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 19:49:00 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm7304.smg -ex -pctl '<<1,2,3,4,5,6,7>> R{"value1234567"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm7304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5, 6, 7]>> R{"value1234567"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 83020 192165 292845 380745 490182 592343 676059 795385 904482 1022727 1055579 1174520 1281130 1399472 1502689 1619277 1726279 1846977 1909230 2021225 2141131 2240416 2357947 2459000 2577669 2678972 2796620 2913235 3016769 3133944 3242282 3349791 3465766 3555019 3671086 3784754 3880211 3996584 4116047 4209264 4327797 4444484 4459085 4568035 4685018 4762701 4876568 4992452 5077256 5194588 5308692 5397449 5513801 5629130 5710688 5821592 5936010 6011299 6127957 6227656 6241312 Reachable states exploration and model construction done in 192.846 secs. Sorting reachable states list... Time for model construction: 215.676 seconds. Type: SMG States: 6241312 (1 initial) Transitions: 19678246 Choices: 10132696 Max/avg: 2/1.62 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5, 6, 7]>> R{"value1234567"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 44.839866691827424 Time for model checking: 932.461 seconds. Result: 44.839866691827424 (value in the initial state)