CamkesAdlSpec: support maybe uses and maybe consumes interfaces

The CAmkES toolchain allows some interfaces to be declared optional.
We add such a flag to the ADL datatype and remove the requirement for
such interfaces to be connected.

camkes/adl-spec/Examples_CAMKES.thy

@@ -102,7 +102,7 @@ where
   "client \<equiv> \<lparr>
     control = True,
     hardware = False,
-    requires = [(''s'', simple)],
+    requires = [(''s'', (InterfaceRequired, simple))],
     provides = [],
     dataports = [],
     emits = [],
@@ -222,7 +222,7 @@ where
     provides = [],
     dataports = [],
     emits = [],
-    consumes = [(''event'', signal)],
+    consumes = [(''event'', (InterfaceRequired, signal))],
     attributes = []
   \<rparr>"
 
@@ -387,7 +387,7 @@ where
   "terminal_client \<equiv> \<lparr>
     control = True,
     hardware = False,
-    requires = [(''d'', display)],
+    requires = [(''d'', (InterfaceRequired, display))],
     provides = [],
     dataports = [],
     emits = [],
@@ -467,7 +467,7 @@ where
   "x \<equiv> \<lparr>
     control = undefined,
     hardware = undefined,
-    requires = [(undefined, [undefined])], \<comment> \<open>1 required interface...\<close>
+    requires = [(undefined, (InterfaceRequired, [undefined]))], \<comment> \<open>1 required interface...\<close>
     provides = undefined,
     dataports = undefined,
     emits = undefined,
@@ -544,7 +544,7 @@ lemma "\<not>wellformed_assembly \<lparr> composition = \<lparr>
     components = [(''foo'', \<lparr>
       control = undefined,
       hardware = undefined,
-      requires = [(''bar'', [undefined])],
+      requires = [(''bar'', (InterfaceRequired, [undefined]))],
       provides = undefined,
       dataports = undefined,
       emits = undefined,

camkes/adl-spec/Types_CAMKES.thy

@@ -283,14 +283,16 @@ text \<open>
       two @{text dataports}.
   \end{enumerate}
 \<close>
+datatype InterfaceRequired = InterfaceRequired | InterfaceOptional
+
 record component =
   control     :: bool
   hardware    :: bool
-  requires    :: "(adl_symbol \<times> procedure) list"
+  requires    :: "(adl_symbol \<times> (InterfaceRequired \<times> procedure)) list"
   provides    :: "(adl_symbol \<times> procedure) list"
   dataports   :: "(adl_symbol \<times> dataport) list"
   emits       :: "(adl_symbol \<times> event) list"
-  consumes    :: "(adl_symbol \<times> event) list"
+  consumes    :: "(adl_symbol \<times> (InterfaceRequired \<times> event)) list"
   attributes  :: "(adl_symbol \<times> param_type) list"
 
 subsection \<open>\label{subsec:assembling}Assembling a System\<close>

camkes/adl-spec/Wellformed_CAMKES.thy

@@ -92,11 +92,11 @@ where
     distinct (map fst (requires c) @ map fst (provides c) @ map fst (dataports c) @
               map fst (emits c) @ map fst (consumes c)) \<and>
      \<comment> \<open>No C symbol collisions.\<close>
-    (\<forall>x \<in> set (requires c). wellformed_procedure (snd x)) \<and>
+    (\<forall>x \<in> set (requires c). wellformed_procedure (snd (snd x))) \<and>
     (\<forall>x \<in> set (provides c). wellformed_procedure (snd x)) \<and>
     \<comment> \<open>Events valid.\<close>
     (\<forall>x \<in> set (emits c). wellformed_event (snd x)) \<and>
-    (\<forall>x \<in> set (consumes c). wellformed_event (snd x)) \<and>
+    (\<forall>x \<in> set (consumes c). wellformed_event (snd (snd x))) \<and>
      \<comment> \<open>Dataports valid.\<close>
     (\<forall>x \<in> set (dataports c). wellformed_dataport (snd x))"
 
@@ -145,12 +145,13 @@ text \<open>
 
 definition
   refs_valid_procedures ::
-    "adl_symbol \<Rightarrow> (adl_symbol \<times> procedure) list \<Rightarrow>
+    "adl_symbol \<Rightarrow> (adl_symbol \<times> (InterfaceRequired \<times> procedure)) list \<Rightarrow>
      (adl_symbol \<times> connection) list \<Rightarrow> bool"
 where
   "refs_valid_procedures component_instance procedures conns \<equiv>
-    \<forall>x \<in> set procedures.
-      snd x \<noteq> [] \<longrightarrow> (\<exists>1 y \<in> conns. \<exists>1 z \<in> conn_from (snd y). z = (component_instance, fst x))"
+    \<forall>(name, (req, proc)) \<in> set procedures.
+      req = InterfaceRequired \<longrightarrow> proc \<noteq> [] \<longrightarrow>
+      (\<exists>1 y \<in> conns. \<exists>1 z \<in> conn_from (snd y). z = (component_instance, name))"
 
 text \<open>
   For events and dataports, an interface can be left unconnected in a system with no
@@ -293,22 +294,23 @@ lemma wellformed_component_ann:
                  map fst (emits c) @ map fst (consumes c)
      in check_wellformed (wellformed_component, ''distinct'', names) (distinct names)) \<and>
     \<comment> \<open>No C symbol collisions.\<close>
-    (\<forall>x \<in> set (requires c). wellformed_procedure (snd x)) \<and>
+    (\<forall>x \<in> set (requires c). wellformed_procedure (snd (snd x))) \<and>
     (\<forall>x \<in> set (provides c). wellformed_procedure (snd x)) \<and>
     \<comment> \<open>Events valid.\<close>
     (\<forall>x \<in> set (emits c). wellformed_event (snd x)) \<and>
-    (\<forall>x \<in> set (consumes c). wellformed_event (snd x)) \<and>
+    (\<forall>x \<in> set (consumes c). wellformed_event (snd (snd x))) \<and>
     \<comment> \<open>Dataports valid.\<close>
     (\<forall>x \<in> set (dataports c). wellformed_dataport (snd x))
    )"
   by (simp only: wellformed_component_def remove_generic_tag simp_thms Let_def)
 
 lemma refs_valid_procedures_ann:
   "refs_valid_procedures component_instance procedures conns =
-     (\<forall>(name, proc) \<in> set procedures.
+     (\<forall>(name, (req, proc)) \<in> set procedures.
+      req = InterfaceRequired \<longrightarrow>
       check_wellformed (refs_valid_procedures, name)
         (proc \<noteq> [] \<longrightarrow> (\<exists>1 y \<in> conns. \<exists>1 z \<in> conn_from (snd y). z = (component_instance, name))))"
-  by (simp only: refs_valid_procedures_def remove_generic_tag simp_thms split_def)
+  by (simp only: refs_valid_procedures_def remove_generic_tag simp_thms)
 
 text \<open>
   For events and dataports, an interface can be left unconnected in a system with no