... passado^2.1

Que só contém os operadores temporais $\ldots$, $\ldots$, $\mathcal{B}$ e $\circleddash$.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... são^2.2

Eventualmente até poderão ser falsas.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... sub-transições^3.1

Esta noção de sub-transição, que não é utilizada explicitamente nas aulas teóricas, deve-se ao facto de algumas instruções gerarem mais do que uma transição. Por exemplo, a instrução de ciclo while gera duas transições. Estas duas transições são denominadas sub-transições no STeP e são agrupadas dentro de uma única secção nos FTSs gerados no STeP.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... FTSs^3.2

É de notar que, ao contrário do apresentado em [6], o STeP não gera as condições de activação que definem em que condições um valor pode ser sintetizado. Por exemplo, no caso da atribuição x := e não é gerada a condição de activação $\exists a \cdot (a = e)$

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.