Buenas tardes.
El paper define el campo active_os de State como os_ident. ¿En este modelo el hipervisor tiene asignado un identificador propio? En caso contrario, ¿no haría falta otro campo para identificar si el hipervisor está corriendo (o en su defecto que active_os sea parcial y si está vacío es el hipervisor el que corre)?
Saludos.