s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Removed restriction that type keyword must be first thing in model file. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@56 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 20 years ago
parent
031c8968b1
commit
52c1294341
4 changed files with 119 additions and 69 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 120
      prism/src/parser/PrismParser.java
  2. 6
      prism/src/parser/PrismParser.jj
  3. 6
      prism/src/parser/PrismParserTokenManager.java
  4. 56
      prism/src/parser/SimpleCharStream.java

120
prism/src/parser/PrismParser.java
View File

@ -302,19 +302,18 @@ public class PrismParser implements PrismParserConstants {
// modules file // modules file
static final public ModulesFile ModulesFile() throws ParseException { static final public ModulesFile ModulesFile() throws ParseException {
int type = 0; int type = 0;
if (jj_2_1(2147483647)) {
type = ModulesFileType();
} else {
;
}
int typeSpecs = 0;
label_1: label_1:
while (true) { while (true) {
if (jj_2_2(2147483647)) {
if (jj_2_1(2147483647)) {
; ;
} else { } else {
break label_1; break label_1;
} }
if (jj_2_3(2147483647)) {
if (jj_2_2(2147483647)) {
type = ModulesFileType();
typeSpecs++;
} else if (jj_2_3(2147483647)) {
FormulaDef(); FormulaDef();
} else if (jj_2_4(2147483647)) { } else if (jj_2_4(2147483647)) {
ConstantDef(); ConstantDef();
@ -336,6 +335,8 @@ public class PrismParser implements PrismParserConstants {
} }
} }
jj_consume_token(0); jj_consume_token(0);
if (typeSpecs > 1) {if (true) throw new ParseException("There were multiple type declarations");}
// create new ModulesFile object // create new ModulesFile object
ModulesFile modulesFile = new ModulesFile(); ModulesFile modulesFile = new ModulesFile();
@ -3662,16 +3663,6 @@ public class PrismParser implements PrismParserConstants {
finally { jj_save(168, xla); } finally { jj_save(168, xla); }
} }
static final private boolean jj_3_66() {
Token xsp;
xsp = jj_scanpos;
if (jj_3_69()) {
jj_scanpos = xsp;
if (jj_3_70()) return true;
}
return false;
}
static final private boolean jj_3_34() { static final private boolean jj_3_34() {
if (jj_3R_38()) return true; if (jj_3R_38()) return true;
return false; return false;
@ -4508,6 +4499,11 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_10() {
if (jj_3R_32()) return true;
return false;
}
static final private boolean jj_3R_69() { static final private boolean jj_3R_69() {
if (jj_3R_88()) return true; if (jj_3R_88()) return true;
return false; return false;
@ -4557,6 +4553,11 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_9() {
if (jj_3R_31()) return true;
return false;
}
static final private boolean jj_3_144() { static final private boolean jj_3_144() {
if (jj_scan_token(MAX)) return true; if (jj_scan_token(MAX)) return true;
return false; return false;
@ -4640,6 +4641,11 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_8() {
if (jj_3R_30()) return true;
return false;
}
static final private boolean jj_3_122() { static final private boolean jj_3_122() {
if (jj_3R_68()) return true; if (jj_3R_68()) return true;
return false; return false;
@ -4689,11 +4695,6 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_10() {
if (jj_3R_32()) return true;
return false;
}
static final private boolean jj_3_46() { static final private boolean jj_3_46() {
if (jj_scan_token(LPARENTH)) return true; if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_42()) return true; if (jj_3R_42()) return true;
@ -4794,6 +4795,11 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_7() {
if (jj_3R_29()) return true;
return false;
}
static final private boolean jj_3R_66() { static final private boolean jj_3R_66() {
Token xsp; Token xsp;
xsp = jj_scanpos; xsp = jj_scanpos;
@ -4829,11 +4835,6 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_9() {
if (jj_3R_31()) return true;
return false;
}
static final private boolean jj_3_140() { static final private boolean jj_3_140() {
Token xsp; Token xsp;
xsp = jj_scanpos; xsp = jj_scanpos;
@ -4845,6 +4846,11 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_6() {
if (jj_3R_28()) return true;
return false;
}
static final private boolean jj_3_45() { static final private boolean jj_3_45() {
if (jj_scan_token(TRUE)) return true; if (jj_scan_token(TRUE)) return true;
return false; return false;
@ -4889,13 +4895,13 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_8() {
if (jj_3R_30()) return true;
static final private boolean jj_3R_34() {
if (jj_3R_59()) return true;
return false; return false;
} }
static final private boolean jj_3R_34() {
if (jj_3R_59()) return true;
static final private boolean jj_3_5() {
if (jj_3R_27()) return true;
return false; return false;
} }
@ -4951,8 +4957,8 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_7() {
if (jj_3R_29()) return true;
static final private boolean jj_3_4() {
if (jj_3R_26()) return true;
return false; return false;
} }
@ -4980,8 +4986,8 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_6() {
if (jj_3R_28()) return true;
static final private boolean jj_3_3() {
if (jj_3R_25()) return true;
return false; return false;
} }
@ -5033,11 +5039,6 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_5() {
if (jj_3R_27()) return true;
return false;
}
static final private boolean jj_3_111() { static final private boolean jj_3_111() {
if (jj_3R_64()) return true; if (jj_3R_64()) return true;
return false; return false;
@ -5072,11 +5073,6 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_4() {
if (jj_3R_26()) return true;
return false;
}
static final private boolean jj_3_118() { static final private boolean jj_3_118() {
if (jj_3R_66()) return true; if (jj_3R_66()) return true;
return false; return false;
@ -5114,9 +5110,11 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_2() {
static final private boolean jj_3_1() {
Token xsp; Token xsp;
xsp = jj_scanpos; xsp = jj_scanpos;
if (jj_3_2()) {
jj_scanpos = xsp;
if (jj_3_3()) { if (jj_3_3()) {
jj_scanpos = xsp; jj_scanpos = xsp;
if (jj_3_4()) { if (jj_3_4()) {
@ -5139,15 +5137,11 @@ public class PrismParser implements PrismParserConstants {
} }
} }
} }
}
return false; return false;
} }
static final private boolean jj_3_3() {
if (jj_3R_25()) return true;
return false;
}
static final private boolean jj_3_1() {
static final private boolean jj_3_2() {
if (jj_3R_24()) return true; if (jj_3R_24()) return true;
return false; return false;
} }
@ -5535,6 +5529,16 @@ public class PrismParser implements PrismParserConstants {
return false; return false;
} }
static final private boolean jj_3_66() {
Token xsp;
xsp = jj_scanpos;
if (jj_3_69()) {
jj_scanpos = xsp;
if (jj_3_70()) return true;
}
return false;
}
static private boolean jj_initialized_once = false; static private boolean jj_initialized_once = false;
static public PrismParserTokenManager token_source; static public PrismParserTokenManager token_source;
static SimpleCharStream jj_input_stream; static SimpleCharStream jj_input_stream;
@ -5568,6 +5572,9 @@ public class PrismParser implements PrismParserConstants {
static private int jj_gc = 0; static private int jj_gc = 0;
public PrismParser(java.io.InputStream stream) { public PrismParser(java.io.InputStream stream) {
this(stream, null);
}
public PrismParser(java.io.InputStream stream, String encoding) {
if (jj_initialized_once) { if (jj_initialized_once) {
System.out.println("ERROR: Second call to constructor of static parser. You must"); System.out.println("ERROR: Second call to constructor of static parser. You must");
System.out.println(" either use ReInit() or set the JavaCC option STATIC to false"); System.out.println(" either use ReInit() or set the JavaCC option STATIC to false");
@ -5575,7 +5582,7 @@ public class PrismParser implements PrismParserConstants {
throw new Error(); throw new Error();
} }
jj_initialized_once = true; jj_initialized_once = true;
jj_input_stream = new SimpleCharStream(stream, 1, 1);
try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
token_source = new PrismParserTokenManager(jj_input_stream); token_source = new PrismParserTokenManager(jj_input_stream);
token = new Token(); token = new Token();
jj_ntk = -1; jj_ntk = -1;
@ -5585,7 +5592,10 @@ public class PrismParser implements PrismParserConstants {
} }
static public void ReInit(java.io.InputStream stream) { static public void ReInit(java.io.InputStream stream) {
jj_input_stream.ReInit(stream, 1, 1);
ReInit(stream, null);
}
static public void ReInit(java.io.InputStream stream, String encoding) {
try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
token_source.ReInit(jj_input_stream); token_source.ReInit(jj_input_stream);
token = new Token(); token = new Token();
jj_ntk = -1; jj_ntk = -1;
@ -5802,6 +5812,7 @@ public class PrismParser implements PrismParserConstants {
static final private void jj_rescan_token() { static final private void jj_rescan_token() {
jj_rescan = true; jj_rescan = true;
for (int i = 0; i < 169; i++) { for (int i = 0; i < 169; i++) {
try {
JJCalls p = jj_2_rtns[i]; JJCalls p = jj_2_rtns[i];
do { do {
if (p.gen > jj_gen) { if (p.gen > jj_gen) {
@ -5980,6 +5991,7 @@ public class PrismParser implements PrismParserConstants {
} }
p = p.next; p = p.next;
} while (p != null); } while (p != null);
} catch(LookaheadSuccess ls) { }
} }
jj_rescan = false; jj_rescan = false;
} }

6
prism/src/parser/PrismParser.jj
View File

@ -441,14 +441,16 @@ TOKEN :
ModulesFile ModulesFile() : ModulesFile ModulesFile() :
{ {
int type = 0; int type = 0;
int typeSpecs = 0;
} }
{ {
( (
( type=ModulesFileType() )?
( FormulaDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )*
( ( type=ModulesFileType() {typeSpecs++;} ) | FormulaDef() | ConstantDef() | GlobalDecl() | Module() | RenamedModule() | SystemComp() | RewardStruct() | Init() )*
<EOF> <EOF>
) )
{ {
if (typeSpecs > 1) throw new ParseException("There were multiple type declarations");
// create new ModulesFile object // create new ModulesFile object
ModulesFile modulesFile = new ModulesFile(); ModulesFile modulesFile = new ModulesFile();

6
prism/src/parser/PrismParserTokenManager.java
View File

@ -1061,14 +1061,12 @@ static protected SimpleCharStream input_stream;
static private final int[] jjrounds = new int[17]; static private final int[] jjrounds = new int[17];
static private final int[] jjstateSet = new int[34]; static private final int[] jjstateSet = new int[34];
static protected char curChar; static protected char curChar;
public PrismParserTokenManager(SimpleCharStream stream)
{
public PrismParserTokenManager(SimpleCharStream stream){
if (input_stream != null) if (input_stream != null)
throw new TokenMgrError("ERROR: Second call to constructor of static lexer. You must use ReInit() to initialize the static variables.", TokenMgrError.STATIC_LEXER_ERROR); throw new TokenMgrError("ERROR: Second call to constructor of static lexer. You must use ReInit() to initialize the static variables.", TokenMgrError.STATIC_LEXER_ERROR);
input_stream = stream; input_stream = stream;
} }
public PrismParserTokenManager(SimpleCharStream stream, int lexState)
{
public PrismParserTokenManager(SimpleCharStream stream, int lexState){
this(stream); this(stream);
SwitchTo(lexState); SwitchTo(lexState);
} }

56
prism/src/parser/SimpleCharStream.java
View File

@ -1,4 +1,4 @@
/* Generated By:JavaCC: Do not edit this line. SimpleCharStream.java Version 3.0 */
/* Generated By:JavaCC: Do not edit this line. SimpleCharStream.java Version 4.0 */
package parser; package parser;
/** /**
@ -27,6 +27,11 @@ public class SimpleCharStream
static protected char[] buffer; static protected char[] buffer;
static protected int maxNextCharInd = 0; static protected int maxNextCharInd = 0;
static protected int inBuf = 0; static protected int inBuf = 0;
static protected int tabSize = 8;
static protected void setTabSize(int i) { tabSize = i; }
static protected int getTabSize(int i) { return tabSize; }
static protected void ExpandBuff(boolean wrapAround) static protected void ExpandBuff(boolean wrapAround)
{ {
@ -162,7 +167,7 @@ public class SimpleCharStream
break; break;
case '\t' : case '\t' :
column--; column--;
column += (8 - (column & 07));
column += (tabSize - (column % tabSize));
break; break;
default : default :
break; break;
@ -252,7 +257,7 @@ public class SimpleCharStream
} }
public SimpleCharStream(java.io.Reader dstream, int startline, public SimpleCharStream(java.io.Reader dstream, int startline,
int startcolumn)
int startcolumn)
{ {
this(dstream, startline, startcolumn, 4096); this(dstream, startline, startcolumn, 4096);
} }
@ -281,7 +286,7 @@ public class SimpleCharStream
} }
public void ReInit(java.io.Reader dstream, int startline, public void ReInit(java.io.Reader dstream, int startline,
int startcolumn)
int startcolumn)
{ {
ReInit(dstream, startline, startcolumn, 4096); ReInit(dstream, startline, startcolumn, 4096);
} }
@ -290,35 +295,68 @@ public class SimpleCharStream
{ {
ReInit(dstream, 1, 1, 4096); ReInit(dstream, 1, 1, 4096);
} }
public SimpleCharStream(java.io.InputStream dstream, String encoding, int startline,
int startcolumn, int buffersize) throws java.io.UnsupportedEncodingException
{
this(encoding == null ? new java.io.InputStreamReader(dstream) : new java.io.InputStreamReader(dstream, encoding), startline, startcolumn, buffersize);
}
public SimpleCharStream(java.io.InputStream dstream, int startline, public SimpleCharStream(java.io.InputStream dstream, int startline,
int startcolumn, int buffersize) int startcolumn, int buffersize)
{ {
this(new java.io.InputStreamReader(dstream), startline, startcolumn, 4096);
this(new java.io.InputStreamReader(dstream), startline, startcolumn, buffersize);
}
public SimpleCharStream(java.io.InputStream dstream, String encoding, int startline,
int startcolumn) throws java.io.UnsupportedEncodingException
{
this(dstream, encoding, startline, startcolumn, 4096);
} }
public SimpleCharStream(java.io.InputStream dstream, int startline, public SimpleCharStream(java.io.InputStream dstream, int startline,
int startcolumn)
int startcolumn)
{ {
this(dstream, startline, startcolumn, 4096); this(dstream, startline, startcolumn, 4096);
} }
public SimpleCharStream(java.io.InputStream dstream, String encoding) throws java.io.UnsupportedEncodingException
{
this(dstream, encoding, 1, 1, 4096);
}
public SimpleCharStream(java.io.InputStream dstream) public SimpleCharStream(java.io.InputStream dstream)
{ {
this(dstream, 1, 1, 4096); this(dstream, 1, 1, 4096);
} }
public void ReInit(java.io.InputStream dstream, String encoding, int startline,
int startcolumn, int buffersize) throws java.io.UnsupportedEncodingException
{
ReInit(encoding == null ? new java.io.InputStreamReader(dstream) : new java.io.InputStreamReader(dstream, encoding), startline, startcolumn, buffersize);
}
public void ReInit(java.io.InputStream dstream, int startline, public void ReInit(java.io.InputStream dstream, int startline,
int startcolumn, int buffersize) int startcolumn, int buffersize)
{ {
ReInit(new java.io.InputStreamReader(dstream), startline, startcolumn, 4096);
ReInit(new java.io.InputStreamReader(dstream), startline, startcolumn, buffersize);
}
public void ReInit(java.io.InputStream dstream, String encoding) throws java.io.UnsupportedEncodingException
{
ReInit(dstream, encoding, 1, 1, 4096);
} }
public void ReInit(java.io.InputStream dstream) public void ReInit(java.io.InputStream dstream)
{ {
ReInit(dstream, 1, 1, 4096); ReInit(dstream, 1, 1, 4096);
} }
public void ReInit(java.io.InputStream dstream, String encoding, int startline,
int startcolumn) throws java.io.UnsupportedEncodingException
{
ReInit(dstream, encoding, startline, startcolumn, 4096);
}
public void ReInit(java.io.InputStream dstream, int startline, public void ReInit(java.io.InputStream dstream, int startline,
int startcolumn)
int startcolumn)
{ {
ReInit(dstream, startline, startcolumn, 4096); ReInit(dstream, startline, startcolumn, 4096);
} }
@ -355,7 +393,7 @@ public class SimpleCharStream
} }
/** /**
* Method to adjust line and column numbers for the start of a token.<BR>
* Method to adjust line and column numbers for the start of a token.
*/ */
static public void adjustBeginLineColumn(int newLine, int newCol) static public void adjustBeginLineColumn(int newLine, int newCol)
{ {

Write Preview
Loading…
Cancel
Save