search

prismmodelchecker / prism

The main development version of the PRISM model checker.
http://www.prismmodelchecker.org/
GNU General Public License v2.0
153 stars 69 forks source link

Tiebraking of the new round operator #118

Closed tquatmann closed 5 years ago

tquatmann commented 5 years ago

The documentation is not very explicit about rounding of halfway cases.

I think the rounding is always towards infinity, as the following model yields just one state:

dtmc

module main
x : [1..2] init 1;
[] x = -round(-0.5) -> (x'=2);
endmodule

Can you confirm this?

Notice that rounding of halfway cases in C/C++ is by default 'away from zero', while java.lang.Math.round() rounds towards infinity.

merkste commented 5 years ago

Yes, rounding towards infinity is the expected behavior. We should clarify this in the documentation. Round is implemented either via java.lang.Math#round or via some variant of round(x) = floor(x + 1/2)

tquatmann commented 5 years ago

Thank you for the clarification :)

davexparker commented 5 years ago

Thanks @tquatmann. Now documented at http://www.prismmodelchecker.org/manual/ThePRISMLanguage/Expressions.