> That modelling was only somewhat successful; based on the constraints applied by each part, I discovered that it would be impossible to make the entire system reliable.
"I discovered I can't satisfy all my requirements at once and need to plan my tradeoffs in advance" sounds like a pretty successful modeling result to me!
You're right :). I sometimes look at that modelling exercise with disappointment; not because I didn't get any value out of it (I got a ton), but because I'm not yet good enough at TLA+ to have been able to successfully write a model that handled all the edge cases.
"I discovered I can't satisfy all my requirements at once and need to plan my tradeoffs in advance" sounds like a pretty successful modeling result to me!