PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:54:34 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.smg -ex -pctl '<<1,2,3,4,5,6>> R{"common_value"}min=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm6304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5, 6]>> R{"common_value"}min=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 115490 261041 419537 567011 655595 808680 962105 1037913 1189680 1326719 1489091 1640775 1803332 1856228 2007628 2144176 2305943 2384369 Reachable states exploration and model construction done in 53.705 secs. Sorting reachable states list... Time for model construction: 61.865 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5, 6]>> R{"common_value"}min=? [ F time=max_time ] Building reward structure... Value in the initial state: 37.919655553067045 Time for model checking: 274.285 seconds. Result: 37.919655553067045 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:00:12 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.smg -ex -pctl '<<1>> R{"value1"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm6304.smg"... 1 property: (1) <<[1]>> R{"value1"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 135979 285468 446736 595023 677509 822198 989269 1059869 1211611 1353941 1516435 1664646 1822428 1973630 2116373 2277988 2384369 Reachable states exploration and model construction done in 52.829 secs. Sorting reachable states list... Time for model construction: 54.753 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1]>> R{"value1"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 8.462101209118808 Time for model checking: 218.098 seconds. Result: 8.462101209118808 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:04:46 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.smg -ex -pctl '<<1,2>> R{"value12"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm6304.smg"... 1 property: (1) <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 131700 277879 438502 583773 664739 814458 968963 1037648 1188378 1331330 1491563 1638123 1801822 1818759 1968482 2108174 2267816 2384369 Reachable states exploration and model construction done in 53.635 secs. Sorting reachable states list... Time for model construction: 55.627 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 16.372495094522055 Time for model checking: 218.817 seconds. Result: 16.372495094522055 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:09:22 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.smg -ex -pctl '<<1,2,3>> R{"value123"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm6304.smg"... 1 property: (1) <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 132414 281815 443337 589935 672035 820628 977824 1048638 1200248 1343264 1504009 1652521 1817718 1823227 1974081 2115722 2277191 2384369 Reachable states exploration and model construction done in 53.099 secs. Sorting reachable states list... Time for model construction: 55.023 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 23.80812372337286 Time for model checking: 221.689 seconds. Result: 23.80812372337286 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:14:00 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.smg -ex -pctl '<<1,2,3,4>> R{"value1234"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm6304.smg"... 1 property: (1) <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 118172 262132 426081 574663 669866 819861 978747 1037805 1191539 1336713 1499932 1649655 1816421 1823511 1962352 2105294 2267433 2384369 Reachable states exploration and model construction done in 53.365 secs. Sorting reachable states list... Time for model construction: 55.246 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 30.869746213267668 Time for model checking: 233.673 seconds. Result: 30.869746213267668 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:18:51 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.smg -ex -pctl '<<1,2,3,4,5>> R{"value12345"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm6304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5]>> R{"value12345"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 127461 261426 423870 571570 652886 806119 959655 1037629 1188985 1330640 1492382 1639484 1792801 1825731 1976974 2119728 2281546 2384369 Reachable states exploration and model construction done in 53.933 secs. Sorting reachable states list... Time for model construction: 56.139 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5]>> R{"value12345"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 37.65792484641405 Time for model checking: 237.405 seconds. Result: 37.65792484641405 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 17:23:46 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm6304.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/dsm6304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5, 6]>> R{"value123456"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 132690 284691 447886 598982 694656 837036 1006755 1055035 1219631 1364549 1529940 1680699 1831643 1985753 2127132 2291366 2384369 Reachable states exploration and model construction done in 52.559 secs. Sorting reachable states list... Time for model construction: 59.466 seconds. Type: SMG States: 2384369 (1 initial) Transitions: 7260756 Choices: 3772529 Max/avg: 2/1.58 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5, 6]>> R{"value123456"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 44.288449311490766 Time for model checking: 227.053 seconds. Result: 44.288449311490766 (value in the initial state)