Re: [tlaplus] Rolling dices in TLA+

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Shameless plug and partially related: 

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

Markus

> On Apr 11, 2023, at 11:28 PM, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
> 
> 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.


-- 
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/F789EC5B-42F5-4A33-B9B6-E8D0D236E9E2%40lemmster.de.