diff --git a/tlatools/build.gradle b/tlatools/build.gradle
index 85660550e7318132a6fe8af3ecc31f3b7bc48640..2ccb27ef4d49fb0dd0f9928597a1b71734eb7de3 100644
--- a/tlatools/build.gradle
+++ b/tlatools/build.gradle
@@ -1,21 +1,22 @@
apply plugin: 'java'
apply plugin: 'eclipse'
-apply plugin: 'maven'
+apply plugin: 'maven-publish'
project.version = '1.0.3-SNAPSHOT'
project.group = 'de.hhu.stups'
project.archivesBaseName = 'tlatools'
-project.sourceCompatibility = '1.7'
-project.targetCompatibility = '1.7'
+project.sourceCompatibility = '1.8'
+project.targetCompatibility = '1.8'
repositories {
mavenCentral()
+ mavenLocal()
}
dependencies {
- compile files ('lib/javax.mail.jar')
- testCompile files ('lib/easymock-3.3.1.jar', 'lib/jpf.jar', 'lib/junit-4.8.2.jar', 'lib/javax.mail.jar')
+ implementation files('lib/javax.mail/javax.activation_1.1.0.v201211130549.jar', 'lib/javax.mail/mailapi-1.6.3.jar', 'lib/smtp-1.6.3.jar')
+ implementation files('lib/easymock-3.3.1.jar', 'lib/jpf/jpf-shell.jar', 'lib/junit-4.12.jar', 'lib/javax.mail/javax.activation_1.1.0.v201211130549.jar', 'lib/javax.mail/mailapi-1.6.3.jar', 'lib/smtp-1.6.3.jar')
}
sourceSets {
@@ -31,16 +32,16 @@ sourceSets {
}
}
-task tlatools(dependsOn: build) << {
- copy {
- from('build/libs/')
- into('build/tlatools')
- include('tlatools-'+project.version+'.jar')
- rename('tlatools-(.+)', 'tlatools.jar')
- }
+tasks.register('tlatools', Copy) {
+ dependsOn tasks.named('build')
+
+ from('build/libs/')
+ into('build/tlatools')
+ include('tlatools-' + project.version + '.jar')
+ rename('tlatools-(.+)', 'tlatools.jar')
}
-if (project.hasProperty('ossrhUsername') && project.hasProperty('ossrhPassword')) {
+/*if (project.hasProperty('ossrhUsername') && project.hasProperty('ossrhPassword')) {
println "Configuring deployment for ${ project.name }"
@@ -110,4 +111,4 @@ uploadArchives {
}
}
}
-}
+}*/
diff --git a/tlatools/src/pcal/trans.java b/tlatools/src/pcal/trans.java
index 428dbcda55863f27945be154b49e9ac8b6d99dad..76a2ff405ae8874c428b73227ec76d9857e976ce 100644
--- a/tlatools/src/pcal/trans.java
+++ b/tlatools/src/pcal/trans.java
@@ -1696,7 +1696,7 @@ class trans {
{
throw new NumberFormatException();
}
- int a = new Integer(args[nextArg]).intValue();
+ int a = Integer.parseInt(args[nextArg]);
if (a < 60)
{
throw new NumberFormatException();
diff --git a/tlatools/src/tla2sany/explorer/ExploreNode.java b/tlatools/src/tla2sany/explorer/ExploreNode.java
index f3eb734631ebc0ed9ae9f6cf46a91a6b88cfdc74..9c9eefb7ec4880f25000da03b45735ca18c2cdf4 100644
--- a/tlatools/src/tla2sany/explorer/ExploreNode.java
+++ b/tlatools/src/tla2sany/explorer/ExploreNode.java
@@ -28,7 +28,11 @@ public interface ExploreNode {
* semNodesTable for itself and every descendant in the semantic tree *
* by executing *
* *
+<<<<<<< Updated upstream
* Integer uid = Integer.valueOf(myUID); *
+=======
+ * Integer uid = myUID; *
+>>>>>>> Stashed changes
* if (semNodesTable.get(uid) != null) return; *
* semNodesTable.put(uid, this); *
* *
diff --git a/tlatools/src/tla2sany/explorer/Explorer.java b/tlatools/src/tla2sany/explorer/Explorer.java
index 04d2e7a28585ac79ad14213d2853417f9a6da7f1..ceba315d6aeec4962fac3695d54c64fe62c11ed0 100644
--- a/tlatools/src/tla2sany/explorer/Explorer.java
+++ b/tlatools/src/tla2sany/explorer/Explorer.java
@@ -324,9 +324,9 @@ public class Explorer {
// "mt" command, which defaults to 2
if (ntokens < 2 || (icmd2 != null && icmd2.intValue() < 0)) {
if (firstToken.toLowerCase().startsWith("mt")) {
- icmd2 = new Integer(2);
+ icmd2 = 2;
} else {
- icmd2 = new Integer(4);
+ icmd2 = 4;
}
}
diff --git a/tlatools/src/tla2sany/parser/TLAplusParser.java b/tlatools/src/tla2sany/parser/TLAplusParser.java
index e5e0b1c895a901dd4bfc5b58f221e39b5639390c..adfd1d37600183cab0f3b7500f80454e1d5819f6 100644
--- a/tlatools/src/tla2sany/parser/TLAplusParser.java
+++ b/tlatools/src/tla2sany/parser/TLAplusParser.java
@@ -14,8 +14,8 @@ import util.UniqueString;
public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree, TLAplusParserConstants {
public String[] dependencies() {
- /***********************************************************************
- * This method is used in modanalyzer/{SyntaxTreePrinter,ParserUnit}. *
+ /***********************************************************************
+ * This method is used in modanalyzer/{SyntaxTreePrinter,ParserUnit}. *
***********************************************************************/
String[]deps = new String[ dependencyList.size() ];
for (int lvi =0; lvi < deps.length; lvi++)
@@ -24,19 +24,19 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
}
public TreeNode rootNode() { return ParseTree; }
public String moduleName() { return mn.toString(); }
-// public tla2sany.st.ParseErrors getErrors() { return PErrors; } Unused, apparently
-// The front end can simply read the public PErrors.
+// public tla2sany.st.ParseErrors getErrors() { return PErrors; } Unused, apparently
+// The front end can simply read the public PErrors.
public SyntaxTreeNode ParseTree;
- /***********************************************************************
- * The root node. *
+ /***********************************************************************
+ * The root node. *
***********************************************************************/
public Vector dependencyList = new Vector( 20 );
private UniqueString mn = null;
- /**********************************************************************
- * The module name. *
+ /**********************************************************************
+ * The module name. *
**********************************************************************/
private boolean numberFlag = false;
@@ -52,31 +52,31 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
private tla2sany.parser.OperatorStack OperatorStack = new tla2sany.parser.OperatorStack( PErrors );
private BracketStack BStack;
- /***********************************************************************
- * This is a stack of the kinds and offsets of the tokens that start a *
- * bulleted list within which the parser is currently grabbing tokens. *
+ /***********************************************************************
+ * This is a stack of the kinds and offsets of the tokens that start a *
+ * bulleted list within which the parser is currently grabbing tokens. *
***********************************************************************/
public boolean parse() {
- /***********************************************************************
- * This is a wrapper for actual parsing procedure CompilationUnit(). *
- * If an exception occurs, or if an error was pushed onto PErrors, *
- * then an error message is printed and it returns false. Otherwise, *
- * it returns true. Note that if we want to be able to parse an *
- * expression, we need to implement a similar wrapper for *
- * Expression(). *
+ /***********************************************************************
+ * This is a wrapper for actual parsing procedure CompilationUnit(). *
+ * If an exception occurs, or if an error was pushed onto PErrors, *
+ * then an error message is printed and it returns false. Otherwise, *
+ * it returns true. Note that if we want to be able to parse an *
+ * expression, we need to implement a similar wrapper for *
+ * Expression(). *
***********************************************************************/
- /***********************************************************************
- * The following code sets BStack to a new BracketStack object and *
- * initializes its classes field as described in BracketStack.java. *
+ /***********************************************************************
+ * The following code sets BStack to a new BracketStack object and *
+ * initializes its classes field as described in BracketStack.java. *
***********************************************************************/
BStack = new BracketStack();
BStack.newClass();
-// BStack.registerInCurrentClass( BAND );
+// BStack.registerInCurrentClass( BAND );
BStack.registerInCurrentClass( AND );
BStack.newClass();
-// BStack.registerInCurrentClass( BOR );
+// BStack.registerInCurrentClass( BOR );
BStack.registerInCurrentClass( OR );
BStack.newClass();
BStack.registerInCurrentClass( PROOF );
@@ -89,159 +89,159 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
catch( ParseException e ) {
PErrors.push( new ParseError( msgStackToString(e) ) ); }
catch( TokenMgrError tme ) {
- // lexical error.
+ // lexical error.
String msg = tme.getMessage();
int bl = jj_input_stream.getBeginLine() + 1;
int el = jj_input_stream.getEndLine() + 1;
- // lexical error.
+ // lexical error.
if ( (msg.indexOf("EOF") != -1) && (bl != el) ) {
PErrors.push(new ParseError(
"Lexical {error: EOF reached, " +
"possibly open comment starting around line " +
(bl-1) )) ;
} else PErrors.push( new ParseError( msg )) ;
-// PErrors.push( new ParseError( tme.getMessage() )) ;
+// PErrors.push( new ParseError( tme.getMessage() )) ;
} /*** end catch(TokenMgrError) ****/
if ( PErrors.empty() ) Assert.check( heirsIndex == 0, EC.SANY_PARSER_CHECK_1
-// "Assertion error in TLA+ Parser sanity check"
+// "Assertion error in TLA+ Parser sanity check"
);
- /*********************************************************************
- * This is a sanity check. The assertion should never be false. *
+ /*********************************************************************
+ * This is a sanity check. The assertion should never be false. *
*********************************************************************/
else {
- /*********************************************************************
- * An error has been pushed onto PErrors. It might have been done *
- * when an exception was caught, or by detecting an error during the *
- * parsing without throwing an exception. This happens in *
- * ExceptComponent() if it finds "!.@", and in FairnessExpr(). *
+ /*********************************************************************
+ * An error has been pushed onto PErrors. It might have been done *
+ * when an exception was caught, or by detecting an error during the *
+ * parsing without throwing an exception. This happens in *
+ * ExceptComponent() if it finds "!.@", and in FairnessExpr(). *
*********************************************************************/
tla2sany.st.ParseError list[] = PErrors.errors();
for (int i = 0; i < list.length; i++ ) {
ToolIO.out.println( list[i].reportedError() );
-// ToolIO.out.println( "+ " + list[i].defaultError() );
+// ToolIO.out.println( "+ " + list[i].defaultError() );
}
}
-// ParseTree.setNumberFlags( numberFlag, decimalFlag );
+// ParseTree.setNumberFlags( numberFlag, decimalFlag );
return PErrors.empty();
}
-/*
- this is required to store temporarily information required by
- the semantic lookahead, as it doesn't have access to the variables
- of the production
+/*
+ this is required to store temporarily information required by
+ the semantic lookahead, as it doesn't have access to the variables
+ of the production
*/
private SyntaxTreeNode local;
void registerTN( SyntaxTreeNode some) { local = some ; }
boolean testTN() {
- /***********************************************************************
- * THIS METHOD IS APPARENTLY NOT USED. *
+ /***********************************************************************
+ * THIS METHOD IS APPARENTLY NOT USED. *
***********************************************************************/
return local.isKind(N_IdPrefix)
&& BStack.aboveReference( local.first().first().location[0] ) ;
}
private SyntaxTreeNode anchor = null;
- /***********************************************************************
- * This is set to a non-null value only in Expression(). If a *
- * ClosedExpressionOrOp node is found when parsing an expression, *
- * anchor is set to that node. It is set to null in the following *
- * places: *
- * *
- * - When beginning to parse a Substitution() *
- * *
- * - When OpSuite() or Substitution() finds that anchor equals an *
- * Op Symbol, as described below. *
- * *
- * The Substitution() and OpSuite() procedures look for an *
- * Expression or Op Symbol by calling Expression() and, if that throws *
- * an exception, catching the expression and checking if anchor is the *
- * desired Op Symbol. *
+ /***********************************************************************
+ * This is set to a non-null value only in Expression(). If a *
+ * ClosedExpressionOrOp node is found when parsing an expression, *
+ * anchor is set to that node. It is set to null in the following *
+ * places: *
+ * *
+ * - When beginning to parse a Substitution() *
+ * *
+ * - When OpSuite() or Substitution() finds that anchor equals an *
+ * Op Symbol, as described below. *
+ * *
+ * The Substitution() and OpSuite() procedures look for an *
+ * Expression or Op Symbol by calling Expression() and, if that throws *
+ * an exception, catching the expression and checking if anchor is the *
+ * desired Op Symbol. *
***********************************************************************/
-// Lookahead mechanisms for definitions
- /*************************************************************************
- * The following code is lifted directly from the getToken method *
- * created by JavaCC in the file TLAplusParser.java. *
- * *
- * J-Ch doesn't remember why he defined this method instead of just *
- * using the GetToken method. He thinks that it was to make sure *
- * it would always return a token rather than null. *
+// Lookahead mechanisms for definitions
+ /*************************************************************************
+ * The following code is lifted directly from the getToken method *
+ * created by JavaCC in the file TLAplusParser.java. *
+ * *
+ * J-Ch doesn't remember why he defined this method instead of just *
+ * using the GetToken method. He thinks that it was to make sure *
+ * it would always return a token rather than null. *
*************************************************************************/
final private Token getNextPreviewToken(Token t) {
if (t.next == null) t.next = token_source.getNextToken();
- /********************************************************************
- * token_source is declared in configuration/Configuration.java to *
- * be a ConfigurationTokenManager. *
+ /********************************************************************
+ * token_source is declared in configuration/Configuration.java to *
+ * be a ConfigurationTokenManager. *
********************************************************************/
return t.next;
}
-// borrowed from code generated by JavaCC.
+// borrowed from code generated by JavaCC.
final private Token initPreviewToken() {
return lookingAhead ? jj_scanpos : token;
- /*********************************************************************
- * `lookingAhead', `token', and `jj_scanpos' are declared in *
- * TLAplusParser (created by javacc from this file). The javacc *
- * documentation says that token is the value returned by *
- * getToken(0). God only knows what lookingAhead and jj_scanpos *
- * are. *
+ /*********************************************************************
+ * `lookingAhead', `token', and `jj_scanpos' are declared in *
+ * TLAplusParser (created by javacc from this file). The javacc *
+ * documentation says that token is the value returned by *
+ * getToken(0). God only knows what lookingAhead and jj_scanpos *
+ * are. *
*********************************************************************/
}
private final void belchDEF() {
- /***********************************************************************
- * The purpose of this method seems to be to introduce a dummy *
- * <DEFBREAK> token into the token stream, which is used in parsing *
- * the OperatorOrFunctionDefinition non-terminal. *
+ /***********************************************************************
+ * The purpose of this method seems to be to introduce a dummy *
+ * <DEFBREAK> token into the token stream, which is used in parsing *
+ * the OperatorOrFunctionDefinition non-terminal. *
***********************************************************************/
Token previousT = initPreviewToken();
Token currentT = getNextPreviewToken( previousT );
- previousT.next = null; // <-- to break recursion
+ previousT.next = null; // <-- to break recursion
Token nextT = getNextPreviewToken( currentT );
currentT.next = previousT;
while ( nextT.kind != EOF
&& nextT.kind != THEOREM
&& nextT.kind != PROPOSITION
- /***************************************************************
- * This test for PROPOSITION added by LL on 5 Sep 2010 to get *
- * the parser to handle a named PROPOSITION, LEMMA, or *
- * COROLLARY. *
+ /***************************************************************
+ * This test for PROPOSITION added by LL on 5 Sep 2010 to get *
+ * the parser to handle a named PROPOSITION, LEMMA, or *
+ * COROLLARY. *
***************************************************************/
-// && nextT.kind != ASSUME
- /****************************************************************
- * This test for ASSUME removed on 26 June 2007. *
- * It made belchDEF get hung up on nested ASSUME/PROVEs. *
- * However, this permitted extra DEFBREAK tokens to be inserted. *
- * Those extra tokens were eliminated by the change on the same *
- * date described below. *
+// && nextT.kind != ASSUME
+ /****************************************************************
+ * This test for ASSUME removed on 26 June 2007. *
+ * It made belchDEF get hung up on nested ASSUME/PROVEs. *
+ * However, this permitted extra DEFBREAK tokens to be inserted. *
+ * Those extra tokens were eliminated by the change on the same *
+ * date described below. *
****************************************************************/
&& nextT.kind != ASSUMPTION
&& nextT.kind != END_MODULE) {
- /*********************************************************************
- * As long as we have not yet reached the end of the stream or a *
- * THEOREM, ASSUME, or END_MODULE token, move forward through the *
- * token stream looking for a "==" token. Maintain a chain of the *
- * tokens passed over, with t.next equal to the previous token, and *
- * t.next = null for the first token. *
- * *
- * At this point, the last three tokens obtained are previoustT, *
- * currentT, and nextT, where currentT.next = previousT and *
- * nextT.next points to the first unexamined token. *
+ /*********************************************************************
+ * As long as we have not yet reached the end of the stream or a *
+ * THEOREM, ASSUME, or END_MODULE token, move forward through the *
+ * token stream looking for a "==" token. Maintain a chain of the *
+ * tokens passed over, with t.next equal to the previous token, and *
+ * t.next = null for the first token. *
+ * *
+ * At this point, the last three tokens obtained are previoustT, *
+ * currentT, and nextT, where currentT.next = previousT and *
+ * nextT.next points to the first unexamined token. *
*********************************************************************/
if ( currentT.kind == DEF ) {
- /*******************************************************************
- * currentT is a "==" token. *
+ /*******************************************************************
+ * currentT is a "==" token. *
*******************************************************************/
Token t = previousT;
if ( t.kind == RBR || t.kind == RSB ) {
- /*****************************************************************
- * t = previousT is a ")" or "]" token. *
+ /*****************************************************************
+ * t = previousT is a ")" or "]" token. *
*****************************************************************/
- // the following code assumes that parentheses are evenly balanced.
- // something could be added to reinforce the test.
- // they do not have to be on the same line either, btw.
+ // the following code assumes that parentheses are evenly balanced.
+ // something could be added to reinforce the test.
+ // they do not have to be on the same line either, btw.
int depth = 1;
while (t.next != null) {
t = t.next;
@@ -252,37 +252,37 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
if (t.next == null ) break;
else if (t.next.kind == IDENTIFIER)
t = t.next;
- // we are positioned at first symbol before "[" or "(" : must be an identifier
+ // we are positioned at first symbol before "[" or "(" : must be an identifier
} else
- /*****************************************************************
- * t = previousT is not a ")" or "]" token. *
+ /*****************************************************************
+ * t = previousT is not a ")" or "]" token. *
*****************************************************************/
if ( t.kind == IDENTIFIER ) {
- /**************************************************************
- * t is an IDENTIFIER token. *
- * *
- * If t.next [the previous token in the input stream] is a *
- * non-prefix operator and is not preceded in the stream by *
- * "<-" [so it belongs to a preceding substitution], then set *
- * t to t.next if it is a prefix operator and to t.next.next *
- * if it is an infix operator. *
- * *
- * Note: If belchDef is called with the input stream at *
- * something like "++ a ==", then evaluating t.next.next *
- * dereferences null. This should happen only if the user *
- * has left off the first parameter of the definitiion and *
- * the resulting exception seems to be caught, but it *
- * produces a misleading error message. This type of rare *
- * error is hardly worth worrying about, but it would be easy *
- * enough to add a test and might be worth doing if it's easy *
- * to produce the right error message. *
- * *
- * Modified 22 Feb 2013 by LL to check that something like *
- * "++ a ==" is preceded by an identifier. This fixes *
- * mishandled case of something like *
- * *
- * USE ... DEF ++ *
- * a == ... *
+ /**************************************************************
+ * t is an IDENTIFIER token. *
+ * *
+ * If t.next [the previous token in the input stream] is a *
+ * non-prefix operator and is not preceded in the stream by *
+ * "<-" [so it belongs to a preceding substitution], then set *
+ * t to t.next if it is a prefix operator and to t.next.next *
+ * if it is an infix operator. *
+ * *
+ * Note: If belchDef is called with the input stream at *
+ * something like "++ a ==", then evaluating t.next.next *
+ * dereferences null. This should happen only if the user *
+ * has left off the first parameter of the definitiion and *
+ * the resulting exception seems to be caught, but it *
+ * produces a misleading error message. This type of rare *
+ * error is hardly worth worrying about, but it would be easy *
+ * enough to add a test and might be worth doing if it's easy *
+ * to produce the right error message. *
+ * *
+ * Modified 22 Feb 2013 by LL to check that something like *
+ * "++ a ==" is preceded by an identifier. This fixes *
+ * mishandled case of something like *
+ * *
+ * USE ... DEF ++ *
+ * a == ... *
**************************************************************/
Token identifier = t;
if ( isOp(t.next)
@@ -294,28 +294,28 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
) {
t = t.next;
if ( t.next.kind == SUBSTITUTE )
- t = identifier; // skip back
+ t = identifier; // skip back
else if ( isInfixOp( t ) ) t = t.next;
- // else assume prefix
+ // else assume prefix
}
} else {
- /**************************************************************
- * t is not an IDENTIFIER token. *
- * *
- * If it is an operator token, set t to t.next. (It will be *
- * a postfix operator unless the user made an error.) *
+ /**************************************************************
+ * t is not an IDENTIFIER token. *
+ * *
+ * If it is an operator token, set t to t.next. (It will be *
+ * a postfix operator unless the user made an error.) *
**************************************************************/
- if ( isOp(t) ) { // assume postfix op, the parser will catch the error
+ if ( isOp(t) ) { // assume postfix op, the parser will catch the error
t = t.next;
}
}
- /*******************************************************************
- * Insert a DEFBREAK token into the input stream right before *
- * token t, and exit the while loop. *
- * *
- * Changed by LL on 26 June 2007 so it doesn't add the DEFBREAK *
- * token if there's already one there. (This could happen because *
- * of the change to pass over ASSUMEs described above.) *
+ /*******************************************************************
+ * Insert a DEFBREAK token into the input stream right before *
+ * token t, and exit the while loop. *
+ * *
+ * Changed by LL on 26 June 2007 so it doesn't add the DEFBREAK *
+ * token if there's already one there. (This could happen because *
+ * of the change to pass over ASSUMEs described above.) *
*******************************************************************/
if ( (t.next == null)
|| (t.next.kind != DEFBREAK)) {
@@ -331,8 +331,8 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
} ;
break; /* EXIT while */
} else {
- /*******************************************************************
- * currentT is not a "==" token. *
+ /*******************************************************************
+ * currentT is not a "==" token. *
*******************************************************************/
previousT = currentT;
currentT = nextT;
@@ -340,10 +340,10 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
currentT.next = previousT;
}
} /* END while */
- // reverse pointers.
- /***********************************************************************
- * Go back through the examined tokens, making t.next point to the *
- * next one for each token t. *
+ // reverse pointers.
+ /***********************************************************************
+ * Go back through the examined tokens, making t.next point to the *
+ * next one for each token t. *
***********************************************************************/
while (previousT != null ) {
currentT.next = nextT;
@@ -351,11 +351,11 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
currentT = previousT;
previousT = currentT.next;
}
- // relink firstT
+ // relink firstT
currentT.next = nextT;
}
-//
+//
void skipOver( int l ) {
while ( true ) {
Token t = getToken(1);
@@ -365,16 +365,16 @@ public class TLAplusParser implements tla2sany.st.SyntaxTreeConstants, ParseTree
}
}
-/***************************************************************************
-* Note: the non-terminal ClosedStart was commented out, apparently to be *
-* replaced by this boolean-valued method. *
+/***************************************************************************
+* Note: the non-terminal ClosedStart was commented out, apparently to be *
+* replaced by this boolean-valued method. *
***************************************************************************/
boolean
ClosedStart( Token t ) {
return t.kind == IDENTIFIER
|| (t.kind >= op_57 && t.kind <= op_119)
- /****************************************************************
- * These are all prefix, infix, and postfix operators. *
+ /****************************************************************
+ * These are all prefix, infix, and postfix operators. *
****************************************************************/
|| t.kind == NUMBER_LITERAL
|| t.kind == LBR
@@ -404,11 +404,11 @@ boolean isPrefixOp( Token t ) {
return t.kind >= op_26 && t.kind <= op_116;
}
-// global variable follows !!! Make sure it is set everywhere as required
+// global variable follows !!! Make sure it is set everywhere as required
Operator lastOp;
- /*************************************************************************
- * This seems to equal the last Prefix, Infix, PostFix, or NonExpPrefix *
- * op that was parsed. *
+ /*************************************************************************
+ * This seems to equal the last Prefix, Infix, PostFix, or NonExpPrefix *
+ * op that was parsed. *
*************************************************************************/
boolean isGenOp(SyntaxTreeNode tn) { /* has to be of the form prefix, opsym */
@@ -423,46 +423,46 @@ Operator lastOp;
return false;
}
-// boolean IsNotExpression () {
-// /***********************************************************************
-// * This method is called only in NumberedAssumeProve. *
-// ***********************************************************************/
-// Token t = initPreviewToken();
-// t = getNextPreviewToken(t);
-// /*********************************************************************
-// * Previous statement added on 1 Mar 2007 by J-Ch and LL to fix bug. *
-// *********************************************************************/
-// int k = t.kind;
-// if ( k == US || k == LOCAL || k == VARIABLE || k == PARAMETER || k == INSTANCE || k == CONSTANT || k == STATE || k == ACTION || k == TEMPORAL ) return true;
-// else {
-// t = getNextPreviewToken(t); k = t.kind;
-// if ( k == US || k == DEF || k == LSB )
-// return true;
-// else if (k == LBR) {
-// int depth = 1;
-// Token nt = getNextPreviewToken(t);
-// while (true) {
-// t = nt; nt = getNextPreviewToken(t); k = t.kind;
-// if ( k == RBR ) {
-// if ( depth == 1 )
-// if ( nt.kind == DEF ) return true;
-// else return false;
-// else
-// depth--;
-// } else
-// if ( k == LBR ) { depth++;
-// } else
-// if ( k == EOF ) return false;
-// }
-// }
-// }
-// return false;
-// }
-//
+// boolean IsNotExpression () {
+// /***********************************************************************
+// * This method is called only in NumberedAssumeProve. *
+// ***********************************************************************/
+// Token t = initPreviewToken();
+// t = getNextPreviewToken(t);
+// /*********************************************************************
+// * Previous statement added on 1 Mar 2007 by J-Ch and LL to fix bug. *
+// *********************************************************************/
+// int k = t.kind;
+// if ( k == US || k == LOCAL || k == VARIABLE || k == PARAMETER || k == INSTANCE || k == CONSTANT || k == STATE || k == ACTION || k == TEMPORAL ) return true;
+// else {
+// t = getNextPreviewToken(t); k = t.kind;
+// if ( k == US || k == DEF || k == LSB )
+// return true;
+// else if (k == LBR) {
+// int depth = 1;
+// Token nt = getNextPreviewToken(t);
+// while (true) {
+// t = nt; nt = getNextPreviewToken(t); k = t.kind;
+// if ( k == RBR ) {
+// if ( depth == 1 )
+// if ( nt.kind == DEF ) return true;
+// else return false;
+// else
+// depth--;
+// } else
+// if ( k == LBR ) { depth++;
+// } else
+// if ( k == EOF ) return false;
+// }
+// }
+// }
+// return false;
+// }
+//
boolean isFieldNameToken( Token t ) {
- /***********************************************************************
- * Modified by LL on 10 Oct 2007 because of new keywords added and *
- * obsolete ones removed. *
+ /***********************************************************************
+ * Modified by LL on 10 Oct 2007 because of new keywords added and *
+ * obsolete ones removed. *
***********************************************************************/
if ( (t.kind >= ACTION && t.kind <= EXCEPT)
||(t.kind == EXTENDS)
@@ -478,11 +478,11 @@ Operator lastOp;
}
boolean isLabel(SyntaxTreeNode node) {
- /***********************************************************************
- * Checks that node is a label, meaning that it is either an *
- * identifier token or else an OpApplication node each of whose *
- * arguments is an OpArgs node whose child is a GeneralId node with an *
- * empty IdPrefix. *
+ /***********************************************************************
+ * Checks that node is a label, meaning that it is either an *
+ * identifier token or else an OpApplication node each of whose *
+ * arguments is an OpArgs node whose child is a GeneralId node with an *
+ * empty IdPrefix. *
***********************************************************************/
if (node == null) {return false;} ;
if (node.isKind(N_GeneralId)) {
@@ -491,32 +491,32 @@ Operator lastOp;
if (! node.isKind(N_OpApplication)) {return false;} ;
SyntaxTreeNode opArgs = (SyntaxTreeNode) node.heirs()[1] ;
if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
- /*******************************************************************
- * Sanity check--can be removed after debugging. *
+ /*******************************************************************
+ * Sanity check--can be removed after debugging. *
*******************************************************************/
for (int i = 1; i < opArgs.heirs().length; i = i+2) {
- /*********************************************************************
- * THe OpArg node for Op(arg_1, ... , arg_N) has the 2N+1 heirs *
- * *
- * "(" arg_1 "," ... "," arg_N ")" *
+ /*********************************************************************
+ * THe OpArg node for Op(arg_1, ... , arg_N) has the 2N+1 heirs *
+ * *
+ * "(" arg_1 "," ... "," arg_N ")" *
*********************************************************************/
SyntaxTreeNode genId = (SyntaxTreeNode) opArgs.heirs()[i] ;
if (genId.kind != N_GeneralId) {return false;} ;
if (genId.heirs()[0].heirs().length != 0){return false;}
- } // for
+ } // for
return true;
}
boolean labelDoesNotChangeParse(SyntaxTreeNode labeledExpr,
Operator labelOp) {
- /***********************************************************************
- * Checks if preceding the expression labeledExpr with a label has not *
- * changed the parsing of the enclosing expression. It has changed *
- * the parsing iff *
- * /\ labeledExpr is an infix or postfix expression with operator *
- * labelOp *
- * /\ the top of OperatorStack is an infix or prefix operator stackOp *
- * /\ it is not the case that stackOp \prec labelOp. *
+ /***********************************************************************
+ * Checks if preceding the expression labeledExpr with a label has not *
+ * changed the parsing of the enclosing expression. It has changed *
+ * the parsing iff *
+ * /\ labeledExpr is an infix or postfix expression with operator *
+ * labelOp *
+ * /\ the top of OperatorStack is an infix or prefix operator stackOp *
+ * /\ it is not the case that stackOp \prec labelOp. *
***********************************************************************/
if ( ! ( labeledExpr.isKind(N_InfixExpr)
|| labeledExpr.isKind(N_PostfixExpr) ) ) {return true;} ;
@@ -529,12 +529,12 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
void checkIndentation(SyntaxTreeNode nd, SyntaxTreeNode junct)
throws ParseException {
- /***********************************************************************
- * Goes through the descendants of node nd, stopping at an N_DisjList *
- * or N_ConjList node. For each node it finds, if checks whether it *
- * is properly indented with respect to the current N_DisjItem or *
- * N_ConjItem junct. If not, it reports an error by throwing an *
- * exception. *
+ /***********************************************************************
+ * Goes through the descendants of node nd, stopping at an N_DisjList *
+ * or N_ConjList node. For each node it finds, if checks whether it *
+ * is properly indented with respect to the current N_DisjItem or *
+ * N_ConjItem junct. If not, it reports an error by throwing an *
+ * exception. *
***********************************************************************/
TreeNode[] children = nd.heirs() ;
for (int i = 0; i < children.length; i++) {
@@ -552,9 +552,9 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
} ;
}
-// predicate used in lookahead to discriminate between the Case Separator and
-// the box operator. Returns true if it is most likely not the separator.
-// This is a weak mechanism.
+// predicate used in lookahead to discriminate between the Case Separator and
+// the box operator. Returns true if it is most likely not the separator.
+// This is a weak mechanism.
boolean boxDisc() {
Token t = getToken(1);
if ( t.kind == CASESEP )
@@ -569,14 +569,14 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
}
boolean matchFcnConst () {
- /***********************************************************************
- * Seems to return true iff the next current token sequence begins *
- * with "<< ... >> \in" or "Identifier [, Identifier] \in". It is *
- * used after a "{" to see if this is a subset expression such as "{x *
- * \in S : exp}" and after a "[" to see if it is a function expression *
- * such as "[x \in S |-> exp]". This leads to the bug that it starts *
- * incorrectly interpreting the expressions "{x \in S}" and *
- * "{<<1, 2>> \in {}}" as a subset expression and reports an error. *
+ /***********************************************************************
+ * Seems to return true iff the next current token sequence begins *
+ * with "<< ... >> \in" or "Identifier [, Identifier] \in". It is *
+ * used after a "{" to see if this is a subset expression such as "{x *
+ * \in S : exp}" and after a "[" to see if it is a function expression *
+ * such as "[x \in S |-> exp]". This leads to the bug that it starts *
+ * incorrectly interpreting the expressions "{x \in S}" and *
+ * "{<<1, 2>> \in {}}" as a subset expression and reports an error. *
***********************************************************************/
Token t = initPreviewToken();
t = getNextPreviewToken( t );
@@ -603,11 +603,11 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
return false;
}
-// int numberFromStep( String step ) {
-// int top = step.indexOf('>');
-// return Integer.parseInt( step.substring( 1, top ) );
-// }
-//
+// int numberFromStep( String step ) {
+// int top = step.indexOf('>');
+// return Integer.parseInt( step.substring( 1, top ) );
+// }
+//
Object msgStack[] = new Object[ 512 ];
int msgStackMaxSize = 512;
int msgStackCurrentSize = 0;
@@ -629,10 +629,10 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
}
private String expecting = "nothing";
- /***********************************************************************
- * It appears that the value of expecting is what is printed out in *
- * error messages as what the parser was expecting when it encountered *
- * an error. *
+ /***********************************************************************
+ * It appears that the value of expecting is what is printed out in *
+ * error messages as what the parser was expecting when it encountered *
+ * an error. *
***********************************************************************/
private final String msgStackToString(ParseException e) {
@@ -646,10 +646,10 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
}
msg.append(e.getShortMessage());
-// msg.append(" while parsing ");
-// msg.append(name);
-//
-// msg.append(".\nResidual stack trace follows:\n");
+// msg.append(" while parsing ");
+// msg.append(name);
+//
+// msg.append(".\nResidual stack trace follows:\n");
msg.append("\n\nResidual stack trace follows:\n");
int last = msgStackCurrentSize - 10;
@@ -666,33 +666,33 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
return msg.toString();
}
-//
-
- /*************************************************************************
- * heirsTable is an array of physical length heirsSize that implements a *
- * dynamic array of length heirsIndex, where heirsIndex <= heirsSize. *
- * Elements are added to heirsTable by the addHeir method, which *
- * increments heirsSize if needed. Elements are removed from the array *
- * by the getLastHeirs() and popHeir() methods. *
- * *
- * It appears that the heirsTable is used as a stack of sequences of *
- * syntax tree nodes, each being the sequence of heirs (children) of a *
- * node that is currently being parsed. The top of the stack is the *
- * sequence at the end of the heirsTable array. Each sequence is begun *
- * by a null entry. The bpa() method is called when about to push such *
- * a sequence onto the stack; it adds the null element that marks the *
- * beginning of the sequence. Similarly, the epa() method is called *
- * after popping a sequence off the top of the stack; it removes the *
- * null element. *
+//
+
+ /*************************************************************************
+ * heirsTable is an array of physical length heirsSize that implements a *
+ * dynamic array of length heirsIndex, where heirsIndex <= heirsSize. *
+ * Elements are added to heirsTable by the addHeir method, which *
+ * increments heirsSize if needed. Elements are removed from the array *
+ * by the getLastHeirs() and popHeir() methods. *
+ * *
+ * It appears that the heirsTable is used as a stack of sequences of *
+ * syntax tree nodes, each being the sequence of heirs (children) of a *
+ * node that is currently being parsed. The top of the stack is the *
+ * sequence at the end of the heirsTable array. Each sequence is begun *
+ * by a null entry. The bpa() method is called when about to push such *
+ * a sequence onto the stack; it adds the null element that marks the *
+ * beginning of the sequence. Similarly, the epa() method is called *
+ * after popping a sequence off the top of the stack; it removes the *
+ * null element. *
*************************************************************************/
private SyntaxTreeNode heirsTable[] = new SyntaxTreeNode[ 512 ];
private int heirsSize = 512;
private int heirsIndex = 0;
private final void addHeir( SyntaxTreeNode sn ) {
- /***********************************************************************
- * Appends the syntax tree sn to the end of the dynamic array *
- * implemented by heirsTable. *
+ /***********************************************************************
+ * Appends the syntax tree sn to the end of the dynamic array *
+ * implemented by heirsTable. *
***********************************************************************/
if ( heirsIndex == heirsSize ) {
SyntaxTreeNode nh[] = new SyntaxTreeNode[ heirsSize + 512 ];
@@ -704,22 +704,22 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
}
private final SyntaxTreeNode[] getLastHeirs() {
- /***********************************************************************
- * This method will throw an array-out-of-bounds exception if called *
- * when heirsIndex = 0 (so the dynamic array implemented by heirsTable *
- * is empty) or if that dynamic array contains no null entry. *
- * *
- * If the last element of the dynamic heirsTable array is null, then *
- * it returns null. Otherwise, it returns an array equal to the *
- * sequence of non-null elements at the end of the dynamic heirsTable *
- * array and removes them from that array. *
+ /***********************************************************************
+ * This method will throw an array-out-of-bounds exception if called *
+ * when heirsIndex = 0 (so the dynamic array implemented by heirsTable *
+ * is empty) or if that dynamic array contains no null entry. *
+ * *
+ * If the last element of the dynamic heirsTable array is null, then *
+ * it returns null. Otherwise, it returns an array equal to the *
+ * sequence of non-null elements at the end of the dynamic heirsTable *
+ * array and removes them from that array. *
***********************************************************************/
int lvi = heirsIndex - 1;
while (heirsTable[ lvi ] != null ) lvi--;
- /***********************************************************************
- * Assert: /\ lvi < heirsIndex *
- * /\ heirsTable[lvi] = null *
- * /\ \A i \in lvi+1 .. heirsIndex-1 : heirsTable[i] # null *
+ /***********************************************************************
+ * Assert: /\ lvi < heirsIndex *
+ * /\ heirsTable[lvi] = null *
+ * /\ \A i \in lvi+1 .. heirsIndex-1 : heirsTable[i] # null *
***********************************************************************/
int as = heirsIndex - lvi - 1;
if (as == 0)
@@ -728,29 +728,29 @@ if (opArgs.kind != N_OpArgs) { ToolIO.out.println("Bug: not N_OpArgs node"); };
SyntaxTreeNode ts[] = new SyntaxTreeNode[ as ];
System.arraycopy( heirsTable, lvi + 1, ts, 0, as);
heirsIndex = lvi + 1;
- /*********************************************************************
- * Assert /\ as > 0 *
- * /\ \A i \in 0..as-1 : ts[i] = heirsTable[lvi + i + 1] *
- * /\ heirsIndex = lvi + 1 *
+ /*********************************************************************
+ * Assert /\ as > 0 *
+ * /\ \A i \in 0..as-1 : ts[i] = heirsTable[lvi + i + 1] *
+ * /\ heirsIndex = lvi + 1 *
*********************************************************************/
return ts;
}
}
private final boolean popHeir() {
- /************************************************************************
- * Throws an array-out-of-bounds exception if heirsIndex = 0 (meaning *
- * that the dynamic array implemented by heirsTable is empty). *
- * *
- * It removes the last element from the heirsTable array and returns *
- * true iff the new last element is null. *
+ /************************************************************************
+ * Throws an array-out-of-bounds exception if heirsIndex = 0 (meaning *
+ * that the dynamic array implemented by heirsTable is empty). *
+ * *
+ * It removes the last element from the heirsTable array and returns *
+ * true iff the new last element is null. *
************************************************************************/
return heirsTable[ --heirsIndex ] == null;
}
private String emptyString = "";
- private final void bpa( String s) { // Beginning of Production Actions
+ private final void bpa( String s) { // Beginning of Production Actions
addHeir( null );
if (System.getProperty("TLA-StackTrace", "off").equals("on")) ToolIO.out.println("Beginning " + s);
pushMsg( s, getToken(1) );
@@ -761,10 +761,10 @@ if (System.getProperty("TLA-StackTrace", "off").equals("on")) ToolIO.out.println
popMsg();
if (System.getProperty("TLA-StackTrace", "off").equals("on")) ToolIO.out.println("Ending " + msgStack [ msgStackCurrentSize ]);
Assert.check( popHeir(), EC.SANY_PARSER_CHECK_2);
- // "Assertion error in epa()"
+ // "Assertion error in epa()"
expecting = emptyString;
}
-//
+//
Stack internals = new Stack();
@@ -796,44 +796,44 @@ if (System.getProperty("TLA-StackTrace", "off").equals("on")) ToolIO.out.println
return UniqueString.uniqueStringOf(copy.toString());
}
-/***************************************************************************
-* Fields and methods for parsing proofs. *
+/***************************************************************************
+* Fields and methods for parsing proofs. *
***************************************************************************/
private int proofDepth = -1 ;
- /*************************************************************************
- * The nesting level of the proof we're currently processing, counting *
- * from 0 a la Java. *
+ /*************************************************************************
+ * The nesting level of the proof we're currently processing, counting *
+ * from 0 a la Java. *
*************************************************************************/
private final int MaxProofDepth = 100 ;
private int[] proofLevelStack = new int[MaxProofDepth] ;
- /*************************************************************************
- * The level number of a proof with steps numbered <n>x is n. The value *
- * of proofLevelStack[proofDepth] is the level number of the current *
- * proof. If we have started processing a proof haven't yet determined *
- * its level, then proofLevelStack[proofDepth] equals -1. *
+ /*************************************************************************
+ * The level number of a proof with steps numbered <n>x is n. The value *
+ * of proofLevelStack[proofDepth] is the level number of the current *
+ * proof. If we have started processing a proof haven't yet determined *
+ * its level, then proofLevelStack[proofDepth] equals -1. *
*************************************************************************/
private int levelOfProofStepLexeme(Token tok){
- /*************************************************************************
- * The level of a ProofStepLexeme or ProofStepDotLexeme. It returns -1 *
- * for "*" and -2 for "*". *
+ /*************************************************************************
+ * The level of a ProofStepLexeme or ProofStepDotLexeme. It returns -1 *
+ * for "*" and -2 for "*". *
*************************************************************************/
String im = tok.image ;
if (im.substring(1,2).equals("*")) {return -1;} ;
if (im.substring(1,2).equals("+")) {return -2;} ;
- return new Integer(im.substring(1, im.indexOf('>'))).intValue() ;
- /***********************************************************************
- * The ".intValue()" added by SZ because Java 1.4 doesn't support *
- * auto-boxing. *
+ return Integer.valueOf(im.substring(1, im.indexOf('>'))).intValue() ;
+ /***********************************************************************
+ * The ".intValue()" added by SZ because Java 1.4 doesn't support *
+ * auto-boxing. *
***********************************************************************/
}
-/***************************************************************************
-* The following method returns the canonical form of the step number *
-* contained in token t. This means that a "+" or "*" is replaced by the *
-* appropriate level number, and leading zeros are removed from a regular *
-* level number. *
+/***************************************************************************
+* The following method returns the canonical form of the step number *
+* contained in token t. This means that a "+" or "*" is replaced by the *
+* appropriate level number, and leading zeros are removed from a regular *
+* level number. *
***************************************************************************/
private UniqueString correctedStepNum(Token t) {
String str = t.image ;
@@ -841,12 +841,12 @@ private UniqueString correctedStepNum(Token t) {
|| str.substring(1,2).equals("+") ) {
int level = getProofLevel() ;
if ((level < 0) && (proofDepth > 0)) {
- /*********************************************************************
- * We've started a proof without yet determining the level number. *
- * Since this method is being called when encountering a step number *
- * token, this means we've encountered a step number inside a BY. So *
- * the actual level number to use here is the "previous" level *
- * number. *
+ /*********************************************************************
+ * We've started a proof without yet determining the level number. *
+ * Since this method is being called when encountering a step number *
+ * token, this means we've encountered a step number inside a BY. So *
+ * the actual level number to use here is the "previous" level *
+ * number. *
*********************************************************************/
level = proofLevelStack[proofDepth-1] ;
}
@@ -858,9 +858,9 @@ private UniqueString correctedStepNum(Token t) {
} ;
private void pushProofLevel() throws ParseException {
- /*************************************************************************
- * Called to begin the processing of a new proof level. It increments *
- * proofDepth and sets the proofLevelStack entry to -1. *
+ /*************************************************************************
+ * Called to begin the processing of a new proof level. It increments *
+ * proofDepth and sets the proofLevelStack entry to -1. *
*************************************************************************/
proofDepth++ ;
if (proofDepth >= MaxProofDepth) {
@@ -889,15 +889,15 @@ private int getProofLevel() {
return proofLevelStack[proofDepth]; }
private boolean beginsProof(Token tok) {
- /*************************************************************************
- * True iff the token tok begins a new proof--that is, iff it is either *
- * "BY", "PROOF", a step number that has a higher level than the current *
- * level, begins "<+>", or begins "<*>" and we are not inside a proof. *
+ /*************************************************************************
+ * True iff the token tok begins a new proof--that is, iff it is either *
+ * "BY", "PROOF", a step number that has a higher level than the current *
+ * level, begins "<+>", or begins "<*>" and we are not inside a proof. *
*************************************************************************/
String im = tok.image ;
if (im.length() < 2) {return false;}
- /***********************************************************************
- * This can happen if the user makes a weird error. *
+ /***********************************************************************
+ * This can happen if the user makes a weird error. *
***********************************************************************/
if (im.substring(1,2).equals("*")) {return (proofDepth < 0);} ;
@@ -916,31 +916,31 @@ private boolean beginsProof(Token tok) {
case OBVIOUS :
case OMITTED :
return true ;
- }; // switch
+ }; // switch
return false ;
}
private boolean correctLevel(Token tok) {
- /*************************************************************************
- * True iff tok is a correct proof step token for the current level of *
- * proof, where precedeByPROOF is true iff the proof is preceded by a *
- * "PROOF" token (needed in case this is the first step of the proof). *
- * If this is the first step being processed for current proof, then it *
- * sets the current proof level. *
+ /*************************************************************************
+ * True iff tok is a correct proof step token for the current level of *
+ * proof, where precedeByPROOF is true iff the proof is preceded by a *
+ * "PROOF" token (needed in case this is the first step of the proof). *
+ * If this is the first step being processed for current proof, then it *
+ * sets the current proof level. *
*************************************************************************/
int tokLevel = levelOfProofStepLexeme(tok) ;
- /*************************************************************************
- * Set lastDepth to the level of the containing proof, or -1 if this is *
- * the top-level proof. *
+ /*************************************************************************
+ * Set lastDepth to the level of the containing proof, or -1 if this is *
+ * the top-level proof. *
*************************************************************************/
int lastLevel = -1 ;
if (proofDepth > 0) {lastLevel = proofLevelStack[proofDepth-1] ;}
switch (tokLevel) {
case -1 :
- /*********************************************************************
- * tok is <*>... This is always legal because it can begin a proof *
- * iff it was preceded by a "PROOF". *
+ /*********************************************************************
+ * tok is <*>... This is always legal because it can begin a proof *
+ * iff it was preceded by a "PROOF". *
*********************************************************************/
if (proofLevelStack[proofDepth] < 0) {
proofLevelStack[proofDepth] = lastLevel + 1 ;
@@ -948,8 +948,8 @@ private boolean correctLevel(Token tok) {
return true ;
case -2 :
- /*********************************************************************
- * tok is <+>... This is legal iff it begins a proof. *
+ /*********************************************************************
+ * tok is <+>... This is legal iff it begins a proof. *
*********************************************************************/
if (proofLevelStack[proofDepth] < 0) {
proofLevelStack[proofDepth] = lastLevel + 1 ;
@@ -1009,9 +1009,9 @@ private boolean correctLevel(Token tok) {
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* NEPrefixOpToken and PrefixOpToken differ because the first includes *
-* "-." while the second contains does not. Neither includes "-". *
+/***************************************************************************
+* NEPrefixOpToken and PrefixOpToken differ because the first includes *
+* "-." while the second contains does not. Neither includes "-". *
***************************************************************************/
final public Token NEPrefixOpToken() throws ParseException {
Token t;
@@ -1684,8 +1684,8 @@ Token t;
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* Used to allow "STATE FUNCTION", "TEMPORAL", etc. *
+/***************************************************************************
+* Used to allow "STATE FUNCTION", "TEMPORAL", etc. *
***************************************************************************/
final public SyntaxTreeNode ParamSubDecl() throws ParseException {
SyntaxTreeNode tn, sn[];
@@ -1699,11 +1699,11 @@ Token t;
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* Recursive ::= <CONSTANT> ConstantDeclarationItems *
-* ( <COMMA> ConstantDeclarationItems )* *
-* *
-* Produces an N_Recursive node. *
+/***************************************************************************
+* Recursive ::= <CONSTANT> ConstantDeclarationItems *
+* ( <COMMA> ConstantDeclarationItems )* *
+* *
+* Produces an N_Recursive node. *
***************************************************************************/
final public SyntaxTreeNode Recursive() throws ParseException {
SyntaxTreeNode tn, sn[];
@@ -1948,13 +1948,13 @@ expecting = "_";
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* The following production OperatorOrFunctionDefinition() produces an *
-* N_OperatorDefinition, N_FunctionDefinition, or N_ModuleDefinition *
-* node. These nodes have syntax "[LOCAL] ...". The resulting node n *
-* has n.zero equal to null if the "LOCAL" is missing and equal to an *
-* array of length 1 containing the LOCAL token if it is present. The *
-* rest of the children/heirs of the node are in the array n.one. *
+/***************************************************************************
+* The following production OperatorOrFunctionDefinition() produces an *
+* N_OperatorDefinition, N_FunctionDefinition, or N_ModuleDefinition *
+* node. These nodes have syntax "[LOCAL] ...". The resulting node n *
+* has n.zero equal to null if the "LOCAL" is missing and equal to an *
+* array of length 1 containing the LOCAL token if it is present. The *
+* rest of the children/heirs of the node are in the array n.one. *
***************************************************************************/
final public SyntaxTreeNode OperatorOrFunctionDefinition() throws ParseException {
SyntaxTreeNode tn;
@@ -2543,9 +2543,9 @@ expecting = emptyString;
SyntaxTreeNode tn = null;
Token t;
anchor = null;
- /***********************************************************************
- * See the comments for the declaration of anchor to see what this is *
- * being used for. *
+ /***********************************************************************
+ * See the comments for the declaration of anchor to see what this is *
+ * being used for. *
***********************************************************************/
String n;
bpa("Substitution");
@@ -2695,24 +2695,24 @@ expecting = "Expression or Op. Symbol";
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* Substitution ::= *
-* ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp) *
-* <SUBSTITUTE> ( <op_76> | Lambda | Expression ) *
-* *
-* Note: <op_76> is "-.", the prefix - operator. *
-* <SUBSTITUTE> is "<-" *
-* *
-* Modified 27 March 2007 by LL to allow Lambda substitutions. *
+/***************************************************************************
+* Substitution ::= *
+* ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp) *
+* <SUBSTITUTE> ( <op_76> | Lambda | Expression ) *
+* *
+* Note: <op_76> is "-.", the prefix - operator. *
+* <SUBSTITUTE> is "<-" *
+* *
+* Modified 27 March 2007 by LL to allow Lambda substitutions. *
***************************************************************************/
final public SyntaxTreeNode OldSubstitution() throws ParseException {
SyntaxTreeNode zn[] = new SyntaxTreeNode[3];
SyntaxTreeNode tn = null;
Token t;
anchor = null;
- /***********************************************************************
- * See the comments for the declaration of anchor to see what this is *
- * being used for. *
+ /***********************************************************************
+ * See the comments for the declaration of anchor to see what this is *
+ * being used for. *
***********************************************************************/
String n;
bpa("Substitution");
@@ -2936,16 +2936,16 @@ epa();
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* Assumption ::= ( <ASSUME> | <ASSUMPTION> ) *
-* ( Identifier <DEF> )? Expression *
+/***************************************************************************
+* Assumption ::= ( <ASSUME> | <ASSUMPTION> ) *
+* ( Identifier <DEF> )? Expression *
***************************************************************************/
final public SyntaxTreeNode Assumption() throws ParseException {
SyntaxTreeNode tn;
SyntaxTreeNode zn = null;
Token t;
bpa("Assumption");
-// expecting = "LOCAL or ASSUM...";
+// expecting = "LOCAL or ASSUM...";
expecting = "ASSUM...";
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case ASSUMPTION:
@@ -2990,31 +2990,31 @@ expecting = "Expression";
}
final public SyntaxTreeNode AssumeProve() throws ParseException {
- /*************************************************************************
- * AssumeProve ::= (<IDENTIFIER> <COLONCOLON>)? *
- * (<ASSUME> | <BOXASSUME>) *
- * (AssumeProve | NewDecl | Expression) *
- * (<COMMA> (AssumeProve | NewDecl | Expression))+ *
- * (<PROVE> | <BOXPROVE>) Expression *
- * *
- * For ASSUME A1, A2 PROVE B, it constructs an AssumeProve node tn with *
- * tn.zero equal to the array containing the 6 elements *
- * *
- * "ASSUME" A1 "," A2 "PROVE" B *
- * *
- * If there is a label "foo::", it returns an N_Label node. *
- * *
- * Changed 18 May 2008 by LL to allow a label. *
- * *
- * Comment by LL on 25 May 2010: I don't understand this "label" *
- * business. Testing shows that an ASSUME/PROVE can't have a label. I *
- * have no idea what the code that apparently is looking for a label is *
- * supposed to do, but it never seems to do anything. *
- * *
- * The []ASSUME / []PROVE added by LL on 9 Feb 2011. This grammar *
- * allows []ASSUME and []PROVE to be used interchangably with ASSUME and *
- * PROVE. The semantic processing should report an error if []ASSUME is *
- * used with PROVE and vice-versa. *
+ /*************************************************************************
+ * AssumeProve ::= (<IDENTIFIER> <COLONCOLON>)? *
+ * (<ASSUME> | <BOXASSUME>) *
+ * (AssumeProve | NewDecl | Expression) *
+ * (<COMMA> (AssumeProve | NewDecl | Expression))+ *
+ * (<PROVE> | <BOXPROVE>) Expression *
+ * *
+ * For ASSUME A1, A2 PROVE B, it constructs an AssumeProve node tn with *
+ * tn.zero equal to the array containing the 6 elements *
+ * *
+ * "ASSUME" A1 "," A2 "PROVE" B *
+ * *
+ * If there is a label "foo::", it returns an N_Label node. *
+ * *
+ * Changed 18 May 2008 by LL to allow a label. *
+ * *
+ * Comment by LL on 25 May 2010: I don't understand this "label" *
+ * business. Testing shows that an ASSUME/PROVE can't have a label. I *
+ * have no idea what the code that apparently is looking for a label is *
+ * supposed to do, but it never seems to do anything. *
+ * *
+ * The []ASSUME / []PROVE added by LL on 9 Feb 2011. This grammar *
+ * allows []ASSUME and []PROVE to be used interchangably with ASSUME and *
+ * PROVE. The semantic processing should report an error if []ASSUME is *
+ * used with PROVE and vice-versa. *
*************************************************************************/
SyntaxTreeNode tn;
Token t;
@@ -3159,21 +3159,21 @@ expecting = "Expression";
}
final public SyntaxTreeNode NewSymb() throws ParseException {
- /*************************************************************************
- * NewSymb ::= (<NEW> | <CONSTANT> | <NEW> <CONSTANT>) *
- * (Identifier <IN> Expression | IdentDecl | SomeFixDecl) *
- * | [<NEW>] <VARIABLE> Identifier *
- * | [<NEW>] (<STATE> | <ACTION> | <TEMPORAL>) *
- * (IdentDecl | SomeFixDecl) *
+ /*************************************************************************
+ * NewSymb ::= (<NEW> | <CONSTANT> | <NEW> <CONSTANT>) *
+ * (Identifier <IN> Expression | IdentDecl | SomeFixDecl) *
+ * | [<NEW>] <VARIABLE> Identifier *
+ * | [<NEW>] (<STATE> | <ACTION> | <TEMPORAL>) *
+ * (IdentDecl | SomeFixDecl) *
*************************************************************************/
SyntaxTreeNode tn ;
Token t ;
boolean hasArgs ;
- /***********************************************************************
- * We want to allow "NEW Id \in S" but disallow "NEW Id(_) \in S". *
- * For simplicity, the we do this by letting javacc accept either, but *
- * set hasArgs to true in the latter case and report the error when we *
- * detect the "\in". *
+ /***********************************************************************
+ * We want to allow "NEW Id \in S" but disallow "NEW Id(_) \in S". *
+ * For simplicity, the we do this by letting javacc accept either, but *
+ * set hasArgs to true in the latter case and report the error when we *
+ * detect the "\in". *
***********************************************************************/
bpa( "NEW symbol declaration");
expecting = "NEW, CONSTANT, VARIABLE, STATE, ACTION, or TEMPORAL";
@@ -3327,50 +3327,50 @@ expecting = "Expression";
throw new Error("Missing return statement in function");
}
-// NumberedAssumeProve() commented out 5 Mar 2007 by LL
-// number . sequence
-// SyntaxTreeNode
-// NumberedAssumeProve () : {
-// SyntaxTreeNode tn;
-// Token t;
-// boolean b = false;
-// bpa("Numbered Assume-Prove");
-// }{
-// [ LOOKAHEAD(2)
-// t = <NUMBER_LITERAL> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "."; }
-// t = <DOT> {
-// BStack.newReference(t.endColumn, ASSUME); b = true;
-// addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "Assume-Prove, Assume-Decl or expression"; } ]
-// ( tn = AssumeProve()
-// | LOOKAHEAD( { IsNotExpression() } ) tn = AssumeDecl()
-// | tn = Expression() ) /* XXX parser confusion here !!! */
-// { if (b) BStack.popReference();
-// addHeir(tn);
-// SyntaxTreeNode sn[] = getLastHeirs();
-// epa(); return new SyntaxTreeNode( mn, N_NumberedAssumeProve, sn); }
-// }
-
-// AssumeDecl() commented out 27 March 2007; it seems to be left over
-// from the old proof grammar.
-// SyntaxTreeNode
-// AssumeDecl () : {
-// SyntaxTreeNode zn[] = null;
-// SyntaxTreeNode tn;
-// Token t;
-// bpa("Assume Decl.");
-// }{
-// ( tn = VariableDeclaration() { zn = new SyntaxTreeNode[1]; zn[0] = tn; }
-// | ( tn = ParamDeclaration() {
-// zn = new SyntaxTreeNode[2]; zn[0] = tn;
-// expecting = "optional \\in or ..."; }
-// zn[1] = MaybeBound() )
-// | LOOKAHEAD (2) tn = OperatorOrFunctionDefinition() { zn = new SyntaxTreeNode[1]; zn[0] = tn; }
-// | tn = Instance() { zn = new SyntaxTreeNode[1]; zn[0] = tn; } )
-// { epa();
-// return new SyntaxTreeNode( mn, N_AssumeDecl, zn ); }
-// }
+// NumberedAssumeProve() commented out 5 Mar 2007 by LL
+// number . sequence
+// SyntaxTreeNode
+// NumberedAssumeProve () : {
+// SyntaxTreeNode tn;
+// Token t;
+// boolean b = false;
+// bpa("Numbered Assume-Prove");
+// }{
+// [ LOOKAHEAD(2)
+// t = <NUMBER_LITERAL> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "."; }
+// t = <DOT> {
+// BStack.newReference(t.endColumn, ASSUME); b = true;
+// addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "Assume-Prove, Assume-Decl or expression"; } ]
+// ( tn = AssumeProve()
+// | LOOKAHEAD( { IsNotExpression() } ) tn = AssumeDecl()
+// | tn = Expression() ) /* XXX parser confusion here !!! */
+// { if (b) BStack.popReference();
+// addHeir(tn);
+// SyntaxTreeNode sn[] = getLastHeirs();
+// epa(); return new SyntaxTreeNode( mn, N_NumberedAssumeProve, sn); }
+// }
+
+// AssumeDecl() commented out 27 March 2007; it seems to be left over
+// from the old proof grammar.
+// SyntaxTreeNode
+// AssumeDecl () : {
+// SyntaxTreeNode zn[] = null;
+// SyntaxTreeNode tn;
+// Token t;
+// bpa("Assume Decl.");
+// }{
+// ( tn = VariableDeclaration() { zn = new SyntaxTreeNode[1]; zn[0] = tn; }
+// | ( tn = ParamDeclaration() {
+// zn = new SyntaxTreeNode[2]; zn[0] = tn;
+// expecting = "optional \\in or ..."; }
+// zn[1] = MaybeBound() )
+// | LOOKAHEAD (2) tn = OperatorOrFunctionDefinition() { zn = new SyntaxTreeNode[1]; zn[0] = tn; }
+// | tn = Instance() { zn = new SyntaxTreeNode[1]; zn[0] = tn; } )
+// { epa();
+// return new SyntaxTreeNode( mn, N_AssumeDecl, zn ); }
+// }
final public SyntaxTreeNode MaybeBound() throws ParseException {
SyntaxTreeNode zn[] = null;
SyntaxTreeNode tn;
@@ -3393,12 +3393,12 @@ expecting = "Expression";
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* Theorem ::= ( <THEOREM> | <PROPOSITION> ) *
-* ( Identifier <DEF> )? ( AssumeProve | Expression ) *
-* *
-* Produces a Theorem node tn with tn.zero containing 2 or 4 nodes, *
-* depending on whether or not the "Identifier <DEF>" is present. *
+/***************************************************************************
+* Theorem ::= ( <THEOREM> | <PROPOSITION> ) *
+* ( Identifier <DEF> )? ( AssumeProve | Expression ) *
+* *
+* Produces a Theorem node tn with tn.zero containing 2 or 4 nodes, *
+* depending on whether or not the "Identifier <DEF>" is present. *
***************************************************************************/
final public SyntaxTreeNode Theorem() throws ParseException {
SyntaxTreeNode tn;
@@ -3457,70 +3457,70 @@ expecting = "==";
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* The Grammar of Proofs *
-* XXXXXXX THIS IS OBSOLETE *
-* Proof ::= InnerProof *
-* // Proof checks that we're not inside a proof at the end. *
-* *
-* InnerProof ::= *
-* TerminalProof *
-* | (<PROOF>)? *
-* ( Step )* // Terminated by lookahead for "QED" *
-* QEDStep *
-* *
-* // Note: (InnerProof)? uses lookahead for beginsProof(...) *
-* *
-* TerminalProof ::= <BY> ... *
-* | (<PROOF>)? OBVIOUS *
-* QEDStep ::= (<ProofStepLexeme> | <ProofStepDotLexeme> )? *
-* <QED> (InnerProof)? *
-* *
-* Step ::= N_DefStep *
-* | N_UseOrHide *
-* | N_NonLocalInstance *
-* | N_NumerableStep *
-* | N_QEDStep *
-* *
-* NumerableStep == ExprStep *
-* | NumberedStep *
-* | UnnumberedStep *
-* *
-* DefStep ::= (<DEFINE>)? OperatorOrFunctionDefinition *
-* *
-* NumberedStep ::= (<ProofStepLexeme> | <ProofStepDotLexeme> ) *
-* UnnumberedStep *
-* *
-* ExprStep ::= ( <PROVE> *
-* | <SUFFICES> *
-* | (<ProofStepLexeme> | <ProofStepDotLexeme> ) *
-* (<SUFFICES>)? *
-* ) *
-* Expression *
-* *
-* UnnumberedStep ::= *
-* Have *
-* | Take *
-* | Witness *
-* | ( Pick *
-* | (<SUFFICES>)? (AssumeProve | <CASE> Expression) *
-* ) *
-* (InnerProof)? *
+/***************************************************************************
+* The Grammar of Proofs *
+* XXXXXXX THIS IS OBSOLETE *
+* Proof ::= InnerProof *
+* // Proof checks that we're not inside a proof at the end. *
+* *
+* InnerProof ::= *
+* TerminalProof *
+* | (<PROOF>)? *
+* ( Step )* // Terminated by lookahead for "QED" *
+* QEDStep *
+* *
+* // Note: (InnerProof)? uses lookahead for beginsProof(...) *
+* *
+* TerminalProof ::= <BY> ... *
+* | (<PROOF>)? OBVIOUS *
+* QEDStep ::= (<ProofStepLexeme> | <ProofStepDotLexeme> )? *
+* <QED> (InnerProof)? *
+* *
+* Step ::= N_DefStep *
+* | N_UseOrHide *
+* | N_NonLocalInstance *
+* | N_NumerableStep *
+* | N_QEDStep *
+* *
+* NumerableStep == ExprStep *
+* | NumberedStep *
+* | UnnumberedStep *
+* *
+* DefStep ::= (<DEFINE>)? OperatorOrFunctionDefinition *
+* *
+* NumberedStep ::= (<ProofStepLexeme> | <ProofStepDotLexeme> ) *
+* UnnumberedStep *
+* *
+* ExprStep ::= ( <PROVE> *
+* | <SUFFICES> *
+* | (<ProofStepLexeme> | <ProofStepDotLexeme> ) *
+* (<SUFFICES>)? *
+* ) *
+* Expression *
+* *
+* UnnumberedStep ::= *
+* Have *
+* | Take *
+* | Witness *
+* | ( Pick *
+* | (<SUFFICES>)? (AssumeProve | <CASE> Expression) *
+* ) *
+* (InnerProof)? *
***************************************************************************/
final public SyntaxTreeNode Proof() throws ParseException {
-/***************************************************************************
-* Returns an N_Proof or N_TerminalProof node. The heirs of an N_Proof *
-* node consist of an option PROOF token followed by a seequence of *
-* N_ProofStep nodes. The heirs of an N_ProofStep node are a StartStep() *
-* token, a statement body, and an optional proof. A statement body is *
-* one of the following node kinds: *
-* *
-* Have no proof: *
-* N_DefStep N_UseOrHide N_NonLocalInstance N_HaveStep, *
-* N_TakeStep N_WitnessStep *
-* *
-* Have a proof *
-* N_QEDStep N_PickStep N_CaseStep N_AssertStep *
+/***************************************************************************
+* Returns an N_Proof or N_TerminalProof node. The heirs of an N_Proof *
+* node consist of an option PROOF token followed by a seequence of *
+* N_ProofStep nodes. The heirs of an N_ProofStep node are a StartStep() *
+* token, a statement body, and an optional proof. A statement body is *
+* one of the following node kinds: *
+* *
+* Have no proof: *
+* N_DefStep N_UseOrHide N_NonLocalInstance N_HaveStep, *
+* N_TakeStep N_WitnessStep *
+* *
+* Have a proof *
+* N_QEDStep N_PickStep N_CaseStep N_AssertStep *
***************************************************************************/
SyntaxTreeNode tn;
Token t = null ;
@@ -3594,15 +3594,15 @@ expecting = "==";
}
final public SyntaxTreeNode UseOrHideOrBy() throws ParseException {
-/***************************************************************************
-* Returns an N_TerminalProof (for a BY) or N_UseOrHide node. Having *
-* one nonterminal that returns both is the only easy way I know to *
-* avoid having to duplicate the code for handling BY and for handling *
-* USE/HIDE. Lookahead should prevent it from being called to parse *
-* the wrong kind of object. *
-* *
-* Note: This production accepts a By, USE, or HIDE with no items. This *
-* should be reported by an error in the semantic analysis phase. *
+/***************************************************************************
+* Returns an N_TerminalProof (for a BY) or N_UseOrHide node. Having *
+* one nonterminal that returns both is the only easy way I know to *
+* avoid having to duplicate the code for handling BY and for handling *
+* USE/HIDE. Lookahead should prevent it from being called to parse *
+* the wrong kind of object. *
+* *
+* Note: This production accepts a By, USE, or HIDE with no items. This *
+* should be reported by an error in the semantic analysis phase. *
***************************************************************************/
SyntaxTreeNode tn;
Token t;
@@ -3809,8 +3809,8 @@ expecting = "==";
}
final public SyntaxTreeNode QEDStep() throws ParseException {
-/***************************************************************************
-* Returns an N_ProofStep node whose body is an N_QEDStep node. *
+/***************************************************************************
+* Returns an N_ProofStep node whose body is an N_QEDStep node. *
***************************************************************************/
Token t ;
SyntaxTreeNode tn;
@@ -3853,21 +3853,21 @@ expecting = "==";
}
final public SyntaxTreeNode Step() throws ParseException {
-/***************************************************************************
-* Returns an N_ProofStep node with the following heirs: *
-* *
-* - A StepStart() token. *
-* *
-* - An N_DefStep (for an operator or function def or named *
-* instantiation, N_UseOrHide, N_NonLocalInstance, N_HaveStep, *
-* N_TakeStep, N_WitnessStep, N_PickStep, N_CaseStep, or *
-* N_AssertStep node. (An N_AssertStep node has an optional *
-* "SUFFICES" followed by an expression or N_AssumeProve node.) *
-* *
-* - An optional N_Proof or N_TerminalProof node. *
-* *
-* Note: The grammar accepts a USE or HIDE with no items. This should *
-* be reported as an error in the semantic analysis phase. *
+/***************************************************************************
+* Returns an N_ProofStep node with the following heirs: *
+* *
+* - A StepStart() token. *
+* *
+* - An N_DefStep (for an operator or function def or named *
+* instantiation, N_UseOrHide, N_NonLocalInstance, N_HaveStep, *
+* N_TakeStep, N_WitnessStep, N_PickStep, N_CaseStep, or *
+* N_AssertStep node. (An N_AssertStep node has an optional *
+* "SUFFICES" followed by an expression or N_AssumeProve node.) *
+* *
+* - An optional N_Proof or N_TerminalProof node. *
+* *
+* Note: The grammar accepts a USE or HIDE with no items. This should *
+* be reported as an error in the semantic analysis phase. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -3950,10 +3950,10 @@ expecting = "==";
}
final public SyntaxTreeNode DefStep() throws ParseException {
-/***************************************************************************
-* Returns an N_DefStep node whose heirs begin with an optional <DEFINE> *
-* followed by a non-empty sequence of nodes returned by *
-* OperatorOrFunctionDefinition(). *
+/***************************************************************************
+* Returns an N_DefStep node whose heirs begin with an optional <DEFINE> *
+* followed by a non-empty sequence of nodes returned by *
+* OperatorOrFunctionDefinition(). *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -3984,9 +3984,9 @@ expecting = "==";
}
final public SyntaxTreeNode HaveStep() throws ParseException {
-/***************************************************************************
-* Returns an N_HaveStep node whose heirs are a <HAVE> token and an *
-* expression node. *
+/***************************************************************************
+* Returns an N_HaveStep node whose heirs are a <HAVE> token and an *
+* expression node. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -4003,10 +4003,10 @@ expecting = "==";
}
final public SyntaxTreeNode TakeStep() throws ParseException {
-/***************************************************************************
-* Returns an N_TakeStep node whose first heir is a <TAKE> token and whose *
-* remaining heirs are a sequence of QuantBound() nodes or a sequence of *
-* identifiers. *
+/***************************************************************************
+* Returns an N_TakeStep node whose first heir is a <TAKE> token and whose *
+* remaining heirs are a sequence of QuantBound() nodes or a sequence of *
+* identifiers. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -4072,11 +4072,11 @@ expecting = "==";
}
final public SyntaxTreeNode WitnessStep() throws ParseException {
-/***************************************************************************
-* Returns an N_WitnessStep node whose heirs are a <WITNESS> token and a *
-* sequence of expression nodes. It's up to later processing to decide if *
-* those expressions have the form <<expr, ... , expr>> \in expr, *
-* expr \in expr, or just expr. *
+/***************************************************************************
+* Returns an N_WitnessStep node whose heirs are a <WITNESS> token and a *
+* sequence of expression nodes. It's up to later processing to decide if *
+* those expressions have the form <<expr, ... , expr>> \in expr, *
+* expr \in expr, or just expr. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -4110,9 +4110,9 @@ expecting = "==";
}
final public SyntaxTreeNode PickStep() throws ParseException {
-/***************************************************************************
-* Returns an N_PickStep node whose heirs are a <PICK> token and an *
-* expression node. *
+/***************************************************************************
+* Returns an N_PickStep node whose heirs are a <PICK> token and an *
+* expression node. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -4185,9 +4185,9 @@ expecting = "==";
}
final public SyntaxTreeNode CaseStep() throws ParseException {
-/***************************************************************************
-* Returns an N_CaseStep node whose heirs are a <CASE> token and an *
-* expression node. *
+/***************************************************************************
+* Returns an N_CaseStep node whose heirs are a <CASE> token and an *
+* expression node. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -4204,9 +4204,9 @@ expecting = "==";
}
final public SyntaxTreeNode AssertStep() throws ParseException {
-/***************************************************************************
-* Returns an N_AssertStep node whose heirs are an optional <SUFFICES> *
-* token and an expression or N_AssumeProve node. *
+/***************************************************************************
+* Returns an N_AssertStep node whose heirs are an optional <SUFFICES> *
+* token and an expression or N_AssumeProve node. *
***************************************************************************/
Token t = null;
SyntaxTreeNode tn = null;
@@ -4236,181 +4236,181 @@ expecting = "==";
throw new Error("Missing return statement in function");
}
-// SyntaxTreeNode
-// NumerableStep() : {
-// /***************************************************************************
-// * Returns an N_NumerableStep node, which has the syntax *
-// * *
-// * ( <ProofStep[Dot]Lexeme> (N_NonExprBody node) *
-// * | N_NonExprBody node ) *
-// * ( N_Proof node | N_TerminalProof node)? *
-// ***************************************************************************/
-// Token t = null;
-// SyntaxTreeNode tn = null;
-// boolean mayHaveProof = true ;
-// bpa("NumerableStep") ;
-// }{( LOOKAHEAD(2)
-// (t = <ProofStepLexeme> | t = <ProofStepDotLexeme>)
-// { tn = new SyntaxTreeNode(mn, t) ;
-// addHeir(tn);
-// if ((proofDepth > 0) && (proofLevelStack[proofDepth-1] == -1)){
-// throw new ParseException(tn.getLocation() +
-// ": numbered step inside unnumbered proof.");
-// } ;
-// if (!correctLevel(t)) {
-// throw new ParseException(tn.getLocation() +
-// ": step number has incorrect level.");
-// } ;
-// }
-// ( (t = <CASE> {addHeir(new SyntaxTreeNode(mn, t)); })? // XXXX
-// // ^^^^^^^^^^^
-// // javacc generates the following warning here:
-// // Choice conflict in [...] construct at line 2700, column 8.
-// // Expansion nested within construct and expansion following construct
-// // have common prefixes, one of which is: "CASE"
-// // Consider using a lookahead of 2 or more for nested expansion.
-// //
-// // This conflict is between "<1>2. CASE expr" and
-// // "<1>2. CASE p -> ...". This is an inherent ambiguity that arises
-// // from the use of "CASE" as a keyword here. Javacc resolves
-// // conflicts by choosing the first successful match. Here, this
-// // means that "<1>2. CASE p -> ..." is parsed as
-// //
-// // <ProofStepDotLexeme> <CASE> Expression()
-// //
-// // causing an error when it tries to parse "-> ..." as an expression.
-//
-//
-//
-// tn = Expression() {addHeir(tn); // XXXX
-// mayHaveProof = true ;} // XXXX
-// | // XXXX
-// tn = NonExprBody() {addHeir(tn);
-// mayHaveProof = nonExprBodyMayHaveProof;}
-// ) // XXXX
-// | t = <CASE> {addHeir(new SyntaxTreeNode(mn, t)); } // XXXX
-// tn = Expression() {addHeir(tn); // XXXX
-// mayHaveProof = nonExprBodyMayHaveProof;} // XXXX
-//
-// | tn = NonExprBody()
-// { addHeir(tn);
-// mayHaveProof = nonExprBodyMayHaveProof;
-// if (getProofLevel() == -2)
-// { setProofLevel(-1) ;
-// }
-// else {
-// if (getProofLevel() != -1) {
-// throw new ParseException(tn.getLocation() +
-// ": Unnumbered step in numbered proof.");
-// }
-// }
-// }
-// )
-// ( LOOKAHEAD( {mayHaveProof && beginsProof(getToken(1))} )
-// tn = Proof()
-// { addHeir(tn) ; }
-// )?
-// { SyntaxTreeNode sn[] = getLastHeirs();
-// epa();
-// return new SyntaxTreeNode(mn, N_NumerableStep, sn);
-// }
-// }
-
-// /***************************************************************************
-// * Hack: In addition to returning a node, NonExprBody() needs to return a *
-// * boolean saying whether or not the statement it is returning can have a *
-// * proof. It does this by setting the field nonExprBodyMayHaveProof. *
-// ***************************************************************************/
-// SyntaxTreeNode
-// NonExprBody() : {
-// SyntaxTreeNode tn = null;
-// Token t = null;
-// nonExprBodyMayHaveProof = false ;
-// bpa("NonExprBody") ;
-// }{ ( LOOKAHEAD(2)
-// (t = <SUFFICES> { addHeir(new SyntaxTreeNode(mn, t)); }) ?
-// tn = AssumeProve() { addHeir(tn) ;
-// nonExprBodyMayHaveProof = true;}
-// | LOOKAHEAD(2)
-// ( t = <PROVE> | t = <SUFFICES>) // | t = <PROOFCASE>
-// { addHeir(new SyntaxTreeNode(mn, t));
-// expecting = "expression";}
-// tn = Expression() { addHeir(tn) ;
-// nonExprBodyMayHaveProof = true;}
-// | t = <HAVE> { addHeir(new SyntaxTreeNode(mn, t)) ;
-// expecting = "expression";}
-// tn = Expression() { addHeir(tn) ; }
-// | t = <TAKE> { addHeir(new SyntaxTreeNode(mn, t)) ;
-// expecting = "identifier";}
-// ( LOOKAHEAD ( <IDENTIFIER> (<COMMA> <IDENTIFIER>)* <IN>
-// | <LAB>)
-// tn = QuantBound() { addHeir(tn) ;
-// expecting = "comma or step";}
-// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "identifier or tuple of identifiers";}
-// tn = QuantBound() { addHeir(tn) ;
-// expecting = "comma or proof step";}
-// )*
-// |
-// tn = Identifier() { addHeir(tn) ;
-// expecting = "comma or proof step";}
-// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "identifier";}
-// tn = Identifier() { addHeir(tn) ;
-// expecting = "comma or proof step";}
-// )*
-// )
-//
-// | t = <WITNESS> { addHeir(new SyntaxTreeNode(mn, t)) ;
-// expecting = "expression";}
-// tn = Expression() { addHeir(tn) ; }
-// /*********************************************************************
-// * Note: The semantic phase must determine if this is expr \in expr, *
-// * or <<expr, ... , expr>> \in expr, or just expr. *
-// *********************************************************************/
-// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "expression";}
-// tn = Expression() { addHeir(tn) ;
-// expecting = "comma or colon";}
-// )*
-//
-// | t = <PICK> { addHeir(new SyntaxTreeNode(mn, t)) ;
-// expecting = "identifier";}
-// ( LOOKAHEAD ( <IDENTIFIER> ( <COMMA> <IDENTIFIER> )* <COLON> )
-// /* CommaList Identifier */
-// tn = Identifier() { addHeir(tn) ;
-// expecting = "comma, or colon";}
-// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "identifier";}
-// tn = Identifier() { addHeir(tn) ;
-// expecting = "comma or colon";}
-// )*
-// |
-// tn = QuantBound() { addHeir(tn) ;
-// expecting = "comma or colon";}
-// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "identifier or tuple of identifiers";}
-// tn = QuantBound() { addHeir(tn) ;
-// expecting = "comma or colon";}
-// )*
-// )
-// t = <COLON> { addHeir( new SyntaxTreeNode(mn, t) );
-// expecting = "expression";}
-// tn = Expression() { addHeir(tn) ; }
-// { nonExprBodyMayHaveProof = true;}
-// )
-// { SyntaxTreeNode sn[] = getLastHeirs();
-// epa();
-// return new SyntaxTreeNode(mn, N_NonExprBody, sn);
-// }
-// }
-
-
-
-/***************************************************************************
-* The GeneralId() production is not used and can be deleted. The parser *
-* uses Java code to construct N_GeneralId nodes inside Extension(), *
-* NoOpExtension(), and BraceCases() *
+// SyntaxTreeNode
+// NumerableStep() : {
+// /***************************************************************************
+// * Returns an N_NumerableStep node, which has the syntax *
+// * *
+// * ( <ProofStep[Dot]Lexeme> (N_NonExprBody node) *
+// * | N_NonExprBody node ) *
+// * ( N_Proof node | N_TerminalProof node)? *
+// ***************************************************************************/
+// Token t = null;
+// SyntaxTreeNode tn = null;
+// boolean mayHaveProof = true ;
+// bpa("NumerableStep") ;
+// }{( LOOKAHEAD(2)
+// (t = <ProofStepLexeme> | t = <ProofStepDotLexeme>)
+// { tn = new SyntaxTreeNode(mn, t) ;
+// addHeir(tn);
+// if ((proofDepth > 0) && (proofLevelStack[proofDepth-1] == -1)){
+// throw new ParseException(tn.getLocation() +
+// ": numbered step inside unnumbered proof.");
+// } ;
+// if (!correctLevel(t)) {
+// throw new ParseException(tn.getLocation() +
+// ": step number has incorrect level.");
+// } ;
+// }
+// ( (t = <CASE> {addHeir(new SyntaxTreeNode(mn, t)); })? // XXXX
+// // ^^^^^^^^^^^
+// // javacc generates the following warning here:
+// // Choice conflict in [...] construct at line 2700, column 8.
+// // Expansion nested within construct and expansion following construct
+// // have common prefixes, one of which is: "CASE"
+// // Consider using a lookahead of 2 or more for nested expansion.
+// //
+// // This conflict is between "<1>2. CASE expr" and
+// // "<1>2. CASE p -> ...". This is an inherent ambiguity that arises
+// // from the use of "CASE" as a keyword here. Javacc resolves
+// // conflicts by choosing the first successful match. Here, this
+// // means that "<1>2. CASE p -> ..." is parsed as
+// //
+// // <ProofStepDotLexeme> <CASE> Expression()
+// //
+// // causing an error when it tries to parse "-> ..." as an expression.
+//
+//
+//
+// tn = Expression() {addHeir(tn); // XXXX
+// mayHaveProof = true ;} // XXXX
+// | // XXXX
+// tn = NonExprBody() {addHeir(tn);
+// mayHaveProof = nonExprBodyMayHaveProof;}
+// ) // XXXX
+// | t = <CASE> {addHeir(new SyntaxTreeNode(mn, t)); } // XXXX
+// tn = Expression() {addHeir(tn); // XXXX
+// mayHaveProof = nonExprBodyMayHaveProof;} // XXXX
+//
+// | tn = NonExprBody()
+// { addHeir(tn);
+// mayHaveProof = nonExprBodyMayHaveProof;
+// if (getProofLevel() == -2)
+// { setProofLevel(-1) ;
+// }
+// else {
+// if (getProofLevel() != -1) {
+// throw new ParseException(tn.getLocation() +
+// ": Unnumbered step in numbered proof.");
+// }
+// }
+// }
+// )
+// ( LOOKAHEAD( {mayHaveProof && beginsProof(getToken(1))} )
+// tn = Proof()
+// { addHeir(tn) ; }
+// )?
+// { SyntaxTreeNode sn[] = getLastHeirs();
+// epa();
+// return new SyntaxTreeNode(mn, N_NumerableStep, sn);
+// }
+// }
+
+// /***************************************************************************
+// * Hack: In addition to returning a node, NonExprBody() needs to return a *
+// * boolean saying whether or not the statement it is returning can have a *
+// * proof. It does this by setting the field nonExprBodyMayHaveProof. *
+// ***************************************************************************/
+// SyntaxTreeNode
+// NonExprBody() : {
+// SyntaxTreeNode tn = null;
+// Token t = null;
+// nonExprBodyMayHaveProof = false ;
+// bpa("NonExprBody") ;
+// }{ ( LOOKAHEAD(2)
+// (t = <SUFFICES> { addHeir(new SyntaxTreeNode(mn, t)); }) ?
+// tn = AssumeProve() { addHeir(tn) ;
+// nonExprBodyMayHaveProof = true;}
+// | LOOKAHEAD(2)
+// ( t = <PROVE> | t = <SUFFICES>) // | t = <PROOFCASE>
+// { addHeir(new SyntaxTreeNode(mn, t));
+// expecting = "expression";}
+// tn = Expression() { addHeir(tn) ;
+// nonExprBodyMayHaveProof = true;}
+// | t = <HAVE> { addHeir(new SyntaxTreeNode(mn, t)) ;
+// expecting = "expression";}
+// tn = Expression() { addHeir(tn) ; }
+// | t = <TAKE> { addHeir(new SyntaxTreeNode(mn, t)) ;
+// expecting = "identifier";}
+// ( LOOKAHEAD ( <IDENTIFIER> (<COMMA> <IDENTIFIER>)* <IN>
+// | <LAB>)
+// tn = QuantBound() { addHeir(tn) ;
+// expecting = "comma or step";}
+// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "identifier or tuple of identifiers";}
+// tn = QuantBound() { addHeir(tn) ;
+// expecting = "comma or proof step";}
+// )*
+// |
+// tn = Identifier() { addHeir(tn) ;
+// expecting = "comma or proof step";}
+// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "identifier";}
+// tn = Identifier() { addHeir(tn) ;
+// expecting = "comma or proof step";}
+// )*
+// )
+//
+// | t = <WITNESS> { addHeir(new SyntaxTreeNode(mn, t)) ;
+// expecting = "expression";}
+// tn = Expression() { addHeir(tn) ; }
+// /*********************************************************************
+// * Note: The semantic phase must determine if this is expr \in expr, *
+// * or <<expr, ... , expr>> \in expr, or just expr. *
+// *********************************************************************/
+// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "expression";}
+// tn = Expression() { addHeir(tn) ;
+// expecting = "comma or colon";}
+// )*
+//
+// | t = <PICK> { addHeir(new SyntaxTreeNode(mn, t)) ;
+// expecting = "identifier";}
+// ( LOOKAHEAD ( <IDENTIFIER> ( <COMMA> <IDENTIFIER> )* <COLON> )
+// /* CommaList Identifier */
+// tn = Identifier() { addHeir(tn) ;
+// expecting = "comma, or colon";}
+// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "identifier";}
+// tn = Identifier() { addHeir(tn) ;
+// expecting = "comma or colon";}
+// )*
+// |
+// tn = QuantBound() { addHeir(tn) ;
+// expecting = "comma or colon";}
+// ( t = <COMMA> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "identifier or tuple of identifiers";}
+// tn = QuantBound() { addHeir(tn) ;
+// expecting = "comma or colon";}
+// )*
+// )
+// t = <COLON> { addHeir( new SyntaxTreeNode(mn, t) );
+// expecting = "expression";}
+// tn = Expression() { addHeir(tn) ; }
+// { nonExprBodyMayHaveProof = true;}
+// )
+// { SyntaxTreeNode sn[] = getLastHeirs();
+// epa();
+// return new SyntaxTreeNode(mn, N_NonExprBody, sn);
+// }
+// }
+
+
+
+/***************************************************************************
+* The GeneralId() production is not used and can be deleted. The parser *
+* uses Java code to construct N_GeneralId nodes inside Extension(), *
+* NoOpExtension(), and BraceCases() *
***************************************************************************/
final public SyntaxTreeNode GeneralId() throws ParseException {
SyntaxTreeNode zn[] = new SyntaxTreeNode[2];
@@ -4636,8 +4636,8 @@ expecting = "==";
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* The following does not seem to be used anywhere. *
+/***************************************************************************
+* The following does not seem to be used anywhere. *
***************************************************************************/
final public SyntaxTreeNode ClosedExpressionOnly() throws ParseException {
SyntaxTreeNode tn;
@@ -4679,8 +4679,8 @@ expecting = "==";
throw new Error("Missing return statement in function");
}
-/*
- L.GeneralId, L.OpApplication, L.String, L.Number, L.GenOp...
+/*
+ L.GeneralId, L.OpApplication, L.String, L.Number, L.GenOp...
*/
final public SyntaxTreeNode ElementaryExpression() throws ParseException {
SyntaxTreeNode tn;
@@ -5071,7 +5071,7 @@ expecting = "==";
}
final public SyntaxTreeNode OpArgs() throws ParseException {
- // OpSuite contributes to Heir list.
+ // OpSuite contributes to Heir list.
SyntaxTreeNode tn;
Token t;
bpa("Optional Arguments");
@@ -5099,91 +5099,91 @@ expecting = "==";
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* OpOrExpr ::= (NonExpPrefixOp | InfixOp | PostfixOp) *
-* followed by *
-* "," | ")" | <DEFBREAK> | "LOCAL" | "INSTANCE" | *
-* "THEOREM" | "ASSUME" | "ASSUMPTION" | *
-* "CONSTANT" | "VARIABLE" | "RECURSIVE" | *
-* <END_MODULE> | <SEPARATOR> | <BEGIN_MODULE> *
-* | Lambda *
-* | Expression *
-* *
-* This production is called where either an operator or an expression is *
-* expected--which is either as the argument of an operator or in a *
-* substitution. For an expression or an operator argument that's a *
-* LAMBDA expression, there's no problem. However, something like Foo!Bar *
-* could be either an expression or an operator. In TLA+2, something like *
-* Foo!+!Bar could only be an operator, while something like *
-* Foo!+(a,b)!Bar could only be an expression. However, in order to *
-* minimize the changes from the TLA+1 parser, we represent both Foo!+!Bar *
-* and Foo!+(a,b)!Bar as a GeneralId node and leave it to the semantic *
-* processing to sort things out. Thus, Foo!+(a,b)!Bar produces the *
-* folowing tree of SyntaxTreeNode objects: *
-* *
-* N_GeneralId *
-* _.N_IdPrefix *
-* _._.N_IdPrefixElement *
-* _._._.IDENTIFIER "Foo" *
-* _._._.BANG "!" *
-* _._.N_IdPrefixElement *
-* _._._.N_InfixOp + *
-* _._._.N_OpArgs *
-* _._._._.LBR "(" *
-* _._._._.whatever a produces *
-* _._._._.COMMA "," *
-* _._._._.whatever b produces *
-* _._._._.RBR ")" *
-* _._._.BANG "!" *
-* _.IDENTIFIER "Bar" *
-* *
-* Something like Foo!+(a,b)!Bar(x) producs an N_OpApplication node *
-* whose first child is the N_GeneralId node above and whose second *
-* child is an N_OpArgs node. *
-* *
-* TLA+2 adds labels and structural operators like "<<" to this kind of *
-* operator or expression. A label in such an expression looks just like *
-* an ordinary identifier. A structural operator is represented by a *
-* token with the new kind "N_StructOp". Such a node is created by *
-* *
-* new SynaxTreeNode(moduleName, N_StructOp, node) *
-* *
-* where node is created by either *
-* *
-* new SyntaxTreeNode(moduleName, tok) *
-* *
-* where tok is "<<", ">>", "@", or ":", or by *
-* *
-* new SynaxTreeNode(moduleName, N_Number, ...) *
-* *
-* for a <NUMBER_LITERAL> token. *
-* *
-* Let OpArgs = (arg_1, ... , arg_k). In general, there are three *
-* interesting classes of expressions of the form e_1!e_2!...!e_n. *
-* *
-* Case 1: e_n = tok OpArgs, *
-* where tok is an Identifier or an In/Pre/PostfixOp. *
-* In this case an OpApplication node is produced with two children: *
-* - An N_GeneralId node with children *
-* - An N_IdPrefixNode with n-1 children consisting N_IdPRefixElement *
-* nodes for e_1!, ... , e_n-1!. *
-* - A node of kind IDENTIFIER, N_PrefixOp, etc. for tok *
-* - An N_OpArgs nodes obtained from OpArgs *
-* *
-* Case 2: e_n = tok *
-* where tok is an Identifier or an In/Pre/PostfixOp. *
-* In this case, it produces just the N_GeneralId node of Case 1 *
-* *
-* Case 3: e_n = OpArgs *
-* In this case, a GeneralId node is produced with two children: *
-* - The N_IdPrefixNode node produced in cases 1 and 2 *
-* - An N_OpArgs node for OpArgs. *
+/***************************************************************************
+* OpOrExpr ::= (NonExpPrefixOp | InfixOp | PostfixOp) *
+* followed by *
+* "," | ")" | <DEFBREAK> | "LOCAL" | "INSTANCE" | *
+* "THEOREM" | "ASSUME" | "ASSUMPTION" | *
+* "CONSTANT" | "VARIABLE" | "RECURSIVE" | *
+* <END_MODULE> | <SEPARATOR> | <BEGIN_MODULE> *
+* | Lambda *
+* | Expression *
+* *
+* This production is called where either an operator or an expression is *
+* expected--which is either as the argument of an operator or in a *
+* substitution. For an expression or an operator argument that's a *
+* LAMBDA expression, there's no problem. However, something like Foo!Bar *
+* could be either an expression or an operator. In TLA+2, something like *
+* Foo!+!Bar could only be an operator, while something like *
+* Foo!+(a,b)!Bar could only be an expression. However, in order to *
+* minimize the changes from the TLA+1 parser, we represent both Foo!+!Bar *
+* and Foo!+(a,b)!Bar as a GeneralId node and leave it to the semantic *
+* processing to sort things out. Thus, Foo!+(a,b)!Bar produces the *
+* folowing tree of SyntaxTreeNode objects: *
+* *
+* N_GeneralId *
+* _.N_IdPrefix *
+* _._.N_IdPrefixElement *
+* _._._.IDENTIFIER "Foo" *
+* _._._.BANG "!" *
+* _._.N_IdPrefixElement *
+* _._._.N_InfixOp + *
+* _._._.N_OpArgs *
+* _._._._.LBR "(" *
+* _._._._.whatever a produces *
+* _._._._.COMMA "," *
+* _._._._.whatever b produces *
+* _._._._.RBR ")" *
+* _._._.BANG "!" *
+* _.IDENTIFIER "Bar" *
+* *
+* Something like Foo!+(a,b)!Bar(x) producs an N_OpApplication node *
+* whose first child is the N_GeneralId node above and whose second *
+* child is an N_OpArgs node. *
+* *
+* TLA+2 adds labels and structural operators like "<<" to this kind of *
+* operator or expression. A label in such an expression looks just like *
+* an ordinary identifier. A structural operator is represented by a *
+* token with the new kind "N_StructOp". Such a node is created by *
+* *
+* new SynaxTreeNode(moduleName, N_StructOp, node) *
+* *
+* where node is created by either *
+* *
+* new SyntaxTreeNode(moduleName, tok) *
+* *
+* where tok is "<<", ">>", "@", or ":", or by *
+* *
+* new SynaxTreeNode(moduleName, N_Number, ...) *
+* *
+* for a <NUMBER_LITERAL> token. *
+* *
+* Let OpArgs = (arg_1, ... , arg_k). In general, there are three *
+* interesting classes of expressions of the form e_1!e_2!...!e_n. *
+* *
+* Case 1: e_n = tok OpArgs, *
+* where tok is an Identifier or an In/Pre/PostfixOp. *
+* In this case an OpApplication node is produced with two children: *
+* - An N_GeneralId node with children *
+* - An N_IdPrefixNode with n-1 children consisting N_IdPRefixElement *
+* nodes for e_1!, ... , e_n-1!. *
+* - A node of kind IDENTIFIER, N_PrefixOp, etc. for tok *
+* - An N_OpArgs nodes obtained from OpArgs *
+* *
+* Case 2: e_n = tok *
+* where tok is an Identifier or an In/Pre/PostfixOp. *
+* In this case, it produces just the N_GeneralId node of Case 1 *
+* *
+* Case 3: e_n = OpArgs *
+* In this case, a GeneralId node is produced with two children: *
+* - The N_IdPrefixNode node produced in cases 1 and 2 *
+* - An N_OpArgs node for OpArgs. *
***************************************************************************/
final public SyntaxTreeNode OpOrExpr() throws ParseException {
- /*************************************************************************
- * Used for parsing an operator argument or the right-hand side of a *
- * substitution, which could be either an operator (like +) or an *
- * expression (like a+b). *
+ /*************************************************************************
+ * Used for parsing an operator argument or the right-hand side of a *
+ * substitution, which could be either an operator (like +) or an *
+ * expression (like a+b). *
*************************************************************************/
SyntaxTreeNode tn;
int kind ;
@@ -5355,62 +5355,62 @@ SyntaxTreeNode tn;
addHeir(tn);
}
- // OpSuite
-
-
-// void /* nodes are linked internally here : no value returned */
-// oldOpSuite() : {
-// SyntaxTreeNode tn = null;
-// anchor = null;
-// /***********************************************************************
-// * See the comments for the declaration of anchor to see what this is *
-// * being used for. *
-// ***********************************************************************/
-// Token t;
-// } {
-// ( /***********************************************************************
-// * This handles the operator argument "-." (token op_76) *
-// ***********************************************************************/
-// // XXXXX -- this won't work with the new expression syntax.
-// t = <op_76> {
-// tn = new SyntaxTreeNode(mn, N_NonExpPrefixOp, t);
-// SyntaxTreeNode heirs[] = new SyntaxTreeNode[2];
-// heirs[0] = new SyntaxTreeNode( mn, N_IdPrefix, ( SyntaxTreeNode []) null );
-// heirs[1] = tn;
-// tn = new SyntaxTreeNode( mn, N_GenNonExpPrefixOp, heirs ); }
-// | LOOKAHEAD( (<AND> | <OR>) (<COMMA>|<RBR>) )
-// tn = InfixOp() {
-// heirs = new SyntaxTreeNode[2];
-// heirs[0] = new SyntaxTreeNode( mn, N_IdPrefix, (SyntaxTreeNode []) null );
-// heirs[1] = tn;
-// tn = new SyntaxTreeNode( mn, N_GenInfixOp, heirs );
-// }
-// | tn = Lambda()
-// | try {
-// tn = Expression()
-// } catch ( ParseException e ) {
-// // ToolIO.out.println("Caught exception (bis)");
-// // first things first - restore evaluation stack
-// if ( OperatorStack.isWellReduced() )
-// OperatorStack.popStack();
-// else
-// throw e;
-// /* it wasn't an expression, what was it ? */
-// /* check the nature of the node returned. It can only be a prefixed op. */
-// if ( ( anchor != null )
-// &&( anchor.isKind( N_GenPrefixOp )
-// || anchor.isKind( N_GenInfixOp )
-// || anchor.isKind( N_GenPostfixOp ) ) ) {tn = anchor; anchor = null;
-// } else {
-// // ToolIO.out.println("anchor is " + anchor.toString());
-// throw e;
-// } // end else
-// } // end catch.
-// )
-// /* it wasn't an expression, what was it ? L.GenNonExpPrefixOp | L.GenInfixOp | L.GenPostfixOp */
-// /* check the nature of the node returned . Below Expression, it has to be a prefixed op. */
-// { addHeir( tn ); }
-// }
+ // OpSuite
+
+
+// void /* nodes are linked internally here : no value returned */
+// oldOpSuite() : {
+// SyntaxTreeNode tn = null;
+// anchor = null;
+// /***********************************************************************
+// * See the comments for the declaration of anchor to see what this is *
+// * being used for. *
+// ***********************************************************************/
+// Token t;
+// } {
+// ( /***********************************************************************
+// * This handles the operator argument "-." (token op_76) *
+// ***********************************************************************/
+// // XXXXX -- this won't work with the new expression syntax.
+// t = <op_76> {
+// tn = new SyntaxTreeNode(mn, N_NonExpPrefixOp, t);
+// SyntaxTreeNode heirs[] = new SyntaxTreeNode[2];
+// heirs[0] = new SyntaxTreeNode( mn, N_IdPrefix, ( SyntaxTreeNode []) null );
+// heirs[1] = tn;
+// tn = new SyntaxTreeNode( mn, N_GenNonExpPrefixOp, heirs ); }
+// | LOOKAHEAD( (<AND> | <OR>) (<COMMA>|<RBR>) )
+// tn = InfixOp() {
+// heirs = new SyntaxTreeNode[2];
+// heirs[0] = new SyntaxTreeNode( mn, N_IdPrefix, (SyntaxTreeNode []) null );
+// heirs[1] = tn;
+// tn = new SyntaxTreeNode( mn, N_GenInfixOp, heirs );
+// }
+// | tn = Lambda()
+// | try {
+// tn = Expression()
+// } catch ( ParseException e ) {
+// // ToolIO.out.println("Caught exception (bis)");
+// // first things first - restore evaluation stack
+// if ( OperatorStack.isWellReduced() )
+// OperatorStack.popStack();
+// else
+// throw e;
+// /* it wasn't an expression, what was it ? */
+// /* check the nature of the node returned. It can only be a prefixed op. */
+// if ( ( anchor != null )
+// &&( anchor.isKind( N_GenPrefixOp )
+// || anchor.isKind( N_GenInfixOp )
+// || anchor.isKind( N_GenPostfixOp ) ) ) {tn = anchor; anchor = null;
+// } else {
+// // ToolIO.out.println("anchor is " + anchor.toString());
+// throw e;
+// } // end else
+// } // end catch.
+// )
+// /* it wasn't an expression, what was it ? L.GenNonExpPrefixOp | L.GenInfixOp | L.GenPostfixOp */
+// /* check the nature of the node returned . Below Expression, it has to be a prefixed op. */
+// { addHeir( tn ); }
+// }
final public SyntaxTreeNode ParenExpr() throws ParseException {
SyntaxTreeNode zn[] = new SyntaxTreeNode[3];
SyntaxTreeNode tn;
@@ -5588,13 +5588,13 @@ SyntaxTreeNode tn;
}
final public SyntaxTreeNode BraceCases() throws ParseException {
- int kind = N_SetEnumerate; // set by default.
+ int kind = N_SetEnumerate; // set by default.
SyntaxTreeNode tn, tn_0, tn_1, tn_2, htn = null;
Token t;
boolean te = false;
- /***********************************************************************
- * The value of te is set in a couple of places, but it is never *
- * read. J-Ch hopes it's obsolete. *
+ /***********************************************************************
+ * The value of te is set in a couple of places, but it is never *
+ * read. J-Ch hopes it's obsolete. *
***********************************************************************/
bpa("Some { } form");
t = jj_consume_token(LBC);
@@ -6114,9 +6114,9 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* The SetExcept non-terminal was eliminated from the grammar, but not *
-* from the parser. *
+/***************************************************************************
+* The SetExcept non-terminal was eliminated from the grammar, but not *
+* from the parser. *
***************************************************************************/
final public SyntaxTreeNode SetExcept() throws ParseException {
SyntaxTreeNode tn;
@@ -6229,7 +6229,7 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-// new SyntaxTreeNode( N_IdPrefix ) ???
+// new SyntaxTreeNode( N_IdPrefix ) ???
final public SyntaxTreeNode NoOpExtension() throws ParseException {
SyntaxTreeNode tid, top, last;
last = null; top = null;
@@ -6276,8 +6276,8 @@ SyntaxTreeNode tn;
}
final public SyntaxTreeNode ReducedExpression() throws ParseException {
- /*************************************************************************
- * This is an expression that can follow "[...]_" or "<<...>>_". *
+ /*************************************************************************
+ * This is an expression that can follow "[...]_" or "<<...>>_". *
*************************************************************************/
SyntaxTreeNode expr;
bpa("restricted form of expression");
@@ -6309,11 +6309,11 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-// The following cases - for the first expression - must be recognized :
-// "GeneralId", "OpApplication", "RecordComponent", "FcnAppl", "ParenExpr", "SetEnumerate", "SubsetOf", "SetOfAll", "FcnConst", "SetOfFcns", "RcdConstructor", "SetOfRcds", "Except", "Tuple", "ActionExpr"
-// The cases break down in two categories: two set of () or a single one.
-// in general, it's going to be some () [] or {} expression, or an Identifier foollowed by . () or [].
-// Note that FcnAppl may be more intricate.
+// The following cases - for the first expression - must be recognized :
+// "GeneralId", "OpApplication", "RecordComponent", "FcnAppl", "ParenExpr", "SetEnumerate", "SubsetOf", "SetOfAll", "FcnConst", "SetOfFcns", "RcdConstructor", "SetOfRcds", "Except", "Tuple", "ActionExpr"
+// The cases break down in two categories: two set of () or a single one.
+// in general, it's going to be some () [] or {} expression, or an Identifier foollowed by . () or [].
+// Note that FcnAppl may be more intricate.
final public SyntaxTreeNode FairnessExpr() throws ParseException {
SyntaxTreeNode zn[] = new SyntaxTreeNode[5];
SyntaxTreeNode tn, expr;
@@ -6461,12 +6461,12 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* LetIn ::= <LET> LetDefinitions() <LETIN> Expression() *
-* *
-* It produces a SyntaxTreeNode tn with the four heirs *
-* "LET", LetDefinitions, "IN", Expression *
-* in tn.zero. *
+/***************************************************************************
+* LetIn ::= <LET> LetDefinitions() <LETIN> Expression() *
+* *
+* It produces a SyntaxTreeNode tn with the four heirs *
+* "LET", LetDefinitions, "IN", Expression *
+* in tn.zero. *
***************************************************************************/
final public SyntaxTreeNode LetIn() throws ParseException {
SyntaxTreeNode zn[] = new SyntaxTreeNode[4];
@@ -6522,9 +6522,9 @@ SyntaxTreeNode tn;
final public SyntaxTreeNode Junctions() throws ParseException {
BStack.newReference(getToken(1).endColumn, getToken(1).kind);
- /***********************************************************************
- * Pushes onto BStack an element of the appropriate kind with offest *
- * equal to the column of the last character in the /\ or \/ token. *
+ /***********************************************************************
+ * Pushes onto BStack an element of the appropriate kind with offest *
+ * equal to the column of the last character in the /\ or \/ token. *
***********************************************************************/
bpa("AND-OR Junction");
@@ -6637,13 +6637,13 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-/***************************************************************************
-* Lambda expression added by LL on 27 March 2007 *
-* *
-* L.Lambda ::= *
-* <LAMBDA> *
-* (IdentDecl | SomeFixDecl) (<COMMA> (IdentDecl | SomeFixDecl))* *
-* <COLON> Expression *
+/***************************************************************************
+* Lambda expression added by LL on 27 March 2007 *
+* *
+* L.Lambda ::= *
+* <LAMBDA> *
+* (IdentDecl | SomeFixDecl) (<COMMA> (IdentDecl | SomeFixDecl))* *
+* <COLON> Expression *
***************************************************************************/
final public SyntaxTreeNode Lambda() throws ParseException {
SyntaxTreeNode tn;
@@ -6683,8 +6683,8 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-// boxDisc (riminate) uses preInEmptyTop
-// note that junction is processed separately.
+// boxDisc (riminate) uses preInEmptyTop
+// note that junction is processed separately.
final public SyntaxTreeNode Expression() throws ParseException {
SyntaxTreeNode tn, tn0, tn1, tn2;
int kind ;
@@ -6852,7 +6852,7 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
- // Expression
+ // Expression
final public void ExtendableExpr() throws ParseException {
SyntaxTreeNode tn, tn0, tn1, tn2;
SyntaxTreeNode[] heirs;
@@ -7135,7 +7135,7 @@ SyntaxTreeNode tn;
epa() ;
}
- // ExtendableExpr
+ // ExtendableExpr
final public SyntaxTreeNode PrimitiveExp() throws ParseException {
SyntaxTreeNode tn, tn0, tn1, tn2;
SyntaxTreeNode tnOpArgs = null ;
@@ -7542,16 +7542,16 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
- // PrimitiveExp
+ // PrimitiveExp
final public SyntaxTreeNode BangExt() throws ParseException {
- /*************************************************************************
- * Returns an N_IdPrefixElement node with 2 or 3 heirs consisting of: *
- * - A "!" (<BANG>) token. *
- * - An Identifier(), PrefixOp(), InfixOp(), or PostfixOp() node. *
- * - An optional OpArgs() node. *
- * Note that this is not the kind of N_IdPrefixElement that the parser *
- * ultimately produces, which ends with a "!" rather than beginning with *
- * one. *
+ /*************************************************************************
+ * Returns an N_IdPrefixElement node with 2 or 3 heirs consisting of: *
+ * - A "!" (<BANG>) token. *
+ * - An Identifier(), PrefixOp(), InfixOp(), or PostfixOp() node. *
+ * - An optional OpArgs() node. *
+ * Note that this is not the kind of N_IdPrefixElement that the parser *
+ * ultimately produces, which ends with a "!" rather than beginning with *
+ * one. *
*************************************************************************/
SyntaxTreeNode tn ;
Token t;
@@ -7722,7 +7722,7 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
- // BangExt
+ // BangExt
final public SyntaxTreeNode StructOp() throws ParseException {
SyntaxTreeNode tn = null ;
Token t = null;
@@ -7763,107 +7763,107 @@ SyntaxTreeNode tn;
throw new Error("Missing return statement in function");
}
-// SyntaxTreeNode
-// oldExpression() : {
-// /*************************************************************************
-// * The basic production is *
-// * *
-// * Expression ::= ( OpenExpression *
-// * | (Junctions *
-// * | ClosedExpressionOrOp *
-// * | <DOT> Identifier *
-// * | <COLONCOLON> Expression *
-// * )+ *
-// * ( OpenExpression )? *
-// * ) *
-// *************************************************************************/
-// SyntaxTreeNode tn, tn0, tn1, tn2;
-// Token t;
-// OperatorStack.newStack();
-// } {
-// (
-// LOOKAHEAD(OpenStart(), {BStack.aboveReference( getToken(1).beginColumn) } )
-// tn = OpenExpression() { OperatorStack.pushOnStack( tn, null ); }
-// | ( LOOKAHEAD( /* <BAND> | <BOR> | */ <AND> | <OR>,
-// // ^^^
-// // Warning 4 -- Eliminated in SANY2
-// { OperatorStack.preInEmptyTop() &&
-// BStack.aboveReference( getToken(1).beginColumn) } )
-// tn = Junctions() { OperatorStack.pushOnStack( tn, null ); }
-// | LOOKAHEAD( { ClosedStart(getToken(1))
-// && boxDisc()
-// /***************************************************
-// * \equiv *
-// * (token is "[]" => it's the temporal operator) *
-// ***************************************************/
-// && BStack.aboveReference(
-// getToken(1).beginColumn) })
-// tn = ClosedExpressionOrOp() {
-// anchor = tn; // XXX is this correct ? Why had it disappered ?
-// // This is the only place where anchor is set it seems.
-// /*****************************************************************
-// * If tn is an operator, push it on the stack and, if it's not *
-// * the only thing on the stack, then reduce the stack. *
-// * Otherwise, just push it on the stack. *
-// *****************************************************************/
-// if ( isGenOp( tn ) ) {
-// OperatorStack.pushOnStack( tn, lastOp );
-// if (OperatorStack.size() != 1)
-// OperatorStack.reduceStack();
-// // else
-// // ToolIO.out.println("size of 1");
-// } else OperatorStack.pushOnStack( tn, null );
-// }
-// |
-// t = <DOT> {
-// Token next = getToken(1);
-// if (isFieldNameToken( next )) next.kind = IDENTIFIER;
-// }
-// tn = Identifier()
-// { OperatorStack.reduceRecord( new SyntaxTreeNode(mn, t) , tn ); }
-// |
-// t = <COLONCOLON> {
-// tn1 = new SyntaxTreeNode(mn, t) ;
-// tn0 = OperatorStack.topOfStack().getNode();
-// if (! isLabel(tn0)) {
-// throw new ParseException("`::' at " + tn1.getLocation().toString()
-// + " does not follow a label.") ;
-// } ;
-// OperatorStack.popCurrentTop() ;
-// } // t = <COLONCOLON>
-// tn2 = Expression() {
-// // String str = "null" ;
-// // if (lastOp != null) { str = lastOp.toString(); } ;
-// // ToolIO.out.println("lastOp after parsing labeled expression is: " + str);
-// if (! labelDoesNotChangeParse(tn2, lastOp)) {
-// /*****************************************************************
-// * Note: if tn1 is a prefix, infix, or postfix expression, then *
-// * I believe (perhaps naively) that lastOp will be its operator. *
-// *****************************************************************/
-// throw new ParseException(
-// "Removing label at " + tn0.getLocation().toString() +
-// " would change expression parsing.") ;
-// } ;
-// SyntaxTreeNode labelHeirs[] = {tn0, tn1, tn2} ;
-// tn = new SyntaxTreeNode(N_Label, labelHeirs) ;
-// OperatorStack.pushOnStack( tn, null );
-// }
-// )+
-// [ LOOKAHEAD( OpenStart(), {BStack.aboveReference( getToken(1).beginColumn) } )
-// tn = OpenExpression() { OperatorStack.pushOnStack( tn, null ); } ]
-// )
-// { tn = OperatorStack.finalReduce();
-// if (tn==null) throw new ParseException( " Couldn't reduce expression stack.");
-// OperatorStack.popStack();
-// return tn; }
-// } // Expression()
-
-/* Obsolete
-void
-ClosedStart() : {
-}{
- <IDENTIFIER> | <STRING_LITERAL> | <NUMBER_LITERAL> | <LBR> | <LSB> | <LAB> | <LBC> | <LWB> | <OpSymbol> | <OR> | <AND> | <WF> | <SF>
-}
+// SyntaxTreeNode
+// oldExpression() : {
+// /*************************************************************************
+// * The basic production is *
+// * *
+// * Expression ::= ( OpenExpression *
+// * | (Junctions *
+// * | ClosedExpressionOrOp *
+// * | <DOT> Identifier *
+// * | <COLONCOLON> Expression *
+// * )+ *
+// * ( OpenExpression )? *
+// * ) *
+// *************************************************************************/
+// SyntaxTreeNode tn, tn0, tn1, tn2;
+// Token t;
+// OperatorStack.newStack();
+// } {
+// (
+// LOOKAHEAD(OpenStart(), {BStack.aboveReference( getToken(1).beginColumn) } )
+// tn = OpenExpression() { OperatorStack.pushOnStack( tn, null ); }
+// | ( LOOKAHEAD( /* <BAND> | <BOR> | */ <AND> | <OR>,
+// // ^^^
+// // Warning 4 -- Eliminated in SANY2
+// { OperatorStack.preInEmptyTop() &&
+// BStack.aboveReference( getToken(1).beginColumn) } )
+// tn = Junctions() { OperatorStack.pushOnStack( tn, null ); }
+// | LOOKAHEAD( { ClosedStart(getToken(1))
+// && boxDisc()
+// /***************************************************
+// * \equiv *
+// * (token is "[]" => it's the temporal operator) *
+// ***************************************************/
+// && BStack.aboveReference(
+// getToken(1).beginColumn) })
+// tn = ClosedExpressionOrOp() {
+// anchor = tn; // XXX is this correct ? Why had it disappered ?
+// // This is the only place where anchor is set it seems.
+// /*****************************************************************
+// * If tn is an operator, push it on the stack and, if it's not *
+// * the only thing on the stack, then reduce the stack. *
+// * Otherwise, just push it on the stack. *
+// *****************************************************************/
+// if ( isGenOp( tn ) ) {
+// OperatorStack.pushOnStack( tn, lastOp );
+// if (OperatorStack.size() != 1)
+// OperatorStack.reduceStack();
+// // else
+// // ToolIO.out.println("size of 1");
+// } else OperatorStack.pushOnStack( tn, null );
+// }
+// |
+// t = <DOT> {
+// Token next = getToken(1);
+// if (isFieldNameToken( next )) next.kind = IDENTIFIER;
+// }
+// tn = Identifier()
+// { OperatorStack.reduceRecord( new SyntaxTreeNode(mn, t) , tn ); }
+// |
+// t = <COLONCOLON> {
+// tn1 = new SyntaxTreeNode(mn, t) ;
+// tn0 = OperatorStack.topOfStack().getNode();
+// if (! isLabel(tn0)) {
+// throw new ParseException("`::' at " + tn1.getLocation().toString()
+// + " does not follow a label.") ;
+// } ;
+// OperatorStack.popCurrentTop() ;
+// } // t = <COLONCOLON>
+// tn2 = Expression() {
+// // String str = "null" ;
+// // if (lastOp != null) { str = lastOp.toString(); } ;
+// // ToolIO.out.println("lastOp after parsing labeled expression is: " + str);
+// if (! labelDoesNotChangeParse(tn2, lastOp)) {
+// /*****************************************************************
+// * Note: if tn1 is a prefix, infix, or postfix expression, then *
+// * I believe (perhaps naively) that lastOp will be its operator. *
+// *****************************************************************/
+// throw new ParseException(
+// "Removing label at " + tn0.getLocation().toString() +
+// " would change expression parsing.") ;
+// } ;
+// SyntaxTreeNode labelHeirs[] = {tn0, tn1, tn2} ;
+// tn = new SyntaxTreeNode(N_Label, labelHeirs) ;
+// OperatorStack.pushOnStack( tn, null );
+// }
+// )+
+// [ LOOKAHEAD( OpenStart(), {BStack.aboveReference( getToken(1).beginColumn) } )
+// tn = OpenExpression() { OperatorStack.pushOnStack( tn, null ); } ]
+// )
+// { tn = OperatorStack.finalReduce();
+// if (tn==null) throw new ParseException( " Couldn't reduce expression stack.");
+// OperatorStack.popStack();
+// return tn; }
+// } // Expression()
+
+/* Obsolete
+void
+ClosedStart() : {
+}{
+ <IDENTIFIER> | <STRING_LITERAL> | <NUMBER_LITERAL> | <LBR> | <LSB> | <LAB> | <LBC> | <LWB> | <OpSymbol> | <OR> | <AND> | <WF> | <SF>
+}
*/
final public void OpenStart() throws ParseException {
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
diff --git a/tlatools/src/tla2sany/semantic/LevelConstants.java b/tlatools/src/tla2sany/semantic/LevelConstants.java
index 9dd9ac81bf3a61636a906911282dc6dbfbc7ebab..086b063023fb46a02713654b667c1839272986fe 100644
--- a/tlatools/src/tla2sany/semantic/LevelConstants.java
+++ b/tlatools/src/tla2sany/semantic/LevelConstants.java
@@ -14,10 +14,10 @@ public interface LevelConstants {
static final int MinLevel = 0;
static final int MaxLevel = 3;
- static final Integer[] Levels = {new Integer(ConstantLevel),
- new Integer(VariableLevel),
- new Integer(ActionLevel),
- new Integer(TemporalLevel)};
+ static final Integer[] Levels = {ConstantLevel,
+ VariableLevel,
+ ActionLevel,
+ TemporalLevel};
static final HashSet EmptySet = new HashSet();
static final SetOfLevelConstraints EmptyLC = new SetOfLevelConstraints();
diff --git a/tlatools/src/tla2sany/semantic/OpApplNode.java b/tlatools/src/tla2sany/semantic/OpApplNode.java
index 474c05c481283ce2bf7207d3d3b962ea830f6b45..741db359ee804a921f740548c9a09027a2f81275 100644
--- a/tlatools/src/tla2sany/semantic/OpApplNode.java
+++ b/tlatools/src/tla2sany/semantic/OpApplNode.java
@@ -1298,7 +1298,7 @@ public class OpApplNode extends ExprNode implements ExploreNode {
if (operator.getName().toString().equals("$Case") && operands.length > 1 /* OTHER cannot occur alone in a CASE */) {
// OTHER should be last operand
ExprOrOpArgNode lastOperand = operands[operands.length-1];
- if (lastOperand instanceof tla2sany.semantic.OpApplNode) {
+ if (lastOperand instanceof OpApplNode) {
OpApplNode other = (OpApplNode)lastOperand;
// indeed the OTHER case
if (other.getOperator().getName().toString().equals("$Pair") && other.getArgs()[0] == null) {
diff --git a/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java b/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java
index edafe574a290a855dbd488667f1fdcc38fe32c7e..95b77a3393d59aa18323c72eb4f489e84ae83631 100644
--- a/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java
+++ b/tlatools/src/tla2sany/semantic/SetOfArgLevelConstraints.java
@@ -29,13 +29,13 @@ class SetOfArgLevelConstraints extends HashMap<ParamAndPosition, Integer> implem
Integer old = this.get(pap);
int oldLevel = (old == null) ? MinLevel : old.intValue();
- super.put(pap, new Integer(Math.max(newLevel, oldLevel)));
+ super.put(pap, Math.max(newLevel, oldLevel));
return old;
}
public final Integer put(SymbolNode param, int position, int level) {
ParamAndPosition pap = new ParamAndPosition(param, position);
- return this.put(pap, new Integer(level));
+ return this.put(pap, level);
}
/**
diff --git a/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java b/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java
index 676bb196cb14fb49f9aea86788468a4939f8e261..1d1000181055cccb4df3da4b4062c86c4bc754da 100644
--- a/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java
+++ b/tlatools/src/tla2sany/semantic/SetOfLevelConstraints.java
@@ -25,7 +25,7 @@ class SetOfLevelConstraints extends HashMap<SymbolNode, Integer> implements Leve
Integer old = this.get(param);
int oldLevel = (old == null) ? MaxLevel : old.intValue();
- super.put(param, new Integer(Math.min(newLevel, oldLevel)));
+ super.put(param, Math.min(newLevel, oldLevel));
return old;
}
diff --git a/tlatools/src/tla2sany/semantic/Subst.java b/tlatools/src/tla2sany/semantic/Subst.java
index 8f3bd4de55010c74d99707e149c317534cb5a859..5dd3e746fbc9256342cb102298df998823ce9e56 100644
--- a/tlatools/src/tla2sany/semantic/Subst.java
+++ b/tlatools/src/tla2sany/semantic/Subst.java
@@ -155,7 +155,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
* check it first, which is why we need the iteration number *
* argument of this method. *
*****************************************************************/
- Integer mlevel = new Integer(subDef.getMaxLevel(alp.i));
+ Integer mlevel = subDef.getMaxLevel(alp.i);
Iterator<SymbolNode> iter1 = paramSet(alp.param, subs).iterator();
while (iter1.hasNext()) {
res.put(iter1.next(), mlevel);
@@ -203,7 +203,7 @@ public class Subst implements LevelConstants, ASTConstants, ExploreNode, XMLExpo
/***************************************************************
* Must invoke levelCheck before invoking getLevel *
***************************************************************/
- Integer subLevel = new Integer(subParam.getLevel());
+ Integer subLevel = subParam.getLevel();
res.put(pap, subLevel);
}
}
diff --git a/tlatools/src/tla2sany/semantic/TheoremNode.java b/tlatools/src/tla2sany/semantic/TheoremNode.java
index 7b07e72372603313e677ad6f34bac6b7e69c2c92..1d6b98f10067b6977f789927281ab9c55951109d 100644
--- a/tlatools/src/tla2sany/semantic/TheoremNode.java
+++ b/tlatools/src/tla2sany/semantic/TheoremNode.java
@@ -428,7 +428,7 @@ public class TheoremNode extends LevelNode {
return "TheoremNodeRef";
}
- protected Element getLevelElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getLevelElement(Document doc, SymbolContext context) {
Element e = doc.createElement("TheoremNode");
//the theorem name is now contained in the definition, if it exists
diff --git a/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java b/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java
index 3e64c84fc28e76e9371ddc7ff9b9e6a8fa8e0bd0..84b93725610dd707b30a3e5d099ff18ced7f1587 100644
--- a/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java
+++ b/tlatools/src/tla2sany/semantic/ThmOrAssumpDefNode.java
@@ -649,7 +649,7 @@ public class ThmOrAssumpDefNode extends SymbolNode
}
}
- protected Element getSymbolElement(Document doc, tla2sany.xml.SymbolContext context) {
+ protected Element getSymbolElement(Document doc, SymbolContext context) {
assert(this.body != null); //A theorem or assumption definition without a body does not make sense.
Element e = null;
if (theorem) {
diff --git a/tlatools/src/tla2sany/xml/SymbolContext.java b/tlatools/src/tla2sany/xml/SymbolContext.java
index c4100a4aca75d7dd705c861e728c1115e2b5e44f..7395ff47e1db7088a75fa19f4369868a4b2549e7 100644
--- a/tlatools/src/tla2sany/xml/SymbolContext.java
+++ b/tlatools/src/tla2sany/xml/SymbolContext.java
@@ -52,7 +52,7 @@ public class SymbolContext {
}
public void put(SymbolNode nd, Document doc) {
- Integer k = new Integer(nd.myUID);
+ Integer k = nd.myUID;
if (!keys.contains(k)) {
// first add the key as it might be mentioned again inside the definition
keys.add(k);
@@ -62,7 +62,7 @@ public class SymbolContext {
}
public void put(TheoremNode nd, Document doc) {
- Integer k = new Integer(nd.myUID);
+ Integer k = nd.myUID;
if (!keys.contains(k)) {
// first add the key as it might be mentioned again inside the definition
keys.add(k);
@@ -72,7 +72,7 @@ public class SymbolContext {
}
public void put(AssumeNode nd, Document doc) {
- Integer k = new Integer(nd.myUID);
+ Integer k = nd.myUID;
if (!keys.contains(k)) {
// first add the key as it might be mentioned again inside the definition
keys.add(k);
diff --git a/tlatools/src/tlc2/module/TransitiveClosure.java b/tlatools/src/tlc2/module/TransitiveClosure.java
index 49e53efa03be6c388127e369e5c27dffb8490dac..abdc1a7436b1c8d2e75f812ef7b43eb6ddfac322 100644
--- a/tlatools/src/tlc2/module/TransitiveClosure.java
+++ b/tlatools/src/tlc2/module/TransitiveClosure.java
@@ -51,7 +51,7 @@ public class TransitiveClosure implements ValueConstants
Integer num = fps.get(elem1);
if (num == null)
{
- fps.put(elem1, new Integer(cnt));
+ fps.put(elem1, cnt);
elemList.addElement(elem1);
cnt++;
} else
@@ -62,7 +62,7 @@ public class TransitiveClosure implements ValueConstants
num = fps.get(elem2);
if (num == null)
{
- fps.put(elem2, new Integer(cnt));
+ fps.put(elem2, cnt);
elemList.addElement(elem2);
cnt++;
} else
diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index 0d1299c019fa4c9b037f3192f7b52bf5aff227f2..a493c59604525335c1218d4ea3bd7c707eb50f86 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -251,6 +251,8 @@ public class MP
{
parameters = EMPTY_PARAMS;
}
+ OutputCollector.saveMessage(messageClass, messageCode, parameters);
+
DebugPrinter.print("entering MP.getMessage() with error code " + messageCode + " and " + parameters.length //$NON-NLS-1$
+ " parameters"); //$NON-NLS-1$
@@ -288,7 +290,7 @@ public class MP
break;
}
}
-
+
b.append(getMessage0(messageClass, messageCode, parameters));
if (TLCGlobals.tool)
@@ -721,11 +723,11 @@ public class MP
case EC.TLC_EXCEPT_APPLIED_TO_UNKNOWN_FIELD:
b.append("The EXCEPT was applied to non-existing fields of the value at\n%1%");
break;
-
+
case EC.TLC_SYMMETRY_SET_TOO_SMALL:
b.append("The set%1% %2% %3% been defined to be a symmetry set but contain%4% less than two elements.");
break;
-
+
case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_QUANTIFIER:
b.append("TLC does not support temporal existential, nor universal, quantification over state variables.");
break;
@@ -960,8 +962,8 @@ public class MP
/*
* The two startup banners below are parsed by the Toolbox in
* org.lamport.tla.toolbox.tool.tlc.output.data.TLCModelLaunchDataProvider.
- * startupMessagePattern. Remember to update when the banners below
- * get changed
+ * startupMessagePattern. Remember to update when the banners below
+ * get changed
* (see org.lamport.tla.toolbox.tool.tlc.output.data.TLCModelLaunchDataProviderTest)!!!
*/
case EC.TLC_MODE_MC:
@@ -1504,7 +1506,7 @@ public class MP
}
if (throwable instanceof Assert.TLCRuntimeException) {
// MK 07/25/2017: Disguise TLCRuntimeException with its parent class
- // RuntimeException to not change the externally visible TLC output
+ // RuntimeException to not change the externally visible TLC output
// when an exception gets reports.
msg = msg + "\nThe exception was a " + RuntimeException.class.getName() + "\n";
} else {
@@ -1604,8 +1606,8 @@ public class MP
}
return tre.errorCode;
}
-
- /**
+
+ /**
* Prints the state
* @param parameters
*/
@@ -1616,7 +1618,7 @@ public class MP
ToolIO.out.println(getMessage(STATE, code, parameters));
DebugPrinter.print("leaving printState(String[])"); //$NON-NLS-1$
}
-
+
public static void printState(int code, String[] parameters, TLCStateInfo stateInfo, int num)
{
recorder.record(code, (TLCStateInfo) stateInfo, num);
@@ -1703,11 +1705,11 @@ public class MP
}
DebugPrinter.print("leaving printWarning(int, String[])"); //$NON-NLS-1$
}
-
+
public static void printStats(final IBucketStatistics inDegree, final IBucketStatistics outDegree) {
// Out degree
ToolIO.out.println(outDegree);
-
+
// In Degree
ToolIO.out.println(inDegree);
diff --git a/tlatools/src/tlc2/output/Message.java b/tlatools/src/tlc2/output/Message.java
new file mode 100644
index 0000000000000000000000000000000000000000..b7d557ba22065eafbf1218a7bab10b08e7063250
--- /dev/null
+++ b/tlatools/src/tlc2/output/Message.java
@@ -0,0 +1,42 @@
+package tlc2.output;
+
+import java.util.Date;
+
+public class Message {
+
+ private int messageClass;
+ private int errorCode;
+ private String[] parameters;
+ private Date date;
+
+ public Message(int errorCode, String[] parameters, Date date){
+ this.errorCode = errorCode;
+ this.parameters = parameters;
+ this.date = date;
+ }
+
+ public Message(int messageClass, int errorCode, String[] parameters,
+ Date date) {
+ this.messageClass = messageClass;
+ this.errorCode = errorCode;
+ this.parameters = parameters;
+ this.date = date;
+ }
+
+ public int getMessageClass(){
+ return messageClass;
+ }
+
+ public int getMessageCode() {
+ return errorCode;
+ }
+
+ public String[] getParameters() {
+ return parameters;
+ }
+
+ public Date getDate(){
+ return date;
+ }
+
+}
\ No newline at end of file
diff --git a/tlatools/src/tlc2/output/OutputCollector.java b/tlatools/src/tlc2/output/OutputCollector.java
new file mode 100644
index 0000000000000000000000000000000000000000..55621afe7074609697a04a94b64d79e3cfc3fdc0
--- /dev/null
+++ b/tlatools/src/tlc2/output/OutputCollector.java
@@ -0,0 +1,80 @@
+package tlc2.output;
+
+import java.util.ArrayList;
+import java.util.Date;
+import java.util.Hashtable;
+
+import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.st.Location;
+import tlc2.tool.TLCState;
+import tlc2.tool.TLCStateInfo;
+
+public class OutputCollector {
+
+ private static TLCState initialState = null;
+ private static ArrayList<TLCStateInfo> trace = null;
+ private static ArrayList<Message> allMessages = new ArrayList<Message>();
+ private static Hashtable<Location, Long> lineCount = new Hashtable<Location, Long>();
+ private static ModuleNode moduleNode = null;
+ private static ArrayList<ExprNode> violatedAssumptions = new ArrayList<>();
+
+ public static ArrayList<TLCStateInfo> getTrace() {
+ return trace;
+ }
+
+ public static void setTrace(ArrayList<TLCStateInfo> trace) {
+ OutputCollector.trace = trace;
+ }
+
+ public static void addStateToTrace(TLCStateInfo tlcStateInfo) {
+ if (trace == null) {
+ trace = new ArrayList<TLCStateInfo>();
+ }
+ trace.add(tlcStateInfo);
+ }
+
+ public static void setInitialState(TLCState initialState) {
+ OutputCollector.initialState = initialState;
+ }
+
+ public static TLCState getInitialState() {
+ return OutputCollector.initialState;
+ }
+
+ public static ArrayList<Message> getAllMessages() {
+ return allMessages;
+ }
+
+ public static void addViolatedAssumption(ExprNode assumption) {
+ violatedAssumptions.add(assumption);
+ }
+
+ public static ArrayList<ExprNode> getViolatedAssumptions() {
+ return violatedAssumptions;
+ }
+
+ public synchronized static void saveMessage(int messageClass,
+ int messageCode, String[] parameters) {
+
+ Message m = new Message(messageClass, messageCode, parameters,
+ new Date());
+ allMessages.add(m);
+ }
+
+ public static ModuleNode getModuleNode() {
+ return moduleNode;
+ }
+
+ public static void setModuleNode(ModuleNode moduleNode) {
+ OutputCollector.moduleNode = moduleNode;
+ }
+
+ public static Hashtable<Location, Long> getLineCountTable() {
+ return new Hashtable<>(lineCount);
+ }
+
+ public static void putLineCount(Location location, long val) {
+ lineCount.put(location, val);
+ }
+}
\ No newline at end of file
diff --git a/tlatools/src/tlc2/output/StatePrinter.java b/tlatools/src/tlc2/output/StatePrinter.java
index aa1078a1603cdacb8fdf5e7b4ac96a6313c9b10d..f81c745c279d81fc17640cf9e3f2f36549d4e8d6 100644
--- a/tlatools/src/tlc2/output/StatePrinter.java
+++ b/tlatools/src/tlc2/output/StatePrinter.java
@@ -78,6 +78,7 @@ public class StatePrinter
MP.printState(EC.TLC_STATE_PRINT2, new String[] { String.valueOf(num), currentStateInfo.info.toString(),
stateString, "-1" }, currentStateInfo, num);
}
+ OutputCollector.addStateToTrace(currentStateInfo);
}
/**
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index 7c2c6722d224b2004f4f5abd4b8ea7f9f92f25dc..0065b8861e672fe97f32ebb66660ead6f4aeae47 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -6,10 +6,12 @@ import java.math.MathContext;
import java.util.Timer;
import java.util.TimerTask;
+import tla2sany.semantic.ModuleNode;
import tlc2.TLC;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.coverage.CostModelCreator;
import tlc2.tool.impl.FastTool;
import tlc2.tool.liveness.AddAndCheckLiveCheck;
@@ -78,6 +80,8 @@ public abstract class AbstractChecker
this.checkDeadlock = deadlock;
this.checkLiveness = !this.tool.livenessIsTrue();
+ OutputCollector.setModuleNode(this.tool.getRootModule());
+
// moved to file utilities
this.metadir = metadir;
diff --git a/tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/src/tlc2/tool/DFIDModelChecker.java
index c333ed588ace262232bccedf31ab9ff82803cf8b..1ff62121930fdf211f530ed76eaa3e63f0e729f7 100644
--- a/tlatools/src/tlc2/tool/DFIDModelChecker.java
+++ b/tlatools/src/tlc2/tool/DFIDModelChecker.java
@@ -12,6 +12,7 @@ import tla2sany.semantic.OpDeclNode;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.fp.dfid.FPIntSet;
import tlc2.tool.fp.dfid.MemFPIntSet;
import tlc2.tool.impl.CallStackTool;
@@ -246,22 +247,25 @@ public class DFIDModelChecker extends AbstractChecker
{
ExprNode[] assumps = this.tool.getAssumptions();
boolean[] isAxiom = this.tool.getAssumptionIsAxiom();
+ int errorCode = EC.NO_ERROR;
for (int i = 0; i < assumps.length; i++)
{
try
{
if ((!isAxiom[i]) && !this.tool.isValid(assumps[i]))
{
- return MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ errorCode = MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
}
- } catch (Exception e)
+ } catch (final Exception e)
{
// Assert.printStack(e);
- return MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ errorCode = MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
new String[] { assumps[i].toString(), e.getMessage() });
}
}
- return EC.NO_ERROR;
+ return errorCode;
}
/* Compute the set of initial states. */
diff --git a/tlatools/src/tlc2/tool/ITool.java b/tlatools/src/tlc2/tool/ITool.java
index 2917e4085a1f160e89896618fd03e680891cb17e..68d899cf476e2576b21ccf1c834255389820fc4e 100644
--- a/tlatools/src/tlc2/tool/ITool.java
+++ b/tlatools/src/tlc2/tool/ITool.java
@@ -28,12 +28,7 @@ package tlc2.tool;
import java.io.File;
import java.util.List;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.SymbolNode;
+import tla2sany.semantic.*;
import tlc2.tool.coverage.CostModel;
import tlc2.tool.impl.ModelConfig;
import tlc2.util.Context;
@@ -178,6 +173,8 @@ public interface ITool extends TraceApp {
*/
String getRootFile();
+ ModuleNode getRootModule();
+
String getConfigFile();
String getSpecDir();
diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java
index 53bbe671db92b82740d2f063346dbad88d4e012e..5a2007d4683bad7eb49e849e6f94aa13330c6bfe 100644
--- a/tlatools/src/tlc2/tool/ModelChecker.java
+++ b/tlatools/src/tlc2/tool/ModelChecker.java
@@ -18,6 +18,7 @@ import tla2sany.semantic.OpDeclNode;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.fp.FPSet;
import tlc2.tool.fp.FPSetConfiguration;
import tlc2.tool.fp.FPSetFactory;
@@ -1131,6 +1132,7 @@ public class ModelChecker extends AbstractChecker
}
}
}
+ OutputCollector.setInitialState(curState);
// Check properties of the state:
if (!seen || forceChecks) {
for (int j = 0; j < tool.getInvariants().length; j++) {
diff --git a/tlatools/src/tlc2/tool/TLCState.java b/tlatools/src/tlc2/tool/TLCState.java
index 67c5fa72575a904595e2b71ffa02dce1d861bc52..1e66db7dc1d732be52c485b24cc392d4a98f4a4f 100644
--- a/tlatools/src/tlc2/tool/TLCState.java
+++ b/tlatools/src/tlc2/tool/TLCState.java
@@ -36,7 +36,7 @@ public abstract class TLCState implements Cloneable, Serializable {
public static TLCState Empty = null;
// The state variables.
- protected static OpDeclNode[] vars = null;
+ public static OpDeclNode[] vars = null;
public void read(IValueInputStream vis) throws IOException {
this.workerId = vis.readShortNat();
diff --git a/tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/src/tlc2/tool/TLCTrace.java
index 157e37f27319bc9d116f4dce0cccb5e5ad491c78..eed6e88f75d7fab23bb4fa9cfae0904a9f69cfa9 100644
--- a/tlatools/src/tlc2/tool/TLCTrace.java
+++ b/tlatools/src/tlc2/tool/TLCTrace.java
@@ -10,11 +10,14 @@ import java.io.DataInputStream;
import java.io.DataOutputStream;
import java.io.File;
import java.io.IOException;
+import java.util.ArrayList;
+import java.util.Arrays;
import java.util.HashMap;
import java.util.Map;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.output.StatePrinter;
import tlc2.util.BufferedRandomAccessFile;
import tlc2.util.LongVec;
@@ -90,7 +93,7 @@ public class TLCTrace {
/**
* Returns the level (monotonically increasing)!
- *
+ *
* LL: The user has no real need of an accurate tree height. Breadth-first
* search is good because it provides the shortest possible error trace.
* Usually approximately breadth-first search is just as good because it
@@ -105,7 +108,7 @@ public class TLCTrace {
* what it means.) I'd like to make the reported value be monotonic because,
* if it's not, users may worry and people already have enough things in
* life to worry about.
- *
+ *
* @see TLCTrace#getLevel()
*/
public synchronized int getLevelForReporting() throws IOException {
@@ -131,7 +134,7 @@ public class TLCTrace {
// on the highest level of the state tree, which is only true if
// states are explored with strict breadth-first search.
//
- // The (execution) trace is a forest of one to n trees, where each path
+ // The (execution) trace is a forest of one to n trees, where each path
// in the forest represents the order in which states have been generated
// by the workers.
// The algorithm, with which the diameter is approximated from the trace,
@@ -143,21 +146,21 @@ public class TLCTrace {
// successors have been appended (yet, assuming there are any).
//
// Once the workers have terminated, TLC traverses the trace from a leaf record
- // back to a root record. This height is what is reported as the diameter.
+ // back to a root record. This height is what is reported as the diameter.
// The selection, from what leaf record TLC starts the traversal, is based on
// the last record inserted into the trace file. If this record is one with a
// low height (because its corresponding worker waited most of the time), the
- // diameter will thus be underreport. If, on the other hand, the last record
+ // diameter will thus be underreport. If, on the other hand, the last record
// happens to be one with a large height, the diameter will be overreported.
- //
- // The selection of the leaf record is the source of the algorithm's
+ //
+ // The selection of the leaf record is the source of the algorithm's
// non-determinism. With a single worker, the last record in the trace is
- // always the same which always corresponds to the longest behavior found so
+ // always the same which always corresponds to the longest behavior found so
// far (strict BFS). This invariant does not hold with multiple workers.
//
// Obviously, with multiple workers the approximation of the diameter will
// improve with the size of the state graph. Assuming a well-shaped state graph,
- // we can argue that the approximation is good enough and document, that its
+ // we can argue that the approximation is good enough and document, that its
// value can be anything from 1 to the longest behavior found so far.
return getLevel(this.lastPtr);
}
@@ -256,7 +259,7 @@ public class TLCTrace {
}
this.raf.seek(curLoc);
}
-
+
return getTrace(fps);
}
@@ -282,7 +285,7 @@ public class TLCTrace {
// This is only necessary though, if TLCGlobals.enumFraction was < 1 during
// the generation of inits.
RandomEnumerableValues.reset();
-
+
// The vector of fingerprints is now being followed forward from the
// initial state (which is the last state in the long vector), to the
// end state.
@@ -326,7 +329,7 @@ public class TLCTrace {
/**
* Write out a sequence of states that reaches s2 from an initial state,
* according to the spec. s2 is a next state of s1.
- *
+ *
* @param s1
* may not be null.
* @param s2
@@ -337,9 +340,11 @@ public class TLCTrace {
public void printTrace(final TLCState s1, final TLCState s2) throws IOException, WorkerException {
printTrace(s1, s2, getTrace(s1.uid, false));
}
-
+
protected synchronized final void printTrace(final TLCState s1, final TLCState s2, final TLCStateInfo[] prefix)
throws IOException, WorkerException {
+ ArrayList<TLCStateInfo> trace = new ArrayList<TLCStateInfo>(); // collecting the whole error trace
+
if (s1.isInitial()) {
// Do not recreate the potentially expensive error trace - e.g. when the set of
// initial states is huge such as during inductive invariant checking. Instead
@@ -360,6 +365,7 @@ public class TLCTrace {
while (idx < prefix.length) {
StatePrinter.printState(prefix[idx], lastState, idx + 1);
lastState = prefix[idx].state;
+ trace.add(prefix[idx]);
idx++;
}
@@ -390,6 +396,7 @@ public class TLCTrace {
}
StatePrinter.printState(sinfo, lastState, ++idx);
lastState = sinfo.state;
+ trace.add(sinfo);
// Print s2:
// The predecessor to s2 is s1.
@@ -402,7 +409,9 @@ public class TLCTrace {
System.exit(1);
}
StatePrinter.printState(sinfo, null, ++idx);
+ trace.add(sinfo);
}
+ OutputCollector.setTrace(trace);
}
/**
@@ -477,7 +486,7 @@ public class TLCTrace {
void close() throws IOException;
void reset(long i) throws IOException;
}
-
+
public class TLCTraceEnumerator implements Enumerator {
long len;
BufferedRandomAccessFile enumRaf;
@@ -508,7 +517,7 @@ public class TLCTrace {
this.enumRaf.readLongNat(); /* drop */
return this.enumRaf.readLong();
}
-
+
public final void close() throws IOException {
this.enumRaf.close();
}
diff --git a/tlatools/src/tlc2/tool/coverage/CostModelCreator.java b/tlatools/src/tlc2/tool/coverage/CostModelCreator.java
index a70c7187074f80a4da80e9272abb24e913fbd13f..582d91c5288add3edbb9e8e3dda307fd3f0af2b0 100644
--- a/tlatools/src/tlc2/tool/coverage/CostModelCreator.java
+++ b/tlatools/src/tlc2/tool/coverage/CostModelCreator.java
@@ -50,6 +50,7 @@ import tla2sany.semantic.SubstInNode;
import tla2sany.semantic.SymbolNode;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.Action;
import tlc2.tool.ITool;
import tlc2.tool.coverage.ActionWrapper.Relation;
@@ -179,6 +180,7 @@ public class CostModelCreator extends ExplorerVisitor {
SemanticNode sn;
while ((sn = keys.nextElement()) != null) {
this.nodes.add(new OpApplNodeWrapper((OpApplNode) sn, null));
+ //locationTable.put(loc, ((SemanticNode) key).getLocation());
}
}
@@ -406,6 +408,8 @@ public class CostModelCreator extends ExplorerVisitor {
public static void report(final ITool tool, final long startTime) {
MP.printMessage(EC.TLC_COVERAGE_START);
+ OutputCollector.setModuleNode(tool.getRootModule());
+ //Hashtable<String, Location> locationTable = new Hashtable<String, Location>();
final Vect<Action> init = tool.getInitStateSpec();
for (int i = 0; i < init.size(); i++) {
final Action initAction = init.elementAt(i);
diff --git a/tlatools/src/tlc2/tool/coverage/OpApplNodeWrapper.java b/tlatools/src/tlc2/tool/coverage/OpApplNodeWrapper.java
index ac2233cf32037dc7f55d5e58f2ba07b7eaacb50a..c624deb63d0cc3acfa464034e8b2435bb2c1f6ef 100644
--- a/tlatools/src/tlc2/tool/coverage/OpApplNodeWrapper.java
+++ b/tlatools/src/tlc2/tool/coverage/OpApplNodeWrapper.java
@@ -36,6 +36,7 @@ import tla2sany.st.Location;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
public class OpApplNodeWrapper extends CostModelNode implements Comparable<OpApplNodeWrapper>, CostModel {
@@ -293,8 +294,12 @@ public class OpApplNodeWrapper extends CostModelNode implements Comparable<OpApp
}
protected void printSelf(final int level, final long count) {
- MP.printMessage(EC.TLC_COVERAGE_VALUE, new String[] {
- indentBegin(level, TLCGlobals.coverageIndent, getLocation().toString()), String.valueOf(count) });
+ /*MP.printMessage(EC.TLC_COVERAGE_VALUE, new String[] {
+ indentBegin(level, TLCGlobals.coverageIndent, getLocation().toString()), String.valueOf(count) });*/
+ Location location = getLocation();
+ if(location != null){
+ OutputCollector.putLineCount(location, count);
+ }
}
protected void printSelf(final int level, final long count, final long cost) {
diff --git a/tlatools/src/tlc2/tool/distributed/TLCApp.java b/tlatools/src/tlc2/tool/distributed/TLCApp.java
index 7e2bce787f2552c5c06000015e48b267431e916e..93b9c4a280e896f398821cf5159279f63447d50c 100644
--- a/tlatools/src/tlc2/tool/distributed/TLCApp.java
+++ b/tlatools/src/tlc2/tool/distributed/TLCApp.java
@@ -91,14 +91,14 @@ public class TLCApp extends DistApp {
* @see tlc2.tool.distributed.DistApp#getCheckDeadlock()
*/
public final Boolean getCheckDeadlock() {
- return new Boolean(this.checkDeadlock);
+ return this.checkDeadlock;
}
/* (non-Javadoc)
* @see tlc2.tool.distributed.DistApp#getPreprocess()
*/
public final Boolean getPreprocess() {
- return new Boolean(this.preprocess);
+ return this.preprocess;
}
/* (non-Javadoc)
diff --git a/tlatools/src/tlc2/tool/fp/DiskFPSet.java b/tlatools/src/tlc2/tool/fp/DiskFPSet.java
index f032773b46e25ddf4f5794a4fba8313fd9503d80..04bb80313a3555934db9ef2a9f799bca353d5367 100644
--- a/tlatools/src/tlc2/tool/fp/DiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/DiskFPSet.java
@@ -281,21 +281,21 @@ public abstract class DiskFPSet extends FPSet implements FPSetStatistic {
/* (non-Javadoc)
* @see java.lang.Object#finalize()
*/
- public final void finalize() {
+ /*public final void finalize() {
/* Close any backing disk files in use by this object. */
- for (int i = 0; i < this.braf.length; i++) {
+ /* for (int i = 0; i < this.braf.length; i++) {
try {
this.braf[i].close();
} catch (IOException e) { /* SKIP */
- }
+ /* }
}
for (int i = 0; i < this.brafPool.length; i++) {
try {
this.brafPool[i].close();
} catch (IOException e) { /* SKIP */
- }
+ /* }
}
- }
+ }*/
/* (non-Javadoc)
* @see tlc2.tool.fp.FPSet#addThread()
diff --git a/tlatools/src/tlc2/tool/impl/Spec.java b/tlatools/src/tlc2/tool/impl/Spec.java
index 69558c2a53c220631d5ca78a51c39e9860f11373..d235e92d55ceb1b18a5961b89c5ff6d84031a02a 100644
--- a/tlatools/src/tlc2/tool/impl/Spec.java
+++ b/tlatools/src/tlc2/tool/impl/Spec.java
@@ -14,20 +14,7 @@ import java.util.List;
import java.util.Set;
import tla2sany.modanalyzer.ParseUnit;
-import tla2sany.semantic.APSubstInNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.FrontEnd;
-import tla2sany.semantic.LabelNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tla2sany.semantic.Subst;
-import tla2sany.semantic.SubstInNode;
-import tla2sany.semantic.SymbolNode;
-import tla2sany.semantic.ThmOrAssumpDefNode;
+import tla2sany.semantic.*;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.tool.Action;
@@ -119,6 +106,10 @@ abstract class Spec
return specProcessor;
}
+ public ModuleNode getRootModule() {
+ return specProcessor.getRootModule();
+ }
+
/* Return the variable if expr is a primed state variable. Otherwise, null. */
public final SymbolNode getPrimedVar(SemanticNode expr, Context c, boolean cutoff)
{
diff --git a/tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/src/tlc2/tool/impl/Tool.java
index 93785eb86c511dfba5d854897526c450a5e8885c..d8c631ac014d32a87c8610b727177e9b9100c428 100644
--- a/tlatools/src/tlc2/tool/impl/Tool.java
+++ b/tlatools/src/tlc2/tool/impl/Tool.java
@@ -30,6 +30,7 @@ import tla2sany.semantic.SymbolNode;
import tla2sany.semantic.ThmOrAssumpDefNode;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.Action;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.EvalControl;
@@ -3101,22 +3102,25 @@ public abstract class Tool
public final int checkAssumptions() {
final ExprNode[] assumps = getAssumptions();
final boolean[] isAxiom = getAssumptionIsAxiom();
+ int errorCode = EC.NO_ERROR;
for (int i = 0; i < assumps.length; i++)
{
try
{
if ((!isAxiom[i]) && !isValid(assumps[i]))
{
- return MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ errorCode = MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
}
} catch (final Exception e)
{
// Assert.printStack(e);
- return MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
- new String[] { assumps[i].toString(), e.getMessage() });
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ errorCode = MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
+ new String[] { assumps[i].toString(), e.getMessage() });
}
}
- return EC.NO_ERROR;
+ return errorCode;
}
/* Reconstruct the initial state whose fingerprint is fp. */
diff --git a/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java b/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java
index c45d7af348b208b14a52eabdb664061fe67c9785..4bfebaaf9af1b309ef0d9bc9965f574edde86f2b 100644
--- a/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java
+++ b/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java
@@ -592,7 +592,7 @@ public abstract class AbstractDiskGraph {
record.read(this.nodeRAF);
Integer inArcCounter = nodes2count.get(record);
if (inArcCounter == null) {
- inArcCounter = new Integer(0);
+ inArcCounter = 0;
}
nodes2count.put(record, inArcCounter + 1);
}
diff --git a/tlatools/src/tlc2/value/impl/LazyValue.java b/tlatools/src/tlc2/value/impl/LazyValue.java
index fe5b1eba3978c9fecdc5ca4e5c9b064a343762c3..29f3fa466354409fb7cdf55e4cd3416568bff435 100644
--- a/tlatools/src/tlc2/value/impl/LazyValue.java
+++ b/tlatools/src/tlc2/value/impl/LazyValue.java
@@ -47,7 +47,7 @@ public class LazyValue extends Value {
public SemanticNode expr;
public Context con;
- private Value val;
+ public Value val;
public LazyValue(SemanticNode expr, Context con, final CostModel cm) {
this(expr, con, true, coverage ? cm.get(expr) : cm);