diff --git a/src/arachne.c b/src/arachne.c index 5129231..1e75cf9 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -36,6 +36,7 @@ Role I_E; Role I_D; static int indentDepth; +static int max_encryption_level; #ifdef DEBUG static char *explanation; // Pointer to a string that describes what we just tried to do @@ -68,6 +69,7 @@ int iterate (); void arachneInit (const System mysys) { + Term GVT; Roledef rd = NULL; Termlist tl, know0; @@ -102,8 +104,9 @@ arachneInit (const System mysys) */ INTRUDER = protocolCreate (makeGlobalConstant (" INTRUDER ")); + GVT = makeGlobalVariable ("GlobalVariable"); - add_event (SEND, NULL); + add_event (SEND, GVT); I_M = add_role ("I_M: Atomic message"); add_event (READ, NULL); @@ -148,6 +151,18 @@ indentPrint () #endif } +//! Print indented binding +void +binding_indent_print (Binding b, int flag) +{ + indentPrint (); + if (flag) + eprintf ("!! "); + binding_print (b); + eprintf ("\n"); +} + + //! Iterate but discard the info of the termlist int mgu_iterate (const Termlist tl) @@ -161,7 +176,7 @@ mgu_iterate (const Termlist tl) *@returns The number of goals added (for destructions) */ int -add_read_goals (const int run, int old, int new) +add_read_goals (const int run, const int old, const int new) { int count; int i; @@ -170,11 +185,13 @@ add_read_goals (const int run, int old, int new) sys->runs[run].length = new; i = old; rd = roledef_shift (sys->runs[run].start, i); - while (i < new) + count = 0; + while (i < new && rd != NULL) { if (rd->type == READ) { goal_add (rd->message, run, i); + count++; } rd = rd->next; i++; @@ -186,7 +203,7 @@ add_read_goals (const int run, int old, int new) void remove_read_goals (int n) { - while (n>0) + while (n > 0) { goal_remove_last (); n--; @@ -301,43 +318,59 @@ bind_existing_to_goal (const Binding b, const int index, const int run, int subterm_iterate (Termlist substlist, Termlist keylist) { - int keycount; int flag; -#ifdef DEBUG - if (DEBUGL (5)) - { - indentPrint (); - eprintf ("Adding key list : "); - termlistPrint (keylist); - eprintf ("\n"); - } -#endif flag = 1; - keycount = 0; - while (flag && keylist != NULL) + if (goal_bind (b, run, index)) { - int keyrun; + int keycount; + Termlist tl; - goal_add (keylist->term, b->run_to, b->ev_to); - keylist = keylist->next; - keycount++; +#ifdef DEBUG + if (DEBUGL (5)) + { + binding_indent_print (b, 0); + indentPrint (); + eprintf ("Adding key list for subterm iteration: "); + termlistPrint (keylist); + eprintf ("\n"); + } +#endif + keycount = 0; + tl = keylist; + while (tl != NULL) + { + int keyrun; + + goal_add (tl->term, b->run_to, b->ev_to); + tl = tl->next; + keycount++; + } + + flag = flag && iterate (); + + while (keycount > 0) + { + goal_remove_last (); + keycount--; + } + termlistDestroy (keylist); } - flag = flag && iterate (); - while (keycount > 0) + else { - goal_remove_last (); - keycount--; +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Aborted binding existing run because of cycle.\n"); + } +#endif + flag = 0; } - termlistDestroy (keylist); + goal_unbind (b); return flag; } - int interm_iterate (Termlist substlist) - { - iterate (); - } - //---------------------------- // Roledef entry rd = roledef_shift (sys->runs[run].start, index); @@ -345,13 +378,9 @@ bind_existing_to_goal (const Binding b, const int index, const int run, // Fix length old_length = sys->runs[run].length; if ((index + 1) > old_length) - { - newgoals = add_read_goals (run, old_length, index+1); - } + newgoals = add_read_goals (run, old_length, index + 1); else - { - newgoals = 0; - } + newgoals = 0; #ifdef DEBUG if (DEBUGL (3)) @@ -361,30 +390,8 @@ bind_existing_to_goal (const Binding b, const int index, const int run, e_term1 = b->term; } #endif - if (goal_bind (b, run, index)) - { - if (subterm) - { - flag = termMguSubTerm (b->term, rd->message, - subterm_iterate, sys->know->inverses, NULL); - } - else - { - flag = termMguInTerm (b->term, rd->message, - interm_iterate); - } - } - else - { -#ifdef DEBUG - if (DEBUGL (5)) - { - indentPrint (); - eprintf ("Aborted binding existing run because of cycle.\n"); - } -#endif - } - goal_unbind (b); + flag = termMguSubTerm (b->term, rd->message, + subterm_iterate, sys->know->inverses, NULL); // Reset length remove_read_goals (newgoals); sys->runs[run].length = old_length; @@ -404,7 +411,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, indentPrint (); eprintf ("Trying to bind "); termPrint (b->term); - eprintf (" to an existing instance of "); + eprintf (" to an existing (of %i runs) instance of ", sys->maxruns); termPrint (p->nameterm); eprintf (", "); termPrint (r->nameterm); @@ -433,7 +440,7 @@ bind_new_run (const Binding b, const Protocol p, const Role r, roleInstance (sys, p, r, NULL, NULL); run = sys->maxruns - 1; - newgoals = add_read_goals (run, 0, index+1); + newgoals = add_read_goals (run, 0, index + 1); #ifdef DEBUG if (DEBUGL (4)) { @@ -447,9 +454,9 @@ bind_new_run (const Binding b, const Protocol p, const Role r, eprintf (", run %i (subterm:%i)\n", run, subterm); } #endif - flag = bind_existing_to_goal (b, index, run, subterm); - roleInstanceDestroy (sys); + flag = bind_existing_to_goal (b, index, run, 1); remove_read_goals (newgoals); + roleInstanceDestroy (sys); return flag; } @@ -461,11 +468,9 @@ printSemiState () int open; List bl; - int binding_indent_print (void *data) + int binding_state_print (void *dt) { - indentPrint (); - eprintf ("!! "); - binding_print (data); + binding_indent_print ((Binding) dt, 1); return 1; } @@ -515,7 +520,7 @@ printSemiState () { indentPrint (); eprintf ("!!\n"); - list_iterate (sys->bindings, binding_indent_print); + list_iterate (sys->bindings, binding_state_print); } indentPrint (); eprintf ("!!\n"); @@ -536,7 +541,9 @@ select_goal () { List bl; Binding best; + float min_constrain; + min_constrain = 2; // 1 is the maximum, but we want to initialize it. best = NULL; bl = sys->bindings; while (bl != NULL) @@ -546,141 +553,20 @@ select_goal () b = (Binding) bl->data; if (!b->done) { - // For now, we simply take the first encountered goal - return b; + float cons; + + cons = term_constrain_level (b->term); + if (cons < min_constrain) + { + min_constrain = cons; + best = b; + } } bl = bl->next; } return best; } -//! Bind a regular goal -int -bind_goal_regular (const Binding b) -{ - int flag; - /* - * This is a local function so we have access to goal - */ - int bind_this_role_send (Protocol p, Role r, Roledef rd, int index) - { - int test_unification (Termlist substlist) - { - // A unification exists; return the signal - return 0; - } - - if (p == INTRUDER) - { - /* only bind to regular runs */ - return 1; - } - else - { - // Test for interm unification -#ifdef DEBUG - if (DEBUGL (5)) - { - indentPrint (); - eprintf ("Checking send candidate with message "); - termPrint (rd->message); - eprintf (" from "); - termPrint (p->nameterm); - eprintf (", "); - termPrint (r->nameterm); - eprintf (", index %i\n", index); - } -#endif - if (!termMguInTerm (b->term, rd->message, test_unification)) - { - // A good candidate -#ifdef DEBUG - if (DEBUGL (5)) - { - indentPrint (); - eprintf ("Term "); - termPrint (b->term); - eprintf (" can possibly be bound by role "); - termPrint (r->nameterm); - eprintf (", index %i\n", index); - } -#endif - return (bind_new_run (b, p, r, index, 0) && - bind_existing_run (b, p, r, index, 0)); - } - else - { - // Cannot unify: no attacks - return 1; - } - } - } - - // Bind to all possible sends or intruder node; -#ifdef DEBUG - if (DEBUGL (5)) - { - indentPrint (); - eprintf ("Try regular role send.\n"); - } -#endif - flag = iterate_role_sends (bind_this_role_send); -#ifdef DEBUG - if (DEBUGL (5)) - { - indentPrint (); - eprintf ("Try intruder send.\n"); - } -#endif - return flag; - // return (flag && add_intruder_goal_iterate (b)); -} - -//! Bind an intruder goal to a regular run -int -bind_intruder_to_regular (Binding b) -{ - int bind_this_roleevent (Protocol p, Role r, Roledef rd, int index) - { - int cannotUnify; - - int test_unification (Termlist substlist, Termlist keylist) - { - // Signal that unification is possible. - return 0; - } - - /** - * Note that we only bind to regular runs here - */ - if (p == INTRUDER) - { - return 1; // don't abort scans - } - else - { // Test for subterm unification - if (termMguSubTerm - (b->term, rd->message, test_unification, - sys->know->inverses, NULL)) - { - // cannot unify - return 1; - } - else - { - /** - * Either from an existing, or from a new run. - */ - return (bind_new_run (b, p, r, index, 1) - && bind_existing_run (b, p, r, index, 1)); - } - } - } - - // Bind to all possible sends? - return iterate_role_sends (bind_this_roleevent); -} - //! Bind an intruder goal by intruder construction /** * Handles the case where the intruder constructs a composed term himself. @@ -696,9 +582,9 @@ bind_intruder_to_construct (const Binding b) flag = 1; term = b->term; /** - * Two options. + * Three options. * - * 1. Constructed from composite terms + * 1. Constructed from smaller composite terms */ if (!realTermLeaf (term)) { @@ -706,6 +592,7 @@ bind_intruder_to_construct (const Binding b) if (realTermTuple (term)) { + warning ("Goal that is a tuple should not occur!"); // tuple construction t1 = term->left.op1; t2 = term->right.op2; @@ -719,12 +606,61 @@ bind_intruder_to_construct (const Binding b) goal_add (t1, b->run_to, b->ev_to); goal_add (t2, b->run_to, b->ev_to); +#ifdef DEBUG + if (DEBUGL (3)) + { + indentPrint (); + eprintf ("Constructing "); + termPrint (term); + eprintf (" from smaller terms "); + termPrint (t1); + eprintf (" and "); + termPrint (t2); + eprintf ("\n"); + } +#endif flag = flag && iterate (); goal_remove_last (); goal_remove_last (); } /** - * 2. Retrieved from M_0 + * 2. Constructed from bigger term and decryption key + */ + /* + if (!realTermLeaf (term)) + { + if (realTermEncrypt (term)) + { + Term t1, t2; + + t1 = term->left.op; + t2 = term->right.key; + + goal_add (t1, b->run_to, b->ev_to); + goal_add (t2, b->run_to, b->ev_to); + #ifdef DEBUG + if (DEBUGL (3)) + { + indentPrint (); + eprintf ("Deriving "); + termPrint (term); + eprintf (" from encrypted term "); + termPrint (t1); + eprintf (" and key "); + termPrint (t2); + eprintf ("\n"); + } + #endif + flag = flag && iterate (); + goal_remove_last (); + goal_remove_last (); + } + + } + */ + + /** + * 3. Retrieved from M_0 */ m0tl = knowledgeSet (sys->know); while (flag && m0tl != NULL) @@ -747,15 +683,20 @@ bind_intruder_to_construct (const Binding b) #ifdef DEBUG if (DEBUGL (3)) { + if (DEBUGL (5)) + { + binding_indent_print (b, 0); + } indentPrint (); eprintf ("Retrieving "); termPrint (term); eprintf (" from the initial knowledge.\n"); } #endif - iterate (); + flag = flag && iterate (); } goal_unbind (b); + roleInstanceDestroy (sys); termlistSubstReset (subst); termlistDelete (subst); } @@ -770,57 +711,104 @@ bind_intruder_to_construct (const Binding b) } -//! Bind an intruder goal -/** - * Computes F2 as in Athena explanations. - */ +//! Bind a regular goal int -bind_goal_intruder (const Binding b) +bind_goal_regular (const Binding b) { - /** - * Special case: when the intruder can bind it to the initial knowledge. - */ - Termlist tl; int flag; - flag = 1; - tl = knowledgeSet (sys->know); - while (flag && tl != NULL) + /* + * This is a local function so we have access to goal + */ + int bind_this_role_send (Protocol p, Role r, Roledef rd, int index) + { + int test_unification (Termlist substlist) { - int hasvars; - Termlist substlist; - - substlist = termMguTerm (tl->term, b->term); - if (substlist != MGUFAIL) - { - // This seems to work - flag = flag && iterate (); - termlistSubstReset (substlist); - termlistDelete (substlist); - } - tl = tl->next; + // A unification exists; return the signal + return 0; } - termlistDelete (tl); - return (flag && bind_intruder_to_regular (b) && - bind_intruder_to_construct (b)); + + // Test for interm unification +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Checking send candidate with message "); + termPrint (rd->message); + eprintf (" from "); + termPrint (p->nameterm); + eprintf (", "); + termPrint (r->nameterm); + eprintf (", index %i\n", index); + } +#endif + if (!termMguSubTerm + (b->term, rd->message, test_unification, sys->know->inverses, NULL)) + { + int flag; + + // A good candidate +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Term "); + termPrint (b->term); + eprintf (" can possibly be bound by role "); + termPrint (r->nameterm); + eprintf (", index %i\n", index); + } +#endif + // Bind to existing run + flag = bind_existing_run (b, p, r, index, 1); + if (p != INTRUDER) + { + // No intruder: bind to new run + flag = flag && bind_new_run (b, p, r, index, 1); + } + return flag; + } + else + { + // Cannot unify: no attacks + return 1; + } + } + + // Bind to all possible sends or intruder node; +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Try regular role send.\n"); + } +#endif + flag = iterate_role_sends (bind_this_role_send); +#ifdef DEBUG + if (DEBUGL (5)) + { + indentPrint (); + eprintf ("Try intruder send.\n"); + } +#endif + + // Other option: bind to term construction + + flag = flag && bind_intruder_to_construct (b); + + // Return result + return flag; } + + //! Bind a goal in all possible ways int bind_goal (const Binding b) { if (!b->done) { - int flag; - if (sys->runs[b->run_to].protocol == INTRUDER) - { - flag = bind_goal_intruder (b); - } - else - { - flag = bind_goal_regular (b); - } - return flag; + return bind_goal_regular (b); } else { @@ -906,6 +894,19 @@ prune () tl = tl->next; } + // Check for c-minimality + if (!bindings_c_minimal ()) + { +#ifdef DEBUG + if (DEBUGL (3)) + { + indentPrint (); + eprintf ("Pruned because this is not <=c-minimal.\n"); + } +#endif + return 1; + } + return 0; } @@ -976,7 +977,7 @@ iterate () */ b = select_goal (); - if (b != NULL) + if (b == NULL) { /* * all goals bound, check for property @@ -1046,11 +1047,26 @@ arachne () eprintf (", %i, ", index); roledefPrint (rd); eprintf ("\n"); + return 1; } + int determine_encrypt_max (Protocol p, Role r, Roledef rd, int index) + { + int tlevel; + + tlevel = term_encryption_level (rd->message); + if (tlevel > max_encryption_level) + max_encryption_level = tlevel; + return 1; + } + + max_encryption_level = 0; + iterate_role_sends (determine_encrypt_max); + #ifdef DEBUG if (DEBUGL (1)) { + eprintf ("Maximum encryption level: %i\n", max_encryption_level); iterate_role_sends (print_send); } #endif @@ -1123,13 +1139,3 @@ arachne () cl = cl->next; } } - -/** - * Done: add_read_goals, remove_read_goals. - * - * Now we must make the new algorithm. - * At role instance (of e.g. claim), fix add_read_goals. - * - * Iterate on roles. Create new roles for intruder (encrypt RRS, decrypt RRS, and M_0 S) - * Check for bindings_c_minimal. - */ diff --git a/src/binding.c b/src/binding.c index 8788946..79aeddd 100644 --- a/src/binding.c +++ b/src/binding.c @@ -11,7 +11,7 @@ #include "term.h" static System sys; -static int* graph; +static int *graph; static int nodes; /* @@ -78,7 +78,8 @@ bindingDone () } //! Destroy graph -void goal_graph_destroy () +void +goal_graph_destroy () { if (graph != NULL) { @@ -88,13 +89,14 @@ void goal_graph_destroy () } //! Compute unclosed graph -void goal_graph_create () +void +goal_graph_create () { int run, ev; List bl; goal_graph_destroy (); - + // Setup graph nodes = node_count (); graph = memAlloc ((nodes * nodes) * sizeof (int)); @@ -120,14 +122,18 @@ void goal_graph_create () Binding b; b = (Binding) bl->data; + if (b->done) + { #ifdef DEBUG - if (graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to) >= - (nodes * nodes)) - error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from, - b->ev_from, b->run_to, b->ev_to); + if (graph_nodes + (nodes, b->run_from, b->ev_from, b->run_to, + b->ev_to) >= (nodes * nodes)) + error ("Node out of scope for %i,%i -> %i,%i.\n", b->run_from, + b->ev_from, b->run_to, b->ev_to); #endif - graph[graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] - = 1; + graph[graph_nodes + (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)] = 1; + } bl = bl->next; } } @@ -203,13 +209,14 @@ graph_nodes (const int nodes, const int run1, const int ev1, const int run2, //! Print a binding (given a binding list pointer) int -binding_print (void *bindany) +binding_print (const Binding b) { - Binding b; - - b = (Binding) bindany; - eprintf ("Binding (%i,%i) --->> (%i,%i)\n", b->run_from, b->ev_from, - b->run_to, b->ev_to); + if (b->done) + eprintf ("Binding (%i,%i) --( ", b->run_from, b->ev_from); + else + eprintf ("Unbound --( "); + termPrint (b->term); + eprintf (" )->> (%i,%i)", b->run_to, b->ev_to); return 1; } @@ -306,51 +313,63 @@ goal_unbind (const Binding b) * *@returns True, if it's okay. If false, it needs to be pruned. */ -int bindings_c_minimal () +int +bindings_c_minimal () { List bl; // Ensure a state graph - goal_graph_create (); + if (graph == NULL) + { + goal_graph_create (); + // Recompute closure; does that work? + if (!warshall (graph, nodes)) + { + // Hmm, cycle + return 0; + } + } + // For all goals bl = sys->bindings; while (bl != NULL) { Binding b; - int run; - int node_from; b = (Binding) bl->data; - node_from = node_number (b->run_from, b->ev_from); - // Find all preceding events - for (run = 0; run <= sys->maxruns; run++) + if (b->done) { - int ev; + int run; + int node_from; - //!@todo hardcoded reference to step, should be length - for (ev = 0; run < sys->runs[run].step; ev++) + node_from = node_number (b->run_from, b->ev_from); + // Find all preceding events + for (run = 0; run <= sys->maxruns; run++) { - int node_comp; + int ev; - node_comp = node_number (run, ev); - if (graph[ graph_index (node_comp, node_from)] > 0) + //!@todo hardcoded reference to step, should be length + for (ev = 0; run < sys->runs[run].step; ev++) { - // this node is *before* the from node - Roledef rd; + int node_comp; - rd = roledef_shift (sys->runs[run].start, ev); - if (termInTerm (rd->message, b->term)) + node_comp = node_number (run, ev); + if (graph[graph_index (node_comp, node_from)] > 0) { - // This term already occurs as interm in a previous node! - return 0; + // this node is *before* the from node + Roledef rd; + + rd = roledef_shift (sys->runs[run].start, ev); + if (termInTerm (rd->message, b->term)) + { + // This term already occurs as interm in a previous node! + return 0; + } } } } } - - bl = bl->next; } return 1; } - diff --git a/src/binding.h b/src/binding.h index ba7b522..48b97bc 100644 --- a/src/binding.h +++ b/src/binding.h @@ -9,8 +9,8 @@ */ struct binding { - int done; //!< Iff true, it is bound - int child; //!< Signifies some tuple unfolding, to remove created bindings. + int done; //!< Iff true, it is bound + int child; //!< Signifies some tuple unfolding, to remove created bindings. int run_from; int ev_from; @@ -34,7 +34,7 @@ int node_count (); int node_number (int run, int ev); -int binding_print (void *bindany); +int binding_print (Binding b); void goal_add (Term term, const int run, const int ev); void goal_remove_last (); diff --git a/src/compiler.c b/src/compiler.c index 594652a..f67aed7 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -109,6 +109,13 @@ makeGlobalConstant (const char *s) return levelDeclare (symbolSysConst (s), 0, 0); } +//! Make a global variable +Term +makeGlobalVariable (const char *s) +{ + return levelDeclare (symbolSysConst (s), 1, 0); +} + //! Clean up afterwards void compilerDone (void) diff --git a/src/compiler.h b/src/compiler.h index 5bb1746..7ea6969 100644 --- a/src/compiler.h +++ b/src/compiler.h @@ -12,6 +12,7 @@ void compile (Tac tc, int maxruns); void preprocess (const System sys); Term findGlobalConstant (const char *s); Term makeGlobalConstant (const char *s); +Term makeGlobalVariable (const char *s); void compute_role_variables (const System sys, Protocol p, Role r); #endif diff --git a/src/ns3 b/src/ns3 index 943fc7f..45148f9 100644 --- a/src/ns3 +++ b/src/ns3 @@ -12,8 +12,8 @@ protocol ns3(I,R) send_1(I,R, {I,ni}pk(R) ); read_2(R,I, {ni,nr}pk(I) ); send_3(I,R, {nr}pk(R) ); - claim_4(I,Secret,ni,nr); - claim_6(I,Nisynch); +// claim_4(I,Secret,ni,nr); +// claim_6(I,Nisynch); } role R @@ -24,49 +24,13 @@ protocol ns3(I,R) read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); read_3(I,R, {nr}pk(R) ); - claim_5(R,Secret,ni,nr); - claim_7(R,Nisynch); + claim_5(R,Secret,nr); +// claim_5(R,Secret,ni,nr); +// claim_7(R,Nisynch); } } -// We leave out: M (from M_0) and Decryption, because that causes -// problems with the inverse key. -protocol I_MALICE (I_F, I_T, I_V, I_R, I_E) -{ - role I_F { - var t; - read_if1 (F,F, t); - } - role I_T { - var t; - read_it1 (T,T, t); - send_it2 (T,T, t); - send_it3 (T,T, t); - } - role I_V { - var t1; - var t2; - read_iv1 (V,V, t1); - read_iv2 (V,V, t2); - send_iv3 (V,V, (t1,t2)); - } - role I_R { - var t1; - var t2; - read_ir1 (I_R,I_R, (t1,t2)); - read_ir2 (I_R,I_R, t1); - send_ir3 (I_R,I_R, t2); - } - role I_E { - var t1; - var t2; - read_ie1 (I_E,I_E, t1); - read_ie2 (I_E,I_E, t2); - send_ie3 (I_E,I_E, {t1}t2); - } -} - -const Alice,Bob,Eve: Agent; +const Alice,Eve: Agent; untrusted Eve; const nc: Nonce; diff --git a/src/term.c b/src/term.c index 71e0ad0..24e8a1c 100644 --- a/src/term.c +++ b/src/term.c @@ -1037,3 +1037,69 @@ term_rolelocals_are_variables () { rolelocal_variable = 1; } + +//! Count the encryption level of a term +int +term_encryption_level (const Term term) +{ + int level, maxlevel, flag; + + int nodel (const Term term) + { + if (realTermEncrypt (term)) + { + level++; + if (level > maxlevel) + maxlevel = level; + } + return 1; + } + int noder (const Term term) + { + if (realTermEncrypt (term)) + { + level--; + } + return 1; + } + + maxlevel = 0; + level = 0; + flag = term_iterate_deVar (term, NULL, nodel, NULL, noder); + return maxlevel; +} + +//! Determine 'constrained factor' of a term +/** + * Actually this is (#vars/structure). + * Thus, 0 means very constrained, no variables. + * Everything else has higher float, but always <=1. In fact, only a single variable has a level 1. + */ +float +term_constrain_level (const Term term) +{ + int vars; + int structure; + int flag; + + int leaf (const Term t) + { + structure++; + if (realTermVariable (t)) + vars++; + return 1; + } + int nodel (const Term t) + { + structure++; + return 1; + } + + if (term == NULL) + error ("Cannot determine constrain level of empty term."); + + vars = 0; + structure = 0; + flag = term_iterate_deVar (term, leaf, nodel, NULL, NULL); + return ((float) vars / (float) structure); +} diff --git a/src/term.h b/src/term.h index fa0f03f..44cd29c 100644 --- a/src/term.h +++ b/src/term.h @@ -175,5 +175,7 @@ int term_iterate_deVar (const Term term, int (*leaf) (), int (*nodel) (), int term_iterate_leaves (const Term t, int (*func) ()); 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); #endif diff --git a/src/warshall.c b/src/warshall.c index 6f189fc..75caed1 100644 --- a/src/warshall.c +++ b/src/warshall.c @@ -1,8 +1,10 @@ /** - * Temp file. I just forgot Warshall... - * + * Warshall's algorithm for transitive closure computation. */ +#include "warshall.h" +#include "debug.h" + void graph_fill (int *graph, int nodes, int value) { @@ -17,7 +19,8 @@ graph_fill (int *graph, int nodes, int value) } //! Show a graph -void graph_display (int *graph, int nodes) +void +graph_display (int *graph, int nodes) { int i; @@ -31,9 +34,9 @@ void graph_display (int *graph, int nodes) { int j; j = 0; - while (j 0) { // Oh no! A cycle. - graph [index (k,i)] = 2; - graph_display (graph, nodes); + graph[index (k, i)] = 2; +#ifdef DEBUG + if (DEBUGL (5)) + { + graph_display (graph, nodes); + } +#endif return 0; } graph[index (k, i)] = 1;