explicit.LTSExplicit: Storage for an LTS

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

prism/src/explicit/LTSExplicit.java

@@ -0,0 +1,239 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.Collections;
+import java.util.Iterator;
+import java.util.LinkedHashSet;
+
+import prism.ModelType;
+import prism.PrismException;
+import prism.PrismLog;
+import strat.MDStrategy;
+
+/**
+ * This is a minimal implementation of an explicitly stored labeled transition system.
+ * Each target state of an edge is modeled as a choice, with a single transition for
+ * this choice.
+ */
+public class LTSExplicit extends ModelExplicit implements LTS
+{
+	protected ArrayList<ArrayList<Integer>> successors = new ArrayList<ArrayList<Integer>>();
+	protected int numTransitions = 0;
+	protected int maxNumChoices = 0;
+
+	public LTSExplicit()
+	{
+		initialise(0);
+	}
+
+	public int addState()
+	{
+		successors.add(new ArrayList<Integer>());
+		return numStates++;
+	}
+
+	public void addEdge(int s, int t)
+	{
+		// we don't care if an edge from s to t already exists
+		successors.get(s).add(t);
+		numTransitions++;
+		maxNumChoices = Math.max(getNumChoices(s), maxNumChoices);
+	}
+
+	@Override
+	public int getNumChoices(int s)
+	{
+		// one choice per successor for s
+		return successors.get(s).size();
+	}
+
+	@Override
+	public int getMaxNumChoices()
+	{
+		return maxNumChoices;
+	}
+
+	@Override
+	public int getNumChoices()
+	{
+		return numTransitions;
+	}
+
+	@Override
+	public Object getAction(int s, int i)
+	{
+		// we don't have action labels
+		return null;
+	}
+
+	@Override
+	public boolean areAllChoiceActionsUnique()
+	{
+		// as we don't assign action labels, they are not unique
+		return false;
+	}
+
+	@Override
+	public int getNumTransitions(int s, int i)
+	{
+		if (i < getNumChoices(s)) {
+			// one transition per choice
+			return 1;
+		}
+		throw new IllegalArgumentException();
+	}
+
+	public int getNumTransitions(int s)
+	{
+		return getNumChoices(s);
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, int i, BitSet set)
+	{
+		// single successor for s, i
+		return set.get(successors.get(s).get(i));
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	{
+		// single successor for s, i
+		return set.get(successors.get(s).get(i));
+	}
+
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(int s, int i)
+	{
+		// single successor for s, i
+		return Collections.singletonList(successors.get(s).get(i)).iterator();
+	}
+
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToDotFileWithStrat(PrismLog out, BitSet mark, int[] strat)
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(int s)
+	{
+		// make successors unique
+		LinkedHashSet<Integer> succ = new LinkedHashSet<Integer>();
+		succ.addAll(successors.get(s));
+		return succ.iterator();
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, BitSet set)
+	{
+		for (int t : successors.get(s)) {
+			if (!set.get(t)) return false;
+		}
+		return true;
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, BitSet set)
+	{
+		for (int t : successors.get(s)) {
+			if (set.get(t)) return true;
+		}
+		return false;
+	}
+
+	@Override
+	public void findDeadlocks(boolean fix) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void buildFromPrismExplicit(String filename) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public ModelType getModelType()
+	{
+		return ModelType.LTS;
+	}
+
+	@Override
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+
+	@Override
+	public boolean isSuccessor(int s1, int s2)
+	{
+		for (Iterator<Integer> it = getSuccessorsIterator(s1); it.hasNext(); ) {
+			if (it.next() == s2) return true;
+		}
+		return false;
+	}
+
+	@Override
+	public void checkForDeadlocks(BitSet except) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void exportToPrismExplicitTra(PrismLog out)
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	protected void exportTransitionsToDotFile(int s, PrismLog out)
+	{
+		for (Iterator<Integer> it = getSuccessorsIterator(s); it.hasNext(); ) {
+			Integer successor = it.next();
+			out.println(s + " -> " + successor + ";");
+		}
+	}
+
+	@Override
+	public void exportToPrismLanguage(String filename) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+}