Skip to content

M
mtp
You need to sign in or sign up before continuing.
Commit 5b4e7740 authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY
Browse files
Options

23/10/17: 

1. Time Automata Working
2. Time push Down system is not working yet!!
parent f0234c74
Hide whitespace changes
Inline Side-by-side
Showing with 437 additions and 184 deletions
drawsystem
View file @ 5b4e7740
No preview for this file type
include/tpdaCGPP.h
View file @ 5b4e7740
...@@ -47,7 +47,7 @@ class stateGCPP{ ...@@ -47,7 +47,7 @@ class stateGCPP{
stateGCPP* reduce(char dn); stateGCPP* reduce(char dn);
stateGCPP* nextDummy(char dn); stateGCPP* nextDummy(char dn);
stateGCPP* reduce1(); stateGCPP* reduce1();
stateGCPP* reduce2(char dn, char wn,short* clockDis,bool* clockAcc,short dlr,bool aclr);
// return true iff clock gurards on new transition 'dn' with tsm value 'wn' is satisfied // return true iff clock gurards on new transition 'dn' with tsm value 'wn' is satisfied
bool consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, bool *clockAcc); bool consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, bool *clockAcc);
......
input1/test1
View file @ 5b4e7740
...@@ -13,5 +13,5 @@ ...@@ -13,5 +13,5 @@
0 0
2 3 0 1 0 2 3 0 1 0
1 1 0 2 1 1 1 0 2 0
0 0
input1/test1.out
View file @ 5b4e7740
...@@ -6,4 +6,5 @@ digraph finite_state_machine { ...@@ -6,4 +6,5 @@ digraph finite_state_machine {
0 -> 1 [ label = "{tn:0,x1:=0}" ]; 0 -> 1 [ label = "{tn:0,x1:=0}" ];
1 -> 1 [ label = "{tn:1,x1:=0}" ]; 1 -> 1 [ label = "{tn:1,x1:=0}" ];
1 -> 2 [ label = "{tn:2,2<=x1<=2}" ]; 1 -> 2 [ label = "{tn:2,2<=x1<=2}" ];
2 -> 3 [ label = "{tn:3,1<=x1<=2}" ];
} }
\ No newline at end of file
input1/test1.png
View replaced file @ f0234c74 View file @ 5b4e7740
input1/test1.png

17.6 KB | W: | H:

input1/test1.png

17.5 KB | W: | H:

input1/test1.png
input1/test1.png
input1/test1.png
input1/test1.png
  • 2-up
  • Swipe
  • Onion skin
input1/tp63.out
View file @ 5b4e7740
...@@ -5,11 +5,11 @@ digraph finite_state_machine { ...@@ -5,11 +5,11 @@ digraph finite_state_machine {
qi0 -> 0; qi0 -> 0;
0 -> 1 [ label = "{tn:0,x1:=0}" ]; 0 -> 1 [ label = "{tn:0,x1:=0}" ];
1 -> 2 [ label = "{tn:1,ps_2}" ]; 1 -> 2 [ label = "{tn:1,ps_2}" ];
1 -> 5 [ label = "{tn:2,1<=x1<=2,pp_2,6<=x2<=8}" ]; 1 -> 5 [ label = "{tn:2,1<=x1<=2,pp_2,6<=ag(2)<=8}" ];
2 -> 1 [ label = "{tn:3}" ]; 2 -> 1 [ label = "{tn:3}" ];
2 -> 2 [ label = "{tn:4,1<=x1<=1,x1:=0,ps_1}" ]; 2 -> 2 [ label = "{tn:4,1<=x1<=1,x1:=0,ps_1}" ];
2 -> 3 [ label = "{tn:5,0<=x1<=1}" ]; 2 -> 3 [ label = "{tn:5,0<=x1<=1}" ];
3 -> 4 [ label = "{tn:6}" ]; 3 -> 4 [ label = "{tn:6}" ];
4 -> 2 [ label = "{tn:7,0<=x1<=2}" ]; 4 -> 2 [ label = "{tn:7,0<=x1<=2}" ];
4 -> 4 [ label = "{tn:8,pp_1,1<=x2<=2}" ]; 4 -> 4 [ label = "{tn:8,pp_1,1<=ag(1)<=2}" ];
} }
\ No newline at end of file
input1/tp63.png
View replaced file @ f0234c74 View file @ 5b4e7740
input1/tp63.png

43.4 KB | W: | H:

input1/tp63.png

52.1 KB | W: | H:

input1/tp63.png
input1/tp63.png
input1/tp63.png
input1/tp63.png
  • 2-up
  • Swipe
  • Onion skin
