Skip to content

M
mtp
Commit 568f036b authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY
Browse files
Options

26/9/17: 

1. Wrote a function to check if the guessed value of the relation actually possible
2. Still have to fill up some if and else
3. Wrote some memory all
parent 0d7183c1
Hide whitespace changes
Inline Side-by-side
Showing with 128 additions and 42 deletions
include/tpdaCGPP.h
View file @ 568f036b
...@@ -25,7 +25,9 @@ class stateGCPP{ ...@@ -25,7 +25,9 @@ class stateGCPP{
relation **r_matrix; // the matrix of relation which denotes the relation between the points fractional part. clearly the size of the matrix is P*P as p is the total number of active colors. relation **r_matrix; // the matrix of relation which denotes the relation between the points fractional part. clearly the size of the matrix is P*P as p is the total number of active colors.
relation **allocate_r_matrix(); relation **allocate_r_matrix();
relation **allocate_r_matrix(char P);
void delete_r_matrix(); void delete_r_matrix();
void delete_r_matrix(relation **matrix,char P);
void delete_del(); void delete_del();
void delete_w(); void delete_w();
void delete_all(); void delete_all();
...@@ -41,11 +43,12 @@ class stateGCPP{ ...@@ -41,11 +43,12 @@ class stateGCPP{
stateGCPP* reduce(char dn); stateGCPP* reduce(char dn);
// 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(char dn, char wn, short *clockDis, bool *clockAcc); bool consSatisfied(char dn, char wn, relation r, short *clockDis, bool *clockAcc);
// check for stack constraint where 'dlr' and 'aclr' are distance and accuracy resp. from L to R // check for stack constraint where 'dlr' and 'aclr' are distance and accuracy resp. from L to R
bool stackCheck(char dn, char wn, short dlr, bool aclr); bool stackCheck(char dn, char wn,relation r, short dlr, bool aclr);
//check if the relation between the fractional parts are good or not.
bool relationSatisfied(char dn,char wn,relation r,short *clockDis,bool *clockAcc);
// reduce the #points after shuffle operation by using forget operation if possible // reduce the #points after shuffle operation by using forget operation if possible
stateGCPP* reduceShuffle(stateGCPP* vs); stateGCPP* reduceShuffle(stateGCPP* vs);
......
src/tpdaCGPP.cpp
View file @ 568f036b
...@@ -352,36 +352,102 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -352,36 +352,102 @@ stateGCPP* stateGCPP::reduce(char dn){
// 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(char dn, char wn, short *clockDis, bool *clockAcc) { bool stateGCPP::consSatisfied(char dn, char wn,relation r, short *clockDis, bool *clockAcc) {
short dis; short dis;
int openl,openu;
openl = transitions[dn].openl;
openu = transitions[dn].openu;
relation **store_matrix = allocate_r_matrix(P+1);
for(int i = 0 ;i < P; i++)
{
for(int j = 0; j < P; j++)
{
store_matrix[i][j] = r_matrix[i][j]; //storing values of the relation matrix to detect any cycle with single les symbol in it.
}
}
for(char x=1; x <= X; x++) { for(char x=1; x <= X; x++) {
if( isChecked(x, dn) ) { // if there is a check for clock 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 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( 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
delete_r_matrix(store_matrix,P+1);
return false; return false;
}
else if( dis == transitions[dn].lbs[x] && (openl & a32[x])) //checking if the distance is equal to the upper value and the constraint is open.
{
//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_<
}
else if(dis == transitions[dn].ubs[x] && (openu & a32[x]))
{
//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_<
}
} }
else if( (transitions[dn].ubs[x]) != INF ) else if( (transitions[dn].ubs[x]) != INF )
{
delete_r_matrix(store_matrix,P+1);
return false; return false;
}
} }
} }
delete_r_matrix(store_matrix,P+1);
return true; return true;
} }
//bool stateGCPP::relationSatisfied(char dn, char wn,relation r,short *clockDis,bool *clockAcc) {
// int lowerbound,upperbound,openl,openu;
// for(char x = 1; x<= X;x++) //looping over the clocks.
// {
// if(isChecked(x,dn)) //if the clock x is checked in the transition point dn
// {
// lowerbound = transitions[dn].lbs[x];
// upperbound = transitions[dn].ubs[x];
// openl = transition[dn].openl;
// openu = transition[dn].openu;
//
// }
// }
//}
// situation : we are trying to add trans 'dn' with tsm 'wn' to the right of current state // situation : we are trying to add trans 'dn' with tsm 'wn' to the right of current state
// 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(char dn, char wn, short dlr, bool aclr) { bool stateGCPP::stackCheck(char dn, char wn,relation r, 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;
openl = transitions[dn].openl;
openu = transitions[dn].openu;
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
if( ( dis < transitions[dn].lbs[0] ) || dis > ub ) // check if d(source,destination) \in I if( ( dis < transitions[dn].lbs[0] ) || dis > ub )
{// check if d(source,destination) \in I
return false; return false;
}
else if(dis == transitions[dn].lbs[0] && (openl & 1)) // if the lower bound of the interval is open
{
//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_<
}
else if (dis == transitions[dn].ubs[0] && (openu & 1)) // if the upper bound of the interval is open
{
//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_<
}
else else
{
return true; 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
...@@ -460,46 +526,50 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -460,46 +526,50 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
} }
// iterate through all possible TSM value for tranistion 'dn' and check for constraints on clocks and stack // iterate through all possible TSM value for tranistion 'dn' and check for constraints on clocks and stack
relation rel[2] = {leq,les};
for(wn=0; wn < M; wn++) { for(wn=0; wn < M; wn++) {
for(int i = 0; i < 2;i++)
// if clock constraint not satisfied {
if( !consSatisfied( dn, wn, clockDis, clockAcc) ) { } // if clock constraint not satisfied
if( !consSatisfied( dn, wn, rel[i], clockDis, clockAcc) ) { }
// if stack constraint not satisfied
else if( ( popflag && ( !stackCheck(dn, wn, dlr, aclr) ) ) ) { }
else { // if clock and stack both constraints are satisfied
stateGCPP* rs = new stateGCPP();
rs->L = L; // left point remain same
rs-> P = vs->P; // #points in new state
rs->del = vs->del; // transitions are same as vs returned in reduce operation
rs->w = new char[vs->P]; // last tsm value different, so change the whole array of tsm's
for(j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs
rs->w[j] = vs->w[j];
}
rs->w[vs->P - 1] = wn; // new tsm value for last point
rs->f = (vs->f) & ( ~a32[vs->P - 1] ); // flag value comes from vs except for last point // if stack constraint not satisfied
else if( ( popflag && ( !stackCheck(dn, wn,rel[i], dlr, aclr) ) ) ) { } //if there is a pop and the constraint on pop is satisfied.
//else if(!relationSatisfied(dn,wn))
// 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 else { // if clock and stack both constraints are satisfied
if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) { stateGCPP* rs = new stateGCPP();
rs->L = L; // left point remain same
rs-> P = vs->P; // #points in new state
rs->del = vs->del; // transitions are same as vs returned in reduce operation
// calculate distance from 2nd last point to last point in new state rs->w = new char[vs->P]; // last tsm value different, so change the whole array of tsm's
dis = vs->w[vs->P - 1] + mod(wn - w[P-1], M); for(j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs
if(dis < M) { // reset vs->P-1 bit to 0 rs->w[j] = vs->w[j];
rs->f |= (a32[vs->P - 1]);
} }
} rs->w[vs->P - 1] = wn; // new tsm value for last point
//assume the relation of fraction part with respect to the new system.
//first assume it to be \leq rs->f = (vs->f) & ( ~a32[vs->P - 1] ); // flag value comes from vs except for last point
rs->r_matrix = rs->allocate_r_matrix();// do we need to allocate? or it is sufficent to just 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( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) {
// calculate distance from 2nd last point to last point in new state
dis = vs->w[vs->P - 1] + mod(wn - w[P-1], M);
if(dis < M) { // reset vs->P-1 bit to 0
rs->f |= (a32[vs->P - 1]);
}
}
//assume the relation of fraction part with respect to the new system.
//first assume it to be \leq
rs->r_matrix = rs->allocate_r_matrix();// do we need to allocate? or it is sufficent to just point?
//I have to allocate because this is changing //I have to allocate because this is changing
//How to propagate values?? //How to propagate values??
//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
}
} }
} }
} }
...@@ -1067,6 +1137,12 @@ void stateGCPP::delete_r_matrix() ...@@ -1067,6 +1137,12 @@ void stateGCPP::delete_r_matrix()
delete [] r_matrix[i]; delete [] r_matrix[i];
delete [] r_matrix; delete [] r_matrix;
} }
void stateGCPP::delete_r_matrix(relation** matrix,char P)
{
for(int i = 0; i < P; i++)
delete [] matrix[i];
delete [] matrix;
}
void stateGCPP::delete_del() void stateGCPP::delete_del()
{ {
...@@ -1084,4 +1160,11 @@ relation ** stateGCPP::allocate_r_matrix() ...@@ -1084,4 +1160,11 @@ relation ** 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];
}
relation** stateGCPP::allocate_r_matrix(char P)
{
relation **matrix = new relation*[P];
for(int i =0; i < P;i ++)
matrix[i] = new relation[P];
return matrix;
} }
\ No newline at end of file
tree
View file @ 568f036b
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