Commit 32cafd41 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

add Circlock example

parent 68491791
......@@ -139,6 +139,7 @@ struct
end ;;
*)
(*
(** Exemple du papier *)
module SimpleExample =
struct
......@@ -174,6 +175,7 @@ struct
let multcompare m1 m2 =
compare (asp_of_mult m1) (asp_of_mult m2) ;;
end ;;
*)
(*
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
......@@ -226,12 +228,85 @@ struct
end ;;
*)
(** Cycle circadien (depuis projet Circlock) *)
module Circlock =
struct
type var = PERCRY | PER1 | PER2 | CRY1 | CRY2 | Clock | RevErbAlpha | BMAL1N | BMAL1C ;;
type mult = PC | PER1PER1 | PER1PER2 | PER2PER2 | CRY1CRY1 | CRY1CRY2 | CRY2CRY2 | ClockBMAL | CBR | Inhib | Acetylation | Context ;;
let varlist = [PERCRY ; PER1 ; PER2 ; CRY1 ; CRY2 ; Clock ; RevErbAlpha ; BMAL1N ; BMAL1C] ;;
let varequals v1 v2 =
match v1, v2 with
| PERCRY, PERCRY -> true
| PER1, PER1 -> true
| PER2, PER2 -> true
| CRY1, CRY1 -> true
| CRY2, CRY2 -> true
| Clock, Clock -> true
| RevErbAlpha, RevErbAlpha -> true
| BMAL1N, BMAL1N -> true
| BMAL1C, BMAL1C -> true
| _, _ -> false ;;
let asp_of_var = function
| PERCRY -> "PERCRY"
| PER1 -> "PER1"
| PER2 -> "PER2"
| CRY1 -> "CRY1"
| CRY2 -> "CRY2"
| Clock -> "Clock"
| RevErbAlpha -> "RevErbAlpha"
| BMAL1N -> "BMAL1N"
| BMAL1C -> "BMAL1C" ;;
let asp_of_mult = function
| PC -> "PC"
| PER1PER1 -> "PER1PER1"
| PER1PER2 -> "PER1PER2"
| PER2PER2 -> "PER2PER2"
| CRY1CRY1 -> "CRY1CRY1"
| CRY1CRY2 -> "CRY1CRY2"
| CRY2CRY2 -> "CRY2CRY2"
| ClockBMAL -> "ClockBMAL"
| CBR -> "CBR"
| Inhib -> "Inhib"
| Acetylation -> "Acetylation"
| Context -> "Context" ;;
let string_of_var = function
| PERCRY -> "PER-CRY (N)"
| PER1 -> "PER1 (C)"
| PER2 -> "PER2 (C)"
| CRY1 -> "CRY1 (C)"
| CRY2 -> "CRY2 (C)"
| Clock -> "Clock (N)"
| RevErbAlpha -> "RevErbα (N)"
| BMAL1N -> "BMAL1 (N)"
| BMAL1C -> "BMAL1 (C)" ;;
let string_of_mult = function
| PC -> "PC"
| PER1PER1 -> "PER1-PER1"
| PER1PER2 -> "PER1-PER2"
| PER2PER2 -> "PER2-PER2"
| CRY1CRY1 -> "CRY1-CRY1"
| CRY1CRY2 -> "CRY1-CRY2"
| CRY2CRY2 -> "CRY2-CRY2"
| ClockBMAL -> "Clock-BMAL (N actif)"
| CBR -> "CB-R"
| Inhib -> "inhib"
| Acetylation -> "Acetylation"
| Context -> "Context" ;;
let multcompare m1 m2 =
compare (asp_of_mult m1) (asp_of_mult m2) ;;
end ;;
(** Sélection du BRN à considérer *)
(* module BRN = ToyExample ;; *)
module BRN = SimpleExample ;;
(* module BRN = SimpleExample ;; *)
(* module BRN = PhageLambda ;; *)
module BRN = Circlock ;;
......@@ -305,6 +380,7 @@ struct
end ;;
*)
(*
(** Exemple du papier *)
module SimpleExampleInfo =
struct
......@@ -325,6 +401,7 @@ struct
| B -> [Lambda ; Sigma]
| C -> [L] ;;
end ;;
*)
(*
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
......@@ -356,12 +433,48 @@ struct
end ;;
*)
(** Cycle circadien (depuis projet Circlock) *)
module CirclockInfo =
struct
open Operators ;;
open Circlock ;;
open FOLmult ;;
let getbound : var -> int = fun _ -> 1 ;;
let getformula = function
| PC -> MPropBin(And,
MPropBin(Or, MPropBin(Or, MMult(PER1PER1), MMult(PER1PER2)), MMult(PER2PER2)),
MPropBin(Or, MPropBin(Or, MMult(CRY1CRY1), MMult(CRY1CRY2)), MMult(CRY2CRY2)))
| PER1PER1 -> MAtom(PER1, 1)
| PER1PER2 -> MPropBin(Or, MAtom(PER1, 1), MAtom(PER2, 1))
| PER2PER2 -> MAtom(PER2, 1)
| CRY1CRY1 -> MAtom(CRY1, 1)
| CRY1CRY2 -> MPropBin(Or, MAtom(CRY1, 1), MAtom(CRY2, 1))
| CRY2CRY2 -> MAtom(CRY2, 1)
| ClockBMAL -> MPropBin(And, MPropBin(And, MAtom(Clock, 1), MAtom(BMAL1N, 1)), MPropUn(Neg, MAtom(PERCRY, 1)))
| CBR -> MPropBin(And, MPropUn(Neg, MAtom(RevErbAlpha, 1)), MMult(ClockBMAL))
| Inhib -> MPropUn(Neg, MAtom(RevErbAlpha, 1))
| Acetylation -> MPropBin(And, MAtom(BMAL1C, 1), MAtom(Clock, 1))
| Context -> MPropConst(True) ;;
let getpredec = function
| PERCRY -> [PC]
| PER1 -> [ClockBMAL]
| PER2 -> [ClockBMAL ; Context]
| CRY1 -> [CBR]
| CRY2 -> [ClockBMAL]
| Clock -> []
| RevErbAlpha -> [ClockBMAL]
| BMAL1N -> [Inhib]
| BMAL1C -> [Acetylation] ;;
end ;;
(** Sélection des informations du BRN à considérer *)
(* module BRNinfo = ToyExampleInfo ;; *)
module BRNinfo = SimpleExampleInfo ;;
(* module BRNinfo = SimpleExampleInfo ;; *)
(* module BRNinfo = PhageLambdaInfo ;; *)
module BRNinfo = CirclockInfo ;;
......@@ -768,7 +881,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 = wp prog1 post1 ;; (* Sans raffinage *) *)
......@@ -851,7 +964,7 @@ print_endline "*** Plus faible pré-condition calculé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) *)
......@@ -876,6 +989,27 @@ write_example prepl1 "phagelex1.lp" ;;
(* Mauvais : explosion combinatoire => trop de résultats *)
*)
(** Cycle circadien (d'après projet Circlock) *)
let prog1 = Skip ;;
let post1 = PropConst(True) ;;
let pre1 = wp prog1 post1 ;;
print_endline "*** Cycle circadien ***" ;;
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 (string_of_formula pre1) ;;
print_endline "***************************" ;;
write_example pre1 "circlock1.lp" ;;
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