module S = { var A: K; fun F=@A+1 }; module M = { import S; proc INIT=A:=0 }; module N = { import S; proc SUCC=A:=F }; in call M.INIT; call N.SUCC