Я написал следующий код: MODULE main VAR status:{empty, no_empty}; x : 0..3; ASSIGN init(status):= empty; init(x):=0; next(status):= case (status = empty): no_empty; (status = no_empty) & (x=0): empty;...