From 3149f54d47e3859d5caa66c32c9674ed596f53a9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 29 Oct 2006 21:10:12 +0000 Subject: [PATCH] Removal of unused code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@80 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../src/simulator/old/ExplorationTesting.java | 187 ------ prism/src/simulator/old/ExploreTesting.java | 428 ------------- .../src/simulator/old/ExpressionTesting.java | 276 -------- prism/src/simulator/old/LoadModelTesting.java | 103 --- prism/src/simulator/old/ManualSimulator.java | 406 ------------ prism/src/simulator/old/UpdatesTesting.java | 602 ------------------ 6 files changed, 2002 deletions(-) delete mode 100644 prism/src/simulator/old/ExplorationTesting.java delete mode 100644 prism/src/simulator/old/ExploreTesting.java delete mode 100644 prism/src/simulator/old/ExpressionTesting.java delete mode 100644 prism/src/simulator/old/LoadModelTesting.java delete mode 100644 prism/src/simulator/old/ManualSimulator.java delete mode 100644 prism/src/simulator/old/UpdatesTesting.java diff --git a/prism/src/simulator/old/ExplorationTesting.java b/prism/src/simulator/old/ExplorationTesting.java deleted file mode 100644 index 6cecfd57..00000000 --- a/prism/src/simulator/old/ExplorationTesting.java +++ /dev/null @@ -1,187 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2004-2005, Andrew Hinton -// -// 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 simulator.old; - -import java.util.*; -import java.io.*; -import parser.*; -import prism.*; - - -public class ExplorationTesting -{ - public static void main(String[]args) - { - try - { - //PRISM initialisation stuff - Prism p = new Prism(null, null); - - //Parse model - ModulesFile mf = p.parseModelFile(new File(args[0])); - - //Define constants - - Values constants = new Values(); - - ConstantList modConstants = mf.getConstantList(); - if(modConstants.getNumUndefined() > 0) - System.out.println("Please enter values for the following undefined model constants:"); - BufferedReader br = new BufferedReader(new InputStreamReader(System.in)); - String input; - if(modConstants != null) - { - for(int i = 0; i < modConstants.getNumUndefined(); i++) - { - - String var = (String)modConstants.getUndefinedConstants().elementAt(i); - - boolean valid = true; - do - { - System.out.print(var+": "); - input = br.readLine(); - if(input.equals("true")) - { - constants.addValue(var, new Integer(1)); - } - else if(input.equals("false")) - { - constants.addValue(var, new Integer(0)); - } - else - { - try - { - constants.addValue(var, new Integer(input)); - valid = true; - } - catch(NumberFormatException e) - { - valid = false; - } - } - } while(!valid); - } - } - System.out.println("Constants done..."); - - - - //Dummy PropertiesFile - PropertiesFile pf = new PropertiesFile(mf); - - //Obtain the default initial state - Values v = mf.getInitialValues(); - - //Setup the simulator engine API - SimulatorEngine engine = new SimulatorEngine(); - - //Load in state v - engine.startNewPath(mf, pf, v); - - //At this point, the updates set has already been calculated, this can be queried: - int numUpdates = engine.getNumUpdates(); - System.out.println("Number of updates: "+numUpdates); - System.out.println(); - System.out.println("Module\tAction\tProb\tAssignments"); - System.out.println("=============================================================="); - for(int i = 0; i < numUpdates; i++) - { - System.out.println(engine.getModuleNameOfUpdate(i)+"\t"+ - engine.getActionLabelOfUpdate(i)+"\t"+ - engine.getProbabilityOfUpdate(i)+"\t"+ - engine.getAssignmentDescriptionOfUpdate(i)); - //Note there are many, many more querying methods should you require them - } - - //Try another set of values - while(true) - { - System.out.println(); - System.out.println("Try another set of values: "); - v = new Values(); - //simple for loop to read some values from the command line. - - for(int i = 0; i < mf.getVarNames().size(); i++) - { - String var = (String)mf.getVarNames().elementAt(i); - - boolean valid = true; - do - { - System.out.print(var+": "); - input = br.readLine(); - if(input.equals("true")) - { - v.addValue(var, new Integer(1)); - } - else if(input.equals("false")) - { - v.addValue(var, new Integer(0)); - } - else - { - try - { - v.addValue(var, new Integer(input)); - valid = true; - } - catch(NumberFormatException e) - { - valid = false; - } - } - } while(!valid); - } - - //Load in state v - engine.restartNewPath(v); - - //At this point, the updates set has already been calculated, this can be queried: - numUpdates = engine.getNumUpdates(); - System.out.println("Number of updates: "+numUpdates); - System.out.println(); - System.out.println("Module\tAction\tProb\tAssignments"); - System.out.println("=============================================================="); - for(int i = 0; i < numUpdates; i++) - { - System.out.println(engine.getModuleNameOfUpdate(i)+"\t"+ - engine.getActionLabelOfUpdate(i)+"\t"+ - engine.getProbabilityOfUpdate(i)+"\t"+ - engine.getAssignmentDescriptionOfUpdate(i)); - //Note there are many, many more querying methods should you require them - } - - } - - } - catch(Exception e) - { - System.out.println("Error: "+e.getMessage()); - e.printStackTrace(); - } - } - - -} diff --git a/prism/src/simulator/old/ExploreTesting.java b/prism/src/simulator/old/ExploreTesting.java deleted file mode 100644 index e3e7be98..00000000 --- a/prism/src/simulator/old/ExploreTesting.java +++ /dev/null @@ -1,428 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2004-2005, Andrew Hinton -// -// 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 simulator.old; - -import java.util.*; -import java.io.*; -import parser.*; -import prism.*; - -/** - */ -public class ExploreTesting -{ - private Prism p; - private Expression e; - private SimulatorEngine s; - - public static void main(String[]args) - { - if(args.length > 0) - new ExploreTesting(args[0]); - else - new ExploreTesting("1"); - } - - public ExploreTesting(String parameter) - { - try - { - p = new Prism(null, null); - s = new SimulatorEngine(p); - int type = 0; - - - ModulesFile m = p.parseModelFile(new File - //("../examples/dice/dice.pm")); - //("../examples/leader/synchronous/leader3_4.pm")); - //("../examples/dice/two_dice.nm")); - //("../examples/leader/asynchronous/leader4.nm")); - //("../andrew.pm")); - ("../examples/cluster/cluster.sm")); - //("../examples/polling/poll3.sm")); - //("../examples/cyclin.sm")); - //("../test.sm")); - //("../examples/molecules/nacl.sm")); - //("../examples/brp/brp.pm")); - //("../examples/tandem/tandem.sm")); - //m.tidyUp(); - //m.setUndefinedConstants(constants); - //System.out.println(m.toString()+"\n\n\n\n\n\n\n"); - type = m.getType(); - long before= System.currentTimeMillis(); - s.loadModulesFile(m); - Values init = new Values(); - - //leader3_4.pm - /*init.addValue("c", new Integer(1)); - init.addValue("s1", new Integer(0)); - init.addValue("u1", new Boolean(false)); - init.addValue("v1", new Integer(0)); - init.addValue("p1", new Integer(0)); - init.addValue("s2", new Integer(0)); - init.addValue("u2", new Boolean(false)); - init.addValue("v2", new Integer(0)); - init.addValue("p2", new Integer(0)); - init.addValue("s3", new Integer(0)); - init.addValue("u3", new Boolean(false)); - init.addValue("v3", new Integer(0)); - init.addValue("p3", new Integer(0)); */ - - //dice.pm - //init.addValue("d", new Integer(0)); - //init.addValue("s", new Integer(0)); - - //two_dice.nm - //init.addValue("d1", new Integer(0)); - //init.addValue("d2", new Integer(0)); - //init.addValue("s1", new Integer(0)); - //init.addValue("s2", new Integer(0)); - - //leader4.nm - /*init.addValue("c1", new Integer(0)); - init.addValue("s1", new Integer(0)); - init.addValue("p1", new Integer(0)); - init.addValue("receive1", new Integer(0)); - init.addValue("sent1", new Integer(0)); - init.addValue("c2", new Integer(0)); - init.addValue("s2", new Integer(0)); - init.addValue("p2", new Integer(0)); - init.addValue("receive2", new Integer(0)); - init.addValue("sent2", new Integer(0)); - init.addValue("c3", new Integer(0)); - init.addValue("s3", new Integer(0)); - init.addValue("p3", new Integer(0)); - init.addValue("receive3", new Integer(0)); - init.addValue("sent3", new Integer(0)); - init.addValue("c4", new Integer(0)); - init.addValue("s4", new Integer(0)); - init.addValue("p4", new Integer(0)); - init.addValue("receive4", new Integer(0)); - init.addValue("sent4", new Integer(0)); */ - - - //cluster.sm - init.addValue("left_n", new Integer(parameter)); - init.addValue("left", new Boolean(false)); - init.addValue("right_n", new Integer(parameter)); - init.addValue("right", new Boolean(false)); - init.addValue("line", new Boolean(false)); - init.addValue("line_n", new Boolean(true)); - init.addValue("Toleft", new Boolean(false)); - init.addValue("Toright", new Boolean(false)); - init.addValue("Toleft_n", new Boolean(true)); - init.addValue("Toright_n", new Boolean(true)); - init.addValue("r", new Boolean(false)); - - //andrew.pm - //init.addValue("s", new Integer(0)); - - //poll23.sm - //init.addValue("s", new Integer(1)); - //init.addValue("a", new Integer(0)); - //init.addValue("s1", new Integer(0)); - //init.addValue("s2", new Integer(0)); - //init.addValue("s3", new Integer(0)); - //init.addValue("s4", new Integer(0)); - //init.addValue("s5", new Integer(0)); - //init.addValue("s6", new Integer(0)); - //init.addValue("s7", new Integer(0)); - //init.addValue("s8", new Integer(0)); - //init.addValue("s9", new Integer(0)); - //init.addValue("s10", new Integer(0)); - //init.addValue("s11", new Integer(0)); - //init.addValue("s12", new Integer(0)); - //init.addValue("s13", new Integer(0)); - //init.addValue("s14", new Integer(0)); - //init.addValue("s15", new Integer(0)); - //init.addValue("s16", new Integer(0)); - //init.addValue("s17", new Integer(0)); - //init.addValue("s18", new Integer(0)); - //init.addValue("s19", new Integer(0)); - //init.addValue("s20", new Integer(0)); - //init.addValue("s21", new Integer(0)); - //init.addValue("s22", new Integer(0)); - //init.addValue("s23", new Integer(0)); - - //cyclic.sm - /*init.addValue("cyclin", new Integer(4)); - init.addValue("cyclin_bound", new Integer(0)); - init.addValue("degc", new Integer(0)); - init.addValue("trim", new Integer(0)); - init.addValue("dim", new Integer(0)); - - init.addValue("bound1", new Integer(0)); - init.addValue("bound2", new Integer(0)); - - init.addValue("cdk", new Integer(2)); - init.addValue("cdk_cat", new Integer(0)); - - init.addValue("cdh1", new Integer(2)); - init.addValue("inact", new Integer(0)); - - init.addValue("cdc14", new Integer(4)); - - init.addValue("cki", new Integer(2)); */ - - //test.sm - //init.addValue("x", new Integer(0)); - - //nacl.sm - //init.addValue("na", new Integer(10)); - //init.addValue("cl", new Integer(10)); - //init.addValue("dummy", new Boolean(false)); - - //brp.pm - /*init.addValue("s", new Integer(0)); - init.addValue("srep", new Integer(0)); - init.addValue("nrtr", new Integer(0)); - init.addValue("i", new Integer(0)); - init.addValue("bs", new Boolean(false)); - init.addValue("s_ab", new Boolean(false)); - init.addValue("fs", new Boolean(false)); - init.addValue("ls", new Boolean(false)); - - init.addValue("r", new Integer(0)); - init.addValue("rrep", new Integer(0)); - init.addValue("fr", new Boolean(false)); - init.addValue("lr", new Boolean(false)); - init.addValue("br", new Boolean(false)); - init.addValue("r_ab", new Boolean(false)); - init.addValue("recv", new Boolean(false)); - - init.addValue("T", new Boolean(false)); - - init.addValue("k", new Boolean(false)); - - init.addValue("l", new Boolean(false)); */ - - //tandem.sm - - //init.addValue("sc", new Integer(0)); - //init.addValue("ph", new Integer(1)); - //init.addValue("sm", new Integer(0)); - - - Values constants = new Values();//m.getConstantValues(); - //constants.addValue("c", new Integer(124)); - - //constants.addValue("r", new Double(parameter)); - - //brp constants - //constants.addValue("N", new Integer(16)); - //constants.addValue("MAX", new Integer(2)); - - - //cluster constants - constants.addValue("N", new Integer(parameter)); - //constants.addValue("T", new Integer(10)); - - //tandem constants - //constants.addValue("c", new Integer(10)); - - m.setUndefinedConstants(constants); - Values v = m.getConstantValues(); - System.out.println(v.toString()); - - PropertiesFile pf = p.parsePropertiesFile(m, new File - //("../examples/dice/dice2.pctl")); - ("../examples/cluster/cluster.csl")); - //("../examples/polling/pollandrew.csl")); - //("../examples/cyclin.csl")); - //("../test.csl")); - //("../examples/molecules/nacl.csl")); - //("../examples/brp/brp.pctl")); - //("../examples/tandem/tandem.csl")); - System.out.println(pf.toString()); - - s.loadProperties(pf); - - Values pConstants = new Values(); - - //cluster property constants - pConstants.addValue("T", new Integer(10)); - - pf.setUndefinedConstants(pConstants); - Values pv = pf.getConstantValues(); - - s.startNewPath(m.getConstantValues(), init); - //s.startNewPath(m.getConstantValues(), pf.getConstantValues(), init); - long timeTaken = System.currentTimeMillis() - before; - //System.out.println("Loading model complete!! Took: "+timeTaken+"ms\n\n"); - - System.out.println(SimulatorEngine.modelToString()); - System.out.println(SimulatorEngine.pathToString()); - - - - - //pctl - - for(int i = 0; i < pf.getNumProperties(); i++) - { - System.out.println("adding property"); - s.addPCTLProperty(pf.getProperty(i)); - } - - //SimulatorEngine.printRegisteredPathFormulae(); - - - //s.doSampling(); - - - BufferedReader br = new BufferedReader(new InputStreamReader(System.in)); - - String input = null; - - System.out.print("SIM::> "); - try - { - input = br.readLine(); - while(!input.equals("exit")) - { - if(input.equals("backtrack")) - { - System.out.print("to step: "); - input = br.readLine(); - try - { - int i = Integer.parseInt(input); - if(i>=0)//protection - { - s.backtrack(i); - - System.out.println(SimulatorEngine.pathToString()); - //SimulatorEngine.printRegisteredPathFormulae(); - } - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - - } - else if(input.equals("remove")) - { - System.out.print("to step: "); - input = br.readLine(); - try - { - int i = Integer.parseInt(input); - if(i>=0)//protection - { - s.removePrecedingStates(i); - - System.out.println(SimulatorEngine.pathToString()); - //SimulatorEngine.printRegisteredPathFormulae(); - } - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - - } - else if(input.equals("auto")) - { - System.out.println("how many steps: "); - input = br.readLine(); - try - { - int i = Integer.parseInt(input); - if(i>=0) - { - long cl = System.currentTimeMillis(); - s.automaticChoices(i); - long ti = System.currentTimeMillis() - cl; - System.out.println(SimulatorEngine.pathToString()); - //SimulatorEngine.printRegisteredPathFormulae(); - //System.out.println(""+i+" steps took: "+ti+"ms"); - } - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - } - else //manual update - { - try - { - - int i = Integer.parseInt(input); - - if(type == ModulesFile.STOCHASTIC) - { - System.out.print("time in state: "); - input = br.readLine(); - try - { - double d = Double.parseDouble(input); - - s.manualUpdate(i,d); - - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - } - else - s.manualUpdate(i); - System.out.println(); - System.out.println(SimulatorEngine.pathToString()); - //SimulatorEngine.printRegisteredPathFormulae(); - } - catch(NumberFormatException e) - { - System.out.println("Invalid input, enter the update index"); - } - catch(SimulatorException e) - { - System.out.println("Invalid input: "+e.getMessage()); - } - - } - System.out.print("SIM::> "); - input = br.readLine(); - } - } - catch (IOException ioe) - { - System.out.println("IO error trying to read your name!"); - System.exit(1); - } - - - } - catch(Exception e) - { - System.out.println("Error: "+e.getMessage()); - e.printStackTrace(); - } - } - - - - -} diff --git a/prism/src/simulator/old/ExpressionTesting.java b/prism/src/simulator/old/ExpressionTesting.java deleted file mode 100644 index 1a2fe8a7..00000000 --- a/prism/src/simulator/old/ExpressionTesting.java +++ /dev/null @@ -1,276 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2004-2005, Andrew Hinton -// -// 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 simulator.old; - -import java.util.*; -import java.io.*; -import parser.*; -import prism.*; - -/** Test cases for expression building - */ -public class ExpressionTesting -{ - private Prism p; - private Expression e; - private SimulatorEngine s; - - public static void main(String[]args) - { - new ExpressionTesting(); - - } - - public ExpressionTesting() - { - try - { - p = new Prism(null, null); - s = new SimulatorEngine(p); - - int startAt = 0; - int current; - - - for(current = startAt; current < tests.length; current++) - { - e = p.parseSingleExpressionString(tests[current]); - System.out.print("Test "+(current+1)+"\t"+tests[current]+"\t"); - //s = new SimulatorEngine(p); - int sim = e.toSimulator(s); - System.out.print(SimulatorEngine.expressionToString(sim)); - System.out.println(""); - SimulatorEngine.deleteExpression(sim); - } - } - catch(Exception e) - { - System.out.println("Error: "+e.getMessage()); - } - } - - public static String[] tests = - { - "(!false)", - "!(3=4)", - "!(3!=4)", - "!(3>4)", - "!(3<4)", - "!(3>=4)", - "!(3<=4)", - "!(true & true)", - "!(true & true & true)", - "!(true | true)", - "!(true | true | false)", - "!false", - "!true", - "ceil(2.23*2)", - "ceil(2.23-2.0)", - "ceil(1/2)", - "ceil(max(2.0,3.0,4.5))", - "ceil(2.23)", - "floor(2.23*2)", - "floor(2.23-2.0)", - "floor(1/2)", - "floor(max(2.0,3.0,4.5))", - "floor(2.23)", - "(!true)=(!true)", - "(!true)=(true=true)", - "(!true)=(true&true)", - "(!true)=(true & true & true)", - "(!true)=(true | true)", - "(!true)=(true | true | true)", - "(!true)=true", - "(!true)=false", - "(true=true)=(!true)", - "(true=true)=(true=true)", - "(true=true)=(true&true)", - "(true=true)=(true & true & true)", - "(true=true)=(true | true)", - "(true=true)=(true | true | true)", - "(true=true)=true", - "(true=true)=false", - "(true & true & true)=(!true)", - "(true&true&true)=(true=true)", - "(true & true & true)=(true&true)", - "(true & true & true)=(true & true & true)", - "(true & true & true)=(true | true)", - "(true & true & true)=(true | true | true)", - "(true & true & true)=true", - "(true & true & true)=false", - "(true | true | true)=(!true)", - "(true | true | true)=(true=true)", - "(true | true | true)=(true&true)", - "(true | true | true)=(true & true & true)", - "(true | true | true)=(true | true)", - "(true | true | true)=(true | true | true)", - "(true | true | true)=true", - "(true | true | true)=false", - "true=(!true)", - "true=(true=true)", - "true=(true&true)", - "true=(true & true & true)", - "true=(true | true)", - "true=(true | true | true)", - "true=true", - "true=false", - "(ceil(2.4))=(ceil(2.4))", - "(ceil(2.4))=(floor(2.4))", - "(ceil(2.4))=(2.0*4.0)", - "(ceil(2.4))=(2.0+4.0)", - "(ceil(2.4))=(2.0/4.0)", - "(ceil(2.4))=(2.0-4.0)", - "(ceil(2.4))=((true) ? (3.0) : (4.0))", - "(ceil(2.4))=max(2.0, 2.4)", - "(ceil(2.4))=min(2.0, 2.4)", - "(ceil(2.4))=3.0", - "(!true)!=(!true)", - "(!true)!=(true=true)", - "(!true)!=(true&true)", - "(!true)!=(true & true & true)", - "(!true)!=(true | true)", - "(!true)!=(true | true | true)", - "(!true)!=true", - "(!true)!=false", - "(true=true)!=(!true)", - "(true=true)!=(true=true)", - "(true=true)!=(true&true)", - "(true=true)!=(true & true & true)", - "(true=true)!=(true | true)", - "(true=true)!=(true | true | true)", - "(true=true)!=true", - "(true=true)!=false", - "(true & true & true)!=(!true)", - "(true&true&true)!=(true=true)", - "(true & true & true)!=(true&true)", - "(true & true & true)!=(true & true & true)", - "(true & true & true)!=(true | true)", - "(true & true & true)!=(true | true | true)", - "(true & true & true)!=true", - "(true & true & true)!=false", - "(true | true | true)!=(!true)", - "(true | true | true)!=(true=true)", - "(true | true | true)!=(true&true)", - "(true | true | true)!=(true & true & true)", - "(true | true | true)!=(true | true)", - "(true | true | true)!=(true | true | true)", - "(true | true | true)!=true", - "(true | true | true)!=false", - "true!=(!true)", - "true!=(true=true)", - "true!=(true&true)", - "true!=(true & true & true)", - "true!=(true | true)", - "true!=(true | true | true)", - "true!=true", - "true!=false", - "(ceil(2.4))!=(ceil(2.4))", - "(ceil(2.4))!=(floor(2.4))", - "(ceil(2.4))!=(2.0*4.0)", - "(ceil(2.4))!=(2.0+4.0)", - "(ceil(2.4))!=(2.0/4.0)", - "(ceil(2.4))!=(2.0-4.0)", - "(ceil(2.4))!=((true) ? (3.0) : (4.0))", - "(ceil(2.4))!=max(2.0, 2.4)", - "(ceil(2.4))!=min(2.0, 2.4)", - "(ceil(2.4))!=3.0", - "(ceil(2.4))>(ceil(2.4))", - "(ceil(2.4))>(floor(2.4))", - "(ceil(2.4))>(2.0*4.0)", - "(ceil(2.4))>(2.0+4.0)", - "(ceil(2.4))>(2.0/4.0)", - "(ceil(2.4))>(2.0-4.0)", - "(ceil(2.4))>((true) ? (3.0) : (4.0))", - "(ceil(2.4))>max(2.0, 2.4)", - "(ceil(2.4))>min(2.0, 2.4)", - "(ceil(2.4))>3.0", - "(ceil(2.4))<(ceil(2.4))", - "(ceil(2.4))<(floor(2.4))", - "(ceil(2.4))<(2.0*4.0)", - "(ceil(2.4))<(2.0+4.0)", - "(ceil(2.4))<(2.0/4.0)", - "(ceil(2.4))<(2.0-4.0)", - "(ceil(2.4))<((true) ? (3.0) : (4.0))", - "(ceil(2.4))=(ceil(2.4))", - "(ceil(2.4))>=(floor(2.4))", - "(ceil(2.4))>=(2.0*4.0)", - "(ceil(2.4))>=(2.0+4.0)", - "(ceil(2.4))>=(2.0/4.0)", - "(ceil(2.4))>=(2.0-4.0)", - "(ceil(2.4))>=((true) ? (3.0) : (4.0))", - "(ceil(2.4))>=max(2.0, 2.4)", - "(ceil(2.4))>=min(2.0, 2.4)", - "(ceil(2.4))>=3.0", - "(ceil(2.4))<=(ceil(2.4))", - "(ceil(2.4))<=(floor(2.4))", - "(ceil(2.4))<=(2.0*4.0)", - "(ceil(2.4))<=(2.0+4.0)", - "(ceil(2.4))<=(2.0/4.0)", - "(ceil(2.4))<=(2.0-4.0)", - "(ceil(2.4))<=((true) ? (3.0) : (4.0))", - "(ceil(2.4))<=max(2.0, 2.4)", - "(ceil(2.4))<=min(2.0, 2.4)", - "(ceil(2.4))<=3.0", - "3.0*ceil(2.4)", - "3.0*floor(2.4)", - "3.0*(3.0*4.0)", - "3.0*(3.0+4.0)", - "3.0*(3.0/4.0)", - "3.0*(4.0-3.0)", - "3.0*((true) ? (3.0) : (4.0))", - "3.0*max(2.5, 2.6)", - "3.0*min(2.5, 2.6)", - "3.0*3.0", - "3*(3*4)", - "3*(3+4)", - "3*(3/4)", - "3*(4-3)", - "3*((true) ? (3) : (4))", - "3*max(3,4)", - "3*min(3,4)", - "3*3", - "3.0+ceil(2.4)", - "3.0+floor(2.4)", - "3.0+(3.0*4.0)", - "3.0+(3.0+4.0)", - "3.0+(3.0/4.0)", - "3.0+(4.0-3.0)", - "3.0+((true) ? (3.0) : (4.0))", - "3.0+max(2.5, 2.6)", - "3.0+min(2.5, 2.6)", - "3.0+3.0", - "3+(3*4)", - "3+(3+4)", - "3+(3/4)", - "3+(4-3)", - "3+((true) ? (3) : (4))", - "3+max(3,4)", - "3+min(3,4)", - "3+3"}; - - - -} diff --git a/prism/src/simulator/old/LoadModelTesting.java b/prism/src/simulator/old/LoadModelTesting.java deleted file mode 100644 index af896be5..00000000 --- a/prism/src/simulator/old/LoadModelTesting.java +++ /dev/null @@ -1,103 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2004-2005, Andrew Hinton -// -// 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 simulator.old; - -import java.util.*; -import java.io.*; -import parser.*; -import prism.*; - -/** Test cases for expression building - */ -public class LoadModelTesting -{ - private Prism p; - private Expression e; - private SimulatorEngine s; - - public static void main(String[]args) - { - new LoadModelTesting(); - - } - - public LoadModelTesting() - { - try - { - p = new Prism(null, null); - s = new SimulatorEngine(p); - - - - ModulesFile m = p.parseModelFile(new File - ("../examples/dice/dice.pm")); - //("../examples/leader/synchronous/leader3_4.pm")); - //m.tidyUp(); - //m.setUndefinedConstants(constants); - System.out.println(m.toString()+"\n\n\n\n\n\n\n"); - long before= System.currentTimeMillis(); - s.loadModulesFile(m); - Values init = new Values(); - /* - init.addValue("c", new Integer(1)); - init.addValue("s1", new Integer(0)); - init.addValue("u1", new Boolean(false)); - init.addValue("v1", new Integer(0)); - init.addValue("p1", new Integer(0)); - init.addValue("s2", new Integer(0)); - init.addValue("u2", new Boolean(false)); - init.addValue("v2", new Integer(0)); - init.addValue("p2", new Integer(0)); - init.addValue("s3", new Integer(0)); - init.addValue("u3", new Boolean(false)); - init.addValue("v3", new Integer(0)); - init.addValue("p3", new Integer(0));*/ - - init.addValue("d", new Integer(0)); - init.addValue("s", new Integer(0)); - - Values constants = new Values();//m.getConstantValues(); - //constants.addValue("c", new Integer(124)); - - m.setUndefinedConstants(constants); - Values v = m.getConstantValues(); - System.out.println(v.toString()); - s.startNewPath(m.getConstantValues(), init); - long timeTaken = System.currentTimeMillis() - before; - System.out.println("Loading model complete!! Took: "+timeTaken+"ms\n\n"); - - System.out.println(SimulatorEngine.modelToString()); - System.out.println(SimulatorEngine.pathToString()); - } - catch(Exception e) - { - System.out.println("Error: "+e.getMessage()); - e.printStackTrace(); - } - } - - - - -} diff --git a/prism/src/simulator/old/ManualSimulator.java b/prism/src/simulator/old/ManualSimulator.java deleted file mode 100644 index ec16de1a..00000000 --- a/prism/src/simulator/old/ManualSimulator.java +++ /dev/null @@ -1,406 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2004-2005, Andrew Hinton -// -// 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 simulator.old; - -import java.util.*; -import java.io.*; -import parser.*; -import prism.*; - -/** - */ -public class ManualSimulator -{ - private Prism p; - private Expression e; - private SimulatorEngine s; - - public static void main(String[]args) - { - if(args.length == 1) - new ManualSimulator(args[0], null, false); - else if(args.length == 2) - new ManualSimulator(args[0], args[1], false); - else if(args.length == 3) - new ManualSimulator(args[0], args[1], args[2].equals("-sample")); - - else - { - System.out.println("usage: simulator "); - System.out.println(" simulator "); - System.out.println(" simulator -sample"); - } - } - - public ManualSimulator(String parameter, String properties, boolean doSampling) - { - //initialise prism - p = new Prism(null, null); - - //initialise simulator engine - s = new SimulatorEngine(p); - int type = 0; - - try - { - //Parse model - ModulesFile m = p.parseModelFile(new File(parameter)); - - //Load this into simulator engine - s.loadModulesFile(m); - - //Console reader - BufferedReader br = new BufferedReader(new InputStreamReader(System.in)); - String input; - - - //Sort out the initial state - System.out.println("Please enter values for the initial state."); - - Values init = new Values(); - for(int i = 0; i < m.getVarNames().size(); i++) - { - String var = (String)m.getVarNames().elementAt(i); - - boolean valid = true; - do - { - System.out.print(var+": "); - input = br.readLine(); - if(input.equals("true")) - { - init.addValue(var, new Integer(1)); - } - else if(input.equals("false")) - { - init.addValue(var, new Integer(0)); - } - else - { - try - { - init.addValue(var, new Integer(input)); - valid = true; - } - catch(NumberFormatException e) - { - valid = false; - } - } - } while(!valid); - } - System.out.println("Initial state done..."); - System.out.println(""); - - - Values constants = new Values(); - - ConstantList modConstants = m.getConstantList(); - if(modConstants.getNumUndefined() > 0) - System.out.println("Please enter values for the following undefined model constants:"); - - if(modConstants != null) - { - for(int i = 0; i < modConstants.getNumUndefined(); i++) - { - - - - String var = (String)modConstants.getUndefinedConstants().elementAt(i); - - boolean valid = true; - do - { - System.out.print(var+": "); - input = br.readLine(); - if(input.equals("true")) - { - constants.addValue(var, new Integer(1)); - } - else if(input.equals("false")) - { - constants.addValue(var, new Integer(0)); - } - else - { - try - { - constants.addValue(var, new Integer(input)); - valid = true; - } - catch(NumberFormatException e) - { - valid = false; - } - } - } while(!valid); - } - } - System.out.println("Constants done..."); - System.out.println(""); - - //define the constants - m.setUndefinedConstants(constants); - - //properties - PropertiesFile pf = null; - Values propertyConstants = new Values(); - - if(properties != null) - { - pf = p.parsePropertiesFile(m, new File(properties)); - - s.loadProperties(pf); - - Values propConValues = new Values(); - - Vector pConstants = pf.getUndefinedConstants(); - - if(pConstants != null) - { - if(pConstants.size() > 0) - System.out.println("Please enter values for the following undefined property constants:"); - for(int i = 0; i < pConstants.size(); i++) - { - - - - String var = (String)pConstants.elementAt(i); - - boolean valid = true; - do - { - System.out.print(var+": "); - input = br.readLine(); - if(input.equals("true")) - { - propConValues.addValue(var, new Integer(1)); - } - else if(input.equals("false")) - { - propConValues.addValue(var, new Integer(0)); - } - else - { - try - { - propConValues.addValue(var, new Integer(input)); - valid = true; - } - catch(NumberFormatException e) - { - valid = false; - } - } - } while(!valid); - } - } - - pf.setUndefinedConstants(propConValues); - - propertyConstants = pf.getConstantValues(); - - s.startNewPath(m.getConstantValues(), propertyConstants, init); - - for(int i = 0; i < pf.getNumProperties(); i++) - { - s.addPCTLProperty(pf.getProperty(i)); - } - - - } - else - s.startNewPath(m.getConstantValues(), propertyConstants, init); - - - System.out.println("Simulator loaded successfully..."); - System.out.println(""); - - - if(doSampling) - { - s.doSampling(); - System.exit(0); - } - - System.out.println(SimulatorEngine.pathToString()); - SimulatorEngine.printRegisteredPathFormulae(); - SimulatorEngine.printCurrentUpdates(); - - - - - System.out.print("SIM::> "); - try - { - input = br.readLine(); - while(!input.equals("exit")) - { - - if(input.equals("reset")) - { - s.initialiseModel(); - s.loadModel(m); - - s.startNewPath(m.getConstantValues(), propertyConstants, init); - if(pf != null) - { - for(int i = 0; i < pf.getNumProperties(); i++) - { - s.addPCTLProperty(pf.getProperty(i)); - } - } - System.out.println(SimulatorEngine.pathToString()); - SimulatorEngine.printRegisteredPathFormulae(); - SimulatorEngine.printCurrentUpdates(); - } - if(input.equals("backtrack")) - { - System.out.print("to step: "); - input = br.readLine(); - try - { - int i = Integer.parseInt(input); - if(i>=0)//protection - { - s.backtrack(i); - - System.out.println(SimulatorEngine.pathToString()); - SimulatorEngine.printRegisteredPathFormulae(); - SimulatorEngine.printCurrentUpdates(); - } - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - - } - else if(input.equals("remove")) - { - System.out.print("to step: "); - input = br.readLine(); - try - { - int i = Integer.parseInt(input); - if(i>=0)//protection - { - s.removePrecedingStates(i); - - System.out.println(SimulatorEngine.pathToString()); - SimulatorEngine.printRegisteredPathFormulae(); - SimulatorEngine.printCurrentUpdates(); - } - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - - } - else if(input.equals("auto")) - { - System.out.println("how many steps: "); - input = br.readLine(); - try - { - int i = Integer.parseInt(input); - if(i>=0) - { - long cl = System.currentTimeMillis(); - s.automaticChoices(i); - long ti = System.currentTimeMillis() - cl; - System.out.println(SimulatorEngine.pathToString()); - SimulatorEngine.printRegisteredPathFormulae(); - SimulatorEngine.printCurrentUpdates(); - //System.out.println(""+i+" steps took: "+ti+"ms"); - } - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - } - else //manual update - { - try - { - - int i = Integer.parseInt(input); - - if(type == ModulesFile.STOCHASTIC) - { - System.out.print("time in state: "); - input = br.readLine(); - try - { - double d = Double.parseDouble(input); - - s.manualUpdate(i,d); - - } - catch(NumberFormatException e) - { - System.out.println("Invalid input"); - } - } - else - s.manualUpdate(i); - System.out.println(); - System.out.println(SimulatorEngine.pathToString()); - SimulatorEngine.printRegisteredPathFormulae(); - SimulatorEngine.printCurrentUpdates(); - } - catch(NumberFormatException e) - { - System.out.println("Invalid input, enter the update index"); - } - catch(SimulatorException e) - { - System.out.println("Invalid input: "+e.getMessage()); - } - - } - System.out.print("SIM::> "); - input = br.readLine(); - } - } - catch (IOException ioe) - { - System.out.println("IO error trying to read your name!"); - System.exit(1); - } - - - } - catch(Exception e) - { - System.out.println("Error: "+e.getMessage()); - e.printStackTrace(); - } - } - - - - -} diff --git a/prism/src/simulator/old/UpdatesTesting.java b/prism/src/simulator/old/UpdatesTesting.java deleted file mode 100644 index d414ae9d..00000000 --- a/prism/src/simulator/old/UpdatesTesting.java +++ /dev/null @@ -1,602 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2004-2005, Andrew Hinton -// -// 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 simulator.old; - -import java.util.*; -import java.io.*; -import parser.*; -import prism.*; - -/** - */ -public class UpdatesTesting -{ - private Prism p; - private Expression e; - private SimulatorEngine s; - - public static void main(String[]args) - { - new UpdatesTesting(); - - } - - public UpdatesTesting() - { - PrismFileLog ppp = new PrismFileLog("stdout"); - p = new Prism(ppp,ppp); - p.initialise(); - - s = new SimulatorEngine(p); - - //Setup the test log - - PrintWriter testLog = null; - try - { - File f = new File("../testing/update_testlog_1.log"); - testLog = new PrintWriter(new FileWriter(f), true); - - //testLog.println("Test the printwriter"); - } - catch(IOException e) - { - System.err.println("Error in opening test log file: \n"+e.getMessage()); - } - - Model builtModel = null; - - //for each test case - for(int i = 0; i < getNumTestCases(); i++) - { - s.initialiseModel(); - - //create ModulesFile for this test case - ModulesFile mf = null; - try - { - File f = new File(getTestFile(i)); - System.err.println("Loading..."+f.toString()); - mf = p.parseModelFile(f); - //System.err.println(mf.toString()); - } - catch(Exception e) - { - testLog.println(getTestFile(i)+"\t"+"Parsing Error: "+e.getMessage()); - continue; - } - Values constants = new Values(); - addConstantsForTestFile(i, constants); - - try - { - mf.setUndefinedConstants(constants); - Values v = mf.getConstantValues(); - } - catch(Exception e) - { - testLog.println(getTestFile(i)+"\t"+"Invalid Constants Provided: "+e.getMessage()); - continue; - } - - try - { - if(builtModel != null) - builtModel.clear(); - builtModel = p.buildModel(mf); - } - catch(PrismException e) - { - testLog.println(getTestFile(i)+"\t"+"Build Error "+e.getMessage()); - continue; - } - - StateList sl = builtModel.getReachableStates(); - - PrismFileLog pfl = new PrismFileLog("../testing/tempStates.txt"); - sl.print(pfl); - pfl.close(); - File stateFile = new File("../testing/tempStates.txt"); - File transFile = new File("../testing/tempTrans.txt"); - try - { - p.exportToFile(builtModel, true, Prism.EXPORT_PLAIN, transFile); - } - catch(Exception e) - { - testLog.println(getTestFile(i)+"\t"+"Error when exporting transitions: "+e.getMessage()); - } - ArrayList states = new ArrayList(); - - try - { - //testLog.println(getTestFile(i)+"\t"+"Before test states and transitions"); - computeStatesAndTransitions(states, stateFile, transFile, builtModel.getNumVars()); - //testLog.println(getTestFile(i)+"\t"+"Computed test states and transitions"); - } - catch(Exception e) - { - testLog.println(getTestFile(i)+"\t"+"Error when computing test states and transitions: "+e.getMessage()); - continue; - } - - int countErrors = 0; - int countTests = 0; - - String[]varNames = new String[mf.getVarNames().size()]; - for(int j = 0; j < varNames.length; j++) - { - varNames[j] = (String)mf.getVarNames().elementAt(j); - //System.out.println("A var: "+varNames[j]); - } - - s.loadModulesFile(mf); - - - for(int j = 0; j < states.size(); j++) - { - if(j%10 == 0) - { - System.err.print("\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b"); - System.err.print("Iteration: "+j); - } - - //System.out.println("Iteration "+j+": "); - State currentTestState = (State)states.get(j); - //System.out.println(currentTestState.toString()); - Values test = new Values(); - for(int k = 0; k < varNames.length; k++) - { - int type = ((Integer)mf.getVarTypes().elementAt(k)).intValue(); - Object obj; - - if(type == Expression.BOOLEAN) - { - obj = (currentTestState.varValues[k] == 0) ? new Boolean(false) : new Boolean(true); - } - else - { - obj = new Integer(currentTestState.varValues[k]); - } - test.addValue(varNames[k], obj); - } - try - { - if(j == 0) - s.startNewPath(mf.getConstantValues(), test); - else - s.startNewPath(test); - //System.err.println(s.modelToString()); - //System.err.println(s.pathToString()); - boolean result = currentTestState.compareUpdates(s, states); - if(!result) - { - //Produce error report - - countErrors++; - - PrintWriter pw = new PrintWriter(new FileWriter(new File("../testing/errorReports/error_"+i+"_"+countErrors+".txt"))); - - pw.println("Error report for "+getTestFile(i)); - pw.println("==================================================================="); - pw.println(); - //pw.println(s.modelToString()); - - int numUpdates = s.getNumUpdates(); - pw.println("Actual Results"); - pw.println(); - - for(int ii = 0; ii < numUpdates; ii++) - { - int[] vars = new int[builtModel.getNumVars()]; - pw.print(s.getProbabilityOfUpdate(ii)+"\t"); - pw.print(s.getDistributionIndexOfUpdate(ii)+"\t"); - double prob = s.getProbabilityOfUpdate(ii); - int dist = s.getDistributionIndexOfUpdate(ii); - for(int jj = 0; jj < builtModel.getNumVars(); jj++) - { - vars[jj] = s.getResultOfUpdate(ii,jj); - //pw.print(s.getResultOfUpdate(i,j)); - } - State ssss = null; - for(int jj = 0; jj < states.size(); jj++) - { - ssss = (State)states.get(jj); - if(ssss.equals(vars)) - { - pw.println(" "+ssss.index); - break; - } - } - - } - pw.println("Expected results"); - pw.println(currentTestState.toString()); - pw.println(); - pw.flush(); - pw.close(); - } - - } - catch(Exception e) - { - testLog.println(getTestFile(i)+"\t"+"Error in starting new path"); - } - countTests++; - } - - testLog.println(getTestFile(i)+"\tno. tests: "+countTests+"\tfailed: "+countErrors); - - } - } - - - public void computeStatesAndTransitions(ArrayList states, File stateFile, File transFile, int numVars) throws Exception - { - BufferedReader br = new BufferedReader(new FileReader(stateFile)); - - int ff= 0; - while(br.ready()) - { - String line = br.readLine(); - //System.err.println("line = "+line); - //find the number - int numEnd = 0; - while(line.charAt(numEnd) != ':') - numEnd++; - int index = Integer.parseInt(line.substring(0,numEnd)); - //System.err.println("step1"); - State st = new State(index, numVars); - - - //System.err.println("numEnd = "+line.charAt(numEnd)); - int curr = numEnd+2; //start where the variables start - int startNum = numEnd+2; - - int varIndex = 0; - //System.err.println("step2"); - while(line.charAt(curr)!= ')') - { - //System.err.println("step "+line.charAt(curr)); - if(line.charAt(curr) == ',') - { - //System.err.println("step3"); - int num = Integer.parseInt(line.substring(startNum, curr)); - startNum = curr+1; - st.varValues[varIndex++] = num; - } - curr++; - } - int num = Integer.parseInt(line.substring(startNum, curr)); - startNum = curr+1; - st.varValues[varIndex++] = num; - - states.add(st); - } - - br = new BufferedReader(new FileReader(transFile)); - - br.readLine(); //ignore the first line header info - - while(br.ready()) - { - String line = br.readLine(); - StringTokenizer tokens = new StringTokenizer(line, " "); - if(tokens.countTokens() == 4) //nondeterministic - { - int fromIndex = Integer.parseInt(tokens.nextToken()); - int distIndex = Integer.parseInt(tokens.nextToken()); - int toIndex = Integer.parseInt(tokens.nextToken()); - double probability = Double.parseDouble(tokens.nextToken()); - - State fromState = (State)states.get(fromIndex); - State toState = (State)states.get(toIndex); - Transition tran = new Transition(toState, distIndex, probability); - - fromState.addTransition(tran); - } - else if(tokens.countTokens() == 3) //dtmc (ctmc) - { - int fromIndex = Integer.parseInt(tokens.nextToken()); - int distIndex = -1; - int toIndex = Integer.parseInt(tokens.nextToken()); - double probability = Double.parseDouble(tokens.nextToken()); - - State fromState = (State)states.get(fromIndex); - State toState = (State)states.get(toIndex); - Transition tran = new Transition(toState, distIndex, probability); - - fromState.addTransition(tran); - } - else throw new Exception("Wrong number of tokens in transition file"); - } - - } - - class State - { - int index; - int[] varValues; - - ArrayList transitions; - - public State(int index, int numVarValues) - { - this.index = index; - varValues = new int[numVarValues]; - - transitions = new ArrayList(); - } - - public boolean equals(int[]test) - { - for(int i = 0; i < varValues.length; i++) - if(varValues[i] != test[i]) return false; - return true; - } - - public boolean compareUpdates(SimulatorEngine s, ArrayList states) - { - int numUpdates = s.getNumUpdates(); - - int[] distribution = new int[100]; - for(int i = 0; i < distribution.length; i++) - { - distribution[i] = -1; - } - - for(int i = 0; i < numUpdates; i++) - { - int[] vars = new int[varValues.length]; - //System.err.print(s.getProbabilityOfUpdate(i)+"\t"); - //System.err.print(s.getDistributionIndexOfUpdate(i)+"\t"); - double prob = s.getProbabilityOfUpdate(i); - int dist = s.getDistributionIndexOfUpdate(i); - for(int j = 0; j < varValues.length; j++) - { - vars[j] = s.getResultOfUpdate(i,j); - //System.err.print(s.getResultOfUpdate(i,j)); - } - State ssss = null; - for(int j = 0; j < states.size(); j++) - { - ssss = (State)states.get(j); - if(ssss.equals(vars)) - { - //System.err.print(" "+ssss.index); - break; - } - } - //System.err.println(); - if(ssss != null) - { - for(int j = 0; j < getNumTransitions(); j++) - { - Transition t = getTransition(j); - if(t.toState.index == ssss.index) - { - if(t.probability > prob-0.0000001 && t.probability < prob+0.0000001) - { - t.checked = true; - /*if(distribution[t.distributionIndex] == -1) - { - distribution[t.distributionIndex] = dist; - } - else - { - //if we have already assigned check - //that it is the same - if(distribution[t.distributionIndex] - != dist) return false; - }*/ - } - else return false; - } - } - } - } - - //all transitions should have been checked - for(int i = 0; i < getNumTransitions(); i++) - { - if(!getTransition(i).checked) return false; - } - //System.err.println(); - //System.err.println(this.toString()); - //System.err.println(); - return true; - } - - public Transition getTransition(int i) - { - return (Transition)transitions.get(i); - } - - public void addTransition(Transition t) - { - transitions.add(t); - } - - public int getNumTransitions() - { - return transitions.size(); - } - - public String toString() - { - String returner = ""+index+":("; - for(int i = 0; i < varValues.length; i++) - { - returner+=""+varValues[i]; - if(i != varValues.length-1) returner+=","; - } - returner+=")"; - for(int i = 0; i < transitions.size(); i++) - returner+="\n\t"+getTransition(i).toString(); - - return returner; - } - } - - class Transition - { - State toState; - int distributionIndex; - double probability; - boolean checked; - - public Transition(State toState, int distributionIndex, double probability) - { - this.toState = toState; - this.distributionIndex = distributionIndex; - this.probability = probability; - } - - public String toString() - { - String returner = distributionIndex >= 0 ? "["+distributionIndex+"]" : ""; - returner+=" "+probability+": "+toState.index; - return returner; - } - } - - - //==================================================================== - // Test Cases - //==================================================================== - - public String getTestFile(int i ) - { - String returner = "../examples/"; - switch(i) - { - /*case 0: return returner+"dice/two_dice.nm"; - case 1: return returner+"leader/asynchronous/leader4.nm"; - case 2: return returner+"leader/asynchronous/leader5.nm"; - case 3: return returner+"firewire/abst/deadline.nm"; - case 4: return returner+"firewire/abst/deadline.nm"; - case 5: return returner+"lrabin/lrabin34.nm"; */ - //case 0: return returner+"/cluster/cluster.sm"; - //case 0: return returner+"mutual/mutual3.nm"; - case 0: return returner+"cyclin.sm"; - case 1: return returner+"phil/phil4.nm"; - case 2: return returner+"rabin/rabin3.nm"; - - case 9: return returner+"lrabin/lrabin35.nm"; - case 10: return returner+"lrabin/lrabin36.nm"; - case 11: return returner+"lrabin/lrabin38.nm"; - case 12: return returner+"lrabin/lrabin44.nm"; - case 13: return returner+"lrabin/lrabin45.nm"; - case 14: return returner+"lrabin/lrabin46.nm"; - case 15: return returner+"lrabin/lrabin48.nm"; - case 16: return returner+"mutual/mutual10.nm"; - case 17: return returner+"mutual/mutual4.nm"; - case 18: return returner+"mutual/mutual5.nm"; - case 19: return returner+"mutual/mutual8.nm"; - - case 20: return returner+"phil/phil15.nm"; - case 21: return returner+"phil/phil2.nm"; - case 22: return returner+"phil/phil20.nm"; - case 24: return returner+"phil/phil25.nm"; - case 25: return returner+"phil/phil3.nm"; - case 26: return returner+"phil/phil30.nm"; - case 27: return returner+"phil/phil35.nm"; - case 28: return returner+"phil/phil4.nm"; - case 29: return returner+"phil/phil5.nm"; - case 30: return returner+"phil/phil6.nm"; - case 31: return returner+"phil/phil7.nm"; - case 32: return returner+"phil/phil8.nm"; - case 33: return returner+"phil/phil9.nm"; - - case 35: return returner+"rabin/rabin12.nm"; - case 36: return returner+"rabin/rabin3.nm"; - case 37: return returner+"rabin/rabin4.nm"; - case 38: return returner+"rabin/rabin5.nm"; - case 39: return returner+"rabin/rabin6.nm"; - case 40: return returner+"rabin/rabin8.nm"; - case 41: return returner+"leader/asynchronous/leader6.nm"; - case 42: return returner+"leader/asynchronous/leader7.nm"; - - - } - return null; - } - - public void addConstantsForTestFile(int i, Values values) - { - switch(i) - { - case 0: values.addValue("N", new Integer(2)); return; - case 1: return; - case 2: return; - case 3: values.addValue("deadline", new Integer(10)); return; //eg - case 4: return; - case 5: return; - case 6: return; - case 7: return; - case 8: return; - case 9: return; - case 10: return; - case 11: return; - case 12: return; - case 13: return; - case 14: return; - case 15: return; - case 16: return; - case 17: return; - case 18: return; - case 19: return; - case 20: return; - case 21: return; - case 22: return; - case 23: return; - case 24: return; - case 25: return; - case 26: return; - case 27: return; - case 28: return; - case 29: return; - case 30: return; - case 31: return; - case 32: return; - case 33: return; - case 34: return; - case 35: return; - case 36: return; - case 37: return; - case 38: return; - case 39: return; - case 40: return; - case 41: return; - case 42: return; - - } - } - - public int getNumTestCases() - { - return 1; - } - - -}