Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 3b2bd83d

History | View | Annotate | Download (2.47 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

    
15
   This is a modified version that handles reset and automaton
16
*)
17

    
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

    
23
open Horn_backend_common
24
open Horn_backend_printers
25
open Horn_backend_collecting_sem
26

    
27
(*
28
TODO:
29
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows
30

    
31
- gerer le reset --- DONE
32
- reconstruire les rechable states DONE
33
- reintroduire le cex/traces ... DONE
34
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
35
*)
36

    
37
let main_print machines fmt =
38
if !Options.main_node <> "" then
39
  begin
40
    let node = !Options.main_node in
41
    let machine = get_machine machines node in
42
    if !Options.horn_cex then(
43
      cex_computation machines fmt node machine;
44
      get_cex machines fmt node machine)
45
    else (
46
      collecting_semantics machines fmt node machine;
47
      check_prop machines fmt node machine;
48
    )
49
end
50

    
51
let print_type_definitions fmt =
52
  let cpt_type = ref 0 in
53
  Hashtbl.iter (fun typ decl ->
54
    match typ with
55
    | Tydec_const var ->
56
      (match decl.top_decl_desc with
57
      | TypeDef tdef -> (
58
	match tdef.tydef_desc with
59
	| Tydec_enum tl ->
60
	  incr cpt_type;
61
	  fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
62
	    var
63
	    (Utils.fprintf_list ~sep:" " pp_print_string) tl
64
	| _ -> assert false
65
      )
66
      | _ -> assert false
67
      )
68
    | _        -> ()) type_table
69

    
70

    
71
let translate fmt basename prog machines =
72
  (* We print typedef *)
73
  print_type_definitions fmt;
74
  List.iter (print_machine machines fmt) (List.rev machines);
75
  main_print machines fmt
76

    
77
(* Local Variables: *)
78
(* compile-command:"make -C ../.." *)
79
(* End: *)