add initial state guard to agents domain

Kappa-Dev · Feb 17, 2025 · 15bad79 · 15bad79
1 parent 3fe6af4
commit 15bad79
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 3 deletions.
diff --git a/core/KaSa_rep/frontend/handler.ml b/core/KaSa_rep/frontend/handler.ml
@@ -833,6 +833,11 @@ let guard_to_bdu parameters error handler_bdu guard bdu_restriction =
   in
   aux error handler_bdu guard
 
+let guard_to_bdu_opt parameters error handler_bdu guard bdu_restriction =
+  match guard with
+  | None -> Ckappa_sig.Views_bdu.mvbdu_true parameters handler_bdu error
+  | Some g -> guard_to_bdu parameters error handler_bdu g bdu_restriction
+
 let print_guard_mvbdu_decompose parameters error kappa_handler bdu_handler
     ?(with_comma = false) mvbdu restriction_bdu =
   let error, bdu_handler, mvbdu_list =

diff --git a/core/KaSa_rep/frontend/handler.mli b/core/KaSa_rep/frontend/handler.mli
@@ -276,6 +276,16 @@ val guard_to_bdu :
   * Ckappa_sig.Views_bdu.handler
   * Ckappa_sig.Views_bdu.mvbdu
 
+val guard_to_bdu_opt :
+  Remanent_parameters_sig.parameters ->
+  Exception_without_parameter.exceptions_caught_and_uncaught ->
+  Ckappa_sig.Views_bdu.handler ->
+  Ckappa_sig.c_guard_parameter LKappa.guard option ->
+  Ckappa_sig.Views_bdu.mvbdu ->
+  Exception_without_parameter.exceptions_caught_and_uncaught
+  * Ckappa_sig.Views_bdu.handler
+  * Ckappa_sig.Views_bdu.mvbdu
+
 val collect_guard_mvbdus :
   Remanent_parameters_sig.parameters ->
   Exception_without_parameter.exceptions_caught_and_uncaught ->

diff --git a/core/KaSa_rep/reachability_analysis/agents_domain.ml b/core/KaSa_rep/reachability_analysis/agents_domain.ml
@@ -434,6 +434,7 @@ module Domain = struct
 
   let init_agents static dynamic error init_state event_list =
     let parameters = get_parameter static in
+    let restriction_bdu = get_restriction_mvbdu static in
     let error, (dynamic, event_list) =
       Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.fold parameters
         error
@@ -446,13 +447,14 @@ module Domain = struct
           | Cckappa_sig.Agent agent ->
             let agent_type = agent.Cckappa_sig.agent_name in
             let bdu_handler = get_mvbdu_handler dynamic in
-            let error, bdu_handler, mvbdu_true =
-              Ckappa_sig.Views_bdu.mvbdu_true parameters bdu_handler error
+            let error, bdu_handler, mvbdu_guard =
+              Handler.guard_to_bdu_opt parameters error bdu_handler
+                init_state.Cckappa_sig.e_init_guard restriction_bdu
             in
             let dynamic = set_mvbdu_handler bdu_handler dynamic in
             let error, (dynamic, event_list) =
               add_event_list static dynamic error agent_type event_list
-                mvbdu_true
+                mvbdu_guard
             in
             error, (dynamic, event_list))
         init_state.Cckappa_sig.e_init_c_mixture.Cckappa_sig.views