Be careful, rules with creation should be tested to deal with implicit sites

Jérôme FERET · Jérôme FERET · commit 452257774db0 · 2026-05-06T23:31:44.000+02:00
diff --git a/core/KaSa_rep/reachability_analysis/composite_domain.ml b/core/KaSa_rep/reachability_analysis/composite_domain.ml
@@ -545,9 +545,10 @@ module Make (Domain : Analyzer_domain_sig.Domain) = struct
         bonds = Ckappa_sig.AgentSite_map_and_set.Map.empty;
       }
     in
+    let error, dynamic = scan_rule_creation static dynamic error in 
     let error, dynamic =
       match patch with
-      | None -> scan_rule_creation static dynamic error
+      | None -> error, dynamic 
       | Some _ -> scan_rule_patch ?start static dynamic error
     in
     let error, dynamic, () = apply_event_list static dynamic error event_list in
diff --git a/tests/integration/incremental/creation_with_implicit_signature/README b/tests/integration/incremental/creation_with_implicit_signature/README
@@ -0,0 +1,2 @@
+cat command.txt|"${KAPPABIN}"KaSaIncremental essai.ka 
+
diff --git a/tests/integration/incremental/creation_with_implicit_signature/command.txt b/tests/integration/incremental/creation_with_implicit_signature/command.txt
@@ -0,0 +1,2 @@
+update file essai_diff.ka as essai.ka 
+q
diff --git a/tests/integration/incremental/creation_with_implicit_signature/essai.ka b/tests/integration/incremental/creation_with_implicit_signature/essai.ka
@@ -0,0 +1,2 @@
+A(x{u}),. -> A(x{u}),B(x{p}) @1 
+%init: 10 A() 
diff --git a/tests/integration/incremental/creation_with_implicit_signature/essai_diff.ka b/tests/integration/incremental/creation_with_implicit_signature/essai_diff.ka
@@ -0,0 +1,3 @@
+A(x{u}),. -> A(x{u}),B(x{p}) @1 
+%init: 10 A() 
+B(x{p},y{u})-> B(x{u},y{p}) @1
diff --git a/tests/integration/incremental/creation_with_implicit_signature/output/LOG.ref b/tests/integration/incremental/creation_with_implicit_signature/output/LOG.ref
@@ -0,0 +1,57 @@
+Parsing essai.ka...
+done
+Compiling...
+Reachability analysis...
+------------------------------------------------------------
+every rule may be applied
+------------------------------------------------------------
+every agent may occur in the model
+
+------------------------------------------------------------
+* Non relational properties:
+------------------------------------------------------------
+A(x) => A(x{u})
+B(x) => B(x{p})
+
+------------------------------------------------------------
+* Relational properties:
+------------------------------------------------------------
+------------------------------------------------------------
+* Properties in connected agents
+------------------------------------------------------------
+------------------------------------------------------------
+* Properties of pairs of bonds
+------------------------------------------------------------
+------------------------------------------------------------
+* Properties of counters
+------------------------------------------------------------
+execution finished without any exception
+Parsing essai_diff.ka...
+done
+------------------------------------------------------------
+every rule may be applied
+------------------------------------------------------------
+every agent may occur in the model
+
+------------------------------------------------------------
+* Non relational properties:
+------------------------------------------------------------
+A(x) => A(x{u})
+B(x) => [ B(x{p}) v B(x{u}) ]
+B(y) => [ B(y{u}) v B(y{p}) ]
+
+------------------------------------------------------------
+* Relational properties:
+------------------------------------------------------------
+B(x{u}) <=> B(y{p})
+------------------------------------------------------------
+* Properties in connected agents
+------------------------------------------------------------
+------------------------------------------------------------
+* Properties of pairs of bonds
+------------------------------------------------------------
+------------------------------------------------------------
+* Properties of counters
+------------------------------------------------------------
+execution finished without any exception
+> 
diff --git a/tests/integration/incremental/creation_with_implicit_signature/output/error.log.ref b/tests/integration/incremental/creation_with_implicit_signature/output/error.log.ref

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+cat command.txt\|"${KAPPABIN}"KaSaIncremental essai.ka`
	`2`	`+`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+update file essai_diff.ka as essai.ka`
	`2`	`+q`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+A(x{u}),. -> A(x{u}),B(x{p}) @1`
	`2`	`+%init: 10 A()`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+A(x{u}),. -> A(x{u}),B(x{p}) @1`
	`2`	`+%init: 10 A()`
	`3`	`+B(x{p},y{u})-> B(x{u},y{p}) @1`