From 58698d6e9f61b61db3c02d1e6dd54f1a99b5002c Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Thu, 9 May 2024 12:41:36 -0500 Subject: [PATCH] When checking imp node realizability, need both node contract and environment --- src/lustre/lustreInput.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index d597e3a5c..19652ba5c 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -311,13 +311,16 @@ let of_channel old_frontend only_parse in_ch = | Some s -> let s_ident = LustreIdent.mk_string_ident s in let main_lustre_node = LN.node_of_name s_ident nodes in - (* If checking realizability and main node is not external (imported), then + (* If checking realizability, then we are actually checking realizability of Kind 2-generated imported nodes representing the (1) the main node's contract instrumented with type info and (2) the main node's enviornment *) if (not main_lustre_node.is_extern) && List.mem `CONTRACTCK (Flags.enabled ()) then [LustreIdent.mk_string_ident (LGI.contract_tag ^ s); LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] + else if main_lustre_node.is_extern && List.mem `CONTRACTCK (Flags.enabled ()) then + [s_ident; + LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] else [s_ident] | None -> ( match LustreNode.get_main_annotated_nodes nodes with