Moved todo text into a more sensible place.

src/todo.txt

@@ -1,54 +0,0 @@
-- When saving a file after 'file changed' warning, an overwrite of the
-  same file should not necessarily generate a warning.
-- Output (claim summary) might have a parameter summary somewhere.
-- Error should have an additional line number parameter (that might be
-  -1 to ignore it) forcing people to use numbers :)
-  Format: "error: [%i] %s\n"
-- Nested functions should be avoided: their implementation requires an
-  executable stack, which is bad for security purposes. However, many of
-  the iterator functions need to pass a function and possibly some
-  variables. Currently, the variables are handled by the nested function
-  mechanism (the iterated nested function and address variables of the
-  function it is part of), which would not work anymore. A possible
-  solution seems variable argument count functions, but this is fairly
-  cumbersome and might impact on performance. Alternatively, iterators
-  can be implemented as macros, which is probably the fastest, but maybe
-  less readable.
-- --check is slightly f***ed up because there is no good semantics for
-  the --disable intruder check. As a result, it is now too strict can
-  cause correct protocols to fail. Fix.
-- When *not* asking for attack output, maybe we should default to
-  --prune = 1. Then, if we ask for --xml output or --dot, we do:
-  if --prune == 1 then --prune == 2 now :) unless otherwise specified.
-  (This should be done after switch checking)
-- Old version enforced some extra orders:
-  1. M_0 roles were ordered before any other roles.
-  2. Local constants order: if a run has a local variable instantiated by
-  somebody else's variable, that should occur then after the initial sending
-  of that value...
-- Test 'sk(x)' in goals, somewhere before assessing a state (dus at the
-  beginning of iterate), immediately reduce to 'sk(Eve)'. Test with
-  --experimental. To that end, reintroduce a state-reporting switch.
-- It is currently not well-defined to define inversekeys within a role:
-  this requires some work at instantiation, because instantiated term
-  couples should be added to the inverses list, and removed at
-  descruction.
-- Simple timestamps could be added by prefixing send message before the
-  role, sending any timestamp constants out first to the intruder. These
-  should of course be hidden in the output somehow.
-- Notes on the new attack group displays:
-  * We want to group runs into consistent protocol runs.
-  * Minimal req. for protocol run: equal \rho.
-  * If two runs are candidates for a role in a protocol run,
-    use a metric based on order and data. Maybe data is more important:
-    if equal data, than order might be irrelevant.
-  * Maybe we should refactor the xmlOut code first. In an extreme case,
-    we first factor out all logic, and ranking, and grouping, in to a
-    prepareAttackOutput structure; with a separate source file. Later we
-    can convert this to either ASCII or DOT or XML or something.
-    Now that I think of it; XML should be a plain state probably, and we
-    could add a switch to also output more detailed attack things (is
-    that relevant?)
-- SConstruct file should check whether ctags actually exists (avoiding
-  errors)
-- Proof output should be XML, with an external converter to dot format.