Browse Source

LTL2DA.main: Don't print formulas (this allows use in automatic LTL->automata test tools such as Spot's ltlcross)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12047 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
commit
9ffb77d859
  1. 6
      prism/src/automata/LTL2DA.java

6
prism/src/automata/LTL2DA.java

@ -342,11 +342,11 @@ public class LTL2DA extends PrismComponent
System.out.println("LTL: " + expr);*/ System.out.println("LTL: " + expr);*/
// Convert to Expression (from LBT format) // Convert to Expression (from LBT format)
String ltl = args[0];
// String ltl = args[0];
SimpleLTL sltl = SimpleLTL.parseFormulaLBT(args[0]); SimpleLTL sltl = SimpleLTL.parseFormulaLBT(args[0]);
Expression expr = Expression.createFromJltl2ba(sltl); Expression expr = Expression.createFromJltl2ba(sltl);
System.out.println("LBT: " + ltl);
System.out.println("LTL: " + expr);
// System.out.println("LBT: " + ltl);
// System.out.println("LTL: " + expr);
// Build/export DA // Build/export DA
LTL2DA ltl2da = new LTL2DA(new PrismComponent()); LTL2DA ltl2da = new LTL2DA(new PrismComponent());

Loading…
Cancel
Save