Buenas, revisando el material me está costando entender a que refiere bien la línea:
s'.memory = (s.memory[ma := <RW(Some val), s.active_os>]).
Interpreto que debe referir a la definición s' = s.[c1,...,cn]v1,...,vn the relation establishes that s and s' differ at most in the values v1,...,vn of the components c1,...,cn in state s'.
Pero de ser así, no me estoy dando cuenta cómo se mapearía en este caso, ya que difiere un poco. Si esta no es la interpretación correcta, no estaría encontrando por donde va.
Muchas gracias.
Saludos,
Bruno Lartigau