Add LTS model type and expose underlying graph of a DA as an LTS.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10012 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/LTS.java

@@ -0,0 +1,34 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+/**
+ * Interface for classes that provide (read) access to an explicit-state labelled transition system (LTS).
+ */
+public interface LTS extends NondetModel
+{
+}

prism/src/prism/LTSFromDA.java

@@ -0,0 +1,204 @@
+package prism;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.Iterator;
+import java.util.List;
+
+import strat.MDStrategy;
+import explicit.LTS;
+import explicit.Model;
+import explicit.ModelExplicit;
+
+/**
+ * Class giving access to the labelled transition system (LTS) underlying a deterministic automaton (DA).
+ * This is not particularly efficiently; we assume the DA will probably be relatively small.
+ */
+public class LTSFromDA extends ModelExplicit implements LTS
+{
+	/** Underlying DA */
+	private DA<?, ?> da;
+
+	public LTSFromDA(DA<?, ?> da)
+	{
+		this.numStates = da.size();
+		this.da = da;
+	}
+
+	// Methods to implement Model
+
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(int s)
+	{
+		List<Integer> succs = new ArrayList<Integer>();
+		int n = da.getNumEdges(s);
+		for (int i = 0; i < n; i++) {
+			succs.add(da.getEdgeDest(s, i));
+		}
+		return succs.iterator();
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, BitSet set)
+	{
+		int n = da.getNumEdges(s);
+		for (int i = 0; i < n; i++) {
+			if (!set.get(da.getEdgeDest(s, i))) {
+				return false;
+			}
+		}
+		return true;
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, BitSet set)
+	{
+		int n = da.getNumEdges(s);
+		for (int i = 0; i < n; i++) {
+			if (set.get(da.getEdgeDest(s, i))) {
+				return true;
+			}
+		}
+		return false;
+	}
+
+	@Override
+	public void findDeadlocks(boolean fix) throws PrismException
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public void buildFromPrismExplicit(String filename) throws PrismException
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public ModelType getModelType()
+	{
+		return ModelType.LTS;
+	}
+
+	@Override
+	public int getNumTransitions()
+	{
+		int size = da.size();
+		int num = 0;
+		for (int s = 0; s < size; s++) {
+			num += da.getNumEdges(s);
+		}
+		return num;
+	}
+
+	@Override
+	public boolean isSuccessor(int s1, int s2)
+	{
+		int n = da.getNumEdges(s1);
+		for (int i = 0; i < n; i++) {
+			if (da.getEdgeDest(s1, i) == s2) {
+				return true;
+			}
+		}
+		return false;
+	}
+
+	@Override
+	public void checkForDeadlocks(BitSet except) throws PrismException
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public void exportToPrismExplicitTra(PrismLog out)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	protected void exportTransitionsToDotFile(int i, PrismLog out)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public void exportToPrismLanguage(String filename) throws PrismException
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	// Methods to implement NondetModel
+
+	@Override
+	public int getNumChoices(int s)
+	{
+		return da.getNumEdges(s);
+	}
+
+	@Override
+	public int getMaxNumChoices()
+	{
+		int size = da.size();
+		int max = 0;
+		for (int s = 0; s < size; s++) {
+			max = Math.max(max, da.getNumEdges(s));
+		}
+		return max;
+	}
+
+	@Override
+	public int getNumChoices()
+	{
+		return getNumTransitions();
+	}
+
+	@Override
+	public Object getAction(int s, int i)
+	{
+		return null;
+	}
+
+	@Override
+	public boolean areAllChoiceActionsUnique()
+	{
+		return false;
+	}
+
+	@Override
+	public int getNumTransitions(int s, int i)
+	{
+		return 1;
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, int i, BitSet set)
+	{
+		return set.get(da.getEdgeDest(s, i));
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	{
+		return set.get(da.getEdgeDest(s, i));
+	}
+
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(int s, int i)
+	{
+		List<Integer> succs = new ArrayList<Integer>();
+		succs.add(da.getEdgeDest(s, i));
+		return succs.iterator();
+	}
+
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+
+	@Override
+	public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int[] strat)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+}

prism/src/prism/ModelType.java

@@ -2,7 +2,7 @@
 //	
 //	Copyright (c) 2002-
 //	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -29,7 +29,7 @@ package prism;
 public enum ModelType {
 
 	// List of model types (ordered alphabetically)
-	CTMC, CTMDP, DTMC, MDP, PTA, STPG, SMG;
+	CTMC, CTMDP, DTMC, LTS, MDP, PTA, STPG, SMG;
 
 	/**
 	 * Get the full name, in words, of the this model type.
@@ -43,6 +43,8 @@ public enum ModelType {
 			return "continuous-time Markov decision process";
 		case DTMC:
 			return "discrete-time Markov chain";
+		case LTS:
+			return "labelled transition system";
 		case MDP:
 			return "Markov decision process";
 		case PTA:
@@ -68,6 +70,8 @@ public enum ModelType {
 			return "ctmdp";
 		case DTMC:
 			return "dtmc";
+		case LTS:
+			return "lts";
 		case MDP:
 			return "mdp";
 		case PTA:
@@ -89,6 +93,7 @@ public enum ModelType {
 	{
 		switch (this) {
 		case DTMC:
+		case LTS:
 		case MDP:
 		case PTA:
 		case STPG:
@@ -109,6 +114,7 @@ public enum ModelType {
 	{
 		switch (this) {
 		case DTMC:
+		case LTS:
 		case MDP:
 		case STPG:
 		case SMG:
@@ -131,6 +137,7 @@ public enum ModelType {
 		case DTMC:
 		case CTMC:
 			return false;
+		case LTS:
 		case MDP:
 		case STPG:
 		case SMG:
@@ -150,6 +157,7 @@ public enum ModelType {
 		switch (this) {
 		case DTMC:
 		case CTMC:
+		case LTS:
 		case MDP:
 		case PTA:
 		case CTMDP:
@@ -162,9 +170,22 @@ public enum ModelType {
 		return true;
 	}
 
+	/**
+	 * Is this model probabilistic?
+	 */
+	public boolean isProbabilistic()
+	{
+		switch (this) {
+		case LTS:
+			return false;
+		default:
+			return true;
+		}
+	}
+	
 	/**
 	 * Does this model have probabilities or rates?
-	 * @return "Probability" or "Rate"
+	 * Returns "Probability" or "Rate", accordingly (or "" if there are neither)
 	 */
 	public String probabilityOrRate()
 	{
@@ -172,6 +193,8 @@ public enum ModelType {
 		case CTMC:
 		case CTMDP:
 			return "Rate";
+		case LTS:
+			return "";
 		default:
 			return "Probability";
 		}
@@ -187,6 +210,8 @@ public enum ModelType {
 			return DTMC;
 		else if ("mdp".equals(name))
 			return MDP;
+		else if ("lts".equals(name))
+			return LTS;
 		else if ("pta".equals(name))
 			return PTA;
 		else if ("stpg".equals(name))