Merge pull request #54 from egLanghaus/master

adding PCR spec

specifications/README

@@ -26,6 +26,9 @@ ewd840
    and van Gasteren for detecting distributed termination on a
    unidirectional ring, together with a safety proof.
 
+glowingRaccoon
+   A specification of PCR using refinement mapping in TLA+.
+
 lamport_mutex
    A TLA+ specification of the distributed mutual-exclusion
    algorithm that appeared as an example in Lamport's classic

specifications/glowingRaccoon/clean.tla

@@ -0,0 +1,105 @@
+----------------------------- MODULE clean -----------------------------
+
+\* PCR amplifies a desired snippet of DNA.
+\* This is the basic picture of PCR:
+\* High heat denatures DNA, producing single-stranded templates. 
+\* Lower heat allows annealing of primers to sites on templates.
+\* (Primers are carefully chosen for this purpose.)
+\* Hybrids are produced by annealing at this lower temperature.
+\* Polymerase attaches to hybrids and extends them to new DNA.
+\* Extension occurs at medium heat, between annealing and denaturing. 
+\* The whole cyle repeats, yield S-curve growth of the product.
+\* The goal is to produce more DNA, but just any DNA? No!
+\* See refinements in "stages.tla" and "product.tla".
+
+\* Many factors contribute to successful PCR.
+\* Most of them are neglected here.
+\* In particular, nucleotides are just assumed to be there.
+\* Two different types of primer are required.
+\* (our spec allows for this; further refinement could distinguish)
+\* Extension is assumed to happen to available hybrids.
+\* Temporal Logic of Actions is not the perfect tool for this!
+\* Hopefully, the exercise is worthwhile.
+
+EXTENDS Naturals \* an import - copies module in there
+
+CONSTANTS DNA, PRIMER \* starting stock of key things
+
+VARIABLES tee, \* temperature, a string
+          primer, \* count of primers remaining
+          dna, \* count of double strands present
+          template, \* count of single strands present
+          hybrid \* count of template-primer hybrids
+
+(* list of state variables, for convenience *)
+vars == << tee, primer, dna, template, hybrid >>
+
+(* helper function *)
+natMin(i,j) == IF i < j THEN i ELSE j \* min of two nats
+
+(* actions *)
+heat == /\ tee = "Hot" \* current temperature is "Hot"
+        /\ tee' = "TooHot" \* heat up to "TooHot"
+        /\ primer' = primer + hybrid \* we'll take those back, thanks
+        /\ dna' = 0 \* the dna denatures
+        /\ template' = template + hybrid + 2 * dna \* has to go somewhere
+        /\ hybrid' = 0 \* these denature too
+
+cool == /\ tee = "TooHot" \* when you just denatured
+        /\ tee' = "Hot" \* cool off to "Hot"
+        /\ UNCHANGED << primer, dna, template, hybrid >>
+
+anneal == /\ tee = "Hot" \* too hot to anneal primers
+          /\ tee' = "Warm" \* "Warm" is just right
+          /\ UNCHANGED dna \* dna can reanneal; we neglect that
+          (* this is the neat part *)
+          /\ \E k \in 1..natMin(primer, template) : 
+             /\ primer' = primer - k \* k consumed
+             /\ template' = template - k \* k consumed
+             /\ hybrid' = hybrid + k \* k more hybrids
+
+extend == /\ tee = "Warm" \* too cool for extension
+            /\ tee' = "Hot" \* "Hot" is just right
+            /\ UNCHANGED <<primer, template>>
+            /\ dna' = dna + hybrid \* assuming it just happens
+            /\ hybrid' = 0 \* all turned to dna
+
+(* initial state *)
+Init == /\ tee = "Hot" \* not really all that hot
+        /\ primer = PRIMER \* we have consumed no primers
+        /\ dna = DNA \* we start with some nice 'frozen' dna
+        /\ template = 0 \* everything is bound up
+        /\ hybrid = 0 \* no annealing has happened yet
+
+(* state transition *)
+Next ==  \/ heat
+         \/ cool
+         \/ anneal
+         \/ extend
+
+(* specification of system *)
+Spec == /\ Init 
+        /\ [][Next]_vars 
+
+(* type invariant *)
+TypeOK == 
+    /\ tee \in {"Warm", "Hot", "TooHot"}
+    /\ primer \in Nat
+    /\ dna \in Nat
+    /\ template \in Nat
+    /\ hybrid \in Nat
+
+(* safety *)
+primerPositive == (primer >= 0) \* a redundant invariant
+
+(* preservation as an invariant *)
+preservationInvariant == template + primer + 2*(dna + hybrid) = PRIMER + 2 * DNA
+
+(* preservation as a property *)
+constantCount == UNCHANGED ( template + primer + 2*(dna + hybrid) )
+preservationProperty == [][constantCount]_vars \* as property
+
+(* liveness *)
+primerDepleted == <>(primer = 0) \* does not hold!
+
+=============================================================================

