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 *)