Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
sasa
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
verimag
synchrone
sasa
Commits
4cf35589
Commit
4cf35589
authored
3 years ago
by
erwan
Browse files
Options
Downloads
Patches
Plain Diff
reindent
parent
9c5e11a4
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/dot2lus.ml
+137
-137
137 additions, 137 deletions
src/dot2lus.ml
with
137 additions
and
137 deletions
src/dot2lus.ml
+
137
−
137
View file @
4cf35589
...
@@ -19,147 +19,147 @@ let algo_name (node : Topology.node) =
...
@@ -19,147 +19,147 @@ let algo_name (node : Topology.node) =
(* prints includes, graph constants and helper functions *)
(* prints includes, graph constants and helper functions *)
let
output_prelude
output
(
graph
:
Topology
.
t
)
=
let
output_prelude
output
(
graph
:
Topology
.
t
)
=
(* NOTE: b2s, array_to_string and matrix_to_string copied from genOracle.ml *)
(* NOTE: b2s, array_to_string and matrix_to_string copied from genOracle.ml *)
let
b2s
b
=
if
b
then
"t"
else
"f"
in
let
b2s
b
=
if
b
then
"t"
else
"f"
in
let
(
array_to_string
:
bool
array
->
string
)
=
let
(
array_to_string
:
bool
array
->
string
)
=
fun
a
->
fun
a
->
let
l
=
Array
.
fold_right
(
fun
b
acc
->
(
b2s
b
)
::
acc
)
a
[]
in
let
l
=
Array
.
fold_right
(
fun
b
acc
->
(
b2s
b
)
::
acc
)
a
[]
in
"["
^
(
String
.
concat
","
l
)
^
"]"
in
"["
^
(
String
.
concat
","
l
)
^
"]"
in
let
(
matrix_to_string
:
bool
array
array
->
string
)
=
let
(
matrix_to_string
:
bool
array
array
->
string
)
=
fun
m
->
fun
m
->
let
l
=
Array
.
fold_right
(
fun
a
acc
->
(
array_to_string
a
)
::
acc
)
m
[]
in
let
l
=
Array
.
fold_right
(
fun
a
acc
->
(
array_to_string
a
)
::
acc
)
m
[]
in
"[
\n\t
"
^
(
String
.
concat
",
\n\t
"
l
)
^
"]"
in
"[
\n\t
"
^
(
String
.
concat
",
\n\t
"
l
)
^
"]"
in
(* include Lustre algos *)
(* include Lustre algos *)
graph
.
nodes
graph
.
nodes
|>
List
.
map
algo_name
|>
List
.
map
algo_name
|>
List
.
sort_uniq
String
.
compare
|>
List
.
sort_uniq
String
.
compare
|>
List
.
iter
(
Printf
.
fprintf
output
"include
\"
%s.lus
\"\n
"
);
|>
List
.
iter
(
Printf
.
fprintf
output
"include
\"
%s.lus
\"\n
"
);
(* define graph constants *)
(* define graph constants *)
output_string
output
"
\n
"
;
output_string
output
"
\n
"
;
Printf
.
fprintf
output
"const card = %d;
\n
"
(
List
.
length
graph
.
nodes
);
Printf
.
fprintf
output
"const card = %d;
\n
"
(
List
.
length
graph
.
nodes
);
Printf
.
fprintf
output
"const links_number = %d;
\n
"
(
Topology
.
get_nb_link
graph
);
Printf
.
fprintf
output
"const links_number = %d;
\n
"
(
Topology
.
get_nb_link
graph
);
let
dmin
,
dmax
=
Topology
.
get_degree
graph
in
let
dmin
,
dmax
=
Topology
.
get_degree
graph
in
Printf
.
fprintf
output
"const max_degree = %d;
\n
"
dmax
;
Printf
.
fprintf
output
"const max_degree = %d;
\n
"
dmax
;
Printf
.
fprintf
output
"const min_degree = %d;
\n
"
dmin
;
Printf
.
fprintf
output
"const min_degree = %d;
\n
"
dmin
;
Printf
.
fprintf
output
"const mean_degree = %f;
\n
"
(
Topology
.
get_mean_degree
graph
);
Printf
.
fprintf
output
"const mean_degree = %f;
\n
"
(
Topology
.
get_mean_degree
graph
);
Printf
.
fprintf
output
"const is_directed = %b;
\n
"
graph
.
directed
;
Printf
.
fprintf
output
"const is_directed = %b;
\n
"
graph
.
directed
;
Printf
.
fprintf
output
"const is_cyclic = %b;
\n
"
(
Topology
.
is_cyclic
graph
);
Printf
.
fprintf
output
"const is_cyclic = %b;
\n
"
(
Topology
.
is_cyclic
graph
);
Printf
.
fprintf
output
"const is_connected = %b;
\n
"
(
Topology
.
is_connected
graph
);
Printf
.
fprintf
output
"const is_connected = %b;
\n
"
(
Topology
.
is_connected
graph
);
(* dot attributes *)
(* dot attributes *)
let
already_defined
=
function
let
already_defined
=
function
|
"card"
|
"card"
|
"links_number"
|
"links_number"
|
"max_degree"
|
"max_degree"
|
"min_degree"
|
"min_degree"
|
"mean_degree"
|
"mean_degree"
|
"is_directed"
|
"is_directed"
|
"is_cyclic"
|
"is_cyclic"
|
"is_connected"
|
"is_connected"
|
"f"
|
"f"
|
"t"
|
"t"
|
"adjacency"
->
true
|
"adjacency"
->
true
|
_
->
false
in
|
_
->
false
in
List
.
iter
List
.
iter
(
fun
(
name
,
value
)
->
(
fun
(
name
,
value
)
->
if
not
(
already_defined
name
)
if
not
(
already_defined
name
)
then
Printf
.
fprintf
output
"const %s = %s;
\n
"
name
value
)
then
Printf
.
fprintf
output
"const %s = %s;
\n
"
name
value
)
graph
.
attributes
;
graph
.
attributes
;
(* adjacency matrix *)
(* adjacency matrix *)
output_string
output
"const t = true;
\n
"
;
output_string
output
"const t = true;
\n
"
;
output_string
output
"const f = false;
\n
"
;
output_string
output
"const f = false;
\n
"
;
Printf
.
fprintf
output
Printf
.
fprintf
output
"const adjacency = %s;
\n
"
"const adjacency = %s;
\n
"
(
graph
|>
Topology
.
to_adjacency
|>
matrix_to_string
);
(
graph
|>
Topology
.
to_adjacency
|>
matrix_to_string
);
(* helper functions *)
(* helper functions *)
output_string
output
"
output_string
output
"
function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int);
function dot2lus_first_set<<const N:int>>(s : bool^N) returns (x : int);
var
var
found : int;
found : int;
let
let
found =
found =
with (N = 1) then (if s[0] then 0 else -1)
with (N = 1) then (if s[0] then 0 else -1)
else dot2lus_first_set<<N-1>>(s[1 .. N-1]);
else dot2lus_first_set<<N-1>>(s[1 .. N-1]);
x =
x =
if s[0] then 0
if s[0] then 0
else if found < 0 then -1
else if found < 0 then -1
else found + 1;
else found + 1;
tel;
\n
"
;
tel;
\n
"
;
Printf
.
fprintf
output
"
Printf
.
fprintf
output
"
function dot2lus_action_of_activation(activation : bool^%s) returns (action : %s);
function dot2lus_action_of_activation(activation : bool^%s) returns (action : %s);
let
let
action = %s(dot2lus_first_set<<%s>>(activation));
action = %s(dot2lus_first_set<<%s>>(activation));
tel;
\n
"
action_number
action_type
action_of_int
action_number
tel;
\n
"
action_number
action_type
action_of_int
action_number
(* prints the actual Lustre node that implements the input topology *)
(* prints the actual Lustre node that implements the input topology *)
let
output_topology
output
(
graph
:
Topology
.
t
)
name
=
let
output_topology
output
(
graph
:
Topology
.
t
)
name
=
let
make_index
(
graph
:
Topology
.
t
)
:
(
Topology
.
node_id
->
int
)
=
let
make_index
(
graph
:
Topology
.
t
)
:
(
Topology
.
node_id
->
int
)
=
let
index_map
=
Hashtbl
.
create
(
List
.
length
graph
.
nodes
)
in
let
index_map
=
Hashtbl
.
create
(
List
.
length
graph
.
nodes
)
in
graph
.
nodes
graph
.
nodes
|>
List
.
map
(
fun
(
n
:
Topology
.
node
)
->
n
.
id
)
|>
List
.
map
(
fun
(
n
:
Topology
.
node
)
->
n
.
id
)
|>
List
.
iteri
(
fun
index
node_id
->
Hashtbl
.
add
index_map
node_id
index
);
|>
List
.
iteri
(
fun
index
node_id
->
Hashtbl
.
add
index_map
node_id
index
);
Hashtbl
.
find
index_map
(* returns the partially applied find *)
in
Hashtbl
.
find
index_map
(* returns the partially applied find *)
in
let
sprint_neighbor_list
neighbor_ids
list
:
string
=
let
sprint_neighbor_list
neighbor_ids
list
:
string
=
match
neighbor_ids
with
match
neighbor_ids
with
|
[]
->
"[]"
|
[]
->
"[]"
|
n
::
ns
->
|
n
::
ns
->
let
prefix
,
sufix
=
Printf
.
sprintf
"[ %s[%d]"
list
n
,
" ]"
in
let
prefix
,
sufix
=
Printf
.
sprintf
"[ %s[%d]"
list
n
,
" ]"
in
let
concat
acc
n
=
acc
^
(
Printf
.
sprintf
", %s[%d]"
list
n
)
in
let
concat
acc
n
=
acc
^
(
Printf
.
sprintf
", %s[%d]"
list
n
)
in
(
List
.
fold_left
concat
prefix
ns
)
^
sufix
in
(
List
.
fold_left
concat
prefix
ns
)
^
sufix
in
Printf
.
fprintf
output
Printf
.
fprintf
output
"
\n
node %s(p : bool^%s^card; initials : %s^card)
\n
"
"
\n
node %s(p : bool^%s^card; initials : %s^card)
\n
"
name
action_number
state_type
;
name
action_number
state_type
;
Printf
.
fprintf
output
Printf
.
fprintf
output
"returns (p_c : %s^card; Enab_p : bool^%s^card);
\n
"
"returns (p_c : %s^card; Enab_p : bool^%s^card);
\n
"
state_type
action_number
;
state_type
action_number
;
output_string
output
"var
\n
"
;
output_string
output
"var
\n
"
;
Printf
.
fprintf
output
"
\t
prev_p_c : %s^card;
\n\n
"
state_type
;
Printf
.
fprintf
output
"
\t
prev_p_c : %s^card;
\n\n
"
state_type
;
graph
.
nodes
graph
.
nodes
|>
List
.
iteri
(
fun
i
_
->
Printf
.
fprintf
output
"
\t
sel_%d : bool;
\n
"
i
);
|>
List
.
iteri
(
fun
i
_
->
Printf
.
fprintf
output
"
\t
sel_%d : bool;
\n
"
i
);
output_string
output
"let
\n
"
;
output_string
output
"let
\n
"
;
output_string
output
"
\t
prev_p_c = initials -> pre(p_c);
\n\n
"
;
output_string
output
"
\t
prev_p_c = initials -> pre(p_c);
\n\n
"
;
graph
.
nodes
graph
.
nodes
|>
List
.
iteri
(
fun
i
_
->
|>
List
.
iteri
(
fun
i
_
->
Printf
.
fprintf
output
Printf
.
fprintf
output
"
\t
sel_%d = false -> boolred<<1,%s,%s>>(p[%d]);
\n
"
"
\t
sel_%d = false -> boolred<<1,%s,%s>>(p[%d]);
\n
"
i
action_number
action_number
i
);
i
action_number
action_number
i
);
let
index_of_id
=
make_index
graph
in
let
index_of_id
=
make_index
graph
in
graph
.
nodes
graph
.
nodes
|>
List
.
iteri
(
fun
i
n
->
|>
List
.
iteri
(
fun
i
n
->
let
algo
=
algo_name
n
in
let
algo
=
algo_name
n
in
let
neighbors
=
graph
.
succ
n
.
id
|>
List
.
map
(
fun
(
_
,
id
)
->
index_of_id
id
)
in
let
neighbors
=
graph
.
succ
n
.
id
|>
List
.
map
(
fun
(
_
,
id
)
->
index_of_id
id
)
in
let
deg
=
List
.
length
neighbors
in
let
deg
=
List
.
length
neighbors
in
let
nl
=
sprint_neighbor_list
neighbors
"p_c"
in
let
nl
=
sprint_neighbor_list
neighbors
"p_c"
in
let
pnl
=
sprint_neighbor_list
neighbors
"prev_p_c"
in
let
pnl
=
sprint_neighbor_list
neighbors
"prev_p_c"
in
Printf
.
fprintf
output
Printf
.
fprintf
output
"
\n\t
p_c[%d] =
\n\t\t
if not sel_%d then prev_p_c[%d]
\n\t\t
else "
"
\n\t
p_c[%d] =
\n\t\t
if not sel_%d then prev_p_c[%d]
\n\t\t
else "
i
i
i
;
i
i
i
;
if
!
clock
then
Printf
.
fprintf
output
if
!
clock
then
Printf
.
fprintf
output
"current(%s_step<<%d>>(
\n\t\t\t
prev_p_c[%d],
\n\t\t\t
%s,
\n\t\t\t
dot2lus_action_of_activation(p[%d])
\n\t\t
) when sel_%d);
\n
"
"current(%s_step<<%d>>(
\n\t\t\t
prev_p_c[%d],
\n\t\t\t
%s,
\n\t\t\t
dot2lus_action_of_activation(p[%d])
\n\t\t
) when sel_%d);
\n
"
algo
deg
i
pnl
i
i
algo
deg
i
pnl
i
i
else
Printf
.
fprintf
output
else
Printf
.
fprintf
output
"%s_step<<%d>>(
\n\t\t\t
prev_p_c[%d],
\n\t\t\t
%s,
\n\t\t\t
dot2lus_action_of_activation(p[%d])
\n\t\t
);
\n
"
"%s_step<<%d>>(
\n\t\t\t
prev_p_c[%d],
\n\t\t\t
%s,
\n\t\t\t
dot2lus_action_of_activation(p[%d])
\n\t\t
);
\n
"
algo
deg
i
pnl
i
;
algo
deg
i
pnl
i
;
Printf
.
fprintf
output
Printf
.
fprintf
output
"
\t
Enab_p[%d] = %s_enable<<%d>>(p_c[%d], %s);
\n
"
"
\t
Enab_p[%d] = %s_enable<<%d>>(p_c[%d], %s);
\n
"
i
algo
deg
i
nl
);
i
algo
deg
i
nl
);
output_string
output
"tel;
\n
"
output_string
output
"tel;
\n
"
let
dot2lus
dotfile
lusfile
=
let
dot2lus
dotfile
lusfile
=
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment