Commit 529730ec authored by Maxime Folschette's avatar Maxime Folschette
Browse files

translate old examples to the new representation

parent 4d931cf4
......@@ -180,257 +180,74 @@ type multformula =
(*** BRN description ***)
(***********************)
(** Types: info on variables and multiplexes *)
(* vars must be a list of ( var * (varmax * varpredec )) *)
(* that is: (string * ( int * string list)) *)
type varinfo = (var * (varmax * varpredec)) list ;;
(* mults must be a list of ( mult * multformula) *)
(* that is: (string * multformula) *)
type multinfo = (mult * multformula) list ;;
(** Main article's toy example *)
(* vars = var * (varmax * varpredec) *)
let vars =
[("a", (1, [])) ;
("b", (1, ["lambda" ; "sigma"])) ;
("c", (1, ["l"]))] ;;
(* mults = mult * multformula *)
let mults =
[("l", MAtom("a", 1)) ;
("lambda", MPropUn(Neg, MAtom("c", 1))) ;
("sigma", MAtom("a", 1))] ;;
(** Old exemples *)
(** Other examples *)
(*
(** Toy example *)
(*
module ToyExample =
struct
type var = A ;;
type mult = M ;;
let varlist = [A] ;;
let varequals v1 v2 =
match v1, v2 with
| A, A -> true ;;
let asp_of_var = function
| A -> "A" ;;
let asp_of_mult = function
| M -> "M" ;;
let string_of_var = function
| A -> "a" ;;
let string_of_mult = function
| M -> "m" ;;
let multcompare m1 m2 =
compare (asp_of_mult m1) (asp_of_mult m2) ;;
end ;;
*)
(*
module ToyExampleInfo =
struct
open Operators ;;
open ToyExample ;;
open FOLmult ;;
let getbound = function
| A -> 1 ;;
let getformula = function
| M -> MPropUn(Neg, MAtom(A, 1)) ;;
let getpredec = function
| A -> [M] ;;
end ;;
*)
let vars : varinfo = [("A", (1, ["M"]))] ;;
let mults : multinfo = [("M", MPropUn(Neg, MAtom("A", 1)))] ;;
(** Lambda phage (from Adrien Richard's PhD thesis) *)
(*
module PhageLambda =
struct
type var = CI | Cro | CII | N ;;
type mult = M1 | M2 | M3 | M4 | M5 | M6 | M7 | M8 ;;
let varlist = [CI ; Cro ; CII ; N] ;;
let varequals v1 v2 =
match v1, v2 with
| CI, CI -> true
| Cro, Cro -> true
| CII, CII -> true
| N, N -> true
| _, _ -> false ;;
let asp_of_var = function
| CI -> "CI"
| Cro -> "Cro"
| CII -> "CII"
| N -> "N" ;;
let asp_of_mult = function
| M1 -> "M1"
| M2 -> "M2"
| M3 -> "M3"
| M4 -> "M4"
| M5 -> "M5"
| M6 -> "M6"
| M7 -> "M7"
| M8 -> "M8" ;;
let string_of_var = function
| CI -> "CI"
| Cro -> "Cro"
| CII -> "CII"
| N -> "N" ;;
let string_of_mult = function
| M1 -> "m1"
| M2 -> "m2"
| M3 -> "m3"
| M4 -> "m4"
| M5 -> "m5"
| M6 -> "m6"
| M7 -> "m7"
| M8 -> "m8" ;;
let multcompare m1 m2 =
compare (asp_of_mult m1) (asp_of_mult m2) ;;
end ;;
*)
(*
module PhageLambdaInfo =
struct
open Operators ;;
open PhageLambda ;;
open FOLmult ;;
let getbound = function
| CI -> 2
| Cro -> 3
| CII -> 1
| N -> 1 ;;
let getformula = function
| M1 -> MAtom(CI, 2)
| M2 -> MPropUn(Neg, MAtom(Cro, 1))
| M3 -> MPropUn(Neg, MAtom(CI, 2))
| M4 -> MPropUn(Neg, MAtom(Cro, 3))
| M5 -> MAtom(CII, 1)
| M6 -> MPropUn(Neg, MAtom(CI, 1))
| M7 -> MPropUn(Neg, MAtom(Cro, 2))
| M8 -> MAtom(N, 1) ;;
let getpredec = function
| CI -> [M1 ; M2 ; M5]
| Cro -> [M3 ; M4]
| CII -> [M3 ; M4 ; M8]
| N -> [M6 ; M7] ;;
end ;;
*)
let vars : varinfo =
[("CI", (2, ["M1" ; "M2" ; "M5"])) ;
("Cro", (3, ["M3" ; "M4"])) ;
("CII", (1, ["M3" ; "M4" ; "M8"])) ;
("N", (1, ["M6" ; "M7"]))] ;;
let mults : multinfo =
[("M1", MAtom("CI", 2)) ;
("M2", MPropUn(Neg, MAtom("Cro", 1))) ;
("M3", MPropUn(Neg, MAtom("CI", 2))) ;
("M4", MPropUn(Neg, MAtom("Cro", 3))) ;
("M5", MAtom("CII", 1)) ;
("M6", MPropUn(Neg, MAtom("CI", 1))) ;
("M7", MPropUn(Neg, MAtom("Cro", 2))) ;
("M8", MAtom("N", 1))] ;;
(** Circadian cycle (from the Circlock project) *)
(*
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 ;;
*)
(*
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 ;;
*)
let vars : varinfo =
[("PERCRY", (1, ["PC"])) ;
("PER1", (1, ["ClockBMAL"])) ;
("PER2", (1, ["ClockBMAL" ; "Context"])) ;
("CRY1", (1, ["CBR"])) ;
("CRY2", (1, ["ClockBMAL"])) ;
("Clock", (1, [])) ;
("RevErbAlpha", (1, ["ClockBMAL"])) ;
("BMAL1N", (1, ["Inhib"])) ;
("BMAL1C", (1, ["Acetylation"]))] ;;
let mults : multinfo =
[("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))] ;;
*)
......@@ -444,13 +261,6 @@ let asp_of_var = String.capitalize_ascii ;;
let asp_of_mult = String.capitalize_ascii ;;
let string_of_var = id ;;
let string_of_mult = id ;;
(*
(* Fonction de conversion personnalisée *)
let string_of_mult = function
| "l" -> "l"
| "lambda" -> "λ"
| "sigma" -> "σ" ;;
*)
(** Extract variables, multiplexes, etc. from the model **)
let varlist = fst (split vars) ;;
......@@ -905,8 +715,8 @@ in
(** Toy example *)
(*
let prog1 = Seq(Incr A, Decr A) ;;
let post1 = Rel(Eq, ExprVar A, ExprConst 0) ;;
let prog1 = Seq(Incr "A", Decr "A") ;;
let post1 = Rel(Eq, ExprVar "A", ExprConst 0) ;;
let pre1 = wp prog1 post1 ;;
print_endline "*****************************************************" ;;
print_endline "*** Toy example: negative feedback with Incr/Decr ***" ;;
......@@ -920,7 +730,7 @@ print_endline (string_of_formula pre1) ;;
write_example pre1 "toyex-incrdecr.lp" ;;
(* OK: One 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)) ;;
let prog2 = While(PropConst True, Rel(Eq, ExprVar "A", ExprConst 0), Seq(Incr "A", Decr "A")) ;;
let post2 = PropConst True (* Rel(Eq, ExprVar A, ExprConst 0) *) ;;
let pre2 = wp prog2 post2 ;;
print_endline "******************************************************" ;;
......@@ -935,9 +745,9 @@ print_endline (string_of_formula pre2) ;;
write_example pre2 "toyex-while.lp" ;;
(* OK: One solution: A = 0, k_a,{} = 0, k_a,{m} = 1 *)
let prog3 = If(Rel(Eq, ExprVar A, ExprConst 1),
While(PropConst True, Rel(Eq, ExprVar A, ExprConst 1), Seq(Decr A, Incr A)),
While(PropConst True, Rel(Eq, ExprVar A, ExprConst 0), Seq(Incr A, Decr A))) ;;
let prog3 = If(Rel(Eq, ExprVar "A", ExprConst 1),
While(PropConst True, Rel(Eq, ExprVar "A", ExprConst 1), Seq(Decr "A", Incr "A")),
While(PropConst True, Rel(Eq, ExprVar "A", ExprConst 0), Seq(Incr "A", Decr "A"))) ;;
let post3 = PropConst True (* Rel(Eq, ExprVar A, ExprConst 0) *) ;;
let pre3 = wp prog3 post3 ;;
print_endline "*************************************" ;;
......@@ -959,7 +769,7 @@ write_example pre3 "toyex-complex.lp" ;;
let prog1 = Seq(Seq(Incr "b", Incr "c"), Decr "b") ;;
let post1 = Rel(Eq, ExprVar "b", ExprConst 0) ;;
let pre1_ns = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar "a", ExprConst 1)) ;; (* Old-fashion refining without simplification *)
let pre1_ns = PropBin(And, wp prog1 post1, Rel(Eq, ExprVar "a", ExprConst 1)) ;; (* Old-fashioned refining without simplification *)
let pre1 = simplify (wp prog1 post1) [("a", 1) ; ("b", 0) ; ("c", 0)] [] ;; (* With refining and simplification *)
print_endline "******************************" ;;
print_endline "*** Example 1 from article ***" ;;
......@@ -1009,10 +819,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 "b"), Decr "c")) ;;
let post4 = Rel(Eq, ExprVar "b", ExprConst 1) ;;
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 *)
let pre4_oldr = PropBin(And, wp prog4 post4, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Old-fashioned refining without 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 = simplify (wp prog4 post4) [("a", 1) ; ("b", 0) ; ("c", 0)] [(("b", ["sigma"]), 0) ; (("b", ["lambda" ; "sigma"]), 0) ; (("c", ["l"]), 0)] ;; (* Avec raffinage et simplification *)
let pre4 = simplify (wp prog4 post4) [("a", 1) ; ("b", 0) ; ("c", 0)] [(("b", ["sigma"]), 0) ; (("b", ["lambda" ; "sigma"]), 0) ; (("c", ["l"]), 0)] ;; (* With refining and simplification *)
print_endline "**********************************************************" ;;
print_endline "*** Example 4 from article: While loop with I ≡ (True) ***" ;;
print_endline "**********************************************************" ;;
......@@ -1029,10 +839,10 @@ write_example pre4 "simpleex4.lp" ;;
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_oldr = PropBin(And, wp prog4b post4b, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Avec raffinage, ancienne implémentation sans simplification *)
let pre4b_oldr = PropBin(And, wp prog4b post4b, PropBin(And, PropBin(And, PropBin(And, PropBin(And, PropBin(And, (* Old-fashioned refining without 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 = simplify (wp prog4b post4b) [("a", 1) ; ("b", 0) ; ("c", 0)] [(("b", ["sigma"]), 0) ; (("b", ["lambda" ; "sigma"]), 0) ; (("c", ["l"]), 0)] ;; (* Avec raffinage et simplification *)
let pre4b = simplify (wp prog4b post4b) [("a", 1) ; ("b", 0) ; ("c", 0)] [(("b", ["sigma"]), 0) ; (("b", ["lambda" ; "sigma"]), 0) ; (("c", ["l"]), 0)] ;; (* With refining and simplification *)
print_endline "***********************************************************" ;;
print_endline "*** Example 4 from article: While loop with I ≡ (a = 1) ***" ;;
print_endline "***********************************************************" ;;
......@@ -1050,7 +860,7 @@ write_example pre4b "simpleex4b.lp" ;;
let prog5 = Seq(Seq(Seq(Incr "b", Set("c", 1)), Assert(PropBin(And, Rel(Eq, ExprVar "b", ExprConst 1), Rel(Eq, ExprVar "a", ExprConst 1)))), Decr "b") ;;
let post5 = PropConst True ;;
(* let pre4b = wp prog4b post4b ;; (* Sans raffinage *) *)
let pre5 = simplify (wp prog5 post5) [(* (A, 1) ; *) ("b", 0) ; ("c", 0)] [] ;; (* Avec raffinage et simplification *)
let pre5 = simplify (wp prog5 post5) [(* (A, 1) ; *) ("b", 0) ; ("c", 0)] [] ;; (* With refining and simplification *)
print_endline "*************************************************" ;;
print_endline "*** Example 5: Simple tests on Set and Assert ***" ;;
print_endline "*************************************************" ;;
......@@ -1069,18 +879,20 @@ write_example pre5 "simpleex5.lp" ;;
(*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 progpl1 = Seq(Seq(Seq(Seq(Seq(Incr "N", Incr "CII"), Incr "CI"), Incr "CI"), Decr "N"), Decr "CII") ;;
(* (* Made before any simplification was possible *)
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 = simplify (wp progpl1 postpl1) [(CI, 0) ; (Cro, 0) ; (CII, 0) ; (N, 0)] [] ;; (* Avec raffinage et simplification *)
let prepl1_nr = wp progpl1 postpl1 ;; (* Without refining *)
let prepl1 = simplify (wp progpl1 postpl1) [("CI", 0) ; ("Cro", 0) ; ("CII", 0) ; ("N", 0)] [] ;; (* With refining and simplification *)
print_endline "*********************************" ;;
print_endline "*** Example 1 on lambda phage ***" ;;
print_endline "*********************************" ;;
print_endline "* Program *" ;;
print_endline (string_of_prog_indent progpl1) ;;
print_endline "* Postcondition *" ;;
......@@ -1104,7 +916,9 @@ let prog1 = Skip ;;
let post1 = PropConst(True) ;;
let pre1 = wp prog1 post1 ;;
print_endline "***********************" ;;
print_endline "*** Circadian cycle ***" ;;
print_endline "***********************" ;;
print_endline "* Program *" ;;
print_endline (string_of_prog_indent prog1) ;;
print_endline "* Postcondition *" ;;
......
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