Theory Friend_Observation_Setup

theory Friend_Observation_Setup
  imports Friend_Intro
begin

subsection ‹Observation setup›

(* *)
type_synonym obs = "act * out"

locale FriendObservationSetup =
  fixes UIDs :: "userID set" ― ‹local group of observers at a given node›
begin

(*  *)
fun γ :: "(state,act,out) trans ⇒ bool" where
"γ (Trans _ a _ _) = (∃ uid. userOfA a = Some uid ∧ uid ∈ UIDs ∨ (∃ca. a = COMact ca))"

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

end

locale FriendNetworkObservationSetup =
  fixes UIDs :: "apiID ⇒ userID set" ― ‹groups of observers at different nodes›
begin

(*  *)
abbreviation γ :: "apiID ⇒ (state,act,out) trans ⇒ bool" where
"γ aid trn ≡ FriendObservationSetup.γ (UIDs aid) trn"

abbreviation g :: "apiID ⇒ (state,act,out)trans ⇒ obs" where
"g aid trn ≡ FriendObservationSetup.g trn"

end

end