epmc

Model:	consensus v.1 (MDP)
Parameter(s)	N = 4, K = 4
Property:	disagree (prob-reach)

java -Xms10240m -Xmx10240m -jar ./epmc-standard.jar check --model-input-files consensus.4.prism --property-input-files consensus.props --property-input-names disagree --translate-messages false --value-floating-point-output-native true --const K=4

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.

Walltime:	16.270522832870483s
Return code:	0
Relative Error:	3.428664520958809e-08

running-epmc-revision bcbb8ed631893b5fa072e28d29126ca3ba5337e0
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property disagree
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 14167 14167
build-model-done 43136 1
iterating
iterating-progress-unbounded 772 0.002730592329398207 1
iterating-progress-unbounded 1663 4.89757838456506E-4 2
iterating-progress-unbounded 2553 9.657062563428465E-5 3
iterating-progress-unbounded 3440 2.353183524400615E-5 4
iterating-progress-unbounded 4323 5.38811243822046E-6 5
iterating-progress-unbounded 5209 1.1706195472693803E-6 6
iterating-progress-unbounded 6097 2.448951459954607E-7 7
iterating-progress-unbounded 6984 5.062379840325981E-8 8
iterating-progress-unbounded 7875 1.0118991533580868E-8 9
iterating-progress-unbounded 8766 2.0156245561508968E-9 10
iterating-progress-unbounded 9658 3.975055840044206E-10 11
iterating-progress-unbounded 10549 7.775152743860758E-11 12
iterating-done 10791 12
model-checking-done 14
disagree: 0.15607305863684218