- Added pruning theorem for untrusted actors.
This commit is contained in:
parent
d43e3d432f
commit
4832e9116c
@ -1461,7 +1461,7 @@ prune_theorems ()
|
|||||||
Termlist tl;
|
Termlist tl;
|
||||||
List bl;
|
List bl;
|
||||||
|
|
||||||
// Check if all agents are valid
|
// Check if all agents of the main run are valid
|
||||||
tl = sys->runs[0].agents;
|
tl = sys->runs[0].agents;
|
||||||
while (tl != NULL)
|
while (tl != NULL)
|
||||||
{
|
{
|
||||||
@ -1499,6 +1499,26 @@ prune_theorems ()
|
|||||||
tl = tl->next;
|
tl = tl->next;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Check if the actors of all other runs are not untrusted
|
||||||
|
if (sys->untrusted != NULL)
|
||||||
|
{
|
||||||
|
int run;
|
||||||
|
|
||||||
|
run = 1;
|
||||||
|
while (run < sys->maxruns)
|
||||||
|
{
|
||||||
|
if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
|
||||||
|
{
|
||||||
|
if (sys->output == PROOF)
|
||||||
|
{
|
||||||
|
indentPrint ();
|
||||||
|
eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
run++;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// Check for c-minimality
|
// Check for c-minimality
|
||||||
if (!bindings_c_minimal ())
|
if (!bindings_c_minimal ())
|
||||||
{
|
{
|
||||||
|
Loading…
Reference in New Issue
Block a user