Rolling dices in TLA+

[Tacettin Emre Bök]

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

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fbc29ec8-6f8c-4c0c-b95a-c0628bfc4cb9n%40googlegroups.com.

[Markus Kuppe]

Shameless plug and partially related:

"Obtaining Statistical Properties by Simulating Specs with TLC”
https://www.youtube.com/watch?v=cYenTPD7740

Markus

[Alex Shirley]

if you want to roll an array of dice here are two options:

\* Same for both version

VARIABLE die

Init ==

    die = [i \in 1..8 |-> 1]

\* Roll Each die by itself

\* Explore if any of the dice are rolled

RollDie(x, val) ==

    die' = [die EXCEPT ![x] = val]

Next == \* Example Usage

    \/ \E d \in DOMAIN die, f \in 1..6: RollDie(d, f)

\* or Roll all the dice simultaneously

RollDie ==

    \E d \in [{1..8} -> 1..6]: die' = d

Generally when it comes to state space exploration, they roughly yield the same results, so it's more about readability and what you're trying to convey

Alex