public abstract class BatchFramework
extends java.lang.Object
An example of using this "framework" is BatchMMJ2 which sub-classes BatchFramework and is invoked via "main(String[] args)", passing those parameters in turn, to BatchFramework.
A RunParmFile is used to provide flexibility for many, many parameters in the future, and to allow for files using different code sets.
This code is experimental and goofy looking :) No warranty provided... The theme is that the order of input RunParmFile commands is unknown and therefore, each function must not make any assumptions about what has been done previously.
"Boss" classes are used to manage "state" information, and "get" commands build objects as needed, invoking functions under the control of other Bosses to obtain needed objects (which are *not* to be retained given the dynamic flux of state information.) This all seems very inefficient but the overhead is very small compared to the amount of work performed by each RunParmFile command.
A list of Bosses in use during a given run is maintained and each input RunParm line is sent to each Boss, in turn, which may or may not do anything with the command. Upon exit, a Boss returns "consumed" to indicate that the RunParm need not be sent to any other Bosses, that the job is done. Adding a new function, such as "Soundness checking" should be simple.
An alternate way to use BatchFramework is to instantiate one but instead of executing "runIt", invoke initializeBatchFramework() and then directly call routines in the various Boss classes, passing them hand-coded RunParmArrayEntry objects built using the UtilConstants RunParm name and value literals.. In other words, don't use a RunParmFile. This approach provides a short-cut for invoking mmj2 functions, to which new functions could be easily applied.
Modifier and Type | Field and Description |
---|---|
protected boolean |
batchFrameworkInitialized |
java.util.List<Boss> |
bossList |
protected CommandLineArguments |
commandLineArguments |
BatchCommand |
currentRunParmCommand |
boolean |
displayMMJ2FailPopupWindow |
GMFFBoss |
gmffBoss |
GrammarBoss |
grammarBoss |
LogicalSystemBoss |
logicalSystemBoss |
MacroBoss |
macroBoss |
MMJ2FailPopupWindow |
mmj2FailPopupWindow |
OutputBoss |
outputBoss |
Paths |
paths |
ProofAsstBoss |
proofAsstBoss |
int |
runParmCnt |
protected RunParmFile |
runParmFile |
StoreBoss |
storeBoss |
SvcBoss |
svcBoss |
TheoremLoaderBoss |
theoremLoaderBoss |
TMFFBoss |
tmffBoss |
VerifyProofBoss |
verifyProofBoss |
WorkVarBoss |
workVarBoss |
Constructor and Description |
---|
BatchFramework() |
Modifier and Type | Method and Description |
---|---|
void |
executeRunParmCommand(RunParmArrayEntry runParm)
Processes a single RunParmFile line.
|
java.lang.String |
getRunParmFileAbsolutePath()
Returns the canonical path name of the RunParmFile.
|
void |
initializeBatchFramework()
Initialize BatchFramework with Boss list and any captions that may have
been overridden.
|
void |
printCommentRunParmLine(int cnt,
RunParmArrayEntry runParm)
Override this to change or eliminate the printout of each Comment
RunParmFile line.
|
void |
printExecutableRunParmLine(int cnt,
RunParmArrayEntry runParm)
Override this to change or eliminate the printout of each executable
RunParmFile line.
|
int |
runIt(java.lang.String[] args)
Uses command line run parms to build
RunParmFile and
Paths objects, performs other initialization and processes each
RunParmFile line. |
protected boolean batchFrameworkInitialized
protected CommandLineArguments commandLineArguments
public Paths paths
public MMJ2FailPopupWindow mmj2FailPopupWindow
public boolean displayMMJ2FailPopupWindow
protected RunParmFile runParmFile
public int runParmCnt
public BatchCommand currentRunParmCommand
public java.util.List<Boss> bossList
public StoreBoss storeBoss
public OutputBoss outputBoss
public LogicalSystemBoss logicalSystemBoss
public VerifyProofBoss verifyProofBoss
public GrammarBoss grammarBoss
public ProofAsstBoss proofAsstBoss
public TMFFBoss tmffBoss
public WorkVarBoss workVarBoss
public SvcBoss svcBoss
public TheoremLoaderBoss theoremLoaderBoss
public GMFFBoss gmffBoss
public MacroBoss macroBoss
public void initializeBatchFramework()
The purpose of doing this here is to allow a BatchFramework to be constructed without executing any runparms from a file: every "doRunParm" function is public and can be called from a program (assuming the program can create a valid RunParmArrayEntry to provide RunParm option values.) This provides a shortcut to invoking complicated mmj2 functions that would otherwise require lots of setup and parameters.
public int runIt(java.lang.String[] args)
RunParmFile
and
Paths
objects, performs other initialization and processes each
RunParmFile line.
The MMJ2FailPopupWindow
object is initialized in startupMode and
gathers/displays error messages during startup logic. See
OutputBoss.printAndClearMessages()
which does the gathering and
displaying of startup errors. Abnormal termination -- "Fail" -- error
messages are displayed here by calling the MMJ2 Fail Popup Window
directly.
args
- command line parms for RunParmFile constructor. (See
CommandLineArguments.java for detailed docpublic void executeRunParmCommand(RunParmArrayEntry runParm) throws java.io.IOException, java.lang.IllegalArgumentException, VerifyException, TheoremLoaderException, MMIOException, GMFFException
runParm
- RunParmFileLine parsed into a RunParmArrayEntry object.java.io.IOException
- if an error occurred in the RunParmGMFFException
- if an error occurred in the RunParmMMIOException
- if an error occurred in the RunParmTheoremLoaderException
- if an error occurred in the RunParmVerifyException
- if an error occurred in the RunParmjava.lang.IllegalArgumentException
- if an error occurred in the RunParmpublic void printExecutableRunParmLine(int cnt, RunParmArrayEntry runParm) throws java.io.IOException
cnt
- RunParmFile line numberrunParm
- RunParmFile line parsed into object RunParmArrayEntry.java.io.IOException
- if an error occurred in the RunParmpublic void printCommentRunParmLine(int cnt, RunParmArrayEntry runParm) throws java.io.IOException
cnt
- RunParmFile line numberrunParm
- RunParmFile line parsed into object RunParmArrayEntry.java.io.IOException
- if an error occurred in the RunParmpublic java.lang.String getRunParmFileAbsolutePath()