1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6(*<*)
7(* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *)
8theory GenSimpleSystem
9imports UserSimple
10begin
11(*>*)
12
13subsection \<open>\label{ssec:procsys}Generated System Theory\<close>
14
15subsubsection \<open>\label{sssec:procsystypes}Types\<close>
16text \<open>
17  At the system level, type instantiations are provided for components and
18  local and global state. These are derived by simply instantiating the
19  relevant types with the types generated in the base theory. Note that
20  the @{term component_state} type is expected to be provided by the user in
21  their intermediate theory.
22\<close>
23
24type_synonym component = "(channel, component_state) comp"
25
26type_synonym lstate = "component_state local_state"
27
28type_synonym gstate = "(inst, channel, component_state) global_state"
29
30subsubsection \<open>\label{ssec:procsysuntrusted}Untrusted Components\<close>
31text \<open>
32  For each component type, a definition is generated that describes its
33  execution without specifying the behaviour of any user-provided code. These
34  definitions allow the component to perform any manipulation of its local
35  state or to send or receive any message on the interfaces available to it.
36  These definitions are intended for use in a system composition when the
37  behaviour of a specific component is not relevant to the desirable property
38  of the whole system.
39  These definitions are more general than the implementation allows, in that
40  they permit an untrusted component to perform actions such as sending on an
41  incoming interface which may not be possible in the implementation.
42
43  Recall from \autoref{h:userstubs} that the user is expected to provide a
44  mapping describing trusted components in their intermediate theory. A
45  definition of untrusted execution for each component is generated regardless
46  of whether all instances of that component in the current system have trusted
47  specifications or not.
48\<close>
49
50definition
51  Client_untrusted :: "(Client_channel \<Rightarrow> channel) \<Rightarrow> component"
52where
53  "Client_untrusted ch \<equiv>
54    LOOP (
55      UserStep
56    \<squnion> ArbitraryRequest (ch Client_s)
57    \<squnion> ArbitraryResponse (ch Client_s))"
58
59definition
60  Echo_untrusted :: "(Echo_channel \<Rightarrow> channel) \<Rightarrow> component"
61where
62  "Echo_untrusted ch \<equiv>
63    LOOP (
64      UserStep
65    \<squnion> ArbitraryRequest (ch Echo_s)
66    \<squnion> ArbitraryResponse (ch Echo_s))"
67
68subsubsection \<open>\label{ssec:procsysinst}Component Instances\<close>
69text \<open>
70  As was the case for the instantiation of primitives in
71  \autoref{sssec:procbaseinst}, with the definition of an untrusted component's
72  execution generated previously, a definition of the execution of an untrusted
73  instance can be formed by partially applying the component definition. A
74  definition of untrusted execution is generated for each component instance,
75  whether it is required or not.
76\<close>
77
78definition
79  client_untrusted :: component
80where
81  "client_untrusted \<equiv> Client_untrusted (\<lambda>c. case c of Client_s \<Rightarrow> simple)"
82
83definition
84  echo_untrusted :: component
85where
86  "echo_untrusted \<equiv> Echo_untrusted (\<lambda>c. case c of Echo_s \<Rightarrow> simple)"
87
88subsubsection \<open>\label{sssec:procsysgs}Initial State\<close>
89text \<open>
90  The final generated definition is the initial state of the system. Following
91  the type instantiations in \autoref{sssec:procsystypes}, the initial global
92  state is
93  a mapping from component instance names to a pair of their program text and
94  local state. The generated definition looks for the instance's definition in
95  the (user-provided) mapping of trusted instances and, if it does not find
96  this, falls back on the generated untrusted definitions.
97\<close>
98
99definition
100  gs\<^sub>0 :: gstate
101where
102  "gs\<^sub>0 p \<equiv> case trusted p of Some s \<Rightarrow> Some s | _ \<Rightarrow>
103  (case p of client \<Rightarrow> Some (client_untrusted, Component init_component_state)
104           | echo \<Rightarrow> Some (echo_untrusted, Component init_component_state))"
105
106(*<*)
107end
108(*>*)
109