Commit 4ff87f3b authored by Ballarini Paolo's avatar Ballarini Paolo
Browse files

Upload New File

parent 0aa2096d
import java.util.*;
import java.io.*;
import java.nio.file.Path;
import java.nio.file.Paths;
public class PRISMGenerator_2phases_properties {
int numStations;
int numBuffers;
int buffSize [];
double failProb [];
double repairProb [];
int initState [];
String modelFileName = "";
String propFileName = "";
public PRISMGenerator_2phases_properties(int numStations, int[] buffSize, double[] failProb,
double[] repairProb, int[] initState) {
super();
if(numStations<=1) {
System.out.println("Incorrect number of stations: a production line must contains at least 2 stations");
return;
}
else {
this.modelFileName += numStations + "M_2phases.prism";
this.propFileName += numStations + "M_2phases.props";
this.numStations = numStations;
this.numBuffers = numStations -1 ;
this.buffSize = new int[numBuffers];
this.buffSize = buffSize;
this.initState = new int[numStations+numBuffers];
this.initState = initState;
this.failProb = new double[numStations];
if(failProb.length == numStations && repairProb.length == numStations && buffSize.length == numStations-1) {
this.failProb = failProb;
this.repairProb = new double[numStations];
this.repairProb = repairProb;
}
else
System.out.println("Incorrect length of probability vectors");
}
}
public PRISMGenerator_2phases_properties() {
// TODO Auto-generated constructor stub
}
public void setup(String fn) {
System.out.println("Reading input from "+fn);
//Path filePath = Paths.get(fn);
//System.out.println(filePath);
File configurationFile = new File(fn);
try {
Scanner scan = new Scanner(configurationFile); // Create a Scanner object
int n=scan.nextInt(); // number of stations
double fP [] = new double [n];
double rP [] = new double [n];
int bS [] = new int [n-1];
int iS [] = new int [2*n-1];
for(int i=0;i<n;i++)
fP[i]=scan.nextDouble();
for(int i=0;i<n;i++)
rP[i]=scan.nextDouble();
for(int i=0;i<n-1;i++)
bS[i]=scan.nextInt();
for(int i=0;i<2*n-1;i++)
iS[i]=scan.nextInt();
this.modelFileName += fn + ".prism";
this.propFileName += fn + ".props";
this.numStations = n;
this.numBuffers = n-1 ;
this.buffSize = new int[numBuffers];
this.buffSize = bS;
this.initState = new int[2*n-1];
this.initState = iS;
this.failProb = new double[n];
this.failProb = fP;
this.repairProb = new double[n];
this.repairProb = rP;
}
catch (FileNotFoundException e) {
e.printStackTrace();
}
}
public void generate() {
BufferedWriter writerModelFile = null;
BufferedWriter writerPropsFile = null;
try {
writerModelFile = new BufferedWriter( new FileWriter( this.modelFileName));
writerModelFile.write("dtmc\n\n");
int i;
for(i=1;i<= this.numStations;i++) {
writerModelFile.write("const double p" + i + "=" + this.failProb[i-1] + "; // fail probability of machine" + i +" \n");
}
for(i=1;i<= this.numStations;i++) {
writerModelFile.write("const double r" + i + "=" + this.repairProb[i-1] + "; // repair probability of machine" + i +" \n");
}
writerModelFile.write("const int n0=2; // capacity of fictitious buffer zero is set to 2 \n");
for(i=1;i< this.numStations;i++) {
writerModelFile.write("const int n" + i + "=" + this.buffSize[i-1] + "; // capacity of buffer " + i +" \n");
}
writerModelFile.write("const int n" + this.numStations + "=2; // capacity of fictitious last buffer is set to 2 \n");
for(i=1;i<= this.numStations;i++) {
writerModelFile.write("const int m" + i + "init=" + this.initState[i-1] + "; // initial state of machine " + i +" \n");
}
for(;i<2*this.numStations;i++) {
writerModelFile.write("const int b" + (i-numStations) + "init=" + this.initState[i-1] + "; // initial state of buffer " + i +" \n");
}
writerModelFile.write("\nmodule Phase\n");
writerModelFile.write("ph : [1..2] init 1;\n");
writerModelFile.write("[tic] ph=1 -> 1:(ph'=2);\n");
writerModelFile.write("[toc] ph=2 -> 1:(ph'=1);\n");
writerModelFile.write("endmodule\n\n");
writerModelFile.write("module B0\n" +
" b0 : [0..n0] init 1; // fictitious buffer with constant state (placeholder)\n" +
"endmodule\n\n");
writerModelFile.write("module M1 // intermediate machine, b0: upstream buffer, b1: downstream buffer\n" +
" m1 : [0..1] init m1init;\n" +
" \n" +
" [tic] m1=1 -> p1:(m1' = (b1=n1 | b0=0) ? 1 : 0) + (1-p1):(m1'=1);\n" +
" [toc] true -> 1:true;\n" +
" [tic] m1=0 -> r1:(m1'=1) + (1-r1):(m1'=0); \n" + "endmodule\n\n");
writerModelFile.write( "module B1 // intermediate buffer, m1: upstream machine, m2: downstream machine, \n" +
" // b0: upstream buffer, b2: downstream buffer\n" +
" b1 : [0..n1] init b1init; \n" +
"\n" +
" [tic] true -> 1:true;\n" +
" [toc] ((m1=1 & b0>0 & b1<n1) & !(m2=1 & b1>0 & b2<n2)) -> 1:(b1'=b1+1); // increase buffer occupation\n" +
" [toc] (!(m1=1 & b0>0 & b1<n1) & (m2=1 & b1>0 & b2<n2)) -> 1:(b1'=b1-1); // decrease buffer occupation\n" +
" [toc] ( (!(m1=1 & b0>0 & b1<n1) & !(m2=1 & b1>0 & b2<n2)) |\n"+
" ((m1=1 & b0>0 & b1<n1) & (m2=1 & b1>0 & b2<n2)) ) -> 1:(b1'=b1); // buffer unchanged\n" +
"endmodule\n\n");
int upstream ;
int upupstream ;
int downstream ;
for(i=2; i<=this.numStations;i++) {
upstream = i-1;
upupstream = i-2;
downstream = i+1;
writerModelFile.write("module M" + i + "= M" + upstream + "[m" + upstream + "=m" + i + ", b" + upupstream +
"=b" + upstream + ", b" + upstream + "=b" + i + ", p" + upstream + "=p" + i + ", r" + upstream +
"=r" + i + ", n" + upstream + "=n" + i +", m"+upstream+"init=m"+i+"init] endmodule \n");
if(i!=this.numStations)
writerModelFile.write("module B" + i + "= B" + upstream + "[b" + upstream + "=b" + i + ", m" + upstream +
"=m" + i + ", m" + i + "=m" + downstream + ", b" + upupstream + "=b" + upstream + ", b" + i +
"=b" + downstream + ", n" + upstream + "=n" + i + ", n" + i + "=n" + downstream +
", b"+upstream+"init=b"+i+"init] endmodule \n");
}
writerModelFile.write("\nmodule B" + this.numStations +"\n" +
" b" + this.numStations + ": [0..n" + this.numStations +"] init 1; // fictitious buffer with constant state (placeholder)\n" +
"endmodule\n\n");
//*********** REWARDS **********************************************************
// WIP
writerModelFile.write("// WIP (work in progress)\n");
writerModelFile.write("rewards \"WIP\"\n" + " true : b");
for(i=1; i<=this.numStations-2;i++) {
writerModelFile.write(i + "+b");
}
writerModelFile.write(this.numStations-1 + ";\n" + "endrewards\n\n");
// BUFFER OCCUPATION
writerModelFile.write("// BUFFER OCCUPATION (num. of pieces in a buffer) \n");
writerModelFile.write("const int N;\n");
for(i=1; i<=this.numStations-1;i++) {
writerModelFile.write("rewards \"B" +i+ "level\"\n");
writerModelFile.write(" b" + i + "=N:1;\nendrewards\n");
}
writerModelFile.write("\n");
// BLOCKING
writerModelFile.write("// BLOCKING (buffer is full) \n");
for(i=1; i<=this.numStations-1;i++) {
writerModelFile.write("rewards \"blocking" + i + "\"\n");
writerModelFile.write(" b" + i + "=n" +i+":1;\nendrewards\n");
}
writerModelFile.write("\n");
// STARVATION
writerModelFile.write("// STARVATION (buffer is empty) \n");
for(i=1; i<=this.numStations-1;i++) {
writerModelFile.write("rewards \"starvation" + i + "\"\n");
writerModelFile.write(" b" + i + "=0:1;\nendrewards\n");
}
writerModelFile.write("\n");
// THROUGHPUT
writerModelFile.write("// THROUGHPUT \n");
for(i=1; i<=this.numStations-1;i++) {
writerModelFile.write("rewards \"throughput_M" + i + "\"\n");
writerModelFile.write("[toc] ((m" + i + "=1 & b" +(i-1) +">0 & b" + i + "<n" + i +") & !(m" + (i+1) + "=1 & b" + i + ">0 & b" + (i+1) +"<n" + (i+1) + ")) | ((m" + i + "=1 & b" + (i-1) + ">0 & b" +i+ "<n" +i+ ") & (m" + (i+1) + "=1 & b" +i +">0 & b" +(i+1) + "<n" +(i+1) + "))" +":1;\nendrewards\n");
}
writerModelFile.write("rewards \"throughput_M" + i + "\"\n");
writerModelFile.write("[toc] ((m" + i + "=1 & b" +(i-1) +">0 & b" + i + "<n" + i +") & !(b" + i + ">0 )) | ((m" + i + "=1 & b" + (i-1) + ">0 & b" +i+ "<n" +i+ ") & (b" +i +">0 ))" +":1;\nendrewards\n");
writerModelFile.write("\n");
// ***************************************************************************************
// WRITING PROPERTY FILE
// ***************************************************************************************
writerPropsFile = new BufferedWriter( new FileWriter( this.propFileName));
// adding constants for properties
writerPropsFile.write("const int T; // time bound constant\n\n");
// safety check1 : a machine cannot be broken while its downstream buffer is down
writerPropsFile.write("// safety check1: a machine cannot be broken and its downstream buffer full\n");
writerPropsFile.write("\"safe1\": P=? [ F(");
for(i=1;i<= this.numStations-1;i++) {
writerPropsFile.write("((m" + i + "=0) & (b" + i + "=n" + i + "))" + (i<this.numStations-1? "|" : "") );
}
writerPropsFile.write(")]\n\n");
// safety check2 : full adjacent buffers cannot become both non-full in one time unit
writerPropsFile.write("// safety check2 : full adjacent buffers cannot become both non-full in one time unit\n");
//writerPropsFile.write("\"safe2\": P=? [ F(");
for(i=1;i<= this.numStations-2;i++) {
writerPropsFile.write("\"safe2_b" + i +"\": (b" + i + "=n" +i + " & b" + (i+1) + "=n" + (i+1) + ") => P<=0[X(b" + i + "<n" +i + " & b" + (i+1) + "<n" + (i+1) + ")]\n");
}
writerPropsFile.write("\"safe2_AllBuffers\": " );
for(i=1;i<= this.numStations-2;i++) {
writerPropsFile.write("((b" + i + "=n" +i + " & b" + (i+1) + "=n" + (i+1) + ") => P<=0[X(b" + i + "<n" +i + " & b" + (i+1) + "<n" + (i+1) + ")])");
writerPropsFile.write(i<this.numStations-2? " & " : "");
}
//writerPropsFile.write(")" );
writerPropsFile.write("\n\n");
writerPropsFile.write("// Probability first N buffers gets full within time T\n");
for(i=1;i<= this.numStations-1;i++) {
writerPropsFile.write("\"full_first_" + i + "_buffers\": P=? [ F<=T(");
for(int j=1;j<=i;j++) {
writerPropsFile.write("b" + j + "=n" + j + (j<i? " & " : ""));
}
writerPropsFile.write(")]\n");
}
writerPropsFile.write("\n\n");
// REWARD PROPERTIES **************************
writerPropsFile.write("// Reward-based formulae\n");
writerPropsFile.write("R{\"WIP\"}=? [ S ] \n\n"); // WIP at steady-state
for(i=1;i<= this.numStations-1;i++) {
writerPropsFile.write("R{\"B" +i+ "level\"}=? [ S ] \n"); // Buffer occupation level at steady-state
}
writerPropsFile.write("\n");
for(i=1;i<= this.numStations-1;i++) {
writerPropsFile.write("R{\"blocking" +i+ "\"}=? [ S ] \n"); // Machine blocking at steady-state
writerPropsFile.write("R{\"blocking" +i+ "\"}=? [ I=T ] \n"); // Machine blocking at time T
}
writerPropsFile.write("\n");
for(i=1;i<= this.numStations-1;i++) {
writerPropsFile.write("R{\"starvation" +i+ "\"}=? [ S ] \n"); // Machine starvation at steady-state
writerPropsFile.write("R{\"starvation" +i+ "\"}=? [ I=T ] \n"); // Machine starvation at time T
}
writerPropsFile.write("\n");
for(i=1;i<= this.numStations;i++) {
writerPropsFile.write("R{\"throughput_M" +i+ "\"}=? [ S ] \n"); // Machine starvation at steady-state
}
// P=? [ F<=T (b1=n1&b2=n2&b3=n3) ]
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
finally
{
try
{
if ( writerModelFile != null)
writerModelFile.close( );
if ( writerPropsFile != null)
writerPropsFile.close( );
}
catch (IOException e)
{
}
}
}
@Override
public String toString() {
return "PRISMGenerator [numStations=" + numStations + ", numBuffers=" + numBuffers + ", buffSize="
+ Arrays.toString(buffSize) + ", failProb=" + Arrays.toString(failProb) + ", repairProb="
+ Arrays.toString(repairProb) + ", initState(machines, buffers)=" + Arrays.toString(initState) +
", outFile=" + modelFileName + "]";
}
public static void main(String[] args) {
PRISMGenerator_2phases_properties g = new PRISMGenerator_2phases_properties();
g.setup(args[0]);
System.out.println(g);
g.generate();
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment