[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Specifying all states on SimpleProgram from the TLA Course
I've been watching the videos on Lamport's TLA Course.
On the DieHard problem he makes a statement on why is it important to specify a state completely:
Here, he insists on adding /\ big' = big.
Now, on the SimpleProgram exercise (the first one), Add is defined like this:
Add == /\ pc = "middle"
/\ pc' = "done"
/\ i' = i + 1
My question is, if we need to specify the whole state space, shouldn't Add need to be defined this way instead?
Add == /\ pc = "middle"
/\ pc' = "done"
/\ i' = i + 1
/\ i \in 0..1000
--
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/8fa93e13-20e7-48fa-8225-75bb5744e93an%40googlegroups.com.
