Theory Observation_Setup

(* The observation functions, the same for all our confidentiality properties *)
theory Observation_Setup
imports Safety_Properties
begin

section‹The observation setup›

text ‹The observers are a arbitrary but fixed set of users:›

consts UIDs :: "userID set"

type_synonym obs = "act * out"

text ‹The observations are all their actions:›

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

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


end