PRISM ===== Version: 4.0.1.games Date: Tue Sep 13 19:53:46 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm3324p.smg -ex -pctl '<<1>> R{"value1"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm3324p.smg"... 1 property: (1) <<[1]>> R{"value1"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 33528 Reachable states exploration and model construction done in 0.998 secs. Sorting reachable states list... Time for model construction: 1.062 seconds. Type: SMG States: 33528 (1 initial) Transitions: 107422 Choices: 48922 Max/avg: 4/1.46 ------------------------------------------- Model checking: <<[1]>> R{"value1"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 10.772976387725066 Time for model checking: 3.0 seconds. Result: 10.772976387725066 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Tue Sep 13 19:53:50 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm3314p.smg -ex -pctl '<<1,2>> R{"value12"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm3314p.smg"... 1 property: (1) <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 33528 Reachable states exploration and model construction done in 0.918 secs. Sorting reachable states list... Time for model construction: 0.985 seconds. Type: SMG States: 33528 (1 initial) Transitions: 111686 Choices: 53186 Max/avg: 4/1.59 ------------------------------------------- Model checking: <<[1, 2]>> R{"value12"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 24.019684659454263 Time for model checking: 3.261 seconds. Result: 24.019684659454263 (value in the initial state) PRISM ===== Version: 4.0.1.games Date: Wed Sep 14 11:51:51 BST 2011 Hostname: qavbench.comlab Command line: prism examples/games/DSM/experiments/value_tradeoff/dsm3304p.smg -ex -pctl '<<1,2,3>> R{"value123"}max=? [F time=max_time]' Parsing model file "examples/games/DSM/experiments/value_tradeoff/dsm3304p.smg"... 1 property: (1) <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] ------------------------------------------- Building model... Computing reachable states... 33528 Reachable states exploration and model construction done in 0.844 secs. Sorting reachable states list... Time for model construction: 0.93 seconds. Type: SMG States: 33528 (1 initial) Transitions: 115950 Choices: 57450 Max/avg: 4/1.71 ------------------------------------------- Model checking: <<[1, 2, 3]>> R{"value123"}max=? [ F time=max_time ] Building reward structure... Value in the initial state: 38.788222413367805 Time for model checking: 3.318 seconds. Result: 38.788222413367805 (value in the initial state)