Merge pull request #187 from imitator-model-checker/feat/exist_proper…

…ties

Supporting exists in properties file

doc/IMITATOR-user-manual.tex

@@ -2114,13 +2114,30 @@ \section{Model templates}\label{section:templates}
 \end{example}
 
 \paragraph{Templates in properties}
-The \styleIMI{forall} construction can also be used in properties.
-Below is an example of property using such a syntax (unrelated to the former model example).
-Note that \styleIMI{NB} is a constant defined in the model, leading to an easy specification of properties.
 
-\begin{IMITATORproperty}
-property := #synth EF(forall i in [0, NB - 1]: loc[train[i]] = train_End);
-\end{IMITATORproperty}
+The \styleIMI{forall} construction can also be used in properties. We also added the analogous \styleIMI{exists} construct,
+which creates a disjunction instead of a conjunction. The user can nest \styleIMI{forall} and \styleIMI{exists}
+in any way he wants. The syntax is exactly the same as for the models. but it has
+lower precedence in comparison to all the other logical operators. This means that, unless the user enclose
+the predicate inside the forall with parenthesis, only the first statement will be considered as part of
+the \styleIMI{forall}/\styleIMI{exists}.
+
+
+\begin{example}
+	Below is an example of property using such a syntax (unrelated to the former model example). It clarifies the precedence and what can be done with nesting.
+	Note that \styleIMI{NB} is a constant defined in the model, leading to an easy specification of properties.
+
+	\begin{IMITATORproperty}
+	(* True || False is outside of the forall *)
+	property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False)
+
+	(* True || False is inside of the forall *)
+	property := #synth AGnot(forall i in [0, N - 1]: (loc[p[i]] <> cs && True || False))
+
+	(* Nesting *)
+	property := #synth AGnot(exists i in [0, N - 1]: (forall i in [0, N - 1]: loc[p[i]] <> cs) && True || False)
+	\end{IMITATORproperty}
+\end{example}
 
 
 
@@ -5757,7 +5774,7 @@ \section{Grammar of the property file}\label{section:grammar-property}
 	$|$ & \styleIMI{PRPC} \styleIMI{(} \nt{state\_predicate} \styleIMI{,} \nt{hyper\_rectangle} \nt{step\_opt} \styleIMI{)}    \\
 
 	% PTG
-	$|$ & \styleIMI{Win(} \nt{state\_predicate} \styleIMI{)}    																\\ 
+	$|$ & \styleIMI{Win(} \nt{state\_predicate} \styleIMI{)}    																\\
 
 	% Observer pattern
 	$|$ & \styleIMI{pattern(} \nt{pattern} \styleIMI{)}                                                                                                 \\

src/lib/ParsingStructure.mli

@@ -445,6 +445,8 @@ type unexpanded_parsed_state_predicate_factor =
 	(* The forall is in this level so we can use it on both sides of `AND` and `OR` *)
 	| Unexpanded_Parsed_forall_simple_predicate of forall_index_data * unexpanded_parsed_simple_predicate
 	| Unexpanded_Parsed_forall_state_predicate of forall_index_data * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_exists_simple_predicate of forall_index_data * unexpanded_parsed_simple_predicate
+	| Unexpanded_Parsed_exists_state_predicate of forall_index_data * unexpanded_parsed_state_predicate
 
 and unexpanded_parsed_state_predicate_term =
 	| Unexpanded_Parsed_state_predicate_term_AND of unexpanded_parsed_state_predicate_term * unexpanded_parsed_state_predicate_term

src/lib/PropertyLexer.mll

@@ -98,6 +98,7 @@ rule token = parse
 	| "before"         { CT_BEFORE }
  	| "eventually"     { CT_EVENTUALLY }
  	| "everytime"      { CT_EVERYTIME }
+	| "exists"         { CT_EXISTS }
 	| "False"          { CT_FALSE }
 	| "forall"         { CT_FORALL }
  	| "happened"       { CT_HAPPENED }

src/lib/PropertyParser.mly

@@ -59,7 +59,7 @@ let resolve_property l =
 	CT_BCBORDER CT_BCLEARN CT_BCRANDOM CT_BCRANDOMSEQ CT_BCSHUFFLE CT_BEFORE
 	CT_COVERCARTOGRAPHY
 	CT_DEADLOCKFREE
