Merge branch 'kmilner-update-annotations'

src/009_precomputation.md

@@ -231,3 +231,24 @@ Tamarin shows a warning on the command line when this limit is reached.
 Default value: `5`
 
 In case Tamarin's precomputations take too long, try fixing smaller values for both parameters, and analyze the sources shown in interactive mode to understand what exactly caused the problem.
+
+Loop breakers {#sec:loopbreakers}
+-----------
+During the precomputation phase, Tamarin determines a minimal set of 'loop-breakers',
+which are premises that can be excluded from the general precomputation of all premise goals 
+to prevent looping. Specifically, the set of loop breakers is a minimal set of premises
+that can be excluded to make the directed graph of rules, when connected from conclusions
+to premises, acyclic.
+
+It is important to note that there is often no unique minimal set of loop-breakers. The
+loop-breaker computation is deterministic for a given set of rules, but a change to
+the set of rules may result in different premises being considered loop-breakers. As such,
+you may find that a small change or addition of a rule to your model can result in changes
+to how some seemingly unrelated properties are solved.
+
+It is possible to manually break loops in particular places by annotating the relevant
+premise with the `no_precomp` annotation. These premises will then be excluded when computing
+loop-breakers over the rule set, and will not have their sources precomputed.
+For more on fact annotations, see 
+[Fact Annotations](011_advanced-features.html#sec:fact-annotations).
+

src/011_advanced-features.md

@@ -139,6 +139,12 @@ with a rule conclusion containing `A(x)`. This allows multiple instances
 of the same fact to be solved with different priorities by annotating them
 differently.
 
+When an `In()` premise is annotated, the annotations are propagated up
+to the corresponding `!KU()` goals. For example, the premise `In(f(x))[+]`
+will generate a `!KU(f(x))[+]` goal that will be solved with high priority,
+while the premise `In(<y,g(y,z)>)[-]` will generate `!KU(y)[-]` and `!KU(g(y,z))[-]`
+goals to be solved with low priority.
+
 The `+` and `-` annotations can also be used to prioritize actions.
 For example, A reusable lemma of the form
 ```
@@ -153,13 +159,15 @@ respectively. Note however that these prefixes must apply to every instance
 of the fact, as a fact `F_A(x)` cannot unify with a fact `A(x)`.
 
 Facts in rule premises can also be annotated with `no_precomp` to prevent the
-tool from precomputing their sources.
-Use of the `no_precomp` annotation in key places can be very
-useful for reducing the precomputation time required to load large models, however
-it should be used sparingly. Preventing the precomputation of sources for a premise
-that is solved frequently will typically slow down the tool, as it must solve the
-premise each time instead of directly applying precomputed sources. Note also that
-using this annotation may cause partial deconstructions if the source of a premise
+tool from precomputing their sources, and to prevent them from being considered
+during the computation of loop-breakers.
+Use of the `no_precomp` annotation allows the modeller to manually control how
+loops are broken, or can be used to reduce
+the precomputation time required to load large models. Note, however
+that preventing the precomputation of sources for a premise
+that is solved frequently will typically slow down the tool, as there will be no
+precomputed sources to apply. Using this annotation may also cause 
+partial deconstructions if the source of a premise
 was necessary to compute a full deconstruction.
 
 The `no_precomp` annotation can be used in combination with heuristic annotations