Merge pull request #1084 from lorchrob/check-env-bug-fix

Fix bug when checking realizability but not environment
kind2-mc · Aug 1, 2024 · ca8dcd3 · ca8dcd3
2 parents 3c2b77d + 4e22745
commit ca8dcd3
Showing 1 changed file with 13 additions and 8 deletions.
diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml
@@ -337,14 +337,19 @@ let of_channel old_frontend only_parse in_ch =
               (* 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]
+                    (2) the main node's enviornment, if environment checking is enabled *)
+              let main_nodes = 
+                if (not main_lustre_node.is_extern) && List.mem `CONTRACTCK (Flags.enabled ()) then 
+                  [LustreIdent.mk_string_ident (LGI.contract_tag ^ s);]
+                else [s_ident] 
+              in
+              let main_nodes = 
+                if (Flags.Contracts.check_environment ()) && List.mem `CONTRACTCK (Flags.enabled ()) then
+                  LustreIdent.mk_string_ident (LGI.inputs_tag ^ s) :: main_nodes 
+                else 
+                  main_nodes 
+                in 
+              main_nodes
             (* User-specified main node in command-line input might not exist *)
             with Not_found -> 
               let msg =