-	CT_E CT_EF CT_EF_timed CT_EFpmax CT_EFpmin CT_EFtmin CT_EG CT_EVENTUALLY CT_EVERYTIME CT_EXEMPLIFY CT_EXHIBIT
+	CT_E CT_EF CT_EF_timed CT_EFpmax CT_EFpmin CT_EFtmin CT_EG CT_EVENTUALLY CT_EVERYTIME CT_EXEMPLIFY CT_EXHIBIT CT_EXISTS
 	CT_FALSE CT_FORALL
 	CT_HAPPENED CT_HAS
 	CT_IF CT_IMCONVEX CT_IMK CT_IMUNION CT_IN CT_INFCYCLE CT_INFCYCLETHROUGH CT_INFINITY CT_IS
@@ -462,6 +462,8 @@ state_predicate_factor:
 	| LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_state_predicate $2 }
 	| forall_common_prefix simple_predicate { Unexpanded_Parsed_forall_simple_predicate ($1, $2) }
 	| forall_common_prefix LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_forall_state_predicate ($1, $3) }
+	| exists_common_prefix simple_predicate { Unexpanded_Parsed_exists_simple_predicate ($1, $2) }
+	| exists_common_prefix LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_exists_state_predicate ($1, $3) }
 
 ;
 
@@ -809,3 +811,9 @@ forall_common_prefix:
   {
     { forall_index_name = $2; forall_lb = $5; forall_ub = $7}
   }
+
+exists_common_prefix:
+  | CT_EXISTS NAME CT_IN LSQBRA arithmetic_expression COMMA arithmetic_expression RSQBRA COLON
+  {
+    { forall_index_name = $2; forall_lb = $5; forall_ub = $7}
+  }

src/lib/Templates.ml

@@ -1,5 +1,6 @@
 open ParsingStructure;;
 open ParsingStructureUtilities;;
+open ImitatorUtilities;;
 
 (* Utilities *)
 
@@ -124,7 +125,10 @@ let indices_from_forall_index_data g_decls forall_index_data =
   let { forall_index_name = _; forall_lb; forall_ub } = forall_index_data in
   let forall_lb_val = eval_parsed_arithmetic_expr g_decls forall_lb |> NumConst.to_bounded_int in
   let forall_ub_val = eval_parsed_arithmetic_expr g_decls forall_ub |> NumConst.to_bounded_int in
-  List.init (forall_ub_val - forall_lb_val + 1) (fun i -> i + forall_lb_val)
+  if forall_ub_val < forall_lb_val then
+    []
+  else
+    List.init (forall_ub_val - forall_lb_val + 1) (fun i -> i + forall_lb_val)
 
 let gen_aux_var_tbl i index_data =
   Hashtbl.of_seq (List.to_seq [(index_data.forall_index_name, Arg_int (NumConst.numconst_of_int i))])
@@ -585,6 +589,7 @@ and instantiate_state_factor (param_map: var_map): unexpanded_parsed_state_predi
   | Unexpanded_Parsed_state_predicate_factor_NOT f -> Unexpanded_Parsed_state_predicate_factor_NOT (instantiate_state_factor param_map f)
   | Unexpanded_Parsed_simple_predicate spred -> Unexpanded_Parsed_simple_predicate (instantiate_simple_predicate param_map spred)
   | Unexpanded_Parsed_state_predicate pred -> Unexpanded_Parsed_state_predicate (instantiate_state_predicate param_map pred)
+  (* TODO: merge next 4 branches *)
   | Unexpanded_Parsed_forall_state_predicate (index_data, pred) ->
       let binded_name = index_data.forall_index_name in
       let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in
@@ -600,15 +605,30 @@ and instantiate_state_factor (param_map: var_map): unexpanded_parsed_state_predi
   | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) ->
       let binded_name = index_data.forall_index_name in
       let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in
-      (* Here we remove the binde to allow the inner forall to rebind it. *)
-      (* This means that if the user had something like `forall i in [0, 1]: (forall i in [0, 1]: (p(i)) && q(i))`, the inner one will be
-         substituted first, and the outer one will substitute only `q(i)` *)
       Hashtbl.remove param_map binded_name;
       let r = Unexpanded_Parsed_forall_simple_predicate (index_data, instantiate_simple_predicate param_map spred) in
       begin match prev_binded_value_opt with
         | Some v -> Hashtbl.add param_map binded_name v; r
         | None -> r
       end
