#### Program

• $x = new ctr; x.inc\left(\right); v = x.n$

#### Transitions

• $<< x = new ctr, %f_1 >> \apijl\left\{ctr_1\right\} << %e, %f_1\left[ x := ctr_1 \right]>>$
• $\left[1\right]$

• $<< n = n + 1, %f_2^\left\{%a\right\} >> -> <<%e, %f_2\left[%a.n = %a.n + 1\right]>>$
• $\left[2\right]$

• $<< x.inc\left(\right), %f_2 >>$ $\apijl\left\{inc_\left\{%a\right\}$ $<< %e, %f_2\left[%f_2\left(x\right).n := %f_2\left(x\right).n \right]>>$
• $\left[2\text{'}\right]$

• $<< v = x.n, %f_3>> -> << %e, %f_3\left[v := %f_3\left(x\right).n\right] >>$
• $\left[3\right]$

#### Trace

• $%f \apijl\left\{%l\right\} %f\text{'}$ with $%f = %f_1$, $%f\text{'} = %f_3$ and $%l = ctr_1 \. inc_\left\{ %a \right\}$

slide: Transitions -- example