Thanks, Hillel, for the feedback! I appreciate it. I didn’t include PRISM examples directly in the docs to avoid redundancy but linked to them where relevant. I also acknowledged PRISM as the state of the art tool for probabilistic modeling. Please let me know if I need to reword anything.
For those unfamiliar, I’m the developer of FizzBee. Here are my thoughts, probabilistic modeling generally involves two phases:
FizzBee simplifies the first phase with a Python-like language where you describe the algorithm, and it automatically generates the state graph.
PRISM excels at the second phase with a full pCTL query language. As Andrew and Elina mentioned, PRISM supports DTMC, CTMC, and MDP, while FizzBee currently covers a subset of DTMC with basic scripting for common queries.
Example models in both tools:
PRISM:
FizzBee:
Since this is the TLA+ group, I don’t want to take the thread off course, happy to continue elsewhere if anyone’s interested!
Thanks,I really don't like how that FizzBee tutorial spends a bunch of time trash talking PRISM and saying FizzBee is better and easier, but doesn't show any PRISM samples or actually compare the two--On Sun, Feb 2, 2025, 8:12 AM Elina Mäkinen <emakinen.helsinki@xxxxxxxxx> wrote:TLA+ do not have native support for probabilistic analysis.If you want more Markov chain analysis consider FizzBee and PRISM. They natively support Markov chain analysis.PRISM supports DTMC, CTMC and MDP.FizzBee supports DTMC.You can attach both probabilities and rewards/cost for probabilistic and performance analysis.--On Sat, 1 Feb 2025 at 20:14, Rob Fielding <rob.fielding@xxxxxxxxx> wrote:I can't envision having state machines without at least having a way to attach transition probabilities. Would it make sense to treat parts without backticks as a "match" that can be annotated with a probability. ie: Just make a proper M/M/1 queue. Or discrete time differential equation. It seems that attaching probabilities for multiple matches, where under 100% match would imply stuttering, but otherwise should do no harm.
lambda := 0.2
mu := 0.3
((x = 0)_{lambda} and (x' = x+1))
or
((x > 0)_{mu} and (x' = x-1))
or
((x > 0)_{lambda} and (x' = x+1)) --
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 visit https://groups.google.com/d/msgid/tlaplus/31c54ba4-df67-4dfc-b041-15f213f86605n%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 visit https://groups.google.com/d/msgid/tlaplus/CAHQi85kyExvut7_C_sq1tfEbdyrU%3DLjYzciWtf82MwdEGinsbw%40mail.gmail.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 visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8sx28qa0DY1nqZ1T7U3dO%2But7w5vTn-PvNbLHkD5BXv81w%40mail.gmail.com.