I don't think there's a built-in way to do this, but you could try generating the initial state as a TLC checkpoint and then use the checkpoint recovery option. I have no idea how that would behave if you try to use the checkpoint in a different spec, though.
H
----I have multiple TLA+ specifications with the same initial state space. The initial state space was computed through a lengthy computation and would require a significant amount of time. Is there an approach that allows the TLA+ Toolbox to read the initial state from a predefined text file? This file could potentially be the output of another model checking process, thus saving time.
--
Guo
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88d08319-a58e-4c95-88f1-2aaf1a06852dn%40googlegroups.com.