Consultas de Práctico

Buenas!

No me queda del todo claro la notación del pdf.

Se refiere a algo como esto? :

...
      | chmod          => (trusted_os ctxt s          /\ aos_exec_mode s' = svc /\ aos_activity s' = running
                                                      /\ active_os  s = active_os  s'
                                                      /\ oss        s = oss        s'
                                                      /\ hypervisor s = hypervisor s'
                                                      /\ memory     s = memory     s'                       ) \/
                          (trusted_os ctxt s -> False /\ aos_exec_mode s' = usr /\ aos_activity s' = running
                                                      /\ active_os  s = active_os  s'
                                                      /\ oss        s = oss        s'
                                                      /\ hypervisor s = hypervisor s'
                                                      /\ memory     s = memory     s'                       )

Básicamente pido que s' tenga las mismas imágenes que s, salvo en aos_exec_mode y aos_activity que pongo lo que dice el pdf. Sino no se me ocurre de qué está hablando.

Gracias!