Buenas,
Al momento de formalizar las post condiciones del write hay que implementar (s1 ∼ memory,ma s2). Para esto se nos ocurrio comparar s2 con un nuevo estado que es igual a copiar el estado s1 pero con una memoria diferente. Algo de la siguiente manera:
s2 = new_state (active_os s1) (aos_exec_mode s1) (aos_activity s1) (oss s1) (hypervisor s1) mem.
Lo que nos esta costando es obtener la nueva memoria "mem". Pensamos en usar una funcion para cambiar la pagina en la direccion ma, pero no vemos como hacerlo.
La otra duda es sobre la propiedad 3 de la parte 7.5. La propiedad dice "if the hypervisor or a trusted OS is running the processor must be in supervisor mode". Para la parte de ver si es un trusted_OS implementamos el predicado mencionado en la pagina 5 (trusted_OS), pero no logramos identificar cuando es el hypervisor el que esta ejecutando. Por lo que leimos, cuando el campo aos_activity esta en waiting es porque el hypervisor esta ejecutando. Esto es correcto? o hay otra situacion en la que ejecute el hypervisor?
Muchas gracias.