Document feature oracle-ranking

See tamarin-prover/tamarin-prover#406.

src/010_advanced-features.md

@@ -10,13 +10,21 @@ preprocessor, and how to measure the time needed for proofs.
 Heuristics {#sec:heuristics}
 ----------
 
-The default heuristic for the automated proof methods can be set either through
-the inclusion of a heuristic choice in the protocol file, or by using a
-commandline option. A heuristic is specified as a word built from the alphabet
-`{s,S,c,C,i,I,o,O}`, with each letter describing a different way to rank the open
-goals of a constraint system. Specifying a default heuristic within a protocol file
-can be done by including `heuristic:` followed by the heuristic, or by using the
-`--heuristic` command line option with the heuristic as the argument.
+A heuristic describes a method to rank the open goals of a constraint system and is specified as a sequence of goal rankings.
+Each goal ranking is abbreviated by a single character from the set `{s,S,c,C,i,I,o,O}`.
+
+A global heuristic for a protocol file can be defined using the `heuristic:` statement followed by the sequence of goal rankings.
+The heuristic which is used for a particular lemma can be overwritten using the `heuristic` lemma attribute.
+Finally, the heuristic can be specified using the `--heuristic` command line option.
+
+\pagebreak
+
+The precedence of heuristics is:
+
+1. Command line option (`--heuristic`)
+2. Lemma attribute (`heuristic=`)
+3. Global (`heuristic:`)
+4. Default (`s`)
 
 The goal rankings are as follows.
 
@@ -66,10 +74,12 @@ The goal rankings are as follows.
 `o`:
 : is the oracle ranking. It allows the user to provide an arbitrary program
   that runs independently of Tamarin and ranks the proof goals.
-  The program must be named `oracle`. Moreover, it must be executable from the
-  current working directory, i.e., with `./oracle`.
-  Alternatively, a different file name, say `FILE`, can be used when
-  additionally passing the `--oraclename=FILE` flag as commandline option (default is `oracle`).
+  The path of the program can be specified after the goal ranking, e.g., `o "oracles/oracle-default"`
+  to use the program `oracles/oracle-default` as the oracle.
+  If no path is specified, the default is `oracle`.
+  The path of the program is relative to the directory of the protocol file containing the goal ranking.
+  If the heuristic is specified using the `--heuristic` option, the path can be given using the
+  `--oraclename` command line option. In this case, the path is relative to the current working directory.
   The oracle's input is a numbered list
   of proof goals, given in the 'Consecutive' ranking (as generated by the heuristic `C`).
   Every line of the input is a new goal and starts with "%i: ", where %i is the
@@ -80,20 +90,14 @@ The goal rankings are as follows.
   In this case, the first goal of the 'Consecutive' ranking will be selected.
 
 `O`:
-: is the oracle ranking based on the 'smart' heuristic `s`. It works the same as `o` but uses 'smart' instead of 'Consecutive' ranking to start with.  Again, for using an oracle at location `FILE` one must
-  additionally pass the `--oraclename=FILE` flag as commandline option.
-
+: is the oracle ranking based on the 'smart' heuristic `s`. It works the same as `o` but uses 'smart' instead of 'Consecutive' ranking to start with.
 
 If several rankings are given for the heuristic flag, then they are employed
 in a round-robin fashion depending on the proof-depth. For example, a flag
 `--heuristic=ssC` always uses two times the smart ranking and then once the
 'Consecutive' goal ranking. The idea is that you can mix goal rankings easily
 in this way.
 
-Individual lemmas may also specify a heuristic to be used when solving them,
-instead of the default heuristic. This is done with the `heuristic=` lemma annotation
-followed by the heuristic.
-
 Fact annotations {#sec:fact-annotations}
 -------------------
 
@@ -156,6 +160,8 @@ Assume the following theory.
 ```
 theory SourceOfUniqueness begin
 
+heuristic: o "myoracle"
+
 builtins: symmetric-encryption
 
 rule generatecomplicated:
@@ -190,8 +196,9 @@ end
 We use the following oracle to generate an efficient proof.
 
 ```
-#!/usr/bin/python
+#!/usr/bin/env python
 
+from __future__ import print_function
 import sys
 
 lines = sys.stdin.readlines()
@@ -221,13 +228,13 @@ for line in lines:
 ranked = l1 + l2 + l3 + l4
 
 for i in ranked:
-  print i
+  print(i)
 ```
 
 Having saved the Tamarin theory in the file `SourceOfUniqueness.spthy`
 and the oracle in the file `myoracle`, we can prove the lemma `uniqueness`, using the following command.
 ```
-tamarin-prover --prove=uniqueness --heuristic=o --oraclename=myoracle SourceOfUniqueness.spthy
+tamarin-prover --prove=uniqueness SourceOfUniqueness.spthy
 ```
 
 The generated proof consists of only 10 steps.

src/015_syntax_description.md

@@ -46,11 +46,13 @@ enable it to parse terms containing exponentiations, e.g.,  g ^ x.
                     | 'multiset' | 'revealing-signing'
 
 A global heuristic sets the default heuristic that will be used when autoproving
-lemmas in the file. The specified heuristic can be any of those discussed in
+lemmas in the file. The specified goal ranking can be any of those discussed in
 Section [Heuristics](009_advanced-features.html#sec:heuristics).
 
-    global_heuristic := 'heuristic' ':' heuristic
-    heuristic        := alpha+
+    global_heuristic      := 'heuristic' ':' goal_ranking+
+    goal_ranking          := standard_goal_ranking | oracle_goal_ganking
+    standard_goal_ranking := 'C' | 'I' | 'P' | 'S' | 'c' | 'i' | 'p' | 's'
+    oracle_goal_ranking   := 'o' '"' [^'"']* '"' | 'O' '"' [^'"']* '"'
 
 Multiset rewriting rules are specified as follows. The protocol corresponding
 to a security protocol theory is the set of all multiset rewriting rules
@@ -103,13 +105,13 @@ quantifier.
              proof_skeleton
     lemma_attrs      := '[' lemma_attr (',' lemma_attr)* ']'
     lemma_attr       := 'sources' | 'reuse' | 'use_induction' |
-                             'hide_lemma=' ident | 'heuristic=' heuristic
+                             'hide_lemma=' ident | 'heuristic=' goalRanking+
     trace_quantifier := 'all-traces' | 'exists-trace'
 
 In observational equivalence mode, lemmas can be associated to one side.
 
     lemma_attrs      := '[' ('sources' | 'reuse' | 'use_induction' | 
-                             'hide_lemma=' ident | 'heuristic=' heuristic |
+                             'hide_lemma=' ident | 'heuristic=' goalRanking+ |
                              'left' | 'right') ']'
 
 A proof skeleton is a complete or partial proof as output by the Tamarin prover.