Hi Andrew,
Thanks for your report on Runway. Without having seen Runway, I can't
comment on it. But I would like to point out that the TLC standard
module provides features for performing the kind of statistical
analysis that you describe Runway doing. The RandomElement operator
allows adding execution probabilities, and the TLCSet/TLCGet operators
allow you to gather statistics when running TLC in simulation mode.
(You didn't mention gathering statistics, but I presume Runway
provides that.) See
They aren't nearly as convenient as having a built-in mechanism,
though I expect they are more expressive than anything built into a
language. I thought they could be useful for getting insight into
performance, but I never had the time to try them on a realistic
example and no one else was interested. It would be nice to know how
well this works in practice for Runway, and how inconvenient it would
be to do it with TLA+/TLC.
Cheers,
Leslie