Revision 07ceae4c
Added by Pierre-Loïc Garoche almost 6 years ago
| src/backends/Horn/horn_backend_collecting_sem.ml | ||
|---|---|---|
| 41 | 41 |
main_output_dummy |
| 42 | 42 |
in |
| 43 | 43 |
|
| 44 |
(* Special case when the main node is stateless *) |
|
| 45 |
let reset_name, step_name = |
|
| 46 |
if is_stateless machine then |
|
| 47 |
pp_machine_stateless_name, pp_machine_stateless_name |
|
| 48 |
else |
|
| 49 |
pp_machine_reset_name, pp_machine_step_name |
|
| 50 |
in |
|
| 51 |
|
|
| 52 | 44 |
fprintf fmt "(declare-rel MAIN (%a))@." |
| 53 | 45 |
(Utils.fprintf_list ~sep:" " pp_type) |
| 54 | 46 |
(List.map (fun v -> v.var_type) main_memory_next); |
| 55 | 47 |
|
| 56 |
fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
|
| 57 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
| 58 |
fprintf fmt "(rule INIT_STATE)@."; |
|
| 59 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
|
| 60 |
fprintf fmt "INIT_STATE@ "; |
|
| 61 |
fprintf fmt "(@[<v 0>%a %a@])@ " |
|
| 62 |
reset_name node |
|
| 63 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
|
| 64 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
| 65 |
step_name node |
|
| 66 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
|
| 67 |
|
|
| 68 |
fprintf fmt "@]@ )@ "; |
|
| 69 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
|
| 70 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
| 48 |
|
|
| 49 |
(* Init case *) |
|
| 50 |
let _ = |
|
| 51 |
(* Special case when the main node is stateless *) |
|
| 52 |
if is_stateless machine then ( |
|
| 53 |
let step_name = pp_machine_stateless_name in |
|
| 54 |
fprintf fmt "; Initial set: One Step(m,x) -- Stateless node! @."; |
|
| 55 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
| 56 |
fprintf fmt "(rule INIT_STATE)@."; |
|
| 57 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
|
| 58 |
fprintf fmt "INIT_STATE@ "; |
|
| 59 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
| 60 |
step_name node |
|
| 61 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
|
| 62 |
fprintf fmt "@]@ )@ "; |
|
| 63 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
|
| 64 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
| 65 |
) |
|
| 66 |
else ( |
|
| 67 |
let reset_name, step_name = |
|
| 68 |
pp_machine_reset_name, pp_machine_step_name |
|
| 69 |
in |
|
| 70 |
fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
|
| 71 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
| 72 |
fprintf fmt "(rule INIT_STATE)@."; |
|
| 73 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
|
| 74 |
fprintf fmt "INIT_STATE@ "; |
|
| 75 |
fprintf fmt "(@[<v 0>%a %a@])@ " |
|
| 76 |
reset_name node |
|
| 77 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
|
| 78 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
| 79 |
step_name node |
|
| 80 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
|
| 81 |
|
|
| 82 |
fprintf fmt "@]@ )@ "; |
|
| 83 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
|
| 84 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
| 85 |
) |
|
| 86 |
in |
|
| 71 | 87 |
|
| 88 |
let step_name = |
|
| 89 |
if is_stateless machine then |
|
| 90 |
pp_machine_stateless_name |
|
| 91 |
else |
|
| 92 |
pp_machine_step_name |
|
| 93 |
in |
|
| 94 |
|
|
| 72 | 95 |
fprintf fmt "; Inductive def@."; |
| 73 | 96 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
| 74 | 97 |
fprintf fmt |
Also available in: Unified diff
[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github: https://github.com/coco-team/lustrec/issues/13