- Improved proof output.
This commit is contained in:
parent
8fa7c4e839
commit
f2bc78cc1f
@ -177,7 +177,7 @@ semiRunCreate (const Protocol p, const Role r)
|
|||||||
else
|
else
|
||||||
num_regular_runs++;
|
num_regular_runs++;
|
||||||
roleInstance (sys, p, r, NULL, NULL);
|
roleInstance (sys, p, r, NULL, NULL);
|
||||||
run = sys->maxruns-1;
|
run = sys->maxruns - 1;
|
||||||
sys->runs[run].length = 0;
|
sys->runs[run].length = 0;
|
||||||
return run;
|
return run;
|
||||||
}
|
}
|
||||||
@ -361,7 +361,7 @@ proof_select_goal (Binding b)
|
|||||||
indentPrint ();
|
indentPrint ();
|
||||||
eprintf ("Selected goal: Where does term ");
|
eprintf ("Selected goal: Where does term ");
|
||||||
termPrint (b->term);
|
termPrint (b->term);
|
||||||
eprintf (" originate first?\n");
|
eprintf (" occur first as an interm?\n");
|
||||||
indentPrint ();
|
indentPrint ();
|
||||||
eprintf ("* It is required for ");
|
eprintf ("* It is required for ");
|
||||||
roledefPrint (rd);
|
roledefPrint (rd);
|
||||||
@ -799,7 +799,7 @@ bind_goal_new_encrypt (const Binding b)
|
|||||||
int can_be_encrypted;
|
int can_be_encrypted;
|
||||||
|
|
||||||
flag = 1;
|
flag = 1;
|
||||||
term = deVar(b->term);
|
term = deVar (b->term);
|
||||||
can_be_encrypted = 0;
|
can_be_encrypted = 0;
|
||||||
|
|
||||||
if (!realTermLeaf (term))
|
if (!realTermLeaf (term))
|
||||||
@ -842,7 +842,7 @@ bind_goal_new_encrypt (const Binding b)
|
|||||||
eprintf ("\n");
|
eprintf ("\n");
|
||||||
}
|
}
|
||||||
newgoals = add_read_goals (run, 0, index + 1);
|
newgoals = add_read_goals (run, 0, index + 1);
|
||||||
|
|
||||||
indentDepth++;
|
indentDepth++;
|
||||||
if (goal_bind (b, run, index))
|
if (goal_bind (b, run, index))
|
||||||
{
|
{
|
||||||
|
Loading…
Reference in New Issue
Block a user