diff --git a/src/cost.c b/src/cost.c index 605c0f5..e2cf111 100644 --- a/src/cost.c +++ b/src/cost.c @@ -7,67 +7,12 @@ * */ #include "switches.h" +#include "system.h" //************************************************************************ // Private methods //************************************************************************ -//! determine whether a run is a so-called self-initiator -int -selfInitiator (const System sys, const int run) -{ - int self_initiator; - - self_initiator = false; - if (sys->runs[run].role->initiator) - { - // An initiator - Termlist agents; - Termlist seen; - - agents = sys->runs[run].rho; - seen = NULL; - while (agents != NULL) - { - Term agent; - - agent = agents->term; - if (inTermlist (seen, agent)) - { - // This agent was already in the seen list - self_initiator = true; - } - else - { - seen = termlistAdd (seen, agent); - } - agents = agents->next; - } - termlistDelete (seen); - } - return self_initiator; -} - -//! Count the number of any self-initiators -int -selfInitiators (const System sys) -{ - int count; - int run; - - count = 0; - run = 0; - while (run < sys->maxruns) - { - if (selfInitiator (sys, run)) - { - count++; - } - run++; - } - return count; -} - //************************************************************************ // Public methods //************************************************************************ diff --git a/src/prune_theorems.c b/src/prune_theorems.c index e1833f2..df60af8 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -210,32 +210,13 @@ prune_theorems (const System sys) */ if (switches.extravert) { - int run; - - for (run = 0; run < sys->maxruns; run++) + if (selfInitiators (sys) > 0) { - // Check this run only if it is an initiator role - if (sys->runs[run].role->initiator) - { - // Check this initiator run - Termlist tl; - Termlist found; - - found = NULL; - for (tl = sys->runs[run].rho; tl != NULL; tl = tl->next) - { - if (inTermlist (found, tl->term)) - { - // XXX TODO - // Still need to fix proof output for this - // - // Pruning because some agents are equal for this role. - return true; - } - found = termlistAdd (found, tl->term); - } - termlistDelete (found); - } + // XXX TODO + // Still need to fix proof output for this + // + // Pruning because some agents are equal for this role. + return true; } } diff --git a/src/system.c b/src/system.c index b652c86..972e839 100644 --- a/src/system.c +++ b/src/system.c @@ -1398,3 +1398,62 @@ eventRoledef (const System sys, const int run, const int ev) { return roledef_shift (sys->runs[run].start, ev); } + +//! determine whether a run is a so-called self-initiator +/** + * Alice starting a run with Bob, Charlie, Bob is also counted as self-initiation. + */ +int +selfInitiator (const System sys, const int run) +{ + int self_initiator; + + self_initiator = false; + if (sys->runs[run].role->initiator) + { + // An initiator + Termlist agents; + Termlist seen; + + agents = sys->runs[run].rho; + seen = NULL; + while (agents != NULL) + { + Term agent; + + agent = agents->term; + if (inTermlist (seen, agent)) + { + // This agent was already in the seen list + self_initiator = true; + } + else + { + seen = termlistAdd (seen, agent); + } + agents = agents->next; + } + termlistDelete (seen); + } + return self_initiator; +} + +//! Count the number of any self-initiators +int +selfInitiators (const System sys) +{ + int count; + int run; + + count = 0; + run = 0; + while (run < sys->maxruns) + { + if (selfInitiator (sys, run)) + { + count++; + } + run++; + } + return count; +} diff --git a/src/system.h b/src/system.h index ef13334..520087d 100644 --- a/src/system.h +++ b/src/system.h @@ -201,6 +201,8 @@ int iterateLocalToOther (const System sys, const int myrun, int (*callback) (Term t)); int firstOccurrence (const System sys, const int r, Term t, int evtype); Roledef eventRoledef (const System sys, const int run, const int ev); +int selfInitiator (const System sys, const int run); +int selfInitiators (const System sys); //! Equality for run structure naming