Merge pull request kind2-mc#997 from daniel-larraz/print-viable-states

Add option for printing the set of viable states

schemas/kind2-output.json

@@ -705,6 +705,9 @@
                 "result": {
                     "enum": ["realizable","unrealizable"]
                 },
+                "viableStates": {
+                    "type": "string"
+                },
                 "deadlockingTrace": {
                     "$ref": "#/definitions/trace"
                 },

schemas/kind2-output.xsd

@@ -393,6 +393,7 @@
     <xs:sequence>
       <xs:element name="Result" type="RealizabilityCheckResult" minOccurs="1" maxOccurs="1"/>
       <xs:element name="Runtime" type="RuntimeType" minOccurs="0" maxOccurs="1"/>
+      <xs:element name="ViableStates" type="xs:string" minOccurs="0" maxOccurs="1"/>
       <xs:element name="DeadlockingTrace" type="TraceInfoType" minOccurs="0" maxOccurs="1"/>
       <xs:element name="ConflictingSet" type="ModelElementSetType" minOccurs="0" maxOccurs="1"/>
     </xs:sequence>

src/flags.ml

@@ -1370,7 +1370,7 @@ module Contracts = struct
 
   let check_contract_is_sat_default = true
   let check_contract_is_sat = ref check_contract_is_sat_default
-let _ = add_spec
+  let _ = add_spec
     "--check_contract_is_sat"
     (bool_arg check_contract_is_sat)
     (fun fmt ->
@@ -1383,6 +1383,22 @@ let _ = add_spec
     )
   let check_contract_is_sat () = !check_contract_is_sat
 
+  let print_viable_states_default = false
+  let print_viable_states = ref print_viable_states_default
+  let _ = add_spec
+    "--print_viable_states"
+    (bool_arg print_viable_states)
+    (fun fmt ->
+      Format.fprintf fmt
+      "@[<v>\
+        Print a lustre-like constraint representing the set of@ \
+        viable states of a realizable contract.@ \
+        Default: %a\
+      @]"
+      fmt_bool print_viable_states_default
+    )
+  let print_viable_states () = !print_viable_states
+
 end
 
 

src/flags.mli

@@ -523,6 +523,9 @@ module Contracts : sig
 
   (** Check whether a unrealizable contract is satisfiable *)
   val check_contract_is_sat : unit -> bool
+
+  (* Print set of viable states as a lustre-like constraint *)
+  val print_viable_states : unit -> bool
 end
 
 

src/inputSystem.ml

@@ -544,6 +544,36 @@ fun sys vars ->
     SVM.empty
 
 
+let call_state_var_to_lustre_reference (type s):
+s t -> StateVar.t list -> string StateVar.StateVarMap.t =
+fun sys vars ->
+SVM.fold
+  (fun sv l acc ->
+    (* If there is more than one alias, the first one is used *)
+    let sv', path = List.hd l in
+    let scope =
+      List.fold_left
+        (fun acc (lid, n, _) ->
+          Format.asprintf "%a[%d]"
+            (LustreIdent.pp_print_ident true) lid n :: acc
+        )
+        []
+        path
+    in
+    match scope with
+    | [] -> acc
+    | _ -> (
+      let var_name = StateVar.name_of_state_var sv' in
+      let full_name =
+        String.concat "." (List.rev (var_name :: scope))
+      in
+      (* Format.printf "%a -> %s@." StateVar.pp_print_state_var sv full_name ; *)
+      SVM.add sv full_name acc
+    )
+  )
+  (reconstruct_lustre_streams sys vars)
+  SVM.empty
+
 let pp_print_term_as_expr
   (type s) (in_sys : s t) sys =
   let var_map =

src/inputSystem.mli

@@ -124,6 +124,9 @@ val reconstruct_lustre_streams :
 val mk_state_var_to_lustre_name_map :
   _ t -> StateVar.t list -> string StateVar.StateVarMap.t
 
+(** Returns a map from call state variables to lustre-like names *)
+val call_state_var_to_lustre_reference :
+  _ t -> StateVar.t list -> string StateVar.StateVarMap.t
 
 val is_lustre_input : _ t -> bool
 

src/lustre/contractChecker.ml

@@ -22,12 +22,14 @@ module ISys = InputSystem
 module TSys = TransSys
 
 module LN = LustreNode
+module LE = LustreExpr
 module LC = LustreContract
 module ME = ModelElement
 module VS = Var.VarSet
 
 module SVS = StateVar.StateVarSet
 module SVM = StateVar.StateVarMap
+module SVT = StateVar.StateVarHashtbl
 module UFM = UfSymbol.UfSymbolMap
 
 
