Skip to content

Commit

Permalink
Fix trace reconstruction for stateless variables
Browse files Browse the repository at this point in the history 
Commit 9efb635 does not take into account stateless variables can refer to
previous values of stateful variables. Fixes kind2-mc#1007.
  • Loading branch information
@daniel-larraz
daniel-larraz committed Sep 18, 2023
1 parent 0cd2600 commit 299f7c6
Showing 1 changed file with 143 additions and 110 deletions.
253 changes: 143 additions & 110 deletions src/lustre/lustrePath.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -151,86 +151,156 @@ let safe_map_top_and_add instances model model' i state_var =
with Not_found -> () (* No state variable is added to model' *)


let reconstruct_and_add_init
node
let add_init_values
equations_of_init
trans_sys
instances
model'
first_model
to_reconstruct
=
let equations_of_init =
(* Equations must be topologically sorted *)
N.ordered_equations_of_node
node (TransSys.state_vars trans_sys) true
in
equations_of_init |> List.iter (fun ((sv, _), def) ->
if SVS.mem sv to_reconstruct then
(* Value for state variable at step *)
let v =
(* Get expression for initial state *)
E.base_term_of_t Model.path_offset def
(* Map variables in term to top system, but
not fail if they are not available *)
|> (map_term_top ~no_fail:true instances)
(* Evaluate term in model *)
|> Eval.eval_term
(TransSys.uf_defs trans_sys)
first_model
(* Return term *)
|> Eval.term_of_value
in
let var =
Var.mk_state_var_instance sv Model.path_offset
in
(* Add value to [first_model] so that it is available when
evaluating the definition of the next variable *)
Var.VarHashtbl.add first_model var (Model.Term v) ;
SVT.add model' sv [Model.Term v]
if SVS.mem sv to_reconstruct then
(* Value for state variable at step *)
let v =
(* Get expression for initial state *)
E.base_term_of_t Model.path_offset def
(* Map variables in term to top system, but
not fail if they are not available *)
|> (map_term_top ~no_fail:true instances)
(* Evaluate term in model *)
|> Eval.eval_term
(TransSys.uf_defs trans_sys)
first_model
(* Return term *)
|> Eval.term_of_value
in
let var =
Var.mk_state_var_instance sv Model.path_offset
in
(* Add value to [first_model] so that it is available when
evaluating the definition of the next variable *)
Var.VarHashtbl.add first_model var (Model.Term v) ;
match SVT.find_opt model' sv with
| None -> SVT.add model' sv [Model.Term v]
| Some l -> SVT.replace model' sv ((Model.Term v) :: l)
)

let reconstruct_and_add_step
let add_step_values
equations_of_step
trans_sys
instances
model'
curr_model
prev_model
to_reconstruct
=
equations_of_step |> List.iter (fun ((sv, _), def) ->
if SVS.mem sv to_reconstruct then
(* Value for state variable at step *)
let v =
(* Get expression for step state *)
E.cur_term_of_t Model.path_offset def
(* Map variables in term to top system, but
not fail if they are not available *)
|> (map_term_top ~no_fail:true instances)
(* Evaluate expression for step state *)
|> Eval.eval_term
(TransSys.uf_defs trans_sys)
(Model.bump_and_merge Numeral.(~- one) curr_model prev_model)
(* Return term *)
|> Eval.term_of_value
in
let var =
Var.mk_state_var_instance sv Model.path_offset
in
(* Add value to [m] so that it is available when
evaluating the definition of the next variable *)
Var.VarHashtbl.add curr_model var (Model.Term v) ;
match SVT.find_opt model' sv with
| None -> SVT.add model' sv [Model.Term v]
| Some l -> SVT.replace model' sv ((Model.Term v) :: l)
)

let reconstruct_and_add
first_is_init
node
trans_sys
instances
model'
step_models
to_reconstruct
=
let equations_of_step =
let equations_of_init =
(* Equations must be topologically sorted *)
N.ordered_equations_of_node
node (TransSys.state_vars trans_sys) false
node (TransSys.state_vars trans_sys) true
in
step_models |> List.iter (fun m ->
equations_of_step |> List.iter (fun ((sv, _), def) ->
if SVS.mem sv to_reconstruct then
(* Value for state variable at step *)
let v =
(* Get expression for step state *)
E.cur_term_of_t Model.path_offset def
(* Map variables in term to top system, but
not fail if they are not available *)
|> (map_term_top ~no_fail:true instances)
(* Evaluate expression for step state *)
|> Eval.eval_term
(TransSys.uf_defs trans_sys)
m
(* Return term *)
|> Eval.term_of_value
in
let var =
Var.mk_state_var_instance sv Model.path_offset
in
(* Add value to [m] so that it is available when
evaluating the definition of the next variable *)
Var.VarHashtbl.add m var (Model.Term v) ;
match SVT.find_opt model' sv with
| None -> assert false
| Some l -> SVT.replace model' sv ((Model.Term v) :: l)
)
let equations_of_step =
match step_models with
| [] ->
(* Unreachable; [map_top_and_add] handles the case where the path is empty *)
assert false
| [_] when first_is_init -> [] (* We don't use equations_of_step later *)
| _ ->
(* Equations must be topologically sorted *)
N.ordered_equations_of_node
node (TransSys.state_vars trans_sys) false
in
let rec aux = function
| [] ->
(* Unreachable; [map_top_and_add] handles the case where the path is empty *)
assert false

| [first_model] when first_is_init -> (
(* The first model is encoding the initial state *)

(* Reconstruct the values for the variables at the initial step
from their (initial) Lustre expressions *)
add_init_values
equations_of_init trans_sys
instances
model'
first_model
to_reconstruct
)

| [curr_model] -> (
(* The first model represents an arbitrary state *)
let prev_model =
(* We do not know the value of the variables at the previous state, so
we use an empty model *)
Model.create 0
in
add_step_values
equations_of_step
trans_sys
instances
model'
curr_model
prev_model
to_reconstruct
)

| curr_model :: tl ->

(* Reconstruct the rest of values for the variables
from their (step) Lustre expressions *)
add_step_values
equations_of_step
trans_sys
instances
model'
curr_model
(List.hd tl)
to_reconstruct ;

(* Continue reconstruction *)
aux tl
in
aux (List.rev step_models)


(* Get the sequence of values in the top system of each local state variable
(if exists) and add it to [model']. Otherwise, reconstruct the sequence of
values from its definition. *)
Expand Down Expand Up @@ -265,59 +335,22 @@ let map_top_or_reconstruct_and_add
locals
in
if not (SVS.is_empty to_reconstruct) then (
(* Create fresh list of models, one for each step on the path,
that can be modified locally for reconstructing values
of local varibles *)
let step_models = Model.models_of_path model in
let step_models =

(* Is the first model encoding the initial state? *)
if first_is_init then (

(* [map_top_and_add] handles the case where the path is empty.
If we are here, there exists at least one element *)
let first_model = List.hd step_models in

(* Reconstruct the values for the variables at the initial step
from their (initial) Lustre expressions *)
reconstruct_and_add_init
node
trans_sys
instances
model'
first_model
to_reconstruct
;
List.tl step_models
)
else (
(* The first model represents an arbitrary state *)

(* Create an entry in [model'] for uniformity *)
SVS.elements to_reconstruct
|> List.iter (fun sv -> SVT.add model' sv []) ;
step_models
)
let step_models =
(* Create fresh list of models, one for each step on the path,
that can be modified locally for reconstructing values
of local varibles *)
Model.models_of_path model
in
if step_models <> [] then
(* Reconstruct the rest of values for the variables
from their (step) Lustre expressions *)
reconstruct_and_add_step
node
trans_sys
instances
model'
step_models
to_reconstruct
;
(* Reverse list of values for each variable.
[reconstruct_and_add_step] stores the values in reverse. *)
SVS.elements to_reconstruct
|> List.iter (fun sv ->
match SVT.find_opt model' sv with
| None -> assert false
| Some l -> SVT.replace model' sv (List.rev l)
)

reconstruct_and_add
first_is_init
node
trans_sys
instances
model'
step_models
to_reconstruct
)


Expand Down

0 comments on commit 299f7c6

Please sign in to comment.