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
951ddbcf
Commit
951ddbcf
authored
Oct 14, 2015
by
Erwan Jahier
Browse files
Fix a bug introduced in march 2014 where the seed was not transmitted
(
53d82954
)
parent
0a154cfa
Changes
4
Hide whitespace changes
Inline
Side-by-side
source/Lutin/lutExe.ml
View file @
951ddbcf
...
...
@@ -262,14 +262,14 @@ Verbose.put ~flag:dbg "LutExe.make: CheckType.check_pack OK\n";
mnode
)
in
let
exped
=
Expand
.
make
tlenv
mainprg
mnode
in
Verbose
.
put
~
flag
:
dbg
"LutExe.make: Expand.make %s OK
\n
"
mnode
;
(* actual result .... *)
(* Printf.printf
"Event.set_seed %i\n"(MainArg.seed opt);
flush stdout; *)
(*
Event.set_seed (MainArg.seed opt); (* transmit the seed to the event handler *)
*)
if
MainArg
.
run
opt
then
of_expanded_code
opt
exped
else
exit
0
Verbose
.
put
~
flag
:
dbg
"LutExe.make: Expand.make %s OK
\n
"
mnode
;
(* actual result .... *)
Verbose
.
put
~
flag
:
dbg
"Event.set_seed %i
\n
"
(
MainArg
.
seed
opt
);
Event
.
set_seed
(
MainArg
.
seed
opt
);
(* transmit the seed to the event handler *)
if
MainArg
.
run
opt
then
of_expanded_code
opt
exped
else
exit
0
)
...
...
source/Lutin/mainArg.ml
View file @
951ddbcf
...
...
@@ -91,7 +91,13 @@ let seed opt = match opt._seed with
|
Some
i
->
i
|
None
->
(
Random
.
self_init
()
;
Random
.
int
1073741823
)
let
set_seed
opt
s
=
opt
._
seed
<-
s
let
set_seed
opt
s
=
(
match
opt
._
seed
with
|
Some
i
->
Printf
.
fprintf
stderr
"The random engine seed is set to %i
\n
"
i
;
flush
stderr
;
|
None
->
()
);
opt
._
seed
<-
s
(* all unrecognized options are accumulated *)
let
(
add_other
:
t
->
string
->
unit
)
=
...
...
source/common/lucky.ml
View file @
951ddbcf
...
...
@@ -182,57 +182,57 @@ let (env_try : Thickness.t -> env_in -> Prog.state -> FGen.t list ->
(*****************************************************************************)
(* Exported *)
let
(
env_step
:
step_mode
->
env_in
->
Prog
.
state
->
FGen
.
t
list
->
Prog
.
state
*
solution
)
=
Prog
.
state
*
solution
)
=
fun
step_mode
input
state
ral
->
let
thick
=
match
step_mode
with
|
StepInside
->
(
1
,
0
,
Thickness
.
AtMost
0
)
|
StepEdges
->
(
0
,
1
,
Thickness
.
AtMost
0
)
|
StepVertices
->
(
0
,
0
,
Thickness
.
AtMost
1
)
in
try
Utils
.
time_C
"env_try_do"
;
let
(
_ral'
,
csl
,
soll
)
=
env_try_do
(
1
,
thick
)
input
state
ral
[]
in
Utils
.
time_R
"env_try_do"
;
let
(
output
,
local
)
=
assert
(
soll
<>
[]
);
List
.
hd
soll
in
let
new_state_dyn
=
{
memory
=
update_pre
input
output
local
state
;
ctrl_state
=
csl
;
last_input
=
input
;
last_output
=
output
;
last_local
=
local
;
verbose
=
state
.
d
.
verbose
}
in
let
new_state
=
{
d
=
new_state_dyn
;
s
=
state
.
s
}
in
(* Clean-up cached info that depends on pre or inputs *)
Formula_to_bdd
.
clear_step
()
;
!
Solver
.
clear_snt
()
;
previous_output
:=
Some
output
;
previous_local
:=
Some
local
;
(
new_state
,
(
output
,
local
))
with
FGen
.
NoMoreFormula
->
match
(
!
previous_output
,
!
previous_local
)
with
|
Some
(
out
)
,
Some
(
loc
)
->
if
state
.
s
.
reactive
then
(
if
state
.
d
.
verbose
>=
1
then
print_string
(
"### No transition is available; "
^
"values of the previous cycle are used.
\n
"
);
flush
stdout
;
(
state
,
(
out
,
loc
))
)
else
(
if
state
.
d
.
verbose
>=
1
then
print_string
(
"# No transition is labelled by a satisfiable formula.
\n
"
^
"# The program is blocked.
\n
"
);
flush
stdout
;
raise
FGen
.
NoMoreFormula
)
|
_
,
_
->
raise
FGen
.
NoMoreFormula
let
thick
=
match
step_mode
with
|
StepInside
->
(
1
,
0
,
Thickness
.
AtMost
0
)
|
StepEdges
->
(
0
,
1
,
Thickness
.
AtMost
0
)
|
StepVertices
->
(
0
,
0
,
Thickness
.
AtMost
1
)
in
try
Utils
.
time_C
"env_try_do"
;
let
(
_ral'
,
csl
,
soll
)
=
env_try_do
(
1
,
thick
)
input
state
ral
[]
in
Utils
.
time_R
"env_try_do"
;
let
(
output
,
local
)
=
assert
(
soll
<>
[]
);
List
.
hd
soll
in
let
new_state_dyn
=
{
memory
=
update_pre
input
output
local
state
;
ctrl_state
=
csl
;
last_input
=
input
;
last_output
=
output
;
last_local
=
local
;
verbose
=
state
.
d
.
verbose
}
in
let
new_state
=
{
d
=
new_state_dyn
;
s
=
state
.
s
}
in
(* Clean-up cached info that depends on pre or inputs *)
Formula_to_bdd
.
clear_step
()
;
!
Solver
.
clear_snt
()
;
previous_output
:=
Some
output
;
previous_local
:=
Some
local
;
(
new_state
,
(
output
,
local
))
with
FGen
.
NoMoreFormula
->
match
(
!
previous_output
,
!
previous_local
)
with
|
Some
(
out
)
,
Some
(
loc
)
->
if
state
.
s
.
reactive
then
(
if
state
.
d
.
verbose
>=
1
then
print_string
(
"### No transition is available; "
^
"values of the previous cycle are used.
\n
"
);
flush
stdout
;
(
state
,
(
out
,
loc
))
)
else
(
if
state
.
d
.
verbose
>=
1
then
print_string
(
"# No transition is labelled by a satisfiable formula.
\n
"
^
"# The program is blocked.
\n
"
);
flush
stdout
;
raise
FGen
.
NoMoreFormula
)
|
_
,
_
->
raise
FGen
.
NoMoreFormula
source/common/luckyDraw.ml
View file @
951ddbcf
...
...
@@ -412,7 +412,9 @@ let random_seed _ =
let
(
set_seed
:
int
->
unit
)
=
fun
seed
->
Random
.
init
seed
Printf
.
fprintf
stderr
"The random engine seed is set to %i
\n
"
seed
;
flush
stderr
;
Random
.
init
seed
let
string_of_value
=
function
B
(
b
)
->
if
b
then
"t"
else
"f"
...
...
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