[General boards] [Winter 2019 courses] [Fall 2018 courses] [Summer 2018 courses] [Older or newer terms]

Exercise 451, confusion about the notation


In Exercise 451, the solution provided lets assignment take time 1.
Originally, the left process looks like this:
but after incorporating time, it looks like this:
Isn’t image just the assignment of ‘not b’ to time t+1? I don’t see how that is the same as image


An interactive variable is a function of time. b is an interactive variable. b(t+1) is the value of interactive variable b at time t+1. An assignment x:=e to an interactive variable x that takes time 1 is
x(t’)=e ∧ t’=t+1
So b:=⊥ is
b(t’)=⊥ ∧ t’=t+1
or equivalently
¬b(t+1) ∧ t’=t+1