src/circuitfinder.cpp
View file @ 5b4e7740
...@@ -36,6 +36,8 @@ bool2 CircuitFinder::circuit(int V) ...@@ -36,6 +36,8 @@ bool2 CircuitFinder::circuit(int V)
return F; return F;
} else if (W > S && !Blocked[W - 1]) { } else if (W > S && !Blocked[W - 1]) {
F = circuit(W); F = circuit(W);
if(F.B)
return F;
} }
} }
......
src/drawsystem.cpp
View file @ 5b4e7740
...@@ -139,16 +139,16 @@ void showsystem(char *outfile) { ...@@ -139,16 +139,16 @@ void showsystem(char *outfile) {
if(openu &a32[0]) if(openu &a32[0])
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << "inf"; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<" << "inf";
else else
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << ub; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<" << ub;
} }
else else
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf"; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<=" << "inf";
else else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<=" << ub;
} }
} }
else else
...@@ -156,16 +156,16 @@ void showsystem(char *outfile) { ...@@ -156,16 +156,16 @@ void showsystem(char *outfile) {
if(openu &a32[0]) if(openu &a32[0])
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf"; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<" << "inf";
else else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<" << ub;
} }
else else
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << "inf"; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<=" << "inf";
else else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<=" << ub;
} }
} }
} }
...@@ -181,16 +181,16 @@ void showsystem(char *outfile) { ...@@ -181,16 +181,16 @@ void showsystem(char *outfile) {
if(openu &a32[0]) if(openu &a32[0])
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << "inf"; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<" << "inf";
else else
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << ub; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<" << ub;
} }
else else
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf"; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<=" << "inf";
else else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub; tiimeoutfile << "," << lb << "<" << "ag(" << pp << ")" << "<=" << ub;
} }
} }
else else
...@@ -198,16 +198,16 @@ void showsystem(char *outfile) { ...@@ -198,16 +198,16 @@ void showsystem(char *outfile) {
if(openu &a32[0]) if(openu &a32[0])
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf"; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<" << "inf";
else else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<" << ub;
} }
else else
{ {
if(ub == INF) if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << "inf"; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<=" << "inf";
else else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub; tiimeoutfile << "," << lb << "<=" << "ag(" << pp << ")" << "<=" << ub;
} }
} }
tiimeoutfile << ",ps_" << ps; tiimeoutfile << ",ps_" << ps;
......
src/tpdaCGPP.cpp
View file @ 5b4e7740
...@@ -316,7 +316,7 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -316,7 +316,7 @@ stateGCPP* stateGCPP::reduce(char dn){
vs->del[count-1] = dn; // trans at last point, till now we don't know the weight vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
char lastindex = P; // 'lastindex' used for accuracy between two points in new state char lastindex = P; // 'lastindex' used for accuracy between two points in new state
char firstindex; //char firstindex;
char j = count-2; // assgin trans and tsm from index count-2 upto L char j = count-2; // assgin trans and tsm from index count-2 upto L
short dis; // variable for distance calculation short dis; // variable for distance calculation
// **** edit last bit of accuracy when u know the tsm of dn // **** edit last bit of accuracy when u know the tsm of dn
...@@ -338,7 +338,7 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -338,7 +338,7 @@ stateGCPP* stateGCPP::reduce(char dn){
// store the distance from last point(active in new state) before dn and P in vs->w[count-1] // store the distance from last point(active in new state) before dn and P in vs->w[count-1]
// we yet don't know the tsm for 'dn', so full calculation is not done in this function // we yet don't know the tsm for 'dn', so full calculation is not done in this function
else{ else{
firstindex = i; //firstindex = i;
if( !big(i+1, P) ) if( !big(i+1, P) )
nf |= a32[j+1]; nf |= a32[j+1];
vs->w[count-1] = dist(i+1, P); vs->w[count-1] = dist(i+1, P);
...@@ -499,28 +499,28 @@ stateGCPP* stateGCPP::reduce1(){ ...@@ -499,28 +499,28 @@ stateGCPP* stateGCPP::reduce1(){
// last distance accuracy // last distance accuracy
vs->f = nf; // add partial flag variable to new state vs->f = nf; // add partial flag variable to new state
print_r_matrix(vs->r_matrix,vs->P); //print_r_matrix(vs->r_matrix,vs->P);
return vs; // return the partially new state, **** last tsm missing with partial nf as given return vs; // return the partially new state, **** last tsm missing with partial nf as given
} }
// return true if constraint on new transition dn with tsm wn is satisfied while adding current transiton 'dn' to the right // return true if constraint on new transition dn with tsm wn is satisfied while adding current transiton 'dn' to the right
bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, bool *clockAcc) { bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, bool *clockAcc) {
short dis,dis_l=1; short dis;
int openl,openu; // int openl,openu;
openl = transitions[dn].openl; // openl = transitions[dn].openl;
openu = transitions[dn].openu; // openu = transitions[dn].openu;
relation **store_matrix = allocate_r_matrix(vs->P); // relation **store_matrix = allocate_r_matrix(vs->P);
//cout <<"Hi I am called" << endl; // //cout <<"Hi I am called" << endl;
// cout << dn << wn << endl; // // cout << dn << wn << endl;
for(char i = 0 ;i < vs->P; i++) // for(char i = 0 ;i < vs->P; i++)
{ // {
for(char j = 0; j < vs->P; j++) // for(char j = 0; j < vs->P; j++)
{ // {
store_matrix[i][j] = vs->r_matrix[i][j]; //storing values of the relation matrix to detect any cycle with single les symbol in it. // store_matrix[i][j] = vs->r_matrix[i][j]; //storing values of the relation matrix to detect any cycle with single les symbol in it.
//cout << store_matrix[i][j] << endl; // //cout << store_matrix[i][j] << endl;
} // }
} // }
// bool flag1; // bool flag1;
// cout << int(dn) << endl; // cout << int(dn) << endl;
// cout << int(wn) << endl; // cout << int(wn) << endl;
...@@ -531,85 +531,88 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b ...@@ -531,85 +531,88 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b
if( clockAcc[x] ) { // if distance from last reset of clock x to point P is accurate if( clockAcc[x] ) { // if distance from last reset of clock x to point P is accurate
dis = clockDis[x] + mod( wn - w[P-1], M ) ; dis = clockDis[x] + mod( wn - w[P-1], M ) ;
if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) { // if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) {
/*********************#***************/ // /*********************#***************/
dis_l = vs->w[vs->P - 1] + mod(wn - w[P-1], M); //distance with the last point // dis_l = vs->w[vs->P - 1] + mod(wn - w[P-1], M); //distance with the last point
} // }
char t = vs->reset_point(dn,x); //? //char t = vs->reset_point(dn,x); //?
if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) ) if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) )
{//if the distance doesnot belong to the interval {//if the distance doesnot belong to the interval
delete_r_matrix(store_matrix,vs->P); // this one added extra //delete_r_matrix(store_matrix,vs->P); // this one added extra
return false; return false;
} }
if( dis == transitions[dn].lbs[x]) //checking if the distance is equal to the upper value and the constraint is open. // if( dis == transitions[dn].lbs[x]) //checking if the distance is equal to the upper value and the constraint is open.
{ // {
//
if((openl & a32[x])) //this condition is open // if((openl & a32[x])) //this condition is open
{ // {
//
if(store_matrix[t][vs->P-1]> les) // if(store_matrix[t][vs->P-1]> les)
store_matrix[t][vs->P-1] = les; // store_matrix[t][vs->P-1] = les;
} // }
else //this condition is closed // else //this condition is closed
{ // {
if(store_matrix[t][vs->P-1] > leq) // if(store_matrix[t][vs->P-1] > leq)
store_matrix[t][vs->P-1] = leq; // store_matrix[t][vs->P-1] = leq;
} // }
//
} // }
if(dis == transitions[dn].ubs[x]) // if(dis == transitions[dn].ubs[x])
{ // {
if((openu & a32[x])) // this condition is open // if((openu & a32[x])) // this condition is open
{ // {
if(store_matrix[vs->P-1][t]> les) // if(store_matrix[vs->P-1][t]> les)
store_matrix[vs->P-1][t] = les; // store_matrix[vs->P-1][t] = les;
//flag1 = true; // //flag1 = true;
} // }
else // this condition is closed. // else // this condition is closed.
{ // {
if(store_matrix[vs->P-1][t] > leq) // if(store_matrix[vs->P-1][t] > leq)
store_matrix[vs->P-1][t] = leq; // store_matrix[vs->P-1][t] = leq;
} // }
//
} // }
if(dis_l == 0) // if(dis_l == 0)
{ // {
store_matrix[vs->P-2][vs->P-1] = leq; // store_matrix[vs->P-2][vs->P-1] = leq;
} // }
// if(flag1) // if(flag1)
cout << endl; // cout << endl;
print_r_matrix(store_matrix,vs->P); // print_r_matrix(store_matrix,vs->P);
pairWiseTightestRelation(store_matrix,vs->P); // pairWiseTightestRelation(store_matrix,vs->P);
// if(flag1) // if(flag1)
// print_r_matrix(store_matrix,vs->P); // print_r_matrix(store_matrix,vs->P);
CircuitFinder cf(store_matrix,vs->P); else if(dis == (transitions[dn].lbs[x] ) || dis == (transitions[dn].ubs[x] ))
bool b = cf.run(); {
if(b){ CircuitFinder cf(vs->r_matrix,vs->P);
print_r_matrix(store_matrix,vs->P); bool b = cf.run();
if(b){
//print_r_matrix(store_matrix,vs->P);
//cout << b <<endl; //cout << b <<endl;
delete_r_matrix(store_matrix,vs->P); //delete_r_matrix(store_matrix,vs->P);
return false; return false;
}
} }
} }
else if( (transitions[dn].ubs[x]) != INF ) else if( (transitions[dn].ubs[x]) != INF )
{ {
delete_r_matrix(store_matrix,vs->P); // this one added extra //delete_r_matrix(store_matrix,vs->P); // this one added extra
return false; return false;
} }
} }
} }
//#pragma openmp parallel for //#pragma openmp parallel for
for(int i = 0 ;i < vs->P; i++) // for(int i = 0 ;i < vs->P; i++)
{ // {
for(int j = 0; j < vs->P; j++) // for(int j = 0; j < vs->P; j++)
{ // {
vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix // vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix
} // }
} // }
delete_r_matrix(store_matrix,vs->P); //this one added extra // delete_r_matrix(store_matrix,vs->P); //this one added extra
return true; return true;
} }
...@@ -634,81 +637,86 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b ...@@ -634,81 +637,86 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b
// check for stack constraint where dlr and aclr are distance and accuracy from L to R resp. // check for stack constraint where dlr and aclr are distance and accuracy from L to R resp.
bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr) { bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr) {
int ub = transitions[dn].ubs[0];// the stacks upper bound int ub = transitions[dn].ubs[0];// the stacks upper bound
int openl,openu; //added extra int lb = transitions[dn].lbs[0];
openl = transitions[dn].openl; // int openl,openu; //added extra
openu = transitions[dn].openu; // openl = transitions[dn].openl;
relation **store_matrix = allocate_r_matrix(vs->P); // openu = transitions[dn].openu;
//#pragma openmp parallel for // relation **store_matrix = allocate_r_matrix(vs->P);
for(int i = 0 ;i < vs->P; i++) ////#pragma openmp parallel for
{ // for(int i = 0 ;i < vs->P; i++)
for(int j = 0; j < vs->P; j++) // {
{ // for(int j = 0; j < vs->P; j++)
store_matrix[i][j] = vs->r_matrix[i][j]; //storing values of the relation matrix to detect any cycle with single les symbol in it. // {
} // store_matrix[i][j] = vs->r_matrix[i][j]; //storing values of the relation matrix to detect any cycle with single les symbol in it.
} // }
// }
if(aclr) { // if distance from L to R is small if(aclr) { // if distance from L to R is small
short dis = dlr + mod( wn - w[P-1], M ); // mark short dis = dlr + mod( wn - w[P-1], M ); // mark
char t = vs->L-1; //the source of push must be L. char t = vs->L-1; //the source of push must be L.
if( ( dis < transitions[dn].lbs[0] ) || dis > ub ) if( ( dis < lb ) || dis > ub )
{// check if d(source,destination) \in I {// check if d(source,destination) \in I
delete_r_matrix(store_matrix,vs->P); //delete_r_matrix(store_matrix,vs->P);
return false; return false;
} }
//added extra //added extra
if(dis == transitions[dn].lbs[0]) // if the lower bound of the interval is open // if(dis == transitions[dn].lbs[0]) // if the lower bound of the interval is open
{ // {
if(openl & 1) // if(openl & 1)
{ // {
if(store_matrix[t][vs->P-1]> les) // if(store_matrix[t][vs->P-1]> les)
store_matrix[t][vs->P-1] = les; // store_matrix[t][vs->P-1] = les;
} // }
else // else
{ // {
if(store_matrix[t][vs->P-1] > leq) // if(store_matrix[t][vs->P-1] > leq)
store_matrix[t][vs->P-1] = leq; // store_matrix[t][vs->P-1] = leq;
} // }
//Here have to check the relationship of the fractional parts of the source and target // //Here have to check the relationship of the fractional parts of the source and target
// Here the relation must be {tsm(i)} < {tsm(j)} // // Here the relation must be {tsm(i)} < {tsm(j)}
// hence (i,j) \in R_< // // hence (i,j) \in R_<
} // }
if (dis == transitions[dn].ubs[0]) // if the upper bound of the interval is open // if (dis == transitions[dn].ubs[0]) // if the upper bound of the interval is open
{ // {
if(openu & 1) // if(openu & 1)
{ // {
if(store_matrix[vs->P-1][t]> les) // if(store_matrix[vs->P-1][t]> les)
store_matrix[vs->P-1][t] = les; // store_matrix[vs->P-1][t] = les;
} // }
else // else
{ // {
if(store_matrix[vs->P-1][t] > leq) // if(store_matrix[vs->P-1][t] > leq)
store_matrix[vs->P-1][t] = leq; // store_matrix[vs->P-1][t] = leq;
} // }
//here we have to check the relationship of the fractional parts of the source and target // //here we have to check the relationship of the fractional parts of the source and target
//Here the relation must be {tsm(j) } < {tsm(i)} // //Here the relation must be {tsm(j) } < {tsm(i)}
// Hence (j,i) \in R_< // // Hence (j,i) \in R_<
// }
//pairWiseTightestRelation(store_matrix,vs->P);
else if( dis == lb || dis == ub)
{
CircuitFinder cf(vs->r_matrix,vs->P);
bool b = cf.run();
if(b)
return false;
} }
pairWiseTightestRelation(store_matrix,vs->P);
CircuitFinder cf(store_matrix,vs->P);
bool b = cf.run();
if(b)
return false;
else else
{ return true;
//#pragma openmp parallel for //#pragma openmp parallel for
for(int i = 0 ;i < vs->P; i++) // for(int i = 0 ;i < vs->P; i++)
{ // {
for(int j = 0; j < vs->P; j++) // for(int j = 0; j < vs->P; j++)
{ // {
vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix // vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix
} // }
} // }
return true;
}
} }
else if(ub == INF) // if distance from L to R is big else if(ub == INF) // if distance from L to R is big
return true; return true;
delete_r_matrix(store_matrix,vs->P); //delete_r_matrix(store_matrix,vs->P);
return false; // distance is big, but upper bound is not infinity return false; // distance is big, but upper bound is not infinity
} }
...@@ -737,7 +745,8 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -737,7 +745,8 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
//char i, j; // loooper //char i, j; // loooper
short dis; // distance calculation variable short dis; // distance calculation variable
//cout << int(P) << endl;
//cout << int(del[P-1]) <<endl;
char q = transitions[ del[P-1] ].target; // target state of last transition char q = transitions[ del[P-1] ].target; // target state of last transition
// iterate through all the upcoming transitions // iterate through all the upcoming transitions
...@@ -760,8 +769,8 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -760,8 +769,8 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
// o.w try to add new transtitions to the right // o.w try to add new transtitions to the right
else{ else{
// add next transition to this state if possible and return all generated states by doing this operation // add next transition to this state if possible and return all generated states by doing this operation
cout << int(dn)<<endl; //cout << int(dn)<<endl;
stateGCPP* vs1 = nextDummy(dn); // get partial new state after adding transition 'dn'(TSM for 'dn' not known yet) // stateGCPP* vs1 = nextDummy(dn); // get partial new state after adding transition 'dn'(TSM for 'dn' not known yet)
short *clockDis = new short[X + 1]; // distance from last reset of clock x to point P, stored in clockDis[x] short *clockDis = new short[X + 1]; // distance from last reset of clock x to point P, stored in clockDis[x]
bool *clockAcc = new bool[X + 1]; // accuracy from last reset of clock x to point P, stored in clockAcc[x] bool *clockAcc = new bool[X + 1]; // accuracy from last reset of clock x to point P, stored in clockAcc[x]
...@@ -789,30 +798,37 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -789,30 +798,37 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
//#pragma openmp parallel for //#pragma openmp parallel for
for(char wn=0; wn < M; wn++) { for(char wn=0; wn < M; wn++) {
stateGCPP* vs = reduce2(dn,wn,clockDis,clockAcc,dlr,aclr);
//is it checking after adding the point to the state returned by reduce? //is it checking after adding the point to the state returned by reduce?
// if clock constraint not satisfied // if clock constraint not satisfied
if( !consSatisfied( vs1,dn, wn, clockDis, clockAcc) ) { } if( !consSatisfied( vs,dn, wn, clockDis, clockAcc) )
{
}
// if stack constraint not satisfied // if stack constraint not satisfied
else if( ( popflag && ( !stackCheck(vs1,dn, wn, dlr, aclr) ) ) ) { } //if there is a pop and the constraint on pop is satisfied. else if( ( popflag && ( !stackCheck(vs,dn, wn, dlr, aclr) ) ) )
{
} //if there is a pop and the constraint on pop is satisfied.
//else if(!relationSatisfied(dn,wn)) //else if(!relationSatisfied(dn,wn))
//else if (( !openGuardConsSat())) //else if (( !openGuardConsSat()))
else { // if clock and stack both constraints are satisfied else { // if clock and stack both constraints are satisfied
stateGCPP* vs = vs1->reduce(dn); // stateGCPP* vs = vs1->reduce(dn);
delete vs1; // delete vs1;
stateGCPP* rs = new stateGCPP(); stateGCPP* rs = new stateGCPP();
rs->L = L; // left point remain same rs->L = L; // left point remain same
rs-> P = vs->P; // #points in new state rs-> P = vs->P; // #points in new state
rs->del = vs->del; // transitions are same as vs returned in reduce operation // transitions are same as vs returned in reduce operation
rs->del = new char[vs->P];
rs->w = new char[vs->P]; // last tsm value different, so change the whole array of tsm's rs->w = new char[vs->P]; // last tsm value different, so change the whole array of tsm's
for(char j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs for(char j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs
rs->w[j] = vs->w[j]; rs->w[j] = vs->w[j];
rs->del[j] = vs->del[j];
} }
rs->w[vs->P - 1] = wn; // new tsm value for last point rs->w[vs->P - 1] = wn; // new tsm value for last point
rs->del[vs->P-1] = dn;
rs->f = (vs->f) & ( ~a32[vs->P - 1] ); // flag value comes from vs except for last point rs->f = (vs->f) & ( ~a32[vs->P - 1] ); // flag value comes from vs except for last point
// if distance from the active point just before 'dn'(in new state) to point P(in old state) is accurate, (vs->P) > 1 means that we have taken at least one point from old state // if distance from the active point just before 'dn'(in new state) to point P(in old state) is accurate, (vs->P) > 1 means that we have taken at least one point from old state
...@@ -828,7 +844,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -828,7 +844,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
} }
//assume the relation of fraction part with respect to the new system. //assume the relation of fraction part with respect to the new system.
//first assume it to be \leq //first assume it to be \leq
rs->allocate_r_matrix();// do we need to allocate? or it is sufficent to just point? rs->allocate_r_matrix(que);// do we need to allocate? or it is sufficent to just point?
for(int a = 0 ;a < rs->P; a++) for(int a = 0 ;a < rs->P; a++)
{ {
for(int b = 0; b < rs->P; b++) for(int b = 0; b < rs->P; b++)
...@@ -841,8 +857,10 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -841,8 +857,10 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
//vs->r_matrix; //vs->r_matrix;
v.push_back(rs); // rs will be a reachable state after add operation v.push_back(rs); // rs will be a reachable state after add operation
} }
//removing after finishing with it //removing after finishing with it
delete vs;
} }
delete[] clockDis,clockAcc; delete[] clockDis,clockAcc;
} }
...@@ -855,25 +873,25 @@ stateGCPP* stateGCPP::nextDummy(char dn){ ...@@ -855,25 +873,25 @@ stateGCPP* stateGCPP::nextDummy(char dn){
//this function adds the new transition without removing any points. //this function adds the new transition without removing any points.
//then check if the returned thing works or not. //then check if the returned thing works or not.
short nf =f; short nf =f;
stateGCPP* vs = new stateGCPP(); stateGCPP* vs = new stateGCPP();// create the dummy state
vs->P = P+1; // adding extra point. vs->P = P+1; // we are adding a new point to the dummy state without deletion
vs->L = L; vs->L = L; // the left point remains the same as before
vs->del = new char[vs->P]; vs->del = new char[vs->P]; //the number of transitions is same as number of points
vs->w = new char[vs->P]; vs->w = new char[vs->P];// similar as above
vs->allocate_r_matrix(que); vs->allocate_r_matrix(que); // we are allocating a matrix
for(char i = 0 ; i < vs->P-1 ; i++) for(char i = 0 ; i < vs->P-1 ; i++) //the values upto point P-1 is same
{ {
vs->del[i] = del[i]; vs->del[i] = del[i];//copying the transitions
vs->w[i] = w[i]; vs->w[i] = w[i]; // copying the weights
for(char j = 0; j < vs->P-1; j++) for(char j = 0; j < vs->P-1; j++) // copying the values of the relation matrix
{ {
vs->r_matrix[i][j] = r_matrix[i][j]; vs->r_matrix[i][j] = r_matrix[i][j];
} }
} }
vs->del[vs->P-1] = dn; vs->del[vs->P-1] = dn; // the last point of the state contains the dn transition.
if( !big(P-1, P-1) )
nf |= a32[vs->P -1];
vs->w[vs->P-1] = dist(P-1, P-1);
if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively
nf |= (1 | a3215) ; nf |= (1 | a3215) ;
else else
...@@ -1311,6 +1329,7 @@ bool isEmptyGCPP() { ...@@ -1311,6 +1329,7 @@ bool isEmptyGCPP() {
cout << count << endl; cout << count << endl;
*/ */
//cout << count << endl;
rs = allStates[count].first; // get the state at index count, process this state now rs = allStates[count].first; // get the state at index count, process this state now
...@@ -1475,6 +1494,12 @@ void stateGCPP::allocate_r_matrix() ...@@ -1475,6 +1494,12 @@ void stateGCPP::allocate_r_matrix()
r_matrix = new relation*[P]; r_matrix = new relation*[P];
for(int i = 0; i < P; i++) for(int i = 0; i < P; i++)
r_matrix[i] = new relation[P]; r_matrix[i] = new relation[P];
for(int i = 0; i <P; i++)
for(int j = 0; j < P; j++)
{if(i==j)
r_matrix[i][j]=z;
else
r_matrix[i][j] = que;}
} }
void stateGCPP::allocate_r_matrix(relation r) void stateGCPP::allocate_r_matrix(relation r)
...@@ -1500,6 +1525,12 @@ relation** stateGCPP::allocate_r_matrix(char P) ...@@ -1500,6 +1525,12 @@ relation** stateGCPP::allocate_r_matrix(char P)
relation **matrix = new relation*[P]; relation **matrix = new relation*[P];
for(int i =0; i < P;i ++) for(int i =0; i < P;i ++)
matrix[i] = new relation[P]; matrix[i] = new relation[P];
for(int i = 0; i <P; i++)
for(int j = 0; j < P; j++)
{ if(i==j)
matrix[i][j]=z;
else
matrix[i][j] = que;}
return matrix; return matrix;
} }
...@@ -1576,4 +1607,223 @@ char stateGCPP::reset_point(char t, char x) ...@@ -1576,4 +1607,223 @@ char stateGCPP::reset_point(char t, char x)
} }
} }
return -1; return -1;
}
stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,short dlr,bool aclr){
short reset; // variable for reset bit vector
short nf = 0; // flag variable for new state
char count = 0; // #points in new state
//char i; // looper
/////
short dis, dis_l = 1;
int openl, openu;
openl = transitions[dn].openl;
openu = transitions[dn].openu;
relation ** store_matrix = allocate_r_matrix(P+1);
for(char i = 0; i < P-1; i++)
for(char j =0 ; j < P-1; j++)
store_matrix[i][j] = r_matrix[i][j];
for(char x = 1; x<=X;x++)
{
if(isChecked(x,dn))
{
if(clockAcc[x])
{
dis = clockDis[x] + mod(wn - w[P-1],M);
dis_l = wn - w[P-1];
char t = reset_point(dn,x);
if( dis == transitions[dn].lbs[x]) //checking if the distance is equal to the upper value and the constraint is open.
{
if((openl & a32[x])) //this condition is open
{
if(store_matrix[t][P]> les)
store_matrix[t][P] = les;
}
else //this condition is closed
{
if(store_matrix[t][P] > leq)
store_matrix[t][P] = leq;
}
}
if(dis == transitions[dn].ubs[x])
{
if((openu & a32[x])) // this condition is open
{
if(store_matrix[P][t]> les)
store_matrix[P][t] = les;
//flag1 = true;
}
else // this condition is closed.
{
if(store_matrix[P][t] > leq)
store_matrix[P][t] = leq;
}
}
if(dis_l == 0)
{
store_matrix[P-1][P] = leq;
}
}
}
}
if(aclr)
{
short dis = dlr + mod(wn - w[P-1],M);
char t = L-1;
if(dis == transitions[dn].lbs[0]) // if the lower bound of the interval is open
{
if(openl & 1)
{
if(store_matrix[t][P]> les)
store_matrix[t][P] = les;
}
else
{
if(store_matrix[t][P] > leq)
store_matrix[t][P] = leq;
}
//Here have to check the relationship of the fractional parts of the source and target
// Here the relation must be {tsm(i)} < {tsm(j)}
// hence (i,j) \in R_<
}
if (dis == transitions[dn].ubs[0]) // if the upper bound of the interval is open
{
if(openu & 1)
{
if(store_matrix[P][t]> les)
store_matrix[P][t] = les;
}
else
{
if(store_matrix[P][t] > leq)
store_matrix[P][t] = leq;
}
//here we have to check the relationship of the fractional parts of the source and target
//Here the relation must be {tsm(j) } < {tsm(i)}
// Hence (j,i) \in R_<
}
}
pairWiseTightestRelation(store_matrix,P+1);
//print_r_matrix(store_matrix,P+1);
short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
for( char i=P-1; i >= L; i-- ) {
reset = transitions[ del[i] ].reset; // reset at transition at the (i+1)-th point
if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has more reset than found so far at right
curReset |= reset; // the 'curReset' will have more bit with value '1'
count++; // we have to take (i+1)-th point
}
}
// all the hanging points and point L and point for transition 'dn' also be there
count += (L+1); // number of points in new state
// pointer to the new state
stateGCPP* vs = new stateGCPP();
vs->P = count; // #points in new state
int map[vs->P]; //mapping points of parent state to child state
vs->L = L; // left point remain same
//**************ALLOCATING MEMORY FOR THE DYNAMICALLY ALLOCATED VARIABLES *****************//
vs->del = new char[count]; // memory allocation for new state transition
vs->w = new char[count]; // memory allocation for new state tsm values
vs->allocate_r_matrix(que); //allocating memory for the matrix for open guard checking
//*************ASSIGNING VALUES TO THE DYNAMICALLY ALLOCATED VARIABLES*****************//
for(char i=0; i < L; i++) { // hanging points and left point(L) remain same
vs->del[i] = del[i];
vs->w[i] = w[i];
map[i] = i; //copying the map upto L-1
// for(int j = 0; j< L; j++)
// vs->r_matrix[i][j] = r_matrix[i][j]; // copying the matrix value for the hanging points
}
for(char i=1; i < L; i++) { // distances between points upto point L remain same
nf |= ( f & a32[i] );
}
vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
char lastindex = P; // 'lastindex' used for accuracy between two points in new state
//char firstindex;
char j = count-2; // assgin trans and tsm from index count-2 upto L
//short dis; // variable for distance calculation
// **** edit last bit of accuracy when u know the tsm of dn
curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
//int vslastindex = vs->P -1; //the last index of the new state vs;
for(char i=P-1; i >= L; i--) {
reset = transitions[ del[i] ].reset; // reset at i+1-th point
if( reset & (~curReset) & (~1) ) {
vs->del[j] = del[i]; // i-th index trans will be part of new state at j-th index
vs->w[j] = w[i]; // i-th index tsm will be part of new state at j-th index
map[j]=i;
if( lastindex != P ) {
if( !big(i+1, lastindex+1) )
nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state
}
// store the accuracy from last point(active in new state) before dn and P in i+1-th bit of nf
// store the distance from last point(active in new state) before dn and P in vs->w[count-1]
// we yet don't know the tsm for 'dn', so full calculation is not done in this function
else{
//firstindex = i;
if( !big(i+1, P) )
nf |= a32[j+1];
vs->w[count-1] = dist(i+1, P);
}
lastindex = i; // this is now the last index
j--; // go to previous point
//vslastindex--;
}
}
//pairWiseTightestRelation(r_matrix,P);
map[count-1] = P;
for(char i = 0; i < vs->P; i++)// this code may change, later.
{
for(char j = 0 ; j< vs->P; j++)
{
vs->r_matrix[i][j]=store_matrix[map[i]][map[j]]; //copying r_matrix values
}
}
// we have to set the accuracy for point L to L+1 in new state
if( lastindex != P ) {
if( !big(L, lastindex+1) ) {
// vs->w[count-1] = dist(L, lastindex+1) ;
nf |= a32[L]; // set the accuracy for (j+1)-th bit of new state
}
}
// store the accuracy from last point(active in new state) before dn and P in i+1-th bit of nf
// store the distance from last point(active in new state) before dn and P in vs->w[count-1]
// we yet don't know the tsm for 'dn', so full calculation is not done in this function
else{ // if you have not choosed any point in the middle starting from point P**
if( !big(L, P) )
nf |= a32[L];
vs->w[count-1] = dist(L, P);
}
if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively
nf |= (1 | a3215) ;
else
nf |= (f & 1) ; // previous push information remain same
// last distance accuracy
vs->f = nf; // add partial flag variable to new state
//print_r_matrix(vs->r_matrix,vs->P);
for(char i = 0; i<=P; i++)
delete[] store_matrix[i];
delete[] store_matrix;
return vs; // return the
} }
\ No newline at end of file
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