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

Add some additional functionality to the LTL test mode of PrismParser. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10563 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
0d5cc45f53
commit
9493710a0f
3 changed files with 90 additions and 66 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 144
      prism/src/parser/PrismParser.java
  2. 11
      prism/src/parser/PrismParser.jj
  3. 1
      prism/src/parser/PrismParserTokenManager.java

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

@ -5,6 +5,7 @@ import java.io.*;
import java.util.List;
import java.util.ArrayList;
import jltl2ba.SimpleLTL;
import parser.BooleanUtils;
import parser.ast.*;
import parser.type.*;
@ -85,18 +86,29 @@ public class PrismParser implements PrismParserConstants {
System.out.println("LTL formula: " + expr.toString());
System.out.print("Tree:\u005cn=====\u005cn" + expr.toTreeString());
expr.typeCheck();
expr.semanticCheck();
//expr.semanticCheck();
System.out.println("Type: " + expr.getType().getTypeString());
boolean pnf = Expression.isPositiveNormalFormLTL(expr);
System.out.println("Positive normal form: " + pnf);
if (!pnf) {
System.out.println("Positive normal form conversion: " + BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy()));
}
Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() {
public Object visit(ExpressionVar e) throws PrismLangException
{
return new parser.ast.ExpressionLabel(e.getName());
}
});
SimpleLTL sltl = expr2.convertForJltl2ba();
System.out.println("LBT: " + sltl.toStringLBT());
System.out.println("Spot: " + sltl.toStringSpot());
System.out.println("Spin: " + sltl.toStringSpin());
} else {
System.out.println("Unknown switch"); System.exit(1);
}
}
catch (PrismLangException e) {
e.printStackTrace();
System.out.println("Error in "+src+": " + e.getMessage()+"."); System.exit(1);
}
catch (FileNotFoundException e) {
@ -3477,64 +3489,6 @@ public class PrismParser implements PrismParserConstants {
finally { jj_save(17, xla); }
}
static private boolean jj_3R_165() {
if (jj_scan_token(P)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_190()) jj_scanpos = xsp;
xsp = jj_scanpos;
if (jj_3R_191()) {
jj_scanpos = xsp;
if (jj_3R_192()) {
jj_scanpos = xsp;
if (jj_3R_193()) {
jj_scanpos = xsp;
if (jj_3R_194()) return true;
}
}
}
return false;
}
static private boolean jj_3R_62() {
if (jj_scan_token(U)) return true;
return false;
}
static private boolean jj_3R_147() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_165()) {
jj_scanpos = xsp;
if (jj_3R_166()) {
jj_scanpos = xsp;
if (jj_3R_167()) return true;
}
}
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_38()) return true;
xsp = jj_scanpos;
if (jj_3R_168()) jj_scanpos = xsp;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static private boolean jj_3R_56() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_62()) {
jj_scanpos = xsp;
if (jj_3R_63()) {
jj_scanpos = xsp;
if (jj_3R_64()) return true;
}
}
xsp = jj_scanpos;
if (jj_3R_65()) jj_scanpos = xsp;
if (jj_3R_55()) return true;
return false;
}
static private boolean jj_3R_189() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_38()) return true;
@ -4337,13 +4291,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3_1() {
if (jj_scan_token(MODULE)) return true;
if (jj_3R_29()) return true;
if (jj_scan_token(EQ)) return true;
return false;
}
static private boolean jj_3R_117() {
Token xsp;
xsp = jj_scanpos;
@ -4355,6 +4302,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3_1() {
if (jj_scan_token(MODULE)) return true;
if (jj_3R_29()) return true;
if (jj_scan_token(EQ)) return true;
return false;
}
static private boolean jj_3R_201() {
if (jj_3R_33()) return true;
return false;
@ -5103,6 +5057,64 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_165() {
if (jj_scan_token(P)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_190()) jj_scanpos = xsp;
xsp = jj_scanpos;
if (jj_3R_191()) {
jj_scanpos = xsp;
if (jj_3R_192()) {
jj_scanpos = xsp;
if (jj_3R_193()) {
jj_scanpos = xsp;
if (jj_3R_194()) return true;
}
}
}
return false;
}
static private boolean jj_3R_62() {
if (jj_scan_token(U)) return true;
return false;
}
static private boolean jj_3R_147() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_165()) {
jj_scanpos = xsp;
if (jj_3R_166()) {
jj_scanpos = xsp;
if (jj_3R_167()) return true;
}
}
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_38()) return true;
xsp = jj_scanpos;
if (jj_3R_168()) jj_scanpos = xsp;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static private boolean jj_3R_56() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_62()) {
jj_scanpos = xsp;
if (jj_3R_63()) {
jj_scanpos = xsp;
if (jj_3R_64()) return true;
}
}
xsp = jj_scanpos;
if (jj_3R_65()) jj_scanpos = xsp;
if (jj_3R_55()) return true;
return false;
}
static private boolean jj_initialized_once = false;
/** Generated Token Manager. */
static public PrismParserTokenManager token_source;

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

@ -37,6 +37,7 @@ import java.io.*;
import java.util.List;
import java.util.ArrayList;
import jltl2ba.SimpleLTL;
import parser.BooleanUtils;
import parser.ast.*;
import parser.type.*;
@ -125,6 +126,16 @@ public class PrismParser
if (!pnf) {
System.out.println("Positive normal form conversion: " + BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy()));
}
Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() {
public Object visit(ExpressionVar e) throws PrismLangException
{
return new parser.ast.ExpressionLabel(e.getName());
}
});
SimpleLTL sltl = expr2.convertForJltl2ba();
System.out.println("LBT: " + sltl.toStringLBT());
System.out.println("Spot: " + sltl.toStringSpot());
System.out.println("Spin: " + sltl.toStringSpin());
} else {
System.out.println("Unknown switch"); System.exit(1);
}

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

@ -3,6 +3,7 @@ package parser;
import java.io.*;
import java.util.List;
import java.util.ArrayList;
import jltl2ba.SimpleLTL;
import parser.BooleanUtils;
import parser.ast.*;
import parser.type.*;

Write Preview
Loading…
Cancel
Save