+  | Unexpanded_Parsed_exists_state_predicate (index_data, pred) ->
+      let binded_name = index_data.forall_index_name in
+      let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in
+      Hashtbl.remove param_map binded_name;
+      let r = Unexpanded_Parsed_exists_state_predicate (index_data, instantiate_state_predicate param_map pred) in
+      begin match prev_binded_value_opt with
+        | Some v -> Hashtbl.add param_map binded_name v; r
+        | None -> r
+      end
+  | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) ->
+      let binded_name = index_data.forall_index_name in
+      let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in
+      Hashtbl.remove param_map binded_name;
+      let r = Unexpanded_Parsed_exists_simple_predicate (index_data, instantiate_simple_predicate param_map spred) in
+      begin match prev_binded_value_opt with
+        | Some v -> Hashtbl.add param_map binded_name v; r
+        | None -> r
+      end
 
 let expand_loc_pred (g_decls: variable_declarations): unexpanded_parsed_loc_predicate -> parsed_loc_predicate = function
   | Unexpanded_Parsed_loc_predicate_EQ (aut_name, loc) -> Parsed_loc_predicate_EQ (expand_name_or_access g_decls aut_name, loc)
@@ -632,49 +652,54 @@ and expand_state_term (g_decls: variable_declarations): unexpanded_parsed_state_
   | Unexpanded_Parsed_state_predicate_factor f -> Parsed_state_predicate_factor (expand_state_factor g_decls f)
 
 and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_parsed_state_predicate_factor): parsed_state_predicate_factor =
+  let instantiate_spred_with index_data spred idx =
+    let param_map_idx = gen_aux_var_tbl idx index_data in
+    instantiate_simple_predicate param_map_idx spred |>
+    expand_simple_predicate g_decls
+  in
+  let instantiate_pred_with index_data pred idx =
+    let param_map_idx = gen_aux_var_tbl idx index_data in
+    instantiate_state_predicate param_map_idx pred |>
+    expand_state_predicate g_decls
+  in
+  let apply_fn_in_forall_range index_data fn =
+    let indices = indices_from_forall_index_data g_decls index_data in
+    match List.rev indices with
+      | [] -> print_warning "Trying to expand a forall with an empty range.";
+              Parsed_simple_predicate Parsed_state_predicate_true
+      | i :: is -> fn i is
+  in
+  let apply_fn_in_exists_range index_data fn =
+    let indices = indices_from_forall_index_data g_decls index_data in
+    match List.rev indices with
+      | [] -> print_warning "Trying to expand an exists with an empty range.";
+              Parsed_simple_predicate Parsed_state_predicate_false
+      | i :: is -> fn i is
+  in
   match factor with
-  (* TODO: Refactor the next two branches *)
-  | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> begin
-      let indices = indices_from_forall_index_data g_decls index_data in
-      (* Here we reverse the list to preserve the order of the index after the fold *)
-      match List.rev indices with
-      | [] -> failwith "error or vacuity?"
-      | i :: is ->
-            (* Compute the conjunction of spred instantiated with each idx in (i::is) *)
-            let instantiate_spred_with idx =
-              let param_map_idx = gen_aux_var_tbl idx index_data in
-              instantiate_simple_predicate param_map_idx spred |>
-              expand_simple_predicate g_decls
-            in
-            let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in
-            let spred_i = instantiate_spred_with i in
-            let fold_fun acc idx =
-                let spred_idx = instantiate_spred_with idx in
-                let spred_idx_term = term_of_simple_pred spred_idx in
-                match acc with
-                  | Parsed_state_predicate (Parsed_state_predicate_term t) ->
-                      Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, t)))
-                  | Parsed_simple_predicate p -> (* Only first iteration of fold, after that I know for sure is a term *)
-                      let p_term = term_of_simple_pred p in
-                      Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, p_term)))
-                  | _ -> failwith "[expand_state_factor]: unreachable"
-                in
-            List.fold_left fold_fun (Parsed_simple_predicate spred_i) is
-  end
-  | Unexpanded_Parsed_forall_state_predicate (index_data, pred) -> begin
-      let indices = indices_from_forall_index_data g_decls index_data in
-      match List.rev indices with
-        | [] -> failwith "error or vacuity?"
-        | i :: is ->
-            let instantiate_pred_with idx =
-              let param_map_idx = gen_aux_var_tbl idx index_data in
-              instantiate_state_predicate param_map_idx pred |>
-              expand_state_predicate g_decls
+  | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) ->
+      apply_fn_in_forall_range index_data (fun i is ->
+        (* Compute the conjunction of spred instantiated with each idx in (i::is) *)
+        let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in
+        let spred_i = instantiate_spred_with index_data spred i in
+        let fold_fun acc idx =
+            let spred_idx = instantiate_spred_with index_data spred idx in
+            let spred_idx_term = term_of_simple_pred spred_idx in
+            match acc with
+              | Parsed_state_predicate (Parsed_state_predicate_term t) ->
+                  Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, t)))
+              | Parsed_simple_predicate p -> (* Only first iteration of fold, after that I know for sure is a term *)
+                  let p_term = term_of_simple_pred p in
+                  Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, p_term)))
+              | _ -> failwith "[expand_state_factor]: unreachable"
             in
