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
lutin
Commits
9e4b5902
Commit
9e4b5902
authored
Jul 05, 2018
by
Erwan Jahier
Browse files
Take #reset pragmas into account + adapt to the new RdbgPlugin.t 1.177 api
(that now have a reset field)
parent
847a16d7
Pipeline
#9677
passed with stages
in 8 minutes and 35 seconds
Changes
7
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Makefile.dev
View file @
9e4b5902
...
...
@@ -87,12 +87,15 @@ $(WWW)/pool/$(PACKNAME).tgz: $(PACKNAME).tgz
$(WWWTEST)/pool/$(PACKNAME).tgz
:
$(PACKNAME).tgz
mv
$^
$@
OPAM_FILE
=
$(
shell
find
$(WWW)
/opam-repository/packages
-name
opam
-cmin
-2
|
sed
-e
's/^./\U&/'
)
OPAM_FILE_TEST
=
$(
shell
find
$(WWWTEST)
/opam-repository/packages
-name
opam
-cmin
-1
|
sed
-e
's/^./\U&/'
)
OPAM_FILE
=
$(
shell
find
$(WWW)
/opam-repository/packages
-name
opam
|
grep
Lutin |
sort
|
tail
-1
|
sed
-e
's/^./\U&/'
)
OPAM_FILE_TEST
=
$(
shell
find
$(WWWTEST)
/opam-repository/packages
-name
opam
|
grep
Lutin |
sort
|
tail
-1
|
sed
-e
's/^./\U&/'
)
OPAM_DIR
=
$(
shell
dirname
$(OPAM_FILE)
)
OFFICIAL_OPAM_DIR
=
/home/jahier/local/opam-repository/packages/lutin
x
:
echo
$(OPAM_FILE_TEST)
opam
:
$(WWW)/pool/$(PACKNAME).tgz
cd
$(WWW)
/opam-repository/packages
&&
\
oasis2opam
$(HTTP)
/pool/
$(PACKNAME)
.tgz
&&
\
...
...
_oasis
View file @
9e4b5902
OASISFormat: 0.4
Name: Lutin
Version: 2.5
6
Version: 2.5
7
Authors: Erwan Jahier, Pascal Raymond, Bertrand Jeannnet (polka), Yvan Roux
Maintainers: erwan.jahier@univ-grenoble-alpes.fr
License: CeCILL
...
...
@@ -27,7 +27,7 @@ SourceRepository "master"
Executable lutin
Path: lutin/src
MainIs: main.ml
BuildDepends: str,unix,num,rdbg-plugin (>= 1.17
0
),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp
BuildDepends: str,unix,num,rdbg-plugin (>= 1.17
7
),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp
NativeOpt: -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true
Install:true
...
...
@@ -69,7 +69,7 @@ Library "lutin-utils"
Executable lurette
Path: lurette-nocaml/src
MainIs: lurette.ml
BuildDepends: str,unix,num,dynlink,extlib,camlp4,lutils (>= 1.9),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp,rdbg-plugin,lustre-v6,lutin
BuildDepends: str,unix,num,dynlink,extlib,camlp4,lutils (>= 1.9),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp,rdbg-plugin
(>= 1.177)
,lustre-v6,lutin
NativeOpt: rdbg4lurette.cmxa # for some reasons not recogniezd as a package
Install:true
CompiledObject: native
...
...
examples/crazy-rabbit/rabbit.ml
View file @
9e4b5902
...
...
@@ -36,6 +36,7 @@ let _ =
let
init
_
=
()
let
kill
_
=
()
let
reset
_
=
()
type
var_type
=
string
...
...
@@ -157,6 +158,7 @@ let plugin = {
id
=
"ze rabbit plugin"
;
inputs
=
inputs
;
outputs
=
outputs
;
reset
=
reset
;
kill
=
kill
;
init_inputs
=
mems_i
;
init_outputs
=
mems_o
;
...
...
ltop/src/lustreRun.ml
View file @
9e4b5902
(* Time-stamp: <modified the 0
9
/0
5
/2018 (at 1
5:49
) by Erwan Jahier> *)
(* Time-stamp: <modified the 0
5
/0
7
/2018 (at 1
4:30
) by Erwan Jahier> *)
open
RdbgPlugin
type
vars
=
(
string
*
Data
.
t
)
list
...
...
@@ -119,6 +119,7 @@ let (make_ec : string -> RdbgPlugin.t) =
id
=
""
;
inputs
=
ec_in
;
outputs
=
ec_out
;
reset
=
(
fun
()
->
RifIO
.
write
ec_oc
"#reset
\n
"
;
flush
ec_oc
);
kill
=
kill
;
init_inputs
=
[]
;
init_outputs
=
[]
;
...
...
@@ -240,6 +241,7 @@ let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
id
=
""
;
inputs
=
vars_in
;
outputs
=
vars_out
;
reset
=
(
fun
()
->
RifIO
.
write
sock_out
"#reset
\n
"
;
flush
sock_out
);
kill
=
kill
;
init_inputs
=
[]
;
init_outputs
=
[]
;
...
...
@@ -346,6 +348,7 @@ let (make_ec_exe : string -> RdbgPlugin.t) =
id
=
""
;
inputs
=
ec_in
;
outputs
=
ec_out
;
reset
=
(
fun
()
->
RifIO
.
write
ec_oc
"#reset
\n
"
;
flush
ec_oc
);
kill
=
kill
;
init_inputs
=
[]
;
init_outputs
=
[]
;
...
...
lutin/src/lutinRun.ml
View file @
9e4b5902
(* Time-stamp: <modified the
3
0/0
3
/201
7
(at 1
7:58
) by Erwan Jahier> *)
(* Time-stamp: <modified the 0
5
/0
7
/201
8
(at 1
4:20
) by Erwan Jahier> *)
(**********************************************************************************)
type
vars
=
(
string
*
Data
.
t
)
list
...
...
@@ -110,6 +110,14 @@ let make argv =
id
=
Printf
.
sprintf
"%s (%s)"
id
version
;
inputs
=
lut_in
;
outputs
=
lut_out
;
reset
=
(
fun
()
->
(
ctrl_state
:=
(
LutExe
.
get_init_state
lut_mach
);
data_state
:=
{
LutExe
.
ins
=
Value
.
OfIdent
.
empty
;
LutExe
.
outs
=
lut_memories
;
LutExe
.
mems
=
LutExe
.
get_init_pres
lut_mach
}
));
kill
=
(
fun
_
->
()
);
init_inputs
=
mems_in
;
init_outputs
=
mems_out
;
...
...
lutin/src/main.ml
View file @
9e4b5902
...
...
@@ -137,34 +137,41 @@ let rec to_simu oc infile mnode opt = (
let
noo
=
not
(
MainArg
.
only_outputs
opt
)
in
Random
.
init
seed
;
if
MainArg
.
compute_volume
opt
then
Solver
.
set_fair_mode
()
else
Solver
.
set_efficient_mode
()
;
if
MainArg
.
compute_volume
opt
then
Solver
.
set_fair_mode
()
else
Solver
.
set_efficient_mode
()
;
!
Solver
.
init_snt
()
;
Rif
.
write
oc
msg
;
Rif
.
write_interface
oc
init_state
.
Prog
.
s
.
Prog
.
in_vars
init_state
.
Prog
.
s
.
Prog
.
out_vars
loc
None
;
Rif
.
write_interface
oc
init_state
.
Prog
.
s
.
Prog
.
in_vars
init_state
.
Prog
.
s
.
Prog
.
out_vars
loc
None
;
Rif
.
flush
oc
;
let
next_state
=
init_state
in
let
lut_memories
=
if
MainArg
.
load_mem
opt
then
(
output_string
oc
"#lutin_outputs_memories "
;
Rif
.
read
(
Verbose
.
level
()
>
0
)
stdin
(
if
noo
then
Some
oc
else
None
)
init_state
.
Prog
.
s
.
Prog
.
out_vars
)
Rif
.
read
(
Verbose
.
level
()
>
0
)
stdin
(
if
noo
then
Some
oc
else
None
)
init_state
.
Prog
.
s
.
Prog
.
out_vars
)
else
Value
.
OfIdent
.
empty
in
(* first main_loop : no pre context *)
main_loop
oc
opt
1
next_state
lut_memories
main_loop
oc
opt
1
next_state
lut_memories
next_state
lut_memories
)
and
main_loop
oc
opt
t
state
pre_lut_output
=
(
and
main_loop
oc
opt
t
init_state
init_pre_lut_output
state
pre_lut_output
=
(
Verbose
.
exe
(
fun
()
->
let
csnme
=
(
Prog
.
ctrl_state_to_string_long
state
.
Prog
.
d
.
Prog
.
ctrl_state
)
in
Verbose
.
put
"#Main.main_loop ctrl_state=%s
\n
"
csnme
;
);
if
state
.
Prog
.
s
.
Prog
.
is_final
state
.
Prog
.
d
.
Prog
.
ctrl_state
then
()
else
main_loop_core
oc
opt
t
state
pre_lut_output
else
try
main_loop_core
oc
opt
t
init_state
init_pre_lut_output
state
pre_lut_output
with
RifIO
.
Reset
->
main_loop_core
oc
opt
t
init_state
init_pre_lut_output
init_state
init_pre_lut_output
)
and
main_loop_core
oc
opt
t
state
pre_lut_output
=
(
and
main_loop_core
oc
opt
t
init_state
init_pre_lut_output
state
pre_lut_output
=
(
let
step_str
=
(
"#step "
^
(
string_of_int
t
))
^
(
if
state
.
Prog
.
d
.
Prog
.
verbose
>=
1
...
...
@@ -175,7 +182,9 @@ and main_loop_core oc opt t state pre_lut_output = (
let
noo
=
not
(
MainArg
.
only_outputs
opt
)
in
let
_
=
if
noo
then
Rif
.
write
oc
step_str
in
let
lut_input
=
if
t
=
1
&&
(
boot
opt
)
then
Value
.
OfIdent
.
empty
else
Rif
.
read
(
Verbose
.
level
()
>
0
)
stdin
(
if
noo
then
Some
oc
else
None
)
state
.
Prog
.
s
.
Prog
.
in_vars
in
Rif
.
read
(
Verbose
.
level
()
>
0
)
stdin
(
if
noo
then
Some
oc
else
None
)
state
.
Prog
.
s
.
Prog
.
in_vars
in
let
generator
=
LucFGen
.
get
lut_input
state
in
(*
Call Lucky explorer/solver
...
...
@@ -223,12 +232,13 @@ and main_loop_core oc opt t state pre_lut_output = (
!
Solver
.
clear_snt
()
;
match
MainArg
.
max_steps
opt
with
|
None
->
main_loop
oc
opt
(
t
+
1
)
next_state
lut_output
|
None
->
main_loop
oc
opt
(
t
+
1
)
init_state
init_pre_lut_output
next_state
lut_output
|
Some
max
->
(
if
(
t
<
max
)
then
(
(* next pre's are current vals *)
(* let next_state = LutProg.memorize_data next_state lut_input lut_output loc in *)
main_loop
oc
opt
(
t
+
1
)
next_state
lut_output
main_loop
oc
opt
(
t
+
1
)
init_state
init_pre_lut_output
next_state
lut_output
)
else
(
if
noo
then
Rif
.
write
oc
"
\n
#end
\n
"
else
Rif
.
write
oc
"
\n
q
\n
"
;
Rif
.
flush
oc
)
...
...
@@ -257,7 +267,7 @@ let to_exe oc infile mnode opt = (
in
let
noo
=
not
(
MainArg
.
only_outputs
opt
)
in
let
rec
do_step
cpt
ctrl
ins
pres
=
(
let
rec
do_step
cpt
init_ctrl
init_ins
init_pres
ctrl
ins
pres
=
(
(* Clean-up cached info that depend on pre or inputs *)
Formula_to_bdd
.
clear_step
()
;
...
...
@@ -328,11 +338,14 @@ let to_exe oc infile mnode opt = (
Rif
.
write
oc
step_str
;
Rif
.
flush
oc
);
let
pres'
=
LutExe
.
make_pre
exe
ins
outs
locs
in
let
ins'
=
Rif
.
read
(
Verbose
.
level
()
>
0
)
stdin
(
if
noo
then
Some
oc
else
None
)
in_vars
in
MainArg
.
event_incr
opt
;
do_step
(
cpt
+
1
)
ctrl'
ins'
pres'
try
let
pres'
=
LutExe
.
make_pre
exe
ins
outs
locs
in
let
ins'
=
Rif
.
read
(
Verbose
.
level
()
>
0
)
stdin
(
if
noo
then
Some
oc
else
None
)
in_vars
in
MainArg
.
event_incr
opt
;
do_step
(
cpt
+
1
)
init_ctrl
init_ins
init_pres
ctrl'
ins'
pres'
with
RifIO
.
Reset
->
do_step
(
cpt
+
1
)
init_ctrl
init_ins
init_pres
init_ctrl
init_ins
init_pres
)
)
|
LutExe
.
Raise
x
->
(
...
...
@@ -379,7 +392,7 @@ let to_exe oc infile mnode opt = (
in
(* HERE: init input/output pres *)
let
pres
=
LutExe
.
get_init_pres
exe
in
do_step
cpt
ctrl
ins
pres
do_step
cpt
ctrl
ins
pres
ctrl
ins
pres
)
(* TEST
...
...
lutin/src/version.ml
View file @
9e4b5902
let
str
=
"2.5
6
"
let
sha
=
"
a7040a2
"
let
str
=
"2.5
7
"
let
sha
=
"
847a16d
"
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