Merge pull request kind2-mc#1050 from daniel-larraz/conservative-circ…

…ularity-check

Make circularity check more conservative

doc/usr/source/2_input/1_lustre.rst

@@ -798,6 +798,12 @@ is used.
 In a modular analysis, ``imported`` nodes will not be analyzed, although if their
 contract has modes they will be checked for exhaustiveness, consistently with
 the usual Kind 2 contract workflow.
+Every output of an imported node is assumed to depend on every input.
+This may lead Kind 2 to detect circular dependencies that do not exist
+in an _actual_ system, resulting in the rejection of an input model.
+To make Kind 2 accept such model, the imported node must be refined
+by decomposing it into smaller subnodes and specifying the actual
+dependencies among inputs and outputs.
 
 
 Partially defined nodes VS ``imported``

src/lustre/lustreAstDependencies.ml

@@ -108,9 +108,9 @@ type node_summary = ((int list) IntMap.t) IMap.t
     we would substitute the indices with the actual call parameters
     during the circularity analysis for equations.
 
-    For functions and imported nodes we assume that
-    output streams do not depend on any of the input streams.
-    This restriction is in place to avoid rejecting valid programs.
+    For imported nodes and functions we make the conservative assumption
+    that each output stream is dependent on the current values 
+    of all the arguments.
     
     We generate the node summary entry by doing a rechablility analysis 
     for each of the output streams equations. 
@@ -1158,8 +1158,8 @@ let mk_node_summary: bool -> node_summary -> LA.node_decl -> node_summary
       s
 (** Computes the node call summary of the node to the input stream of the node.
     
-    For imported nodes and imported functions we assume that output streams do not depend on
-    any of the input streams. This restriction is in place to avoid rejecting valid programs.
+    For imported nodes and imported functions we assume that output streams depend on 
+    every input stream.
  *)
 
 
@@ -1284,7 +1284,7 @@ let check_node_equations: dependency_analysis_data
   = fun ad ((i, imported, params, ips, ops, locals, items, contract_opt) as ndecl)->
   (if not imported then
     let* _ = check_no_input_output_local_duplicate ips ops locals in
-    analyze_circ_node_equations ad.nsummary items
+    analyze_circ_node_equations ad.nsummary2 items
    else R.ok())
   >> match contract_opt with
      | None -> R.ok ndecl