Show KBmagPackage.h syntax highlighted
// Copyright (C) 1994 The New York Group Theory Cooperative
// See magnus/doc/COPYRIGHT for the full notice.
// Contents: Definition of KBmagPackage class.
//
// Principal Author: Sarah Rees
//
// Status: in progress
//
// Revision History:
//
// * 06/24/95 Roger moved the ctors to .C, and made the static
// const Chars cdbin
// into a class data member, to both work around a compiler
// bug, and to avoid problems with the order of static init.
//
// Next implementation steps:
//
// * Deal with the many @rn, @rn:@sr, @sr comments here and in KBmagPackage.C
#ifndef _KBmagPackage_H_
#define _KBmagPackage_H_
#include <iostream>
#include <iomanip>
#include "Vector.h"
#include "Chars.h"
#include "Set.h"
#include "Word.h"
#include "DFSA.h"
#include "DiffMachine.h"
#include "GenMult.h"
#include "WordOrder.h"
class KBmagPackage {
public:
// KBmagPackage is a wrapper for Derek Holt's implementation of the automatic
// group procedures which attempt to prove a group automatic by constructing
// and verifying a shortlex automatic structure.
// Each of the relevant programs corresponds to a method in this class,
// which carries the name of Holt's program.
// Various automata are computed by these programs, and are stored in
// temporary files, but may be accessed by methods in this class.
//
// The method autgroup() runs the whole procedure. It returns YES if the
// procedure completes and proves the group automatic, NO if the procedure
// 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
// is not automatic, autgroup() could run forever, so it is unwise to call it. // It is wiser to run its constituent parts individually.
//
// These are as follows:-
//
// The method kbprog() runs a Knuth-Bendix procedure for a finite amount
// of time, and, given enough resources, must eventually terminate,
// when certain parameter bounds are met.
// When it terminates a difference machine is computed.
// YES is returned on successful termination, DONTKNOW if the
// program cannot terminate through lack of resources.
//
// Once a difference machine has been supplied, the method gpwa() computes
// a word acceptor from it. The construction is a finite logical operation,
// and, given enough resources, must terminate.
// Once a difference machine and word acceptor have been supplied, the
// method gpgenmult() computes a general multiplier from it. Given
// enough resources, this mult also terminate.
// For both gpwa() and gpgenmult(),
// YES is returned on successful termination, DONTKNOW if the
// program cannot terminate through lack of resources.
//
// gpcheckmult() performs preliminary checks on the word acceptor and
// general multipliers, and returns NO if those checks fails, YES on
// successful termination and DONTKNOW if the program cannot terminate through
// lack of resources. In the case of a NO answer, additional word
// differences are found and the difference machine is accordingly modified.
// A new word acceptor and new general multiplier may be computed from
// the modified difference machine, using gpwa() and gpgenmult()
// and the preliminary checks run again.
// The loop may be run until a YES answer is obtained from gpcheckmult()
//
// gpaxioms() performs further checks on the word acceptor and general
// multipliers, and returns YES if those check verify that the automata
// form an automatic structure, NO if the checks fail and DONTKNOW
// if the checks fail to complete due to lack of resources.
//
// The sensible way to test whether or not a group is automatic is thus
// to run kbprog(), then the sequence gpwa(), gpgenmult(), gpcheckmult()
// repeatedly until a YES answer is obtained from gpcheckmult(),
// then finally gpaxioms(). autgroup() runs the full suite of
// programs as above, and gpmakefsa() runs the loop gpwa(), gpcheckmult(),
// gpcheckmult(), stopping only when a YES answer is obtained.
// Hence both of autgroup() and gpmakefsa() should be used only with extreme
// caution.
//
// The automata may be recovered from the package using the
// methods wordAcceptor(), differenceMachine() and generalMultiplier().
// These automata may also be set, in which case any previously calculated
// by the package will be overwritten using the methods setWordAcceptor(),
// setDifferenceMachine() and setGeneralMultiplier(). Thus for instance
// the method gpwa() may be used to compute a word acceptor from any
// difference machine, and gpgenmult() may be used to compute the general
// multiplier based on any difference machine and word acceptor.
// In fact the automatic groups procedure builds in general two difference
// machines, the first of which accepts a sublanguage of the second.
//
// The integer argument of the methods differenceMachine and
// setDifferenceMachine() differentiates between those two automata. At the
// present the second is always used by the methods gpwa() and gpgenmult() -
// the Holt programs may be run to use the first as a space-saving device,
// but currently this option is not available within this class.
//
// The Package is initialised with the list of generators and relators
// of the groups,
// and (optionally)
// an integer array with specifies the order of the generators
// and their inverses used in the shortlex ordering.
// and an integer tidyint, which is a parameter for the KnuthBendix procedure.
KBmagPackage(const VectorOf<Chars>& genNames, const SetOf<Word>& rels,
const WordOrder & word_order,int tidyint) ;
KBmagPackage(const VectorOf<Chars>& genNames, const SetOf<Word>& rels,
const WordOrder & word_order) ;
KBmagPackage(const VectorOf<Chars>& genNames, const SetOf<Word>& rels);
~KBmagPackage();
// Takes care of shutting down the programs, and unlinking temp files/pipes.
Bool sanityCheck() const { return !error; }
// In each of the below, YES is returned if the program completes successfully
// having verified all checks which need to be made, and DONTKNOW is returned
// if for some reason the program cannot complete (usually because of lack of
// memory). NO is returned if the program completes and some checks have failed.
// In fact a NO answer is not possible from gpgenmult, gpmakefsa, gpwa or
// kbprog.
Trichotomy autgroup();
Trichotomy gpaxioms();
Trichotomy gpcheckmult();
Trichotomy gpgenmult(Bool eqcheck=YES);
Trichotomy gpmakefsa(Bool eqcheck=YES);
Trichotomy gpwa();
Trichotomy kbprog (int haltingfactor=100,int tidyint=20,int maxeqns=200,
int maxstates=1000);
Chars getName() const { Chars s = problemName; return s;}
Bool isProvedAutomatic( ) const { return provedAutomatic; }
Bool isProvedConfluent( ) const { return provedConfluent; }
Chars getGeneratorName(Generator g) const {
int i = ord(g);
if (i>0) return generatorNames[i-1];
else return(generatorNames[-i-1]+"^-1");
}
GroupDFSA wordAcceptor();
GenMult generalMultiplier();
DiffMachine differenceMachine(int i);
void setWordAcceptor(const GroupDFSA & WA);
void setGeneralMultiplier(const GenMult & GM);
void setDifferenceMachine(const DiffMachine & Diff,int i);
// and now versions of the above which use DFSARep's rather than DFSA's
// Maybe these should be private.
// They are necessary for use in code which needs to do serious manipulation
// with the automata, e.g. hyperbolicity testing.
GroupDFSARep wordAcceptorRep();
GenMultRep generalMultiplierRep();
DiffMachineRep differenceMachineRep(int i);
void setWordAcceptor(const GroupDFSARep & WARep);
void setGeneralMultiplier(const GenMultRep & GMRep);
void setDifferenceMachine(const DiffMachineRep & DiffRep,int i);
Bool minimize(DFSA & D);
Bool minimize(GroupDFSA & D);
Bool minimize(DFSARep & D);
Bool minimize(GroupDFSARep & D);
Bool gpcomp(GroupDFSA & D1,GroupDFSA & D2,GroupDFSA & D3);
Bool gpcomp(GroupDFSARep & D1,GroupDFSARep & D2,GroupDFSARep & D3);
private:
int numOfSymbols;
int tidyInterval;
Chars problemName; // Problem name supplied to KBmagPackage
VectorOf<Chars> generatorNames;
SetOf<Word> relators;
WordOrder order;
Bool error;
Bool provedAutomatic;
Bool provedConfluent;
Chars cdbin; //@rn Should be const, but then trouble initing.
// Methods:
Bool findInputFile(const Chars & fname);
void createRWSFile();
Word readWord(istream& istr);
void printWord(ostream& str,const Word& w);
/*
void restartProcess();
void haltProcess();
*/
};
#endif
See more files for this project here