From 0fc008fe331dac789c928058887f4c597d3fa1d3 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 20 Aug 2004 19:16:56 +0000 Subject: [PATCH] - Added keylevels to symbols. This is to help pruning the proofs, for terms and patterns that do not originate on regular nodes. --- src/compiler.c | 11 +++++ src/symbol.c | 41 +++++++++++++++++ src/symbol.h | 3 ++ src/term.c | 118 +++++++++++++++++++++++++++++++++++++------------ src/term.h | 1 + src/todo.txt | 1 + 6 files changed, 146 insertions(+), 29 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index 3ddd37a..33736ca 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -140,6 +140,9 @@ compile (Tac tc, int maxrunsset) /* process the tac */ tacProcess (tac_root); + /* Clean up keylevels */ + symbol_fix_keylevels (); + /* cleanup */ levelDone (); } @@ -402,6 +405,14 @@ commEvent (int event, Tac tc) msg = tacTerm (tacTuple ((trip->next->next))); cl = NULL; + if (event == SEND) + { + /* set keylevels based on send events */ + term_set_keylevels (fromrole); + term_set_keylevels (torole); + term_set_keylevels (msg); + } + break; case CLAIM: /* now parse tuple info */ diff --git a/src/symbol.c b/src/symbol.c index 7abd442..18c375f 100644 --- a/src/symbol.c +++ b/src/symbol.c @@ -1,8 +1,10 @@ #include #include #include +#include #include "symbol.h" +#include "debug.h" #include "memory.h" /* @@ -79,6 +81,7 @@ get_symb (void) t->allocnext = symb_alloc; symb_alloc = t; } + t->keylevel = INT_MAX; return t; } @@ -206,6 +209,44 @@ symbolSysConst (const char *str) return symb; } +//! Fix all the unset keylevels +void +symbol_fix_keylevels (void) +{ + int i; + + for (i = 0; i < HASHSIZE; i++) + { + Symbol sym; + + sym = symbtab[i]; + while (sym != NULL) + { +#ifdef DEBUG + if (DEBUGL (5)) + { + eprintf ("Symbol "); + symbolPrint (sym); + } +#endif + if (sym->keylevel == INT_MAX) + { + // Nothing currently, this simply does not originate on a strand. + } +#ifdef DEBUG + else + { + if (DEBUGL (5)) + { + eprintf (" has keylevel %i\n", sym->keylevel); + } + } +#endif + sym = sym->next; + } + } +} + //! Print out according to globalError /** * Input is comparable to printf, only depends on globalError. This should be used by any function trying to do output. diff --git a/src/symbol.h b/src/symbol.h index cbcb090..6d74bb5 100644 --- a/src/symbol.h +++ b/src/symbol.h @@ -20,6 +20,8 @@ struct symbol int type; //! Line number at which it occurred. int lineno; + //! Level of occurrence in role nodes. 0 for as non-key, 1 for key only, 2 for key of key only, etc.. + int keylevel; //! Ascii string with name of the symbol. const char *text; //! Possible next pointer. @@ -41,6 +43,7 @@ Symbol lookup (const char *s); void symbolPrint (const Symbol s); void symbolPrintAll (void); Symbol symbolSysConst (const char *str); +void symbol_fix_keylevels (void); void eprintf (char *fmt, ...); diff --git a/src/term.c b/src/term.c index c47270e..ed67f30 100644 --- a/src/term.c +++ b/src/term.c @@ -962,7 +962,7 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (), //! Generic term iteration int term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), - int (*nodem) (), int (*noder) ()) + int (*nodem) (), int (*noder) ()) { term = deVar (term); if (term != NULL) @@ -986,20 +986,26 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (), if (realTermTuple (term)) flag = flag - && (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder)); + && + (term_iterate_deVar + (term->left.op1, leaf, nodel, nodem, noder)); else flag = flag - && (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder)); + && + (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder)); if (nodem != NULL) flag = flag && nodem (term); if (realTermTuple (term)) flag = flag - && (term_iterate_deVar (term->left.op1, leaf, nodel, nodem, noder)); + && + (term_iterate_deVar + (term->left.op1, leaf, nodel, nodem, noder)); else flag = flag - && (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder)); + && + (term_iterate_deVar (term->left.op, leaf, nodel, nodem, noder)); if (noder != NULL) flag = flag && noder (term); @@ -1108,30 +1114,29 @@ term_constrain_level (const Term term) int structure; int flag; - void - tcl_iterate (Term t) - { - t = deVar (t); - structure++; - if (realTermLeaf (t)) - { - if (realTermVariable (t)) - vars++; - } - else - { - if (realTermTuple (t)) - { - tcl_iterate (t->left.op1); - tcl_iterate (t->right.op2); - } - else - { - tcl_iterate (t->left.op); - tcl_iterate (t->right.key); - } - } - } + void tcl_iterate (Term t) + { + t = deVar (t); + structure++; + if (realTermLeaf (t)) + { + if (realTermVariable (t)) + vars++; + } + else + { + if (realTermTuple (t)) + { + tcl_iterate (t->left.op1); + tcl_iterate (t->right.op2); + } + else + { + tcl_iterate (t->left.op); + tcl_iterate (t->right.key); + } + } + } if (term == NULL) error ("Cannot determine constrain level of empty term."); @@ -1141,3 +1146,58 @@ term_constrain_level (const Term term) tcl_iterate (term); return ((float) vars / (float) structure); } + +//! Adjust the keylevels of the symbols in a term. +/** + * This is used to scan the roles. For each symbol, this function does the bookkeeping of the keylevels at which they occur. + */ +void +term_set_keylevels (const Term term) +{ + void scan_levels (int level, Term t) + { +#ifdef DEBUG + if (DEBUGL (5)) + { + int c; + + c = 0; + while (c < level) + { + eprintf (" "); + c++; + } + eprintf ("Scanning keylevel %i for term ", level); + termPrint (t); + eprintf ("\n"); + } +#endif + if (realTermLeaf (t)) + { + Symbol sym; + + // So, it occurs at 'level' as key. If that is less than known, store. + sym = t->left.symb; + if (level < sym->keylevel) + { + // New minimum level + sym->keylevel = level; + } + } + else + { + if (realTermTuple (t)) + { + scan_levels (level, t->left.op1); + scan_levels (level, t->right.op2); + } + else + { + scan_levels (level, t->left.op); + scan_levels ((level + 1), t->right.key); + } + } + } + + scan_levels (0, term); +} diff --git a/src/term.h b/src/term.h index 2effd7b..e9a2ba8 100644 --- a/src/term.h +++ b/src/term.h @@ -177,5 +177,6 @@ int term_iterate_open_leaves (const Term term, int (*func) ()); void term_rolelocals_are_variables (); int term_encryption_level (const Term term); float term_constrain_level (const Term term); +void term_set_keylevels (const Term term); #endif diff --git a/src/todo.txt b/src/todo.txt index a1d2458..eb271ad 100644 --- a/src/todo.txt +++ b/src/todo.txt @@ -1,3 +1,4 @@ +- Agent terms must have keylevel 0; enforce this! - './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. - Select_goal should consider, for singular variables, whether their type can be found in M_0. If so, the goal can be ignored.