Skip to content

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

11/10/17: 

1. Rewritten the conssat and stackconssat
2. resolved some bugs
3. a bug? found in the earlier code have to ask ilias
4. have to implement shuffle and addnext both
parent a3aedafb
Show whitespace changes
Inline Side-by-side
Showing with 85 additions and 34 deletions
include/tpdaCGPP.h
View file @ f1349727
......@@ -25,6 +25,7 @@ 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 **allocate_r_matrix();
relation **allocate_r_matrix(relation r);
relation **allocate_r_matrix(char P);
void delete_r_matrix();
void delete_r_matrix(relation **matrix,char P);
......
src/tpdaCGPP.cpp
View file @ f1349727
......@@ -267,7 +267,7 @@ stateGCPP* stateGCPP::reduce(char dn){
vs->del = new char[count]; // memory allocation for new state transition
vs->w = new char[count]; // memory allocation for new state tsm values
vs->r_matrix = vs->allocate_r_matrix(); //allocating memory for the matrix for open guard checking
vs->r_matrix = vs->allocate_r_matrix(que); //allocating memory for the matrix for open guard checking
//*************ASSIGNING VALUES TO THE DYNAMICALLY ALLOCATED VARIABLES*****************//
for(i=0; i < L; i++) { // hanging points and left point(L) remain same
vs->del[i] = del[i];
......@@ -355,11 +355,11 @@ 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
bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char wn, short *clockDis, bool *clockAcc) {
short dis;
short dis,dis_l=1;
int openl,openu;
openl = transitions[dn].openl;
openu = transitions[dn].openu;
relation **store_matrix = allocate_r_matrix(vs->P+1);
relation **store_matrix = allocate_r_matrix(vs->P);
for(int i = 0 ;i < vs->P; i++)
{
for(int j = 0; j < vs->P; j++)
......@@ -372,10 +372,14 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
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 ) ;
char t = transitionMap[recent_matrix[dn][x]];
if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) {
/*********************#***************/
dis_l = vs->w[vs->P - 2] + mod(wn - w[P-1], M); //distance with the last point
}
char t = transitionMap[recent_matrix[dn][x-1]]; //?
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+1); // this one added extra
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.
......@@ -384,11 +388,13 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
if((openl & a32[x])) //this condition is open
{
store_matrix[t][vs->P]= les;
if(store_matrix[t][vs->P-1]> les)
store_matrix[t][vs->P-1] = les;
}
else //this condition is closed
{
store_matrix[t][vs->P] = leq;
if(store_matrix[t][vs->P-1] > leq)
store_matrix[t][vs->P-1] = leq;
}
}
......@@ -396,31 +402,36 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
{
if((openu & a32[x])) // this condition is open
{
store_matrix[vs->P][t] = les;
if(store_matrix[t][vs->P-1]> les)
store_matrix[t][vs->P-1] = les;
}
else // this condition is closed.
{
store_matrix[vs->P][t] = leq;
if(store_matrix[t][vs->P-1] > leq)
store_matrix[t][vs->P-1] = leq;
}
}
pairWiseTightestRelation(store_matrix,vs->P+1);
CircuitFinder cf(store_matrix,vs->P+1);
if(dis_l == 0)
{
store_matrix[vs->P-2][vs->P-1] = leq;
}
pairWiseTightestRelation(store_matrix,vs->P);
CircuitFinder cf(store_matrix,vs->P);
bool b = cf.run();
if(b)
return false;
else
return true;
}
else if( (transitions[dn].ubs[x]) != INF )
{
delete_r_matrix(store_matrix,vs->P+1); // this one added extra
delete_r_matrix(store_matrix,vs->P); // this one added extra
return false;
}
}
}
//delete_r_matrix(store_matrix,P+1); //this one added extra
delete_r_matrix(store_matrix,P); //this one added extra
return true;
}
......@@ -448,36 +459,67 @@ bool stateGCPP::stackCheck(stateGCPP* vs,short* transitionMap,char dn, char wn,
int openl,openu; //added extra
openl = transitions[dn].openl;
openu = transitions[dn].openu;
relation **store_matrix = allocate_r_matrix(vs->P);
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
short dis = dlr + mod( wn - w[P-1], M ); // mark
char t = vs->L; //the source of push must be L.
if( ( dis < transitions[dn].lbs[0] ) || dis > ub )
{// check if d(source,destination) \in I
delete_r_matrix(store_matrix,vs->P);
return false;
}
//added extra
// 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_<
// }
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
{
return true;
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[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 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);
CircuitFinder cf(store_matrix,vs->P);
bool b = cf.run();
if(b)
return false;
else
return true;
}
else if(ub == INF) // if distance from L to R is big
return true;
delete_r_matrix(store_matrix,vs->P);
return false; // distance is big, but upper bound is not infinity
}
......@@ -583,8 +625,10 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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
/*******************#*****************/
dis = vs->w[vs->P - 2] + mod(wn - w[P-1], M); ///put the change ****
/*******************************************/
if(dis < M) { // reset vs->P-1 bit to 1
rs->f |= (a32[vs->P - 1]);
}
}
......@@ -1188,6 +1232,12 @@ relation ** stateGCPP::allocate_r_matrix()
for(int i = 0; i < P; i++)
r_matrix[i] = new relation[P];
}
relation ** stateGCPP::allocate_r_matrix(relation r)
{
r_matrix = new relation*[P];
for(int i = 0; i < P; i++)
r_matrix[i] = new relation[P]{r};
}
relation** stateGCPP::allocate_r_matrix(char P)
{
relation **matrix = new relation*[P];
......
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