diff --git a/Models/CAV14/Cycle/svn-commit.tmp~ b/Models/CAV14/Cycle/svn-commit.tmp~ deleted file mode 100644 index 3573c6046..000000000 --- a/Models/CAV14/Cycle/svn-commit.tmp~ +++ /dev/null @@ -1,5 +0,0 @@ - ---This line, and those below, will be ignored-- - -AM SSkin1DAnalysisInput.xml -AM SSkin2D_3cells_2layersAnalysisInput.xml diff --git a/Models/Demo/BMA-demo-script.txt~ b/Models/Demo/BMA-demo-script.txt~ deleted file mode 100644 index 10f5143bb..000000000 --- a/Models/Demo/BMA-demo-script.txt~ +++ /dev/null @@ -1,91 +0,0 @@ - -BMA Demo Script - - -Intro -===== - -Bring together formal_modelling/verification, biology and UI to understand cancer -development. - -Applying these ideas in the domain of biology. -Diagrams as standard language in biology to communicate models; - -An important property to prove of a biological artifact like Skin or -Leukemia is homeostasis, that the organism reaches stability with some -certain values. - -If these verification techniques are to be used, they need to be in a -tool that's usable by a biologist. MSRC expertise in system -verification and UX/design brought together to solve problem. - -Complexity on three fronts; bio model, formal methods and UI; unique -collaboration playing to expertise in all three areas allows us to -develop unique tool built on Azure - -Interest from pharma and academia, opening new avenues for analysing -and sharing models - - -BcrAblNoFeedback -================ - -Here we have a model showing how the events leading to leukaemia -developing in white blood cells. -BcrAbl (caused by gene fusion/mutation) causes uncontrolled proliferation. -The cells on the right are behavioural markers, telling us the cell fate. - -1st run: model stabilizes implies that model is sound. Markers -(Proliferation=2, Self Renewal Capacity=2) show that it's growing -uncontrollably, and control-type behaviours (Growth Arrest=0, Correct -Differentiation=0, Apoptosis=0) are shut down. - -We then change the BcrAbl protein (make range [0,0]) to mimic the effect of the "Gleevec" drug. - -2nd run: model stabilizes with -(Proliferation=1, Self Renewal Capacity=1, Growth Arrest=0, Correct Differentiation=1, Apoptosis=1) - - -If we have time ... - - -Skin1D_unstable -=============== - -Skin. Made up of 5 layers of cells. -Lowest one on left, topmost is on right. -Develops so that lowest becomes epidermis: divides and pushes one up. - topmost eventually sheds. -Each cell is mirrored. -The Wnt and Ligand-in model the environment. In this case, they code up the gradient. - - -On the formal side, this is a QN. -Each variable ranges over an interval, and has a target function that the variable "wants to become". - -This was the initial model, hypothesizing the relationship between the proteins of cell. -But analysis showed that this model didn't reach homeostasis. -Cause: missing relationship b/t GT1-->Jagged. - - -Skin1D -====== - -Stability is not just about reaching a fixed point. -The values at the fixed point can be read as a phenotype. This determines fate. - - -Verification -============ - -Search for ever increasing regions of stability. -General approach, proving FG(x tighter), until x's interval single point works but doesn't scale. -Faster procedure, based on abstract interpretation over interval domain, scales to very large models. -If stability can't be proven, then fall back to Z3 for completeness. - - -Result -====== - -A lot of design iteration on how to show proof and counter-example to biologist. -Currently coloring variables green (stable), pink (cex to stability: bifurcates or cycles). diff --git a/Models/OriginalModels/IntermediatesModelRebuiltAnalysisInput.xml~ b/Models/OriginalModels/IntermediatesModelRebuiltAnalysisInput.xml~ deleted file mode 100644 index 0867cca74..000000000 --- a/Models/OriginalModels/IntermediatesModelRebuiltAnalysisInput.xml~ +++ /dev/null @@ -1,1079 +0,0 @@ - - - - - Scl - 0 - 3 - ceil((var(15)* 3 + var(10)*2 + var(3)*2 + var(16)*2 + var(18)*2 + var(36)*2 + var(25)*2 + var(28) + var(7) - var(30) + var(39) + var(38))/ (63)) - - - Lyl1 - 0 - 3 - ceil((var(15)*2 + var(18)*2 + var(23)*4 + var(37)*4 + var(25)*2 + var(10) * 4 - var(34) * 4 - var(38)) / (54)) - - - - - - - Ebox - 0 - 3 - Min(3, var(1) + var(2)) - - - Erg - 0 - 3 - ceil((var(3)*2 + var(16)*2 + var(15)*2 + var(18)*2 + var(23)*2 + var(36)*2 + var(Runx1Gata2)*2 + var(28)*3 + var(7)* 3 + var(35) – var(30)*3)/60) - - - Fli1 - 0 - 3 - ceil((var(15)*3 + var(18)*3 + var(23)*3 + var(24) + var(7)* 11 – var(30)*2 + var(39) + var(38))/69) - - - Pu.1 - 0 - 3 - ceil((var(1)*2 + var(15)*2 + var(4)*3 + var(19) + var(21) + var(24)*3 + var(10)*3 – var(30)*2 – var(34)*3 – var(38))/45) - - - EtsA - 0 - 3 - min(3, var(4) + Fli1) - - - EtsB - 0 - 3 - min(3, var(4) + var(6)) - - - EtsC - 0 - 3 - min(3, var(5) + var(6)) - - - Ets - 0 - 3 - Min(3, var(4)+var(5)+var(6)) - - - valEtsA - 0 - 3 - var(4)+var(5) - - - valEts - 0 - 3 - var(4)+var(5)+var(6) - - - Runx1 - 0 - 3 - ceil((var(3) + var(16) + var(15) + var(18) + var(23) + var(24) + var(10)*5 – var(34)*5 + var(35) – var(40) + var(38))/ 54) - - - Runx1Gata2 - 0 - 3 - var(24)*var(15)*(1/3) - - - Runx1Scl - 0 - 3 - var(24)*var(1)*(1/3) - - - Runx1Erg - 0 - 3 - var(24)*var(4)*(1/3) - - - Runx1EtsA - 0 - 3 - var(24)*var(7)*(1/3) - - - Runx1Fli1 - 0 - 3 - var(24)*var(5)*(1/3) - - - Runx1Ebox - 0 - 3 - var(24)*var(3)*(1/3) - - - Runx1Ets/A - 0 - 3 - var(24)*min((var(12)/var(13)*3), var(7))*(1/3) - - - Meis1 - 0 - 3 - ceil((var(15)*3 + var(18)*3 + var(23)*3 + var(25)*3 + var(37)*6 + var(10)*6 + var(35) – var(30))/75) - - - Gata2 - 0 - 3 - ceil((var(3)*2 + var(16)*2 + var(15)*4 + var(18)*4 + var(24)*3 + var(10)*7 + var(35)*2 – var(30) + var(39) – var(38))/75) - - - Gata2Lmo2Scl - 0 - 3 - var(15)*var(17)*var(1)*(1/9) - - - Gata2Lmo2Lyl1 - 0 - 3 - var(15)*var(17)*var(2)*(1/9) - - - Gata2Lmo2Ebox - 0 - 3 - var(15)*var(17)*var(3)*(1/9) - - - EboxLmo2 - 0 - 3 - var(3)*var(17)*(1/3) - - - Lmo2 - 0 - 3 - ceil((var(15)*4 + var(18)*4 + var(23)*2 + var(36) + var(25)*2 + var(28)*4 + var(4)* 7 + var(7)*6 + var(35)*4 + var(24)*2 + var(10)*4 + var(8) – var(32)*7 + var(38))/126) - - - Gata2Lmo2 - 0 - 3 - var(15)*var(17)*(1/3) - - - SclLmo2 - 0 - 3 - var(1)*var(17)*(1/3) - - - Lyl1Lmo2 - 0 - 3 - var(2)*var(17)*(1/3) - - - Gfi1b - 0 - 3 - ceil((var(3)*3 + var(16)*3 + var(15)*2 + var(18)*2 + var(23)*2 + var(36)*3 + var(25)*2 + var(28)*7 + var(7)*7 – var(30)*2 + var(38))/96) - - - Gfi1bFli1 - 0 - 3 - var(30)*var(5)*(1/3) - - - Gfi1bErg - 0 - 3 - var(30)*var(4)*(1/3) - - - Gfi1bPu.1 - 0 - 3 - var(30)*var(6)*(1/3) - - - Gfi1bEts - 0 - 3 - var(30)*var(10)*(1/3) - - - Gata1 - 0 - 3 - ceil((var(1) + var(17) + var(24) + var(5) + var(38) – var(15) – var(6) – var(30))/ 15) - - - Etv2 - 0 - 3 - 1 - - - Hoxa3 - 0 - 3 - 1 - - - - - 1 - 3 - Activator - - - 2 - 3 - Activator - - - 3 - 1 - Activator - - - 4 - 7 - Activator - - - 5 - 7 - Activator - - - 4 - 8 - Activator - - - 6 - 8 - Activator - - - 5 - 9 - Activator - - - 6 - 9 - Activator - - - 4 - 10 - Activator - - - 5 - 10 - Activator - - - 6 - 10 - Activator - - - 4 - 12 - Activator - - - 5 - 12 - Activator - - - 4 - 13 - Activator - - - 5 - 13 - Activator - - - 6 - 13 - Activator - - - 7 - 5 - Activator - - - 7 - 4 - Activator - - - 4 - 6 - Activator - - - 10 - 6 - Activator - - - 24 - 25 - Activator - - - 24 - 26 - Activator - - - 24 - 28 - Activator - - - 24 - 29 - Activator - - - 24 - 27 - Activator - - - 24 - 36 - Activator - - - 24 - 37 - Activator - - - 24 - 24 - Activator - - - 35 - 35 - Activator - - - 15 - 23 - Activator - - - 15 - 21 - Activator - - - 15 - 22 - Activator - - - 15 - 15 - Activator - - - 17 - 19 - Activator - - - 17 - 16 - Activator - - - 17 - 20 - Activator - - - 17 - 18 - Activator - - - 18 - 17 - Activator - - - 30 - 31 - Activator - - - 30 - 32 - Activator - - - 30 - 33 - Activator - - - 30 - 34 - Activator - - - 30 - 30 - Inhibitor - - - 38 - 38 - Activator - - - 15 - 18 - Activator - - - 2 - 20 - Activator - - - 3 - 16 - Activator - - - 1 - 19 - Activator - - - 17 - 23 - Activator - - - 17 - 21 - Activator - - - 17 - 22 - Activator - - - 2 - 22 - Activator - - - 3 - 23 - Activator - - - 1 - 21 - Activator - - - 15 - 25 - Activator - - - 1 - 26 - Activator - - - 7 - 28 - Activator - - - 4 - 27 - Activator - - - 5 - 29 - Activator - - - 5 - 31 - Activator - - - 6 - 33 - Activator - - - 4 - 32 - Activator - - - 10 - 34 - Activator - - - 3 - 36 - Activator - - - 10 - 37 - Activator - - - 13 - 37 - Activator - - - 12 - 37 - Activator - - - 7 - 37 - Activator - - - 15 - 1 - Activator - - - 10 - 1 - Activator - - - 16 - 1 - Activator - - - 18 - 1 - Activator - - - 36 - 1 - Activator - - - 25 - 1 - Activator - - - 28 - 1 - Activator - - - 7 - 1 - Activator - - - 30 - 1 - Inhibitor - - - 15 - 5 - Activator - - - 18 - 5 - Activator - - - 23 - 5 - Activator - - - 24 - 5 - Activator - - - 3 - 15 - Activator - - - 16 - 15 - Activator - - - 18 - 15 - Activator - - - 24 - 15 - Activator - - - 10 - 15 - Activator - - - 35 - 15 - Activator - - - 30 - 15 - Inhibitor - - - 3 - 4 - Activator - - - 16 - 4 - Activator - - - 15 - 4 - Activator - - - 18 - 4 - Activator - - - 23 - 4 - Activator - - - 36 - 4 - Activator - - - 28 - 4 - Activator - - - 35 - 4 - Activator - - - 30 - 4 - Inhibitor - - - 30 - 5 - Inhibitor - - - 3 - 24 - Activator - - - 16 - 24 - Activator - - - 15 - 24 - Activator - - - 18 - 24 - Activator - - - 23 - 24 - Activator - - - 10 - 24 - Activator - - - 35 - 24 - Activator - - - 34 - 24 - Inhibitor - - - 1 - 6 - Activator - - - 15 - 6 - Activator - - - 19 - 6 - Activator - - - 21 - 6 - Activator - - - 24 - 6 - Activator - - - 30 - 6 - Inhibitor - - - 34 - 6 - Inhibitor - - - 34 - 2 - Inhibitor - - - 15 - 2 - Activator - - - 18 - 2 - Activator - - - 23 - 2 - Activator - - - 37 - 2 - Activator - - - 25 - 2 - Activator - - - 10 - 2 - Activator - - - 3 - 30 - Activator - - - 16 - 30 - Activator - - - 15 - 30 - Activator - - - 18 - 30 - Activator - - - 23 - 30 - Activator - - - 36 - 30 - Activator - - - 25 - 30 - Activator - - - 28 - 30 - Activator - - - 7 - 30 - Activator - - - 15 - 35 - Activator - - - 18 - 35 - Activator - - - 23 - 35 - Activator - - - 25 - 35 - Activator - - - 37 - 35 - Activator - - - 10 - 35 - Activator - - - 30 - 35 - Inhibitor - - - 15 - 17 - Activator - - - 23 - 17 - Activator - - - 36 - 17 - Activator - - - 25 - 17 - Activator - - - 28 - 17 - Activator - - - 4 - 17 - Activator - - - 7 - 17 - Activator - - - 35 - 17 - Activator - - - 24 - 17 - Activator - - - 10 - 17 - Activator - - - 8 - 17 - Activator - - - 32 - 17 - Inhibitor - - - 1 - 38 - Activator - - - 17 - 38 - Activator - - - 24 - 38 - Activator - - - 5 - 38 - Activator - - - 6 - 38 - Inhibitor - - - 30 - 38 - Inhibitor - - - 38 - 1 - Activator - - - 38 - 2 - Inhibitor - - - 38 - 17 - Activator - - - 15 - 38 - Inhibitor - - - 38 - 15 - Inhibitor - - - 38 - 24 - Activator - - - 38 - 5 - Activator - - - 38 - 6 - Inhibitor - - - 38 - 30 - Activator - - - 40 - 24 - Inhibitor - - - 39 - 5 - Activator - - - 39 - 15 - Activator - - - 39 - 1 - Activator - - - \ No newline at end of file diff --git a/Models/OriginalModels/fs_NirShouldCycle.xml~ b/Models/OriginalModels/fs_NirShouldCycle.xml~ deleted file mode 100644 index 36e6c365d..000000000 --- a/Models/OriginalModels/fs_NirShouldCycle.xml~ +++ /dev/null @@ -1,57 +0,0 @@ - - - - - - 0 - 0 - - - - in - 0 - 4 - 4 - - - a - 0 - 4 - var(7) - - - b - 0 - 4 - var(8)-var(12) - - - c - 0 - 4 - var(9) - - - - - 7 - 8 - Activator - - - 8 - 9 - Activator - - - 9 - 12 - Activator - - - 12 - 9 - Inhibitor - - - \ No newline at end of file