Commit 68491791 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

simplification of Ks (esp. for FresStates)

parent d3f7aa65
......@@ -433,7 +433,7 @@ struct
function
| ExprBin(op, e1, e2) -> ("(" ^ (asp_of_state_expr s e1) ^ (asp_of_exprop2 op) ^ (asp_of_state_expr s e2) ^ ")")
| ExprVar(v) -> (if s = 0 then "" else "S" ^ (string_of_int s) ^ "X") ^ (BRN.asp_of_var v) (* TODO: Énumération préalable des variables ? *)
| ExprParam(v, l) -> ((if s = 0 then "" else "S" ^ (string_of_int s)) ^ "K_" ^ BRN.asp_of_var v ^ "_" ^ (string_of_int (index (List.nth paramlist (index BRN.varlist v)) (List.sort BRN.multcompare l))))
| ExprParam(v, l) -> ("K_" ^ BRN.asp_of_var v ^ "_" ^ (string_of_int (index (List.nth paramlist (index BRN.varlist v)) (List.sort BRN.multcompare l))))
| ExprConst(i) -> string_of_int i ;;
let asp_of_expr = asp_of_state_expr 0 ;;
......@@ -587,14 +587,18 @@ struct
let rec power x i = if i = 0 then 1 else x * power x (i - 1) in
let rec from_up_to n m = if n > m then [] else n :: (from_up_to (n + 1) m) in
let asp_of_state_var s v = (if s = 0 then "" else "S" ^ (string_of_int s) ^ "X") ^ (BRN.asp_of_var v) in
let asp_of_state_param s p = let (v, n) = p in (if s = 0 then "" else "S" ^ (string_of_int s)) ^ "K_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) in
let asp_of_state_param p = let (v, n) = p in "K_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) in
let param_enum_var v = List.fold_right (fun n l -> (v, n) :: l) (from_up_to 0 ((power 2 (List.length (BRNinfo.getpredec v))) - 1)) [] in
let param_enum = List.fold_right (fun v l -> (param_enum_var v) @ l) BRN.varlist [] in
let vars_enum s = ((string_of_list (asp_of_state_var s) "," BRN.varlist) ^ "," ^ (string_of_list (asp_of_state_param s) "," param_enum)) in
let hard_state_enum s = ((if s = 0 then "main_" else "") ^ "state(" ^ (vars_enum s) ^ ")") in
let soft_state_enum s = if s = 0 then "" else (hard_state_enum s) ^ ", " in
(* let vars_enum s = ((string_of_list (asp_of_state_var s) "," BRN.varlist) ^ "," ^ (string_of_list (asp_of_state_param s) "," param_enum)) in *)
(* let hard_state_enum s = ((if s = 0 then "main_" else "") ^ "state(" ^ (vars_enum s) ^ ")") in
let soft_state_enum s = if s = 0 then "" else ("state(" ^ (string_of_list (asp_of_state_var s) "," BRN.varlist) ^ ")") ^ ", " in *)
let state_enum s = ((if s = 0 then "main_" else "") ^ "state(" ^ (string_of_list (asp_of_state_var s) "," BRN.varlist) ^ ")") in
let soft_state_enum s = if s = 0 then "" else ((state_enum s) ^ ", ") in
let params_enum = ("params(" ^ (string_of_list asp_of_state_param "," param_enum) ^ ")") in
let iatom = ref (-1) in
let nextatom s = iatom := !iatom + 1 ; "prop" ^ (string_of_int !iatom) ^ (if s = 0 then "" else "(" ^ (vars_enum s) ^ ")") in
let nextatom s = iatom := !iatom + 1 ; "prop" ^ (string_of_int !iatom) ^
(if s = 0 then "" else "(" ^ (string_of_list (asp_of_state_var s) "," BRN.varlist) ^ ")") in
let istate = ref (0) in
let nextstate () = istate := !istate + 1 ; !istate in
let rec write_atom_state out f s =
......@@ -618,7 +622,7 @@ struct
ncurrent ^ " :- " ^ (soft_state_enum s) ^ "not " ^ nf1 ^ ".\n")
) ; ncurrent)
| Rel(op, e1, e2) -> (let ncurrent = nextatom s in
output_string out (ncurrent ^ " :- " ^ (hard_state_enum s) ^ ", " ^
output_string out (ncurrent ^ " :- " ^ (state_enum s) ^ ", " ^ params_enum ^ ", " ^
(asp_of_state_expr s e1) ^ " " ^ (asp_of_relop2 op) ^ " " ^ (asp_of_state_expr s e2) ^ ".\n")
; ncurrent)
| FreshState(f) -> (let ncurrent = nextatom s in
......@@ -626,7 +630,7 @@ struct
let ns = nextstate () in
let nf2 = write_atom_state out f ns in
output_string out (ncurrent ^ " :- not " ^ nf1 ^ ".\n") ;
output_string out (nf1 ^ " :- " ^ (hard_state_enum ns) ^ ", not " ^ nf2 ^ ".\n")
output_string out (nf1 ^ " :- " ^ (state_enum ns) ^ ", not " ^ nf2 ^ ".\n")
; ncurrent) in
let write_atoms out f =
output_string out ("main_state :- " ^ write_atom_state out f 0 ^ ".\n") ;
......@@ -642,20 +646,40 @@ struct
(from_up_to 0 ((power 2 (List.length (BRNinfo.getpredec v))) - 1))
)) BRN.varlist ;
output_string out "\n" ;
output_string out ((hard_state_enum 0) ^ " :- ") ;
List.iter (fun v -> output_string out ("var_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ "), ")) BRN.varlist ;
output_string out ((state_enum 0) ^ " :- ") ;
output_string out (string_of_list (fun v -> "var_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ ")") ", " BRN.varlist) ;
output_string out ".\n\n" ;
output_string out ("state(" ^ (string_of_list asp_of_var "," BRN.varlist) ^ ") :- ") ;
output_string out (string_of_list (fun v -> "varbound_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ ")") ", " BRN.varlist) ;
output_string out ".\n\n" ;
output_string out (params_enum ^ " :- ") ;
output_string out (string_of_list
(fun c -> let (v, n) = c in "param_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) ^ "(K_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) ^ ")")
", " param_enum) ;
output_string out ".\n\n" ;
output_string out ("state(" ^ (vars_enum 0) ^ ") :- ") ;
List.iter (fun v -> output_string out ("varbound_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ "), ")) BRN.varlist ;
(* output_string out ((hard_state_enum 0) ^ " :- ") ;
List.iter (fun v -> output_string out ("var_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ "), ")) BRN.varlist ;
output_string out (string_of_list
(fun c -> let (v, n) = c in "param_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) ^ "(K_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) ^ ")")
", " param_enum) ;
output_string out ".\n\n" ; in
output_string out ".\n\n" ; *)
(* output_string out ("state(" ^ (string_of_list (asp_of_state_var 0) "," BRN.varlist) ^ ") :- ") ;
output_string out (string_of_list (fun v -> "varbound_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ ")") ", " BRN.varlist) ;
(* List.iter (fun v -> output_string out ("varbound_" ^ (asp_of_var v) ^ "(" ^ (asp_of_var v) ^ "), ")) BRN.varlist ; *)
(* output_string out (string_of_list
(fun c -> let (v, n) = c in "param_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) ^ "(K_" ^ (asp_of_var v) ^ "_" ^ (string_of_int n) ^ ")")
", " param_enum) ; *)
output_string out ".\n\n" ; in *)
in
let write_footer out =
output_string out ("\n#hide.\n#show main_state/" ^ (string_of_int ((List.length BRN.varlist) + (List.length param_enum))) ^ ".\n") in
output_string out ("\n#hide.\n#show main_state/" ^ (string_of_int (List.length BRN.varlist)) ^
".\n#show params/" ^ (string_of_int (List.length param_enum)) ^ ".\n\n") in
write_header out ; write_atoms out f ; write_footer out ;;
(** Écriture dans un fichier *)
......@@ -705,7 +729,7 @@ print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post1) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline (string_of_formula pre1) ;;
print_endline "*********************************************************" ;;
write_example pre1 "toyex-incrdecr.lp" ;;
(* OK : Une solution : A = 0, k_a,{} = 0, k_a,{m} = 1 *)
let prog2 = While(PropConst True, Rel(Eq, ExprVar A, ExprConst 0), Seq(Incr A, Decr A)) ;;
......@@ -720,7 +744,7 @@ 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 "*****************************************************" ;;
write_example pre2 "toyex-while.lp" ;;
(* OK : Une solution : A = 0, k_a,{} = 0, k_a,{m} = 1 *)
let prog3 = If(Rel(Eq, ExprVar A, ExprConst 1),
......@@ -737,43 +761,59 @@ print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post3) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline (string_of_formula pre3) ;;
print_endline "********************************************" ;;
(* OK : Deux solutions : A = 0/1, k_a,{} = 0, k_a,{m} = 1 *)
write_example pre1 "toyex-incrdecr.lp" ;;
write_example pre2 "toyex-while.lp" ;;
write_example pre3 "toyex-complex.lp" ;;
(* OK : Deux solutions : A = 0/1, k_a,{} = 0, k_a,{m} = 1 *)
*)
(** Exemple du papier *)
let prog1 = Seq(Seq(Incr B, Incr C), Decr B) ;;
let post1 = Rel(Eq, ExprVar B, ExprConst 0) ;;
(* let pre1 = wp prog1 post1 ;; (* Sans raffinage *) *)
let pre1 = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar A, ExprConst 1)) ;; (* Avec raffinage *)
print_endline "***************************" ;;
print_endline "*** Exemple 1 du papier ***" ;;
print_endline "* Programme *" ;;
print_endline "***************************" ;;
print_endline "*** Programme ***" ;;
print_endline (string_of_prog_indent prog1) ;;
print_endline "* Post-condition *" ;;
print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post1) ;;
print_endline "* Plus faible pré-condition calculée *" ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline (string_of_formula pre1) ;;
print_endline "***************************" ;;
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 ;;
print_endline "***************************" ;;
print_endline "*** Exemple 2 du papier ***" ;;
print_endline "***************************" ;;
print_endline "*** Programme ***" ;;
print_endline (string_of_prog_indent prog2) ;;
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 "" ;;
write_example pre2 "simpleex2.lp" ;;
(* OK : Aucune solution *)
let prog3 = Incr C ;;
let post3 = post1 ;;
let pre3 = wp prog3 post3 ;;
print_endline "***************************" ;;
print_endline "*** Exemple 3 du papier ***" ;;
print_endline "***************************" ;;
print_endline "*** Programme ***" ;;
print_endline (string_of_prog_indent prog3) ;;
print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post3) ;;
print_endline "*** Plus faible pré-condition calculée ***" ;;
print_endline (string_of_formula pre3) ;;
print_endline "" ;;
write_example pre3 "simpleex3.lp" ;;
(* OK : 128 solutions *)
let prog4 = While(Rel(LT, ExprVar B, ExprConst 1), PropConst True, Exists(Exists(Exists(Incr B, Decr B), Incr C), Decr C)) ;;
......@@ -782,8 +822,16 @@ let post4 = Rel(Eq, ExprVar B, ExprConst 1) ;;
let pre4 = PropBin(And, wp prog4 post4, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage *)
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))) ;;
print_endline "***************************************************" ;;
print_endline "*** Exemple 4 du papier : While avec I ≡ (True) ***" ;;
print_endline "***************************************************" ;;
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 (string_of_formula pre4) ;;
print_endline "" ;;
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)) ;;
......@@ -792,15 +840,18 @@ let post4b = Rel(Eq, ExprVar B, ExprConst 1) ;;
let pre4b = PropBin(And, wp prog4b post4b, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage *)
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))) ;;
print_endline "****************************************************" ;;
print_endline "*** Exemple 4 du papier : While avec I ≡ (a = 0) ***" ;;
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 (string_of_formula pre4b) ;;
print_endline "" ;;
write_example pre4b "simpleex4b.lp" ;;
(* OK : Aucune solution (avec raffinage) *)
write_example pre1 "simpleex1.lp" ;;
write_example pre2 "simpleex2.lp" ;;
write_example pre3 "simpleex3.lp" ;;
write_example pre4 "simpleex4.lp" ;;
write_example pre4b "simpleex4b.lp" ;;
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
......@@ -822,7 +873,9 @@ print_endline (string_of_formula prepl1) ;;
print_endline "***************************" ;;
write_example prepl1 "phagelex1.lp" ;;
(* Mauvais : explosion combinatoire => trop de résultats *)
*)
print_endline " *****" ;;
asp_params () ;;
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