### Profile

« Previous | Next »

## Revision d5ec9f63

Minor modif on seal

View differences:

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