Revision d5ec9f63
Added by PierreLoïc Garoche about 4 years ago
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