From 06547ddddd4344bd644064194e0f39c00adf1368 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Feb 2016 08:07:36 +0000 Subject: [PATCH] LTL2NBA: cleanup and activate LTL formula simplification The NBA construction is already exposed with SimpleLTL.toNBA(), use that. Additionally, activate formula simplification. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11187 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/automata/LTL2NBA.java | 26 +++----------------------- 1 file changed, 3 insertions(+), 23 deletions(-) diff --git a/prism/src/automata/LTL2NBA.java b/prism/src/automata/LTL2NBA.java index 3d251892..a517d84d 100644 --- a/prism/src/automata/LTL2NBA.java +++ b/prism/src/automata/LTL2NBA.java @@ -26,10 +26,6 @@ package automata; -import jltl2ba.APSet; -import jltl2ba.Alternating; -import jltl2ba.Buchi; -import jltl2ba.Generalized; import jltl2ba.SimpleLTL; import jltl2dstar.NBA; import parser.Values; @@ -61,24 +57,8 @@ public class LTL2NBA extends PrismComponent throw new PrismNotSupportedException("LTL with time bounds currently not supported for LTL model checking."); } - SimpleLTL ltlSimple = ltl.convertForJltl2ba(); - APSet apset = ltlSimple.getAPs(); - - Alternating a = new Alternating(ltlSimple, apset); - // a.print(System.out); - Generalized g = new Generalized(a); - // g.print(System.out, apset); - Buchi b = new Buchi(g); - // b.print_spin(System.out, apset); - NBA nba = b.toNBA(apset); - // nba.print(System.out); - - // jltl2ba should never produce disjoint NBA, - // i.e., where some states are not reachable - // from the intial state, so we want to fail - // later if the NBA is discovered to be disjoint: - nba.setFailIfDisjoint(true); - - return nba; + // convert to jltl2ba LTL, simplify formula + SimpleLTL ltlSimple = ltl.convertForJltl2ba().simplify(); + return ltlSimple.toNBA(); } }