Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
sasa
Commits
f3f31512
Commit
f3f31512
authored
Jun 03, 2021
by
erwan
Browse files
Update: some progress to get time-travel working with rdbgui4sasa
parent
66b73846
Changes
2
Hide whitespace changes
Inline
Side-by-side
tools/rdbg4sasa/gtkgui.ml
View file @
f3f31512
(* Time-stamp: <modified the 3
1
/0
5
/2021 (at 1
1:56
) by Erwan Jahier> *)
(* Time-stamp: <modified the
0
3/0
6
/2021 (at 1
2:02
) by Erwan Jahier> *)
#
thread
#
require
"lablgtk3"
...
...
@@ -117,14 +117,23 @@ let display_event b =
(**********************************************************************************)
(* *)
let
goto_hook_call
()
=
if
custom_mode
then
(
e
:=
next_cond
!
e
(
fun
e
->
e
.
name
=
"mv_hook"
&&
e
.
kind
=
Call
)
)
let
goto_hook_call
e
=
if
custom_mode
then
next_cond
e
(
fun
e
->
e
.
name
=
"mv_hook"
&&
e
.
kind
=
Call
)
else
e
let
goto_hook_exit
e
=
if
custom_mode
then
next_cond
e
(
fun
e
->
e
.
name
=
"mv_hook"
&&
e
.
kind
=
Exit
)
else
e
let
goto_
hook_exit
()
=
let
goto_
top
e
=
if
custom_mode
then
e
:=
next_cond
!
e
(
fun
e
->
e
.
name
=
"mv_hook"
&&
e
.
kind
=
Exit
)
next_cond
e
(
fun
e
->
e
.
kind
=
Ltop
)
else
e
let
init_rdbg_hook
()
=
let
guidaemon
sl
=
...
...
@@ -175,7 +184,7 @@ let init_rdbg_hook () =
let
set_tooltip
b
=
b
#
misc
#
set_tooltip_text
let
custom_daemon
p
gtext
vbox
step_button
round_button
legitimate_button
=
let
custom_daemon
p
gtext
vbox
step_button
back_step_button
round_button
legitimate_button
=
(* création du rdbg_mv_hook et de tout ce qu'il faut autour *)
init_rdbg_hook
()
;
...
...
@@ -200,8 +209,8 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
(* Necessary for salut (to perform a fake step that let sasa provide
the first set of enables) *)
if
args
.
salut_mode
then
goto_hook_exit
()
;
goto_hook_call
()
;
if
args
.
salut_mode
then
e
:=
goto_hook_exit
!
e
;
e
:=
goto_hook_call
!
e
;
blue_add
gtext
#
buffer
(
str_of_sasa_event
false
!
e
);
d
()
;
let
nodes_enabled
=
rdbg_nodes_enabled
!
e
in
...
...
@@ -222,7 +231,6 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
blue
gtext
#
buffer
txt
;
Hashtbl
.
replace
daemongui_activate
node
activate
);
in
(* 1 case par noeud : activer/pas activer *)
...
...
@@ -291,8 +299,8 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
ignore
(
pushbox
#
event
#
connect
#
button_press
~
callback
:
(
fun
_
->
update_rdbg_hook
name
true
;
goto_hook_exit
()
;
goto_hook_call
()
;
e
:=
goto_hook_exit
!
e
;
e
:=
goto_hook_call
!
e
;
display_event
gtext
;
store
!
e
.
nb
;
refresh
()
;
...
...
@@ -348,6 +356,7 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
match
!
daemon_kind
with
|
Manual
->
show
step_button
;
show
checkbox_grid
;
hide
back_step_button
;
hide
legitimate_button
;
(
match
!
oracle_button_ref
with
Some
b
->
hide
b
|
None
->
()
);
hide
round_button
;
hide
pushbox_grid
;
hide
counter_grid
;
...
...
@@ -362,14 +371,17 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
|
ManualCentral
->
hide
legitimate_button
;
(
match
!
oracle_button_ref
with
Some
b
->
hide
b
|
None
->
()
);
hide
step_button
;
hide
round_button
;
hide
checkbox_grid
;
hide
counter_grid
;
(* hide back_step_button; *)
hide
step_button
;
hide
round_button
;
hide
checkbox_grid
;
hide
counter_grid
;
show
pushbox_grid
;
let
pushbox
=
Hashtbl
.
find
pushbox_map
node
in
if
enabled
then
show
pushbox
else
hide
pushbox
;
pushbox
#
set_sensitive
enabled
|
Distributed
|
Synchronous
|
Central
|
LocCentral
->
(
match
!
oracle_button_ref
with
Some
b
->
show
b
|
None
->
()
);
show
step_button
;
show
round_button
;
show
counter_grid
;
show
legitimate_button
;
show
back_step_button
;
show
step_button
;
show
round_button
;
show
counter_grid
;
show
legitimate_button
;
hide
checkbox_grid
;
hide
pushbox_grid
;
in
let
update_all_checkboxes
()
=
...
...
@@ -425,63 +437,57 @@ let custom_daemon p gtext vbox step_button round_button legitimate_button =
in
aux
0
[]
nl
in
let
step
()
=
let
nodes_enabled
=
rdbg_nodes_enabled
!
e
in
let
set_daemongui_tbl
e
=
(* In automatic modes:
- looks who is enabled,
- chooses whom to activate, and
- sets the the tbl shared with the hook function
Should therefore be used at events where the enabled process info is available
*)
let
nodes_enabled
=
rdbg_nodes_enabled
e
in
let
nodes
=
List
.
filter
(
fun
(
_
,
b
)
->
b
)
nodes_enabled
in
let
nodes
=
get_higher_prioriry
nodes
in
(* p ("==> gtkgui: CALL =" ^ (string_of_event
!
e)); *)
(* p ("==> gtkgui: CALL =" ^ (string_of_event e)); *)
(
match
!
daemon_kind
with
|
Distributed
->
(
let
nodes
=
List
.
map
(
fun
x
->
[
x
])
nodes
in
let
to_activate
=
Daemon
.
distributed
nodes
in
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Hashtbl
.
replace
daemongui_activate
n
true
)
to_activate
;
goto_hook_exit
()
;
goto_hook_call
()
;
)
|
Synchronous
->
(
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Hashtbl
.
replace
daemongui_activate
n
true
)
nodes
;
goto_hook_exit
()
;
goto_hook_call
()
;
)
|
Central
->
(
let
nodes
=
List
.
map
(
fun
x
->
[
x
])
nodes
in
let
to_activate
=
Daemon
.
central
nodes
in
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Printf
.
printf
"Activating %s
\n
"
n
;
Hashtbl
.
replace
daemongui_activate
n
true
)
to_activate
;
goto_hook_exit
()
;
goto_hook_call
()
;
)
|
LocCentral
->
(
let
get_neigbors
x
=
let
succ
=
snd
(
List
.
split
(
topology
.
succ
x
))
in
let
pred
=
topology
.
pred
x
in
let
res
=
List
.
fold_left
(
fun
acc
x
->
if
List
.
mem
x
acc
then
acc
else
x
::
acc
)
succ
pred
in
(* p (Printf.sprintf "voisins(%s)=%s\n" x (String.concat "," res)); *)
res
in
let
nodes
=
List
.
map
(
fun
x
->
[
x
,
get_neigbors
x
])
nodes
in
let
to_activate
=
Daemon
.
locally_central
nodes
in
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Hashtbl
.
replace
daemongui_activate
n
true
)
to_activate
;
goto_hook_exit
()
;
goto_hook_call
()
;
|
Distributed
->
(
let
nodes
=
List
.
map
(
fun
x
->
[
x
])
nodes
in
let
to_activate
=
Daemon
.
distributed
nodes
in
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Hashtbl
.
replace
daemongui_activate
n
true
)
to_activate
)
|
Synchronous
->
(
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Hashtbl
.
replace
daemongui_activate
n
true
)
nodes
)
|
Central
->
(
let
nodes
=
List
.
map
(
fun
x
->
[
x
])
nodes
in
let
to_activate
=
Daemon
.
central
nodes
in
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Printf
.
printf
"Activating %s
\n
"
n
;
Hashtbl
.
replace
daemongui_activate
n
true
)
to_activate
)
|
LocCentral
->
(
let
get_neigbors
x
=
let
succ
=
snd
(
List
.
split
(
topology
.
succ
x
))
in
let
pred
=
topology
.
pred
x
in
let
res
=
List
.
fold_left
(
fun
acc
x
->
if
List
.
mem
x
acc
then
acc
else
x
::
acc
)
succ
pred
in
(* p (Printf.sprintf "voisins(%s)=%s\n" x (String.concat "," res)); *)
res
in
let
nodes
=
List
.
map
(
fun
x
->
[
x
,
get_neigbors
x
])
nodes
in
let
to_activate
=
Daemon
.
locally_central
nodes
in
Hashtbl
.
clear
daemongui_activate
;
List
.
iter
(
fun
n
->
Hashtbl
.
replace
daemongui_activate
n
true
)
to_activate
)
|
ManualCentral
->
()
(* SNO; the step is done in pushbox callbacks *)
|
Manual
->
()
)
|
ManualCentral
->
()
(* SNO; the step is done in pushbox callbacks *)
|
Manual
->
goto_hook_exit
()
;
goto_hook_call
()
;
store
!
e
.
nb
;
);
if
not
args
.
salut_mode
&&
is_silent
!
e
then
(* go to Ltop so that the round number can be updated *)
e
:=
next_cond
!
e
(
fun
e
->
e
.
kind
=
Ltop
);
d
()
in
s
tep
s
et_daemongui_tbl
let
prefix
=
try
...
...
@@ -550,7 +556,6 @@ let main () =
let
back_step_button
=
button
~
use_mnemonic
:
true
~
stock
:
`GO_BACK
~
packing
:
bbox
#
add
()
in
set_tooltip
back_step_button
"Move BACKWARD to the previous STEP"
;
change_label
back_step_button
"Ste_p"
;
ignore
(
back_step_button
#
connect
#
clicked
~
callback
:
(
button_cb
true
true
bd
));
let
step_button
=
button
~
use_mnemonic
:
true
~
packing
:
bbox
#
add
~
stock
:
`GO_FORWARD
()
in
let
back_round_button
=
...
...
@@ -564,19 +569,55 @@ let main () =
"Move FORWARD until a legitimate configuration is reached (silence by default)"
;
let
image
=
GMisc
.
image
~
file
:
(
libui_prefix
^
"/chut_small.svg"
)
()
in
legitimate_button
#
set_image
image
#
coerce
;
let
ze_step
=
let
set_daemongui_tbl
=
if
custom_mode
then
custom_daemon
p
text_out
w
step_button
round_button
legitimate_button
custom_daemon
p
text_out
w
step_button
back_step_button
round_button
legitimate_button
else
s
(* cf sasa-rdbg-cmds.ml *)
in
let
step
()
=
ze_step
()
;
d
()
(
fun
_
->
()
)
in
let
a_gui_step
e
=
(* set the daemongui_tbl and step to the next event where the user
is asked to choose whom to activate *)
if
custom_mode
then
(
set_daemongui_tbl
e
;
let
e
=
goto_hook_exit
e
in
let
e
=
goto_hook_call
e
in
if
not
args
.
salut_mode
&&
is_silent
e
then
(* go to Ltop so that the round number can be updated *)
next_cond
e
(
fun
e
->
e
.
kind
=
Ltop
)
else
e
)
else
let
e
=
sasa_step
e
in
store
e
.
nb
;
print_event
e
;
e
in
let
back_step_gui
()
=
let
lnext
e
=
if
args
.
salut_mode
then
let
e
=
goto_top
e
in
set_daemongui_tbl
e
;
e
else
let
e
=
goto_hook_call
e
in
set_daemongui_tbl
e
;
e
in
let
ne
=
rev_cond_gen
!
e
(
fun
ne
->
ne
.
step
=
!
e
.
step
-
1
)
lnext
in
if
ne
.
kind
<>
!
e
.
kind
||
ne
.
name
<>
!
e
.
name
then
e
:=
next_cond
ne
(
fun
ne
->
ne
.
kind
=
!
e
.
kind
||
ne
.
name
=
!
e
.
name
)
else
e
:=
ne
in
ignore
(
back_step_button
#
connect
#
clicked
~
callback
:
(
button_cb
true
false
back_step_gui
));
let
step
()
=
if
not
(
is_silent
!
e
)
then
(
e
:=
a_gui_step
!
e
;
d
()
)
in
let
rec
legitimate_gui
()
=
ze_step
()
;
if
is_silent
!
e
then
()
else
e
:=
a_gui_step
!
e
;
if
is_legitimate
!
e
||
is_silent
!
e
then
()
else
(
legitimate_gui
()
);
in
(* change_label legitimate_button "Silen_t"; *)
...
...
@@ -588,7 +629,7 @@ let main () =
if
custom_mode
then
legitimate_button
#
misc
#
hide
()
;
(* indeed, in the defaut mode (manual central), it should be hided *)
let
rec
next_round_gui
rn
=
ze_step
()
;
if
is_silent
!
e
then
()
else
e
:=
a_gui_step
!
e
;
if
rn
<
!
roundnb
||
is_silent
!
e
then
()
else
(
next_round_gui
rn
);
in
...
...
@@ -602,8 +643,10 @@ let main () =
button_cb
true
true
(
fun
()
->
if
custom_mode
then
(
next_round_gui
!
roundnb
;
if
custom_mode
&&
!
e
.
name
<>
"mv_hook"
&&
!
e
.
kind
<>
Call
then
goto_hook_call
()
if
custom_mode
&&
!
e
.
name
<>
"mv_hook"
&&
!
e
.
kind
<>
Call
&&
not
(
is_silent
!
e
)
then
e
:=
goto_hook_call
!
e
)
else
nr
()
...
...
@@ -612,7 +655,7 @@ let main () =
set_tooltip
back_round_button
"Move BACKWARD to the previous ROUND"
;
change_label
back_round_button
"Roun_d"
;
ignore
(
back_round_button
#
connect
#
clicked
~
callback
:
(
button_cb
true
true
(
fun
()
->
pr
()
;
pr
()
;
goto_hook_call
()
)));
~
callback
:
(
button_cb
true
true
(
fun
()
->
pr
()
;
pr
()
;
e
:=
goto_hook_call
!
e
)));
let
graph
()
=
...
...
@@ -636,7 +679,7 @@ let main () =
let
oracle_button
=
make_button
`OK
"_Oracle"
"Move FORWARD until an oracle is violated"
(
button_cb_string
(
fun
()
->
let
str
=
viol_string
()
in
goto_hook_call
()
;
d
()
;
store
!
e
.
nb
;
str
))
(
fun
()
->
let
str
=
viol_string
()
in
e
:=
goto_hook_call
!
e
;
d
()
;
store
!
e
.
nb
;
str
))
in
oracle_button
#
misc
#
hide
()
;
(* indeed, in the defaut mode (manual central), it should be hided *)
oracle_button_ref
:=
Some
oracle_button
...
...
@@ -653,8 +696,8 @@ let main () =
(* in this mode, the hook plays first to provide fake values to sasa
but the hook does not need input at this first step
*)
goto_hook_exit
()
;
goto_hook_call
()
;
e
:=
goto_hook_exit
!
e
;
e
:=
goto_hook_call
!
e
;
d
()
))
in
let
_
=
make_button
`REFRESH
"_New Seed"
"Restart from the beginning using a New Seed"
...
...
@@ -670,8 +713,8 @@ let main () =
(* in this mode, the hook plays first to provide fake values to sasa
but the hook does not need input at this first step
*)
goto_hook_exit
()
;
goto_hook_call
()
;
e
:=
goto_hook_exit
!
e
;
e
:=
goto_hook_call
!
e
;
d
()
))
in
let
_
=
make_button
`MEDIA_PLAY
"_Sim2chro"
"Launch sim2chro on the generated data (so far)"
...
...
tools/rdbg4sasa/sasa-rdbg-cmds.ml
View file @
f3f31512
...
...
@@ -8,13 +8,24 @@ open RdbgMain
open
Sasacore
.
Topology
;;
#
use
"dot4sasa.ml"
;;
let
is_silent
e
=
match
List
.
assoc_opt
"silent"
e
.
data
with
|
Some
B
b
->
b
|
_
->
failwith
"The silent value is not available in this event"
let
is_legitimate
e
=
match
List
.
assoc_opt
"legitimate"
e
.
data
with
|
Some
B
b
->
b
|
_
->
failwith
(
"legitimate not available at this event: "
^
(
string_of_event
e
))
(**********************************************************************)
(** Computing rounds *)
let
roundnb
=
ref
(
-
666
)
let
mask
=
ref
[]
(* nodes we look the activation of *)
(* XXX use an array! *)
let
roundtbl
=
Hashtbl
.
create
10
;;
let
roundtbl
=
Hashtbl
.
create
10
;;
(* maps event nb to round + round nb *)
(* let _ = Hashtbl.add roundtbl 1 (1,true);; *)
let
verbose
=
ref
false
...
...
@@ -47,12 +58,14 @@ let enabled pl = (* returns the enabled processes *)
(* called at each event via the time-travel hook *)
let
(
round
:
RdbgEvent
.
t
->
bool
)
=
fun
e
->
match
Hashtbl
.
find_opt
roundtbl
e
.
nb
with
|
Some
(
croundnb
,
round
)
->
|
Some
(
croundnb
,
round
,
cmask
)
->
(* Printf.printf "round tabulated at e.nb %d: croundnb=%d round = %b\n%!" *)
(* e.nb croundnb round; *)
roundnb
:=
croundnb
;
mask
:=
cmask
;
round
|
None
->
if
!
mask
=
[]
&&
is_silent
e
then
false
else
let
round
=
(
(* we check if a round occurs when activated processes are available *)
if
args
.
salut_mode
then
...
...
@@ -91,7 +104,7 @@ let (round : RdbgEvent.t -> bool) = fun e ->
res
in
if
round
then
incr
roundnb
;
Hashtbl
.
add
roundtbl
e
.
nb
(
!
roundnb
,
round
);
Hashtbl
.
add
roundtbl
e
.
nb
(
!
roundnb
,
round
,
!
mask
);
(* Printf.printf "round computed at e.nb %d: croundnb=%d round = %b\n%!"
e.nb !roundnb round; *)
round
...
...
@@ -99,7 +112,7 @@ let (round : RdbgEvent.t -> bool) = fun e ->
let
update_round_nb
e
=
match
Hashtbl
.
find_opt
roundtbl
e
.
nb
with
|
None
->
()
|
Some
(
n
,_
)
->
roundnb
:=
n
|
Some
(
n
,_
,
m
)
->
roundnb
:=
n
;
mask
:=
m
(* go to next round *)
let
next_round
e
=
...
...
@@ -108,8 +121,8 @@ let next_round e =
(**********************************************************************)
(* redefine (more meaningful) step and back-step for sasa *)
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
sasa_step
e
=
next_cond
e
(
fun
ne
->
ne
.
kind
=
e
.
kind
&&
ne
.
name
=
e
.
name
)
let
sasa_bstep
e
=
rev_cond
e
(
fun
ne
->
ne
.
kind
=
e
.
kind
&&
ne
.
name
=
e
.
name
)
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
()
...
...
@@ -168,6 +181,33 @@ let r () =
(* if the first event is not a round, add it as a check_point *)
if
!
ckpt_list
=
[]
then
ckpt_list
:=
[
!
e
];;
(**********************************************************************)
(* Move forward until silence *)
let
goto_silence
e
=
next_cond
e
is_silent
let
silence
()
=
e
:=
goto_silence
!
e
;
!
dot_view
()
;;
let
_
=
add_doc_entry
"silence"
"unit -> unit"
"Move forward until is_silent returns true"
"sasa"
"sasa-rdbg-cmds.ml"
;
add_doc_entry
"is_silent"
"RdbgEvent.t -> bool"
"does the event correspond to a silent configuration? (i.e., no enable node)"
"sasa"
"sasa-rdbg-cmds.ml"
;;
let
goto_legitimate
e
=
next_cond
e
is_legitimate
let
legitimate
()
=
e
:=
goto_legitimate
!
e
;
!
dot_view
()
;;
let
_
=
add_doc_entry
"legitimate"
"unit -> unit"
" Move forward until a legitimate configuration is reached (uses 'silence' by default)"
"sasa"
"sasa-rdbg-cmds.ml"
;
add_doc_entry
"is_legitimate"
"RdbgEvent.t -> bool"
"does the event correspond to a legitimate configuration?"
"sasa"
"sasa-rdbg-cmds.ml"
;;
(**********************************************************************)
(* print_event tuning *)
...
...
@@ -279,42 +319,6 @@ let _ = add_doc_entry
"sasa"
"sasa-rdbg-cmds.ml"
(**********************************************************************)
(* Move forward until silence *)
let
is_silent
e
=
match
List
.
assoc_opt
"silent"
e
.
data
with
|
Some
B
b
->
b
|
_
->
failwith
"The silent value is not available in this event"
let
goto_silence
e
=
next_cond
e
is_silent
let
silence
()
=
e
:=
goto_silence
!
e
;
!
dot_view
()
;;
let
_
=
add_doc_entry
"silence"
"unit -> unit"
"Move forward until is_silent returns true"
"sasa"
"sasa-rdbg-cmds.ml"
;
add_doc_entry
"is_silent"
"RdbgEvent.t -> bool"
"does the event correspond to a silent configuration? (i.e., no enable node)"
"sasa"
"sasa-rdbg-cmds.ml"
;;
let
is_legitimate
e
=
match
List
.
assoc_opt
"legitimate"
e
.
data
with
|
Some
B
b
->
b
|
_
->
failwith
(
"legitimate not available at this event: "
^
(
string_of_event
e
))
let
goto_legitimate
e
=
next_cond
e
is_legitimate
let
legitimate
()
=
e
:=
goto_legitimate
!
e
;
!
dot_view
()
;;
let
_
=
add_doc_entry
"legitimate"
"unit -> unit"
" Move forward until a legitimate configuration is reached (uses 'silence' by default)"
"sasa"
"sasa-rdbg-cmds.ml"
;
add_doc_entry
"is_legitimate"
"RdbgEvent.t -> bool"
"does the event correspond to a legitimate configuration?"
"sasa"
"sasa-rdbg-cmds.ml"
;;
(**********************************************************************)
(* Perform the checkpointing at rounds! *)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment