Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Folschette Maxime
Hoare-fol
Commits
4b705bc4
Commit
4b705bc4
authored
Nov 05, 2012
by
Maxime Folschette
Browse files
switched back to SimpleExample
parent
c88fd934
Changes
1
Hide whitespace changes
Inline
Side-by-side
main.ml
View file @
4b705bc4
...
...
@@ -139,7 +139,6 @@ struct
end ;;
*)
(*
(** Exemple du papier *)
module
SimpleExample
=
struct
...
...
@@ -175,8 +174,8 @@ struct
let
multcompare
m1
m2
=
compare
(
asp_of_mult
m1
)
(
asp_of_mult
m2
)
;;
end
;;
*)
(*
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
module PhageLambda =
struct
...
...
@@ -225,6 +224,7 @@ struct
let multcompare m1 m2 =
compare (asp_of_mult m1) (asp_of_mult m2) ;;
end ;;
*)
(*
(** Cycle circadien (depuis projet Circlock) *)
...
...
@@ -304,8 +304,8 @@ end ;;
(** Sélection du BRN à considérer *)
(* module BRN = ToyExample ;; *)
(*
module BRN = SimpleExample ;;
*)
module
BRN
=
PhageLambda
;;
module
BRN
=
SimpleExample
;;
(*
module BRN = PhageLambda ;;
*)
(* module BRN = Circlock ;; *)
...
...
@@ -380,7 +380,6 @@ struct
end ;;
*)
(*
(** Exemple du papier *)
module
SimpleExampleInfo
=
struct
...
...
@@ -401,8 +400,8 @@ struct
|
B
->
[
Lambda
;
Sigma
]
|
C
->
[
L
]
;;
end
;;
*)
(*
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
module PhageLambdaInfo =
struct
...
...
@@ -430,6 +429,7 @@ struct
| CII -> [M3 ; M4 ; M8]
| N -> [M6 ; M7] ;;
end ;;
*)
(*
(** Cycle circadien (depuis projet Circlock) *)
...
...
@@ -472,8 +472,8 @@ end ;;
(** Sélection des informations du BRN à considérer *)
(* module BRNinfo = ToyExampleInfo ;; *)
(*
module BRNinfo = SimpleExampleInfo ;;
*)
module
BRNinfo
=
PhageLambdaInfo
;;
module
BRNinfo
=
SimpleExampleInfo
;;
(*
module BRNinfo = PhageLambdaInfo ;;
*)
(* module BRNinfo = CirclockInfo ;; *)
...
...
@@ -984,12 +984,12 @@ write_example pre3 "toyex-complex.lp" ;;
(** Exemple du papier *)
(*
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 = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar A, ExprConst 1)) ;; (* Avec raffinage
,
ancienne
implémentation
sans simplification *)
*)
let pre1 = and_simplify (wp prog1 post1) [(A, 1)
(*
; (C, 0) ; (B, 0)
*)
] [] ;; (* Avec raffinage et simplification *)
let
pre1
_ns
=
PropBin
(
And
,
wp
prog1
post1
,
Rel
(
Eq
,
ExprVar
A
,
ExprConst
1
))
;;
(* Avec raffinage
à l'
ancienne
et
sans 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
"***************************"
;;
...
...
@@ -997,8 +997,11 @@ print_endline "*** Programme ***" ;;
print_endline
(
string_of_prog_indent
prog1
)
;;
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 raffinée mais sans simplification ***"
;;
print_endline
(
string_of_formula
pre1_ns
)
;;
print_endline
"*** Plus faible pré-condition calculée raffinée et avec simplification ***"
;;
print_endline
(
string_of_formula
pre1
)
;;
write_example
pre1_ns
"simpleex1_ns.lp"
;;
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 *)
...
...
@@ -1015,8 +1018,6 @@ 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 *)
...
...
@@ -1076,11 +1077,11 @@ 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) *)
*)
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
(*
(*Qa = N+; CII+; CI+; CI+; N−; CII−
Ra ≡ (CI = 2 ∧ Cro = 0 ∧ CII = 0 ∧ N = 0)*)
...
...
@@ -1109,6 +1110,7 @@ print_endline "***************************" ;;
write_example prepl1_nr "phagelex1_nr.lp" ;;
write_example prepl1 "phagelex1.lp" ;;
(* Mauvais : explosion combinatoire => trop de résultats *)
*)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment