I am assuming that your task is to verify the executions of the system in its different configurations, rather than just static properties of these configurations. The basic idea is then to define your initial predicate as a conjunction of formulas of the form
var \in ValidInitialStates
where the set ValidInitialStates characterizes the initial values of variable var in these initial configurations.
For a simple example, look at EWD840  where almost all variables can take arbitrary (type-correct) values.
Hope this helps,
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/13F08E3B-4935-4FFE-82C0-817E388103C2%40gmail.com.