Question about IO automaton
Let S be the set of all traces in which "11" does not appear (a safety property) and L be the liveness property defined such that if 1 appears then eventually 2 will appear after (in temporal logic: $\square( 1 \rightarrow \lozenge 2)$).
Then trace(P)=trace(S)$\cap$trace(L).