Hola:
No entiendo bien como considerar las funciones os_accesible y trusted_os
para formular las precondiciones.
Veo que aparecen como campos de un record Context definido en State.v.
¿La idea es considerar un parámetro que es de tipo Context y usar directamente esas funciones ? o ¿habría que definirlas de alguna manera?
Hola.
Antes de definir la semántica de las acciones tenés que incluir State.v y podés definir:
Parameter ctx : context.
Luego, por ejemplo al definir las precondiciones de las acciones podrías tener:
Definition Pre (a : Action) (s : state) := match a with
| Read va =>
ctxt_vadd_accessible ctx va = true
/\ aos_activity s = running
/\ ...
...
Saludos, Carlos
