25/10/17:

1. Some special case appearing ..
2. need to see it.

Sparsa Roychowdhury

input1/example

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

input1/example.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,x2:=0}" ];
+	1 -> 2 [ label = "{tn:1,x1:=0}" ];
+	2 -> 3 [ label = "{tn:2,0<=x1<1,x2:=0}" ];
+	3 -> 4 [ label = "{tn:3,0<=x1<1,1<x2<=2}" ];
+}
\ No newline at end of file

input1/example1

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

input1/test1

@@ -13,5 +13,5 @@
 0
 
 2 3 0 1 0
-1 1 0 2 1
+1 1 0 2 0
 0

input1/test1.out

@@ -6,5 +6,5 @@ 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}" ];
+	2 -> 3 [ label = "{tn:3,1<=x1<2}" ];
 }
\ No newline at end of file

input1/test2

-4 4 1 0 1
+4 3 1 0 1
 
 1 
 
@@ -6,11 +6,8 @@
 4
 
 
-1 1 0 0 1
+1 2 0 0 1
 1
-0
-
-1 2 0 0 0 
 1 1
 
 2 3 0 1 0

input1/test2.out

@@ -4,8 +4,7 @@ digraph finite_state_machine {
 	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<=ag(1)<=2}" ];
+	1 -> 2 [ label = "{tn:1,x1:=0,ps_1}" ];
+	2 -> 3 [ label = "{tn:2,2<=x1<=2}" ];
+	3 -> 4 [ label = "{tn:3,pp_1,1<=ag(1)<2}" ];
 }
\ No newline at end of file

src/tpdaCGPP.cpp

@@ -177,7 +177,7 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
             if(storage_matrix[map_p2[i]][map_p2[j]] > s2->r_matrix[i][j])
                 storage_matrix[map_p2[i]][map_p2[j]] = s2->r_matrix[i][j];
         }
-    print_r_matrix(storage_matrix,points_before_reduce);
+    //print_r_matrix(storage_matrix,points_before_reduce);
     pairWiseTightestRelation(storage_matrix,(points_before_reduce));
     
     char map[count];
@@ -292,7 +292,7 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
     
     vs->f = nf; // add the flag variable also
     //vs->P = count; // #points in new state
-    cout << int(count) << "the cound " << endl;
+    //cout << int(count) << "the cound " << endl;
 //    for(char i = 0 ; i < count ; i++)
 //        cout << int(map[i]) << endl;
     
@@ -302,9 +302,11 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
             vs->r_matrix[i][j] = storage_matrix[map[i]][map[j]];
         }
     //print_r_matrix(storage_matrix,points_before_reduce);
-    print_r_matrix(vs->r_matrix,vs->P);
+    //print_r_matrix(r_matrix,P);
+    //print_r_matrix(s2->r_matrix,s2->P);
+    //print_r_matrix(vs->r_matrix,vs->P);
     pairWiseTightestRelation(vs->r_matrix,vs->P);
-    print_r_matrix(vs->r_matrix,vs->P);
+    //print_r_matrix(vs->r_matrix,vs->P);
     delete_r_matrix(storage_matrix,points_before_reduce);
     return vs;
 }
@@ -1812,9 +1814,18 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
 //    cout << "_______________________" << endl;
 //    print_r_matrix(store_matrix,P+1);
 //    }
-    pairWiseTightestRelation(store_matrix,P+1);
     
-//    print_r_matrix(store_matrix,P+1);
+    cout << "dn=" <<int(dn) << " wn=" << int(wn) << endl;
+    for(char i =0; i < P; i++)
+    {
+        cout << int(del[i]) << "\t" ;
+    }
+    cout << int(dn) << endl;
+    cout << "before tightning" << endl;
+    print_r_matrix(store_matrix,P+1);
+    pairWiseTightestRelation(store_matrix,P+1);
+    cout << "after tightning" << endl;
+    print_r_matrix(store_matrix,P+1);
 	
 //    if(dn==4){
 //    
@@ -1838,6 +1849,7 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
     stateGCPP* vs = new stateGCPP();
     
     vs->P = count; // #points in new state
+    //cout << int(count) << endl;
     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 *****************//
@@ -1903,6 +1915,7 @@ stateGCPP* stateGCPP::reduce2(char dn,char wn,short* clockDis,bool* clockAcc,sho
             vs->r_matrix[i][j]=store_matrix[map[i]][map[j]]; //copying r_matrix values 
         }
     }
+    pairWiseTightestRelation(r_matrix,P);
     // we have to set the accuracy for point L to L+1 in new state
     if( lastindex != P ) {
         if( !big(L, lastindex+1) ) {