Commit 781e10c7 authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY

22/9/17:

1. Revised the file reading for openness 
2. Changed the reduce(dn) function to incorporate the change of open guards.\
3. Started changing the addnextpoint function, it is not done yet. Need some logic to do.
parent 3a3fc041
...@@ -19,7 +19,7 @@ public: ...@@ -19,7 +19,7 @@ public:
int openl; // i-th bit openl is 1 iff lower bound of constraint for clock i is open int openl; // i-th bit openl is 1 iff lower bound of constraint for clock i is open
int openu; // i-th bit openr is 1 iff upper bound of constraint for clock i is open int openu; // i-th bit openr is 1 iff upper bound of constraint for clock i is open
/* /*
0-th bit of gurad and reset is for stack operation 0-th bit of gurad, reset,openl and openu is for stack operation
1 to 15-th bits are for clock(15 clock supported) 1 to 15-th bits are for clock(15 clock supported)
g_i=1(1<=i<=15) : i-th clock is checked in this transition g_i=1(1<=i<=15) : i-th clock is checked in this transition
......
...@@ -24,6 +24,11 @@ class stateGCPP{ ...@@ -24,6 +24,11 @@ class stateGCPP{
char L; // left point of the non-trivial block char L; // left point of the non-trivial block
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();
void delete_r_matrix();
void delete_del();
void delete_w();
void delete_all();
bool big(char i, char j); // return true iff distance between point i to point j is big bool big(char i, char j); // return true iff distance between point i to point j is big
......
...@@ -113,6 +113,7 @@ void inputSystem() { ...@@ -113,6 +113,7 @@ void inputSystem() {
int x; // temporary variable int x; // temporary variable
int i, j; // loopers int i, j; // loopers
int lb, ub; // used as lower and upper bound int lb, ub; // used as lower and upper bound
//int openl, openu;
int noofguards, noofresets; // #gurads and #reset clocks in a transition int noofguards, noofresets; // #gurads and #reset clocks in a transition
int guard, reset; int guard, reset;
...@@ -151,7 +152,8 @@ void inputSystem() { ...@@ -151,7 +152,8 @@ void inputSystem() {
transitions[0].lbs = new int[X+1]; // allocate memory for lower bounds for clock's check and stack pop operation transitions[0].lbs = new int[X+1]; // allocate memory for lower bounds for clock's check and stack pop operation
transitions[0].ubs = new int[X+1]; // allocate memory for upper bounds for clock's check and stack pop operation transitions[0].ubs = new int[X+1]; // allocate memory for upper bounds for clock's check and stack pop operation
transitions[0].guard = 0; // 0-th bits of gurad and reset are '0' / no stack operation transitions[0].guard = 0; // 0-th bits of gurad and reset are '0' / no stack operation
transitions[0].openl =0;
transitions[0].openu = 0;
// Reset all clocks at 0-th transition // Reset all clocks at 0-th transition
transitions[0].reset = ( b32[X] & (~1) ); transitions[0].reset = ( b32[X] & (~1) );
...@@ -182,6 +184,9 @@ void inputSystem() { ...@@ -182,6 +184,9 @@ void inputSystem() {
transitions[i].ubs = new int[X+1]; // allocate memory for upper bounds for clock's check and stack pop operation transitions[i].ubs = new int[X+1]; // allocate memory for upper bounds for clock's check and stack pop operation
guard = 0; guard = 0;
int opnl,opnu;
int openl=0;
int openu = 0;
for(j=0; j < noofguards; j++) { for(j=0; j < noofguards; j++) {
tiimeinfile >> x; // clock number for guard tiimeinfile >> x; // clock number for guard
...@@ -192,7 +197,21 @@ void inputSystem() { ...@@ -192,7 +197,21 @@ void inputSystem() {
} }
guard |= a32[x]; // set i-th bit of guard to '1' guard |= a32[x]; // set i-th bit of guard to '1'
tiimeinfile >> lb >> ub; // bounds on the guard tiimeinfile >> lb;
tiimeinfile >> opnl;
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
if(opnl == 1)
{
openl |= a32[x]; //if left value is open then the xth bit of the open is 1
}
if(opnu == 1)
openu |= a32[x]; // similar as above
if(lb < 0 || ub < (-1)) { if(lb < 0 || ub < (-1)) {
cout << "Bounds can't be negative!" << endl; cout << "Bounds can't be negative!" << endl;
...@@ -231,7 +250,7 @@ void inputSystem() { ...@@ -231,7 +250,7 @@ void inputSystem() {
// read stack operation number, 0 : nop, 1 : push, 2 : pop, 3 : pop & push // read stack operation number, 0 : nop, 1 : push, 2 : pop, 3 : pop & push
tiimeinfile >> x; tiimeinfile >> x;
//openl = openu = 0;
if(x == 0) { // nop operation if(x == 0) { // nop operation
// do nothing // do nothing
} }
...@@ -251,7 +270,21 @@ void inputSystem() { ...@@ -251,7 +270,21 @@ void inputSystem() {
transitions[i].as = x; transitions[i].as = x;
transitions[i].pp = x; transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds tiimeinfile >> lb;
tiimeinfile >> opnl;
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
if(opnl == 1)
{
openl |= 1; //setting 0th bit of the openl to 1
}
if(opnu == 1)
openu |= 1; // similar as above
M = max(lb,M); // update M if M < lb M = max(lb,M); // update M if M < lb
transitions[i].lbs[0] = lb; // lower bound for clock x transitions[i].lbs[0] = lb; // lower bound for clock x
...@@ -281,7 +314,21 @@ void inputSystem() { ...@@ -281,7 +314,21 @@ void inputSystem() {
tiimeinfile >> x; // stack pop symbol tiimeinfile >> x; // stack pop symbol
transitions[i].pp = x; transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds tiimeinfile >> lb;
tiimeinfile >> opnl;
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
if(opnl == 1)
{
openl |= 1; //if left value is open then the xth bit of the open is 1
}
if(opnu == 1)
openu |= 1; // similar as above
M = max(lb,M); // update M if M < lb M = max(lb,M); // update M if M < lb
transitions[i].lbs[0] = lb; // lower bound for clock x transitions[i].lbs[0] = lb; // lower bound for clock x
...@@ -312,7 +359,8 @@ void inputSystem() { ...@@ -312,7 +359,8 @@ void inputSystem() {
transitions[i].guard = guard; transitions[i].guard = guard;
transitions[i].reset = reset; transitions[i].reset = reset;
transitions[i].openl = openl;
transitions[i].openu = openu;
// resetting and checking in which transitions for each clock // resetting and checking in which transitions for each clock
for(j=1; j <= X; j++) { // forget this for(j=1; j <= X; j++) { // forget this
if(guard & a32[j]) // if j-th clock has been checked at i-th transitions if(guard & a32[j]) // if j-th clock has been checked at i-th transitions
......
...@@ -259,14 +259,20 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -259,14 +259,20 @@ stateGCPP* stateGCPP::reduce(char dn){
stateGCPP* vs = new stateGCPP(); stateGCPP* vs = new stateGCPP();
vs->P = count; // #points in new state 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 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->del = new char[count]; // memory allocation for new state transition
vs->w = new char[count]; // memory allocation for new state tsm values 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
//*************ASSIGNING VALUES TO THE DYNAMICALLY ALLOCATED VARIABLES*****************//
for(i=0; i < L; i++) { // hanging points and left point(L) remain same for(i=0; i < L; i++) { // hanging points and left point(L) remain same
vs->del[i] = del[i]; vs->del[i] = del[i];
vs->w[i] = w[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(i=1; i < L; i++) { // distances between points upto point L remain same for(i=1; i < L; i++) { // distances between points upto point L remain same
...@@ -281,13 +287,14 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -281,13 +287,14 @@ stateGCPP* stateGCPP::reduce(char dn){
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
curReset = transitions[dn].reset; // set of clocks reset at transition '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(i=P-1; i >= L; i--) { for(i=P-1; i >= L; i--) {
reset = transitions[ del[i] ].reset; // reset at i+1-th point reset = transitions[ del[i] ].reset; // reset at i+1-th point
if( reset & (~curReset) & (~1) ) { if( reset & (~curReset) & (~1) ) {
vs->del[j] = del[i]; // i-th index trans will be part of new state at j-th index 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 vs->w[j] = w[i]; // i-th index tsm will be part of new state at j-th index
map[vslastindex]=i;
if( lastindex != P ) { if( lastindex != P ) {
if( !big(i+1, lastindex+1) ) if( !big(i+1, lastindex+1) )
nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state
...@@ -305,9 +312,16 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -305,9 +312,16 @@ stateGCPP* stateGCPP::reduce(char dn){
lastindex = i; // this is now the last index lastindex = i; // this is now the last index
j--; // go to previous point j--; // go to previous point
vslastindex--;
}
}
for(int i = 0; i < vs->P-1; i++)// this code may change, later.
{
for(int j = 0 ; j< vs->P-1; j++)
{
vs->r_matrix[i][j]=r_matrix[map[i]][map[j]]; //copying r_matrix values
} }
} }
// we have to set the accuracy for point L to L+1 in new state // we have to set the accuracy for point L to L+1 in new state
if( lastindex != P ) { if( lastindex != P ) {
if( !big(L, lastindex+1) ) { if( !big(L, lastindex+1) ) {
...@@ -422,7 +436,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -422,7 +436,7 @@ 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
stateGCPP* vs = reduce(dn); // get partial new state after adding transition 'dn'(TSM for 'dn' not known yet) stateGCPP* vs = reduce(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]
...@@ -478,6 +492,11 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -478,6 +492,11 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
rs->f |= (a32[vs->P - 1]); 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?
//How to propagate values??
//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
} }
...@@ -698,11 +717,7 @@ stateGCPP* getZeroState() { ...@@ -698,11 +717,7 @@ stateGCPP* getZeroState() {
vs->L = 1; // only one point is there vs->L = 1; // only one point is there
vs->P = 1; vs->P = 1;
vs->f = 0; // no push pop info yet, no accuracy info yet vs->f = 0; // no push pop info yet, no accuracy info yet
vs->r_matrix = new relation*[vs->P]; //starting the first matrix for the open vs->r_matrix = vs->allocate_r_matrix();
for(int i = 0;i < vs->P;i++) // guard checking, the first point cant have any
{
vs->r_matrix[i] = new relation[vs->P]; // information so we will assign it
}
for(int i =0 ; i < vs->P;i++) // with 'na'. for(int i =0 ; i < vs->P;i++) // with 'na'.
for(int j = 0; j < vs->P; j++) for(int j = 0; j < vs->P; j++)
vs->r_matrix[i][j] = na; vs->r_matrix[i][j] = na;
...@@ -1038,7 +1053,34 @@ bool isEmptyGCPP() { ...@@ -1038,7 +1053,34 @@ bool isEmptyGCPP() {
return true; return true;
} }
void stateGCPP::delete_all()
{
delete_r_matrix();
delete_w();
delete_del();
}
void stateGCPP::delete_r_matrix()
{
for(int i = 0; i < P; i++)
delete [] r_matrix[i];
delete [] r_matrix;
}
void stateGCPP::delete_del()
{
delete [] del;
}
void stateGCPP::delete_w()
{
delete [] w;
}
relation ** stateGCPP::allocate_r_matrix()
{
r_matrix = new relation*[P];
for(int i = 0; i < P; i++)
r_matrix[i] = new relation[P];
}
\ No newline at end of file
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