From 8a354882f7835b2a8c8a639be6b25f0435799650 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 18 Jul 2023 14:47:24 +0200 Subject: [PATCH] Add option for printing the set of viable states --- schemas/kind2-output.json | 3 ++ schemas/kind2-output.xsd | 1 + src/flags.ml | 18 +++++++- src/flags.mli | 3 ++ src/inputSystem.ml | 30 ++++++++++++ src/inputSystem.mli | 3 ++ src/lustre/contractChecker.ml | 86 ++++++++++++++++++++++++++++++++--- src/lustre/lustreExpr.ml | 33 ++++++++++++-- src/lustre/lustreExpr.mli | 18 +++++++- src/lustre/lustreSlicing.ml | 16 ++++--- 10 files changed, 191 insertions(+), 20 deletions(-) diff --git a/schemas/kind2-output.json b/schemas/kind2-output.json index a14135581..456f05042 100644 --- a/schemas/kind2-output.json +++ b/schemas/kind2-output.json @@ -705,6 +705,9 @@ "result": { "enum": ["realizable","unrealizable"] }, + "viableStates": { + "type": "string" + }, "deadlockingTrace": { "$ref": "#/definitions/trace" }, diff --git a/schemas/kind2-output.xsd b/schemas/kind2-output.xsd index 82b02cf35..f52d0b4f2 100644 --- a/schemas/kind2-output.xsd +++ b/schemas/kind2-output.xsd @@ -393,6 +393,7 @@ + diff --git a/src/flags.ml b/src/flags.ml index 052958054..cd77ae1df 100644 --- a/src/flags.ml +++ b/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 + "@[\ + 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 diff --git a/src/flags.mli b/src/flags.mli index fe89b8b7f..5204d242d 100644 --- a/src/flags.mli +++ b/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 diff --git a/src/inputSystem.ml b/src/inputSystem.ml index 1c2260418..c2c1e8dee 100644 --- a/src/inputSystem.ml +++ b/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 = diff --git a/src/inputSystem.mli b/src/inputSystem.mli index 66ed4d434..6a7aa51b5 100644 --- a/src/inputSystem.mli +++ b/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 diff --git a/src/lustre/contractChecker.ml b/src/lustre/contractChecker.ml index 0e98deb26..067f3f38d 100644 --- a/src/lustre/contractChecker.ml +++ b/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 "@[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 "@[%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 "@{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 + "@," + (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 diff --git a/src/lustre/lustreExpr.ml b/src/lustre/lustreExpr.ml index 8c7ddd5b9..911029d03 100644 --- a/src/lustre/lustreExpr.ml +++ b/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 + "@[(%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 "@[(%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 *) diff --git a/src/lustre/lustreExpr.mli b/src/lustre/lustreExpr.mli index 0d2e4bb15..82f2084bc 100644 --- a/src/lustre/lustreExpr.mli +++ b/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} *) diff --git a/src/lustre/lustreSlicing.ml b/src/lustre/lustreSlicing.ml index 3bd3d4ed2..9ce0b9aa2 100644 --- a/src/lustre/lustreSlicing.ml +++ b/src/lustre/lustreSlicing.ml @@ -171,7 +171,7 @@ let rec describe_cycle node accum = function (* Checks if the state variable appears in some accumulator [accum] or if there exists a cycle, then checks that this same variable is also on the cycle. *) -let [@ocaml.warning "-27"] break_cycle accum parents state_var sv inds = +let break_cycle accum parents state_var sv _ = List.exists (fun (sv', _) -> StateVar.equal_state_vars sv sv') accum || List.exists (fun path -> @@ -203,7 +203,7 @@ let add_dep_to_parents sv indgrps parents = (* Strategy for merging dependencies on indexes of array accesses (we keep them all). *) -let [@ocaml.warning "-27"] merge_deps sv oind1 oind2 = match oind1, oind2 with +let merge_deps _ oind1 oind2 = match oind1, oind2 with | Some i1, Some i2 -> Some (i1 @ i2) | Some i, None | None, Some i -> Some i | _ -> None @@ -1137,12 +1137,11 @@ let root_and_leaves_of_impl (* Slice a node to its contracts, starting from contracts, stopping at outputs *) -let [@ocaml.warning "-27"] root_and_leaves_of_contracts +let root_and_leaves_of_contracts is_top roots ({ N.outputs; - N.contract; - N.props } as node) = + N.contract } as node) = (* Slice everything from node *) let node_sliced = @@ -1156,8 +1155,11 @@ let [@ocaml.warning "-27"] root_and_leaves_of_contracts (* Slice starting with contracts *) let node_roots = match roots node false with - | None -> roots_of_contract contract |> SVS.elements - | Some r -> SVS.elements r + | None -> + roots_of_contract ~with_sofar_var:(not is_top) contract + |> SVS.elements + | Some r -> + SVS.elements r in (* Do not consider anything below outputs *)