The initialization statement. This only runs once right at the beginning
Init x = m ∧ y = 0 mode = Loop
(mode = Loop ∧ x > 0 ∧ x’ = x - 1 ∧ y’ = y + n ∧ mode’ = loop) ∨ (mode = Loop ∧ x = 0 ∧ x’ = x ∧ y’ = y ∧ mode’ = stop)
”∨” means that it is just the ONE statement. So either the top part of the bottom part can happen, NOT BOTH
”∧” Essentially just means that it will both both statements.
look at Session 4 Safety requirements (part 2) for the actual tasks and lecture associated with it.
