jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Attractivity property of Controllable-Nbac output; minor refactorings.

Browse source
This commit is contained in:
Nicolas Berthier 2013-11-13 15:35:15 +01:00
parent 216550c0d1
commit ae6a3aac2e
3 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
compiler/minils/ctrl-n/ctrlNbac.ml
View file

@ -157,8 +157,9 @@ type process =
cn_decls: decls; (** all variable specifications *) cn_decls: decls; (** all variable specifications *)
cn_init: bexp; (** initial state specification *) cn_init: bexp; (** initial state specification *)
cn_assertion: bexp; (** assertion on environment *) cn_assertion: bexp; (** assertion on environment *)
cn_invariance: bexp option; (** {e invariance} property to enforce *) cn_invariant: bexp option; (** {e invariance} property to enforce *)
cn_reachability: bexp option; (** {e reachability} property to enforce *) cn_reachable: bexp option; (** {e reachability} property to enforce *)
cn_attractive: bexp option; (** {e attractivity} property to enforce *)
} }
(** A whole controllable-nbac program contains type definitions and (** A whole controllable-nbac program contains type definitions and
@ -176,7 +177,7 @@ type prog =
(** Building variables *) (** Building variables *)
let mk_var s = s let mk_var s = s
(** Prefixing variables with a string. *) (** Prefixing variables with a string *)
let (^~) = Printf.sprintf "%s%s" let (^~) = Printf.sprintf "%s%s"
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
@ -198,15 +199,15 @@ type process_infos =
of various information about [process]. *) of various information about [process]. *)
let gather_info { cn_decls } = let gather_info { cn_decls } =
let empty = VMap.empty in let empty = VMap.empty in
let s, i, c, l, d, f = VMap.fold begin fun v -> function let s, i, c, l, d, f = VMap.fold begin fun v (t, e) -> match e with
| t, NBstate e -> fun (s,i,c,l,d,f) -> (VMap.add v t s,i,c,l, d,VMap.add v e f) | 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) | 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) | 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) | 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 end cn_decls (empty, empty, empty, empty, empty, empty) in
let cl = VMap.bindings c in let cl = VMap.bindings c in
let cl = List.sort (fun (_, (_, a)) (_, (_, b)) -> compare a b) cl 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 *) let cl = List.map (fun (v, (t, _)) -> (v, t)) cl in (* forget rank *)
{ cni_state_vars = s; { cni_state_vars = s;
cni_input_vars = i; cni_input_vars = i;
cni_contr_vars = c; cni_contr_vars' = cl; cni_contr_vars = c; cni_contr_vars' = cl;
@ -529,8 +530,9 @@ module Printer = struct
print_cat fmt "transition" print_trans pi.cni_trans_specs; print_cat fmt "transition" print_trans pi.cni_trans_specs;
print_cat fmt "initial" print_predicate process.cn_init; print_cat fmt "initial" print_predicate process.cn_init;
print_cat fmt "assertion" print_predicate process.cn_assertion; print_cat fmt "assertion" print_predicate process.cn_assertion;
print_cao' fmt "invariant" print_predicate process.cn_invariance; print_cao' fmt "invariant" print_predicate process.cn_invariant;
print_cao' fmt "reachable" print_predicate process.cn_reachability print_cao' fmt "reachable" print_predicate process.cn_reachable;
print_cao' fmt "attractive" print_predicate process.cn_attractive
(** [dumps mk_fmt p] dumps separately each process of program [p] in (** [dumps mk_fmt p] dumps separately each process of program [p] in
formatters produced calling [mk_fmt] with the process's name. The latter formatters produced calling [mk_fmt] with the process's name. The latter

9
compiler/minils/ctrl-n/ctrlNbac.mli
View file

@ -97,10 +97,6 @@ type exp =
| `Nexp of nexp | `Nexp of nexp
] ]
(* type pbexp = [ exp | bexp ] *)
(* type peexp = [ exp | eexp ] *)
(* type pnexp = [ exp | nexp ] *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(** {3 Nodes & Programs} *) (** {3 Nodes & Programs} *)
@ -118,8 +114,9 @@ type process =
cn_decls: decls; cn_decls: decls;
cn_init: bexp; cn_init: bexp;
cn_assertion: bexp; cn_assertion: bexp;
cn_invariance: bexp option; cn_invariant: bexp option;
cn_reachability: bexp option; cn_reachable: bexp option;
cn_attractive: bexp option;
} }
type prog = type prog =
{ {

5
compiler/minils/ctrl-n/ctrlNbacGen.ml
View file

@ -300,8 +300,9 @@ let translate_node typdefs = function
cn_decls = gd.decls; cn_decls = gd.decls;
cn_init = gd.init; cn_init = gd.init;
cn_assertion = mk_or' init_cond gd.assertion; cn_assertion = mk_or' init_cond gd.assertion;
cn_invariance = Some (mk_or' init_cond gd.invariant); cn_invariant = Some (mk_or' init_cond gd.invariant);
cn_reachability = None; cn_reachable = None;
cn_attractive = None;
} in } in
node, Some ctrln_proc node, Some ctrln_proc