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.