diff --git a/specifications/README b/specifications/README index 9605b73d..4ad52ca8 100644 --- a/specifications/README +++ b/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 diff --git a/specifications/glowingRaccoon/clean.tla b/specifications/glowingRaccoon/clean.tla new file mode 100644 index 00000000..e0e0333e --- /dev/null +++ b/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 <> + /\ 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! + +============================================================================= diff --git a/specifications/glowingRaccoon/product.tla b/specifications/glowingRaccoon/product.tla new file mode 100644 index 00000000..c9e2d18b --- /dev/null +++ b/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 == <> + +(* more variable lists, for convenience *) +templates == <> + +hybrids == <> + +doubles == <> + +(* 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 <> + /\ 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 + +============================================================================= + diff --git a/specifications/glowingRaccoon/stages.tla b/specifications/glowingRaccoon/stages.tla new file mode 100644 index 00000000..6243f0ab --- /dev/null +++ b/specifications/glowingRaccoon/stages.tla @@ -0,0 +1,105 @@ +----------------------------- MODULE stages ----------------------------- + +\* The basic spec allowed senseless thermal changes. +\* You can think of "stage" as a history variable. +\* The previous action now dictates the next. +\* (and we can now show that primers get depleted, eventually) +\* This further enables us to count (legitimate) cycles of PCR. +\* (hence the new "cycle" variable) + +EXTENDS Naturals \* an import + +CONSTANTS DNA, PRIMER \* starting stock of key things + +VARIABLES tee, \* temperature + primer, \* count of primers remaining + dna, \* count of double strands present + template, \* count of single strands present + hybrid, \* count of template-primer hybrids + stage, \* new arrival - a history of sorts + cycle \* now we can count...! + +(* list of state variables, for convenience *) +vars == << tee, primer, dna, template, hybrid, stage, cycle >> + +(* helper function *) +natMin(i,j) == IF i < j THEN i ELSE j \* min of two nats + +(* steps *) +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 + /\ (stage = "init" \/ stage = "extended") + /\ stage' = "denatured" + /\ UNCHANGED cycle + +cool == /\ tee = "TooHot" \* when you just denatured + /\ tee' = "Hot" \* cool off to "Hot" + /\ UNCHANGED << cycle, primer, dna, template, hybrid >> + /\ stage = "denatured" + /\ stage' = "ready" + +anneal == /\ tee = "Hot" \* too hot to anneal primers + /\ tee' = "Warm" \* "Warm" is just right + /\ UNCHANGED <> \* 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 + /\ stage = "ready" + /\ stage' = "annealed" + +extend == /\ tee = "Warm" \* too cool for extension + /\ tee' = "Hot" \* "Hot" is just right + /\ UNCHANGED <> + /\ dna' = dna + hybrid \* assuming it just happens + /\ hybrid' = 0 \* all turned to dna + /\ 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 + /\ dna = DNA \* we start with some nice 'frozen' dna + /\ template = 0 \* everything is bound up + /\ hybrid = 0 \* no annealing has happened yet + /\ 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 + +(* instance of clean *) +cleanInstance == INSTANCE clean +cleanSpec == cleanInstance!Spec +primerDepleted == cleanInstance!primerDepleted + + + +=============================================================================