- Initial knowledge displayed when running --check.
This commit is contained in:
parent
f00392ac3e
commit
4e085f0eb8
@ -867,7 +867,8 @@ roleCompile (Term nameterm, Tac tc)
|
|||||||
void
|
void
|
||||||
roleKnows (Tac tc)
|
roleKnows (Tac tc)
|
||||||
{
|
{
|
||||||
thisRole->knows = termlistConcat (thisRole->knows, tacTermlist (tc->t1.tac));
|
thisRole->knows =
|
||||||
|
termlistConcat (thisRole->knows, tacTermlist (tc->t1.tac));
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
@ -1812,17 +1813,21 @@ preprocess (const System sys)
|
|||||||
* compute hidelevels
|
* compute hidelevels
|
||||||
*/
|
*/
|
||||||
hidelevelCompute (sys);
|
hidelevelCompute (sys);
|
||||||
/*
|
|
||||||
* display initial role knowledge
|
|
||||||
*/
|
|
||||||
|
|
||||||
int showRK (Protocol p, Role r)
|
if (switches.check)
|
||||||
{
|
{
|
||||||
eprintf ("Role ");
|
/*
|
||||||
termPrint (r->nameterm);
|
* display initial role knowledge
|
||||||
eprintf (" knows ");
|
*/
|
||||||
termlistPrint (r->knows);
|
|
||||||
eprintf ("\n");
|
int showRK (Protocol p, Role r)
|
||||||
}
|
{
|
||||||
iterateRoles (sys,showRK);
|
eprintf ("Role ");
|
||||||
|
termPrint (r->nameterm);
|
||||||
|
eprintf (" knows ");
|
||||||
|
termlistPrint (r->knows);
|
||||||
|
eprintf ("\n");
|
||||||
|
}
|
||||||
|
iterateRoles (sys, showRK);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user