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.
This commit is contained in:
Nicolas Berthier
parent
106b1339ac
commit
8aeab651ce
7 changed files with 1211 additions and 3 deletions
|
|
@ -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) ]
|
||||
|
|
|
|||
|
|
@ -1,2 +1,3 @@
|
|||
<analysis> or <transformations> or <main> or <parsing>:include
|
||||
<sigali>:include
|
||||
<sigali>:include
|
||||
<ctrl-n>:include
|
||||
|
|
|
|||
550
compiler/minils/ctrl-n/ctrlNbac.ml
Normal file
550
compiler/minils/ctrl-n/ctrlNbac.ml
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/> *)
|
||||
(* *)
|
||||
(***********************************************************************)
|
||||
|
||||
(** 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;;
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
266
compiler/minils/ctrl-n/ctrlNbac.mli
Normal file
266
compiler/minils/ctrl-n/ctrlNbac.mli
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/> *)
|
||||
(* *)
|
||||
(***********************************************************************)
|
||||
|
||||
(* 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;;
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
338
compiler/minils/ctrl-n/ctrlNbacGen.ml
Normal file
338
compiler/minils/ctrl-n/ctrlNbacGen.ml
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/> *)
|
||||
(* *)
|
||||
(***********************************************************************)
|
||||
|
||||
(** 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 }
|
||||
34
compiler/minils/ctrl-n/ctrlNbacGen.mli
Normal file
34
compiler/minils/ctrl-n/ctrlNbacGen.mli
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/> *)
|
||||
(* *)
|
||||
(***********************************************************************)
|
||||
|
||||
(* Interface documentation is in `ctrlNbacGen.ml' only. *)
|
||||
(** *)
|
||||
|
||||
val gen: Minils.program -> CtrlNbac.prog * Minils.program
|
||||
|
|
@ -26,13 +26,27 @@
|
|||
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
|
||||
(* *)
|
||||
(***********************************************************************)
|
||||
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 *)
|
||||
|
|
|
|||
Loading…
Reference in a new issue