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