Revision d5ec9f63
Added by Pierre-Loïc Garoche about 4 years ago
| src/_tags.in | ||
|---|---|---|
| 23 | 23 |
"tools/stateflow/models": include |
| 24 | 24 |
"tools/stateflow/json-parser": include |
| 25 | 25 |
"tools/importer": include |
| 26 |
"tools/seal": include |
|
| 26 | 27 |
|
| 27 | 28 |
# svn |
| 28 | 29 |
<**/.svn>: -traverse |
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 326 | 326 |
| _ -> assert false (* should have been removed by normalization *) |
| 327 | 327 |
) [] sorted_eqs |
| 328 | 328 |
in |
| 329 |
report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out memories definitions (may takes time)@."); |
|
| 329 |
report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out (guarded) memories definitions (may takes time)@.");
|
|
| 330 | 330 |
(* Printing memories definitions *) |
| 331 | 331 |
report ~level:3 |
| 332 | 332 |
(fun fmt -> |
| 333 | 333 |
Format.fprintf fmt |
| 334 |
"%a"
|
|
| 335 |
(Utils.fprintf_list ~sep:"@."
|
|
| 334 |
"@[<v 0>%a@]@ "
|
|
| 335 |
(Utils.fprintf_list ~sep:"@ "
|
|
| 336 | 336 |
(fun fmt (m,mdefs) -> |
| 337 | 337 |
Format.fprintf fmt |
| 338 |
"%s -> @[<v 0>[%a@] ]@."
|
|
| 338 |
"%s -> [@[<v 0>%a@] ]@ "
|
|
| 339 | 339 |
m |
| 340 | 340 |
(Utils.fprintf_list ~sep:"@ " |
| 341 | 341 |
pp_guard_expr) mdefs |
| ... | ... | |
| 347 | 347 |
report ~level:3 |
| 348 | 348 |
(fun fmt -> |
| 349 | 349 |
Format.fprintf fmt |
| 350 |
"Init:@.%a@.Step@.%a"
|
|
| 351 |
(Utils.fprintf_list ~sep:"@."
|
|
| 350 |
"@[<v 0>Init:@ %a@ Step@ %a@]@ "
|
|
| 351 |
(Utils.fprintf_list ~sep:"@ "
|
|
| 352 | 352 |
(fun fmt (m,mdefs) -> |
| 353 | 353 |
Format.fprintf fmt |
| 354 |
"%s -> @[<v 0>[%a@] ]@."
|
|
| 354 |
"%s -> @[<v 0>[%a@] ]@ "
|
|
| 355 | 355 |
m |
| 356 | 356 |
(Utils.fprintf_list ~sep:"@ " |
| 357 | 357 |
pp_guard_expr) mdefs |
| 358 | 358 |
)) |
| 359 | 359 |
init_defs |
| 360 |
(Utils.fprintf_list ~sep:"@."
|
|
| 360 |
(Utils.fprintf_list ~sep:"@ "
|
|
| 361 | 361 |
(fun fmt (m,mdefs) -> |
| 362 | 362 |
Format.fprintf fmt |
| 363 |
"%s -> @[<v 0>[%a@] ]@."
|
|
| 363 |
"%s -> @[<v 0>[%a@] ]@ "
|
|
| 364 | 364 |
m |
| 365 | 365 |
(Utils.fprintf_list ~sep:"@ " |
| 366 | 366 |
pp_guard_expr) mdefs |
| src/tools/seal/seal_verifier.ml | ||
|---|---|---|
| 4 | 4 |
|
| 5 | 5 |
let active = ref false |
| 6 | 6 |
|
| 7 |
(* TODO |
|
| 8 |
|
|
| 9 |
- build the output function: for the moment we slice the node with |
|
| 10 |
its memories, building the function updating the memory. We will |
|
| 11 |
need later the output function, using inputs and memories to |
|
| 12 |
compute the output. A way to do this would be to declared memories |
|
| 13 |
as input, remove their definitions, and slice the node with its |
|
| 14 |
outputs. This should clean up unnecessary internal variables and |
|
| 15 |
give us the output function. |
|
| 16 |
|
|
| 17 |
- compute the dimension of the node (nb of memories) |
|
| 18 |
|
|
| 19 |
- if the updates are all linear or affine, provide the update as a |
|
| 20 |
matrix rather then a polynomial. Check if this is simpler to do |
|
| 21 |
here or in matlab. |
|
| 22 |
|
|
| 23 |
- analyzes require bounds on inputs or sometimes target property |
|
| 24 |
over states. These could be specified as node annotations: eg |
|
| 25 |
- /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) |
|
| 26 |
to specify that the inputs are constrained by a semialgebraic |
|
| 27 |
set (p,b) such as p(inputs) <= b |
|
| 28 |
- /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. |
|
| 29 |
To be defined depending on needs. |
|
| 30 |
- /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 <= 2 is |
|
| 31 |
the property to prove |
|
| 32 |
|
|
| 33 |
*) |
|
| 34 |
|
|
| 7 | 35 |
(* Select the appropriate node, should have been inlined already and |
| 8 | 36 |
extract update/output functions. *) |
| 9 | 37 |
let seal_run basename prog machines = |
Also available in: Unified diff
Minor modif on seal