Re: [tlaplus] Rolling dices in TLA+

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Rolling a die is naturally represented using non-determinism, via a formula such as

\E d \in 1 .. 6 : ... 

in TLA+ or a statement

with (d \in 1 .. 6) {

  ...

}

in PlusCal. Note, however, that TLA+ will not allow you to verify any properties related to probability distributions, such as expected rewards. Prism [1] would be a suitable tool for such analyses.

Stephan

[1] https://www.prismmodelchecker.org

On 11 Apr 2023, at 17:09, Tacettin Emre Bök <emreturkk1@xxxxxxxxx> wrote:

Hi,

I've been trying to specify a game called "Heckmeck" using TLA+. The game includes rolling of 8 dices each having 6 faces, repeatedly. How can I specify this behavior on TLA+? Can you help?

Thanks,

Taci

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fbc29ec8-6f8c-4c0c-b95a-c0628bfc4cb9n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/43C57D2F-3A70-4C9F-AD9D-D7D1705C94B4%40gmail.com.