-            let pred_i = instantiate_pred_with i in
+        List.fold_left fold_fun (Parsed_simple_predicate spred_i) is)
+  | Unexpanded_Parsed_forall_state_predicate (index_data, pred) ->
+      apply_fn_in_forall_range index_data (fun i is ->
+            let pred_i = instantiate_pred_with index_data pred i in
             let term_of_state_pred p = Parsed_state_predicate_factor (Parsed_state_predicate p) in
             let fold_fun acc idx =
-              let pred_idx = instantiate_pred_with idx in
+              let pred_idx = instantiate_pred_with index_data pred idx in
               let pred_idx_term = term_of_state_pred pred_idx in
               match acc with
                 | Parsed_state_predicate (Parsed_state_predicate_term t) ->
@@ -684,8 +709,36 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par
                     Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (pred_idx_term, p_term)))
                 | _ -> failwith "[expand_state_factor]: unreachable"
             in
-            List.fold_left fold_fun (Parsed_state_predicate pred_i) is
-  end
+            List.fold_left fold_fun (Parsed_state_predicate pred_i) is)
+  | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) ->
+      apply_fn_in_exists_range index_data (fun i is ->
+            (* Compute the disjunction of spred instantiated with each idx in (i::is) *)
+            let spred_i = instantiate_spred_with index_data spred i in
+            let state_pred_of_simple_pred p =
+              Parsed_state_predicate_term (Parsed_state_predicate_factor (Parsed_simple_predicate p))
+            in
+            let fold_fun acc idx =
+                let spred_idx = instantiate_spred_with index_data spred idx in
+                let spred_idx_state = state_pred_of_simple_pred spred_idx in
+                match acc with
+                  | Parsed_state_predicate p ->
+                      Parsed_state_predicate (Parsed_state_predicate_OR (spred_idx_state, p))
+                  | Parsed_simple_predicate p ->
+                      let p_state= state_pred_of_simple_pred p in
+                      Parsed_state_predicate (Parsed_state_predicate_OR (spred_idx_state, p_state))
+                  | _ -> failwith "[expand_state_factor]: unreachable"
+                in
+            List.fold_left fold_fun (Parsed_simple_predicate spred_i) is)
+  | Unexpanded_Parsed_exists_state_predicate (index_data, pred) ->
+      apply_fn_in_exists_range index_data (fun i is ->
+            let pred_i = instantiate_pred_with index_data pred i in
+            let fold_fun acc idx =
+              let pred_idx = instantiate_pred_with index_data pred idx in
+              match acc with
+                | Parsed_state_predicate p -> Parsed_state_predicate (Parsed_state_predicate_OR (pred_idx, p))
+                | _ -> failwith "[expand_state_factor]: unreachable"
+            in
+            List.fold_left fold_fun (Parsed_state_predicate pred_i) is)
   | Unexpanded_Parsed_state_predicate_factor_NOT f -> Parsed_state_predicate_factor_NOT (expand_state_factor g_decls f)
   | Unexpanded_Parsed_simple_predicate spred -> Parsed_simple_predicate (expand_simple_predicate g_decls spred)
   | Unexpanded_Parsed_state_predicate pred -> Parsed_state_predicate (expand_state_predicate g_decls pred)

tests/testcases/templates/properties/fischer.imiprop

@@ -5,4 +5,13 @@
 (* property := #synth AGnot(forall i in [0, N - 1]: (forall j in [0, N - 1]: loc[p[i]] <> cs)) *)
 
 (* Works -> True || False is outside of forall *)
-property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False)
+(* property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False) *)
+
+(* Works *)
+(* property := #synth AGnot(exists i in [0, N - 1]: (forall i in [0, N - 1]: loc[p[i]] <> cs) && True || False) *)
+
+(* Works *)
+property := #synth AGnot(True && exists i in [0, N - 1]: (loc[p[i]] = cs && loc[p[i]] <> cs) || False)
+
+(* Empty range raises a warning *)
+(* property := #synth AGnot(True && exists i in [100, N - 1]: (loc[p[i]] = cs && loc[p[i]] <> cs) || False) *)