andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Huge documentation effort.

Browse Source
This commit is contained in:
ccremers 2004-05-15 12:33:01 +00:00
parent 89e83b1661
commit e26d97bf2b
9 changed files with 394 additions and 194 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
README
View File

@ -31,3 +31,7 @@ If you want LaTeX output we need
- The MSC macro package msc.sty
- preamble.tex and postamble.tex
For the documentation generation, optionally with graphs.
- Doxygen: http://www.doxygen.org/
- Dot: http://www.research.att.com/sw/tools/graphviz/

2
src/doxyconfig
View File

@ -997,7 +997,7 @@ HIDE_UNDOC_RELATIONS = YES
# toolkit from AT&T and Lucent Bell Labs. The other options in this section
# have no effect if this option is set to NO (the default)
HAVE_DOT = NO
HAVE_DOT = YES
# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen
# will generate a graph for each documented class showing the direct and

14
src/knowledge.h
View File

@ -4,18 +4,31 @@
#include "terms.h"
#include "termlists.h"
//! Knowledge structure.
/**
* Contains a miminal representation of a knowledge set.
*/
struct knowledge
{
//! A list of non-encrypted terms.
Termlist basic;
//! A list of terms encrypted, such that the inverse is not in the knowledge set.
Termlist encrypt;
Termlist inverses;
union
{
//! List of open variables in the knowledge set.
/**
* This list is used to determine whether the knowledge needs to be rewritten.
* If a new substitution is done, one of the elements of this list will become closed,
* and we need to reconstruct the knowledge set.
*/
Termlist vars; // special: denotes unsubstituted variables
struct knowledge *next; // use for alternative memory management.
};
};
//! Shorthand for knowledge pointer.
typedef struct knowledge *Knowledge;
void knowledgeInit (void);
@ -41,6 +54,7 @@ Knowledge knowledgeSubstDo (const Knowledge know);
void knowledgeSubstUndo (const Knowledge know);
Termlist knowledgeNew (const Knowledge oldk, const Knowledge newk);
//! Harnass macro for recursive procedures.
#define mindwipe(k,recurse) \
if (k != NULL && k->vars != NULL) { \
Termlist tl = k->vars; \

9
src/runs.c
View File

@ -1,3 +1,7 @@
/**
* @file runs.c Originally contained only procedures related to runs, but has grown
* somewhat over time.
*/
#include <stdlib.h>
#include <stdio.h>
#include <limits.h>
@ -14,7 +18,10 @@
/* from compiler.o */
extern Term TERM_Type;
/* for e.g. termprinting */
//! Global flag that signals LaTeX output.
/**
* True iff LaTeX output is desired.
*/
int globalLatex;
static int indentState = 0;

117
src/runs.h
View File

@ -13,125 +13,192 @@
#define runPointerGet(sys,run) sys->runs[run].index
#define runPointerSet(sys,run,newp) sys->runs[run].index = newp
//! Structure for a role event node or list.
/**
*\sa role
*/
struct roledef
{
/* flag for internal actions (overriding normal type) */
//! flag for internal actions.
/**
* Typically, this is true to signify internal reads (e.g. variable choices)
* as opposed to a normal read.
*/
int internal;
//! Type of event.
/**
*\sa READ, SEND, CLAIM
*/
int type;
//! Event label.
Term label;
//! Event sender.
Term from;
//! Event target.
Term to;
//! Event message.
Term message;
//! Pointer to next roledef node.
struct roledef *next;
/* illegal injections */
//! Illegal injections for this event.
Knowledge forbidden;
/* knowledge transitions counter */
//! knowledge transitions counter.
int knowPhase;
/* evt runid for synchronisation, but that is implied in the
base array */
};
//! Shorthand for roledef pointer.
typedef struct roledef *Roledef;
//! Role definition.
/**
*\sa roledef
*/
struct role
{
//! Name of the role encoded in a term.
Term nameterm;
//! List of role events.
Roledef roledef;
//! Local constants for this role.
Termlist locals;
//! Pointer to next role definition.
struct role *next;
};
//! Shorthand for role pointer.
typedef struct role *Role;
//! Protocol definition.
struct protocol
{
//! Name of the protocol encoded in a term.
Term nameterm;
//! List of role definitions.
Role roles;
//! List of role names.
Termlist rolenames;
//! List of local terms for this protocol.
Termlist locals;
//! Pointer to next protocol.
struct protocol *next;
};
//! Shorthand for protocol pointer.
typedef struct protocol *Protocol;
//! Run container.
struct run
{
//! Protocol of this run.
Protocol protocol;
//! Role of this run.
Role role;
//! Agents involved in this run.
Termlist agents;
//! Current execution point in the run.
Roledef index;
//! Head of the run definition.
Roledef start;
//! Current knowledge of the run.
Knowledge know;
//! Locals of the run.
Termlist locals;
};
//! Shorthand for run pointer.
typedef struct run *Run;
//! Buffer for variables substitution state.
struct varbuf
{
//! List of closed variables.
Termlist from;
//! List of terms to which the closed variables are bound.
Termlist to;
//! List of open variables.
Termlist empty;
};
//! Shorthand for varbuf pointer.
typedef struct varbuf *Varbuf;
//! Trace buffer.
struct tracebuf
{
//! Length of trace.
int length;
//! Length of trace minus the redundant events.
int reallength;
//! Array of events.
Roledef *event;
//! Array of run identifiers for each event.
int *run;
//! Array of status flags for each event.
/**
*\sa S_OKE, S_RED, S_TOD, S_UNK
*/
int *status;
//! Array for matching sends to reads.
int *link;
int violatedclaim; // index of violated claim in trace
//! Index of violated claim in trace.
int violatedclaim;
//! Array of knowledge sets for each event.
Knowledge *know;
//! List of terms required to be in the final knowledge.
Termlist requiredterms;
//! List of variables in the system.
Varbuf variables;
};
//! The main state structure.
struct system
{
int step; // can be managed globally
Knowledge know;
int step; //!< Step in trace during exploration. Can be managed globally
Knowledge know; //!< Knowledge in currect step of system.
struct parameters *parameters; // misc
/* static run info, maxruns */
Run runs;
/* global */
int maxruns;
int maxruns; //!< Number of runs in the system.
/* properties */
Termlist secrets; // integrate secrets list into system
int shortestattack; // length of shortest attack trace
Termlist secrets; //!< Integrate secrets list into system.
int shortestattack; //!< Length of shortest attack trace.
/* switches */
int report;
int prune; // type of pruning
int switch_maxtracelength; // helps to remember the length of the last trace
int maxtracelength; // helps to remember the length of the last trace
int switchM; // memory
int switchT; // time
int switchS; // progress (traversed states)
int porparam; // a multi-purpose integer parameter, passed to the partial order reduction method selected
int latex; // latex output switch
int prune; //!< Type of pruning.
int switch_maxtracelength; //!< Helps to remember the length of the last trace.
int maxtracelength; //!< helps to remember the length of the last trace.
int switchM; //!< Memory display switch.
int switchT; //!< Time display switch.
int switchS; //!< Progress display switch. (traversed states)
int porparam; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
//! Latex output switch.
/**
* Obsolete. Use globalLatex instead.
*\sa globalLatex
*/
int latex;
/* traversal */
int traverse; // traversal method
int explore; // boolean: explore states after actions or not
int traverse; //!< Traversal method.
int explore; //!< Boolean: explore states after actions or not.
/* counters */
unsigned long int statesLow;
unsigned long int statesHigh;
unsigned long int claims; // number of claims encountered
unsigned long int failed; // number of claims failed
unsigned long int claims; //!< Number of claims encountered.
unsigned long int failed; //!< Number of claims failed.
/* matching */
int match; // matching type
int clp; // do we use clp?
int match; //!< Matching type.
int clp; //!< Do we use clp?
/* protocol definition */
Protocol protocols;
@ -150,7 +217,7 @@ struct system
int knowPhase; // which knowPhase have we already explored?
Constraintlist constraints; // only needed for CLP match
/* relevant: storage of shortest attack */
//! Shortest attack storage.
struct tracebuf* attack;
};

238
src/termlists.c
View File

@ -11,34 +11,36 @@
extern Term TERM_Function;
extern Term TERM_Hidden;
//! Open termlists code.
void
termlistsInit (void)
{
return;
}
//! Close termlists code.
void
termlistsDone (void)
{
return;
}
/* inline candidate */
//! Allocate memory for a termlist node.
/**
*@return A pointer to uninitialised memory of the size of a termlist node.
*/
Termlist
makeTermlist ()
{
/* inline candidate */
return (Termlist) memAlloc (sizeof (struct termlist));
}
/*
termlistDuplicate
A deep copy.
//! Duplicate a termlist.
/**
* Uses termDuplicate to copy the elements, and allocated new memory for the list nodes.
*\sa termDuplicate(), termlistShallow()
*/
Termlist
termlistDuplicate (Termlist tl)
{
@ -55,15 +57,12 @@ termlistDuplicate (Termlist tl)
return newtl;
}
/*
termlistShallow
A shallow copy, because I gather we won't be modifying any terms, only
termlists. Oh, and it reverses the order :) Don't forget!
//! Shallow reverse copy of a termlist.
/**
* Just copies the element pointers. Allocates new memory for the list nodes.
* Note that it reverses the order of the list.
*\sa termlistDuplicate()
*/
Termlist
termlistShallow (Termlist tl)
{
@ -78,14 +77,11 @@ termlistShallow (Termlist tl)
return newtl;
}
/*
termlistDelete
(shallow)
//! Shallow deletion of a termlist.
/**
* Deletes the termlist nodes only. Elements are intact after exit.
*\sa termlistShallow()
*/
void
termlistDelete (Termlist tl)
{
@ -96,14 +92,11 @@ termlistDelete (Termlist tl)
}
/*
termlistDestroy
(deep)
//! Deep deletion of a termlist.
/**
* Deletes the termlist nodes as well as the elements.
*\sa termlistDuplicate(), termDuplicate(), termDelete()
*/
void
termlistDestroy (Termlist tl)
{
@ -114,14 +107,10 @@ termlistDestroy (Termlist tl)
memFree (tl, sizeof (struct termlist));
}
/*
inTermlist
check whether a term occurs in a termlist
//! Determine whether a term is an element of a termlist.
/**
*@return True iff the term is an element of the termlist.
*/
int
inTermlist (Termlist tl, Term term)
{
@ -141,8 +130,11 @@ inTermlist (Termlist tl, Term term)
}
}
/* are all elements of list 1 in list 2, and vice versa?
Note that we assume unique elements !
//! Equality of two term lists.
/**
* Are all elements of list 1 in list 2, and vice versa?
* Note that we assume unique elements!
*@param True iff every element of the list is in the other list.
*/
int
@ -159,15 +151,12 @@ isTermlistEqual (Termlist tl1, Termlist tl2)
return 1;
}
/*
termlistAdd
Adds a term. Duplicates are allowed.
A new list pointer is returned.
//! Adds a term to the front of a termlist.
/**
* Duplicates are allowed.
*@return A new list pointer.
*\sa termlistAppend()
*/
Termlist
termlistAdd (Termlist tl, Term term)
{
@ -191,15 +180,12 @@ termlistAdd (Termlist tl, Term term)
return newtl;
}
/*
termlistAppend
Appends a term to the end of the list. Duplicates are allowed.
A new list pointer is returned.
//! Adds a term to the end of a termlist.
/**
* Duplicates are allowed.
*@return A new list pointer if the termlist was NULL.
*\sa termlistAdd()
*/
Termlist
termlistAppend (const Termlist tl, const Term term)
{
@ -226,6 +212,11 @@ termlistAppend (const Termlist tl, const Term term)
return tl;
}
//! Concatenates two termlists.
/**
* The last pointer of the first list is made to point to the second list.
*@return The pointer to the concatenated list.
*/
Termlist
termlistConcat (Termlist tl1, Termlist tl2)
{
@ -241,13 +232,11 @@ termlistConcat (Termlist tl1, Termlist tl2)
return tl1;
}
/*
termlistDelTerm
remove the current element from the termlist. Easier because of the
double linked list.
//! Remove the pointed at element from the termlist.
/**
* Easier because of the double linked list.
*@param tl The pointer to the termlist node to be deleted from the list.
*@return The possibly new head pointer to the termlist.
*/
Termlist
termlistDelTerm (Termlist tl)
@ -273,6 +262,10 @@ termlistDelTerm (Termlist tl)
return newhead;
}
//! Construct the conjunction of two termlists.
/**
*@return A new termlist containing the elements in both lists.
*/
Termlist
termlistConjunct (Termlist tl1, Termlist tl2)
{
@ -290,6 +283,10 @@ termlistConjunct (Termlist tl1, Termlist tl2)
return newtl;
}
//! Construct the conjunction of two termlists, and a certain type.
/**
*@return A new termlist containing the elements in both lists, that are also of the desired type.
*/
Termlist
termlistConjunctType (Termlist tl1, Termlist tl2, int termtype)
{
@ -307,6 +304,10 @@ termlistConjunctType (Termlist tl1, Termlist tl2, int termtype)
return newtl;
}
//! Construct the conjunction of a termlist and a certain type.
/**
*@return A new termlist containing the elements in the list that are of the desired type.
*/
Termlist
termlistType (Termlist tl, int termtype)
{
@ -324,6 +325,10 @@ termlistType (Termlist tl, int termtype)
return newtl;
}
//! Display a termlist.
/**
* Lists of terms are displayed between square brackets, and seperated by commas.
*/
void
termlistPrint (Termlist tl)
{
@ -343,6 +348,13 @@ termlistPrint (Termlist tl)
printf ("]");
}
//! Append all open variables in a term to a list.
/**
*@param tl The list to which to append to.
*@param t The term possibly containing open variables.
*@return The pointer to the extended list.
*\sa termlistAddRealVariables()
*/
Termlist
termlistAddVariables (Termlist tl, Term t)
{
@ -368,6 +380,13 @@ termlistAddVariables (Termlist tl, Term t)
}
}
//! Append all variables in a term to a list.
/**
*@param tl The list to which to append to.
*@param t The term possibly containing open and closed variables.
*@return The pointer to the extended list.
*\sa termlistAddVariables()
*/
Termlist
termlistAddRealVariables (Termlist tl, Term t)
{
@ -403,6 +422,13 @@ termlistAddRealVariables (Termlist tl, Term t)
}
}
//! Append all basic terms in a term to a list.
/**
*@param tl The list to which to append to.
*@param t The term containing basic terms.
*@return The pointer to the extended list.
*\sa termlistAddBasics()
*/
Termlist
termlistAddBasic (Termlist tl, Term t)
{
@ -426,6 +452,13 @@ termlistAddBasic (Termlist tl, Term t)
return tl;
}
//! Append all basic terms in a termlist to another list.
/**
*@param tl The list to which to append to.
*@param scan The termlist with terms containing basic terms.
*@return The pointer to the extended list.
*\sa termlistAddBasic()
*/
Termlist
termlistAddBasics (Termlist tl, Termlist scan)
{
@ -437,13 +470,11 @@ termlistAddBasics (Termlist tl, Termlist scan)
return tl;
}
/*
* termlistMinusTerm
*
* Remove a term from a termlist, and yield a new termlist pointer.
* Semantics: remove the first occurrence of the term.
//! Remove a term from a termlist.
/**
* Removes the first occurrence of the term.
*@return A new termlist pointer.
*/
Termlist
termlistMinusTerm (Termlist tl, Term t)
{
@ -460,6 +491,7 @@ termlistMinusTerm (Termlist tl, Term t)
return tl;
}
//! Determine the length of a termlist.
int
termlistLength (Termlist tl)
{
@ -473,13 +505,14 @@ termlistLength (Termlist tl)
return i;
}
/*
inverseKey
Gives the inverse Key of some term (which is used to encrypt something), as is defined
by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
//! Give the inverse key term of a term.
/**
* Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
* by the termlist, which is a list of key1,key1inv, key2, key2inv, etc...
*@param inverses The list of inverses, typically from the knowledge.
*@param key Any term of which the inverse will be determined.
*@return A pointer to a duplicate of the inverse key term.
*\sa termDuplicate(), knowledge::inverses
*/
@ -535,14 +568,12 @@ inverseKey (Termlist inverses, Term key)
return termDuplicate (key); /* defaults to symmetrical */
}
//! Create a term local to a run.
/*
* localTerm
*
* Creates a term local to a run.
* We assume that at this point, no variables have been instantiated yet that occur in this term.
* We also assume that fromlist, tolist and locals only hold real leaves.
*\sa termlistLocal()
*/
Term
termLocal (const Term t, Termlist fromlist, Termlist tolist,
const Termlist locals, const int runid)
@ -585,12 +616,11 @@ termLocal (const Term t, Termlist fromlist, Termlist tolist,
}
}
/*
* termlistLocal
*
* We expand the previous concept to termlists.
//! Create a list of instance terms.
/**
* We expand the termlocal concept to termlists.
*\sa termLocal()
*/
Termlist
termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist,
const Termlist locals, int runid)
@ -607,10 +637,12 @@ termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist,
return newtl;
}
/*
* Check whether tl2 is contained in tl1.
//! Check whether a termlist is contained in another.
/**
*@param tlbig The big list.
*@param tlsmall The list that is possibly contained in the big one.
*@return True iff tlsmall is contained in tlbig.
*/
int
termlistContained (const Termlist tlbig, Termlist tlsmall)
{
@ -623,9 +655,14 @@ termlistContained (const Termlist tlbig, Termlist tlsmall)
return 1;
}
/*
//! Check substitution validity
/**
* Determine whether a variable has been substituted with something with
* the right type.
*@param matchmode The system matching mode, typically system::match
*@param term The closed variable term.
*@return True iff the substitution is valid in the current mode.
*\sa system::match
*/
int
@ -653,15 +690,15 @@ validSubst (const int matchmode, const Term term)
}
}
/*
* termFunction
*
* An assist function that helps to simulate Term->Term functions, using
* termlists. One termlist functions as the domain, and the other as the
* range.
*
* Extending a function with a value y = f(x) amounts to extending the
* domain with x, and the range with y.
//! Yield the result of f(x)
/**
* This function interpretes two termlists as the domain and range of a function,
* and if the term occurs in the domain, returns the matching value from the range.
* Note that these functions cannot have NULL in the domain or the range.
*@param fromlist The domain list.
*@param tolist The range list, in a one-to-one correspondence with the fromlist.
*@param tx The point on which the function is to be evaluated.
*@return The result of the function application or NULL if the point is not within the domain.
*/
Term
@ -679,10 +716,7 @@ termFunction (Termlist fromlist, Termlist tolist, Term tx)
return NULL;
}
/*
* Forward the termlist pointer to the last item
*/
//! Yield the last node of a termlist.
Termlist
termlistForward (Termlist tl)
{

9
src/termlists.h
View File

@ -3,13 +3,22 @@
#include "terms.h"
//! The list container for the term type.
/**
* Implemented as a double linked list to allow for element deletion.
*\sa term
*/
struct termlist
{
//! The term element for this node.
Term term;
//! Next node pointer or NULL for the tail of the list.
struct termlist *next;
//! Previous node pointer or NULL for the head of the list.
struct termlist *prev;
};
//! Shorthand for termlist pointers.
typedef struct termlist *Termlist;
void termlistsInit (void);

147
src/terms.c
View File

@ -25,24 +25,34 @@ void indent (void);
/* Two types of terms: general, and normalized. Normalized rewrites all
tuples to (x,(y,z))..NULL form, making list traversal easy. */
//! Initialization of terms code.
void
termsInit (void)
{
return;
}
//! Cleanup of terms code.
void
termsDone (void)
{
return;
}
//! Allocate memory for a term.
/**
*@return A pointer to the new term memory, which is not yet initialised.
*/
Term
makeTerm ()
{
return (Term) memAlloc (sizeof (struct term));
}
//! Create a fresh encrypted term from two existing terms.
/**
*@return A pointer to the new term.
*/
Term
makeTermEncrypt (Term t1, Term t2)
{
@ -54,6 +64,10 @@ makeTermEncrypt (Term t1, Term t2)
return term;
}
//! Create a fresh term tuple from two existing terms.
/**
*@return A pointer to the new term.
*/
Term
makeTermTuple (Term t1, Term t2)
{
@ -82,6 +96,11 @@ makeTermTuple (Term t1, Term t2)
return tt;
}
//! Make a term of the given type with run identifier and symbol.
/**
*@return A pointer to the new term.
*\sa GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE
*/
Term
makeTermType (const int type, const Symbol symb, const int runid)
{
@ -94,12 +113,13 @@ makeTermType (const int type, const Symbol symb, const int runid)
return term;
}
/* deVar unwraps any substitutions.
*
* For speed, it is a macro. Sometimes it will call
//! Unwrap any substitutions.
/**
* For speed, it is also a macro. Sometimes it will call
* deVarScan to do the actual unwinding.
*@return A term that is either not a variable, or has a NULL substitution.
*\sa deVar()
*/
Term
deVarScan (Term t)
{
@ -108,6 +128,10 @@ deVarScan (Term t)
return t;
}
//! Determine whether a term contains an unsubstituted variable as subterm.
/**
*@return True iff there is an open variable as subterm.
*/
int
hasTermVariable (Term term)
{
@ -125,17 +149,15 @@ hasTermVariable (Term term)
}
}
/*
isTermEqualFn(term,term)
Tests whether two terms are completely identical. This also includes
variables. This is the recursive function.
We assume the term is normalized, e.g. no tupling has direct
subtupling.
Out: 0 unequal, 1 equal
//!Tests whether two terms are completely identical.
/**
* This also includes
* variables. This is the recursive function.
* We assume the term is normalized, e.g. no tupling has direct
* subtupling.
*@return True iff the terms are equal.
*\sa isTermEqual()
*/
int
@ -179,6 +201,12 @@ isTermEqualFn (Term term1, Term term2)
}
}
//! See if a term is a subterm of another.
/**
*@param t Term to be checked for a subterm.
*@param tsub Subterm.
*@return True iff tsub is a subterm of t.
*/
int
termOccurs (Term t, Term tsub)
{
@ -195,7 +223,7 @@ termOccurs (Term t, Term tsub)
return (termOccurs (t->op, tsub) || termOccurs (t->key, tsub));
}
//! Print a term to stdout.
void
termPrint (Term term)
{
@ -282,12 +310,11 @@ termPrint (Term term)
}
/*
Duplicate
make a deep copy of a term, but not of leaves.
//! Make a deep copy of a term.
/**
* Leaves are not copied.
*@return If the original was a leaf, then the pointer is simply returned. Otherwise, new memory is allocated and the node is copied recursively.
*\sa termDuplicateDeep()
*/
Term
@ -315,14 +342,14 @@ termDuplicate (const Term term)
return newterm;
}
/*
DuplicateDeep
make a deep copy of a term, and also of leaves.
//! Make a true deep copy of a term.
/**
* Currently, it this function is not to be used, so we can be sure leaf nodes occur only once in the system.
*@return New memory is allocated and the node is copied recursively.
*\sa termDuplicate()
*/
Term
termDuplicateDeep (const Term term)
{
@ -353,10 +380,10 @@ termDuplicateDeep (const Term term)
return newterm;
}
/*
* DuplicateUV
*
//! Make a copy of a term, but remove substituted variable nodes.
/**
* Remove all instantiated variables on the way down.
*\sa termDuplicate()
*/
Term
@ -423,12 +450,11 @@ realTermDuplicate (const Term term)
return newterm;
}
/*
termDelete
Removes a term and deallocates memory
//!Removes a term and deallocates memory.
/**
* Is meant to remove terms make with termDuplicate. Only deallocates memory
* of nodes, not of leaves.
*\sa termDuplicate(), termDuplicateUV()
*/
void
@ -450,13 +476,13 @@ termDelete (const Term term)
}
}
/*
termNormalize
avoids problems with associativity by rewriting every ((x,y),z) to
(x,y,z)), i.e. a normal form for terms, after which equality is
okay.
*/
//! Normalize a term with respect to tupling.
/**
* Avoids problems with associativity by rewriting every ((x,y),z) to
* (x,(y,z)), i.e. a normal form for terms, after which equality is
* okay. No memory was allocated or deallocated, as only pointers are swapped.
*
*@return After execution, the term pointed at has been normalized. */
void
termNormalize (Term term)
@ -493,7 +519,12 @@ termNormalize (Term term)
}
}
//! Copy a term, and ensure all run identifiers are set to the new value.
/**
* Strange code. Only to be used on locals, as is stupidly replaces all run identifiers.
*@return The new term.
*\sa termDuplicate()
*/
Term
termRunid (Term term, int runid)
{
@ -527,8 +558,10 @@ termRunid (Term term, int runid)
}
}
/* tupleCount yields the size of the top tuple in the term */
//! Determine tuple width of a given term.
/**
*\sa tupleProject()
*/
int
tupleCount (Term tt)
{
@ -550,9 +583,13 @@ tupleCount (Term tt)
}
}
/* tupleProject yields the projection pi (0 .. n-1) on a top tuple. Returns
* NULL if the range is incorrect. */
//! Yield the projection Pi(n) of a term.
/**
*@param tt Term
*@param n The index in the tuple.
*@return Returns either a pointer to a term, or NULL if the index is out of range.
*\sa tupleCount()
*/
Term
tupleProject (Term tt, int n)
{
@ -591,9 +628,12 @@ tupleProject (Term tt, int n)
}
}
/* number of elements in a term.
*
//! Determine size of term.
/**
* Determines the size of a term according to some heuristic.
* Currently, the encryption operator is weighed as well.
*@return Returns a nonnegative integer.
*\sa termDistance()
*/
int
@ -622,7 +662,10 @@ termSize(Term t)
}
}
/* Yield some sort of distance between two terms, as a float between 0 and 1.
//! Determine distance between two terms.
/**
*@return A float value between 0, completely dissimilar, and 1, equal.
*\sa termSize()
*/
float

24
src/terms.h
View File

@ -9,31 +9,53 @@
#define ENCRYPT 4
#define TUPLE 5
//! The most basic datatype in the modelchecker.
/**
* Describes a single term.
*/
struct term
{
/* basic : name,runid
encrypt: op,key
tuple : op,next
*/
//! The type of term.
/**
* \sa GLOBAL, VARIABLE, LEAF, ENCRYPT, TUPLE
*/
int type;
void *stype; // only for leaf, termlist pointer
//! Data Type termlist (e.g. agent or nonce)
/** Only for leaves. */
void *stype;
//! Substitution term.
/**
* If this is non-NULL, this leaf term is apparently substituted by
* this term.
*/
struct term *subst; // only for variable/leaf, substitution term
union
{
Symbol symb;
//! Encrypted subterm.
struct term *op;
//! Left-hand side of tuple pair.
struct term *op1;
struct term *next; // for alternative memory management
};
union
{
int runid;
//! Key used to encrypt subterm.
struct term *key;
//! Right-hand side of tuple pair.
struct term *op2;
};
};
//! Pointer shorthand.
typedef struct term *Term;
void termsInit (void);