Re: [tlaplus] Re: Ideas for model-checking probabilistic consensus systems?

[Hillel Wayne <hwayne@xxxxxxxxx>]

I did some research on this and PRISM is actually the most advanced probabilistic modeling language out there. Verifying probability is really, really hard! For your use case you're probs best off writing a python script to autogen PRISM specs for you. You might be able to use the PRISM preprocessor, but that's still in beta: http://www.prismmodelchecker.org/prismpp/

Alernatively you might want to try using one of the experimental extensions to PRISM, like ProFeat: https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/ProFeat/

On 8/14/19 9:14 AM, Andrew Helwer wrote:

Per Hillel's post on PRISM (https://www.hillelwayne.com/post/prism/) it doesn't do sets/tuples/etc., you have to hardcode every element in the model; are there other modeling languages which don't have this restriction?

On Tuesday, August 13, 2019 at 7:05:18 PM UTC-7, Kai wrote:

Rather than waiting for a non-trivial extension to TLA and the toolbox, you may want to explore existing tools that target probabilistic systems, e.g., PRISM. The literature on it should have poiters to formalisms and tools in the area.

--
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/6d157040-12c3-491c-94fd-bf1b88c2013e%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/0415754b-e45d-ac3f-d90f-a3d8cc65645b%40gmail.com.