19/10/17:

1. Atleast  time automata is working

include/tpdaCGPP.h

@@ -32,7 +32,10 @@ class stateGCPP{
         void delete_del();
         void delete_w();
         void delete_all();
-        
+        ~stateGCPP()
+        {
+            delete_all();
+        }
         bool big(char i, char j); // return true iff distance between point i to point j is big
 	
 	short int dist(char i, char j); // return distance between point i to point j
@@ -43,6 +46,8 @@ class stateGCPP{
 	// add transition 'dn' to this state and then forget some points if possible, return the new state, tsm value of last point not decided yet
 	stateGCPP* reduce(char dn);
 	stateGCPP* nextDummy(char dn);
+        stateGCPP* reduce1();
+        
 	// return true iff clock gurards on new transition 'dn' with tsm value 'wn' is satisfied
 	bool consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, bool *clockAcc);
 	

input1/test1

-3 2 1 0 0
+3 3 1 0 0
 
 1
  
 3
 
+1 1 0 0 1
+1 
+0
 
 1 2 0 1 0
 1 2 0 2 0

input1/test1.out

@@ -6,5 +6,4 @@ digraph finite_state_machine {
 	0 -> 1 [ label = "{tn:0,x1:=0}" ];
 	1 -> 1 [ label = "{tn:1,x1:=0}" ];
 	1 -> 2 [ label = "{tn:2,2<=x1<=2}" ];
-	2 -> 3 [ label = "{tn:3,1<=x1<2}" ];
 }
\ No newline at end of file

input1/test2

+4 4 1 0 1
+
+1 
+
+
+4
+
+
+1 1 0 0 1
+1
+0
+
+1 2 0 0 0 
+1 1 
+
+2 3 0 1 0
+1 2 0 2 0
+0 
+
+3 4 0 0 0 
+2 1 1 0 2 0

input1/test2.out

+digraph finite_state_machine {
+	node [shape = point ]; qi0;
+	node [shape = doublecircle];4;
+	node [shape=circle];
+	qi0 -> 0;
+	0 -> 1 [ label = "{tn:0,x1:=0}" ];
+	1 -> 1 [ label = "{tn:1,x1:=0}" ];
+	1 -> 2 [ label = "{tn:2,ps_1}" ];
+	2 -> 3 [ label = "{tn:3,2<=x1<=2}" ];
+	3 -> 4 [ label = "{tn:4,pp_1,1<=x2<=2}" ];
+}
\ No newline at end of file

input1/tp63

@@ -31,4 +31,4 @@
 0
 
 4 4 0 0 0
-2 1 1 1 2 0
+2 1 1 0 2 0

input1/tp63.out

@@ -11,5 +11,5 @@ digraph finite_state_machine {
 	2 -> 3 [ label = "{tn:5,0<=x1<=1}" ];
 	3 -> 4 [ label = "{tn:6}" ];
 	4 -> 2 [ label = "{tn:7,0<=x1<=2}" ];
-	4 -> 4 [ label = "{tn:8,pp_1,1<x2<=2}" ];
+	4 -> 4 [ label = "{tn:8,pp_1,1<=x2<=2}" ];
 }
\ No newline at end of file

src/tpdaCGPP.cpp

@@ -269,7 +269,6 @@ stateGCPP* stateGCPP::shuffle(stateGCPP *s2){ // shuffle  with state s2
 
 
 
-// add transition 'dn' to current state and then forget some points if possible, return the new state
 stateGCPP* stateGCPP::reduce(char dn){
     
     short reset; // variable for reset bit vector
@@ -386,6 +385,124 @@ stateGCPP* stateGCPP::reduce(char dn){
     return vs; // return the partially new state, **** last tsm missing with partial nf as given
 }
 
+// add transition 'dn' to current state and then forget some points if possible, return the new state
+stateGCPP* stateGCPP::reduce1(){
+    
+    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
+    
+    short curReset = transitions[del[P-1]].reset; // set of clocks reset at transition 'dn'
+    
+    for( char i=P-2; i >= L; i-- ) {
+        reset = transitions[ del[i] ].reset; // reset at transition at the (i+1)-th point
+        if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has more reset than found so far at right
+            curReset |= reset; // the 'curReset' will have more bit with value '1'
+            count++; // we have to take (i+1)-th point
+        }
+    }
+    
+    // all the hanging points and point L and point for transition 'dn' also be there 
+    count += (L+1); // number of points in new state
+    
+    // pointer to the new state
+    stateGCPP* vs = new stateGCPP();
+    
+    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
+    //**************ALLOCATING MEMORY FOR THE DYNAMICALLY ALLOCATED VARIABLES *****************//
+    vs->del = new char[vs->P]; // memory allocation for new state transition
+    vs->w = new char[vs->P]; // memory allocation for new state tsm values
+    
+    vs->allocate_r_matrix(que); //allocating memory for the matrix for open guard checking
+    //*************ASSIGNING VALUES TO THE DYNAMICALLY ALLOCATED VARIABLES*****************//
+    for(char i=0; i < L; i++) { // hanging points and left point(L) remain same
+        vs->del[i] = del[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(char i=1; i < L; i++) { // distances between points upto point L remain same
+        nf |= ( f & a32[i] );
+    }
+    
+    //vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
+    
+    char lastindex = P-1; // 'lastindex' used for accuracy between two points in new state
+    //char firstindex;
+    char j = count-2; // assgin trans and tsm from index count-2 upto L
+    short dis; // variable for distance calculation
+    // **** edit last bit of accuracy when u know the tsm of dn
+    curReset = transitions[del[P-1]].reset; // set of clocks reset at transition 'dn'
+    //int vslastindex = vs->P -1; //the last index of the new state vs;
+    for(char i=P-2; i >= L; i--) {
+        reset = transitions[ del[i] ].reset; // reset at i+1-th point
+        
+        if( reset & (~curReset) & (~1) ) {
+            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
+            map[j]=i;
+            if( lastindex != P-1 ) {			
+                if( !big(i+1, lastindex+1) )
+                    nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state
+            }
+            
+            // store the accuracy from last point(active in new state) before dn and P in  i+1-th bit of nf
+            // store the distance from last point(active in new state) before dn and P in vs->w[count-1]
+            // we yet don't know the tsm for 'dn', so full calculation is not done in this function
+            else{ 
+                //firstindex = i;
+                if( !big(i+1, P-1) )
+                    nf |= a32[j+1];
+                vs->w[count-1] = dist(i+1, P-1);
+            }
+            
+            lastindex = i; // this is now the last index
+            j--; // go to previous point
+            //vslastindex--;
+        }
+    }
+    map[count-1] = P-1;
+    //pairWiseTightestRelation(r_matrix,P);
+    for(char i = 0; i < vs->P; i++)// this code may change, later.
+    {
+        for(char j = 0 ; j< vs->P; 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
+    if( lastindex != P-1 ) {
+        if( !big(L, lastindex+1) ) {
+            //	vs->w[count-1] = dist(L, lastindex+1) ;
+            nf |= a32[L]; // set the accuracy for (j+1)-th bit of new state
+        }
+    }
+    
+    // store the accuracy from last point(active in new state) before dn and P in  i+1-th bit of nf
+    // store the distance from last point(active in new state) before dn and P in vs->w[count-1]
+    // we yet don't know the tsm for 'dn', so full calculation is not done in this function
+    else{  // if you have not choosed any point in the middle starting from point P**
+        if( !big(L, P-1) )
+            nf |= a32[L];
+        vs->w[count-1] = dist(L, P-1);
+    }
+    
+    if(isPop(del[P-1]) ) // if dn has a pop, then push-pop has been added to L and R repectively
+        nf |= (1 | a3215) ;
+    else
+        nf |= (f & 1) ; // previous push information remain same
+    
+    // last distance accuracy
+    vs->f = nf; // add partial flag variable to new state
+    print_r_matrix(vs->r_matrix,vs->P);
+    return vs; // return the partially new state, **** last tsm missing with partial nf as given
+}
+
 
 // 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) {
@@ -644,7 +761,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* vs = reduce(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)
             
             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]
@@ -675,13 +792,15 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
                 
                 //is it checking after adding the point to the state returned by reduce?
                 // if clock constraint not satisfied
-                if( !consSatisfied( vs,dn, wn, clockDis, clockAcc)  ) {  }
+                if( !consSatisfied( vs1,dn, wn, clockDis, clockAcc)  ) {  }
                 
                 // 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( ( popflag && ( !stackCheck(vs1,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* rs = new stateGCPP();
                     
                     rs->L = L; // left point remain same
@@ -735,6 +854,32 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
 stateGCPP* stateGCPP::nextDummy(char dn){
     //this function adds the new transition without removing any points.
     //then check if the returned thing works or not.
+    short nf =f;
+    stateGCPP* vs = new stateGCPP();
+    vs->P = P+1; // adding extra point.
+    vs->L = L;
+    vs->del = new char[vs->P];
+    vs->w = new char[vs->P];
+    vs->allocate_r_matrix(que);
+    for(char i = 0 ; i < vs->P-1 ; i++)
+    {
+        vs->del[i] = del[i];
+        vs->w[i] = w[i];
+        for(char j = 0; j < vs->P-1; j++)
+        {
+            vs->r_matrix[i][j] = r_matrix[i][j];
+        }
+    }
+    vs->del[vs->P-1] = dn;
+    if( !big(P-1, P-1) )
+        nf |= a32[vs->P -1];
+    vs->w[vs->P-1] = dist(P-1, P-1);
+    if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively
+        nf |= (1 | a3215) ;
+    else
+        nf |= (f & 1) ; // previous push information remain same
+    vs->f = nf;
+    return vs;
 }
 // Return template successor state whose descendent states will be right states for shuffle operation with this state
 stateGCPP* stateGCPP::sucState(){