From 8aeab651cedd563cc62c9b587e94debba1926748 Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Fri, 8 Nov 2013 14:49:18 +0100 Subject: [PATCH] First draft for Controllable-Nbac format generation. - CtrlNbac: new module for internal representation and output code for Controllable-Nbac format; - CtrlNbacGen: translation into Controllable-Nbac of Minils nodes necessitating controller synthesis; the insertion of calls to controllers is not yet done, and the nodes are left unchanged. --- compiler/main/mls2seq.ml | 1 + compiler/minils/_tags | 3 +- compiler/minils/ctrl-n/ctrlNbac.ml | 550 +++++++++++++++++++++++++ compiler/minils/ctrl-n/ctrlNbac.mli | 266 ++++++++++++ compiler/minils/ctrl-n/ctrlNbacGen.ml | 338 +++++++++++++++ compiler/minils/ctrl-n/ctrlNbacGen.mli | 34 ++ compiler/minils/main/mls_compiler.ml | 22 +- 7 files changed, 1211 insertions(+), 3 deletions(-) create mode 100644 compiler/minils/ctrl-n/ctrlNbac.ml create mode 100644 compiler/minils/ctrl-n/ctrlNbac.mli create mode 100644 compiler/minils/ctrl-n/ctrlNbacGen.ml create mode 100644 compiler/minils/ctrl-n/ctrlNbacGen.mli diff --git a/compiler/main/mls2seq.ml b/compiler/main/mls2seq.ml index cc1911b..6e72f6c 100644 --- a/compiler/main/mls2seq.ml +++ b/compiler/main/mls2seq.ml @@ -84,6 +84,7 @@ let targets = mk_target ~load_conf:java_conf "java" (Obc Java_main.program); mk_target ~load_conf:java_conf "java14" (Obc Java14_main.program); mk_target "z3z" (Minils_no_params ignore); + mk_target "ctrl-n" (Minils_no_params ignore); (* NB: `ignore'? *) mk_target "obc" (Obc write_obc_file); mk_target "obc_np" (Obc_no_params write_obc_file); mk_target "epo" (Minils write_object_file) ] diff --git a/compiler/minils/_tags b/compiler/minils/_tags index 7d88cc5..1a78220 100644 --- a/compiler/minils/_tags +++ b/compiler/minils/_tags @@ -1,2 +1,3 @@ or or
or :include -:include \ No newline at end of file +:include +:include diff --git a/compiler/minils/ctrl-n/ctrlNbac.ml b/compiler/minils/ctrl-n/ctrlNbac.ml new file mode 100644 index 0000000..7dd3113 --- /dev/null +++ b/compiler/minils/ctrl-n/ctrlNbac.ml @@ -0,0 +1,550 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* Nicolas Berthier, SUMO, INRIA *) +(* *) +(* Copyright 2013 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see *) +(* *) +(***********************************************************************) + +(** Controllable-Nbac representation and output module + + @author Nicolas Berthier *) + +(* -------------------------------------------------------------------------- *) + +(** Variable names *) +type var = Names.name + +(** Module for variable mappings *) +module VMap = Names.NamesEnv + +(** Module for variable sets *) +module VSet = Names.NamesSet + +(** User-defined type names *) +type typname = Names.name + +(** Enumaration labels *) +type label = string + +(** Enumeration type definition *) +type typdef = + | EnumDef of label list + +(** Collection of enumeration type definitions *) +type typdefs = typdef VMap.t + +(** Numerical types *) +type ntyp = [ `Int | `Real ] + +(** All handled types *) +type typ = [ `Bool | `Enum of typname | ntyp ] + +(* -------------------------------------------------------------------------- *) +(* {3 Expressions} *) + +(** Equivalence relation operators *) +type eqrel = [ `Eq | `Ne ] + +(** Total ordering relation operators *) +type totrel = [ eqrel | `Lt | `Le | `Gt | `Ge ] + +(** Boolean unary operator *) +type buop = [ `Neg ] + +(** Boolean nary operators. [`Excl] denotes {e mutual exclusion} between all its + arguments. *) +type bnop = [ `Conj | `Disj | `Excl ] + +(** Numerical unary operator *) +type nuop = [ `Opp ] + +(** Numerical nary operators *) +type nnop = [ `Add | `Sub | `Mul | `Div ] + +(** Polymorphic conditional operator *) +type ('t, 'b) cond = [ `Ite of 'b * 't * 't ] + +(** Numerical expressions *) +type nexp = + [ + | `Ref of var + | `Int of int + | `Real of float + | `Nuop of nuop * nexp + | `Nnop of nnop * nexp * nexp * nexp list (** (>=2)-ary operations *) + | ('a, bexp) cond + ] as 'a + +(** Enumeration expressions *) +and eexp = + [ + | `Ref of var + | `Enum of label + | ('a, bexp) cond + ] as 'a + +(** Boolean expressions *) +and bexp = + [ + | `Ref of var + | `Bool of bool + | `Buop of buop * bexp + | `Bnop of bnop * bexp * bexp * bexp list (** (>=2)-ary operations *) + | `Bcmp of eqrel * bexp * bexp + | `Ncmp of totrel * nexp * nexp + | `Ecmp of eqrel * eexp * eexp + | `Ein of eexp * label * label list (** at least one label *) + | ('a, bexp) cond + ] as 'a + +(** Untyped expressions *) +type exp = + [ + | `Bexp of bexp + | `Eexp of eexp + | `Nexp of nexp + ] + +(* -------------------------------------------------------------------------- *) +(* {3 Nodes & Programs} *) + +(** Rank of controllable inputs *) +type rank = int + +(** All kinds of variable specifications *) +type var_spec = + | NBstate of exp (** state variables define the transition function *) + | NBinput (** input *) + | NBcontr of rank (** controllables have a {e unique} rank (not checked) *) + | NBlocal of exp (** local definitions *) + +(** Variable declarations combine a type with a specification. Note that the + conformance between the declared type and any expression in the + specification is not checked. *) +type var_decl = typ * var_spec + +(** Sets of variable declarations. *) +type decls = var_decl VMap.t + +(** Controllable-nbac process (aka: node). Note the initial state specification + may not define all values of the state variables. *) +type process = + { + cn_name: Names.name; (** node name *) + cn_decls: decls; (** all variable specifications *) + cn_init: bexp; (** initial state specification *) + cn_assertion: bexp; (** assertion on environment *) + cn_invariance: bexp option; (** {e invariance} property to enforce *) + cn_reachability: bexp option; (** {e reachability} property to enforce *) + } + +(** A whole controllable-nbac program contains type definitions and + processes. *) +type prog = + { + cnp_name: Names.name; + cnp_typs: typdefs; + cnp_procs: process list; + } + +(* -------------------------------------------------------------------------- *) +(* {2 Utilities} *) + +(** Building variables *) +let mk_var s = s + +(** Prefixing variables with a string. *) +let (^~) = Printf.sprintf "%s%s" + +(* -------------------------------------------------------------------------- *) +(* {3 Gathering process info} *) + +(** Type of data returned by {!gather_info} *) +type process_infos = + { + cni_state_vars: typ VMap.t; (** state variable declarations *) + cni_input_vars: typ VMap.t; (** input variable declarations *) + cni_contr_vars: (typ * rank) VMap.t; (** controllable variable decls *) + cni_contr_vars': (var * typ) list; (** ordered controllable variables *) + cni_local_vars: typ VMap.t; (** local variable declarations *) + cni_local_specs: exp VMap.t; (** local variable definitions *) + cni_trans_specs: exp VMap.t; (** state variable definitions *) + } + +(** [gather_info process] computes data structures suitable for fast retrieval + of various information about [process]. *) +let gather_info { cn_decls } = + let empty = VMap.empty in + let s, i, c, l, d, f = VMap.fold begin fun v -> function + | t, NBstate e -> fun (s,i,c,l,d,f) -> (VMap.add v t s,i,c,l, d,VMap.add v e f) + | t, NBlocal e -> fun (s,i,c,l,d,f) -> (s,i,c,VMap.add v t l, VMap.add v e d,f) + | t, NBinput -> fun (s,i,c,l,d,f) -> (s,VMap.add v t i,c,l, d,f) + | t, NBcontr p -> fun (s,i,c,l,d,f) -> (s,i,VMap.add v (t,p) c,l, d,f) + end cn_decls (empty, empty, empty, empty, empty, empty) in + let cl = VMap.bindings c in + let cl = List.sort (fun (_, (_, a)) (_, (_, b)) -> compare a b) cl in + let cl = List.map (fun (v, (t, _)) -> (v, t)) cl in (* forger rank *) + { cni_state_vars = s; + cni_input_vars = i; + cni_contr_vars = c; cni_contr_vars' = cl; + cni_local_vars = l; + cni_local_specs = d; + cni_trans_specs = f; } + +(* -------------------------------------------------------------------------- *) +(* {3 Building and declaring enumerations} *) + +(** Empty set of type definitions *) +let empty_typdefs: typdefs = VMap.empty + +(** Adds a type definition into the given set. Any type previously defined with + the same name is removed. *) +let declare_typ: typname -> typdef -> typdefs -> typdefs = VMap.add + +(** Builds a type name; enforces compatibility with Nbac format. *) +let mk_typname: Names.name -> typname = String.capitalize + +(** Builds a label; enforces compatibility with Nbac format. *) +let mk_label: Names.name -> label = String.capitalize + +(** Builds an enumeration type definition *) +let mk_etyp: label list -> typdef = fun l -> EnumDef l + +(* -------------------------------------------------------------------------- *) +(* {3 Building expressions} *) + +(** Exception raised when an invalid expression is given to the non-primed + functions bellow. *) +exception TypeError of string + +let as_bexp: exp -> bexp = function + | `Bexp e -> e + | _ -> raise (TypeError "Boolean expression expected!") + +let as_eexp: exp -> eexp = function + | `Eexp e -> e + | _ -> raise (TypeError "Enumeration expression expected!") + +let as_nexp: exp -> nexp = function + | `Nexp e -> e + | _ -> raise (TypeError "Numerical expression expected") + +type bexp' = [ `Bexp of bexp ] +and eexp' = [ `Eexp of eexp ] +and nexp' = [ `Nexp of nexp ] +(** [bexp'], [eexp'] and [nexp'] are alias types for shortening signatures; + recall that a type [[> t]] can be coerced into a larger one without further + annotations ({i e.g.}, the result of [(mk_bref v)] can be used directly as + if it were of type {!exp}). *) + +let mk_bref' v :> bexp = `Ref v +let mk_bcst' c :> bexp = `Bool c + +let mk_neg': bexp -> bexp = function + | `Buop (`Neg, e) -> e + | e -> `Buop (`Neg, e) + +let mk_and': bexp -> bexp -> bexp = + let rec conj leaf a = function + | `Bool true -> a + | `Bool false as b -> b + | `Bnop (`Conj, e, f, l) as b -> (match a with + | `Bnop (`Conj, e', f', l') -> `Bnop (`Conj, e, f, e' :: f' :: l @ l') + | a when leaf -> `Bnop (`Conj, e, f, a :: l) + | a -> conj true b a) + | b when leaf -> `Bnop (`Conj, b, a, []) + | b -> conj true b a + in + conj false + +let mk_or': bexp -> bexp -> bexp = + let rec disj leaf a = function + | `Bool true as b -> b + | `Bool false -> a + | `Bnop (`Disj, e, f, l) as b -> (match a with + | `Bnop (`Disj, e', f', l') -> `Bnop (`Disj, e, f, e' :: f' :: l @ l') + | a when leaf -> `Bnop (`Disj, e, f, a :: l) + | a -> disj true b a) + | b when leaf -> `Bnop (`Disj, b, a, []) + | b -> disj true b a + in + disj false + +let mk_xor': bexp -> bexp -> bexp = fun a b -> `Bnop (`Excl, a, b, []) + +(**/**) + +let _mk_bcmp': eqrel -> bexp -> bexp -> bexp = fun op a b -> match op, a, b with + | `Eq, `Bool true, b | `Ne, `Bool false, b -> b + | `Eq, `Bool false, b | `Ne, `Bool true, b -> mk_neg' b + | `Eq, a, `Bool true | `Ne, a, `Bool false -> a + | `Eq, a, `Bool false | `Ne, a, `Bool true -> mk_neg' a + | op, a, b -> `Bcmp (op, a, b) +let _mk_ecmp': eqrel -> eexp -> eexp -> bexp = fun op a b -> `Ecmp (op, a, b) +let _mk_ncmp': totrel -> nexp -> nexp -> bexp = fun op a b -> `Ncmp (op, a, b) + +let _mk ~bexp ~eexp ~nexp x y = match x, y with + | `Bexp x, `Bexp y -> bexp x y + | `Eexp x, `Eexp y -> eexp x y + | `Nexp x, `Nexp y -> nexp x y + | _ -> raise (TypeError "Type mismatch!") + +let _mk_bnary' a1 an e = function + | [] -> a1 e + | f :: l -> an e f l + +let _mk_bnary filter a1 an e el = + _mk_bnary' a1 an (filter e) (List.rev_map filter el) + +let _mk_nary' filter an e f el = an (filter e) (filter f) (List.map filter el) + +(**/**) + +let mk_conj': bexp -> bexp list -> bexp = _mk_bnary' + (fun e -> e) (fun e f l -> List.fold_left mk_and' (mk_and' e f) l) +let mk_disj': bexp -> bexp list -> bexp = _mk_bnary' + (fun e -> e) (fun e f l -> List.fold_left mk_or' (mk_or' e f) l) +let mk_excl': bexp -> bexp list -> bexp = _mk_bnary' + (fun e -> e) (fun e f l -> `Bnop (`Excl, e, f, l)) + +let mk_ein': eexp -> label -> label list -> bexp = fun e l ll -> `Ein (e, l, ll) + +let mk_beq' = _mk_bcmp' `Eq and mk_eeq' = _mk_ecmp' `Eq +and mk_neq' = _mk_ncmp' `Eq +and mk_bne' = _mk_bcmp' `Ne and mk_ene' = _mk_ecmp' `Ne +and mk_nne' = _mk_ncmp' `Ne +and mk_lt' = _mk_ncmp' `Lt and mk_le' = _mk_ncmp' `Le +and mk_gt' = _mk_ncmp' `Gt and mk_ge' = _mk_ncmp' `Ge + +let mk_eref' v :> eexp = `Ref v +let mk_ecst' l :> eexp = `Enum l + +let mk_nref' v :> nexp = `Ref v +let mk_nicst' i :> nexp = `Int i +let mk_nrcst' f :> nexp = `Real f + +let _mk_nnop': nnop -> nexp -> nexp -> nexp list -> nexp = fun op e f l -> + `Nnop (op, e, f, l) +let mk_add' = _mk_nnop' `Add and mk_sub' = _mk_nnop' `Sub +and mk_mul' = _mk_nnop' `Mul and mk_div' = _mk_nnop' `Div + +(** Conditional operator, to be used with enumeration and numerical + expressions. *) +let mk_cond': bexp -> ([> `Ite of bexp * 'a * 'a ] as 'a) -> 'a -> 'a = function + | `Bool true -> fun t _e -> t + | `Bool false -> fun _t e -> e + | c -> fun t e -> `Ite (c, t, e) + +(** Conditional operator constructor, specialized for Boolean expressions. *) +let mk_bcond': bexp -> bexp -> bexp -> bexp = function + | `Bool true -> fun t _e -> t + | `Bool false -> fun _t e -> e + | c -> fun t e -> match t, e with + | `Bool true, `Bool false -> c + | `Bool false, `Bool true -> mk_neg' c + | t, e -> `Ite (c, t, e) + +(* --- *) + +let mk_bref v :> [> bexp' ] = `Bexp (mk_bref' v) +let mk_bcst c :> [> bexp' ] = `Bexp (mk_bcst' c) + +let mk_neg e : [> bexp' ] = `Bexp (mk_neg' (as_bexp e)) +let mk_and a b : [> bexp' ] = `Bexp (mk_and' (as_bexp a) (as_bexp b)) +let mk_or a b : [> bexp' ] = `Bexp (mk_or' (as_bexp a) (as_bexp b)) +let mk_xor a b : [> bexp' ] = `Bexp (mk_xor' (as_bexp a) (as_bexp b)) + +let mk_conj: exp -> exp list -> [> bexp' ] = _mk_bnary as_bexp + (fun e -> `Bexp e) (fun e f l -> `Bexp (List.fold_left mk_and' (mk_and' e f) l)) +let mk_disj: exp -> exp list -> [> bexp' ] = _mk_bnary as_bexp + (fun e -> `Bexp e) (fun e f l -> `Bexp (List.fold_left mk_or' (mk_or' e f) l)) +let mk_excl: exp -> exp list -> [> bexp' ] = _mk_bnary as_bexp + (fun e -> `Bexp e) (fun e f l -> `Bexp (mk_excl' e (f::l))) + +let mk_ein: exp -> label -> label list -> [> bexp' ] = fun e l ll -> + `Bexp (mk_ein' (as_eexp e) l ll) + +let _mk_cmp: eqrel -> exp -> exp -> [> bexp' ] = fun op -> _mk + ~bexp:(fun a b -> `Bexp (_mk_bcmp' op a b)) + ~eexp:(fun a b -> `Bexp (_mk_ecmp' op a b)) + ~nexp:(fun a b -> `Bexp (_mk_ncmp' (op :> totrel) a b)) +let mk_eq = _mk_cmp `Eq and mk_ne = _mk_cmp `Ne + +let _mk_ncmp: totrel -> exp -> exp -> [> bexp' ] = fun op a b -> + `Bexp (_mk_ncmp' op (as_nexp a) (as_nexp b) :> bexp) +let mk_lt = _mk_ncmp `Lt and mk_le = _mk_ncmp `Le +and mk_gt = _mk_ncmp `Gt and mk_ge = _mk_ncmp `Ge + +(* --- *) + +let mk_eref v : [> eexp' ] = `Eexp (mk_eref' v) +and mk_ecst l : [> eexp' ] = `Eexp (mk_ecst' l) + +let mk_nref v : [> nexp' ] = `Nexp (mk_nref' v) +and mk_nicst i : [> nexp' ] = `Nexp (mk_nicst' i) +and mk_nrcst f : [> nexp' ] = `Nexp (mk_nrcst' f) + +(* --- *) + +let _mk_nnop: nnop -> exp -> exp -> exp list -> [> nexp' ] = fun op -> + _mk_nary' as_nexp (fun e f l -> `Nexp (_mk_nnop' op e f l)) +let mk_add = _mk_nnop `Add and mk_sub = _mk_nnop `Sub +and mk_mul = _mk_nnop `Mul and mk_div = _mk_nnop `Div + +(* --- *) + +let mk_condb: bexp -> exp -> exp -> exp = fun c -> _mk + ~bexp:(fun a b -> `Bexp (mk_bcond' c a b)) + ~eexp:(fun a b -> `Eexp (mk_cond' c a b)) + ~nexp:(fun a b -> `Nexp (mk_cond' c a b)) + +let mk_cond c = mk_condb (as_bexp c) + +(* -------------------------------------------------------------------------- *) +(* {3 Pretty-printing} *) + +(** Module for dumping Controllable-Nbac programs. *) +module Printer = struct + + open Format + + (**/**) + + let peqrel = function + | `Eq -> " = " + | `Ne -> " <> " + let ptotrel = function + | #eqrel as op -> peqrel op + | `Lt -> " < " | `Le -> " <= " + | `Gt -> " > " | `Ge -> " >= " + + let ps = pp_print_string + let pv = ps (* XXX Names.print_name (?) *) + + let pcond pb p' fmt = function + | `Ite (b, e, f) -> + fprintf fmt "(if@ @[%a@]@ then@ @[%a@]@ else@ @[%a@])" pb b p' e p' f + + (** Pretty-printing types. *) + + let print_typ fmt = function + | `Bool -> ps fmt "bool" + | `Int -> ps fmt "int" + | `Real -> ps fmt "real" + | `Enum tn -> ps fmt tn + + let rec pb fmt : bexp -> unit = function + | `Ref v -> pv fmt v + | `Bool b -> fprintf fmt "%b" b + | `Buop (`Neg,`Ref v) -> fprintf fmt "not %a" pv v + | `Buop (`Neg,e) -> fprintf fmt "not (%a)" pb e + | `Bnop (`Conj,e,f,l) -> Pp_tools.print_list_r pb "" " and" "" fmt (e::f::l) + | `Bnop (`Disj,e,f,l) -> Pp_tools.print_list_r pb "(" " or" ")" fmt (e::f::l) + | `Bnop (`Excl,e,f,l) -> Pp_tools.print_list_r pb "#(" "," ")" fmt (e::f::l) + | `Bcmp (cmp,e,f) -> fprintf fmt "(%a%s%a)" pb e (peqrel cmp) pb f + | `Ncmp (cmp,i,j) -> fprintf fmt "(%a%s%a)" pn i (ptotrel cmp) pn j + | `Ecmp (cmp,e,f) -> fprintf fmt "(%a%s%a)" pe e (peqrel cmp) pe f + | `Ein (e, l, l') ->(fprintf fmt "%a in %a" pe e + (Pp_tools.print_list_r pv "{" "," "}") (l::l')) + | #cond as c -> pcond pb pb fmt c + and pe fmt : eexp -> unit = function + | `Ref v -> pv fmt v + | `Enum s -> pv fmt s + | #cond as c -> pcond pb pe fmt c + and pn fmt : nexp -> unit = function + | `Ref v -> pv fmt v + | `Int i -> fprintf fmt "%d" i + | `Real f -> fprintf fmt "%f" f + | `Nuop (`Opp,`Ref v) -> fprintf fmt "- %a" pv v + | `Nuop (`Opp,e) -> fprintf fmt "- (%a)" pn e + | `Nnop (`Add,e,f,l) -> Pp_tools.print_list_r pn "(" " +" ")" fmt (e::f::l) + | `Nnop (`Sub,e,f,l) -> Pp_tools.print_list_r pn "(" " -" ")" fmt (e::f::l) + | `Nnop (`Mul,e,f,l) -> Pp_tools.print_list_r pn "" " *" "" fmt (e::f::l) + | `Nnop (`Div,e,f,l) -> Pp_tools.print_list_r pn "" " /" "" fmt (e::f::l) + | #cond as c -> pcond pb pn fmt c + + (**/**) + + let print_var = pv + + let print_typdef f : typdef -> unit = function + | EnumDef labels -> Pp_tools.print_list ps "{" "," "}" f labels + + let print_typdefs f = VMap.iter (fun tn -> + fprintf f "%s = enum @[%a@];@\n" tn print_typdef) + + let print_bexp = pb + and print_eexp = pe + and print_nexp = pn + and print_exp fmt : exp -> unit = function + | `Bexp b -> pb fmt b + | `Eexp e -> pe fmt e + | `Nexp n -> pn fmt n + + (**/**) + + let print_decls f = VMap.iter (fun v -> fprintf f "%s: %a;@\n" v print_typ) + let print_decll f = List.iter (fun (v,t) -> fprintf f "%s: %a;@\n" v print_typ t) + let print_defs f = VMap.iter (fun v -> fprintf f "%s = @[%a@];@\n" v print_exp) + let print_trans f = VMap.iter (fun v -> fprintf f "%s'= @[%a@];@\n" v print_exp) + let print_predicate f = fprintf f "%a;" pb + + let print_cat f = fprintf f "%s@\n @[%a@]@\n" + let print_cat' f n p m = if not (VMap.is_empty m) then print_cat f n p m + let print_cal' f n p l = if l <> [] then print_cat f n p l + let print_cao' f n p = function | None -> () | Some e -> print_cat f n p e + + (**/**) + + let print_proc fmt process = + let pi = gather_info process in + print_cat fmt "state" print_decls pi.cni_state_vars; + print_cat' fmt "input" print_decls pi.cni_input_vars; + print_cal' fmt "controllable" print_decll pi.cni_contr_vars'; + print_cat' fmt "local" print_decls pi.cni_local_vars; + print_cat' fmt "definition" print_defs pi.cni_local_specs; + print_cat fmt "transition" print_trans pi.cni_trans_specs; + print_cat fmt "initial" print_predicate process.cn_init; + print_cat fmt "assertion" print_predicate process.cn_assertion; + print_cao' fmt "invariant" print_predicate process.cn_invariance; + print_cao' fmt "reachable" print_predicate process.cn_reachability + + (** [dumps mk_fmt p] dumps separately each process of program [p] in + formatters produced calling [mk_fmt] with the process's name. The latter + function returns a couple gathering the formatter and a procedure to + release any attached resources ({i e.g}, to close output channels). *) + let dump mk_fmt { cnp_typs = typs; cnp_procs } = + List.iter begin fun ({ cn_name = name } as proc) -> + let fmt, release = mk_fmt name in + Compiler_utils.print_header_info fmt "(*" "*)"; + print_cat' fmt "typedef" print_typdefs typs; + print_proc fmt proc; + release fmt; + end cnp_procs + +end;; + +(* -------------------------------------------------------------------------- *) diff --git a/compiler/minils/ctrl-n/ctrlNbac.mli b/compiler/minils/ctrl-n/ctrlNbac.mli new file mode 100644 index 0000000..a97714d --- /dev/null +++ b/compiler/minils/ctrl-n/ctrlNbac.mli @@ -0,0 +1,266 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* Nicolas Berthier, SUMO, INRIA *) +(* *) +(* Copyright 2013 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see *) +(* *) +(***********************************************************************) + +(* Interface documentation is in `ctrlNbac.ml' only. *) +(** *) + +(* -------------------------------------------------------------------------- *) +(** {2 Controllable-Nbac Program Specification} *) + +(* -------------------------------------------------------------------------- *) +(** {3 Types} *) + +type typname +type label +type typdef +type typdefs +type ntyp = [ `Int | `Real ] +type typ = [ `Bool | `Enum of typname | ntyp ] + +(* -------------------------------------------------------------------------- *) +(** {3 Variables} *) + +type var +module VMap: Map.S with type key = var +module VSet: Set.S with type elt = var + +(* -------------------------------------------------------------------------- *) +(** {3 Expressions} *) + +type eqrel = [ `Eq | `Ne ] +type totrel = [ eqrel | `Lt | `Le | `Gt | `Ge ] +type buop = [ `Neg ] +type bnop = [ `Conj | `Disj | `Excl ] +type nuop = [ `Opp ] +type nnop = [ `Add | `Sub | `Mul | `Div ] + +type ('t, 'b) cond = [ `Ite of 'b * 't * 't ] + +type nexp = + [ + | `Ref of var + | `Int of int + | `Real of float + | `Nuop of nuop * nexp + | `Nnop of nnop * nexp * nexp * nexp list + | ('a, bexp) cond + ] as 'a +and eexp = + [ + | `Ref of var + | `Enum of label + | ('a, bexp) cond + ] as 'a +and bexp = + [ + | `Ref of var + | `Bool of bool + | `Buop of buop * bexp + | `Bnop of bnop * bexp * bexp * bexp list + | `Bcmp of eqrel * bexp * bexp + | `Ncmp of totrel * nexp * nexp + | `Ecmp of eqrel * eexp * eexp + | `Ein of eexp * label * label list + | ('a, bexp) cond + ] as 'a +type exp = + [ + | `Bexp of bexp + | `Eexp of eexp + | `Nexp of nexp + ] + +(* type pbexp = [ exp | bexp ] *) +(* type peexp = [ exp | eexp ] *) +(* type pnexp = [ exp | nexp ] *) + +(* -------------------------------------------------------------------------- *) +(** {3 Nodes & Programs} *) + +type rank = int +type var_spec = + | NBstate of exp + | NBinput + | NBcontr of rank + | NBlocal of exp +type var_decl = typ * var_spec +type decls = var_decl VMap.t +type process = + { + cn_name: Names.name; + cn_decls: decls; + cn_init: bexp; + cn_assertion: bexp; + cn_invariance: bexp option; + cn_reachability: bexp option; + } +type prog = + { + cnp_name: Names.name; + cnp_typs: typdefs; + cnp_procs: process list; + } + +(* -------------------------------------------------------------------------- *) +(** {2 Utilities} *) + +val mk_var: Names.name -> var +val (^~): string -> var -> var + +(* -------------------------------------------------------------------------- *) +(** {3 Building and declaring enumerations} *) + +val empty_typdefs: typdefs +val declare_typ: typname -> typdef -> typdefs -> typdefs +val mk_typname: Names.name -> typname +val mk_label: Names.name -> label +val mk_etyp: label list -> typdef + +(* -------------------------------------------------------------------------- *) +(** {3 Building expressions} *) + +(** The functions bellow are helpers for building expressions. + + Non-primed functions are given polymorphic expressions ({!exp}) and raise + {!TypeError} exceptions when actual types mismatch; primed versions do not, as + they take arguments of type {!bexp}, {!nexp} or {!eexp} directly. *) + +val mk_bref' : var -> bexp +val mk_bcst' : bool -> bexp +val mk_neg' : bexp -> bexp +val mk_and' : bexp -> bexp -> bexp +val mk_or' : bexp -> bexp -> bexp +val mk_xor' : bexp -> bexp -> bexp +val mk_conj' : bexp -> bexp list -> bexp +val mk_disj' : bexp -> bexp list -> bexp +val mk_excl' : bexp -> bexp list -> bexp +val mk_ein' : eexp -> label -> label list -> bexp +val mk_beq' : bexp -> bexp -> bexp +val mk_eeq' : eexp -> eexp -> bexp +val mk_neq' : nexp -> nexp -> bexp +val mk_bne' : bexp -> bexp -> bexp +val mk_ene' : eexp -> eexp -> bexp +val mk_nne' : nexp -> nexp -> bexp +val mk_lt' : nexp -> nexp -> bexp +val mk_le' : nexp -> nexp -> bexp +val mk_gt' : nexp -> nexp -> bexp +val mk_ge' : nexp -> nexp -> bexp + +val mk_eref' : var -> eexp +val mk_ecst' : label -> eexp + +val mk_nref' : var -> nexp +val mk_nicst' : int -> nexp +val mk_nrcst' : float -> nexp +val mk_add' : nexp -> nexp -> nexp list -> nexp +val mk_sub' : nexp -> nexp -> nexp list -> nexp +val mk_mul' : nexp -> nexp -> nexp list -> nexp +val mk_div' : nexp -> nexp -> nexp list -> nexp + +val mk_cond' : bexp -> ([> `Ite of bexp * 'a * 'a ] as 'a) -> 'a -> 'a +val mk_bcond' : bexp -> bexp -> bexp -> bexp + +(* --- *) + +exception TypeError of string + +val as_bexp: exp -> bexp +val as_eexp: exp -> eexp +val as_nexp: exp -> nexp + +type bexp' = [ `Bexp of bexp ] +and eexp' = [ `Eexp of eexp ] +and nexp' = [ `Nexp of nexp ] + +val mk_bref : var -> [> bexp' ] +val mk_bcst : bool -> [> bexp' ] +val mk_neg : exp -> [> bexp' ] +val mk_and : exp -> exp -> [> bexp' ] +val mk_or : exp -> exp -> [> bexp' ] +val mk_xor : exp -> exp -> [> bexp' ] +val mk_conj : exp -> exp list -> [> bexp' ] +val mk_disj : exp -> exp list -> [> bexp' ] +val mk_excl : exp -> exp list -> [> bexp' ] +val mk_ein : exp -> label -> label list -> [> bexp' ] +val mk_eq : exp -> exp -> [> bexp' ] +val mk_ne : exp -> exp -> [> bexp' ] +val mk_lt : exp -> exp -> [> bexp' ] +val mk_le : exp -> exp -> [> bexp' ] +val mk_gt : exp -> exp -> [> bexp' ] +val mk_ge : exp -> exp -> [> bexp' ] + +val mk_eref : var -> [> eexp' ] +val mk_ecst : label -> [> eexp' ] + +val mk_nref : var -> [> nexp' ] +val mk_nicst : int -> [> nexp' ] +val mk_nrcst : float -> [> nexp' ] +val mk_add : exp -> exp -> exp list -> [> nexp' ] +val mk_sub : exp -> exp -> exp list -> [> nexp' ] +val mk_mul : exp -> exp -> exp list -> [> nexp' ] +val mk_div : exp -> exp -> exp list -> [> nexp' ] + +val mk_cond : exp -> exp -> exp -> exp +val mk_condb : bexp -> exp -> exp -> exp + +(* -------------------------------------------------------------------------- *) +(** {3 Gathering process info} *) + +type process_infos = + { + cni_state_vars: typ VMap.t; + cni_input_vars: typ VMap.t; + cni_contr_vars: (typ * rank) VMap.t; + cni_contr_vars': (var * typ) list; + cni_local_vars: typ VMap.t; + cni_local_specs: exp VMap.t; + cni_trans_specs: exp VMap.t; + } +val gather_info: process -> process_infos + +(* -------------------------------------------------------------------------- *) +(** {3 Pretty-printing} *) + +module Printer: sig + + val print_var : Format.formatter -> var -> unit + val print_typdef : Format.formatter -> typdef -> unit + val print_typdefs : Format.formatter -> typdefs -> unit + val print_bexp : Format.formatter -> bexp -> unit + val print_eexp : Format.formatter -> eexp -> unit + val print_nexp : Format.formatter -> nexp -> unit + val print_exp : Format.formatter -> exp -> unit + val print_proc : Format.formatter -> process -> unit + val dump: (Names.name -> Format.formatter * (Format.formatter -> unit)) -> prog -> + unit + +end;; + +(* -------------------------------------------------------------------------- *) diff --git a/compiler/minils/ctrl-n/ctrlNbacGen.ml b/compiler/minils/ctrl-n/ctrlNbacGen.ml new file mode 100644 index 0000000..fac76da --- /dev/null +++ b/compiler/minils/ctrl-n/ctrlNbacGen.ml @@ -0,0 +1,338 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* Nicolas Berthier, SUMO, INRIA *) +(* *) +(* Copyright 2013 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see *) +(* *) +(***********************************************************************) + +(** Translation from the source language to Controllable-Nbac + + @author Nicolas Berthier *) + +(* -------------------------------------------------------------------------- *) + +open Signature +open Clocks +open Types +open Names +open Idents +open Minils +open CtrlNbac + +let (&) f g = f g + +exception Untranslatable of string (* XXX not catched yet! *) + +(* --- *) + +(** Private record gathering temporary generation data *) +type gen_data = + { + typdefs: typdefs; + decls: decls; + outputs: VSet.t; + init: bexp; + init_cond: bexp; + assertion: bexp; + invariant: bexp; + (* reachable: bexp; *) + } + +(* --- *) + +let tt = mk_bcst' true +let ff = mk_bcst' false +let init_state_var = mk_var "__init__" (* XXX uniqueness? *) +let init_cond = `Ref init_state_var + +let ref_of_typ = function + | `Bool -> mk_bref + | `Enum _ -> mk_eref + | `Int | `Real -> mk_nref + +(* --- *) + +let translate_constr { name } = mk_label name (* XXX use module name (?) *) +let translate_constrs cl = mk_etyp (List.map translate_constr cl) + +(* --- *) + +let translate_typ typ = match Modules.unalias_type typ with + | Tid ({ qual = Pervasives; name = "bool" }) -> `Bool + | Tid ({ qual = Pervasives; name = "int" }) -> `Int + | Tid ({ qual = Pervasives; name = "real" }) -> `Real (* XXX? *) + | Tid ({ name = tn } as t) -> (match Modules.find_type t with + | Tenum _ -> `Enum (mk_typname tn) + | _ -> raise & Untranslatable ("type "^ fullname t)) + | Tprod _ -> raise & Untranslatable ("product type") + | Tarray _ -> raise & Untranslatable ("array type") + | Tinvalid -> failwith "Encountered an invalid type!" + +(* --- *) + +let simplify_static_exp se = (Static.simplify QualEnv.empty se).se_desc + +let translate_static_bexp se = match simplify_static_exp se with + | Sbool true | Sconstructor { qual=Pervasives; name="true" } -> tt + | Sbool false | Sconstructor { qual=Pervasives; name="false" } -> ff + | _ -> failwith ("Boolean static expression expected!") + +let translate_static_eexp se = match simplify_static_exp se with + | Sconstructor { qual=Pervasives; name="true" as n } + | Sconstructor { qual=Pervasives; name="false" as n } -> + failwith ("Enum static expression expected! (found `"^n^"')") + | Sconstructor c -> `Enum (translate_constr c) + | _ -> failwith ("Enum static expression expected!") + +let translate_static_nexp se = match simplify_static_exp se with + | Sint v -> `Int v + | Sfloat v -> `Real v + | Sop ({ qual=Pervasives; name="~-" },[{ se_desc=Sint v }]) -> `Int (-v) + | Sop ({ qual=Pervasives; name="~-." },[{ se_desc=Sfloat v }]) -> `Real (-.v) + | _ -> failwith ("Numerical static expression expected!") + +(* --- *) + +let rec translate_ext_bexp ~pref : _ -> bexp = function + | Wconst se -> translate_static_bexp se + | Wvar id -> `Ref (pref & mk_var & name id) + | Wfield _ -> failwith "TODO Unsupported Boolean `field' expression!" + | Wwhen (ev, _, _) -> translate_ext_bexp ~pref ev.w_desc + | Wreinit _ -> failwith "TODO Unsupported Boolean `reinit' expression!" + +and translate_ext_eexp ~pref : _ -> eexp = function + | Wconst se -> translate_static_eexp se + | Wvar id -> `Ref (pref & mk_var & name id) + | _ -> failwith "TODO Unsupported Enum expression!" + +and translate_ext_nexp ~pref : _ -> nexp = function + | Wconst se -> translate_static_nexp se + | Wvar id -> `Ref (pref & mk_var & name id) + | _ -> failwith "TODO Unsupported Numerical expression!" + +let translate_ext ~pref ext = match translate_typ ext.w_ty with + | `Bool -> `Bexp (translate_ext_bexp ~pref ext.w_desc) + | `Enum _ -> `Eexp (translate_ext_eexp ~pref ext.w_desc) + | `Int | `Real -> `Nexp (translate_ext_nexp ~pref ext.w_desc) + +(* --- *) + +let translate_app ~pref op el = + let pervasives = function + | "not", [e] -> mk_neg e + | "or", e::l -> mk_disj e l + | "&", e::l -> mk_conj e l + | "xor", [e;f] -> mk_xor e f + | "=", [e;f] -> mk_eq e f + | "<>", [e;f] -> mk_ne e f + |("<" | "<."), [e;f] -> mk_lt e f + |("<=" | "<=."), [e;f] -> mk_le e f + |(">" | ">."), [e;f] -> mk_gt e f + |(">=" | ">=."), [e;f] -> mk_ge e f + |("+" | "+."), e::f::l -> mk_add e f l + |("-" | "-."), e::f::l -> mk_sub e f l + |("*" | "*."), e::f::l -> mk_mul e f l + |("/" | "/."), e::f::l -> mk_div e f l + | name, _ -> raise (Untranslatable name) + in + match op, List.map (translate_ext ~pref) el with + | Eequal, [e;f] -> mk_eq e f + | Efun { qual=Pervasives; name }, el -> pervasives (name, el) + | Eifthenelse, [c;t;e] -> mk_cond c t e + | _ -> failwith "Unsupported application!" + +(** [translate_exp gd e] translates the {e memoryless} expression [e] into its + Controllable Nbac representation. *) +let translate_exp ~pref t ({ e_desc = desc; e_ty = ty }) = (* XXX clock? *) + let typ = translate_typ ty in assert (t = typ); match desc with + | Eextvalue ext -> translate_ext ~pref ext + | Eapp ({ a_op }, el, _) -> translate_app ~pref a_op el + | Emerge (v, (_c, e) :: l) -> + let v = pref & mk_var & name v in + List.fold_left + (fun x (c, e) -> mk_cond + (mk_eq (mk_eref v) (mk_ecst (translate_constr c))) + (translate_ext ~pref e) x) + (translate_ext ~pref e) + l + | Ewhen _ -> failwith "TODO Unsupported operation: isolated `when'!" + | Efby _ -> failwith "TODO: translate_exp (fby)" + | Estruct _ -> failwith "TODO: translate_exp (struct)" + | _ -> failwith "TODO: translate_exp" + +(* --- *) + +let rec translate_clk ~pref on off = function + | Cbase | Cvar { contents = Cindex _ } -> on + | Cvar { contents = Clink ck } -> translate_clk ~pref on off ck + | Con (ck, {name = cstr}, v) -> + let v = pref & mk_var & name v in + let c = mk_eq (mk_eref v) (mk_ecst (mk_label cstr)) in + translate_clk ~pref (mk_cond c on off) off ck + +(* --- *) + +let add_state_var gd v typ exp i = + let mk_init = match typ, i with + | _, None -> mk_and' tt + | `Bool, Some i -> mk_and' (mk_beq' (mk_bref' v) (translate_static_bexp i)) + | `Enum _, Some i -> mk_and' (mk_eeq' (mk_eref' v) (translate_static_eexp i)) + | #ntyp, Some i -> mk_and' (mk_neq' (mk_nref' v) (translate_static_nexp i)) + in + { gd with + decls = VMap.add v (typ, NBstate exp) gd.decls; + init = mk_init gd.init; } + +let add_output_var gd v typ exp = add_state_var gd v typ exp None + +let add_local_var gd v typ exp = + { gd with decls = VMap.add v (typ, NBlocal exp) gd.decls; } + +(* --- *) + +let translate_eq ~pref gd ({ eq_lhs = pat; + eq_rhs = { e_desc = exp; e_ty = typ } as rhs; + eq_base_ck = clk }) = + let typ = translate_typ typ in + match pat with + | Evarpat id -> + begin + let v = pref & mk_var & name id in + match exp with + | Efby (init, ev) -> + let ev = translate_ext ~pref ev in + let ev = translate_clk ~pref ev (ref_of_typ typ v) clk in + add_state_var gd v typ ev init + | _ when VSet.mem v gd.outputs -> + add_output_var gd v typ (translate_exp ~pref typ rhs) + | _ -> + add_local_var gd v typ (translate_exp ~pref typ rhs) + end + | Etuplepat _ -> failwith "TODO: Minils.Etuplepat!" + +let translate_eqs ~pref = List.fold_left (translate_eq ~pref) + +(* --- *) + +let prefix_vars ~pref vars = + let vars = List.fold_left + (fun acc { v_ident = id } -> (* XXX "_" only? *) + let v = mk_var & name id in VMap.add v ("_" ^~ v) acc) + VMap.empty vars + in + fun p -> pref (try VMap.find p vars with Not_found -> p) + +(** Contract translation *) +let translate_contract ~pref gd + ({ c_local; c_eq = equs; + c_assume = a; c_enforce = g; + c_assume_loc = a'; c_enforce_loc = g'; + c_controllables = cl }) = + let declare_contr decls { v_ident = id; v_type = typ } i = + let v = mk_var & name id in + VMap.add v (translate_typ typ, NBcontr i) decls in + let declare_contrs decls cl = fst & List.fold_left + (fun (decls, i) c -> (declare_contr decls c i, succ i)) (decls, 0) cl in + + let pref = prefix_vars ~pref c_local in + let gd = { gd with decls = declare_contrs gd.decls cl } in + let gd = translate_eqs ~pref gd equs in + let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a') + and ok = as_bexp & mk_and (translate_ext ~pref g) (translate_ext ~pref g') in + + let gd, ok = + if !Compiler_options.nosink + then (gd, ok) + else let sink = pref & mk_var "_ok_state_flag" in (* XXX uniqueness? *) + let ok = `Bexp (mk_bcond' gd.init_cond tt ok) in + (add_state_var gd sink `Bool ok None, mk_bref' sink) + in + { gd with + assertion = mk_and' gd.assertion ak; + invariant = mk_and' gd.invariant ok; } + +(* --- *) + +(** Node translation. Note the given node is not expored if it does not comprize a + contract. *) +let translate_node typdefs = function + | ({ n_contract = None } as node) -> node, None + | ({ n_name; n_input; n_output; n_equs; n_contract = Some contr } as node) -> + let declare_output om { v_ident = id } = VSet.add (mk_var & name id) om in + let declare_input decls { v_ident = id; v_type = typ } = + VMap.add (mk_var & name id) (translate_typ typ, NBinput) decls in + + let pref p = p in + let outputs = List.fold_left declare_output VSet.empty n_output in + let decls = List.fold_left declare_input VMap.empty n_input in + let decls = VMap.add init_state_var (`Bool, NBstate (`Bexp ff)) decls in + + let gd = { typdefs; decls; outputs; init_cond; init = init_cond; + assertion = tt; invariant = tt; } in + let gd = translate_contract ~pref gd contr in + let gd = translate_eqs ~pref gd n_equs in + + let ctrln_proc = { + cn_name = n_name.name; + cn_decls = gd.decls; + cn_init = gd.init; + cn_assertion = mk_or' init_cond gd.assertion; + cn_invariance = Some (mk_or' init_cond gd.invariant); + cn_reachability = None; + } in + node, Some ctrln_proc + +(* --- *) + +(** [gen p] translates all type definitions, plus the nodes comprizing a + contract, into Controllable-Nbac. + + @return a Controllable-Nbac program comprizing one process for each node + necessitating controller synthesis), (TODO: and a new Minils program, in + which those nodes have been transformed so that they "call" their respective + controller). *) +let gen ({ p_desc = desc } as p) = + (* Highly insprited by Sigalimain.program. *) + + let cnp_typs, procs, descs = + (* XXX Should we gather all the type definitions before translating any + node? *) + List.fold_left begin fun (typdefs, procs, descs) -> function + | Pnode n -> + begin match translate_node typdefs n with + | node, Some proc -> (typdefs, proc :: procs, Pnode node :: descs) + | node, None -> (typdefs, procs, Pnode node :: descs) + end + | Ptype { t_name = { name }; t_desc = Type_enum cl } -> + let tn = mk_typname name and typ = translate_constrs cl in + let typdefs = declare_typ tn typ typdefs in + (typdefs, procs, descs) + | p -> (typdefs, procs, p :: descs) + end (empty_typdefs, [], []) desc + in + let cnp_name = Names.modul_to_string p.p_modname + and cnp_procs = List.rev procs and p_desc = List.rev descs in + { cnp_name; cnp_typs; cnp_procs }, { p with p_desc } diff --git a/compiler/minils/ctrl-n/ctrlNbacGen.mli b/compiler/minils/ctrl-n/ctrlNbacGen.mli new file mode 100644 index 0000000..8bd17a9 --- /dev/null +++ b/compiler/minils/ctrl-n/ctrlNbacGen.mli @@ -0,0 +1,34 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* Nicolas Berthier, SUMO, INRIA *) +(* *) +(* Copyright 2013 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see *) +(* *) +(***********************************************************************) + +(* Interface documentation is in `ctrlNbacGen.ml' only. *) +(** *) + +val gen: Minils.program -> CtrlNbac.prog * Minils.program diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 2e67178..504a05e 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -26,13 +26,27 @@ (* along with Heptagon. If not, see *) (* *) (***********************************************************************) -open Misc -open Location open Compiler_utils open Compiler_options let pp p = if !verbose then Mls_printer.print stdout p +(* NB: I localize file name determination logics for CtrlNbac output into this + module, because its place is not in CtrlNbacGen... *) +(** [gen_n_output_ctrln p] translates the Minils program [p] into + Controllable-Nbac format, and then output its nodes separately in files + under a specific directory; typically, a node ["n"] in file ["f.ept"] is + output into a file called "f_ctrln/n.nbac" *) +let gen_n_output_ctrln p = + let cnp, p = CtrlNbacGen.gen p in + let filename = filename_of_name cnp.CtrlNbac.cnp_name in + let dir = clean_dir (build_path (filename ^"_ctrln")) in + CtrlNbac.Printer.dump begin fun n -> + let oc = open_out (dir ^"/"^ n ^".nbac") in + Format.formatter_of_out_channel oc, (fun _ -> close_out oc) + end cnp; + p + let compile_program p = (* Clocking *) let p = @@ -72,6 +86,10 @@ let compile_program p = pass "Scheduling" true Schedule.program p pp in + let ctrln = List.mem "ctrl-n" !target_languages in + let _p = pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp in + (* NB: XXX _p is ignored for now... *) + let z3z = List.mem "z3z" !target_languages in let p = pass "Sigali generation" z3z Sigalimain.program p pp in (* Re-scheduling after sigali generation *)