public class SeqAssigner extends java.lang.Object implements TheoremLoaderCommitListener
SeqAssigner
generates sequence numbers for Metamath objects
(MObj) within the mmj2 Logical System.
SeqAssigner.java's job is assigning sequence numbers to Metamath objects (MObj's) as they are loaded and inserted in the mmj2 Logical System. Sequence numbers are assigned sequentially and provide the basis for the mechanism which ensures that cyclic or forward references by Metamath objects are rejected (as invalid).
The motivation for this new feature is assignment of sequence numbers for theorems inserted by the new Theorem Loader enhancement. Previously all Metamath objects were appended to the "end" of the Logical System and sequence numbers were assigned from 10 by 10 up to the maximum of 2**31 - 1.
The Theorem Loader aims to "insert" theorems and logical hypotheses into the sequence number "gaps" left over from the initial Metamath .mm file load(s) (RunParm "LoadFile").
The Theorem Loader determines the Metamath object dependencies of objects to be inserted and instructs SeqAssigner to assign in the gap after the referenced object with the highest sequence number. The SeqAssigner determines whether or not the "gap" is full and assigns the appropriate sequence number for each new object. A full gap results in an "append"ed sequence number, which may or may not be suitable -- if a new theorem is referred to by an existing theorem, then appending the new theorem is not acceptable (which results in an error and backout of all changes prior to detection of the error.)
Associated with SeqAssigner.java is a new RunParm,
SeqAssignerIntervalSize,9999The default sequence number interval is 1000, thus allowing for 999 inserts into every gap. It also provides the capability to load at least 1 million Metamath objects (perhaps more) into the mmj2 Logical System. An interval size of 100 would be suitable for almost every purpose -- the exception being automated updates from an external system via the new "mmj2 Service" feature.
Constructor and Description |
---|
SeqAssigner()
Construct with default set of parameters.
|
SeqAssigner(int intervalSize,
int intervalTblInitialSize)
Construct with full set of parameters.
|
Modifier and Type | Method and Description |
---|---|
void |
commit(MMTTheoremSet mmtTheoremSet)
Bit of a misnomer as this function merely turns off checkpointing.
|
int |
nextInsertSeq(int locAfterSeq)
Constructs MObj.seq value for a Metamath object to be inserted in the
number gap between two existing object.
|
int |
nextSeq()
Constructs MObj.seq value for new object.
|
void |
rollback(MMTTheoremSet mmtTheoremSet,
Messages messages,
boolean auditMessages)
Reverses all changes made to the SeqAssigner state variables since the
last checkpoing was taken.
|
void |
turnOnCheckpointing()
Bit of a misnomer as this function takes a checkpoint in case a rollback
is needed by TheoremLoader.
|
static void |
validateIntervalSize(int n)
Validates Interval Size parameter.
|
static void |
validateIntervalTblInitialSize(int n)
Validates Interval Table Initial Size parameter.
|
public SeqAssigner()
public SeqAssigner(int intervalSize, int intervalTblInitialSize)
intervalSize
- numbering interval for MObj.seq numbers.intervalTblInitialSize
- initial size of HashMap for recording
insertions in the sequence number interval gaps.public static void validateIntervalSize(int n)
Provided this function so that the same code can be used by LogicalSystemBoss.
n
- interval size for MObj.seq numbers.java.lang.IllegalArgumentException
- if invalid interval size.public static void validateIntervalTblInitialSize(int n)
Provided this function so that the same code can be used by LogicalSystemBoss.
n
- interval table initial size for MObj.seq numbers.public int nextSeq()
The return number is one of the "appended" sequence numbers, located logically at the end of LogicalSystem.
java.lang.IllegalArgumentException
- if the next available sequence number is
beyond the number range available to a Java "int".public int nextInsertSeq(int locAfterSeq)
The return number is one of the "inserted" sequence numbers, located logically at the end of LogicalSystem.
The input locAfterSeq designates a an "interval" which contains the "gap" of numbers (e.g. seq 3501 is in the 35 interval which has gap 3501 thru 3599.) The inserted sequence number goes into this gap if the gap is not already full. (A HashMap of BitSet is used to keep track of the intervals and gaps, respectively.)
To conserve empty gap space, if the locAfterSeq is assigned to the last interval in the system, then the next sequence number is not inserted, but appended.
If the next sequence number is not inserted (meaning that it is to be appended), then -1 is returned instead of the assigned sequence number.
locAfterSeq
- see descriptionjava.lang.IllegalArgumentException
- if the next available sequence number is
beyond the number range available to a Java "int".public void turnOnCheckpointing()
java.lang.IllegalArgumentException
- if checkpointing is already on.public void commit(MMTTheoremSet mmtTheoremSet)
commit
in interface TheoremLoaderCommitListener
mmtTheoremSet
- Set of TheoremStmtGroup updates now committedjava.lang.IllegalArgumentException
- if checkpointing is not already on.public void rollback(MMTTheoremSet mmtTheoremSet, Messages messages, boolean auditMessages)
Notice that only inserted sequence numbers are individually backed out. Appended sequence numbers are backed out en masse by reverting to the checkpointed value of "nbrIntervals" -- that is because there is no BitSet created for an interval until there is an insert in the interval's gap.
Audit messages are produced primarily so that the code is testable -- they provide "instrumentation".
mmtTheoremSet
- TheoremLoader's set of adds and updates.messages
- the Messages object for error loggingauditMessages
- true to write audit messagesjava.lang.IllegalArgumentException
- if a checkpoint was not taken prior to
the rollback request.