From 4bb807cb8ee66f74be63a281b32551561f3b86a0 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 8 Jul 2015 12:04:03 +0000 Subject: [PATCH] Code rearrange: move automata stuff to a separate "automata" package. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10234 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/{prism => automata}/DA.java | 5 ++++- .../{prism => automata}/DASimplifyAcceptance.java | 3 ++- prism/src/{prism => automata}/HOAF2DA.java | 3 ++- prism/src/{prism => automata}/LTL2DA.java | 6 +++++- prism/src/{prism => automata}/LTL2RabinLibrary.java | 7 ++++++- prism/src/{prism => automata}/LTSFromDA.java | 5 ++++- prism/src/explicit/LTLModelChecker.java | 5 ++--- prism/src/jltl2dstar/DRA.java | 12 ++++++------ prism/src/jltl2dstar/LTL2Rabin.java | 8 ++++---- prism/src/prism/LTLModelChecker.java | 1 + prism/src/prism/MultiObjModelChecker.java | 2 ++ prism/src/prism/NondetModelChecker.java | 2 ++ prism/src/prism/ProbModelChecker.java | 2 ++ 13 files changed, 42 insertions(+), 19 deletions(-) rename prism/src/{prism => automata}/DA.java (98%) rename prism/src/{prism => automata}/DASimplifyAcceptance.java (98%) rename prism/src/{prism => automata}/HOAF2DA.java (99%) rename prism/src/{prism => automata}/LTL2DA.java (98%) rename prism/src/{prism => automata}/LTL2RabinLibrary.java (99%) rename prism/src/{prism => automata}/LTSFromDA.java (98%) diff --git a/prism/src/prism/DA.java b/prism/src/automata/DA.java similarity index 98% rename from prism/src/prism/DA.java rename to prism/src/automata/DA.java index 70d61c03..3d0733c4 100644 --- a/prism/src/prism/DA.java +++ b/prism/src/automata/DA.java @@ -27,11 +27,14 @@ // //============================================================================== -package prism; +package automata; import java.io.PrintStream; import java.util.*; +import prism.PrismException; +import prism.PrismLog; +import prism.PrismPrintStreamLog; import jltl2ba.APElement; import jltl2ba.APElementIterator; import acceptance.AcceptanceOmega; diff --git a/prism/src/prism/DASimplifyAcceptance.java b/prism/src/automata/DASimplifyAcceptance.java similarity index 98% rename from prism/src/prism/DASimplifyAcceptance.java rename to prism/src/automata/DASimplifyAcceptance.java index 2a61152d..8d0ecfe3 100644 --- a/prism/src/prism/DASimplifyAcceptance.java +++ b/prism/src/automata/DASimplifyAcceptance.java @@ -1,7 +1,8 @@ -package prism; +package automata; import java.util.BitSet; +import prism.PrismException; import explicit.SCCComputer; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; diff --git a/prism/src/prism/HOAF2DA.java b/prism/src/automata/HOAF2DA.java similarity index 99% rename from prism/src/prism/HOAF2DA.java rename to prism/src/automata/HOAF2DA.java index 78230c16..6b694b0b 100644 --- a/prism/src/prism/HOAF2DA.java +++ b/prism/src/automata/HOAF2DA.java @@ -26,13 +26,14 @@ //============================================================================== -package prism; +package automata; import java.util.ArrayList; import java.util.BitSet; import java.util.List; import java.util.Set; +import prism.PrismException; import jhoafparser.ast.AtomAcceptance; import jhoafparser.ast.AtomLabel; import jhoafparser.ast.BooleanExpression; diff --git a/prism/src/prism/LTL2DA.java b/prism/src/automata/LTL2DA.java similarity index 98% rename from prism/src/prism/LTL2DA.java rename to prism/src/automata/LTL2DA.java index b980fca6..cc77562c 100644 --- a/prism/src/prism/LTL2DA.java +++ b/prism/src/automata/LTL2DA.java @@ -25,7 +25,7 @@ // //============================================================================== -package prism; +package automata; import java.io.File; import java.io.FileInputStream; @@ -48,6 +48,10 @@ import jltl2ba.SimpleLTL; import jltl2dstar.LTL2Rabin; import parser.Values; import parser.ast.Expression; +import prism.PrismComponent; +import prism.PrismException; +import prism.PrismNotSupportedException; +import prism.PrismSettings; /** * Infrastructure for constructing deterministic automata for LTL formulas. diff --git a/prism/src/prism/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java similarity index 99% rename from prism/src/prism/LTL2RabinLibrary.java rename to prism/src/automata/LTL2RabinLibrary.java index 1ce216f2..c0f594ac 100644 --- a/prism/src/prism/LTL2RabinLibrary.java +++ b/prism/src/automata/LTL2RabinLibrary.java @@ -25,7 +25,7 @@ // //============================================================================== -package prism; +package automata; import java.io.*; import java.util.*; @@ -36,6 +36,11 @@ import parser.Values; import parser.ast.*; import parser.visitor.ASTTraverse; import parser.visitor.ASTTraverseModify; +import prism.IntegerBound; +import prism.Prism; +import prism.PrismException; +import prism.PrismLangException; +import prism.PrismNotSupportedException; /** * LTL-to-DRA conversion via diff --git a/prism/src/prism/LTSFromDA.java b/prism/src/automata/LTSFromDA.java similarity index 98% rename from prism/src/prism/LTSFromDA.java rename to prism/src/automata/LTSFromDA.java index 7eb3011e..5da6fcb2 100644 --- a/prism/src/prism/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -24,13 +24,16 @@ // //============================================================================== -package prism; +package automata; import java.util.BitSet; import java.util.HashSet; import java.util.Iterator; import java.util.Set; +import prism.ModelType; +import prism.PrismException; +import prism.PrismLog; import strat.MDStrategy; import explicit.LTS; import explicit.Model; diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index cb6cce1b..4786882c 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -45,8 +45,6 @@ import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.type.TypeBool; import parser.type.TypePathBool; -import prism.DA; -import prism.LTL2DA; import prism.ModelType; import prism.PrismComponent; import prism.PrismException; @@ -58,7 +56,8 @@ import acceptance.AcceptanceGenRabin; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; import acceptance.AcceptanceType; - +import automata.DA; +import automata.LTL2DA; import common.IterableStateSet; /** diff --git a/prism/src/jltl2dstar/DRA.java b/prism/src/jltl2dstar/DRA.java index c007ad5d..cd48db92 100644 --- a/prism/src/jltl2dstar/DRA.java +++ b/prism/src/jltl2dstar/DRA.java @@ -148,14 +148,14 @@ public class DRA extends DA { /** * Convert this jltl2dstar deterministic automaton to PRISM data structures. */ - public prism.DA createPrismDA() throws PrismException + public automata.DA createPrismDA() throws PrismException { int numStates = size(); if (!isStreett()) { // Rabin - prism.DA draNew; + automata.DA draNew; - draNew = new prism.DA(numStates); + draNew = new automata.DA(numStates); createPrismDA(draNew); AcceptanceRabin accNew = createRabinAcceptance(); draNew.setAcceptance(accNew); @@ -163,9 +163,9 @@ public class DRA extends DA { return draNew; } else { // Streett - prism.DA dsaNew; + automata.DA dsaNew; - dsaNew = new prism.DA(numStates); + dsaNew = new automata.DA(numStates); createPrismDA(dsaNew); AcceptanceStreett accNew = createStreettAcceptance(); dsaNew.setAcceptance(accNew); @@ -178,7 +178,7 @@ public class DRA extends DA { * Convert the state and transition structure of this jltl2dstar deterministic automaton * to the PRISM data structures. */ - private void createPrismDA(prism.DA da) throws PrismException + private void createPrismDA(automata.DA da) throws PrismException { int i, k, numLabels, numStates, src, dest; List apList; diff --git a/prism/src/jltl2dstar/LTL2Rabin.java b/prism/src/jltl2dstar/LTL2Rabin.java index 17f4918e..74e0d71c 100644 --- a/prism/src/jltl2dstar/LTL2Rabin.java +++ b/prism/src/jltl2dstar/LTL2Rabin.java @@ -27,16 +27,16 @@ import prism.PrismException; import java.util.BitSet; -import prism.DA; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; import acceptance.AcceptanceStreett; import acceptance.AcceptanceType; +import automata.DA; public class LTL2Rabin { @SuppressWarnings("unchecked") - public static prism.DA ltl2rabin(SimpleLTL ltlFormula) throws PrismException + public static automata.DA ltl2rabin(SimpleLTL ltlFormula) throws PrismException { DA result; result = ltl2da(ltlFormula, AcceptanceType.RABIN); @@ -44,14 +44,14 @@ public class LTL2Rabin { } @SuppressWarnings("unchecked") - public static prism.DA ltl2streett(SimpleLTL ltlFormula) throws PrismException + public static automata.DA ltl2streett(SimpleLTL ltlFormula) throws PrismException { DA result; result = ltl2da(ltlFormula, AcceptanceType.STREETT); return (DA)result; } - public static prism.DA ltl2da(SimpleLTL ltlFormula, AcceptanceType... allowedAcceptance) throws PrismException + public static automata.DA ltl2da(SimpleLTL ltlFormula, AcceptanceType... allowedAcceptance) throws PrismException { SimpleLTL ltl = ltlFormula.simplify(); diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 0f58c6bb..3dab3277 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -37,6 +37,7 @@ import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; import acceptance.AcceptanceRabinDD; +import automata.DA; import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 6c9f3c33..6c0e27f4 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -36,6 +36,8 @@ import java.util.List; import java.util.Vector; import acceptance.AcceptanceRabin; +import automata.DA; +import automata.LTL2DA; import parser.ast.Expression; import parser.ast.RelOp; import dv.DoubleVector; diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index fce4a4ad..a657bbb3 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -39,6 +39,8 @@ import acceptance.AcceptanceRabin; import acceptance.AcceptanceRabinDD; import acceptance.AcceptanceReachDD; import acceptance.AcceptanceType; +import automata.DA; +import automata.LTL2DA; import odd.ODDUtils; import jdd.*; import dv.*; diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 8f3601d0..241c3d64 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -38,6 +38,8 @@ import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceReachDD; import acceptance.AcceptanceType; +import automata.DA; +import automata.LTL2DA; import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars;