For a synchronous program, every variable has a unique value at any point of time. The input variables are thereby determined by the environment, i.e., they receive a new value (randomly) at every point of time. The local and output variables are determined by the module.
In one macro step, a finite number of micro steps can take place. The number of micro steps is not bounded, but it must be finite. Which actions (micro steps) are executed is precisely determined by the operational semantics. For the statement [weak] abort S when(i); emit(o3), it is the case that if we are inside of S and i holds, then the abort statement terminates and emit(o3) is executed as a further micro step in the same macro step. The SOS rules precisely define that behavior.
