demo_1.1 Tau spec that talk about Tau spec that talk about Tau spec

[S1r_4zdr3w(OP)]

I try to understand the statement ({ i1[t]'o1[t] = 0 } i1[t] = 0) ? (o1[t] = 0) : (o1[t] = 1) found in demo_1.1-basic_syntax_and_history.tau

What does it mean when Tau says (Error) Empty program?

What is the flow of the execution?

This is how I chunk the ideas

Tau Specification:
Simple boolean function represented as BDD (Binary Decision Diagram)
Input 1 is negated ANDed with output 1, if the statement result is T (1) then statement is equal to F (0)

{ i1[t]'o1[t] = 0 }

> talks about Tau Specification
The result of { } is ANDed to i1[t] and if the statement T (1) then is assigned as F (0)

({ i1[t]'o1[t] = 0 } i1[t] = 0)

> that talks about Tau Specification
The result of ( { } AND ) becomes the statement in the if ? then is the (o1[t] =0)   :  (o1[t] = 1) is the else

({ i1[t]'o1[t] = 0 } i1[t] = 0) ? (o1[t] = 0) : (o1[t] = 1)

We cannot say 1st, 2nd and 3rd in order as all of the three specs are executed at the same time [t]
({ i1[t]'o1[t] = 0 } i1[t] = 0) ? (o1[t] = 0) : (o1[t] = 1)

Please correct me if I'm wrong, thanks!