- Static run symmetry detection seems to work just fine.

- Added 'warning' call to error.h
This commit is contained in:
ccremers 2004-07-14 07:31:01 +00:00
parent 508d49efbb
commit a5efc6106a
4 changed files with 100 additions and 0 deletions

View File

@ -54,3 +54,19 @@ error (char *fmt, ... )
va_end (args); va_end (args);
error_die (); error_die ();
} }
//! Print warning
/**
* Input is comparable to printf, only end of line is not required.
*/
void
warning (char *fmt, ... )
{
va_list args;
va_start (args, fmt);
fprintf (stderr, "warning: ");
vfprintf (stderr, fmt, args);
fprintf (stderr, "\n");
va_end (args);
}

View File

@ -5,5 +5,6 @@ void error_die (void);
void error_pre (void); void error_pre (void);
void error_post (char *fmt, ... ); void error_post (char *fmt, ... );
void error (char *fmt, ... ); void error (char *fmt, ... );
void warning (char *fmt, ... );
#endif #endif

View File

@ -253,6 +253,7 @@ ensureValidRun (System sys, int run)
myrun.index = NULL; myrun.index = NULL;
myrun.start = NULL; myrun.start = NULL;
myrun.know = knowledgeDuplicate (sys->know); myrun.know = knowledgeDuplicate (sys->know);
myrun.prevSymmRun = -1;
} }
} }
@ -441,6 +442,85 @@ roledefDestroy (Roledef rd)
return; return;
} }
/**
* A new run is created; now we want to know if it depends on any previous run.
* This occurs when there is a smaller runid with an identical protocol role, with the
* same agent pattern. However, there must be at least a variable in the pattern or no
* symmetry gains are to be made.
*
* Return -1 if there is no such symmetry.
*/
int staticRunSymmetry (const System sys,const int rid)
{
int ridSymm; // previous symmetrical run
Termlist agents; // list of agents for rid
Run runs; // shortcut usage
ridSymm = -1;
runs = sys->runs;
agents = runs[rid].agents;
while (agents != NULL)
{
if (isTermVariable(agents->term))
ridSymm = rid - 1;
agents = agents->next;
}
/* there is no variable in this roledef, abort */
if (ridSymm == -1)
return -1;
agents = runs[rid].agents;
while (ridSymm >= 0)
{
/* compare protocol name, role name */
if (runs[ridSymm].protocol == runs[rid].protocol &&
runs[ridSymm].role == runs[rid].role)
{
/* same stuff */
int isEqual;
Termlist al, alSymm; // agent lists
isEqual = 1;
al = agents;
alSymm = runs[ridSymm].agents;
while (isEqual && al != NULL)
{
/* determine equality */
if (isTermVariable (al->term))
{
/* case 1: variable, should match type */
if (isTermVariable (alSymm->term))
{
if (!isTermlistEqual (al->term->stype, alSymm->term->stype))
isEqual = 0;
}
else
{
isEqual = 0;
}
}
else
{
/* case 2: constant, should match */
if (!isTermEqual (al->term, alSymm->term))
isEqual = 0;
}
alSymm = alSymm->next;
al = al->next;
}
if (al == NULL && isEqual)
{
/* this candidate is allright */
warning ("Symmetry detection. #%i can depend on #%i.",rid,ridSymm);
return ridSymm;
}
}
ridSymm--;
}
return -1; // signal that no symmetrical run was found
}
//! Instantiate a role by making a new run. //! Instantiate a role by making a new run.
/** /**
* This involves creation of a new run(id). * This involves creation of a new run(id).
@ -565,6 +645,8 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
} }
termlistDelete (fromlist); termlistDelete (fromlist);
runs[rid].locals = tolist; runs[rid].locals = tolist;
runs[rid].prevSymmRun = staticRunSymmetry (sys, rid); // symmetry reduction static analysis
} }
//! Make a new role event with the specified parameters. //! Make a new role event with the specified parameters.

View File

@ -133,6 +133,7 @@ struct run
Roledef start; //!< Head of the run definition. Roledef start; //!< Head of the run definition.
Knowledge know; //!< Current knowledge of the run. Knowledge know; //!< Current knowledge of the run.
Termlist locals; //!< Locals of the run. Termlist locals; //!< Locals of the run.
int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
}; };
//! Shorthand for run pointer. //! Shorthand for run pointer.