> I don’t know whether it’s better to cover all the static Alloy and then dynamics or to thread temporal logic through the usual route. I'd personally prefer t

> I don’t know whether it’s better to cover all the static Alloy and then dynamics or to thread temporal logic through the usual route. I'd personally prefer the latter. I find that temporal logic is significantly easier to understand than the usual Alloy workarounds (vs. e.g. stuff I've done with TLA+).