From 9493710a0f0ec838290e418a51d7f55b01b40a2a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 24 Aug 2015 14:38:39 +0000 Subject: [PATCH] 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 --- prism/src/parser/PrismParser.java | 144 ++++++++++-------- prism/src/parser/PrismParser.jj | 11 ++ prism/src/parser/PrismParserTokenManager.java | 1 + 3 files changed, 90 insertions(+), 66 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 3fb86b5c..33445136 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -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; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index ee8bccdf..bcdc3eae 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -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); } diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java index dc522b57..190db239 100644 --- a/prism/src/parser/PrismParserTokenManager.java +++ b/prism/src/parser/PrismParserTokenManager.java @@ -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.*;