explicit.ExplicitFiles2Model: explicit model import

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

prism/src/explicit/ExplicitFiles2Model.java

@@ -0,0 +1,216 @@
+//==============================================================================
+//	
+//	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.io.BufferedReader;
+import java.io.File;
+import java.io.FileReader;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+
+import common.IterableStateSet;
+import parser.State;
+import parser.ast.ModulesFile;
+import prism.PrismComponent;
+import prism.PrismException;
+import prism.PrismNotSupportedException;
+
+/**
+ * Class to convert explicit-state file storage of a model to a model of the explicit engine.
+ */
+public class ExplicitFiles2Model extends PrismComponent
+{
+	/** Constructor */
+	public ExplicitFiles2Model(PrismComponent parent)
+	{
+		super(parent);
+	}
+
+	/**
+	 * Build a Model corresponding to the passed in states/transitions/labels files.
+	 * Variable info and model type is taken from {@code modulesFile}.
+	 * The number of states should also be passed in as {@code numStates}.
+	 *
+	 * @param statesFile .sta file (optional, may be {@code null})
+	 * @param transFile .tra file
+	 * @param labelsFile .lab file (optional, may be {@code null})
+	 * @param modulesFile modules file (normally created with ExplicitFiles2ModulesFile)
+	 * @param numStates number of states
+	 * @return the constructed model
+	 */
+	public Model build(File statesFile, File transFile, File labelsFile, ModulesFile modulesFile, int numStates) throws PrismException
+	{
+		ModelExplicit model = null;
+		switch (modulesFile.getModelType()) {
+		case DTMC:
+			DTMCSimple dtmc = new DTMCSimple();
+			dtmc.buildFromPrismExplicit(transFile.getAbsolutePath());
+			model = dtmc;
+			break;
+		case CTMC:
+			CTMCSimple ctmc = new CTMCSimple();
+			ctmc.buildFromPrismExplicit(transFile.getAbsolutePath());
+			model = ctmc;
+			break;
+		case MDP:
+			MDPSimple mdp = new MDPSimple();
+			mdp.buildFromPrismExplicit(transFile.getAbsolutePath());
+			model = mdp;
+			break;
+		case CTMDP:
+		case LTS:
+		case PTA:
+		case SMG:
+		case STPG:
+			throw new PrismNotSupportedException("Currently, importing " + modulesFile.getModelType() + " is not supported");
+		}
+		if (model == null) {
+			throw new PrismException("Could not import " + modulesFile.getModelType());
+		}
+
+		if (model.getNumStates() == 0) {
+			throw new PrismNotSupportedException("Imported model has no states, not supported");
+		}
+
+		if (labelsFile != null) {
+			// load labels
+			loadLabels(model, labelsFile);
+		} else {
+			// no init label, we choose the first state
+			model.addInitialState(0);
+		}
+
+		if (!model.getInitialStates().iterator().hasNext()) {
+			throw new PrismException("Imported model has no initial states");
+		}
+
+		if (statesFile != null) {
+			loadStates(model, statesFile, modulesFile);
+		} else {
+			// in absence of a statesFile, there is a single variable x
+			// in the model, with value corresponding to the state index
+			List<State> states = new ArrayList<State>(model.getNumStates());
+			for (int i = 0; i < model.getNumStates(); i++) {
+				State s = new State(1);
+				s.setValue(0, i); // set x = state index
+				states.add(s);
+			}
+			model.setStatesList(states);
+		}
+
+		return model;
+	}
+
+	/**
+	 * Load the label information and attach to the model.
+	 * The "init" label states become the initial states of the model
+	 * and the "deadlock" label states become the deadlock states of the model.
+	 */
+	private void loadLabels(ModelExplicit model, File labelsFile) throws PrismException
+	{
+		Map<String, BitSet> labels = StateModelChecker.loadLabelsFile(labelsFile.getAbsolutePath());
+
+		for (Entry<String, BitSet> e : labels.entrySet()) {
+			if (e.getKey().equals("init")) {
+				for (int state : new IterableStateSet(e.getValue(), model.getNumStates())) {
+					model.addInitialState(state);
+				}
+			} else if (e.getKey().equals("deadlock")) {
+				for (int state : new IterableStateSet(e.getValue(), model.getNumStates())) {
+					model.addDeadlockState(state);
+				}
+			} else {
+				model.addLabel(e.getKey(), e.getValue());
+			}
+		}
+	}
+
+	/** Load the state information, construct the statesList and attach to model */
+	private void loadStates(ModelExplicit model, File statesFile, ModulesFile mf) throws PrismException
+	{
+		int numStates = model.getNumStates();
+		List<State> statesList = new ArrayList<State>(numStates);
+		for (int i = 0; i < numStates; i++) {
+			statesList.add(null);
+		}
+
+		String s, ss[];
+		int i, j, lineNum = 0;
+
+		int numVars = mf.getNumVars();
+
+		// open file for reading, automatic close when done
+		try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) {
+			// skip first line
+			in.readLine();
+			lineNum = 1;
+			// read remaining lines
+			s = in.readLine();
+			lineNum++;
+			while (s != null) {
+				// skip blank lines
+				s = s.trim();
+				if (s.length() > 0) {
+					// split into two parts
+					ss = s.split(":");
+					// determine which state this line describes
+					i = Integer.parseInt(ss[0]);
+					// now split up middle bit and extract var info
+					ss = ss[1].substring(ss[1].indexOf('(') + 1, ss[1].indexOf(')')).split(",");
+
+					State state = new State(numVars);
+					if (ss.length != numVars)
+						throw new PrismException("(wrong number of variable values) ");
+					for (j = 0; j < numVars; j++) {
+						if (ss[j].equals("true")) {
+							state.setValue(j, true);
+						} else if (ss[j].equals("false")) {
+							state.setValue(j, false);
+						} else {
+							state.setValue(j, Integer.parseInt(ss[j]));
+						}
+					}
+					if (statesList.get(i) != null)
+						throw new PrismException("(duplicated state) ");
+					statesList.set(i, state);
+				}
+				// read next line
+				s = in.readLine();
+				lineNum++;
+			}
+			model.setStatesList(statesList);
+		} catch (IOException e) {
+			throw new PrismException("File I/O error reading from \"" + statesFile + "\"");
+		} catch (PrismException e) {
+			throw new PrismException("Error detected " + e.getMessage() + "at line " + lineNum + " of states file \"" + statesFile + "\"");
+		}
+	}
+}