s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Removal of unused code. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@80 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 20 years ago
parent
79d765eedb
commit
3149f54d47
6 changed files with 0 additions and 2002 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 187
      prism/src/simulator/old/ExplorationTesting.java
  2. 428
      prism/src/simulator/old/ExploreTesting.java
  3. 276
      prism/src/simulator/old/ExpressionTesting.java
  4. 103
      prism/src/simulator/old/LoadModelTesting.java
  5. 406
      prism/src/simulator/old/ManualSimulator.java
  6. 602
      prism/src/simulator/old/UpdatesTesting.java

187
prism/src/simulator/old/ExplorationTesting.java
View File

@ -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();
}
}
}

428
prism/src/simulator/old/ExploreTesting.java
View File

@ -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();
}
}
}

276
prism/src/simulator/old/ExpressionTesting.java
View File

@ -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))<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))<=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"};
}

103
prism/src/simulator/old/LoadModelTesting.java
View File

@ -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();
}
}
}

406
prism/src/simulator/old/ManualSimulator.java
View File

@ -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 <model_file>");
System.out.println(" simulator <model_file> <properties_file>");
System.out.println(" simulator <model_file> <properties_file> -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();
}
}
}

602
prism/src/simulator/old/UpdatesTesting.java
View File

@ -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;
}
}
Write Preview
Loading…
Cancel
Save