Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
L
lustre-v6
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
lustre-v6
Commits
a3b50883
Commit
a3b50883
authored
1 year ago
by
erwan
Browse files
Options
Downloads
Patches
Plain Diff
Add a missing file
parent
e6b5c982
No related branches found
No related tags found
No related merge requests found
Pipeline
#140836
passed
1 year ago
Stage: build
Stage: test
Changes
1
Pipelines
2
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
lib/lic2smv.ml
+110
-0
110 additions, 0 deletions
lib/lic2smv.ml
with
110 additions
and
0 deletions
lib/lic2smv.ml
0 → 100644
+
110
−
0
View file @
a3b50883
(* Time-stamp: <modified the 09/06/2023 (at 16:18) by Erwan Jahier> *)
(** Generate smv programs
- simple equations and (memoryless) function calls are put in the ASSIGN section
- asserts are put in the INVAR section
- node calls (with memory) are put in the TRANS section
- if the first boolean output is named ok, the SPEC section contains
AG ok
*)
let
(
string_of_soc_key
:
Soc
.
key
->
string
)
=
Soc2cIdent
.
get_soc_name
(* XXX add a CLi argument ? *)
let
integer
=
"0..100"
let
rec
(
type_to_string_gen
:
bool
->
Data
.
t
->
string
)
=
fun
alias
v
->
let
str
=
match
v
with
|
String
->
"string"
|
Bool
->
"boolean"
|
Int
->
integer
|
Real
->
"real"
|
Extern
_s
->
"string"
(* what else should be done? *)
(* | Enum (s, sl) -> "enum " ^ s ^ " {" ^ (String.concat ", " sl) ^ "}" *)
|
Enum
(
s
,
_sl
)
->
s
|
Struct
(
sid
,_
)
->
sid
|
Array
(
ty
,
sz
)
->
Printf
.
sprintf
"%s^%d"
(
type_to_string_gen
alias
ty
)
sz
|
Alpha
nb
->
(* On génère des "types" à la Caml : 'a, 'b, 'c, etc. *)
let
a_value
=
Char
.
code
(
'
a'
)
in
let
z_value
=
Char
.
code
(
'
z'
)
in
let
str
=
if
(
nb
>=
0
&&
nb
<=
(
z_value
-
a_value
))
then
(
"'"
^
(
Char
.
escaped
(
Char
.
chr
(
a_value
+
nb
))))
else
(
"'a"
^
(
string_of_int
nb
))
in
str
|
Alias
(
n
,
t
)
->
if
alias
then
n
else
type_to_string_gen
alias
t
in
str
let
(
type_to_string
:
Lic
.
type_
->
string
)
=
function
|
Bool_type_eff
->
"boolean"
|
Int_type_eff
->
integer
|
Real_type_eff
->
assert
false
|
External_type_eff
(
_name
)
->
assert
false
|
Abstract_type_eff
(
_name
,
_t
)
->
assert
false
|
Enum_type_eff
(
name
,
_
)
->
Lv6Id
.
no_pack_string_of_long
name
|
Array_type_eff
(
_ty
,
_sz
)
->
assert
false
|
Struct_type_eff
(
_name
,
_
)
->
assert
false
|
TypeVar
_
->
assert
false
let
(
type_to_string_alias
:
Data
.
t
->
string
)
=
type_to_string_gen
true
open
Printf
open
Lic
let
(
f
:
Lv6MainArgs
.
t
->
LicPrg
.
t
->
Lv6Id
.
idref
option
->
unit
)
=
fun
opt
licprg
main_node
->
let
main_node_exp
=
LicPrg
.
get_main_node_exp
licprg
main_node
in
let
_base0
=
if
opt
.
outfile
<>
""
then
opt
.
outfile
else
let
file
=
List
.
hd
opt
.
infiles
in
try
(
Filename
.
chop_extension
(
Filename
.
basename
file
))
with
_
->
print_string
(
"*** Error: '"
^
file
^
"'is a bad file name.
\n
"
);
exit
2
in
let
base0
=
Filename
.
chop_extension
(
Filename
.
basename
(
Lxm
.
file
main_node_exp
.
lxm
))
in
let
dir
=
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
dir
in
let
base
=
Filename
.
concat
dir
base0
in
let
smv_file
=
base
^
".smv"
in
let
oc
=
open_out
smv_file
in
let
inputs
=
main_node_exp
.
inlist_eff
in
let
outputs
=
main_node_exp
.
outlist_eff
in
let
locals
=
match
main_node_exp
.
loclist_eff
with
Some
l
->
l
|
None
->
[]
in
let
p
=
Printf
.
fprintf
oc
"%s"
in
let
pn
=
Printf
.
fprintf
oc
"%s
\n
"
in
Lv6util
.
entete
oc
"--"
""
;
pn
"MODULE main
VAR"
;
p
""
;
let
decl_var
v
=
Printf
.
fprintf
oc
" %s: %s;
\n
"
v
.
var_name_eff
(
type_to_string
v
.
var_type_eff
)
in
List
.
iter
decl_var
inputs
;
List
.
iter
decl_var
outputs
;
List
.
iter
decl_var
locals
;
pn
"INVAR"
;
pn
"ASSIGN"
;
pn
(
sprintf
"SPEC AG %s;"
(
List
.
hd
outputs
)
.
var_name_eff
);
pn
"TRANS"
;
close_out
oc
;
Printf
.
eprintf
"W: %s has been generated.
\n
%!"
smv_file
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