PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:44:52 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm4304.smg -ex -pctl '<<1,2,3,4>> R{"common_value"}min=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm4304.smg"... 1 property: (1) <<[1, 2, 3, 4]>> R{"common_value"}min=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 178272 Reachable states exploration and model construction done in 2.444 secs. Sorting reachable states list... Time for model construction: 2.648 seconds. Type: SMG States: 178272 (1 initial) Transitions: 473088 Choices: 256416 Max/avg: 2/1.44 ------------------------------------------- Model checking: <<[1, 2, 3, 4]>> R{"common_value"}min=? [ F time=max_time ] Building reward structure... Value in the initial state: 37.576177457913126 Time for model checking: 16.067 seconds. Result: 37.576177457913126 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:45:11 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm4304.smg -ex -pctl '<<1>> R{"value1"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm4304.smg"... 1 property: (1) <<[1]>> R{"value1"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 178272 Reachable states exploration and model construction done in 2.521 secs. Sorting reachable states list... Time for model construction: 2.721 seconds. Type: SMG States: 178272 (1 initial) Transitions: 473088 Choices: 256416 Max/avg: 2/1.44 ------------------------------------------- Model checking: <<[1]>> R{"value1"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 11.785865194548677 Time for model checking: 17.517 seconds. Result: 11.785865194548677 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:45:32 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm4304.smg -ex -pctl '<<1,2>> R{"value12"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm4304.smg"... 1 property: (1) <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 178272 Reachable states exploration and model construction done in 2.487 secs. Sorting reachable states list... Time for model construction: 2.686 seconds. Type: SMG States: 178272 (1 initial) Transitions: 473088 Choices: 256416 Max/avg: 2/1.44 ------------------------------------------- Model checking: <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 22.516567954673143 Time for model checking: 17.751 seconds. Result: 22.516567954673143 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:45:53 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm4304.smg -ex -pctl '<<1,2,3>> R{"value123"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm4304.smg"... 1 property: (1) <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 178272 Reachable states exploration and model construction done in 2.621 secs. Sorting reachable states list... Time for model construction: 2.818 seconds. Type: SMG States: 178272 (1 initial) Transitions: 473088 Choices: 256416 Max/avg: 2/1.44 ------------------------------------------- Model checking: <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 32.379256568730185 Time for model checking: 19.579 seconds. Result: 32.379256568730185 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Sun Sep 11 16:46:17 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm4304.smg -ex -pctl '<<1,2,3,4>> R{"value1234"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm4304.smg"... 1 property: (1) <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 178272 Reachable states exploration and model construction done in 2.515 secs. Sorting reachable states list... Time for model construction: 2.713 seconds. Type: SMG States: 178272 (1 initial) Transitions: 473088 Choices: 256416 Max/avg: 2/1.44 ------------------------------------------- Model checking: <<[1, 2, 3, 4]>> R{"value1234"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 41.60726370397802 Time for model checking: 17.241 seconds. Result: 41.60726370397802 (value in the initial state)