Commit 6767b472 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

fixed simplification

parent 66d7a2fc
......@@ -714,10 +714,10 @@ let rec simpl_formula f lv lk =
(* Simplification d'une formule *)
match f with
| PropConst(op) -> PropConst(op)
| PropUn(op, f) -> simpl_propop1 op f lv lk
| PropBin(op, f1, f2) -> simpl_propop2 op f1 f2 lv lk
| Rel(op, e1, e2) -> simpl_exprop2 op e1 e2 lv lk
| FreshState(f) -> FreshState(f) and (* TODO: Réfléchir à la simplification de FreshState *)
| PropUn(op, f) -> (* DEBUG print_endline (" === PropUn ===\n" ^ (string_of_formula f) ^ "\n" ^ (string_of_formula (simpl_propop1 op f lv lk))) ; *) simpl_propop1 op f lv lk
| PropBin(op, f1, f2) -> (* DEBUG print_endline (" === PropBin ===\n" ^ (string_of_formula f) ^ "\n" ^ (string_of_formula (simpl_propop2 op f1 f2 lv lk))) ; *) simpl_propop2 op f1 f2 lv lk
| Rel(op, e1, e2) -> (* DEBUG print_endline (" === Rel ===\n" ^ (string_of_formula f) ^ "\n" ^ (string_of_formula (simpl_exprop2 op e1 e2 lv lk))) ; *) simpl_exprop2 op e1 e2 lv lk
| FreshState(f) -> FreshState(f) and (* TODO: Réfléchir à la simplification de FreshState : simplification des paramètres ? *)
(* Simplifications atomiques pour chaque forme de proposition *)
(* Opérateur unaire *)
simpl_propop1 op f lv lk =
......@@ -752,7 +752,7 @@ simpl_propop2_Impl f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(True)
| fs1 -> (match simpl_formula f1 lv lk with
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> PropUn(Neg, fs1)
| fs2 -> PropBin(Impl, fs1, fs2)) ;;
......@@ -1017,13 +1017,6 @@ open ASP ;;
(** Tests sur super_replace *)
(***********************************)
(*** Traitement sur les exemples ***)
(***********************************)
......@@ -1088,9 +1081,9 @@ let and_simplify f lv lk =
let prog1 = Seq(Seq(Incr B, Incr C), Decr B) ;;
let post1 = Rel(Eq, ExprVar B, ExprConst 0) ;;
let pre1_nr = wp prog1 post1 ;; (* Sans raffinage *)
(* let pre1_nr = wp prog1 post1 ;; (* Sans raffinage *) *)
(* let pre1 = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar A, ExprConst 1)) ;; (* Avec raffinage, ancienne implémentation sans simplification *) *)
let pre1 = and_simplify pre1_nr [(A, 1) ; (C, 0) ; (B, 0)] [] ;; (* Avec raffinage et simplification *)
let pre1 = and_simplify (wp prog1 post1) [(A, 1) (* ; (C, 0) ; (B, 0) *)] [] ;; (* Avec raffinage et simplification *)
print_endline "***************************" ;;
print_endline "*** Exemple 1 du papier ***" ;;
print_endline "***************************" ;;
......@@ -1104,7 +1097,6 @@ write_example pre1 "simpleex1.lp" ;;
(* OK : 16 solutions (avec raffinage) *)
(* Contraintes trouvées : a = 1, b = 0, c = 0, k_b,{σ} = 0, k_b,{λ;σ} = 1, k_c,{l} = 1 *)
(*
let prog2 = Seq(Incr B, Decr B) ;;
let post2 = post1 ;;
let pre2 = wp prog2 post2 ;;
......@@ -1117,6 +1109,8 @@ print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post2) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline (string_of_formula pre2) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline (string_of_formula pre2) ;;
write_example pre2 "simpleex2.lp" ;;
(* OK : Aucune solution *)
......@@ -1138,9 +1132,10 @@ write_example pre3 "simpleex3.lp" ;;
let prog4 = While(Rel(LT, ExprVar B, ExprConst 1), PropConst True, Exists(Exists(Exists(Incr B, Decr B), Incr C), Decr C)) ;;
let post4 = Rel(Eq, ExprVar B, ExprConst 1) ;;
(* let pre4 = wp prog4 post4 ;; (* Sans raffinage *) *)
let pre4 = PropBin(And, wp prog4 post4, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage *)
let pre4_oldr = PropBin(And, wp prog4 post4, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage, ancienne implémentation sans simplification *)
Rel(Eq, ExprVar A, ExprConst 1), Rel(Eq, ExprVar B, ExprConst 0)), Rel(Eq, ExprVar C, ExprConst 0)),
Rel(Eq, ExprParam(B, [Sigma]), ExprConst 0)), Rel(Eq, ExprParam(B, [Lambda ; Sigma]), ExprConst 0)), Rel(Eq, ExprParam(C, [L]), ExprConst 0))) ;;
let pre4 = and_simplify (wp prog4 post4) [(A, 1) ; (B, 0) ; (C, 0)] [((B, [Sigma]), 0) ; ((B, [Lambda ; Sigma]), 0) ; ((C, [L]), 0)] ;; (* Avec raffinage et simplification *)
print_endline "***************************************************" ;;
print_endline "*** Exemple 4 du papier : While avec I ≡ (True) ***" ;;
print_endline "***************************************************" ;;
......@@ -1148,33 +1143,34 @@ print_endline "*** Programme ***" ;;
print_endline (string_of_prog_indent prog4) ;;
print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post4) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline "*** Plus faible pré-condition calculée non simplifiée ***" ;;
print_endline (string_of_formula pre4_oldr) ;;
print_endline "*** Plus faible pré-condition calculée raffinée et simplifiée ***" ;;
print_endline (string_of_formula pre4) ;;
write_example pre4 "simpleex4.lp" ;;
(* OK : Aucune solution (avec raffinage) *)
let prog4b = While(Rel(LT, ExprVar B, ExprConst 1), Rel(Eq, ExprVar A, ExprConst 0), Exists(Exists(Exists(Incr B, Decr B), Incr C), Decr C)) ;;
let prog4b = While(Rel(LT, ExprVar B, ExprConst 1), Rel(Eq, ExprVar A, ExprConst 1), Exists(Exists(Exists(Incr B, Decr B), Incr C), Decr C)) ;;
let post4b = Rel(Eq, ExprVar B, ExprConst 1) ;;
(* let pre4b = wp prog4b post4b ;; (* Sans raffinage *) *)
let pre4b = PropBin(And, wp prog4b post4b, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage *)
let pre4b_oldr = PropBin(And, wp prog4b post4b, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage, ancienne implémentation sans simplification *)
Rel(Eq, ExprVar A, ExprConst 1), Rel(Eq, ExprVar B, ExprConst 0)), Rel(Eq, ExprVar C, ExprConst 0)),
Rel(Eq, ExprParam(B, [Sigma]), ExprConst 0)), Rel(Eq, ExprParam(B, [Lambda ; Sigma]), ExprConst 0)), Rel(Eq, ExprParam(C, [L]), ExprConst 0))) ;;
let pre4b = and_simplify (wp prog4b post4b) [(A, 1) ; (B, 0) ; (C, 0)] [((B, [Sigma]), 0) ; ((B, [Lambda ; Sigma]), 0) ; ((C, [L]), 0)] ;; (* Avec raffinage et simplification *)
print_endline "****************************************************" ;;
print_endline "*** Exemple 4 du papier : While avec I ≡ (a = 0) ***" ;;
print_endline "*** Exemple 4 du papier : While avec I ≡ (a = 1) ***" ;;
print_endline "****************************************************" ;;
print_endline "*** Programme ***" ;;
print_endline (string_of_prog_indent prog4b) ;;
print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post4b) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline "*** Plus faible pré-condition calculée non simplifiée ***" ;;
print_endline (string_of_formula pre4b_oldr) ;;
print_endline "*** Plus faible pré-condition calculée raffinée et simplifiée ***" ;;
print_endline (string_of_formula pre4b) ;;
write_example pre4b "simpleex4b.lp" ;;
(* OK : Aucune solution (avec raffinage) *)
(* Essai : résolution sur la post-condition VRAI *)
write_example (PropConst True) "simpleex5.lp" ;;
*)
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
......
Supports Markdown
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