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/DA.java → 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;

prism/src/prism/DASimplifyAcceptance.java → 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;

prism/src/prism/HOAF2DA.java → 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;

prism/src/prism/LTL2DA.java → 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.

prism/src/prism/LTL2RabinLibrary.java → 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

prism/src/prism/LTSFromDA.java → 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;

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;
 
 /**

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<BitSet,? extends AcceptanceOmega> createPrismDA() throws PrismException
+	public automata.DA<BitSet,? extends AcceptanceOmega> createPrismDA() throws PrismException
 	{
 		int numStates = size();
 		if (!isStreett()) {
 			// Rabin
-			prism.DA<BitSet, AcceptanceRabin> draNew;
+			automata.DA<BitSet, AcceptanceRabin> draNew;
 
-			draNew = new prism.DA<BitSet, AcceptanceRabin>(numStates);
+			draNew = new automata.DA<BitSet, AcceptanceRabin>(numStates);
 			createPrismDA(draNew);
 			AcceptanceRabin accNew = createRabinAcceptance();
 			draNew.setAcceptance(accNew);
@@ -163,9 +163,9 @@ public class DRA extends DA {
 			return draNew;
 		} else {
 			// Streett
-			prism.DA<BitSet, AcceptanceStreett> dsaNew;
+			automata.DA<BitSet, AcceptanceStreett> dsaNew;
 
-			dsaNew = new prism.DA<BitSet, AcceptanceStreett>(numStates);
+			dsaNew = new automata.DA<BitSet, AcceptanceStreett>(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<BitSet, ?> da) throws PrismException
+	private void createPrismDA(automata.DA<BitSet, ?> da) throws PrismException
 	{
 		int i, k, numLabels, numStates, src, dest;
 		List<String> apList;

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<BitSet,AcceptanceRabin> ltl2rabin(SimpleLTL ltlFormula) throws PrismException
+	public static automata.DA<BitSet,AcceptanceRabin> ltl2rabin(SimpleLTL ltlFormula) throws PrismException
 	{
 		DA<BitSet, ? extends AcceptanceOmega> result;
 		result = ltl2da(ltlFormula, AcceptanceType.RABIN);
@@ -44,14 +44,14 @@ public class LTL2Rabin {
 	}
 
 	@SuppressWarnings("unchecked")
-	public static prism.DA<BitSet, AcceptanceStreett> ltl2streett(SimpleLTL ltlFormula) throws PrismException
+	public static automata.DA<BitSet, AcceptanceStreett> ltl2streett(SimpleLTL ltlFormula) throws PrismException
 	{
 		DA<BitSet, ? extends AcceptanceOmega> result;
 		result = ltl2da(ltlFormula, AcceptanceType.STREETT);
 		return (DA<BitSet, AcceptanceStreett>)result;
 	}
 	
-	public static prism.DA<BitSet, ? extends AcceptanceOmega> ltl2da(SimpleLTL ltlFormula, AcceptanceType... allowedAcceptance) throws PrismException
+	public static automata.DA<BitSet, ? extends AcceptanceOmega> ltl2da(SimpleLTL ltlFormula, AcceptanceType... allowedAcceptance) throws PrismException
 	{
 		SimpleLTL ltl = ltlFormula.simplify();
 

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;

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;

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.*;

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;