@@ -220,6 +222,51 @@ let compute_unviable_trace_and_core analyze in_sys param sys u_result =
 
 let core_desc = "conflicting constraints"
 
+let pp_print_viable_states in_sys param sys fmt fp =
+  if fp = Term.t_true then
+    Format.fprintf fmt "@[<hov>true@]"
+  else
+    let top_node =
+      match ISys.get_lustre_node in_sys (Analysis.info_of_param param).top with
+      | Some n -> n
+      | None -> assert false
+    in
+
+    let sv_expr_map = LN.get_state_var_expr_map top_node in
+    let oracles = top_node.LN.oracles |> SVS.of_list in
+
+    let some_oracle = not (SVS.is_empty oracles) in
+
+    let sv_ln_map =
+      match top_node.LN.calls with
+      | [] -> SVM.empty
+      | _ -> ISys.call_state_var_to_lustre_reference in_sys (TSys.state_vars sys)
+    in
+
+    let rec pvar fmt sv =
+      match SVM.find_opt sv sv_ln_map with
+      | Some ln -> Format.fprintf fmt "%s" ln
+      | None -> (
+        match SVT.find_opt sv_expr_map sv with
+        | None -> Format.fprintf fmt "%s" (StateVar.name_of_state_var sv)
+        | Some expr -> (
+          let has_oracle =
+            try some_oracle && SVS.mem (LE.var_of_init_expr expr
+                |> Var.state_var_of_state_var_instance) oracles
+            with Invalid_argument _ -> false
+          in
+          let expr =
+            if has_oracle then LE.mk_of_expr (LE.step_expr expr)
+            else expr
+          in
+          Format.fprintf fmt "%a"
+              (LE.pp_print_lustre_expr_pvar false pvar) expr
+        )
+      )
+    in
+    Format.fprintf fmt "@[<hov>%a@]"
+      (LE.pp_print_term_as_expr_pvar false pvar) fp
+
 let pp_print_realizability_result_pt
   analyze in_sys param sys fmt result =
   (* Update time *)
@@ -247,8 +294,12 @@ let pp_print_realizability_result_pt
       Scope.pp_print_scope scope
       (Stat.get_float Stat.analysis_time)
   )
-  | Realizable _ ->
-    print_not_unknown_result Pretty.success_tag
+  | Realizable fp ->
+    print_not_unknown_result Pretty.success_tag ;
+
+    if Flags.Contracts.print_viable_states () then
+      Format.fprintf fmt "@{<b>Viable States@}:@,%a@.@."
+        (pp_print_viable_states in_sys param sys) fp;
 
   | Unrealizable u_res ->
     print_not_unknown_result Pretty.failure_tag ;
@@ -290,8 +341,22 @@ let pp_print_realizability_result_json
   (* Update time *)
   Stat.update_time Stat.total_time ;
   Stat.update_time Stat.analysis_time ;
-  let pp_print_trace_and_core =
+  let pp_print_additional_info =
     match result with
