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

Exercise 451, confusion about the notation


#1

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


#2

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