epmc

Benchmark
Model:mapk_cascade v.1 (CTMC)
Parameter(s)N = 4, T = 30
Property:activated_time (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files mapk_cascade.prism --property-input-files mapk_cascade.props --property-input-names activated_time --translate-messages false --value-floating-point-output-native true --const N=4,T=30
Default settings. The option --translate-messages is set to false to ease the parsing of the output while the --value-floating-point-output-native is set to true to get the float values printed in full, instead of with only 7 digits of precision given by the default %.7f format.
Execution
Walltime:14.33588695526123s
Return code:0
Relative Error:1.3225750372297463e-10
Log
running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property activated_time
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 16269 16268
build-model-states-explored 37014 20746
build-model-states-explored 57423 20409
build-model-states-explored 77239 19816
build-model-states-explored 97803 20564
build-model-done 99535 5
iterating
iterating-progress-unbounded 400 0.014757353726508882 1
iterating-progress-unbounded 849 4.118848915339868E-4 2
iterating-progress-unbounded 1298 1.1495906434788594E-5 3
iterating-progress-unbounded 1745 3.2601205646187736E-7 4
iterating-progress-unbounded 2193 9.17196274485832E-9 5
iterating-progress-unbounded 2640 2.601083792796999E-10 6
iterating-done 2848 6
model-checking-done 13
activated_time: 40.67650299055258