specifications/glowingRaccoon/product.tla

@@ -0,0 +1,208 @@
+---------------------------- MODULE product ----------------------------
+
+\* Now that we can cycle properly and also count...
+\* let's look at the actual "product" of the process.
+\* This requires more variables, for a hi-res view.
+
+
+EXTENDS Naturals, Sequences \* imports
+
+CONSTANTS DNA, PRIMER \* starting stock of key things
+
+VARIABLES tee, 
+          stage, 
+          cycle, 
+          primer, 
+          (* and single-stranded templates *)
+          longTemplate,
+          shortTemplate,
+          tinyTemplate,
+          (* and the hybrids *)
+          longHybrid,
+          shortHybrid,
+          tinyHybrid,
+          (* and double strands *)
+          longLongDouble,
+          shortLongDouble,
+          tinyShortDouble,          
+          (* and the product *)
+          product \* a tinyTiny double, if you prefer
+
+(* list of state variables *)
+vars == <<tee, \* temperature
+          stage, \* a history, if you think about it
+          cycle, \* we can count
+          primer,
+          (* and single-stranded templates *)
+          longTemplate,
+          shortTemplate,
+          tinyTemplate,
+          (* and the hybrids *)
+          longHybrid,
+          shortHybrid,
+          tinyHybrid,          
+          (* and doubles *)
+          longLongDouble,
+          shortLongDouble,
+          tinyShortDouble,                    
+          (* and the product *)
+          product
+        >>  
+
+(* more variable lists, for convenience *)
+templates == <<longTemplate,
+               shortTemplate,
+               tinyTemplate>>
+
+hybrids == <<longHybrid,
+             shortHybrid,
+             tinyHybrid>>
+
+doubles == <<longLongDouble,
+             shortLongDouble,
+             tinyShortDouble,
+             product>>
+
+(* helper functions *)
+natMin(i,j) == IF i < j THEN i ELSE j \* min of two nats
+RECURSIVE sumList(_) \* sum of a list
+sumList(s) == IF s = <<>> THEN 0 ELSE Head(s) + sumList(Tail(s))
+
+(* actions *)
+heat ==    /\ tee = "Hot" \* current temperature is "Hot"
+           /\ tee' = "TooHot" \* heat up to "TooHot"
+           /\ primer' = primer + sumList(hybrids) \* recover primers from hybrids
+           (* double strands denature *)
+           /\ longLongDouble' = 0
+           /\ shortLongDouble' = 0
+           /\ tinyShortDouble' = 0
+           /\ product' = 0
+           (* hybrids denature *)
+           /\ longHybrid' = 0
+           /\ shortHybrid' = 0
+           /\ tinyHybrid' = 0
+           (* templates absorb all this*)
+           /\ longTemplate' = longTemplate + longHybrid + shortLongDouble + 2 * longLongDouble \* only place they come from
+           /\ shortTemplate' = shortTemplate + shortHybrid + shortLongDouble + tinyShortDouble
+           /\ tinyTemplate' = tinyTemplate + tinyHybrid + tinyShortDouble + 2 * product
+           (* stage and cycle*)
+           /\ (stage = "init" \/ stage = "extended")
+           /\ stage' = "denatured"
+           /\ UNCHANGED cycle
+
+cool ==   /\ tee = "TooHot" \* when you just denatured
+          /\ tee' = "Hot" \* cool off to "Hot"
+          /\ stage = "denatured"
+          /\ stage' = "ready"
+          /\ UNCHANGED <<cycle, primer>>
+          /\ UNCHANGED doubles
+          /\ UNCHANGED templates
+          /\ UNCHANGED hybrids
+
+anneal ==   /\ tee = "Hot" \* too hot to anneal primers
+            /\ tee' = "Warm" \* "Warm" is just right
+            (* template/primer annealing *)
+            /\ \E k \in 1..natMin(primer, sumList(templates)) : 
+                /\ primer' = primer - k \* k consumed
+                (* choose templates to anneal with primer *)
+                /\ \E tup \in ((0..longTemplate) \X (0..shortTemplate) \X (0..tinyTemplate)):
+                   /\ sumList(tup) = k
+                   /\ longTemplate' = longTemplate - tup[1]
+                   /\ longHybrid' = longHybrid + tup[1]
+                   /\ shortTemplate' = shortTemplate - tup[2]
+                   /\ shortHybrid' = shortHybrid + tup[2]
+                   /\ tinyTemplate' = tinyTemplate - tup[3]
+                   /\ tinyHybrid' = tinyHybrid + tup[3] 
+            /\ stage = "ready"
+            /\ stage' = "annealed"
+            /\ UNCHANGED cycle \* dna can reanneal; we neglect that
+            /\ UNCHANGED doubles            
+
+extend ==   /\ tee = "Warm" \* too cool for extension
+            /\ tee' = "Hot" \* "Hot" is just right
+            (* any not annealed remained *)
+            /\ UNCHANGED primer
+            /\ UNCHANGED templates
+            (* update doubles *)
+            /\ UNCHANGED longLongDouble
+            /\ shortLongDouble' = shortLongDouble + longHybrid
+            /\ tinyShortDouble' = tinyShortDouble + shortHybrid
+            /\ product' = product + tinyHybrid \* the only place you get hybrid from
+            (* hybrids consumed *)
+            /\ longHybrid' = 0
+            /\ shortHybrid' = 0
+            /\ tinyHybrid' = 0
+            (* stage and cycle *)
+            /\ stage = "annealed"
+            /\ stage' = "extended"
+            /\ cycle' = cycle + 1 \* only place this changes
+
+(* initial state *)
+Init == /\ tee = "Hot" \* not really all that hot
+        /\ primer = PRIMER \* we have consumed no primers
+        /\ longLongDouble = DNA \* subtle but important change
+        (* and single-stranded templates *)
+        /\ longTemplate = 0
+        /\  shortTemplate = 0
+        /\  tinyTemplate = 0
+        (* and the hybrids *)
+        /\  longHybrid = 0
+        /\  shortHybrid = 0
+        /\  tinyHybrid = 0          
+        (* other doubles *)
+        /\  shortLongDouble = 0
+        /\  tinyShortDouble = 0                    
+        /\  product = 0
+        (* stage & cycle *)
+        /\ stage = "init"
+        /\ cycle = 0 \* no cycles completed
+
+(* gathering up actions *)
+Next == \/ heat
+        \/ cool
+        \/ anneal
+        \/ extend
+
+(* system spec *)
+Spec == /\ Init 
+        /\ [][Next]_vars 
+        /\ WF_vars(anneal) 
+        /\ WF_vars(heat)
+        /\ WF_vars(cool)
+        /\ WF_vars(extend)
+
+(* type invariant *)
+TypeOK == 
+    /\ tee \in {"Warm", "Hot", "TooHot"}
+    /\ primer \in Nat
+    /\ dna \in Nat
+    /\ template \in Nat
+    /\ hybrid \in Nat
+    /\ stage \in {"init","ready","annealed","extended","denatured"}
+    /\ cycle \in Nat
+    /\ longTemplate \in Nat
+    /\ shortTemplate \in Nat
+    /\ tinyTemplate \in Nat
+    /\ longHybrid \in Nat
+    /\ shortHybrid \in Nat
+    /\ tinyHybrid \in Nat
+    /\ longLongDouble \in Nat
+    /\ shortLongDouble \in Nat
+    /\ tinyShortDouble \in Nat          
+    /\ product \in Nat
+
+(* safety *)
+thirdCycleProduct == ((cycle < 3) => (product = 0))
+
+(* refinement *)
+stagesInstance == INSTANCE stages WITH
+    template <- sumList(templates),
+    hybrid <- sumList(hybrids),
+    dna <- sumList(doubles)
+
+stagesSpec == stagesInstance!Spec
+
+primerDepleted == stagesInstance!primerDepleted
+
+=============================================================================
+