(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)
(*<*)
(* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *)
theory GenEventSystem
imports UserEvent
begin
(*>*)

subsection \<open>\label{ssec:eventsys}Generated System Theory\<close>

subsubsection \<open>\label{sssec:eventsystypes}Types\<close>
text \<open>
  Identical types to those presented in \autoref{sssec:procsystypes} are
  generated for a system involving events.
\<close>

type_synonym component = "(channel, component_state) comp"

type_synonym lstate = "component_state local_state"

type_synonym gstate = "(inst, channel, component_state) global_state"

subsubsection \<open>\label{sssec:eventsysuntrusted}Untrusted Components\<close>
text \<open>
  As before, an untrusted definition is generated for each component type that
  permits any local operation or sending or receiving on any available
  interface.
\<close>

definition
  Collector_untrusted :: "(Collector_channel \<Rightarrow> channel) \<Rightarrow> component"
where
  "Collector_untrusted ch \<equiv>
    LOOP (
      UserStep
    \<squnion> ArbitraryRequest (ch Collector_ev)
    \<squnion> ArbitraryResponse (ch Collector_ev))"

definition
  Emitter_untrusted :: "(Emitter_channel \<Rightarrow> channel) \<Rightarrow> component"
where
  "Emitter_untrusted ch \<equiv>
    LOOP (
      UserStep
    \<squnion> ArbitraryRequest (ch Emitter_ev)
    \<squnion> ArbitraryResponse (ch Emitter_ev))"

subsubsection \<open>\label{sssec:eventsysev}Event Components\<close>
text \<open>
  For each connection in the system over which events are transmitted, a
  definition is generated of a component type that models the state of the
  event. The type enumerating the interfaces of this component is expressed as
  @{term unit} because, naturally, there is only a single interface to this
  introduced
  component. The details of the execution of the component can largely be
  expressed statically, and are captured by the definition, @{term event},
  described in \autoref{ssec:eventcomponents}.
\<close>

type_synonym SomethingHappenedEvent_channel = unit

definition
  SomethingHappenedEvent :: "(SomethingHappenedEvent_channel \<Rightarrow> channel) \<Rightarrow>
    component"
where
  "SomethingHappenedEvent ch \<equiv> event (ch ())"

subsubsection \<open>\label{sssec:eventsysinst}Component Instances\<close>
text \<open>
  The definitions of untrusted component instances are generated as in
  \autoref{h:procbase}, but a definition is also derived for an instance of the
  introduced component. There is no opportunity for the user to provide a
  definition of the trusted execution of this component, because we already
  know exactly what actions this component takes. Being part of the component
  platform itself, we can generate a definition that exactly expresses its
  execution.
\<close>

definition
  sink_untrusted :: component
where
  "sink_untrusted \<equiv>
    Collector_untrusted (\<lambda>c. case c of Collector_ev \<Rightarrow> simpleEvent1)"

definition
  source_untrusted :: component
where
  "source_untrusted \<equiv>
    Emitter_untrusted (\<lambda>c. case c of Emitter_ev \<Rightarrow> simpleEvent1)"

definition
  simpleEvent1\<^sub>e_instance :: component
where
  "simpleEvent1\<^sub>e_instance \<equiv> SomethingHappenedEvent (\<lambda>_. simpleEvent1)"

subsubsection \<open>\label{sssec:eventsysgs}Initial State\<close>
text \<open>
  The generated global state for this system also contains a case for the
  introduced event component, mapping to the instance definition presented
  above and the common initial event state. While this definition of the global
  state makes it possible for the user to override the mapping of
  @{term simpleEvent1\<^sub>e} in @{term trusted}, there is no practical
  reason to do this.
\<close>

definition
  gs\<^sub>0 :: gstate
where
  "gs\<^sub>0 p \<equiv> case trusted p of Some s \<Rightarrow> Some s | _ \<Rightarrow>
  (case p of sink \<Rightarrow> Some (sink_untrusted, Component init_component_state)
           | source \<Rightarrow> Some (source_untrusted, Component init_component_state)
           | simpleEvent1\<^sub>e \<Rightarrow> Some (simpleEvent1\<^sub>e_instance, init_event_state))"

(*<*)
end
(*>*)