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
c88fd934
Commit
c88fd934
authored
Nov 05, 2012
by
Maxime Folschette
Browse files
fix and update phage lambda example
parent
edab1e7b
Changes
1
Hide whitespace changes
Inline
Side-by-side
main.ml
View file @
c88fd934
...
...
@@ -139,11 +139,12 @@ struct
end ;;
*)
(*
(** Exemple du papier *)
module SimpleExample =
struct
type var = A | B | C ;;
type
mult
=
L
|
Lambda
|
Sigma
;;
(* TODO: Analyse des formules traitées pour générer une varlist automatique et minimale *)
type mult = L | Lambda | Sigma ;; (* TODO: Analyse des formules traitées pour générer une varlist automatique et minimale
?
*)
(* TODO bis: Même chose pour les paramètres *)
let varlist = [A ; B ; C] ;;
let varequals v1 v2 =
...
...
@@ -174,8 +175,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
...
...
@@ -224,7 +225,6 @@ 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,6 +380,7 @@ struct
end ;;
*)
(*
(** Exemple du papier *)
module SimpleExampleInfo =
struct
...
...
@@ -400,8 +401,8 @@ struct
| B -> [Lambda ; Sigma]
| C -> [L] ;;
end ;;
*)
(*
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
module
PhageLambdaInfo
=
struct
...
...
@@ -419,7 +420,7 @@ struct
|
M2
->
MPropUn
(
Neg
,
MAtom
(
Cro
,
1
))
|
M3
->
MPropUn
(
Neg
,
MAtom
(
CI
,
2
))
|
M4
->
MPropUn
(
Neg
,
MAtom
(
Cro
,
3
))
| M5 -> MAtom(CI, 1)
|
M5
->
MAtom
(
CI
I
,
1
)
|
M6
->
MPropUn
(
Neg
,
MAtom
(
CI
,
1
))
|
M7
->
MPropUn
(
Neg
,
MAtom
(
Cro
,
2
))
|
M8
->
MAtom
(
N
,
1
)
;;
...
...
@@ -429,7 +430,6 @@ 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,7 +984,7 @@ 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 *) *)
...
...
@@ -1076,30 +1076,40 @@ 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) *)
(*
(*Qa = N+; CII+; CI+; CI+; N−; CII−
Ra ≡ (CI = 2 ∧ Cro = 0 ∧ CII = 0 ∧ N = 0)*)
let
progpl1
=
Seq
(
Seq
(
Seq
(
Seq
(
Seq
(
Incr
N
,
Incr
CII
)
,
Incr
CI
)
,
Incr
CI
)
,
Decr
N
)
,
Decr
CII
)
;;
(* (* Avant possibilité de simplification *)
let postpl1 = PropBin(And, PropBin(And, PropBin(And, Rel(Eq, ExprVar CI, ExprConst 2), Rel(Eq, ExprVar Cro, ExprConst 0)),
Rel(Eq, ExprVar CII, ExprConst 0)), Rel(Eq, ExprVar N, ExprConst 0)) ;;
let prepl1 = wp progpl1 postpl1 ;;
*)
let
postpl1
=
PropConst
True
;;
let
prepl1_nr
=
wp
progpl1
postpl1
;;
(* Sans raffinage *)
let
prepl1
=
and_simplify
(
wp
progpl1
postpl1
)
[(
CI
,
0
)
;
(
Cro
,
0
)
;
(
CII
,
0
)
;
(
N
,
0
)]
[]
;;
(* Avec raffinage et simplification *)
print_endline
"*** Exemple 1 du phage lambda ***"
;;
print_endline
"* Programme *"
;;
print_endline
(
string_of_prog_indent
progpl1
)
;;
print_endline
"* Post-condition *"
;;
print_endline
(
string_of_formula
postpl1
)
;;
print_endline
"* Plus faible pré-condition calculée non raffinée *"
;;
print_endline
(
string_of_formula
prepl1_nr
)
;;
print_endline
"* Plus faible pré-condition calculée *"
;;
print_endline
(
string_of_formula
prepl1
)
;;
print_endline
"***************************"
;;
write_example
prepl1_nr
"phagelex1_nr.lp"
;;
write_example
prepl1
"phagelex1.lp"
;;
(* Mauvais : explosion combinatoire => trop de résultats *)
*)
(** Cycle circadien (d'après projet Circlock) *)
...
...
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