Add new plugin for polynomial inequalities (using OSDP) #499
Conversation
|
The commit message contains the reference of the related publication and an example of goal that is now solved by Alt-Ergo. Should it be added to some non regression test? Also note that this does not add any dependency to the currently existing opam packages for alt-ergo. Only the new alt-ergo-osdp packages depends on osdp (which has a non trivial depext). |
ploc
force-pushed
the
osdp
branch
2 times, most recently
from
99a6d57
to
9cdc3c5
Compare
|
Updated opam osdp dependency to 1.1.0 which has been released (cf ocaml/opam-repository@c353c5a) |
|
That's very impressive ! We'll try and review as soon as possible, ^^ |
ploc
force-pushed
the
osdp
branch
3 times, most recently
from
76cf4dc
to
d25b3d9
Compare
|
Issues in CI workflows were caused by the recent release of Cmdliner (1.1.0). I don't know why it doesn't show up in the CI of the "next" branch. I added the explicit version to Cmdliner 1.0.4 in the dune-project and .opam files (see ploc@76cf4dc). |
It doesn't show up in the Ci runs of |
|
Impact is significant ! Most uses of Cmdliner in Alt-ergo rely on the deprecated Term module. It causes many warning and one error in the last line of the module. |
|
Indeed, I'll try and fix that in |
|
The |
|
@ploc could you remove the last commit? |
|
(feel free to add |
|
Hi @Gbury , what's the status? Do you need us to do anything? |
|
my apologies, I've been busy with another project recently. I'll try and look at this PR in detail (including the thing about plugins) next week. |
|
@Gbury it seems we'll both attend JFLA in a few weeks. If you want, we could take some time there to look together at the code (and I could take the opportunity to improve comments as the code may sometimes be a bit dry). |
|
Any news since JFLA ? I am still interested in the merge! |
|
We talked a bit with @proux01 during the JFLA. There are a few things left to do before we can merge:
|
|
Sorry, I'm ridiculously late here. I hope to complete my tasks in the coming weeks. |
|
So finally, here it is: https://github.com/proux01/alt-ergo/tree/osdp @Gbury said:
done
done
Sorry, don't remember that but feel free to resend it, I'll have a look. P.S.: @ploc can't push on your branch, you probably have to do something like: |
This is the plugin presented in the following paper:
A Non-linear Arithmetic Procedure for Control-Command Software Verification,
Pierre Roux, Mohamed Iguernlala, Sylvain Conchon, TACAS 2018
In particular, it enables to solve goals like:
logic v__0 : real
logic v_x0 : real
logic v_x1 : real
logic v_x2 : real
goal g:
6.04 * v_x0 * v_x0 + (- (9.65)) * v_x0 * v_x1 + (- (2.26)) * v_x0 * v_x2
+ 11.36 * v_x1 * v_x1 + 2.67 * v_x1 * v_x2 + 3.76 * v_x2 * v_x2 <= 1.0
and v__0 <= 1.0 and (- (1.0)) <= v__0
-> 6.04
* (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
+ 0.0237 * v__0)
* (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
+ 0.0237 * v__0)
+ (- (9.65))
* (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
+ 0.0237 * v__0)
* ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
+ 0.0143 * v__0)
+ (- (2.26))
* (0.9379 * v_x0 + (- (0.0381)) * v_x1 + (- (0.0414)) * v_x2
+ 0.0237 * v__0)
* (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
+ 11.36
* ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
+ 0.0143 * v__0)
* ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
+ 0.0143 * v__0)
+ 2.67
* ((- (0.0404)) * v_x0 + 0.968 * v_x1 + (- (0.0179)) * v_x2
+ 0.0143 * v__0)
* (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
+ 3.76
* (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
* (0.0142 * v_x0 + (- (0.0197)) * v_x1 + 0.9823 * v_x2 + 0.0077 * v__0)
<= 1.0
that are out of reach of most SMT solvers.
This goals come from verification of the following linear controller:
typedef struct { double x0, x1, x2; } state;
/*@ predicate inv(state *s) = 6.04 * s->x0 * s->x0 - 9.65 * s->x0 * s->x1
@ - 2.26 * s->x0 * s->x2 + 11.36 * s->x1 * s->x1
@ + 2.67 * s->x1 * s->x2 + 3.76 * s->x2 * s->x2 <= 1; */
/*@ requires \valid(s) && inv(s) && -1 <= in0 <= 1;
@ ensures inv(s); */
void step(state *s, double in0) {
double pre_x0 = s->x0, pre_x1 = s->x1, pre_x2 = s->x2;
s->x0 = 0.9379 * pre_x0 - 0.0381 * pre_x1 - 0.0414 * pre_x2 + 0.0237 * in0;
s->x1 = -0.0404 * pre_x0 + 0.968 * pre_x1 - 0.0179 * pre_x2 + 0.0143 * in0;
s->x2 = 0.0142 * pre_x0 - 0.0197 * pre_x1 + 0.9823 * pre_x2 + 0.0077 * in0;
}
|
|
The purpose of this PR is to add a new plugin based on semi-definite programming (SDP, aka convex optimization). It solves problems involving polynomial inequalities which cannot be solved with alt-ergo today. It relies on the opam package OSDP which provides the interface to SDP solvers.
It is developed as a plugin, following the structure of fm-simplex plugin.
Usage:
alt-ergo --polynomial-plugin osdp-plugin.cmxs file.ae
Details
With @proux01, we commit to maintain the package alt-ergo-osdp and keep it in sync with alt-ergo, as well as OSDP.
Last, there is an issue with the loading order of modules for plugins. We solved this for our inequalities plugin, and will prepare a separate PR for fm-simplex which has the same issue (it is not currently properly loaded).