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 GenDataportSystem
9imports UserDataport
10begin
11(*>*)
12
13subsection \<open>\label{ssec:dataportsys}Generated System Theory\<close>
14
15subsubsection \<open>\label{sssec:dataportsystypes}Types\<close>
16text \<open>
17  At the system level we have the now familiar generated types.
18\<close>
19
20type_synonym component = "(channel, component_state) comp"
21
22type_synonym lstate = "component_state local_state"
23
24type_synonym gstate = "(inst, channel, component_state) global_state"
25
26subsubsection \<open>\label{sssec:dataportsysuntrusted}Untrusted Components\<close>
27text \<open>
28  A definition is generated for the untrusted execution of the component,
29  @{term DataportTest}. In this definition there are two interfaces the
30  component can send and receive on, but the other details of the definition
31  are identical to the previous examples.
32\<close>
33
34definition
35  DataportTest_untrusted :: "(DataportTest_channel \<Rightarrow> channel) \<Rightarrow> component"
36where
37  "DataportTest_untrusted ch \<equiv>
38    LOOP (
39      UserStep
40    \<squnion> ArbitraryRequest (ch DataportTest_d2)
41    \<squnion> ArbitraryResponse (ch DataportTest_d2)
42    \<squnion> ArbitraryRequest (ch DataportTest_d1)
43    \<squnion> ArbitraryResponse (ch DataportTest_d1))"
44
45subsubsection \<open>\label{sssec:dataportsysinst}Component Instances\<close>
46text \<open>
47  The definitions for untrusted execution of the two component instances are
48  generated by partially applying the untrusted definition of
49  @{term DataportTest} with different functions mapping its interfaces to
50  connections. In this way, two processes are formed that have identical local
51  behaviour, but have different effects when they perform communication
52  actions.
53\<close>
54
55definition
56  comp2_untrusted :: component
57where
58  "comp2_untrusted \<equiv>
59    DataportTest_untrusted (\<lambda>c. case c of DataportTest_d1 \<Rightarrow> simple2
60                                        | DataportTest_d2 \<Rightarrow> simple1)"
61
62definition
63  comp1_untrusted :: component
64where
65  "comp1_untrusted \<equiv>
66    DataportTest_untrusted (\<lambda>c. case c of DataportTest_d2 \<Rightarrow> simple2
67                                        | DataportTest_d1 \<Rightarrow> simple1)"
68
69subsubsection \<open>\label{ssecdataportsysmem}Shared Memory Components\<close>
70text \<open>
71  A component instance is generated for each connection involving a dataport,
72  as mentioned previously. As for events, the user is given no opportunity to
73  provide trusted definitions for these instances because we can automatically
74  generate their precise behaviour without ambiguity.
75\<close>
76
77definition
78  simple2\<^sub>d_instance :: component
79where
80  "simple2\<^sub>d_instance \<equiv> Buf\<^sub>d (\<lambda>_. simple2)"
81
82definition
83  simple1\<^sub>d_instance :: component
84where
85  "simple1\<^sub>d_instance \<equiv> Buf\<^sub>d (\<lambda>_. simple1)"
86
87subsubsection \<open>\label{sssec:dataportsysgs}Initial State\<close>
88text \<open>
89  The initial state for this system includes cases for the introduced shared
90  memory components, using the definitions presented above. Both begin in the
91  common initial memory state containing the empty map.
92\<close>
93
94definition
95  gs\<^sub>0 :: gstate
96where
97  "gs\<^sub>0 p \<equiv> case trusted p of Some s \<Rightarrow> Some s | _ \<Rightarrow>
98  (case p of comp2 \<Rightarrow> Some (comp2_untrusted, Component init_component_state)
99           | comp1 \<Rightarrow> Some (comp1_untrusted, Component init_component_state)
100           | simple2\<^sub>d \<Rightarrow> Some (simple2\<^sub>d_instance, init_memory_state)
101           | simple1\<^sub>d \<Rightarrow> Some (simple1\<^sub>d_instance, init_memory_state))"
102
103(*<*)
104end
105(*>*)
106