From 6ff3094b91b306c7f4fdaa22a04bc9db4b0973bb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 14:45:37 +0000 Subject: [PATCH] jltl2dstar: support generation of Rabin and Streett automata. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9602 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jltl2dstar/DRA.java | 82 ++++++++++++++++++++++++----- prism/src/jltl2dstar/LTL2Rabin.java | 49 +++++++++++++++-- 2 files changed, 113 insertions(+), 18 deletions(-) diff --git a/prism/src/jltl2dstar/DRA.java b/prism/src/jltl2dstar/DRA.java index bde3b3a8..c007ad5d 100644 --- a/prism/src/jltl2dstar/DRA.java +++ b/prism/src/jltl2dstar/DRA.java @@ -26,7 +26,9 @@ import java.io.FileWriter; import java.io.PrintStream; import java.util.*; +import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; +import acceptance.AcceptanceStreett; import jltl2ba.APElement; import jltl2ba.APSet; import prism.PrismException; @@ -144,28 +146,54 @@ public class DRA extends DA { } /** - * Convert the DRA from jltl2dstar to PRISM data structures. + * Convert this jltl2dstar deterministic automaton to PRISM data structures. */ - public prism.DA createPrismDRA() throws PrismException + public prism.DA createPrismDA() throws PrismException + { + int numStates = size(); + if (!isStreett()) { + // Rabin + prism.DA draNew; + + draNew = new prism.DA(numStates); + createPrismDA(draNew); + AcceptanceRabin accNew = createRabinAcceptance(); + draNew.setAcceptance(accNew); + + return draNew; + } else { + // Streett + prism.DA dsaNew; + + dsaNew = new prism.DA(numStates); + createPrismDA(dsaNew); + AcceptanceStreett accNew = createStreettAcceptance(); + dsaNew.setAcceptance(accNew); + + return dsaNew; + } + } + + /** + * Convert the state and transition structure of this jltl2dstar deterministic automaton + * to the PRISM data structures. + */ + private void createPrismDA(prism.DA da) throws PrismException { int i, k, numLabels, numStates, src, dest; List apList; BitSet bitset; - RabinAcceptance acc; - prism.DA draNew; - AcceptanceRabin accNew = new AcceptanceRabin(); numLabels = getAPSize(); numStates = size(); - draNew = new prism.DA(numStates); // Copy AP set apList = new ArrayList(numLabels); for (i = 0; i < numLabels; i++) { apList.add(getAPSet().getAP(i)); } - draNew.setAPList(apList); + da.setAPList(apList); // Copy start state - draNew.setStartState(getStartState().getName()); + da.setStartState(getStartState().getName()); // Copy edges for (i = 0; i < numStates; i++) { DA_State cur_state = get(i); @@ -176,23 +204,51 @@ public class DRA extends DA { for (k = 0; k < numLabels; k++) { bitset.set(k, transition.getKey().get(k)); } - draNew.addEdge(src, bitset, dest); + da.addEdge(src, bitset, dest); } } + } + + /** + * Create an AcceptanceRabin acceptance condition from the acceptance condition + * of this jltl2dstar deterministic automaton. + */ + private AcceptanceRabin createRabinAcceptance() throws PrismException { + AcceptanceRabin accNew = new AcceptanceRabin(); + // Copy acceptance pairs - acc = acceptance(); - for (i = 0; i < acc.size(); i++) { + RabinAcceptance acc = acceptance(); + for (int i = 0; i < acc.size(); i++) { // Note: Pairs (U_i,L_i) become (L_i,K_i) in PRISM's notation BitSet newL = (BitSet)acc.getAcceptance_U(i).clone(); BitSet newK = (BitSet)acc.getAcceptance_L(i).clone(); AcceptanceRabin.RabinPair pair = new AcceptanceRabin.RabinPair(newL, newK); accNew.add(pair); } + return accNew; + } + + /** + * Create an AcceptanceStreett acceptance condition from the acceptance condition + * of this jltl2dstar deterministic automaton. + */ + private AcceptanceStreett createStreettAcceptance() throws PrismException { + AcceptanceStreett accNew = new AcceptanceStreett(); - draNew.setAcceptance(accNew); + // Copy acceptance pairs, interpreting the RabinAcceptance from this automaton + // as Streett acceptance + RabinAcceptance acc = acceptance(); + for (int i = 0; i < acc.size(); i++) { + // Note: Pairs (U_i,L_i) become (G_i,R_i) in PRISM's notation + BitSet newR = (BitSet)acc.getAcceptance_L(i).clone(); + BitSet newG = (BitSet)acc.getAcceptance_U(i).clone(); + AcceptanceStreett.StreettPair pair = new AcceptanceStreett.StreettPair(newR, newG); - return draNew; + accNew.add(pair); + } + return accNew; } + // public DRA calculateUnionStuttered(DRA other, // StutterSensitivenessInformation stutter_information, diff --git a/prism/src/jltl2dstar/LTL2Rabin.java b/prism/src/jltl2dstar/LTL2Rabin.java index 131bc0d2..17f4918e 100644 --- a/prism/src/jltl2dstar/LTL2Rabin.java +++ b/prism/src/jltl2dstar/LTL2Rabin.java @@ -27,16 +27,46 @@ import prism.PrismException; import java.util.BitSet; +import prism.DA; +import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; +import acceptance.AcceptanceStreett; +import acceptance.AcceptanceType; public class LTL2Rabin { + + @SuppressWarnings("unchecked") + public static prism.DA ltl2rabin(SimpleLTL ltlFormula) throws PrismException + { + DA result; + result = ltl2da(ltlFormula, AcceptanceType.RABIN); + return (DA)result; + } + + @SuppressWarnings("unchecked") + public static prism.DA ltl2streett(SimpleLTL ltlFormula) throws PrismException + { + DA result; + result = ltl2da(ltlFormula, AcceptanceType.STREETT); + return (DA)result; + } - public static prism.DA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { + public static prism.DA ltl2da(SimpleLTL ltlFormula, AcceptanceType... allowedAcceptance) throws PrismException + { SimpleLTL ltl = ltlFormula.simplify(); - return ltl2rabin(ltl, ltl.getAPs()).createPrismDRA(); + + boolean allowRabin=AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN); + boolean allowStreett=AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT); + + if (allowRabin && allowStreett) { + // currently, disable opportunistic generation of either Rabin or Streett automaton + allowStreett = false; + } + + return ltl2da(ltl, ltl.getAPs(), allowRabin, allowStreett).createPrismDA(); } - - private static DRA ltl2rabin(SimpleLTL ltl, APSet apset) throws PrismException { + + private static DRA ltl2da(SimpleLTL ltl, APSet apset, boolean allowRabin, boolean allowStreett) throws PrismException { DRA dra = null; Options_LTL2DRA opt_ltl2rabin = new Options_LTL2DRA(); @@ -57,7 +87,16 @@ public class LTL2Rabin { // opt_ltl2dstar.scheck_path=""; // stuttercheck_timekeep = true; // stuttercheck_print = false; - opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.RABIN; + if (allowRabin) { + if (allowStreett) + opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.RABIN_AND_STREETT; + else + opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.RABIN; + } else if (allowStreett) { + opt_ltl2rabin.automata = Options_LTL2DRA.AutomataType.STREETT; + } else { + throw new PrismException("Can not generate deterministic automata if neither Rabin nor Streett is allowed."); + } opt_ltl2rabin.detailed_states = false; opt_ltl2rabin.verbose_scheduler = false; opt_ltl2rabin.opt_safra.opt_accloop = true;