From 53b1ec3def7600fc051772cf2d245c9837e7b4d3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 23 May 2008 07:42:52 +0000 Subject: [PATCH] Added PrismStaTra tool. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@789 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismStaTra.java | 147 +++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 prism/src/prism/PrismStaTra.java diff --git a/prism/src/prism/PrismStaTra.java b/prism/src/prism/PrismStaTra.java new file mode 100644 index 00000000..9766e63f --- /dev/null +++ b/prism/src/prism/PrismStaTra.java @@ -0,0 +1,147 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// 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 prism; + +import java.io.*; +import java.util.ArrayList; + +// Small utility to merge PRISM states and transition files + +public class PrismStaTra +{ + // files to read in from + private File statesFile; + private File transFile; + + // states info + private ArrayList states; + + public PrismStaTra(File sf, File tf) + { + statesFile = sf; + transFile = tf; + } + + // Read info about reachable state space from file and store string + + public void readStatesFromFile() throws PrismException + { + BufferedReader in; + String s, ss[]; + int lineNum = 0; + + // create arrays for explicit state storage + states = new ArrayList(); + try { + // open file for reading + in = new BufferedReader(new FileReader(statesFile)); + // skip first line + in.readLine(); lineNum = 1; + // read remaining lines + s = in.readLine(); lineNum++; + while (s != null) { + s = s.trim(); + ss = s.split(":"); + //i = Integer.parseInt(ss[0]); + states.add(ss[1]); + s = in.readLine(); lineNum++; + } + // close file + in.close(); + } + catch (IOException e) { + throw new PrismException("File I/O error reading from \"" + statesFile + "\""); + } + catch (NumberFormatException e) { + throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\""); + } + } + + // Read info about transitions from file, insert state info and re-output + + private void readTransitionsFromFile() throws PrismException + { + BufferedReader in; + String s, ss[]; + int r, c, lineNum = 0; + + try { + // open file for reading + in = new BufferedReader(new FileReader(transFile)); + // skip first line + s = in.readLine(); System.out.println(s); lineNum = 1; + // read remaining lines + s = in.readLine(); lineNum++; + while (s != null) { + // parse line, split into parts + s = s.trim(); + ss = s.split(" "); + // case for dtmcs/ctmcs... + if (ss.length == 3) { + r = Integer.parseInt(ss[0]); + c = Integer.parseInt(ss[1]); + System.out.println(states.get(r) + " " + states.get(c) + " " + ss[2]); + } + // case for mdps... + else if (ss.length == 4) { + r = Integer.parseInt(ss[0]); + c = Integer.parseInt(ss[2]); + System.out.println(states.get(r) + " " + ss[1] + " " + states.get(c) + " " + ss[3]); + } + // read next line + s = in.readLine(); lineNum++; + } + // close file + in.close(); + } + catch (IOException e) { + throw new PrismException("File I/O error reading from \"" + transFile + "\""); + } + catch (NumberFormatException e) { + throw new PrismException("Error detected at line " + lineNum + " of transition matrix file \"" + transFile + "\""); + } + } + + public static void main(String args[]) + { + if (args.length < 2) { + System.out.println("Error: Need two arguments (states and transitions file)"); + System.exit(1); + } + try { + PrismStaTra pst = new PrismStaTra(new File(args[0]), new File(args[1])); + pst.readStatesFromFile(); + pst.readTransitionsFromFile(); + } + catch (PrismException e) { + System.out.println("Error: " + e.getMessage()); + System.exit(1); + } + } +} + +//------------------------------------------------------------------------------