Commit fce2eeb0 authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY

14/7/2017:

1.Re wrote the reduceshuffle function, though some doubts are there about the approach
2. last portion where we are copying the weights have some doubt here that I want to solve in the next time i deal with the code.
3. Running the code and checking the output with other output have to check.
Sparsa Roychowdhury...
parent e4eea6fc
......@@ -12,6 +12,8 @@
<group>
<file>file:/home/sparsa/Programming/mtp/src/tpdaZone.cpp</file>
<file>file:/home/sparsa/Programming/mtp/include/timePushDown.h</file>
<file>file:/home/sparsa/Programming/mtp/src/timePushDown.cpp</file>
<file>file:/home/sparsa/Programming/mtp/main.cpp</file>
<file>file:/home/sparsa/Programming/mtp/src/tpdaCGPP.cpp</file>
<file>file:/home/sparsa/Programming/mtp/include/tpdaZone.h</file>
</group>
......
......@@ -112,170 +112,240 @@ bool identity(stateZone *vs) {
return true;;
}
}
/*bool findVector(vector <int> vector1, int val)
{
int n = find(vector1.begin(),vector1.end(),val);
if( n == vector1.end())
return false;
return true;
}*/
// reduce the #points after shuffle by using forget operation if possible and return the new state
stateZone* stateZone::reduceShuffle(stateZone* s2) {
char *del2 = s2->del, *w2 = s2->w;
char *del2 = s2->del;
short *w2 = s2->w;
char P2 = s2->P;
short f2 = s2->f;
short L = f&127;
short L2 = f2 & 127;
short curReset, reset, tempReset; // temp variables to keep reset for a range of points
char count=0; // used for storing #points in new state
char i, j; // loopers
// we have to take all the points from s2->L+1 to s2->P, point s2->L may not be there
// all the points from 1 to L of first state will be there in new state, last point P may not be there
char indexNew; // looping invariant
int lb,ub,openl,openu;
// take union of resets for points between s2->L+1(including) and s2->P(including)
curReset = 0;
for(i=L2; i < P2; i++)
curReset |= ( transitions[ del2[i] ].reset ); //this contain union of the resets in the second state
count = P + P2 - (L2+1); //total number of points before reducing the state, the point P1 and L2 are same so reduced by 1.
tempReset = curReset; // store this value for later use
stateZone *vs = new stateZone(); // new Shuffled state but not reduced.
for( i=P-1; i >= L; i--) {
reset = ( transitions[ del[i] ].reset );
vs->del = new char[count]; // allocate memory for the transitions in the state
// there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
//reset at (i+1) point of 1st state which has not reset to any of its right points for both state
if( reset & (~curReset) & (~1) ) { // (~1) : ignore the 0-th bit, used for stack operation
count++; // this point should be in new state, so increase the counter
curReset |= reset; // union reset set at this point with earlier set
}
}
vs->w = new short[count*(count-1)]; //this will hold the matrix without the diagonal element the index will be given by the macro
// 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
vs->f = f; //f contains the push complete command flag bit along with the value of L
stateZone *vs = new stateZone(); // new TA state
for(int i = 0; i < count*count ; i++) //initially fill the matrix WT1 with 0 and infinity as usual, later values will get replaced.
for(int j = 0; j < count*count ; j++)
{
if ( i == j) ////Initializing all edge values
WT1[i][j] = 0;
else if( i < j)
WT1[i][j]=INF16;
else
WT1[i][j] = 0;
}
vs->del = new char[count]; // allocate memory
vs->w = new char[count*(count-1)]; //this will hold the matrix without the diagonal element
vs->f = f; //f contains the push complete command flag bit along with the value of L
//short nf = 0; // initially flag is zero
//short dis; // distance variable
/*copying the transitions for both the states to this 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(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
//for zone the W contains the details of matrix which we need to copy and check for negetive cycle
// 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];
}
// Here we are copying points from 1 to L-1 of 1st state to new state
for(j=0; j < (L-1); j++) {
vs->del[j] = del[j];
//vs->w[j] = w[j];
// same reasons as above
// 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] ); // here f means some thing different
}
indexNew = count - 1; // index of the last transition of the new state.
//copy the point L, doing it separately because of the flag variable which is not applicable for L-th point
vs->del[L-1] = del[L-1];
//vs->w[L-1] = w[L-1]; w doesnot contains time stamps any more it contains the matrix
/*copying transition details done*/
//Here goes the logic of creating the matrix altogether with given values.
/*copying matrix details to the new state*/
// copy weights of first state to WT1
for(i=0; i < P; i++) {
for(j=0; j < P; j++) {
if(i==j) { //same transition points
//first I want to copy the transitions of the state 1.
for(int i=0; i <P; i++) {
vs->del[i] = del[i]; // copy (i+1)-th transition to (j+1) transition of new state
for(int m =0; m <P; m++)
{
if(i==m) { //same transition points
WT1[i][i] = 0;
open1[i][i] = false;
}
else if(i < j) {
WT1[i][j] = w[index(i, j, P)] & (~a32[15]); // 15-TH bit is used for open or not
else if(i < m) {
WT1[i][m] = min(int(WT1[i][m]),int(w[index((i-P), (m-P), P2)] & (~a32[15]))); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
if( w[index((i-P), (m-P), P2)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][m] = true;
else
open1[i][j] = false;
open1[i][m] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index(i, j, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
WT1[i][m] = - ( min(int(w[index((i-P), (m-P), P2)] & (~a32[15])),-int(WT1[i][m]) )); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] )
open1[i][j] = true;
if( w[index((i-P), (m-P), P2)] & a32[15] )
open1[i][m] = true;
else
open1[i][j] = false;
open1[i][m] = false;
}
}
}
//copy weights of second state to WT1
// copy weights of current state to WT1
for(i=P; i < count; i++) {
for(j=P; j < count; j++) {
char indexNew1 = indexNew;
// Here we are copying points of state 2.
for(int j=P2-1; j >=0; j--,indexNew--) {
vs->del[indexNew] = del2[j];
for(int i =P2-1 ; i >=0 ; i--,indexNew1--)
{
if(i==j) { //same transition points
WT1[i][i] = 0;
open1[i][i] = false;
WT1[indexNew][indexNew1] = 0;
open1[indexNew][indexNew1] = false;
}
else if(i < j) {
WT1[i][j] = w[index((i-P), (j-P), P2)] & (~a32[15]); // 15-TH bit is used for open or not
else if(j < i) {
WT1[indexNew][indexNew1] = min(int(w2[index(j, i, P)] & (~a32[15])),int(WT1[indexNew][indexNew1])); // 15-TH bit is used for open or not
if( w[index((i-P), (j-P), P2)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
if( w2[index(j, i, P)] & a32[15] ) // as 15th bit is used for open and close interval
open1[indexNew][indexNew1] = true;
else
open1[i][j] = false;
open1[indexNew][indexNew1] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index((i-P), (j-P), P2)] & (~a32[15]) ); // 15-TH bit is used for open or not
WT1[indexNew][indexNew1] = - (min(int( w2[index(j, i, P)] & (~a32[15])),int(WT1[indexNew][indexNew1])) ); // 15-TH bit is used for open or not
if( w[index((i-P), (j-P), P2)] & a32[15] )
open1[i][j] = true;
if( w2[index(j, i, P)] & a32[15] )
open1[indexNew][indexNew1] = true;
else
open1[i][j] = false;
open1[indexNew][indexNew1] = false;
}
}
//vs->w[j] = w[j];
// same reasons as above
// 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] ); // here f means some thing different
}
//Now before reducing the state we want to check if the state is at all feasible..
// so we run the APSP algo.
allPairSP(count+1); //this is the Floyd–Warshall algorithm implementation
short **WT;
bool **open;
if(count & 1) { // if P is odd, the shortest path stored in WT1 and open1
WT = WT1;
open = open1;
}
else{ // if P is even, the shortest path stored in WT2 and open2
WT = WT2;
open = open2;
}
//both the matrices is copied to the variable,
//here P = L2 Now we have to check the check points and their
//recent reset points
//now there are some hangng edges which are
// 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
/*
cout << "After" << endl;
for(i=0; i <= P; i++){
for(j=0; j <= P; j++) {
cout << WT[i][j] << "." << open[i][j] << "\t";
}
cout << endl << endl;
}
*/
curReset = tempReset; //get the union of resets for points between s2->L+1 and s2->P
int lb,ub,openl,openu;
// current indices j of new state we have to take care
j = (count - 1) - (P2 - L2);//this is the start of hanging points of state 2
// checking if there is any negative cycle by applying floyd warshal algorithm
for(int i=0; i <= count; i++){
if(WT[i][i] < 0 || open[i][i])
return NULL;
}
short countNew = 1; // var for storing #points in new state after applying forget operation
int forgetFlag = 0; // i-th bit of forgetFlag is 1 iff i-th point is forgotten
curReset = 0, reset = 0;
int prevPoints = 0;
for(int i=L2; i < P2; i++)
curReset |= ( transitions[ del2[i] ].reset );
for(int i=P-1; i >= L; i--,prevPoints++) {
reset = ( transitions[ del[i] ].reset );
/* there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
reset at (i+1) point of 1st state which has not reset to any of its right points for both state */
if( reset & (~curReset) & (~1) ) { // (~) : ignore the 0-th bit, used for stack operation
countNew++; // this point should be in new state, so increase the counter
curReset |= reset; // union reset set at this point with earlier set
}
else{
forgetFlag |= a32[i+1]; // i+1-th point will be forgotten in new state
}
}
char newcount = count - prevPoints + countNew;
char *newToOldRef = new char[newcount];
for(int i =0, j = 0; i < count; i++) { // find the reference from old point to new point
if( (forgetFlag & a32[i+1] ) == 0 ) {
newToOldRef[j] = i;
j++;
}
}
stateZone *vs = new stateZone(); // new TA state
vs->del = new char[newcount]; // allocate memory
vs->w = new short[newcount*newcount - newcount];
vs->f = f; // **** must edit this for tpda
vs->P = newcount;
for(int i=0; i < newcount; i++) {
vs->del[i]= del[newToOldRef[i]];
}
//vs->del[count-1] = dn;
//I have doubt on this part... have to think about it.....
///date 14/7/2017
for(int i=0;i < newcount; i++){
for(int j=0; j < newcount; j++){
if(i < j) {
vs->w[index(i, j, count)] = WT[ newToOldRef[i] ][ newToOldRef[j] ];
//cout << int(newToOldRef[i]) << "," << int(newToOldRef[j]) << endl;
if( open[ newToOldRef[i] ][ newToOldRef[j] ] )
vs->w[index(i, j, count)] |= a32[15];
}
else if(i > j) {
vs->w[index(i, j, count)] = - WT[ newToOldRef[i] ][ newToOldRef[j] ];
//cout << int(newToOldRef[i]) << "," << int(newToOldRef[j]) << endl;
if( open[ newToOldRef[i] ][ newToOldRef[j] ] )
vs->w[index(i, j, count)] |= a32[15];
}
}
}
//for(i=P-1; i >= L; i--) { //iterating on the points of the first state
// current point reset set
/* j = (count - 1) - (P2 - L2);//this is the start of hanging points of state 2
for(int k = L2 -1; k < count ; k++) //iterating through the points of second state to find any clock constraint check
for(int k = 0; k < P2 ; k++) //iterating through the points of second state to find any clock constraint check
{
for(int x=1; x <= X; x++) { // iterate for every clocks
if( isChecked(x, k) ) { // if there is a constraint for clock x in the transition k of second state
if( isChecked(x, del2[k]) ) { // if there is a constraint for clock x in the transition k of second state
lb = transitions[k].lbs[x];
ub = transitions[k].ubs[x];
openl = (transitions[k].openl) & a32[x]; // lower bound for clock x is open or not
openu = (transitions[k].openu) & a32[x];
lb = transitions[del2[k]].lbs[x];//storing the value of the upper bound of the constraint
ub = transitions[del2[k]].ubs[x]; // storing the lower bound of the constraint
openl = (transitions[del2[k]].openl) & a32[x]; // lower bound for clock x is open or not
openu = (transitions[del2[k]].openu) & a32[x]; // upper bound of the clock x is open or not
for(i=P-1; i >= L; i--) { // find reset point for clock x in the first state
reset = ( transitions[ del[i] ].reset );
if( reset & (~curReset) & (~1) && isReset(x, del[i]) ) { // if current point has more reset then seen earlier
//if the current
reset = ( transitions[ del[i] ].reset ); //storing the reset information for this transition
if( (reset & (~curReset) & (~1)) && (isReset(x, del[i])) ) { // if current point has more reset then seen earlier
//and if this point have the a reset point of the clock x
vs->del[j] = del[i]; //copy the transition number
//if( ) { // if clock x is reset at point i+1
......@@ -299,36 +369,353 @@ stateZone* stateZone::reduceShuffle(stateZone* s2) {
}
i = -1;
}
curReset |= reset;
//curReset |= reset;
j--;
lastindex = i;
//lastindex = i;
}
}
}
}
/* //vs->w[j] = w[i];
// 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
// if( !big(i+1, P) && ( i == (P-1) || (f2 & a32[L2]) ) ) {
// dis = dist(i+1, P) + mod( w2[L2] - w[P-1], M);
// if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
// nf |= a32[j+1];
// }
// }
// else {
// if( !big(i+1, lastindex+1) )
// nf |= a32[j+1];
// } */
vs->P = count; // #points in new state
*/
//vs->P = count; // #points in new state
return vs;
}
// reduce the #points after shuffle by using forget operation if possible and return the new state
//stateZone* stateZone::reduceShuffle(stateZone* s2) {
//
// char *del2 = s2->del, *w2 = s2->w;
// char P2 = s2->P;
// short f2 = s2->f;
// short L = f&127;
// short L2 = f2 & 127;
// short curReset, reset, tempReset; // temp variables to keep reset for a range of points
// char count=0; // used for storing #points in new state
// char i, j; // loopers
// int lb,ub,openl,openu;
//// char mappingS1ToNew[P];
//// char mappingS2ToNew[P2];
//// vector <int> indexNotPresentIn1;
// // we have to take all the points from s2->L+1 to s2->P, point s2->L may not be there
// // all the points from 1 to L of first state will be there in new state, last point P may not be there
//
// // take union of resets for points between s2->L+1(including) and s2->P(including)
// curReset = 0;
// for(i=L2; i < P2; i++)
// curReset |= ( transitions[ del2[i] ].reset ); //this contain union of the resets in the second state
//
// tempReset = curReset; // store this value for later use
//
// for( i=P-1; i >= L; i--) {
// reset = ( transitions[ del[i] ].reset );
//
// // there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
// //reset at (i+1) point of 1st state which has not reset to any of its right points for both state
// if( reset & (~curReset) & (~1) ) { // (~1) : ignore the 0-th bit, used for stack operation
// count++; // this point should be in new state, so increase the counter
// //storethe index
//
// curReset |= reset; // union reset set at this point with earlier set
// }
//// else
//// indexNotPresentIn1.push_back(i);
// }
//
// // 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
//// int indexOfNewState = 0;
//// for(i = 0; i < P; i++)
//// {
//// if(! findVector(indexNotPresentIn1,i))
//// {
//// mappingS1ToNew[i]=indexOfNewState;
//// indexOfNewState++;
//// }
//// else
//// mappingS1ToNew[i]= -1;
////
//// }
//
//// for(i = 0 ; i < P2; i++)
//// {
////
//// }
//
// stateZone *vs = new stateZone(); // new TA state
//
// vs->del = new char[count]; // allocate memory
// vs->w = new char[count*(count-1)]; //this will hold the matrix without the diagonal element
// vs->f = f; //f contains the push complete command flag bit along with the value of L
// for(int i = 0; i < count*count ; i++)
// for(int j = 0; j < count*count ; j++)
// {
// if ( i == j) ////Initializing all edge values
// WT1[i][j] = 0;
// else if( i < j)
// WT1[i][j]=INF16;
// else
// WT1[i][j] = 0;
// }
// //short nf = 0; // initially flag is zero
// //short dis; // distance variable
// /*copying the transitions for both the states to this 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(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
// //for zone the W contains the details of matrix which we need to copy and check for negetive cycle
// // 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];
// for(int m =P2 - 1; m >= L2; i--)
// {
// if(i==m) { //same transition points
// WT1[i][i] = 0;
// open1[i][i] = false;
// }
// else if(i < m) {
// WT1[i][m] = w2[index((i-P), (m-P), P2)] & (~a32[15]); // 15-TH bit is used for open or not
//
// if( w2[index((i-P), (m-P), P2)] & a32[15] ) // as 15th bit is used for open and close interval
// open1[i][m] = true;
// else
// open1[i][m] = false;
// }
//
// else{ ///when i > j i.e the edges coming from j to i it must be negetive.
// WT1[i][m] = - ( w2[index((i-P), (m-P), P2)] & (~a32[15]) ); // 15-TH bit is used for open or not
//
// if( w2[index((i-P), (m-P), P2)] & a32[15] )
// open1[i][m] = true;
// else
// open1[i][m] = false;
// }
// }
// }
//
// // Here we are copying points from 1 to L-1 of 1st state to new state
// for(j=0; j < (L-1); j++) {
// vs->del[j] = del[j];
// for(int i = 0; i < (L-1); i++)
// {
// if(i==j) { //same transition points
// WT1[i][i] = 0;
// open1[i][i] = false;
// }
// else if(j < i) {
// WT1[j][i] = w[index(j, i, P)] & (~a32[15]); // 15-TH bit is used for open or not
//
// if( w[index(j, i, P)] & a32[15] ) // as 15th bit is used for open and close interval
// open1[j][i] = true;
// else
// open1[j][i] = false;
// }
//
// else{ ///when i > j i.e the edges coming from j to i it must be negetive.
// WT1[j][i] = - ( w[index(j, i, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
//
// if( w[index(j, i, P)] & a32[15] )
// open1[j][i] = true;
// else
// open1[j][i] = false;
// }
// }
// //vs->w[j] = w[j];
// // same reasons as above
// // 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] ); // here f means some thing different
// }
//
// //copy the point L, doing it separately because of the flag variable which is not applicable for L-th point
// vs->del[L-1] = del[L-1];
// for(int x = 0; x < X ; x++) // checking if L have any checking or not?
// {
// if(isChecked(x,del[L-1]))
// {
// lb = transitions[del[L-1]].lbs[x];
// ub = transitions[del[L-1]].ubs[x];
// openl = (transitions[del[L-1]].openl) & a32[x]; // lower bound for clock x is open or not
// openu = (transitions[del[L-1]].openu) & a32[x];
//
// for(i=L-2; i >=0; i--) { // find reset point for clock x
//
// if( isReset(x, del[i]) ) { // if clock x is reset at point i+1
//
// // tighten the lower and upper bounds
// if( (-lb) < WT1[L-1][i] ) {
// WT1[L-1][i] = -lb;
// open1[L-1][i] = (openl & a32[x]);
// }
//
// else if( (-lb) == WT1[i][L-1] )
// open1[L-1][i] |= (openl & a32[x]);
//
// if(ub != INF) {
// if(ub < WT1[i][L-1]) {
// WT1[i][L-1] = ub;
// open1[i][L-1] = (openu & a32[x]);
// }
//
// else if( ub == WT1[i][L-1] )
// open1[i][L-1] |= (openu & a32[x]);
// }
// i = -1; //stopping the loop cause there is only one recent reset point
// }
// }
// }
// }
//
// /* //vs->w[L-1] = w[L-1]; w doesnot contains time stamps any more it contains the matrix
// /*copying transition details done*/
// //Here goes the logic of creating the matrix altogether with given values.
// /*copying matrix details to the new state*/
// // copy weights of first state to WT1
//// for(i=0; i < P; i++) {
//// for(j=0; j < P; j++) {
//// if(i==j) { //same transition points
//// WT1[i][i] = 0;
//// open1[i][i] = false;
//// }
//// else if(i < j) {
//// WT1[i][j] = w[index(i, j, P)] & (~a32[15]); // 15-TH bit is used for open or not
////
//// if( w[index(i, j, P)] & a32[15] ) // as 15th bit is used for open and close interval
//// open1[i][j] = true;
//// else
//// open1[i][j] = false;
//// }
////
//// else{ ///when i > j i.e the edges coming from j to i it must be negetive.
//// WT1[i][j] = - ( w[index(i, j, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
////
//// if( w[index(i, j, P)] & a32[15] )
//// open1[i][j] = true;
//// else
//// open1[i][j] = false;
//// }
////
//// }
//// }
// //copy weights of second state to WT1
// // copy weights of current state to WT1
//// for(i=P; i < count; i++) {
//// for(j=P; j < count; j++) {
//// if(i==j) { //same transition points
//// WT1[i][i] = 0;
//// open1[i][i] = false;
//// }
//// else if(i < j) {
//// WT1[i][j] = w[index((i-P), (j-P), P2)] & (~a32[15]); // 15-TH bit is used for open or not
////
//// if( w[index((i-P), (j-P), P2)] & a32[15] ) // as 15th bit is used for open and close interval
//// open1[i][j] = true;
//// else
//// open1[i][j] = false;
//// }
////
//// else{ ///when i > j i.e the edges coming from j to i it must be negetive.
//// WT1[i][j] = - ( w[index((i-P), (j-P), P2)] & (~a32[15]) ); // 15-TH bit is used for open or not
////
//// if( w[index((i-P), (j-P), P2)] & a32[15] )
//// open1[i][j] = true;
//// else
//// open1[i][j] = false;
//// }
////
//// }
//// }
//
// //both the matrices is copied to the variable,
// //here P = L2 Now we have to check the check points and their
// //recent reset points
// //now there are some hangng edges which are
// // 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
//
// curReset = tempReset; //get the union of resets for points between s2->L+1 and s2->P
//
// // current indices j of new state we have to take care
//
//
//
// //for(i=P-1; i >= L; i--) { //iterating on the points of the first state
// // current point reset set
//
// j = (count - 1) - (P2 - L2);//this is the start of hanging points of state 2
//
// for(int k = 0; k < P2 ; k++) //iterating through the points of second state to find any clock constraint check
// {
// for(int x=1; x <= X; x++) { // iterate for every clocks
//
// if( isChecked(x, del2[k]) ) { // if there is a constraint for clock x in the transition k of second state
//
//
// lb = transitions[del2[k]].lbs[x];//storing the value of the upper bound of the constraint
// ub = transitions[del2[k]].ubs[x]; // storing the lower bound of the constraint
// openl = (transitions[del2[k]].openl) & a32[x]; // lower bound for clock x is open or not
// openu = (transitions[del2[k]].openu) & a32[x]; // upper bound of the clock x is open or not
//
// for(i=P-1; i >= L; i--) { // find reset point for clock x in the first state
// reset = ( transitions[ del[i] ].reset ); //storing the reset information for this transition
// if( (reset & (~curReset) & (~1)) && (isReset(x, del[i])) ) { // if current point has more reset then seen earlier
// //and if this point have the a reset point of the clock x
// vs->del[j] = del[i]; //copy the transition number
// //if( ) { // if clock x is reset at point i+1
//
// // tighten the lower and upper bounds
// if( (-lb) < WT1[P][i] ) {
// WT1[P][i] = -lb;
// open1[P][i] = (openl & a32[x]);
// }
//
// else if( (-lb) == WT1[i][P] )
// open1[P][i] |= (openl & a32[x]);
//
// if(ub != INF) {
// if(ub < WT1[i][P]) {
// WT1[i][P] = ub;
// open1[i][P] = (openu & a32[x]);
// }
//
// else if( ub == WT1[i][P] )
// open1[i][P] |= (openu & a32[x]);
// }
// i = -1;
// }
// //curReset |= reset;
// j--;
// //lastindex = i;
// }
// }
// }
// }
// /* //vs->w[j] = w[i];
//
//
// // 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
// // if( !big(i+1, P) && ( i == (P-1) || (f2 & a32[L2]) ) ) {
// // dis = dist(i+1, P) + mod( w2[L2] - w[P-1], M);
// // if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
// // nf |= a32[j+1];
// // }
// // }
//
// // else {
// // if( !big(i+1, lastindex+1) )
// // nf |= a32[j+1];
// // } */
//
// vs->P = count; // #points in new state
//
// return vs;
//}
// one accuracy we yet have to compute which starts from L-th point of first state
// if( lastindex == P ) { // if we have not taken any point from L+1 to P of 1st state
......
No preview for this file type
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