Theory Observation_Setup

theory Observation_Setup
imports Safety_Properties
begin

section ‹Observation setup for confidentiality properties›


text ‹The observation infrastructure, consisting of
a discriminator $\gamma$ and a selector $g$,
is the same for all our confidentiality properties.
Namely, we fix a group UIDs of users, and consider
the actions and outputs of these users.
›

consts UIDs :: "userID set" (* the observers *)

type_synonym obs = "act * out"

fun γ :: "(state,act,out) trans ⇒ bool" where
"γ (Trans _ a _ _) = (userOfA a ∈ UIDs)"

fun g :: "(state,act,out)trans ⇒ obs" where
"g (Trans _ a ou _) = (a,ou)"


end