I proposed a little while back that we somehow combine Alloy for structure and TLA+ for order since they’re the easiest methods to learn. Either use both languages with a translator or extend one for the other. So, I’ve been looking for anyone doing something similar. I accidentally found this looking for a TLA+ spec-based test generator. Electrum extends Alloy with temporal operators. Tool is here.
@hwayne, these are the people I told you we should talk to about figuring something out. They’re already done lol. At least saved us some work. Now it’s more about seeing what their tool can handle with what improvements are needed. Aside from eliminating Java [again].