From 2308df9367ecd985041e66086302672579b93fc1 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 29 Dec 2021 10:50:44 +0100
Subject: [PATCH] [aorai] add missing assumes for out-of-state bhvs of
 unobserved functions

---
 src/plugins/aorai/aorai_visitors.ml           | 26 +++++++++++--------
 .../aorai/tests/ya/oracle/observed.res.oracle |  2 ++
 2 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 08dff72aecd..9a375909b53 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -421,18 +421,22 @@ let neg_trans kf trans =
           ([stop],[]) l
       in
       let cond =
-        List.fold_left
-          (fun cond stop ->
-             let trans = Path_analysis.get_edges start stop auto in
-             List.fold_left
-               (fun cond tr ->
-                  Logic_simplification.tand
-                    cond (Logic_simplification.tnot tr.cross))
-               cond trans)
-          TTrue same_start
+        if Data_for_aorai.isObservableFunction kf then begin
+          let cond =
+            List.fold_left
+              (fun cond stop ->
+                 let trans = Path_analysis.get_edges start stop auto in
+                 List.fold_left
+                   (fun cond tr ->
+                      Logic_simplification.tand
+                        cond (Logic_simplification.tnot tr.cross))
+                   cond trans)
+              TTrue same_start
+          in
+          let cond = fst (Logic_simplification.simplifyCond cond) in
+          Aorai_utils.crosscond_to_pred cond kf Promelaast.Call
+        end else Logic_const.pfalse
       in
-      let cond = fst (Logic_simplification.simplifyCond cond) in
-      let cond = Aorai_utils.crosscond_to_pred cond kf Promelaast.Call in
       let cond =
         Logic_const.por (Aorai_utils.is_out_of_state_pred start, cond)
       in
diff --git a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
index ffb2b1dba40..393c8d85224 100644
--- a/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/observed.res.oracle
@@ -170,12 +170,14 @@ void f(void)
       ensures 0 ≡ aorai_intermediate_state;
     
     behavior Buchi_behavior_out_1:
+      assumes 0 ≡ aorai_intermediate_state_0;
       ensures 0 ≡ aorai_intermediate_state_0;
     
     behavior Buchi_behavior_out_2:
       ensures 0 ≡ final;
     
     behavior Buchi_behavior_out_3:
+      assumes 0 ≡ first_step;
       ensures 0 ≡ first_step;
     
     behavior Buchi_behavior_out_4:
-- 
GitLab