Commit a3aedafb authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY

10/10/17:

1. removed template from the circuit finder
2. combined the program, logic is up
3. testing remains 
4. have to write the shuffle function
parent 7a997dbf
...@@ -25,7 +25,7 @@ typedef list<int> NodeList; ...@@ -25,7 +25,7 @@ typedef list<int> NodeList;
//void pairWiseTightestRelation (relation **graph, int V); //for tightening the matrix //void pairWiseTightestRelation (relation **graph, int V); //for tightening the matrix
typedef struct{bool A; bool B;} bool2; typedef struct{bool A; bool B;} bool2;
void pairWiseTightestRelation (relation **graph, int V); //for tightening the matrix void pairWiseTightestRelation (relation **graph, int V); //for tightening the matrix
template<int N>
class CircuitFinder // defining a circuit finder class class CircuitFinder // defining a circuit finder class
{ {
vector<NodeList> AK; //this is the matrix representaion using node list vector<NodeList> AK; //this is the matrix representaion using node list
...@@ -33,24 +33,15 @@ class CircuitFinder // defining a circuit finder class ...@@ -33,24 +33,15 @@ class CircuitFinder // defining a circuit finder class
vector<bool> Blocked; // a boolean array to indicate which nodes are blocked and which are not vector<bool> Blocked; // a boolean array to indicate which nodes are blocked and which are not
vector<NodeList> B; // special node. vector<NodeList> B; // special node.
int S; int S;
int N;
void unblock(int U); //function to unblock the vertix U void unblock(int U); //function to unblock the vertix U
bool2 circuit(int V); // function to check if there is a circuit from note V bool2 circuit(int V); // function to check if there is a circuit from note V
bool cycleCheck(); //function to output the list of circuits in the graph bool cycleCheck(); //function to output the list of circuits in the graph
relation **relmatrix; relation **relmatrix;
public: public:
CircuitFinder(int Array[N][N]) //convert associate matrix representation to list representation of grph CircuitFinder(relation **matrix,int N) :AK(N), Blocked(N), B(N)
: AK(N), Blocked(N), B(N) {
for (int I = 0; I < N; ++I) {
for (int J = 0; J < N; ++J) {
if (Array[I][J]) {
AK[I].push_back(Array[I][J]);
}
}
}
}
CircuitFinder(relation **matrix) :AK(N), Blocked(N), B(N)
{ {
this->N = N;
relmatrix = new relation*[N]; relmatrix = new relation*[N];
for(int i = 0; i < N; i++) for(int i = 0; i < N; i++)
relmatrix[i] = new relation[N]; relmatrix[i] = new relation[N];
...@@ -76,106 +67,7 @@ public: ...@@ -76,106 +67,7 @@ public:
bool run(); //start the run bool run(); //start the run
}; };
template<int N>
void CircuitFinder<N>::unblock(int U)
{
Blocked[U - 1] = false;
while (!B[U - 1].empty()) {
int W = B[U - 1].front();
B[U - 1].pop_front();
if (Blocked[W - 1]) {
unblock(W);
}
}
}
template<int N>
bool2 CircuitFinder<N>::circuit(int V)
{
bool2 F;
F.A= false;
F.B = false;
Stack.push_back(V);
Blocked[V - 1] = true;
//bool check;
for (int W : AK[V - 1]) {
if (W == S) {
F.B = cycleCheck();
F.A = true;
} else if (W > S && !Blocked[W - 1]) {
F = circuit(W);
}
}
if (F.A) {
unblock(V);
} else {
for (int W : AK[V - 1]) {
auto IT = std::find(B[W - 1].begin(), B[W - 1].end(), V);
if (IT == B[W - 1].end()) {
B[W - 1].push_back(V);
}
}
}
Stack.pop_back();
return F;
}
template<int N>
bool CircuitFinder<N>::cycleCheck() //here we need to check if there exists any cycle
{ // with <+<=* regex. return 1 if there is a cycle and return 0 if not.
//cout << "circuit: "<<endl;
int countles=0;
for (auto I = Stack.begin(), E = Stack.end(); I != E; ++I) {
//checking of if the cycle have a < along with other <=
// cout << *I << " -> ";
if(I+1 != E)
{
if(relmatrix[*I][*(I+1)] != leq || relmatrix[*I][*(I+1)] != les)
{
return false;
}
else if(relmatrix[*I][*(I+1)] == les)
countles++;
}
else
{
if(relmatrix[*I][*Stack.begin()] != leq || relmatrix[*I][*Stack.begin()] != les)
return false;
else if (relmatrix[*I][*Stack.begin()] == les)
countles ++;
}
if( countles == 1)
return true;
else
return false;
}
// cout << *Stack.begin() << std::endl;
}
template<int N>
bool CircuitFinder<N>::run()
{
Stack.clear();
S = 1;
bool2 returnval;
while (S < N) {
for (int I = S; I <= N; ++I) {
Blocked[I - 1] = false;
B[I - 1].clear();
}
returnval= circuit(S);
if(returnval.B == true)
return true;
++S;
}
return false;
}
#endif /* CIRCUITFINDER_H */ #endif /* CIRCUITFINDER_H */
......
...@@ -43,10 +43,10 @@ class stateGCPP{ ...@@ -43,10 +43,10 @@ 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, relation r, short *clockDis, bool *clockAcc); bool consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char wn, 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,relation r, short dlr, bool aclr); bool stackCheck(stateGCPP* vs,short* transitionMap,char dn, char wn, short dlr, bool aclr);
//check if the relation between the fractional parts are good or not. //check if the relation between the fractional parts are good or not.
bool relationSatisfied(char dn,char wn,relation r,short *clockDis,bool *clockAcc); 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
......
...@@ -7,12 +7,13 @@ EXE := tree ...@@ -7,12 +7,13 @@ EXE := tree
GDB := -g GDB := -g
tree : main.o $(OBJ)/treeBitOperations.o $(OBJ)/timePushDown.o $(OBJ)/continuoustpda.o $(OBJ)/pds.o $(OBJ)/tpdaCGPP.o $(OBJ)/tpdaZone.o $(OBJ)/tpda2.o drawsystem tree : main.o $(OBJ)/treeBitOperations.o $(OBJ)/timePushDown.o $(OBJ)/continuoustpda.o $(OBJ)/pds.o $(OBJ)/tpdaCGPP.o $(OBJ)/tpdaZone.o $(OBJ)/tpda2.o $(OBJ)/circuitfinder.o drawsystem
g++ $(GDB) main.o $(OBJ)/treeBitOperations.o $(OBJ)/timePushDown.o $(OBJ)/continuoustpda.o $(OBJ)/pds.o $(OBJ)/tpdaCGPP.o $(OBJ)/tpdaZone.o $(OBJ)/tpda2.o -o $(EXE) $(CFLAG) g++ $(GDB) main.o $(OBJ)/treeBitOperations.o $(OBJ)/timePushDown.o $(OBJ)/continuoustpda.o $(OBJ)/pds.o $(OBJ)/tpdaCGPP.o $(OBJ)/tpdaZone.o $(OBJ)/tpda2.o $(OBJ)/circuitfinder.o -o $(EXE) $(CFLAG)
main.o : main.cpp main.o : main.cpp
g++ $(GDB) -I $(INC) -c main.cpp -o main.o $(CFLAG) g++ $(GDB) -I $(INC) -c main.cpp -o main.o $(CFLAG)
$(OBJ)/circuitfinder.o : $(SRC)/circuitfinder.cpp
g++ $(GDB) -I $(INC) -c $(SRC)/circuitfinder.cpp -o $(OBJ)/circuitfinder.o $(CFLAG)
$(OBJ)/tpdaZone.o : $(SRC)/tpdaZone.cpp $(OBJ)/tpdaZone.o : $(SRC)/tpdaZone.cpp
g++ $(GDB) -I $(INC) -c $(SRC)/tpdaZone.cpp -o $(OBJ)/tpdaZone.o $(CFLAG) g++ $(GDB) -I $(INC) -c $(SRC)/tpdaZone.cpp -o $(OBJ)/tpdaZone.o $(CFLAG)
......
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
<in>circuitfinder.h</in> <in>circuitfinder.h</in>
</df> </df>
<df name="src"> <df name="src">
<in>allpairshortest.cpp</in> <in>circuitfinder.cpp</in>
<in>continuoustpda.cpp</in> <in>continuoustpda.cpp</in>
<in>drawsystem.cpp</in> <in>drawsystem.cpp</in>
<in>pds.cpp</in> <in>pds.cpp</in>
...@@ -73,7 +73,7 @@ ...@@ -73,7 +73,7 @@
<ccTool flags="0"> <ccTool flags="0">
</ccTool> </ccTool>
</item> </item>
<item path="src/allpairshortest.cpp" ex="false" tool="1" flavor2="0"> <item path="src/circuitfinder.cpp" ex="false" tool="1" flavor2="0">
</item> </item>
<item path="src/continuoustpda.cpp" ex="false" tool="1" flavor2="8"> <item path="src/continuoustpda.cpp" ex="false" tool="1" flavor2="8">
<ccTool flags="0"> <ccTool flags="0">
......
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
<df name="output"> <df name="output">
</df> </df>
<df name="src"> <df name="src">
<in>allpairshortest.cpp</in> <in>circuitfinder.cpp</in>
<in>continuoustpda.cpp</in> <in>continuoustpda.cpp</in>
<in>drawsystem.cpp</in> <in>drawsystem.cpp</in>
<in>pds.cpp</in> <in>pds.cpp</in>
......
/*
* To change this license header, choose License Headers in Project Properties.
* To change this template file, choose Tools | Templates
* and open the template in the editor.
*/
// C Program for Floyd Warshall Algorithm
#include<iostream>
using namespace std;
typedef enum {z,les,leq,que,na} relation;
// Number of vertices in the graph
//#define V 4
relation addition[4][4] = {{les,les,que,les},{les,leq,que,leq},{que,que,que,que},{les,leq,que,na}};
string sarr[4] = {"<","<=","?","NA"};
/* Define Infinite as a large enough value. This value will be used
for vertices not connected to each other */
//#define INF na
// A function to print the solution matrix
void printSolution(relation dist[][], int V);
// Solves the all-pairs shortest path problem using Floyd Warshall algorithm
void floydWarshall (relation graph[][], int V)
{
/* dist[][] will be the output matrix that will finally have the shortest
distances between every pair of vertices */
relation dist[V][V];
int i, j, k;
/* Initialize the solution matrix same as input graph matrix. Or
we can say the initial values of shortest distances are based
on shortest paths considering no intermediate vertex. */
for (i = 0; i < V; i++)
for (j = 0; j < V; j++)
dist[i][j] = graph[i][j];
/* Add all vertices one by one to the set of intermediate vertices.
---> Before start of a iteration, we have shortest distances between all
pairs of vertices such that the shortest distances consider only the
vertices in set {0, 1, 2, .. k-1} as intermediate vertices.
----> After the end of a iteration, vertex no. k is added to the set of
intermediate vertices and the set becomes {0, 1, 2, .. k} */
for (k = 0; k < V; k++)
{
// Pick all vertices as source one by one
for (i = 0; i < V; i++)
{
// Pick all vertices as destination for the
// above picked source
for (j = 0; j < V; j++)
{
// If vertex k is on the shortest path from
// i to j, then update the value of dist[i][j]
relation m = addition[dist[i][k]][dist[k][j]];
if (m < dist[i][j])
dist[i][j] = m;
}
}
}
// Print the shortest distance matrix
printSolution(dist);
}
/* A utility function to print solution */
void printSolution(relation dist[][],int V)
{
cout << "Following matrix shows the shortest distances" <<
" between every pair of vertices" << endl;
cout.width(7);
for (int i = 0; i < V; i++)
{
for (int j = 0; j < V; j++)
{
cout << sarr[dist[i][j]];
}
cout << endl;
}
}
// driver program to test above function
int main()
{
/* Let us create the following weighted graph
10
(0)------->(3)
| /|\
5 | |
| | 1
\|/ |
(1)------->(2)
3 */
relation graph[V][V] = { {z,que,les,na},
{na,z,na,leq},
{na,les,z,na},
{leq,na,na,z}
};
// Print the solution
floydWarshall(graph);
return 0;
}
/*
* To change this license header, choose License Headers in Project Properties.
* To change this template file, choose Tools | Templates
* and open the template in the editor.
*/
#include "circuitfinder.h"
void CircuitFinder::unblock(int U)
{
Blocked[U - 1] = false;
while (!B[U - 1].empty()) {
int W = B[U - 1].front();
B[U - 1].pop_front();
if (Blocked[W - 1]) {
unblock(W);
}
}
}
bool2 CircuitFinder::circuit(int V)
{
bool2 F;
F.A= false;
F.B = false;
Stack.push_back(V);
Blocked[V - 1] = true;
//bool check;
for (int W : AK[V - 1]) {
if (W == S) {
F.B = cycleCheck();
F.A = true;
if(F.B)
return F;
} else if (W > S && !Blocked[W - 1]) {
F = circuit(W);
}
}
if (F.A) {
unblock(V);
} else {
for (int W : AK[V - 1]) {
auto IT = std::find(B[W - 1].begin(), B[W - 1].end(), V);
if (IT == B[W - 1].end()) {
B[W - 1].push_back(V);
}
}
}
Stack.pop_back();
return F;
}
bool CircuitFinder::cycleCheck() //here we need to check if there exists any cycle
{ // with <+<=* regex. return 1 if there is a cycle and return 0 if not.
cout << "circuit: ";
int countles=0;
for (auto I = Stack.begin(), E = Stack.end(); I != E; ++I) {
//checking of if the cycle have a < along with other <=
cout << *I << " -> ";
if(I+1 != E)
{
if(relmatrix[(*I)-1][(*(I+1))-1] != leq && relmatrix[(*I)-1][(*(I+1))-1] != les)
{
return false;
}
else if(relmatrix[(*I)-1][(*(I+1))-1] == les)
countles++;
}
else
{
if(relmatrix[(*I)-1][(*Stack.begin())-1] != leq && relmatrix[(*I)-1][(*Stack.begin())-1] != les)
{
return false;
}
else if (relmatrix[(*I)-1][(*Stack.begin())-1] == les)
countles ++;
}
if( countles == 1)
return true;
else
return false;
}
cout << *Stack.begin() << std::endl;
}
bool CircuitFinder::run()
{
Stack.clear();
S = 1;
bool2 returnval;
while (S < N) {
for (int I = S; I <= N; ++I) {
Blocked[I - 1] = false;
B[I - 1].clear();
}
returnval= circuit(S);
if(returnval.B == true)
return true;
++S;
}
return false;
}
...@@ -142,10 +142,10 @@ void inputSystem() { ...@@ -142,10 +142,10 @@ void inputSystem() {
{ {
clock_reset[i] = 0; // the first reset points of every clocks is 0th transition. clock_reset[i] = 0; // the first reset points of every clocks is 0th transition.
} }
recent_matrix = new char*[T+1]; recent_matrix = new char*[T+1]; //allocate rows to the matrix which is the total number of transitions.
for(int i = 0; i < T+1 ; i++) for(int i = 0; i < T+1 ; i++)
{ {
recent_matrix[i] = new char[X]; recent_matrix[i] = new char[X]; //for every row we have columns with the number of clocks
} }
for(int i = 0; i <X; i++) for(int i = 0; i <X; i++)
...@@ -262,7 +262,7 @@ void inputSystem() { ...@@ -262,7 +262,7 @@ void inputSystem() {
exit(1); exit(1);
} }
reset |= a32[x]; // set x-th bit of 'reset' to '1' reset |= a32[x]; // set x-th bit of 'reset' to '1'
clock_reset[x] = i; clock_reset[x] = i; // the latest transition which resets the clocks x is i.
} }
// 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
......
...@@ -273,8 +273,8 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -273,8 +273,8 @@ stateGCPP* stateGCPP::reduce(char dn){
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 map[i] = i; //copying the map upto L-1
// for(int j = 0; j< L; j++) // for(int j = 0; j< L; j++)
// vs->r_matrix[i][j] = r_matrix[i][j]; // copying the matrix value for the hanging points // 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
...@@ -354,17 +354,17 @@ stateGCPP* stateGCPP::reduce(char dn){ ...@@ -354,17 +354,17 @@ 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,relation r, short *clockDis, bool *clockAcc) { bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char wn, short *clockDis, bool *clockAcc) {
short dis; short dis;
int openl,openu; int openl,openu;
openl = transitions[dn].openl; openl = transitions[dn].openl;
openu = transitions[dn].openu; openu = transitions[dn].openu;
relation **store_matrix = allocate_r_matrix(P+1); relation **store_matrix = allocate_r_matrix(vs->P+1);
for(int i = 0 ;i < P; i++) for(int i = 0 ;i < vs->P; i++)
{ {
for(int j = 0; j < P; j++) for(int j = 0; j < vs->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. 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.
} }
} }
for(char x=1; x <= X; x++) { for(char x=1; x <= X; x++) {
...@@ -372,33 +372,55 @@ bool stateGCPP::consSatisfied(char dn, char wn,relation r, short *clockDis, bool ...@@ -372,33 +372,55 @@ bool stateGCPP::consSatisfied(char dn, char wn,relation r, short *clockDis, bool
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 ) ;
char t = transitionMap[recent_matrix[dn][x]];
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 {//if the distance doesnot belong to the interval
delete_r_matrix(store_matrix,P+1); delete_r_matrix(store_matrix,vs->P+1); // this one added extra
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. if( dis == transitions[dn].lbs[x]) //checking if the distance is equal to the upper value and the constraint is open.
{
if((openl & a32[x])) //this condition 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)} store_matrix[t][vs->P]= les;
// hence (i,j) \in R_<
} }
else if(dis == transitions[dn].ubs[x] && (openu & a32[x])) else //this condition is closed
{ {
//here we have to check the relationship of the fractional parts of the source and target store_matrix[t][vs->P] = leq;
//Here the relation must be {tsm(j) } < {tsm(i)}
// Hence (j,i) \in R_<
} }
}
if(dis == transitions[dn].ubs[x])
{
if((openu & a32[x])) // this condition is open
{
store_matrix[vs->P][t] = les;
}
else // this condition is closed.
{
store_matrix[vs->P][t] = leq;
}
}
pairWiseTightestRelation(store_matrix,vs->P+1);
CircuitFinder cf(store_matrix,vs->P+1);
bool b = cf.run();
if(b)
return false;
else
return true;
} }
else if( (transitions[dn].ubs[x]) != INF ) else if( (transitions[dn].ubs[x]) != INF )
{ {
delete_r_matrix(store_matrix,P+1); delete_r_matrix(store_matrix,vs->P+1); // this one added extra
return false; return false;
} }
} }
} }
delete_r_matrix(store_matrix,P+1); //delete_r_matrix(store_matrix,P+1); //this one added extra
return true; return true;
} }
...@@ -421,9 +443,9 @@ bool stateGCPP::consSatisfied(char dn, char wn,relation r, short *clockDis, bool ...@@ -421,9 +443,9 @@ bool stateGCPP::consSatisfied(char dn, char wn,relation r, short *clockDis, bool
// 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,relation r, short dlr, bool aclr) { bool stateGCPP::stackCheck(stateGCPP* vs,short* transitionMap,char dn, char wn, 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; int openl,openu; //added extra
openl = transitions[dn].openl; openl = transitions[dn].openl;
openu = transitions[dn].openu; openu = transitions[dn].openu;
if(aclr) { // if distance from L to R is small if(aclr) { // if distance from L to R is small
...@@ -433,18 +455,19 @@ bool stateGCPP::stackCheck(char dn, char wn,relation r, short dlr, bool aclr) { ...@@ -433,18 +455,19 @@ bool stateGCPP::stackCheck(char dn, char wn,relation r, short dlr, bool aclr) {
{// check if d(source,destination) \in I {// 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 //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)} // //Here have to check the relationship of the fractional parts of the source and target
// hence (i,j) \in R_< // // 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 // }
{ // 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)} // //here we have to check the relationship of the fractional parts of the source and target
// Hence (j,i) \in R_< // //Here the relation must be {tsm(j) } < {tsm(i)}
} // // Hence (j,i) \in R_<
// }
else else
{ {
return true; return true;
...@@ -509,7 +532,9 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -509,7 +532,9 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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]
bool *clockAcc = new bool[X + 1]; // accuracy from last reset of clock x to point P, stored in clockAcc[x] bool *clockAcc = new bool[X + 1]; // accuracy from last reset of clock x to point P, stored in clockAcc[x]
short *transitionMap = new short[T+1]{-1}; //for a given state and a given transition, which colored point the transition maps into is given by this vector
for(int q = 0 ; q < vs->P; q++)
transitionMap[vs->del[q]] = q; //this gives transitions to clolore point ka map.
for(char x=1; x <= X; x++) { // calculate the distances and accuracy from last reset point to point P for each clock for(char x=1; x <= X; x++) { // calculate the distances and accuracy from last reset point to point P for each clock
for(j=P-1; j >= 0; j--) { for(j=P-1; j >= 0; j--) {
...@@ -528,17 +553,17 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -528,17 +553,17 @@ 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}; //relation rel[2] = {leq,les};
for(wn=0; wn < M; wn++) { for(wn=0; wn < M; wn++) {
for(int i = 0; i < 2;i++)
{ //is it checking after adding the point to the state returned by reduce?
// if clock constraint not satisfied // if clock constraint not satisfied
if( !consSatisfied( dn, wn, rel[i], clockDis, clockAcc) ) { } if( !consSatisfied( vs,transitionMap,dn, wn, clockDis, clockAcc) ) { }
// if stack constraint not satisfied // 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( ( popflag && ( !stackCheck(vs,transitionMap,dn, wn, dlr, aclr) ) ) ) { } //if there is a pop and the constraint on pop is satisfied.
//else if(!relationSatisfied(dn,wn)) //else if(!relationSatisfied(dn,wn))
//else if (( !openGuardConsSat()))
else { // if clock and stack both constraints are satisfied else { // if clock and stack both constraints are satisfied
stateGCPP* rs = new stateGCPP(); stateGCPP* rs = new stateGCPP();
...@@ -572,7 +597,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -572,7 +597,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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
} }
} delete[] clockDis,clockAcc,transitionMap; //removing after finishing with it
} }
} }
} }
......
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