From 8b30526a574d67c1a5a0b7ba6c1ed59b41c010dd Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 7 Jan 2006 13:28:13 +0000 Subject: [PATCH] - Added a note about inversekeys in a role definition. --- src/todo.txt | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/todo.txt b/src/todo.txt index a6b8544..e9e75ff 100644 --- a/src/todo.txt +++ b/src/todo.txt @@ -1,5 +1,7 @@ -- Add '--untyped' check for typeflaw detection (instead of the fairly - vague '--match'. +- 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. - Warshall is taking a third of the time running. - Make 'dirty' flag. - Make a push-graph structure, where old graphs are simply remembered? @@ -28,8 +30,7 @@ int termSymbolEqual(Term t1, Term t2); Iteration through the termlist should be done by hand. - Maybe add warning for type of matching in the output, maybe stderr. + Maybe all state-space bounding info should be displayed. - SConstruct file should check whether ctags actually exists (avoiding errors) - Proof output should be XML, with an external converter to dot format. -- Internal hash over input files (maybe after parsing?) and switch - structure. This would make a caching mechanism much easier.