Commit d599f741 authored by erwan's avatar erwan
Browse files

New: Add a --gen-lustre-oracle-skeleton (-glos) option that generated a Lustre oracle skeleton

Add use it to add an oracle to the BFS
parent 0c654451
Pipeline #26557 canceled with stages
in 4 minutes and 26 seconds
......@@ -6,12 +6,15 @@
(setq auto-mode-alist (cons '("\\.lut$" . lutin-mode) auto-mode-alist))
(setq auto-mode-alist (cons '("\\.lus$" . lustre-mode) auto-mode-alist))
(setq auto-mode-alist (cons '("\\.rif$" . rif-mode) auto-mode-alist))
(setq auto-mode-alist (cons '("\\.ml$" . tuareg-mode) auto-mode-alist))
(autoload 'rif-mode "rif" "" t)
(autoload 'lutin-mode "lutin" "Edition de code lutin" t)
(autoload 'lustre-mode "lustre" "Edition de code lustre" t)
;;(autoload 'tuareg-mode "ocaml" "" t)
(require 'org)
......@@ -35,6 +38,7 @@
(and (not (string= lang "dot")) (not (string= lang "sh"))))
(setq org-confirm-babel-evaluate 'my-org-confirm-babel-evaluate)
; (mapcar #'cdr (org-babel--get-vars params))
(org-babel-do-load-languages
'org-babel-load-languages
......@@ -42,6 +46,7 @@
(ocaml . t)
(dot . t)
(lustre . t)
(lutin . t)
(rif . t)
(sh . t)
)
......
(* Time-stamp: <modified the 21/06/2019 (at 17:25) by Erwan Jahier> *)
(* Time-stamp: <modified the 02/07/2019 (at 17:19) by Erwan> *)
open Sasacore
......@@ -75,3 +75,6 @@ let (register : 's to_register -> unit) =
let card = Register.card
let get_graph_attributes = Register.get_graph_attributes
(* Time-stamp: <modified the 21/06/2019 (at 17:17) by Erwan Jahier> *)
(* Time-stamp: <modified the 02/07/2019 (at 17:16) by Erwan> *)
(** Process programmer API *)
type 's neighbor = {
......@@ -49,3 +49,5 @@ val register : 's to_register -> unit
val card : unit -> int
(* val degree : unit -> int *)
(* val diameter : unit -> int *)
val get_graph_attributes : string -> string
(* Time-stamp: <modified the 21/06/2019 (at 18:21) by Erwan Jahier> *)
(* Time-stamp: <modified the 03/07/2019 (at 10:04) by Erwan Jahier> *)
type 's neighbor = {
state: 's ;
......@@ -21,6 +21,7 @@ type 's internal_tables = {
value_to_string : (string, Obj.t) Hashtbl.t;
value_of_string : (string, Obj.t) Hashtbl.t;
copy_value : (string, Obj.t) Hashtbl.t;
graph_attributes : (string, string) Hashtbl.t;
mutable card : int
}
......@@ -32,6 +33,7 @@ let (tbls:'s internal_tables) = {
value_to_string = Hashtbl.create 1;
value_of_string = Hashtbl.create 1;
copy_value = Hashtbl.create 1;
graph_attributes = Hashtbl.create 1;
card = (-1)
}
......@@ -135,3 +137,12 @@ let (set_card : int -> unit) =
let (to_string : 's -> string) =
fun v ->
(get_value_to_string ()) v
let (get_graph_attributes : string -> string) =
fun str ->
try Hashtbl.find tbls.graph_attributes str
with Not_found ->
failwith (Printf.sprintf "The graph attribute %s does not seem to exist" str)
let (set_graph_attributes : string -> string -> unit) =
Hashtbl.replace tbls.graph_attributes
(* Time-stamp: <modified the 21/06/2019 (at 18:21) by Erwan Jahier> *)
(* Time-stamp: <modified the 03/07/2019 (at 10:03) by Erwan Jahier> *)
type 's neighbor = {
state: 's ;
......@@ -38,5 +38,8 @@ val set_card : int -> unit
val card : unit -> int
(* val degree : unit -> int *)
(* val diameter : unit -> int *)
val get_graph_attributes : string -> string
val set_graph_attributes : string -> string -> unit
val verbose_level: int ref
(* Time-stamp: <modified the 21/06/2019 (at 18:14) by Erwan Jahier> *)
(* Time-stamp: <modified the 03/07/2019 (at 10:09) by Erwan Jahier> *)
open Graph
open Graph.Dot_ast
......@@ -63,7 +63,14 @@ let rec (get_weight: Dot_ast.attr -> int option ) =
| (Ident "weight", Some Number n)::_ -> (try Some (int_of_string n) with _ -> None)
| _::tail -> get_weight tail
| [] -> None
let (do_graph_attr : (Dot_ast.id * Dot_ast.id option) list -> unit) =
fun l ->
let f = function
| id, Some v -> Register.set_graph_attributes (of_id id) (of_id v)
| _, None -> ()
in
List.iter f l
let (do_stmt: bool -> node list -> Dot_ast.stmt -> node list) =
fun directed n stmt ->
......@@ -101,7 +108,7 @@ let (do_stmt: bool -> node list -> Dot_ast.stmt -> node list) =
in
ignore (List.fold_left add_edge node nodes);
n
| Attr_graph _attrs -> n
| Attr_graph attrs -> do_graph_attr (List.flatten attrs); n
| Attr_node _attrs -> n
| Attr_edge _attrs -> n
| Equal (_id1, _id2) -> assert false
......
graph fig4_1 {
graph [diameter=7]
p1 [algo="unison.ml" init="clock=7"]
p2 [algo="unison.ml" init="clock=8"]
......
graph ring7 {
graph [diameter=7]
p1 [algo="unison.ml"]
p2 [algo="unison.ml" ]
p3 [algo="unison.ml"]
......
(* Time-stamp: <modified the 21/06/2019 (at 17:29) by Erwan Jahier> *)
(* Time-stamp: <modified the 03/07/2019 (at 09:54) by Erwan Jahier> *)
open Algo
let m=10 (* max 2 (1+2*diameter ()) *)
(* let m=10 (* max 2 (1+2*diameter ()) *) *)
let diameter = int_of_string (get_graph_attributes "diameter")
let m = max 2 (1+2*diameter)
let (init_state: int -> 'v) =
fun _nl ->
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment