Skip to content

GitLab

Commit 7778193e authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Improvement verification float_quat_of_rmat

parent d435994e
Hide whitespace changes
Inline Side-by-side
Showing with 20 additions and 35 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ 7778193e
......@@ -59,7 +59,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -71,7 +71,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -83,11 +83,11 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.9272,
"steps": 383 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 3.5527,
"steps": 2040 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ 7778193e
......@@ -59,7 +59,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -71,7 +71,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -83,11 +83,11 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.4666,
"steps": 385 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 2.8084,
"steps": 1398 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ 7778193e
......@@ -20,7 +20,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -32,11 +32,11 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.6638,
"steps": 372 } ] } } ] } } ] } } ] } } ]
"time": 11.0712,
"steps": 814 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_complete_a00_max_a11_max_a22_max_trace.json deleted 100644 → 0
View file @ d435994e
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 10. },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ 7778193e
......@@ -69,11 +69,11 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 4.6223,
"steps": 1005 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 13.5863,
"steps": 3572 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/math/pprz_algebra_float.c
View file @ 7778193e
......@@ -646,15 +646,6 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
/*printf("m22 largest\n");*/
}
}
//@ assert \at(rm->m[0], Pre) == rm->m[0];
//@ assert \at(rm->m[1], Pre) == rm->m[1];
//@ assert \at(rm->m[2], Pre) == rm->m[2];
//@ assert \at(rm->m[3], Pre) == rm->m[3];
//@ assert \at(rm->m[4], Pre) == rm->m[4];
//@ assert \at(rm->m[5], Pre) == rm->m[5];
//@ assert \at(rm->m[6], Pre) == rm->m[6];
//@ assert \at(rm->m[7], Pre) == rm->m[7];
//@ assert \at(rm->m[8], Pre) == rm->m[8];
}
......
sw/airborne/math/pprz_algebra_float.h
View file @ 7778193e
......@@ -898,14 +898,14 @@ extern void float_quat_of_orientation_vect(struct FloatQuat *q, const struct Flo
behavior a11_max:
assumes trace(rm) <= 0
&& RMAT_ELMT(*rm, 1, 1) > RMAT_ELMT(*rm, 0, 0)
&& RMAT_ELMT(*rm, 1, 1) >= RMAT_ELMT(*rm, 0, 0)
&& RMAT_ELMT(*rm, 1, 1) > RMAT_ELMT(*rm, 2, 2);
ensures l_FloatQuat_of_RMat_1_max_t(rm) == l_Quat_of_FloatQuat(q);
behavior a22_max:
assumes trace(rm) <= 0
&& RMAT_ELMT(*rm, 2, 2) > RMAT_ELMT(*rm, 0, 0)
&& RMAT_ELMT(*rm, 2, 2) > RMAT_ELMT(*rm, 1, 1);
&& RMAT_ELMT(*rm, 2, 2) >= RMAT_ELMT(*rm, 0, 0)
&& RMAT_ELMT(*rm, 2, 2) >= RMAT_ELMT(*rm, 1, 1);
ensures l_FloatQuat_of_RMat_2_max_t(rm) == l_Quat_of_FloatQuat(q);
disjoint behaviors;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment