Commit 7df6d8e0 authored by erwan's avatar erwan
Browse files

Merge branch 'daemon-gui' into 'master'

A new rdbgui4sasa with automatic daemons

See merge request !14
parents 8dbaa1c8 3e2fb322
Pipeline #66598 passed with stages
in 3 minutes and 41 seconds
opam-version: "2.0"
synopsis: "A Graphical User Interface for XXX"
maintainer: "XXX"
description: """
sasa is a *Self-stabilizing Algorithms SimulAtor*. XXX
"""
authors: [ "XXX" ]
license: "CeCILL"
homepage: "https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa"
dev-repo: "https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git"
bug-reports: "https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/issues"
build: [make "build"]
install: [make "install"]
depends: [
"lablgtk3"
"sasa"
]
depexts: [
["graphviz" "emacs" "gnuplot" "zathura"]
]
post-messages: ["The last version can be obtained via (opam repo add) http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository/ "]
(* Time-stamp: <modified the 03/05/2021 (at 16:16) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/05/2021 (at 16:43) by Erwan Jahier> *)
type t =
| Synchronous (* select all actions *)
......@@ -54,7 +54,7 @@ let (synchrone: 'a list list -> 'a list) = fun all ->
XXX this daemon is not fair: it is biased by the degree of nodes.
*)
let (locally_central: 'v pna list list -> 'v pna list) =
let (locally_central_pna: 'v pna list list -> 'v pna list) =
fun all ->
let remove_one_conflict al =
let _a, al = random_list2 al in
......@@ -74,6 +74,27 @@ let (locally_central: 'v pna list list -> 'v pna list) =
let al = distributed all in
remove_conflicts al
(* Somewhat duplicate the previous one. Hard to avoid... *)
let (locally_central: ('v * 'v list) list list -> 'v list) =
fun all ->
let remove_one_conflict al =
let _a, al = random_list2 al in
al
in
let rec remove_conflicts al =
let activated_pids = List.map (fun (pid,_) -> pid) al in
let conflicts, ok = List.partition (fun (_p,nl) ->
List.exists (fun n -> List.mem n activated_pids) nl
) al
in
if conflicts = [] then ok else
let conflicts = remove_one_conflict conflicts in
ok @ (remove_conflicts conflicts)
in
if all = [] then [] else
let al = distributed all in
fst (List.split (remove_conflicts al))
let rec map3 f l1 l2 l3 =
match (l1, l2, l3) with
([], [], []) -> []
......@@ -137,7 +158,7 @@ let (f: bool -> bool -> t -> 'v Process.t list ->
let al = central nall in
get_activate_val al pl, al
| LocallyCentral ->
let al = locally_central nall in
let al = locally_central_pna nall in
get_activate_val al pl, al
| Distributed ->
let al = distributed nall in
......
(* Time-stamp: <modified the 03/05/2021 (at 16:16) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/05/2021 (at 16:42) by Erwan Jahier> *)
type t =
| Synchronous (* select all actions *)
......@@ -49,3 +49,10 @@ val f : bool -> bool -> t -> 'v Process.t list ->
'v Env.t -> 'v pna list list -> bool list list ->
(string -> string -> bool) -> bool list list * 'v pna list
(** Used in gtkgui.ml *)
val central: 'a list list -> 'a list
val distributed: 'a list list -> 'a list
(* pid + its neighbors in input *)
val locally_central: ('v * 'v list) list list -> 'v list
......@@ -23,7 +23,7 @@ depends: [
"dune" { >= "1.11" }
"ocamlgraph"
"lutils"
"rdbg" { >= "1.184" }
"rdbg" { >= "1.190" }
]
depopts: [
"lustre-v6"
......
# Time-stamp: <modified the 09/04/2021 (at 10:48) by Erwan Jahier>
# Time-stamp: <modified the 05/05/2021 (at 13:20) by Erwan Jahier>
# Rules to generate various dot files.
# The DECO_PATTERN variable should be defined
......
# Time-stamp: <modified the 04/05/2021 (at 11:11) by Erwan Jahier>
# Time-stamp: <modified the 06/05/2021 (at 14:39) by Erwan Jahier>
sasa=$(DIR)/bin/sasa -l 100
......@@ -58,11 +58,11 @@ rdbgui-demo: grid10.ml
rdbg-luciole: grid4.ml
echo "" > include.ml
rdbg --luciole -sut "sasa -rif grid4.dot --custom-daemon" --missing-vars-last
rdbg --luciole -sut "sasa -rif grid4.dot --custom-daemon"
rdbgui-luciole: grid4.ml
rdbgui-custd: grid4.ml
echo "" > include.ml
rdbgui4sasa --luciole -sut "sasa -rif grid4.dot --custom-daemon" --missing-vars-last
rdbgui4sasa -sut "sasa -rif grid4.dot --custom-daemon"
rdbg3: ring.ml
......
......@@ -3,7 +3,7 @@
#use "rdbg-cmds.ml";;
#use "sasa-rdbg-cmds.ml";;
#use "include.ml";;
#use "include.ml";;
let _ =
del_hook "print_event";
......
#!/bin/bash
ocamlfind ocamlc str.cma -g -thread -package lablgtk3 -linkpkg gui.ml -o gui
(executables
(names gui )
(flags :standard -w -3-6-7-10-24-26-27-33-35 -no-strict-sequence)
(libraries lablgtk3 str lutils))
(install
(section bin)
(package gui)
(files
(gui.exe as daemongui)
)
)
open GMain
open GdkKeysyms
(* Lance rdbg avec les arguments passés au gui *)
let from_rdbg, to_rdbg =
let quote str = if String.contains str ' ' then ("\""^str^"\"") else str in
let rdbg_cmd = String.concat " " ("rdbg"::(List.tl (List.map quote (Array.to_list Sys.argv)))) in
Unix.open_process rdbg_cmd
let _ = Unix.set_nonblock (Unix.descr_of_in_channel from_rdbg)
(** Lit la sortie d'un processus.
Renvoie None si la fin du flux est atteinte *)
let read_stdout (ic: in_channel): string option =
let buff = Bytes.create 512 in
let res = ref "" in
let cond = ref true in
let eof = ref false in
Unix.sleepf 0.5;
while !cond do
try
let n = Stdlib.input ic buff 0 512 in
res := !res ^ (Bytes.sub_string buff 0 n);
if n < 512 then cond := false;
if n == 0 then eof := true;
with Sys_blocked_io -> cond := false
done;
if !eof then None else Some !res
(* Fonctions pour travailler avec les commandes rdbg *)
type command_state =
| Normal
| Save
let cmd_loop = ref false
let cmd_state = ref Normal
let cmd_output: string option ref = ref None
let read_rdbg_out (): bool =
let res = read_stdout from_rdbg in
match res with
| None ->
if !cmd_state == Save then
cmd_output := Some ""; (* set cmd_output to exit the loop in rdbg_get *)
false
| Some str ->
let str = String.trim str in
if String.length str > 0 then Printf.printf "%s" str;
match !cmd_state with
| Normal -> ();
| Save ->
cmd_output := res;
cmd_state := Normal;
;
true
(** Envoie une commande à rdbg *)
let rdbg (str: string) =
Printf.fprintf to_rdbg "%s\n%!" str;
Printf.printf "%s\n%!" str;
()
(** Envoie une commande à rdbg et récupère son résultat *)
let rdbg_get (cmd: string): string =
cmd_state := Save;
cmd_output := None;
rdbg cmd;
while !cmd_output == None do
(*
Si cmd_loop vaut true c'est qu'il y a une boucle en court qui lit la sortie de rdbg
Sinon, il faut lire la sortie ici.
*)
if not !cmd_loop then ignore(read_rdbg_out ()) else ();
done;
cmd_state := Normal;
match !cmd_output with
| Some str ->
(* supprime le prompt rdbg du résultat *)
Str.global_replace (Str.regexp_string "(rdbg) ") "" str
| None -> assert false
(** Compte le nombre de noeuds *)
let rdbg_count_nodes (): int =
let cmd = " List.length (List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = \"Enab_\") !e.outputs);;" in
let res = rdbg_get cmd in
(* rdbg renvoie une réponse qui ressemble à "- : int = 7" *)
(* on prend ce qui est après le '=' *)
let count_str = List.hd (List.tl (String.split_on_char '=' res)) in
int_of_string (String.trim count_str)
(**
Extrait le nom et l'état des noeuds
@return liste de tuples (nom, etat, activable)
*)
let rdbg_nodes_info (): (string * string * bool) list =
(* récupère une liste qui dit si chaque état de chaque noeud est activable/pas activable *)
let cmd = " String.concat \";\" (List.map (fun (n,v) -> Printf.sprintf \"%s=%s\" (String.sub n 5 (String.length n - 5)) (val_to_string string_of_float v)) (List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = \"Enab_\") !e.data));;" in
let res =
let res = rdbg_get cmd in
if not (Str.string_partial_match (Str.regexp "[ \n]*- : string =") res 0) then
(* On recommence si on a obtenu un résultat incohérent (bug suite à la vérification que
!e.data a été chargé) *)
rdbg_get " ;;"
else
res
in
(* rdbg renvoie - : string = "p1_conflict=f;p2_conflict=t" etc. *)
(* "p1" est le nom du noeud, "conflict" le nom de l'état, f=false donc non activable, t=true donc activable *)
let data = String.trim (String.sub res 13 (String.length res - 13)) in
let data = String.trim (Str.global_replace (Str.regexp_string "\"") "" data) in
List.map (fun str ->
let parts = String.split_on_char '=' str in
match parts with
| a::b::[] ->
(match String.split_on_char '_' a with
| node::state::[] ->
let node_enabled = match b with
| "t" | "true" -> true
| _ -> false
in
(node, state, node_enabled)
| _ ->
Printf.printf "\nERROR: %s" a;
assert false;)
| _ ->
Printf.printf "\nERROR: %s" str;
assert false;
) (String.split_on_char ';' data)
(** Hashtable qui dit pour chaque noeud s'il est activable (càd s'il a un état activable) ou non.
On considère que les états sont mutuellement exclusifs. *)
let rdbg_nodes_enabled () =
let table = Hashtbl.create 8 in
List.iter (fun (node, state, enabled) ->
let prev_enab =
match Hashtbl.find_opt table node with
| None -> false
| Some e -> e
in
Hashtbl.replace table node (prev_enab || enabled)
) (rdbg_nodes_info ());
table
(** Nom de la table utilisée par le hook dans rdbg *)
let hook_hashtbl_name = "daemongui_activate"
(** Met en place le hook *)
let init_rdbg_hook () =
let value = "Hashtbl.create 1" in
let cmd = Printf.sprintf " let %s = %s;;" hook_hashtbl_name value in
assert (String.length (rdbg_get cmd) > 0);
let cmd = Printf.sprintf " let daemongui sl =
let sl = List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = \"Enab_\") sl in
let res = List.map (fun (n,enabled) ->
(* n est de la forme Enab_node_state, enabled est un Data.v *)
let str = String.sub n 5 ((String.length n)-5) in
let node_name = List.hd (String.split_on_char '_' str) in
let to_activate = match Hashtbl.find_opt %s node_name with
| None -> false
| Some x -> x
in
let activate = match enabled with
| B true -> B to_activate
| _ -> B false
in
(str, activate)
) sl in
Some res;;" hook_hashtbl_name in
assert (String.length (rdbg_get cmd) > 0);
let cmd = " rdbg_mv_hook := Some daemongui;;" in
assert (String.length (rdbg_get cmd) > 0);
()
(** Met à jour le hook pour un noeud *)
let update_rdbg_hook node activate =
let cmd = Printf.sprintf " Hashtbl.replace %s \"%s\" %B;;"
hook_hashtbl_name node activate
in
rdbg cmd;
ignore(read_rdbg_out ());
()
(* GTK3 *)
let locale = GtkMain.Main.init ()
let thread = GtkThread.start()
let main () =
let window = GWindow.window ~width:320 ~height:240
~title:"Daemon GUI"
~show:true () in
let vbox = GPack.vbox ~packing:window#add () in
ignore (window#connect#destroy ~callback: (
fun () ->
rdbg "q"; (* quit rdbg, this will stop the readloop below *)
Main.quit () (* terminate gtk *)
));
(* attend le chargement de la session rdbg *)
(* On attend après avoir lancé l'UI pour que l'utilisateur ne s'impatiente pas *)
let rec wait_for_rdbg () =
match read_stdout from_rdbg with
| None -> ();
| Some str ->
Printf.printf "%s%!" str;
let tr = String.trim str in
if not (Str.string_match (Str.regexp ".*\\(rdbg\\).*") tr 0) then wait_for_rdbg ()
in
wait_for_rdbg ();
(* création du rdbg_mv_hook et de tout ce qu'il faut autour *)
init_rdbg_hook ();
(* attend que !e.data soit dispo *)
(*
BUG - la sortie de la commande ci-dessous ne sera visible qu'à la commande suivante,
ce qui décale tout...
Cet assert échoue mais ne devrait pas :
assert (String.length (String.trim (rdbg_get " !e.data;;")) > 0);
*)
rdbg " !e.data;;";
Unix.sleepf 1.5;
ignore(read_rdbg_out ());
(* 1 case par noeud : activer/pas activer *)
(* NB : lablgtk3 ne propose pas le FlowBox (pourtant dispo dans GTK >= 3.12) *)
let container = GPack.hbox ~packing:vbox#add () in
let nodes_table = rdbg_nodes_enabled () in
let nodes_enabled = Hashtbl.to_seq nodes_table in
let n = Hashtbl.length nodes_table in
let checkboxes_map = Hashtbl.create n in
Seq.iter (fun (name, enabled) ->
(* cf. classe toggle_button de lablgtk3 *)
let checkbox = GButton.check_button ~label:name ~packing:container#add () in
(* Quand on coche/décoche, met à jour le rdbg_mv_hook *)
ignore(checkbox#connect#toggled ~callback: (fun () ->
update_rdbg_hook name checkbox#active
));
checkbox#set_sensitive enabled; (* désactive la box si le noeud n'est pas activable *)
checkbox#set_active false; (* décoche la case *)
Hashtbl.add checkboxes_map name checkbox
) nodes_enabled;
let update_checkbox node enabled =
let checkbox = Hashtbl.find checkboxes_map node in
checkbox#set_sensitive enabled
in
(* Affichage d'informations *)
let scrolled = GBin.scrolled_window ~border_width:10
~shadow_type:`OUT ~height:250 ~packing:vbox#add ()
in
let gtext = GText.view ~wrap_mode:`CHAR ~height:50 ~editable:false ~width:50
~packing: scrolled#add () ~cursor_visible:true
in
let gtext_content = ref "Noeuds activables :" in
gtext#buffer#set_text !gtext_content;
let print_gui str =
let txt = Printf.sprintf "%s\n%s" !gtext_content str in
gtext#buffer#set_text txt;
gtext_content := txt;
in
Seq.iter (fun (name, enabled) ->
print_gui (Printf.sprintf "%s : %B" name enabled);
) nodes_enabled;
(* Boutons de contrôle de la simulation *)
let hbox = GPack.hbox ~packing:vbox#add () in
let update_all_checkboxes () =
print_gui "Nouveaux noeuds activables :";
Seq.iter (fun (name, enabled) ->
update_checkbox name enabled;
print_gui (Printf.sprintf "%s : %B" name enabled);
) (Hashtbl.to_seq (rdbg_nodes_enabled ()))
in
let rdbg_btn label cmd =
let btn = GButton.button ~label:label ~packing:hbox#add () in
btn#misc#set_tooltip_text "tooltip";
ignore (btn#connect#clicked ~callback: (
fun () ->
rdbg cmd;
ignore (read_rdbg_out ());
print_gui (Printf.sprintf "> %s" cmd);
update_all_checkboxes ();
)
);
btn
in
let _ = rdbg_btn "<<" "pr" in
let _ = rdbg_btn "<" "bd" in
let _ = rdbg_btn "G" "graph_view" in
let _ = rdbg_btn ">" "sd" in
let _ = rdbg_btn ">>" "nr" in
(* Read rdbg output until rdbg is closed *)
let rec read_stdout_loop () =
if read_rdbg_out () then read_stdout_loop () else ()
in
cmd_loop := true;
read_stdout_loop ()
let () =
(* choix de session *)
ignore (read_rdbg_out ());
ignore (rdbg "\n");
(* lance l'interface graphique *)
main ()
#!/bin/bash
set -e
cd $(dirname "$0")
exe=$(readlink -f ./gui)
./build.sh
cd ../../test/coloring
"$exe" -sut "sasa -custd ring.dot" --missing-vars-last
#"$exe" -sut "sasa ring.dot"
(install
(files sasa-rdbg-cmds.ml dot4sasa.ml)
(files sasa-rdbg-cmds.ml dot4sasa.ml gtkgui.ml)
(section lib)
(package sasa)
)
This diff is collapsed.
......@@ -16,10 +16,10 @@ let _ = Hashtbl.add roundtbl 1 (1,true);;
(**********************************************************************)
(* redefine (more meaningful) step and back-step for sasa *)
let sasa_step e = next_cond e (fun ne -> ne.kind = Ltop)
let sasa_bstep e = rev_cond e (fun ne -> ne.kind = Ltop);;
let s () = e:=sasa_step !e ; emacs_udate !e; store !e.nb;pe();;
let b () = e:=sasa_bstep !e ; emacs_udate !e; store !e.nb;pe();;
let sasa_step e = next_cond e (fun ne -> ne.kind = e.kind)
let sasa_bstep e = rev_cond e (fun ne -> ne.kind = e.kind)
let s () = e:=sasa_step !e ; emacs_udate !e; store !e.nb;pe()
let b () = e:=sasa_bstep !e ; emacs_udate !e; store !e.nb;pe()
let p =
try Topology.read dotfile
......@@ -137,7 +137,10 @@ let update_round_nb e =
| Some (n,_) -> roundnb := n
(* go to next and previous rounds *)
let next_round e = next_cond e round;;
let next_round e =
let ne = next_cond e round in
if ne.kind = e.kind then ne else next e
let nr () = e:=next_round !e; store !e.nb; !dot_view ();;
let pr () =
e:=goto_last_ckpt !e.nb;
......@@ -220,13 +223,18 @@ let goto_next_false_oracle e =
List.mem ("ok", Bool) e.outputs &&
not (vb "ok" e))
let viol () =
let viol_string () =
if args.oracles <> [] then (
e:=goto_next_false_oracle !e; !dot_view ()
e:=goto_next_false_oracle !e; !dot_view (); "An oracle has been violated. Cf the .rif file"
) else (
Printf.printf "No oracle is set.\n%!"
"No oracle is set."
)
;;
let viol () = Printf.printf "%s\n%!" (viol_string ())
let _ = add_doc_entry
"viol" "unit -> unit" "Move forward until the oracle is violated"
"sasa" "sasa-rdbg-cmds.ml"
(**********************************************************************)
(* Move forward until silence *)
......@@ -280,8 +288,16 @@ let _ =
add_doc_entry "nd" "unit -> unit" "go to the next event and update the network" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "bd" "unit -> unit" "go to the previous event and update the network" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "nr" "unit -> unit" "go to the next round and update the network" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "pr" "unit -> unit" "go to the previous round and update the network" "sasa" "sasa-rdbg-cmds.ml"
;;
add_doc_entry "pr" "unit -> unit" "go to the previous round and update the network" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "d_par" "unit -> unit" "cf d (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "ne_par" "unit -> unit" "cf ne (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "tw_par" "unit -> unit" "cf tw (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "ci_par" "unit -> unit" "cf ci (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "fd_par" "unit -> unit" "cf fd (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "sf_par" "unit -> unit" "cf sf (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "pa_par" "unit -> unit" "cf pa (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "os_par" "unit -> unit" "cf os (for topology with a parent field)" "sasa" "sasa-rdbg-cmds.ml";
()
let l () =
l();
......
......@@ -13,7 +13,7 @@
)
)
(install
(files chut_small.svg graph_small.png)
(files chut_small.svg graph_small.png rdbgui.ml)
(section lib)
(package rdbgui4sasa)
)
......
let quote str = if String.contains str ' ' then ("\""^str^"\"") else str
let rdbg_cmd =
String.concat " " ("rdbg"::(List.tl (List.map quote (Array.to_list Sys.argv))))
(* let oc_stdin = Unix.open_process_out rdbg_cmd *)
let ic_stdout, oc_stdin = Unix.open_process rdbg_cmd
(* let ic_stdout, oc_stdin, ic_stderr =
Unix.open_process_full rdbg_cmd (Unix.environment()) *)
let _ =
Unix.set_nonblock (Unix.descr_of_in_channel ic_stdout);
(* Unix.set_nonblock (Unix.descr_of_in_channel ic_stderr) *)
()
(* let p str = Printf.printf "%s\n%!" str *)
let read_stdout ic =
let buff = Bytes.create 256 in
let res = ref "" in
let cond = ref true in
Unix.sleepf 0.5;
while !cond do
try
let n = Stdlib.input ic buff 0 256 in
res := !res ^ (Bytes.sub_string buff 0 n);
if n < 256 then cond := false;