Main Page   Class Hierarchy   Compound List   File List   Compound Members   File Members  

/magnus/back_end/KB/include/KBmagPackage.h

Go to the documentation of this file.
00001 /*
00002   *   $Id: KBmagPackage.h,v 1.3 1996/08/15 18:55:48 bormotov Exp $
00003  */
00004 
00005 // Copyright (C) 1994 The New York Group Theory Cooperative
00006 // See magnus/doc/COPYRIGHT for the full notice.
00007 
00008 // Contents: Definition of KBmagPackage class.
00009 //
00010 // Principal Author: Sarah Rees
00011 //
00012 // Status: in progress
00013 //
00014 // Revision History:
00015 //
00016 // * 06/24/95 Roger moved the ctors to .C, and made the static
00017 //            const Chars cdbin
00018 //            into a class data member, to both work around a compiler
00019 //            bug, and to avoid problems with the order of static init.
00020 //
00021 // Next implementation steps:
00022 //
00023 // * Deal with the many @rn, @rn:@sr, @sr comments here and in KBmagPackage.C
00024 
00025 
00026 #ifndef _KBmagPackage_H_
00027 #define _KBmagPackage_H_
00028 
00029 #include <iomanip.h>
00030 
00031 #include "Vector.h"
00032 #include "Chars.h"
00033 #include "Set.h"
00034 #include "Word.h"
00035 #include "DFSA.h"
00036 #include "DiffMachine.h"
00037 #include "GenMult.h"
00038 #include "WordOrder.h"
00039 
00040 extern "C" {
00041   char* tempnam(const char*,const char *); 
00042          // Lib functions SunOS doesn't declare.
00043 }
00044 class KBmagPackage {
00045 public:
00046  
00047   // KBmagPackage is a wrapper for Derek Holt's implementation of the automatic
00048   // group procedures which attempt to prove a group automatic by constructing
00049   // and verifying a shortlex automatic structure.
00050   // Each of the relevant programs corresponds to a method in this class,
00051   // which carries the name of Holt's program.
00052   // Various automata are computed by these programs, and are stored in
00053   // temporary files, but may be accessed by methods in this class.
00054   //
00055   // The method autgroup() runs the whole procedure. It returns YES if the
00056   // procedure completes and proves the group automatic, NO if the procedure
00057   // completes but fails to prove the group automatic, DONTKNOW if the procedure  // is unable to complete (probably through lack of memory). For a group which
00058   // is not automatic, autgroup() could run forever, so it is unwise to call it.  // It is wiser to run its constituent parts individually.
00059   //
00060   // These are as follows:-
00061   //
00062   // The method kbprog() runs a Knuth-Bendix procedure for a finite amount
00063   // of time, and, given enough resources, must eventually terminate,
00064   // when certain parameter bounds are met.
00065   // When it terminates a difference machine is computed.
00066   // YES is returned on successful termination, DONTKNOW if the
00067   // program cannot terminate through lack of resources.
00068   //
00069   // Once a difference machine has been supplied, the method gpwa() computes
00070   // a word acceptor from it. The construction is a finite logical operation,
00071   // and, given enough resources, must terminate.
00072   // Once a difference machine and word acceptor have been supplied, the
00073   // method gpgenmult() computes a general multiplier from it. Given
00074   // enough resources, this mult also terminate.
00075   // For both gpwa() and gpgenmult(),
00076   // YES is returned on successful termination, DONTKNOW if the
00077   // program cannot terminate through lack of resources.
00078   //
00079   // gpcheckmult() performs preliminary checks on the word acceptor and
00080   // general multipliers, and returns NO if those checks fails, YES on
00081   // successful termination and DONTKNOW if the program cannot terminate through  
00082   // lack of resources. In the case of a NO answer, additional word
00083   // differences are found and the difference machine is accordingly modified.
00084   // A new word acceptor and new general multiplier may be computed from
00085   // the modified difference machine, using gpwa() and gpgenmult()
00086   // and the preliminary checks run again.
00087   // The loop may be run until a YES answer is obtained from gpcheckmult()
00088   //
00089   // gpaxioms() performs further checks on the word acceptor and general
00090   // multipliers, and returns YES if those check verify that the automata
00091   // form an automatic structure, NO if the checks fail and DONTKNOW
00092   // if the checks fail to complete due to lack of resources.
00093   //
00094   // The sensible way to test whether or not a group is automatic is thus
00095   // to run kbprog(), then the sequence gpwa(), gpgenmult(), gpcheckmult()
00096   // repeatedly until a YES answer is obtained from gpcheckmult(),
00097   // then finally gpaxioms(). autgroup() runs the full suite of
00098   // programs as above, and gpmakefsa() runs the loop gpwa(), gpcheckmult(),
00099   // gpcheckmult(), stopping only when a YES answer is obtained.
00100   // Hence both of autgroup() and gpmakefsa() should be used only with extreme
00101   // caution.
00102   //
00103   // The automata may be recovered from the package using the
00104   // methods wordAcceptor(), differenceMachine() and generalMultiplier().
00105   // These automata may also be set, in which case any previously calculated
00106   // by the package will be overwritten using the methods setWordAcceptor(),
00107   // setDifferenceMachine() and setGeneralMultiplier(). Thus for instance
00108   // the method gpwa() may be used to compute a word acceptor from any
00109   // difference machine, and gpgenmult() may be used to compute the general
00110   // multiplier based on any difference machine and word acceptor.
00111   // In fact the automatic groups procedure builds in general two difference
00112   // machines, the first of which accepts a sublanguage of the second.
00113   //
00114   // The integer argument of the methods differenceMachine and
00115   // setDifferenceMachine() differentiates between those two automata. At the
00116   // present the second is always used by the methods gpwa() and gpgenmult() -
00117   // the Holt programs may be run to use the first as a space-saving device,
00118   // but currently this option is not available within this class.
00119   //
00120  
00121   // The Package is initialised with the list of generators and relators
00122   // of the groups,
00123   // and (optionally)
00124   // an integer array with specifies the order of the generators
00125   // and their inverses used in the shortlex ordering.
00126   // and an integer tidyint, which is a parameter for the KnuthBendix procedure. 
00127 
00128 
00129 
00130 
00131   KBmagPackage(const VectorOf<Chars>& genNames, const SetOf<Word>& rels,
00132           const WordOrder & word_order,int tidyint) ; 
00133 
00134   KBmagPackage(const VectorOf<Chars>& genNames, const SetOf<Word>& rels,
00135           const WordOrder & word_order) ; 
00136 
00137   KBmagPackage(const VectorOf<Chars>& genNames, const SetOf<Word>& rels);
00138 
00139   ~KBmagPackage();
00140   // Takes care of shutting down the programs, and unlinking temp files/pipes.
00141   Bool sanityCheck() const { return !error; }
00142 
00143 // In each of the below, YES is returned if the program completes successfully
00144 // having verified all checks which need to be made, and DONTKNOW is returned
00145 // if for some reason the program cannot complete (usually because of lack of
00146 // memory). NO is returned if the program completes and some checks have failed.
00147 // In fact a NO answer is not possible from gpgenmult, gpmakefsa, gpwa or
00148 // kbprog.
00149   Trichotomy autgroup();
00150   Trichotomy gpaxioms();
00151   Trichotomy gpcheckmult();
00152   Trichotomy gpgenmult(Bool eqcheck=YES);
00153   Trichotomy gpmakefsa(Bool eqcheck=YES);
00154   Trichotomy gpwa();
00155   Trichotomy kbprog (int haltingfactor=100,int tidyint=20,int maxeqns=200,
00156          int maxstates=1000);
00157 
00158   Chars getName() const { Chars s = problemName; return s;}
00159 
00160   Bool isProvedAutomatic( ) const { return provedAutomatic; }
00161   Bool isProvedConfluent( ) const { return provedConfluent; }
00162 
00163 
00164   Chars getGeneratorName(Generator g) const {
00165      int i = ord(g);
00166      if (i>0) return generatorNames[i-1];
00167      else return(generatorNames[-i-1]+"^-1");
00168   }
00169 
00170   GroupDFSA wordAcceptor();
00171   GenMult generalMultiplier();
00172   DiffMachine differenceMachine(int i);
00173 
00174   void setWordAcceptor(const GroupDFSA & WA);
00175   void setGeneralMultiplier(const GenMult & GM);
00176   void setDifferenceMachine(const DiffMachine & Diff,int i);
00177 
00178 // and now versions of the above which use DFSARep's rather than DFSA's
00179 // Maybe these should be private.
00180 // They are necessary for use in code which needs to do serious manipulation
00181 // with the automata, e.g. hyperbolicity testing.
00182 
00183   GroupDFSARep wordAcceptorRep();
00184   GenMultRep generalMultiplierRep();
00185   DiffMachineRep differenceMachineRep(int i);
00186 
00187   void setWordAcceptor(const GroupDFSARep & WARep);
00188   void setGeneralMultiplier(const GenMultRep & GMRep);
00189   void setDifferenceMachine(const DiffMachineRep & DiffRep,int i);
00190   Bool minimize(DFSA & D);
00191   Bool minimize(GroupDFSA & D);
00192   Bool minimize(DFSARep & D);
00193   Bool minimize(GroupDFSARep & D);
00194   Bool gpcomp(GroupDFSA & D1,GroupDFSA & D2,GroupDFSA & D3);
00195   Bool gpcomp(GroupDFSARep & D1,GroupDFSARep & D2,GroupDFSARep & D3);
00196 
00197 private:
00198 
00199   int numOfSymbols;
00200   int tidyInterval;
00201 
00202   Chars problemName;     // Problem name supplied to KBmagPackage
00203 
00204   VectorOf<Chars> generatorNames;
00205   SetOf<Word> relators;
00206   WordOrder order;
00207   
00208   Bool error;
00209   Bool provedAutomatic;
00210   Bool provedConfluent;
00211 
00212   Chars cdbin;  //@rn Should be const, but then trouble initing.
00213 
00214 
00215   // Methods:
00216 
00217   Bool findInputFile(const Chars & fname);
00218   void createRWSFile();
00219   Word readWord(istream& istr);
00220   void printWord(ostream& str,const Word& w);
00221 /*
00222   void restartProcess();
00223   void haltProcess();
00224 */
00225 };
00226 
00227 #endif  

Generated at Tue Jun 19 09:49:36 2001 for Magnus Classes by doxygen1.2.6 written by Dimitri van Heesch, © 1997-2001