Yeah, as far as I can tell TLA+ can accomplish more or less the same stuff as Colored Petri Nets. You get a pretty graph with CPNs and it can be interesting to watch the data flow around in the animators, but I've had trouble doing anything terribly useful with Petri Nets.

I haven't really done anything with it, but I've heard Alloy gives you a graphical animation while giving you similar utility to TLA+.