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