Skip to content

M
mtp
Commit 67a3c636 authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY
Browse files
Options

25/10/17: 

1. Solved a serious Bug in reduce2 
2. But still have to find the special case bug.
Sparsa Roychowdhury
parent 431808ab
Hide whitespace changes
Inline Side-by-side
Showing with 327 additions and 252 deletions
drawsystem
View file @ 67a3c636
No preview for this file type
include/circuitfinder.h
View file @ 67a3c636
......@@ -62,7 +62,9 @@ public:
~CircuitFinder()
{
for(int i = 0;i < N; i++)
{
delete[] relmatrix[i];
}
delete[] relmatrix;
}
bool run(); //start the run
......
input1/test 0 → 100644
View file @ 67a3c636
3 2 1 0 0
1
3
1 2 0 0 1
1
0
2 3 0 1 0
1 1 1 1 1
0
input1/test.out 0 → 100644
View file @ 67a3c636
digraph finite_state_machine {
node [shape = point ]; qi0;
node [shape = doublecircle];3;
node [shape=circle];
qi0 -> 0;
0 -> 1 [ label = "{tn:0,x1:=0}" ];
1 -> 2 [ label = "{tn:1,x1:=0}" ];
2 -> 3 [ label = "{tn:2,1<x1<1}" ];
}
\ No newline at end of file
input1/test1
View file @ 67a3c636
......@@ -13,5 +13,5 @@
0
2 3 0 1 0
1 1 0 2 0
1 1 0 2 1
0
input1/test3 0 → 100644
View file @ 67a3c636
4 3 2 0 0
1
4
1 2 0 0 1
1
0
2 3 0 1 0
1 0 0 1 1
0
3 4 0 2 0
1 1 1 -1 1
2 0 0 1 1
0
input1/test3.out 0 → 100644
View file @ 67a3c636
digraph finite_state_machine {
node [shape = point ]; qi0;
node [shape = doublecircle];4;
node [shape=circle];
qi0 -> 0;
0 -> 1 [ label = "{tn:0,x1:=0,x2:=0}" ];
1 -> 2 [ label = "{tn:1,x1:=0}" ];
2 -> 3 [ label = "{tn:2,0<=x1<1}" ];
3 -> 4 [ label = "{tn:3,1<x1<inf,0<=x2<1}" ];
}
\ No newline at end of file
main.cpp
View file @ 67a3c636
......@@ -52,7 +52,7 @@ inline unsigned int p2(unsigned int x) {
// string to integer conversion
int str_to_int(string s) {
int sum = 0;
for(int i=0; i < s.size(); i++) {
for(unsigned int i=0; i < s.size(); i++) {
sum = sum*10 + s[i]-'0';
}
return sum;
......@@ -84,7 +84,7 @@ int main(int argc, char *argv[]) {
////**********////
setGlobal(argv[1]); // set all the global variables
bool b,b1;
bool b;
if(argc >= 3) { // If there is any arguments for special kind of TPDA
......
makefile
View file @ 67a3c636
CC := g++
CFLAG := -lm -fopenmp -Wall -std=c++14
CFLAG := -lm -fopenmp -std=c++14
SRC := ./src
OBJ := ./obj
INC := ./include
......@@ -30,7 +30,7 @@ $(OBJ)/pds.o : $(SRC)/pds.cpp
$(CC) $(GDB) -I $(INC) -c $(SRC)/pds.cpp -o $(OBJ)/pds.o $(CFLAG)
drawsystem : $(OBJ)/drawsystem.o $(OBJ)/treeBitOperations.o
$(CC $(GDB) $(OBJ)/drawsystem.o $(OBJ)/treeBitOperations.o -o drawsystem $(CFLAG)
$(CC) $(GDB) $(OBJ)/drawsystem.o $(OBJ)/treeBitOperations.o -o drawsystem $(CFLAG)
$(OBJ)/drawsystem.o : $(SRC)/drawsystem.cpp
$(CC) $(GDB) -I $(INC) -c $(SRC)/drawsystem.cpp -o $(OBJ)/drawsystem.o $(CFLAG)
......
src/timePushDown.cpp
View file @ 67a3c636
......@@ -45,7 +45,7 @@ bool** pushDone;
// make a dfs from a reset transition to find some checked transition for clock x
void getChecker(short int acttran, bool *visit, short int i, char x, bool *flag) {
short int s = transitions[i].target;
for(int j=0; j < nexttrans[s].size(); j++) {
for(unsigned int j=0; j < nexttrans[s].size(); j++) {
short int t = nexttrans[s][j];
if( isChecked(x, t) && !(*flag) && acttran == t) {
......@@ -72,7 +72,7 @@ void getChecker(short int acttran, bool *visit, short int i, char x, bool *flag)
void getresecktrans() {
bool *visit = new bool[T+1];
int i,j;
unsigned int i,j;
resecktrans.resize(X+1);
bool flag = false;
......@@ -101,7 +101,7 @@ void getresecktrans() {
// if d1 and d2 are valid pair of reset-check for only clock x1(used for one clock + one stack special tpda)
bool isPossibleReset(char d1, char d2){
for(char i=0; i < possibleresets[d2].size(); i++) {
for(unsigned int i=0; i < possibleresets[d2].size(); i++) {
if(d1 == (possibleresets[d2][i]) )
return true;
}
......@@ -171,7 +171,7 @@ void inputSystem() {
transitions[0].openl =0;
transitions[0].openu = 0;
// Reset all clocks at 0-th transition
transitions[0].reset = ( b32[X] & (~1) );
transitions[0].reset = ( b32[int(X)] & (~1) );
resettrans.resize(X+1); // used for earlier code
checktrans.resize(X+1); // used for earlier
......@@ -407,10 +407,10 @@ void inputSystem() {
//******* forget this
pushDone = new bool*[T+1];
for(char t=0; t <= T; t++){
for(unsigned int t=0; t <= T; t++){
pushDone[t] = new bool[M];
for(char w=0; w < M; w++) {
pushDone[t][w] = false;
pushDone[t][int(w)] = false;
}
}
......@@ -532,7 +532,7 @@ void print_system() {
// is clock x has been reset at transition d
bool isReset(char x, short int d) {
if( (transitions[d].reset) & a32[x])
if( (transitions[d].reset) & a32[ int(x)])
return true;
return false;
}
......@@ -540,7 +540,7 @@ bool isReset(char x, short int d) {
// is clock x has been checked at transition delta
bool isChecked(char x, short int d) {
if( (transitions[d].guard) & a32[x])
if( (transitions[d].guard) & a32[ int(x)])
return true;
return false;
}
......
src/tpdaCGPP.cpp
View file @ 67a3c636
......@@ -112,7 +112,7 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
curReset |= reset; // union reset set at this point with earlier set
}
}
// addition of 'L' below comes from the fact that all point from 1 to L of first state is there in new state
// addition of 'L' below comes from the fact that all point from 1 to L of first state is there in new state
// (s2->P - s2-> L) comes from : all points s2->L+1 to s2->P are there in new state
count += L + (P2 - L2); // #points in new state
///////////////new addition//////////
......@@ -153,7 +153,7 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
}
}
stateGCPP *vs = new stateGCPP(); // new TA state
......@@ -184,17 +184,17 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
short nf = 0; // initially flag is zero
short dis; // distance variable
j = count-1; // index of the rightmost point of new state
j = count-1; // index of the rightmost point of new state
// Here we are copying points from s2->L+1 to s2->P of 2nd state to new state
for(char i=P2 - 1; i >= L2; i--, j--) {
vs->del[j] = del2[i]; // copy (i+1)-th transition to (j+1) transition of new state
vs->w[j] = w2[i]; // copy (i+1)-th tsm to (j+1) tsm of new state
map[j] = map_p2[i];
// for(char a=P2-1, b = count-1; a>=L2; a--,b--)
// {
// if(vs->r_matrix[j][b] > s2->r_matrix[i][a])
// vs->r_matrix[j][b] = s2->r_matrix[i][a];
// }
// for(char a=P2-1, b = count-1; a>=L2; a--,b--)
// {
// if(vs->r_matrix[j][b] > s2->r_matrix[i][a])
// vs->r_matrix[j][b] = s2->r_matrix[i][a];
// }
// if distance (i+1)->(i+2) of 2nd state is accurate, then distance (j+1)->(j+2) of new state is accurate
if( f2 & a32[i+1] )
nf |= a32[j+1];
......@@ -205,11 +205,11 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
vs->del[j] = del[j];
vs->w[j] = w[j];
map[j] = map_p1[j];
// for(int a = 0 ; a < (L-1) ; a ++)
// {
// if(vs->r_matrix[j][a] > r_matrix[j][a])
// vs->r_matrix[j][a] = r_matrix[j][a];
// }
// for(int a = 0 ; a < (L-1) ; a ++)
// {
// if(vs->r_matrix[j][a] > r_matrix[j][a])
// vs->r_matrix[j][a] = r_matrix[j][a];
// }
// if distance (j+1)->(j+2) of 1st state is accurate, then distance (j+1)->(j+2) of new state is accurate
nf |= ( f & a32[j+1] );
}
......@@ -218,11 +218,11 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
vs->del[L-1] = del[L-1];
vs->w[L-1] = w[L-1];
map[L-1] = map_p1[L-1];
// for(int i = 0 ; i < L ;i++)
// {
// vs->r_matrix[vs->P-1][i] = r_matrix[P-1][i];
// vs->r_matrix[i][vs->P-1] = r_matrix[i][P-1];
// }
// for(int i = 0 ; i < L ;i++)
// {
// vs->r_matrix[vs->P-1][i] = r_matrix[P-1][i];
// vs->r_matrix[i][vs->P-1] = r_matrix[i][P-1];
// }
// Now we watch out for points from L+1 to P of 1st state
char lastindex = P;// last index of the point we have taken so far, although P might not be included
......@@ -236,17 +236,17 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
vs->del[j] = del[i];
vs->w[j] = w[i];
map[j] = map_p1[j];
// char b = (count -1) - (P2 - L2);
// for(char a = P-1; a >= L; a--)
// {
// reset2 = (transitions[del[a]].reset);
// if(reset2 &(!curReset2) & ~(1))
// {
// vs->r_matrix[j][b] = r_matrix[i][a];
// curReset2 |= reset2;
// b--;
// }
// }
// char b = (count -1) - (P2 - L2);
// for(char a = P-1; a >= L; a--)
// {
// reset2 = (transitions[del[a]].reset);
// if(reset2 &(!curReset2) & ~(1))
// {
// vs->r_matrix[j][b] = r_matrix[i][a];
// curReset2 |= reset2;
// b--;
// }
// }
if( lastindex == P ) { // if (i+1) is the first point we are considering after starting the loop
// In if : first check is for accuracy check from L to P of left state
// In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen
......@@ -293,8 +293,8 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
vs->f = nf; // add the flag variable also
//vs->P = count; // #points in new state
//cout << int(count) << "the cound " << endl;
// for(char i = 0 ; i < count ; i++)
// cout << int(map[i]) << endl;
// for(char i = 0 ; i < count ; i++)
// cout << int(map[i]) << endl;
for(char i = 0; i < count ; i ++)
for(char j = 0 ; j < count ; j++)
......@@ -584,91 +584,91 @@ stateGCPP* stateGCPP::reduce1(){
// 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) {
short dis;
// int openl,openu;
// openl = transitions[dn].openl;
// openu = transitions[dn].openu;
// relation **store_matrix = allocate_r_matrix(vs->P);
// //cout <<"Hi I am called" << endl;
// // cout << dn << wn << endl;
// for(char i = 0 ;i < vs->P; i++)
// {
// 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.
// //cout << store_matrix[i][j] << endl;
// }
// }
// bool flag1;
// cout << int(dn) << endl;
// cout << int(wn) << endl;
// cout << endl;
//#pragma openmp parallel for
// int openl,openu;
// openl = transitions[dn].openl;
// openu = transitions[dn].openu;
// relation **store_matrix = allocate_r_matrix(vs->P);
// //cout <<"Hi I am called" << endl;
// // cout << dn << wn << endl;
// for(char i = 0 ;i < vs->P; i++)
// {
// 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.
// //cout << store_matrix[i][j] << endl;
// }
// }
// bool flag1;
// cout << int(dn) << endl;
// cout << int(wn) << endl;
// cout << endl;
//#pragma openmp parallel for
for(char x=1; x <= X; x++) {
if( isChecked(x, dn) ) { // if there is a check for clock x
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 ) ;
// 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
// }
// 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
// }
//char t = vs->reset_point(dn,x); //?
if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) )
{//if the distance doesnot belong to the interval
//delete_r_matrix(store_matrix,vs->P); // this one added extra
return false;
}
// 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][vs->P-1]> les)
// store_matrix[t][vs->P-1] = les;
// }
// else //this condition is closed
// {
// if(store_matrix[t][vs->P-1] > leq)
// store_matrix[t][vs->P-1] = leq;
// }
//
// }
// if(dis == transitions[dn].ubs[x])
// {
// if((openu & a32[x])) // this condition is open
// {
// if(store_matrix[vs->P-1][t]> les)
// store_matrix[vs->P-1][t] = les;
// //flag1 = true;
// }
// else // this condition is closed.
// {
// if(store_matrix[vs->P-1][t] > leq)
// store_matrix[vs->P-1][t] = leq;
// }
//
// }
// if(dis_l == 0)
// {
// store_matrix[vs->P-2][vs->P-1] = leq;
// }
// if(flag1)
// cout << endl;
// print_r_matrix(store_matrix,vs->P);
// pairWiseTightestRelation(store_matrix,vs->P);
// if(flag1)
// print_r_matrix(store_matrix,vs->P);
// 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][vs->P-1]> les)
// store_matrix[t][vs->P-1] = les;
// }
// else //this condition is closed
// {
// if(store_matrix[t][vs->P-1] > leq)
// store_matrix[t][vs->P-1] = leq;
// }
//
// }
// if(dis == transitions[dn].ubs[x])
// {
// if((openu & a32[x])) // this condition is open
// {
// if(store_matrix[vs->P-1][t]> les)
// store_matrix[vs->P-1][t] = les;
// //flag1 = true;
// }
// else // this condition is closed.
// {
// if(store_matrix[vs->P-1][t] > leq)
// store_matrix[vs->P-1][t] = leq;
// }
//
// }
// if(dis_l == 0)
// {
// store_matrix[vs->P-2][vs->P-1] = leq;
// }
// if(flag1)
// cout << endl;
// print_r_matrix(store_matrix,vs->P);
// pairWiseTightestRelation(store_matrix,vs->P);
// if(flag1)
// print_r_matrix(store_matrix,vs->P);
else if(dis == (transitions[dn].lbs[x] ) || dis == (transitions[dn].ubs[x] ))
{
CircuitFinder cf(vs->r_matrix,vs->P);
bool b = cf.run();
if(b){
//print_r_matrix(vs->r_matrix,vs->P);
//cout << b <<endl;
//delete_r_matrix(store_matrix,vs->P);
//print_r_matrix(vs->r_matrix,vs->P);
//cout << b <<endl;
//delete_r_matrix(store_matrix,vs->P);
return false;
}
}
......@@ -681,15 +681,15 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b
}
}
}
//#pragma openmp parallel for
// for(int i = 0 ;i < vs->P; i++)
// {
// for(int j = 0; j < vs->P; j++)
// {
// 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
//#pragma openmp parallel for
// for(int i = 0 ;i < vs->P; i++)
// {
// for(int j = 0; j < vs->P; j++)
// {
// 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
return true;
}
......@@ -716,21 +716,21 @@ bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr)
//cout << int(dn) << endl;
int ub = transitions[dn].ubs[0];// the stacks upper bound
//int lb = transitions[dn].lbs[0];
// int openl,openu; //added extra
// openl = transitions[dn].openl;
// openu = transitions[dn].openu;
// relation **store_matrix = allocate_r_matrix(vs->P);
////#pragma openmp parallel for
// for(int i = 0 ;i < vs->P; i++)
// {
// 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.
// }
// }
// int openl,openu; //added extra
// openl = transitions[dn].openl;
// openu = transitions[dn].openu;
// relation **store_matrix = allocate_r_matrix(vs->P);
////#pragma openmp parallel for
// for(int i = 0 ;i < vs->P; i++)
// {
// 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.
// }
// }
if(aclr) { // if distance from L to R is small
// if(dn == 4)
// cout << "true aclr" << endl;
// if(dn == 4)
// cout << "true aclr" << endl;
short dis = dlr + mod( wn - w[P-1], M ); // mark
char t = vs->L-1; //the source of push must be L.
if( ( dis < transitions[dn].lbs[0] ) || dis > ub )
......@@ -739,38 +739,38 @@ bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr)
return false;
}
//added extra
// if(dis == transitions[dn].lbs[0]) // if the lower bound of the interval is open
// {
// if(openl & 1)
// {
// if(store_matrix[t][vs->P-1]> les)
// store_matrix[t][vs->P-1] = les;
// }
// else
// {
// if(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 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[vs->P-1][t]> les)
// store_matrix[vs->P-1][t] = les;
// }
// else
// {
// if(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 the relation must be {tsm(j) } < {tsm(i)}
// // Hence (j,i) \in R_<
// }
// if(dis == transitions[dn].lbs[0]) // if the lower bound of the interval is open
// {
// if(openl & 1)
// {
// if(store_matrix[t][vs->P-1]> les)
// store_matrix[t][vs->P-1] = les;
// }
// else
// {
// if(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 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[vs->P-1][t]> les)
// store_matrix[vs->P-1][t] = les;
// }
// else
// {
// if(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 the relation must be {tsm(j) } < {tsm(i)}
// // Hence (j,i) \in R_<
// }
//pairWiseTightestRelation(store_matrix,vs->P);
else if( dis == transitions[dn].lbs[0] || dis == ub)
{
......@@ -785,20 +785,20 @@ bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr)
{
//print_r_matrix(vs->r_matrix,vs->P);
}
}
//#pragma openmp parallel for
// for(int i = 0 ;i < vs->P; i++)
// {
// for(int j = 0; j < vs->P; j++)
// {
// vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix
// }
// }
}
//#pragma openmp parallel for
// for(int i = 0 ;i < vs->P; i++)
// {
// for(int j = 0; j < vs->P; j++)
// {
// vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix
// }
// }
}
else if(ub != INF) // if distance from L to R is big
......@@ -837,7 +837,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
char q = transitions[ del[P-1] ].target; // target state of last transition
// iterate through all the upcoming transitions
//#pragma openmp parallel for
//#pragma openmp parallel for
for(char i=0; i < nexttrans[q].size(); i++) {
dn = nexttrans[q][i]; // i-th upcoming transition
......@@ -857,7 +857,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
else{
// add next transition to this state if possible and return all generated states by doing this operation
//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)
//cout << int(dn) << endl;
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]
......@@ -882,7 +882,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
// iterate through all possible TSM value for tranistion 'dn' and check for constraints on clocks and stack
//relation rel[2] = {leq,les};
//#pragma openmp parallel for
//#pragma openmp parallel for
for(char wn=0; wn < M; wn++) {
stateGCPP* vs = reduce2(dn,wn,clockDis,clockAcc,dlr,aclr);
......@@ -896,19 +896,19 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
// if stack constraint not 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 (( !openGuardConsSat()))
else { // if clock and stack both constraints are satisfied
// stateGCPP* vs = vs1->reduce(dn);
// delete vs1;
// stateGCPP* vs = vs1->reduce(dn);
// delete vs1;
//cout << int(dn) << endl;
stateGCPP* rs = new stateGCPP();
rs->L = L; // left point remain same
rs-> P = vs->P; // #points in new state
// 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
for(char j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs
......@@ -947,7 +947,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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;
......@@ -978,7 +978,7 @@ stateGCPP* stateGCPP::nextDummy(char dn){
}
vs->del[vs->P-1] = dn; // the last point of the state contains the dn transition.
if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively
nf |= (1 | a3215) ;
......@@ -1044,7 +1044,7 @@ stateGCPP* stateGCPP::sucState(){
vs->f = nf; // copy flag information, no stack info is there till now for the template state
//we also have to copy the value of the relation matrix for those points.
for(int i = 0; i < count ;i ++)
{
for(int j =0; j < count ; j++)
......@@ -1209,9 +1209,9 @@ stateGCPP* getZeroState() {
vs->P = 1;
vs->f = 0; // no push pop info yet, no accuracy info yet
vs->allocate_r_matrix(que);
// for(int i =0 ; i < vs->P;i++) // with 'na'.
// for(int j = 0; j < vs->P; j++)
// vs->r_matrix[i][j] = que;
// for(int i =0 ; i < vs->P;i++) // with 'na'.
// for(int j = 0; j < vs->P; j++)
// vs->r_matrix[i][j] = que;
vs->del = new char[1]; // memory allocation
vs->w = new char[1];
......@@ -1590,12 +1590,12 @@ void stateGCPP::allocate_r_matrix()
r_matrix = new relation*[P];
for(int i = 0; i < P; i++)
r_matrix[i] = new relation[P];
for(int i = 0; i <P; i++)
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;}
r_matrix[i][j]=z;
else
r_matrix[i][j] = que;}
}
void stateGCPP::allocate_r_matrix(relation r)
......@@ -1612,7 +1612,7 @@ void stateGCPP::allocate_r_matrix(relation r)
else
r_matrix[i][j] = r;
}
}
relation** stateGCPP::allocate_r_matrix(char P)
{
......@@ -1624,9 +1624,9 @@ relation** stateGCPP::allocate_r_matrix(char 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;}
matrix[i][j]=z;
else
matrix[i][j] = que;}
return matrix;
}
......@@ -1644,41 +1644,64 @@ void pairWiseTightestRelation (relation **graph,int V) //this function does the
/* Initialize the solution matrix same as input graph matrix. Or
we can say the initial values of shortest distances are based
on shortest paths considering no intermediate vertex. */
for (int i = 0; i < V; i++)
for (int j = 0; j < V; j++)
dist[i][j] = graph[i][j]; // copying value to the local variable
// for (int i = 0; i < V; i++)
// for (int j = 0; j < V; j++)
// dist[i][j] = graph[i][j]; // copying value to the local variable
//
/* Add all vertices one by one to the set of intermediate vertices.
---> Before start of a iteration, we have shortest distances between all
pairs of vertices such that the shortest distances consider only the
vertices in set {0, 1, 2, .. k-1} as intermediate vertices.
----> After the end of a iteration, vertex no. k is added to the set of
intermediate vertices and the set becomes {0, 1, 2, .. k} */
for (int k = 0; k < V; k++)
{
// Pick all vertices as source one by one
for (int i = 0; i < V; i++)
{
// Pick all vertices as destination for the
// above picked source
for (int j = 0; j < V; j++)
{
// If vertex k is on the shortest path from
// i to j, then update the value of dist[i][j]
relation m = addition[dist[i][k]][dist[k][j]];
if (m < dist[i][j])
dist[i][j] = m;
for(int k=0; k < V; k++) {
for(int i=0; i < V; i++) {
for(int j=0; j < V; j++){
if(k & 1) { // if k is odd, transfer weights from dist to graph
if( ( addition[dist[i][k]][dist[k][j]] ) < dist[i][j] ) { // if using node k, we update distance from i to j
graph[i][j] = addition[dist[i][k]][dist[k][j]];
//open1[i][j] = open2[i][k] || open2[k][j] ;
}
else if( ( addition[dist[i][k]][dist[k][j]] ) == dist[i][j]) { // if any distance is open, then the new distance is also open
graph[i][j] = dist[i][j];
//open1[i][j] = open2[i][k] || open2[k][j] || open2[i][j] ;
}
else {
graph[i][j] = dist[i][j];
//open1[i][j] = open2[i][j] ;
}
}
else{ // if k is even , transfer weights from graph to dist
if( ( addition[graph[i][k]][graph[k][j]] ) < graph[i][j] ) {
dist[i][j] = addition[graph[i][k]][graph[k][j]];
//open2[i][j] = open1[i][k] || open1[k][j] ;
}
else if( ( addition[graph[i][k]][graph[k][j]] ) == graph[i][j]) {
dist[i][j] = graph[i][j];
//open2[i][j] = open1[i][k] || open1[k][j] || open1[i][j] ;
}
else{
dist[i][j] = graph[i][j];
//open2[i][j] = open1[i][j] ;
}
}
}
}
}
// Print the shortest distance matrix
//printSolution(dist,V);
//printSolution(graph,V);
if(!((V-1) & 1)){
for(int i = 0 ; i < V; i++)
for(int j = 0; j < V ; j++)
graph[i][j] = dist[i][j]; // change the original matrix
//printSolution(graph,V);
}
for(int i = 0; i < V ; i++) // delete the space allocated for the sub matrix
delete[] dist[i];
delete[] dist;
......@@ -1699,31 +1722,31 @@ char stateGCPP::reset_point(char t, char x)
{
return i;
}
}
}
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
/////
bool popflag; // 1 iff there is pop at the new transition 'dn'
bool pushAtL = isPush( del[L-1] );
short dis, dis_l = 1;
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
/////
bool popflag; // 1 iff there is pop at the new transition 'dn'
bool pushAtL = isPush( del[L-1] );
short dis, dis_l = 1;
int openl, openu;
openl = transitions[dn].openl;
openu = transitions[dn].openu;
popflag = isPop(dn);
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 i = 0; i < P; i++)
for(char j =0 ; j < P; j++)
store_matrix[i][j] = r_matrix[i][j];
for(char x = 1; x<=X;x++)
{
......@@ -1731,10 +1754,10 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
{
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.
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
......@@ -1768,7 +1791,7 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
if(dis_l == 0)
{
if(store_matrix[P-1][P] > leq)
store_matrix[P-1][P] = leq;
store_matrix[P-1][P] = leq;
}
}
}
......@@ -1811,10 +1834,10 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
// Hence (j,i) \in R_<
}
}
// if(dn==4){
// cout << "_______________________" << endl;
// print_r_matrix(store_matrix,P+1);
// }
// if(dn==4){
// cout << "_______________________" << endl;
// print_r_matrix(store_matrix,P+1);
// }
cout << "dn=" <<int(dn) << " wn=" << int(wn) << endl;
for(char i =0; i < P; i++)
......@@ -1827,12 +1850,12 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
pairWiseTightestRelation(store_matrix,P+1);
cout << "after tightning" << endl;
print_r_matrix(store_matrix,P+1);
// if(dn==4){
//
// print_r_matrix(store_matrix,P+1);
// cout << "_______________________" << endl;
// }
// if(dn==4){
//
// print_r_matrix(store_matrix,P+1);
// cout << "_______________________" << endl;
// }
short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
for( char i=P-1; i >= L; i-- ) {
......@@ -1945,5 +1968,5 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
for(char i = 0; i<=P; i++)
delete[] store_matrix[i];
delete[] store_matrix;
return vs; // return the
return vs; // return the
}
\ No newline at end of file
src/treeBitOperations.cpp
View file @ 67a3c636
......@@ -57,7 +57,7 @@ string inttobinary(int x) {
// initialization of the integer arrays a,b and c defined above
void setBits() {
char i;
unsigned int i;
unsigned int x32=1,y32=1;
......
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