Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
L
lutin
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
verimag
synchrone
lutin
Commits
dd9c4a6a
Commit
dd9c4a6a
authored
Apr 05, 2019
by
erwan
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
RdbgPlugin.t now has a reset field
parent
6ab04529
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
40 additions
and
11 deletions
+40
-11
ltop/src/lustreRun.ml
ltop/src/lustreRun.ml
+4
-1
ltop/src/runDirect.ml
ltop/src/runDirect.ml
+29
-10
lutin/src/lutExe.ml
lutin/src/lutExe.ml
+7
-0
No files found.
ltop/src/lustreRun.ml
View file @
dd9c4a6a
(* Time-stamp: <modified the 0
5/07/2018 (at 14:30
) by Erwan Jahier> *)
(* Time-stamp: <modified the 0
4/04/2019 (at 16:45
) by Erwan Jahier> *)
open
RdbgPlugin
type
vars
=
(
string
*
Data
.
t
)
list
...
...
@@ -113,6 +113,7 @@ let (make_ec : string -> RdbgPlugin.t) =
Event
.
data
=
ctx
.
Event
.
data
;
Event
.
next
=
(
fun
()
->
cont
(
step
sl
)
ctx
);
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
{
...
...
@@ -235,6 +236,7 @@ let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
Event
.
sinfo
=
None
;
Event
.
next
=
(
fun
()
->
cont
(
step
sl
)
ctx
);
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
let
plugin
=
{
...
...
@@ -342,6 +344,7 @@ let (make_ec_exe : string -> RdbgPlugin.t) =
Event
.
sinfo
=
None
;
Event
.
next
=
(
fun
()
->
cont
(
step
sl
)
ctx
);
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
{
...
...
ltop/src/runDirect.ml
View file @
dd9c4a6a
...
...
@@ -71,9 +71,18 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars ->
type
ctx
=
Event
.
t
type
e
=
Event
.
t
let
rec
(
list_split8
:
(
'
a
*
'
b
*
'
c
*
'
d
*
'
e
*
'
f
*
'
g
*
'
h
)
list
->
'
a
list
*
'
b
list
*
'
c
list
*
'
d
list
*
'
e
list
*
'
f
list
*
'
g
list
*
'
h
list
)
=
function
|
[]
->
([]
,
[]
,
[]
,
[]
,
[]
,
[]
,
[]
,
[]
)
|
(
x
,
y
,
z
,
t
,
u
,
v
,
w
,
a
)
::
l
->
let
(
rx
,
ry
,
rz
,
rt
,
ru
,
rv
,
rw
,
ra
)
=
list_split8
l
in
(
x
::
rx
,
y
::
ry
,
z
::
rz
,
t
::
rt
,
u
::
ru
,
v
::
rv
,
w
::
rw
,
a
::
ra
)
open
RdbgPlugin
let
(
make_rp_list
:
reactive_program
list
->
vars
list
*
vars
list
*
(
string
->
unit
)
list
*
vars
list
*
vars
list
*
(
unit
->
unit
)
list
*
(
string
->
unit
)
list
*
(
Data
.
subst
list
->
Data
.
subst
list
)
list
*
(
Data
.
subst
list
->
ctx
->
(
Data
.
subst
list
->
ctx
->
Event
.
t
)
->
Event
.
t
)
list
*
Data
.
subst
list
list
*
Data
.
subst
list
list
)
=
...
...
@@ -92,8 +101,8 @@ let (make_rp_list : reactive_program list ->
|
Ocaml
(
cmxs
)
->
OcamlRun
.
make_ocaml
cmxs
|
Lutin
(
args
)
->
LutinRun
.
make
args
in
let
ins
,
outs
,
kill
,
step
,
step_dbg
,
initin
,
initout
=
plugin
.
inputs
,
plugin
.
outputs
,
plugin
.
kill
,
plugin
.
step
,
plugin
.
step_dbg
,
let
ins
,
outs
,
reset
,
kill
,
step
,
step_dbg
,
initin
,
initout
=
plugin
.
inputs
,
plugin
.
outputs
,
plugin
.
reset
,
plugin
.
kill
,
plugin
.
step
,
plugin
.
step_dbg
,
plugin
.
init_inputs
,
plugin
.
init_outputs
in
let
step
=
if
args
.
debug_ltop
then
...
...
@@ -110,9 +119,9 @@ let (make_rp_list : reactive_program list ->
else
step
in
ins
,
outs
,
kill
,
step
,
step_dbg
,
initin
,
initout
ins
,
outs
,
reset
,
kill
,
step
,
step_dbg
,
initin
,
initout
in
Util
.
list_split7
(
List
.
map
aux
rpl
)
list_split8
(
List
.
map
aux
rpl
)
type
cov_opt
=
...
...
@@ -149,27 +158,35 @@ let (start : unit -> Event.t) =
fun
()
->
(* Get sut info (var names, step func, etc.) *)
let
_
=
if
args
.
debug_ltop
then
LustreRun
.
debug
:=
args
.
debug_ltop
in
let
sut_in_l
,
sut_out_l
,
sut_kill_l
,
sut_step_sl_l
,
sut_step_dbg_sl_l
,
let
sut_in_l
,
sut_out_l
,
sut_
reset_l
,
sut_
kill_l
,
sut_step_sl_l
,
sut_step_dbg_sl_l
,
sut_init_in_l
,
sut_init_out_l
=
make_rp_list
args
.
suts
in
let
sut_reset
()
=
List
.
iter
(
fun
f
->
f
()
)
sut_reset_l
in
let
sut_kill
msg
=
List
.
iter
(
fun
f
->
f
msg
)
sut_kill_l
in
let
sut_init_in
=
List
.
flatten
sut_init_in_l
in
let
sut_init_out
=
List
.
flatten
sut_init_out_l
in
(* Get oracle info (var names, step func, etc.)*)
let
oracle_in_l
,
oracle_out_l
,
oracle_kill_l
,
oracle_step_sl_l
,
let
oracle_in_l
,
oracle_out_l
,
oracle_
reset_l
,
oracle_
kill_l
,
oracle_step_sl_l
,
oracle_step_dbg_sl_l
,
_
,
_
=
make_rp_list
args
.
oracles
in
let
oracle_kill
msg
=
List
.
iter
(
fun
f
->
f
msg
)
oracle_kill_l
in
let
oracle_reset
()
=
List
.
iter
(
fun
f
->
f
()
)
oracle_reset_l
in
(* Get env info (var names, step func, etc.)*)
let
env_in_l
,
env_out_l
,
env_kill_l
,
env_step_sl_l
,
env_step_dbg_sl_l
,
let
env_in_l
,
env_out_l
,
env_
reset_l
,
env_
kill_l
,
env_step_sl_l
,
env_step_dbg_sl_l
,
env_init_in_l
,
env_init_out_l
=
make_rp_list
args
.
envs
in
let
env_reset
()
=
List
.
iter
(
fun
f
->
f
()
)
env_reset_l
in
let
env_kill
msg
=
List
.
iter
(
fun
f
->
f
msg
)
env_kill_l
in
let
_env_init_in
=
Util
.
rm_dup
(
List
.
flatten
env_init_in_l
)
in
let
_env_init_out
=
Util
.
rm_dup
(
List
.
flatten
env_init_out_l
)
in
let
reset
()
=
if
args
.
verbose
>
0
then
(
Printf
.
eprintf
"rdbgRun.start: resetting all RPs
\n
"
;
flush
stderr
);
sut_reset
()
;
env_reset
()
;
oracle_reset
()
in
let
vars_to_string
l
=
String
.
concat
"
\n
"
(
List
.
map
(
fun
(
vn
,
vt
)
->
...
...
@@ -464,7 +481,8 @@ let (start : unit -> Event.t) =
loop
(
check_oracles
oracle_in_vals
i
oracle_out_l
oracle_out_vals_l
cov
)
sut_out_vals
env_out_vals
ctx
(
i
+
1
)
()
);
Event
.
terminate
=
term
Event
.
terminate
=
term
;
Event
.
reset
=
ctx
.
Event
.
reset
}
)
else
...
...
@@ -502,6 +520,7 @@ let (start : unit -> Event.t) =
Event
.
locals
=
[]
;
Event
.
data
=
[]
;
Event
.
terminate
=
(
fun
()
->
killem_all
cov_init
);
Event
.
reset
=
(
fun
()
->
reset
()
);
Event
.
lang
=
""
;
Event
.
next
=
(
fun
()
->
assert
false
);
Event
.
kind
=
Event
.
Ltop
;
...
...
lutin/src/lutExe.ml
View file @
dd9c4a6a
...
...
@@ -1561,6 +1561,7 @@ let rec (genpath_ldbg :
Event
.
locals
=
[]
;
(* fixme *)
Event
.
data
=
ctx
.
Event
.
data
;
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
else
(* the constraint is unsat *)
let
lazy_ci
=
fun
()
->
...
...
@@ -1598,6 +1599,7 @@ let rec (genpath_ldbg :
Event
.
locals
=
[]
;
(* fixme *)
Event
.
data
=
ctx
.
Event
.
data
;
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
usat_event
...
...
@@ -1623,6 +1625,7 @@ let rec (genpath_ldbg :
Event
.
locals
=
[]
;
(* fixme *)
Event
.
data
=
ctx
.
Event
.
data
;
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
Event
.
next
=
try_cont
ctx
;
}
)
...
...
@@ -2106,6 +2109,7 @@ let rec (genpath_ldbg :
Event
.
next
=
(
fun
()
->
Reactive
.
step_ldbg
ctx
react
ins
cont3
fail_cont
excn_cont
);
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
event
...
...
@@ -2379,6 +2383,7 @@ and (to_reactive_prg_ldbg :
cont
ctx2
(
Reactive
.
DoStep_ldbg
(
to_reactive_prg_ldbg
rid
it
state'
))
outvals
);
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
}
in
event
...
...
@@ -2399,6 +2404,7 @@ and (to_reactive_prg_ldbg :
Event
.
data
=
edata
@
predata
;
Event
.
next
=
(
fun
()
->
genpath_ldbg
it
data
cstate
ctx
cont2
fail_cont
excn_cont
);
Event
.
terminate
=
ctx
.
Event
.
terminate
;
Event
.
reset
=
ctx
.
Event
.
reset
;
Event
.
sinfo
=
None
;
}
...
...
@@ -2591,6 +2597,7 @@ let (step_ldbg: ctx -> string -> t -> control_state -> data_state ->
(* Event.Exit (guard_to_string zeguard, cstr, lazy_si) *)
Event
.
next
=
(
fun
()
->
cont
ctx2
ctrl
data
);
Event
.
terminate
=
ctx2
.
Event
.
terminate
;
Event
.
reset
=
ctx2
.
Event
.
reset
;
}
)
)
...
...
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