Hola, no me queda muy claro cómo implementar la relación de que dos estados s y s' difieren a lo sumo en el valor asociado a idx en el componente map del estado s'.
Saludos,
Jairo.
En respuesta a Jairo Yamil Bonanata Silva
Re: [Práctico 7] Relación entre estados
Al menos hasta donde había llegado yo, se usaba solamente una instancia de esas relaciones (cuando difieren en el mapeo de la memoria, en una dirección ma).
En vez de definir la relación genérica, definí en particular para ese mapping memoria, mi firma es Definition eq_memory_ma (s s' : state)(ma : madd) : Prop.
Dados dos estados, cada entrada del record (que no sea memory) de uno y otro deben ser iguales.
Y el caso de las memorias, para todo índice que no sea ma, las imágenes por el mapping tienen que ser iguales.
En respuesta a Juan Pablo Garcia Garland
Re: [Práctico 7] Relación entre estados
Gracias, creo que es cómo vos decís!
Saludos!
Hola.
Está muy bien la respuesta de Juan Pablo.
Saludos, Carlos
En respuesta a Juan Pablo Garcia Garland
Re: [Práctico 7] Relación entre estados
Otro detalle, hay que poner que existe una página en la post condición del write. Porque si no, no podemos escribir en el aire como quién dice. ¿Es correcto?
Saludos,
Jairo.
Hola.
Si, es correcto lo que decís.
Saludos, Carlos
Hola, leyendo estos comentarios me surge la duda de si mi solución es también correcta.
¿Es estrictamente necesario poner el "existe una página"?
Yo lo que hice fue tomar en cuenta la sugerencia de Juan Pablo y luego para chequear la parte "s'.memory = (s.memory[ma := <RW(Some val),s.active_os>])" redefiní la entrada de ma en el map y le impuse que el owner era el sistema operativo activo.
Haciendo esto, me parece que no preciso el "existe página" ¿o sí?.
Además, con esta implementación, sería redundante chequear que "para todo índice que no sea ma, las imágenes por el mapping tienen que ser iguales" en una función eq_memory_ma porque queda verificado en la redefinición del map ¿o no?
Desde ya gracias.
Saludos
Hola.
Si, es correcto también.
Saludos, Carlos