PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:46:37 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm5304.smg -ex -pctl '<<1,2,3,4,5>> R{"common_value"}min=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm5304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5]>> R{"common_value"}min=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 130890 320583 530345 629457 743904 Reachable states exploration and model construction done in 13.982 secs. Sorting reachable states list... Time for model construction: 14.511 seconds. Type: SMG States: 743904 (1 initial) Transitions: 2145120 Choices: 1131744 Max/avg: 2/1.52 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5]>> R{"common_value"}min=? [ F time=max_time ] Building reward structure... Value in the initial state: 37.87180478993185 Time for model checking: 70.312 seconds. Result: 37.87180478993185 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:48:03 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm5304.smg -ex -pctl '<<1>> R{"value1"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm5304.smg"... 1 property: (1) <<[1]>> R{"value1"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 163591 355681 562929 652785 743904 Reachable states exploration and model construction done in 13.287 secs. Sorting reachable states list... Time for model construction: 13.97 seconds. Type: SMG States: 743904 (1 initial) Transitions: 2145120 Choices: 1131744 Max/avg: 2/1.52 ------------------------------------------- Model checking: <<[1]>> R{"value1"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 9.85303842753782 Time for model checking: 61.693 seconds. Result: 9.85303842753782 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:49:20 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm5304.smg -ex -pctl '<<1,2>> R{"value12"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm5304.smg"... 1 property: (1) <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 163591 354154 559307 648918 743904 Reachable states exploration and model construction done in 13.375 secs. Sorting reachable states list... Time for model construction: 14.061 seconds. Type: SMG States: 743904 (1 initial) Transitions: 2145120 Choices: 1131744 Max/avg: 2/1.52 ------------------------------------------- Model checking: <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 18.958427956039536 Time for model checking: 61.872 seconds. Result: 18.958427956039536 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:50:37 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm5304.smg -ex -pctl '<<1,2,3>> R{"value123"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm5304.smg"... 1 property: (1) <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 155842 342142 548113 640803 743904 Reachable states exploration and model construction done in 13.52 secs. Sorting reachable states list... Time for model construction: 14.202 seconds. Type: SMG States: 743904 (1 initial) Transitions: 2145120 Choices: 1131744 Max/avg: 2/1.52 ------------------------------------------- Model checking: <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 27.432356729420455 Time for model checking: 61.817 seconds. Result: 27.432356729420455 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:51:54 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm5304.smg -ex -pctl '<<1,2,3,4>> R{"value1234"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm5304.smg"... 1 property: (1) <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 159448 350729 561886 654577 743904 Reachable states exploration and model construction done in 13.267 secs. Sorting reachable states list... Time for model construction: 15.74 seconds. Type: SMG States: 743904 (1 initial) Transitions: 2145120 Choices: 1131744 Max/avg: 2/1.52 ------------------------------------------- Model checking: <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 35.423392728765364 Time for model checking: 65.323 seconds. Result: 35.423392728765364 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:53:16 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm5304.smg -ex -pctl '<<1,2,3,4,5>> R{"value12345"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm5304.smg"... 1 property: (1) <<[1, 2, 3, 4, 5]>> R{"value12345"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 162050 352583 560711 652144 743904 Reachable states exploration and model construction done in 13.296 secs. Sorting reachable states list... Time for model construction: 13.979 seconds. Type: SMG States: 743904 (1 initial) Transitions: 2145120 Choices: 1131744 Max/avg: 2/1.52 ------------------------------------------- Model checking: <<[1, 2, 3, 4, 5]>> R{"value12345"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 43.0870312409867 Time for model checking: 62.274 seconds. Result: 43.0870312409867 (value in the initial state)