From c17f92e172003f1cd44103ab67964591af04280c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 13 Jun 2015 09:16:12 +0000 Subject: [PATCH] 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 | 34 ++++++ prism/src/prism/LTSFromDA.java | 204 +++++++++++++++++++++++++++++++++ prism/src/prism/ModelType.java | 31 ++++- 3 files changed, 266 insertions(+), 3 deletions(-) create mode 100644 prism/src/explicit/LTS.java create mode 100644 prism/src/prism/LTSFromDA.java diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java new file mode 100644 index 00000000..8578fe55 --- /dev/null +++ b/prism/src/explicit/LTS.java @@ -0,0 +1,34 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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 +{ +} diff --git a/prism/src/prism/LTSFromDA.java b/prism/src/prism/LTSFromDA.java new file mode 100644 index 00000000..e2601b28 --- /dev/null +++ b/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 getSuccessorsIterator(int s) + { + List succs = new ArrayList(); + 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 getSuccessorsIterator(int s, int i) + { + List succs = new ArrayList(); + 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"); + } +} diff --git a/prism/src/prism/ModelType.java b/prism/src/prism/ModelType.java index ffeea423..eaf85373 100644 --- a/prism/src/prism/ModelType.java +++ b/prism/src/prism/ModelType.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford) +// * Dave Parker (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))