+    | Realizable fp -> (
+      if Flags.Contracts.print_viable_states () then (fun fmt ->
+        let fp_str =
+          Format.asprintf "%a"
+            (pp_print_viable_states in_sys param sys) fp
+          |> Str.global_replace (Str.regexp "\n") " "
+          |> Str.global_replace (Str.regexp "\ \ +") " "
+        in
+        Format.fprintf
+          fmt
+          ",@,\"viableStates\" : \"%s\"" fp_str
+      )
+      else (fun _ -> ())
+    )
     | Unrealizable u_res -> (
       if Flags.Contracts.print_deadlock () then (
         let trace, core =
@@ -330,7 +395,7 @@ let pp_print_realizability_result_json
   "
   (Stat.get_float Stat.analysis_time)
   (Realizability.result_to_string result)
-  pp_print_trace_and_core
+  pp_print_additional_info
 
 
 let pp_print_realizability_result_xml
@@ -339,8 +404,17 @@ let pp_print_realizability_result_xml
   (* Update time *)
   Stat.update_time Stat.total_time ;
   Stat.update_time Stat.analysis_time ;
-  let pp_print_trace_and_core =
+  let pp_print_additional_info =
     match result with
+    | Realizable fp -> (
+      if Flags.Contracts.print_viable_states () then (fun fmt ->
+        Format.fprintf
+          fmt
+          "@,<ViableStates><![CDATA[@,%a@,]]></ViableStates>"
+          (pp_print_viable_states in_sys param sys) fp
+      )
+      else (fun _ -> ())
+    )
     | Unrealizable u_res -> (
       if Flags.Contracts.print_deadlock () then (
         let trace, core =
@@ -373,7 +447,7 @@ let pp_print_realizability_result_xml
     tag
     (Stat.get_float Stat.analysis_time)
     (Realizability.result_to_string result)
-    pp_print_trace_and_core
+    pp_print_additional_info
     tag
 
 

src/lustre/lustreExpr.ml

@@ -792,6 +792,23 @@ let pp_print_expr_pvar ?as_type safe pvar ppf expr =
 let pp_print_expr ?as_type safe ppf expr =
   pp_print_expr_pvar ?as_type safe (pp_print_lustre_var safe) ppf expr
 
+let pp_print_lustre_expr_pvar safe pvar ppf = function
+
+  (* Same expression for initial state and following states *)
+  | { expr_init; expr_step; expr_type }
+       when Term.equal expr_init expr_step -> 
+
+    pp_print_expr_pvar ~as_type:expr_type safe pvar ppf expr_step
+
+  (* Print expression of initial state followed by expression for
+     following states *)
+  | { expr_init; expr_step; expr_type } -> 
+
+    Format.fprintf ppf 
+      "@[<hv 1>(%a@ ->@ %a)@]" 
+      (pp_print_expr_pvar ~as_type:expr_type safe pvar) expr_init
+      (pp_print_expr_pvar ~as_type:expr_type safe pvar) expr_step
+
 (* Pretty-print a term as an expr. *)
 let pp_print_term_as_expr = pp_print_expr
 
@@ -820,15 +837,15 @@ let pp_print_lustre_expr safe ppf = function
 
   (* Same expression for initial state and following states *)
   | { expr_init; expr_step; expr_type }
-       when Term.equal expr_init expr_step -> 
+       when Term.equal expr_init expr_step ->
 
     pp_print_expr ~as_type:expr_type safe ppf expr_step
 
   (* Print expression of initial state followed by expression for
      following states *)
-  | { expr_init; expr_step; expr_type } -> 
+  | { expr_init; expr_step; expr_type } ->
 
-    Format.fprintf ppf 
+    Format.fprintf ppf
       "@[<hv 1>(%a@ ->@ %a)@]" 
       (pp_print_expr ~as_type:expr_type safe) expr_init
       (pp_print_expr ~as_type:expr_type safe) expr_step
@@ -1041,7 +1058,11 @@ let var_of_expr { expr_init } =
   (* Fail if any of the above fails *)
   with Invalid_argument _ -> raise (Invalid_argument "var_of_expr")
 
-
+let var_of_init_expr { expr_init } = 
+  try
+    Term.free_var_of_term expr_init
+  (* Fail if any of the above fails *)
+  with Invalid_argument _ -> raise (Invalid_argument "var_of_init_expr")
 
 (* Return all state variables *)
 let state_vars_of_expr { expr_init; expr_step } = 
@@ -1113,6 +1134,10 @@ let split_expr_list list =
     list      
 
 
+let init_expr { expr_init } = expr_init
+
+let step_expr { expr_step } = expr_step 
+
 
 (* ********************************************************************** *)
 (* Generic constructors                                                   *)

src/lustre/lustreExpr.mli

@@ -153,6 +153,11 @@ val pp_print_lustre_expr : bool -> Format.formatter -> t -> unit
     for encoded enumerated datatypes). *)
 val pp_print_expr : ?as_type:Type.t -> bool -> Format.formatter -> expr -> unit
 
+val pp_print_lustre_expr_pvar :
+  bool ->
+  (Format.formatter -> StateVar.t -> unit) ->
+  Format.formatter -> t -> unit
+
 val pp_print_expr_pvar :
   ?as_type:Type.t -> bool ->
   (Format.formatter -> StateVar.t -> unit) ->
@@ -263,12 +268,18 @@ val pre_term_of_t : Numeral.t -> t -> Term.t
     is not a variable at the current or previous offset. *)
 val state_var_of_expr : t -> StateVar.t
 
-(** Return the free variable of a variable 
+(** Return the free variable of a expresion 
 
     Fail with [Invalid_argument "var_of_expr"] if the expression
     is not a free variable. *)
 val var_of_expr : t -> Var.t
-
+
+(** Return the free variable of the initial state expression 
+
+    Fail with [Invalid_argument "var_of_init_expr"] if the initial state expression
+    is not a free variable. *)
+val var_of_init_expr : t -> Var.t
+
 (** Return all state variables occurring in the expression in a set *)
 val state_vars_of_expr : t -> StateVar.StateVarSet.t
 
@@ -291,6 +302,9 @@ val indexes_of_state_vars_in_step : StateVar.t -> t -> expr list list
     respectively *)
 val split_expr_list : t list -> expr list * expr list 
 
+val init_expr : t -> expr
+
+val step_expr : t -> expr
 
 (** {1 Constants} *)