Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lutin
Commits
2926e5a5
Commit
2926e5a5
authored
Apr 30, 2019
by
erwan
Browse files
Fix: a LocalDeadlock was not properly catched from rdbg
parent
421bcc4d
Pipeline
#23493
failed with stages
in 4 minutes and 9 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
ltop/src/runDirect.ml
View file @
2926e5a5
...
...
@@ -248,11 +248,11 @@ let (start : unit -> Event.t) =
(
LustreRun
.
make_luciole
"./lurette_luciole.dro"
luciole_in
luciole_out
)
,
luciole_out
in
(*
let seed =
*)
(*
match args.seed with
*)
(*
| None -> random_seed ()
*)
(*
| Some seed -> seed
*)
(*
in
*)
let
seed
=
match
args
.
seed
with
|
None
->
random_seed
()
|
Some
seed
->
seed
in
let
cov_init
=
(* XXX faut-il renommer les sorties de l'oracle ou raler en
cas de clash ? *)
if
List
.
flatten
oracle_out_l
=
[]
then
NO
else
...
...
lutin/src/lutExe.ml
View file @
2926e5a5
...
...
@@ -562,14 +562,14 @@ let add_to_guard_nc it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info)
g_src
=
if
snd
si
=
[]
then
acc
.
g_src
else
(
snd
si
)
::
acc
.
g_src
}
exception
LocalDeadlock
exception
LocalDeadlock
of
t
(** Add a new constraint to an existing guard *)
let
add_to_guard
it
data
(
e
:
CoAlgExp
.
t
)
(
acc
:
guard
)
(
si
:
CoTraceExp
.
src_info
)
=
(
let
res
=
add_to_guard_nc
it
data
e
acc
si
in
let
it
,
res
,
ok
=
check_satisfiablity
it
res
in
if
ok
then
it
,
res
else
raise
LocalDeadlock
else
raise
(
LocalDeadlock
it
)
)
(** Tries to compute a value in a context *)
...
...
@@ -852,7 +852,8 @@ let rec genpath (t : t) (data : store) (* data env = inputs + pres *)
it
:=
nit
;
MainArg
.
event_incr
!
it
.
arg_opt
;
(* sat ou usat*)
cont
.
doit
(
Goto
(
new_acc
,
TE_eps
))
with
LocalDeadlock
->
with
LocalDeadlock
nit
->
it
:=
nit
;
raise
(
Deadlock
(
MainArg
.
get_event_nb
!
it
.
arg_opt
))
(* n.b. raise Deadlock if impossible *)
)
...
...
@@ -1073,11 +1074,13 @@ let rec genpath (t : t) (data : store) (* data env = inputs + pres *)
let
(
sum
,
cel
)
=
List
.
fold_left
weval
(
0
,
[]
)
wtel
in
try
let
e'
=
match
cel
with
|
[]
->
raise
(
LocalDeadlock
)
|
[]
->
raise
(
LocalDeadlock
!
it
)
|
[(
_
,
e
)]
->
e
|
_
->
TE_dyn_choice
(
sum
,
cel
)
in
rec_genpath
({
br
with
br_ctrl
=
e'
})
with
LocalDeadlock
->
raise
(
Deadlock
(
MainArg
.
get_event_nb
!
it
.
arg_opt
))
with
LocalDeadlock
nit
->
it
:=
nit
;
raise
(
Deadlock
(
MainArg
.
get_event_nb
!
it
.
arg_opt
))
)
(* ad hoc node for dynamic simulation:
weights are evaluated (int), guaranted to be > 0,
...
...
@@ -1118,7 +1121,7 @@ let rec genpath (t : t) (data : store) (* data env = inputs + pres *)
let
(
gw
,
sw
)
=
getweights
cpt
in
try
let
e'
=
(
match
(
gw
,
sw
)
with
|
(
0
,
0
)
->
raise
(
LocalDeadlock
)
|
(
0
,
0
)
->
raise
(
LocalDeadlock
!
it
)
|
(
0
,_
)
->
TE_eps
|
(
_
,_
)
->
(
let
goon_branch
=
put_in_seq
...
...
@@ -1131,7 +1134,9 @@ let rec genpath (t : t) (data : store) (* data env = inputs + pres *)
)
)
in
rec_genpath
({
br
with
br_ctrl
=
e'
})
with
LocalDeadlock
->
raise
(
Deadlock
(
MainArg
.
get_event_nb
!
it
.
arg_opt
))
with
LocalDeadlock
nit
->
it
:=
nit
;
raise
(
Deadlock
(
MainArg
.
get_event_nb
!
it
.
arg_opt
))
)
(** N.B. the "cpt" here is a unique identifier used for compilation
-> not relevant for dynamic simulation
...
...
@@ -1529,13 +1534,13 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
)
(** Constraint: ~same but solve the conjunction first *)
|
TE_constraint
(
ae
,
si
)
->
(
let
t
,
new_acc
=
add_to_guard
t
data
ae
acc
si
in
let
new_acc
=
add_to_guard
_nc
t
data
ae
acc
si
in
let
cstr
=
Exp
.
to_expr
new_acc
.
g_form
in
let
si_atoms
=
List
.
map
to_src_info
(
if
snd
si
=
[]
then
acc
.
g_src
else
(
snd
si
)
::
acc
.
g_src
)
in
let
try_cont
ctx
t
()
=
let
try_cont
ctx
t
()
=
let
t
,
new_acc
,
is_sat
=
check_satisfiablity
t
new_acc
in
if
(
is_sat
)
then
let
enb
=
ctx
.
Event
.
nb
in
...
...
@@ -1592,18 +1597,10 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
Event
.
in_subst
=
[]
;
Event
.
out_subst
=
[]
;
});
Event
.
depth
=
ctx
.
Event
.
depth
;
Event
.
step
=
ctx
.
Event
.
step
;
Event
.
name
=
ctx
.
Event
.
name
;
Event
.
inputs
=
ctx
.
Event
.
inputs
;
Event
.
outputs
=
ctx
.
Event
.
outputs
;
Event
.
locals
=
[]
;
(* fixme *)
Event
.
data
=
ctx
.
Event
.
data
;
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
usat_event
usat_event
in
let
enb
=
ctx
.
Event
.
nb
in
let
ctx
=
event_incr
ctx
t
.
arg_opt
in
...
...
@@ -1618,17 +1615,9 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
Event
.
in_subst
=
[]
;
Event
.
out_subst
=
[]
;
});
Event
.
depth
=
ctx
.
Event
.
depth
;
Event
.
step
=
ctx
.
Event
.
step
;
Event
.
name
=
ctx
.
Event
.
name
;
Event
.
inputs
=
ctx
.
Event
.
inputs
;
Event
.
outputs
=
ctx
.
Event
.
outputs
;
Event
.
locals
=
[]
;
(* fixme *)
Event
.
data
=
ctx
.
Event
.
data
;
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
Event
.
next
=
try_cont
ctx
t
;
}
}
)
(** Sequence *)
|
TE_fby
(
te1
,
te2
)
->
(
...
...
@@ -1897,13 +1886,13 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
try
let
(
sum
,
cel
)
=
List
.
fold_left
weval
(
0
,
[]
)
wtel
in
let
e'
=
match
cel
with
|
[]
->
raise
LocalDeadlock
|
[]
->
raise
(
LocalDeadlock
t
)
|
[(
_
,
e
)]
->
e
|
_
->
TE_dyn_choice
(
sum
,
cel
)
in
rec_genpath_ldbg
ctx
t
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
with
LocalDeadlock
->
fail_cont
ctx
t
with
LocalDeadlock
t
->
fail_cont
ctx
t
)
(* ad hoc node for dynamic simulation:
weights are evaluated (int), guaranted to be > 0,
...
...
@@ -1956,7 +1945,7 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
try
let
e'
=
match
(
gw
,
sw
)
with
|
(
0
,
0
)
->
raise
LocalDeadlock
|
(
0
,
0
)
->
raise
(
LocalDeadlock
t
)
|
(
0
,_
)
->
TE_eps
|
(
_
,_
)
->
(
let
goon_branch
=
put_in_seq
...
...
@@ -1970,7 +1959,7 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
in
rec_genpath_ldbg
ctx
t
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
with
LocalDeadlock
->
fail_cont
ctx
t
with
LocalDeadlock
t
->
fail_cont
ctx
t
)
(** N.B. the "cpt" here is a unique identifier used for compilation
-> not relevant for dynamic simulation
...
...
Write
Preview
Markdown
is supported
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