diff --git a/prism/src/explicit/ExplicitFiles2Model.java b/prism/src/explicit/ExplicitFiles2Model.java new file mode 100644 index 00000000..0216b15a --- /dev/null +++ b/prism/src/explicit/ExplicitFiles2Model.java @@ -0,0 +1,216 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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 states = new ArrayList(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 labels = StateModelChecker.loadLabelsFile(labelsFile.getAbsolutePath()); + + for (Entry 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 statesList = new ArrayList(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 + "\""); + } + } +}