Skip to content

M
mtp
You need to sign in or sign up before continuing.
Commit e4eea6fc authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY
Browse files
Options

12/7/2017: 

1. Some change done in the reduce shuffle function
2. Completely Indented code.
parent 8a8fb4bc
Hide whitespace changes
Inline Side-by-side
Showing with 2453 additions and 2406 deletions
include/timePushDown.h
View file @ e4eea6fc
...@@ -2,48 +2,48 @@ ...@@ -2,48 +2,48 @@
using namespace std; using namespace std;
class transition{ class transition{
public: public:
short source; // source state short source; // source state
short target; // target state short target; // target state
char a; // action in this transition char a; // action in this transition
char as; // stack symbol in this transition, **** this variable is obsolete in new version of code char as; // stack symbol in this transition, **** this variable is obsolete in new version of code
char ps; // push symbol in this transition char ps; // push symbol in this transition
char pp; // pop symbol in this transition char pp; // pop symbol in this transition
int guard; // Let i-th bit of guard from right hand is g_i int guard; // Let i-th bit of guard from right hand is g_i
int reset; // Let i-th bit of reset from right hand is r_i int reset; // Let i-th bit of reset from right hand is r_i
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 and reset 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
r_i=1(1<=i<=15) : i-th clock is reset in this transition r_i=1(1<=i<=15) : i-th clock is reset in this transition
g_0=0 && r_0=0 : no stack operation g_0=0 && r_0=0 : no stack operation
g_0=1 && r_0=0 : stack push operation g_0=1 && r_0=0 : stack push operation
g_0=0 && r_0=1 : stack pop operation g_0=0 && r_0=1 : stack pop operation
g_0=1 && r_0=1 : invalid : push and pop at the same time not possible g_0=1 && r_0=1 : invalid : push and pop at the same time not possible
*/ */
int *lbs; // constraint lower bounds int *lbs; // constraint lower bounds
int *ubs; // constraint upper bounds int *ubs; // constraint upper bounds
/* /*
size of lbs and ubs is equal to (|X|+1), where |X| is the number of clocks size of lbs and ubs is equal to (|X|+1), where |X| is the number of clocks
lbs[0] : lower bound for pop operation lbs[0] : lower bound for pop operation
lbs[i](1<=i<=15) : lower bound for i-th clock lbs[i](1<=i<=15) : lower bound for i-th clock
ubs[0] : upper bound for pop operation ubs[0] : upper bound for pop operation
ubs[i](1<=i<=15) : upper bound for i-th clock ubs[i](1<=i<=15) : upper bound for i-th clock
*/ */
}; };
......
include/tpdaZone.h
View file @ e4eea6fc
...@@ -17,61 +17,61 @@ extern bool **open1, **open2; // temporary variables for storing some edge weigh ...@@ -17,61 +17,61 @@ extern bool **open1, **open2; // temporary variables for storing some edge weigh
// state for timed automata // state for timed automata
class stateZone{ class stateZone{
public: public:
char P; // number of points in this state char P; // number of points in this state
char f; // 7-th bit is 1 iff push at L is done, rightmost 7 bits used for L or L = f & 127 char f; // 7-th bit is 1 iff push at L is done, rightmost 7 bits used for L or L = f & 127
char *del; // transitions in this state char *del; // transitions in this state
short *w; // forward and backward edges weight, this will act like a 2d array, index can calculated using function index(i, j, n) defined tpdaZone.h short *w; // forward and backward edges weight, this will act like a 2d array, index can calculated using function index(i, j, n) defined tpdaZone.h
// add next transition to this state if possible and return all generated states by doing this operation // add next transition to this state if possible and return all generated states by doing this operation
stateZone* addNextTPDA(char dn); stateZone* addNextTPDA(char dn);
// check if shuffle of this state with s2 is possible // check if shuffle of this state with s2 is possible
bool shuffleCheck(stateZone *s2); bool shuffleCheck(stateZone *s2);
// return shuffle of this state with s2 // return shuffle of this state with s2
stateZone* shuffle(stateZone *s2); stateZone* shuffle(stateZone *s2);
stateZone* reduceShuffle(stateZone *s2); stateZone* reduceShuffle(stateZone *s2);
// Return the first successor state whoose childrens will be right state for shuffle with current state // Return the first successor state whoose childrens will be right state for shuffle with current state
stateZone* sucState(); stateZone* sucState();
bool isFinal(); // return true iff this state is final bool isFinal(); // return true iff this state is final
void print(); // print this state void print(); // print this state
// return unique string for last reset points of a state participating in a combine operation as a left state // return unique string for last reset points of a state participating in a combine operation as a left state
string getKeyLeft(); string getKeyLeft();
// return unique string for hanging points of a state participating in a combine operation as a right state // return unique string for hanging points of a state participating in a combine operation as a right state
string getKeyRight(); string getKeyRight();
}; };
// partial run of the timed system as a sequence of pairs: (1) transition and (2) tsm value // partial run of the timed system as a sequence of pairs: (1) transition and (2) tsm value
class runZone{ class runZone{
public : public :
short P; // #points short P; // #points
char *del; // transitions char *del; // transitions
short **w; // weight matrix short **w; // weight matrix
runZone* addNext(char dn, char wn); // new run after adding transition 'dn' of tsm value 'wn' runZone* addNext(char dn, char wn); // new run after adding transition 'dn' of tsm value 'wn'
runZone* shuffle(runZone *s2); // concatenation of two partial runs runZone* shuffle(runZone *s2); // concatenation of two partial runs
void print(); // print the run with concrete global time stamps void print(); // print the run with concrete global time stamps
}; };
// info to keep track parents of current state or who are the states generated current state // info to keep track parents of current state or who are the states generated current state
class trackZone{ class trackZone{
public : public :
char type; //***** type of operation : atomic : 0, addNextTPDA : 1, shuffle or combine : 2 char type; //***** type of operation : atomic : 0, addNextTPDA : 1, shuffle or combine : 2
int left; // *****shuffle left state index in the main vector int left; // *****shuffle left state index in the main vector
int right; // ****shuffle right state index in the main vector int right; // ****shuffle right state index in the main vector
}; };
//this is used for checking if newly generated state was already generated earlier or not //this is used for checking if newly generated state was already generated earlier or not
......
src/timePushDown.cpp
View file @ e4eea6fc
...@@ -43,455 +43,455 @@ bool** pushDone; ...@@ -43,455 +43,455 @@ bool** pushDone;
// make a dfs from a reset transition to find some checked transition for clock x // make a dfs from a reset transition to find some checked transition for clock x
void getChecker(short int acttran, bool *visit, short int i, char x, bool *flag) { void getChecker(short int acttran, bool *visit, short int i, char x, bool *flag) {
short int s = transitions[i].target; short int s = transitions[i].target;
for(int j=0; j < nexttrans[s].size(); j++) { for(int j=0; j < nexttrans[s].size(); j++) {
short int t = nexttrans[s][j]; short int t = nexttrans[s][j];
if( isChecked(x, t) && !(*flag) && acttran == t) { if( isChecked(x, t) && !(*flag) && acttran == t) {
resecktrans[x].push_back(make_pair(acttran, t)); resecktrans[x].push_back(make_pair(acttran, t));
*flag = true; *flag = true;
} }
if( !visit[t] ) { // if transition t is not visited yet if( !visit[t] ) { // if transition t is not visited yet
visit[t] = true; visit[t] = true;
if(isChecked(x, t)) { // if x is reset at transition t if(isChecked(x, t)) { // if x is reset at transition t
resecktrans[x].push_back(make_pair(acttran, t)); resecktrans[x].push_back(make_pair(acttran, t));
} }
if(!isReset(x, t)) { // if clock x is not reset at transition t if(!isReset(x, t)) { // if clock x is not reset at transition t
getChecker(acttran, visit, t, x, flag); getChecker(acttran, visit, t, x, flag);
} }
} }
} }
} }
// get all the reset-check pair of transition for some clock // get all the reset-check pair of transition for some clock
void getresecktrans() { void getresecktrans() {
bool *visit = new bool[T+1]; bool *visit = new bool[T+1];
int i,j; int i,j;
resecktrans.resize(X+1); resecktrans.resize(X+1);
bool flag = false; bool flag = false;
for(char x=1; x <= X; x++) { // iterate through all clocks for(char x=1; x <= X; x++) { // iterate through all clocks
for(i=0; i <= T; i++) { // for all transitions for(i=0; i <= T; i++) { // for all transitions
if( (transitions[i].target) == (transitions[i].source) && isReset(x, i) && isChecked(x, i)) { if( (transitions[i].target) == (transitions[i].source) && isReset(x, i) && isChecked(x, i)) {
resecktrans[x].push_back(make_pair(i, i)); resecktrans[x].push_back(make_pair(i, i));
flag = true; flag = true;
} }
if(isReset(x, i)) { // if clock x is reset at transition i if(isReset(x, i)) { // if clock x is reset at transition i
for(j=0; j <= T; j++) for(j=0; j <= T; j++)
visit[j] = false; visit[j] = false;
visit[i] = true; visit[i] = true;
getChecker(i, visit, i, x, &flag); getChecker(i, visit, i, x, &flag);
} }
} }
} }
// for each clock x and each check(x # c) transition t, find the reset transitions(x:=0) // for each clock x and each check(x # c) transition t, find the reset transitions(x:=0)
possibleresets.resize(T+1); possibleresets.resize(T+1);
for(i=0; i < resecktrans[1].size(); i++) { for(i=0; i < resecktrans[1].size(); i++) {
possibleresets[resecktrans[1][i].second].push_back(resecktrans[1][i].first); possibleresets[resecktrans[1][i].second].push_back(resecktrans[1][i].first);
} }
} }
// if d1 and d2 are valid pair of reset-check for only clock x1(used for one clock + one stack special tpda) // if d1 and d2 are valid pair of reset-check for only clock x1(used for one clock + one stack special tpda)
bool isPossibleReset(char d1, char d2){ bool isPossibleReset(char d1, char d2){
for(char i=0; i < possibleresets[d2].size(); i++) { for(char i=0; i < possibleresets[d2].size(); i++) {
if(d1 == (possibleresets[d2][i]) ) if(d1 == (possibleresets[d2][i]) )
return true; return true;
} }
return false; return false;
} }
// get the input timed system given as a file(file name stored in the global variable 'inputfilename') // get the input timed system given as a file(file name stored in the global variable 'inputfilename')
void inputSystem() { 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 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;
//ifstream tiimeinfile ("in"); // timed system input file stream //ifstream tiimeinfile ("in"); // timed system input file stream
ifstream tiimeinfile (inputfilename); // timed system input file stream ifstream tiimeinfile (inputfilename); // timed system input file stream
// if there is any error opening the file // if there is any error opening the file
if( !(tiimeinfile.is_open()) ) { if( !(tiimeinfile.is_open()) ) {
cout << "\n****INPUT TIMED PUSH-DOWN FILE NOT FOUND ! ****\n"; cout << "\n****INPUT TIMED PUSH-DOWN FILE NOT FOUND ! ****\n";
exit(1); exit(1);
} }
tiimeinfile >> S; // #states in origianl automata tiimeinfile >> S; // #states in origianl automata
tiimeinfile >> T; // #transitions tiimeinfile >> T; // #transitions
transitions = new transition[T+1]; // allocate memory for transitions transitions = new transition[T+1]; // allocate memory for transitions
tiimeinfile >> x; // #clocks tiimeinfile >> x; // #clocks
X = x; X = x;
tiimeinfile >> x; // #actions tiimeinfile >> x; // #actions
A = x; A = x;
tiimeinfile >> x; // #stack_symbols tiimeinfile >> x; // #stack_symbols
AS = x; AS = x;
tiimeinfile >> SI; // input initial state tiimeinfile >> SI; // input initial state
tiimeinfile >> SF; // input final state tiimeinfile >> SF; // input final state
// 0-th transition // 0-th transition
transitions[0].source = 0; transitions[0].source = 0;
transitions[0].target = SI; transitions[0].target = SI;
transitions[0].a = 0; // event or action in this transition is silent transitions[0].a = 0; // event or action in this transition is silent
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
// 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) );
resettrans.resize(X+1); // used for earlier code resettrans.resize(X+1); // used for earlier code
checktrans.resize(X+1); // used for earlier checktrans.resize(X+1); // used for earlier
// all clock has been reset at 0-th transition // all clock has been reset at 0-th transition
for(j=1; j <= X; j++) { for(j=1; j <= X; j++) {
resettrans[j].push_back(0); resettrans[j].push_back(0);
} }
// get all the transitions // get all the transitions
for(i=1; i <= T; i++) { for(i=1; i <= T; i++) {
tiimeinfile >> x;
transitions[i].source = x; // source state in this transition
tiimeinfile >> x;
transitions[i].target = x; // target state in this transition
tiimeinfile >> x;
transitions[i].a = x; // event or action in this transition
tiimeinfile >> noofguards; // #guards in this transition
tiimeinfile >> noofresets; // #resets in this transition
transitions[i].lbs = new int[X+1]; // allocate memory for lower 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;
for(j=0; j < noofguards; j++) {
tiimeinfile >> x; // clock number for guard
if(x <= 0 || x > X) {
cout << "Clock number is not in the limit!" << endl;
exit(1);
}
guard |= a32[x]; // set i-th bit of guard to '1'
tiimeinfile >> lb >> ub; // bounds on the guard
if(lb < 0 || ub < (-1)) {
cout << "Bounds can't be negative!" << endl;
exit(1);
}
M = max(lb,M); // update M if M < lb
transitions[i].lbs[x] = lb; // lower bound for clock x
if(ub == (-1)) { // upper bound -1 means infinity
transitions[i].ubs[x] = INF;
}
else {
if(lb > ub) {
cout << " Lower bound can't be greater than upper bound!, lb :" << lb <<",ub :" << ub << endl;
exit(1);
}
M = max(ub, M); // update M if M < ub
transitions[i].ubs[x] = ub;
}
}
reset = 0;
// set i-th bit of 'reset' to '1' if i-th clock has been reset in this transition
for(j=0; j < noofresets; j++) {
tiimeinfile >> x; // clock number for guard
if(x <= 0 || x > X) {
cout << "Clock number is not in the limit!" << endl;
exit(1);
}
reset |= a32[x]; // set x-th bit of 'reset' to '1'
}
// read stack operation number, 0 : nop, 1 : push, 2 : pop, 3 : pop & push
tiimeinfile >> x;
if(x == 0) { // nop operation
// do nothing
}
else if(x == 1) { // push operation
guard |= 1; // set 0-th bit of gurad to '1'
tiimeinfile >> x; // stack push symbol
transitions[i].as = x;
transitions[i].ps = x;
}
else if(x == 2) { // pop operation
reset |= 1; // set 0-th bit of reset to '1'
tiimeinfile >> x; // stack pop symbol
transitions[i].as = x;
transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds
M = max(lb,M); // update M if M < lb
transitions[i].lbs[0] = lb; // lower bound for clock x
if(ub == (-1)) { // upper bound -1 means infinity
transitions[i].ubs[0] = INF;
}
else {
if(lb > ub) {
cout << " Lower bound can't be greater than upper bound!, lb :" << lb <<",ub :" << ub << endl;
exit(1);
}
M = max(ub, M); // update M if M < ub
transitions[i].ubs[0] = ub;
}
}
else if(x == 3) { // pop & then a push operation
// both push and pop operations are involved
reset |= 1; // set 0-th bit of reset to '1'
guard |= 1; // set 0-th bit of gurad to '1'
tiimeinfile >> x; // stack pop symbol
transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds
M = max(lb,M); // update M if M < lb
transitions[i].lbs[0] = lb; // lower bound for clock x
if(ub == (-1)) { // upper bound -1 means infinity
transitions[i].ubs[0] = INF;
}
else {
if(lb > ub) {
cout << " Lower bound can't be greater than upper bound!, lb :" << lb <<",ub :" << ub << endl;
exit(1);
}
M = max(ub, M); // update M if M < ub
transitions[i].ubs[0] = ub;
}
tiimeinfile >> x; // stack push symbol
transitions[i].ps = x;
}
else {
cout << "Invalid stack operation!" << endl;
exit(1);
}
transitions[i].guard = guard;
transitions[i].reset = reset;
// resetting and checking in which transitions for each clock
for(j=1; j <= X; j++) { // forget this
if(guard & a32[j]) // if j-th clock has been checked at i-th transitions
checktrans[j].push_back(i);
if(reset & a32[j]) // if j-th clock has been reset at i-th transitions // forget this
resettrans[j].push_back(i);
}
}
prevtrans.resize(S+1); // #rows = S+1 in the 2D vector prevtrans and nexttrans // forget this
nexttrans.resize(S+1); // forget this
for(i=0; i <= T; i++) {
prevtrans[transitions[i].target].push_back(i);
nexttrans[transitions[i].source].push_back(i);
}
tiimeinfile.close();
//******* forget this
pushDone = new bool*[T+1];
for(char t=0; t <= T; t++){
pushDone[t] = new bool[M];
for(char w=0; w < M; w++) {
pushDone[t][w] = false;
}
}
tiimeinfile >> x;
transitions[i].source = x; // source state in this transition
tiimeinfile >> x;
transitions[i].target = x; // target state in this transition
tiimeinfile >> x;
transitions[i].a = x; // event or action in this transition
tiimeinfile >> noofguards; // #guards in this transition
tiimeinfile >> noofresets; // #resets in this transition
transitions[i].lbs = new int[X+1]; // allocate memory for lower 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;
for(j=0; j < noofguards; j++) {
tiimeinfile >> x; // clock number for guard
if(x <= 0 || x > X) {
cout << "Clock number is not in the limit!" << endl;
exit(1);
}
guard |= a32[x]; // set i-th bit of guard to '1'
tiimeinfile >> lb >> ub; // bounds on the guard
if(lb < 0 || ub < (-1)) {
cout << "Bounds can't be negative!" << endl;
exit(1);
}
M = max(lb,M); // update M if M < lb
transitions[i].lbs[x] = lb; // lower bound for clock x
if(ub == (-1)) { // upper bound -1 means infinity
transitions[i].ubs[x] = INF;
}
else {
if(lb > ub) {
cout << " Lower bound can't be greater than upper bound!, lb :" << lb <<",ub :" << ub << endl;
exit(1);
}
M = max(ub, M); // update M if M < ub
transitions[i].ubs[x] = ub;
}
}
reset = 0;
// set i-th bit of 'reset' to '1' if i-th clock has been reset in this transition
for(j=0; j < noofresets; j++) {
tiimeinfile >> x; // clock number for guard
if(x <= 0 || x > X) {
cout << "Clock number is not in the limit!" << endl;
exit(1);
}
reset |= a32[x]; // set x-th bit of 'reset' to '1'
}
// read stack operation number, 0 : nop, 1 : push, 2 : pop, 3 : pop & push
tiimeinfile >> x;
if(x == 0) { // nop operation
// do nothing
}
else if(x == 1) { // push operation
guard |= 1; // set 0-th bit of gurad to '1'
tiimeinfile >> x; // stack push symbol
transitions[i].as = x;
transitions[i].ps = x;
}
else if(x == 2) { // pop operation
reset |= 1; // set 0-th bit of reset to '1'
tiimeinfile >> x; // stack pop symbol
transitions[i].as = x;
transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds
M = max(lb,M); // update M if M < lb
transitions[i].lbs[0] = lb; // lower bound for clock x
if(ub == (-1)) { // upper bound -1 means infinity
transitions[i].ubs[0] = INF;
}
else {
if(lb > ub) {
cout << " Lower bound can't be greater than upper bound!, lb :" << lb <<",ub :" << ub << endl;
exit(1);
}
M = max(ub, M); // update M if M < ub
transitions[i].ubs[0] = ub;
}
}
else if(x == 3) { // pop & then a push operation
// both push and pop operations are involved
reset |= 1; // set 0-th bit of reset to '1'
guard |= 1; // set 0-th bit of gurad to '1'
tiimeinfile >> x; // stack pop symbol
transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds
M = max(lb,M); // update M if M < lb
transitions[i].lbs[0] = lb; // lower bound for clock x
if(ub == (-1)) { // upper bound -1 means infinity
transitions[i].ubs[0] = INF;
}
else {
if(lb > ub) {
cout << " Lower bound can't be greater than upper bound!, lb :" << lb <<",ub :" << ub << endl;
exit(1);
}
M = max(ub, M); // update M if M < ub
transitions[i].ubs[0] = ub;
}
tiimeinfile >> x; // stack push symbol
transitions[i].ps = x;
}
else {
cout << "Invalid stack operation!" << endl;
exit(1);
}
transitions[i].guard = guard;
transitions[i].reset = reset;
// resetting and checking in which transitions for each clock
for(j=1; j <= X; j++) { // forget this
if(guard & a32[j]) // if j-th clock has been checked at i-th transitions
checktrans[j].push_back(i);
if(reset & a32[j]) // if j-th clock has been reset at i-th transitions // forget this
resettrans[j].push_back(i);
}
}
prevtrans.resize(S+1); // #rows = S+1 in the 2D vector prevtrans and nexttrans // forget this
nexttrans.resize(S+1); // forget this
for(i=0; i <= T; i++) {
prevtrans[transitions[i].target].push_back(i);
nexttrans[transitions[i].source].push_back(i);
}
tiimeinfile.close();
//******* forget this
pushDone = new bool*[T+1];
for(char t=0; t <= T; t++){
pushDone[t] = new bool[M];
for(char w=0; w < M; w++) {
pushDone[t][w] = false;
}
}
} }
void print_system() { void print_system() {
cout << "#States :" << S << endl; cout << "#States :" << S << endl;
cout << "#Transitions :" << T << endl; cout << "#Transitions :" << T << endl;
cout << "Initial state :" << SI << endl; cout << "Initial state :" << SI << endl;
cout << "Final state :" << SF << endl; cout << "Final state :" << SF << endl;
cout << "#Clocks :" << int(X) << endl; cout << "#Clocks :" << int(X) << endl;
cout << "#actions :" << int(A) << endl; cout << "#actions :" << int(A) << endl;
cout << "#Stack symbols :" << int(AS) << endl << endl; cout << "#Stack symbols :" << int(AS) << endl << endl;
cout << "Showing the transitions:" << endl << endl; cout << "Showing the transitions:" << endl << endl;
int reset, guard; int reset, guard;
int i,j; int i,j;
for(i = 0; i < T; i++) { for(i = 0; i < T; i++) {
reset = transitions[i].reset; reset = transitions[i].reset;
guard = transitions[i].guard; guard = transitions[i].guard;
cout << i << "-th transition :\n"; cout << i << "-th transition :\n";
cout << "\tGurad bit vector : " << inttobinary(transitions[i].guard) << endl; cout << "\tGurad bit vector : " << inttobinary(transitions[i].guard) << endl;
cout << "\tClock Constraints:\n"; cout << "\tClock Constraints:\n";
for(j=1; j <= X; j++) { for(j=1; j <= X; j++) {
if( (transitions[i].guard) & a32[j]) { if( (transitions[i].guard) & a32[j]) {
cout << "\t\t" << (transitions[i].lbs[j]) << " <= x" << j ; cout << "\t\t" << (transitions[i].lbs[j]) << " <= x" << j ;
if( (transitions[i].ubs[j]) == INF) if( (transitions[i].ubs[j]) == INF)
cout << " <= inf" << endl; cout << " <= inf" << endl;
else else
cout << " <= " << (transitions[i].ubs[j]) << endl; cout << " <= " << (transitions[i].ubs[j]) << endl;
} }
} }
//cout << endl << endl; //cout << endl << endl;
cout << "\tReset bit vector : " << inttobinary(transitions[i].reset) << endl; cout << "\tReset bit vector : " << inttobinary(transitions[i].reset) << endl;
cout << "\tReset = {"; cout << "\tReset = {";
for(j=1; j <= X; j++) { for(j=1; j <= X; j++) {
if( (transitions[i].reset) & a32[j]) if( (transitions[i].reset) & a32[j])
cout << " x" << j ; cout << " x" << j ;
} }
cout << "}" << endl; cout << "}" << endl;
cout << "\tStack operation : "; cout << "\tStack operation : ";
if( !(guard & 1) && !(reset & 1) ) { if( !(guard & 1) && !(reset & 1) ) {
cout << "nop" << endl; cout << "nop" << endl;
} }
else if( (guard & 1) && !(reset & 1) ) { else if( (guard & 1) && !(reset & 1) ) {
cout << "push" << endl; cout << "push" << endl;
cout << "\t\tstack symbol : " << int(transitions[i].ps) << endl ; cout << "\t\tstack symbol : " << int(transitions[i].ps) << endl ;
} }
else if( !(guard & 1) && (reset & 1) ) { else if( !(guard & 1) && (reset & 1) ) {
cout << "pop" << endl; cout << "pop" << endl;
cout << "\t\tstack symbol : " << int(transitions[i].pp) << endl ; cout << "\t\tstack symbol : " << int(transitions[i].pp) << endl ;
cout << "\t\tpop condition : " << (transitions[i].lbs[0]) << " <= age(" << int(transitions[i].pp) << ") <= "; cout << "\t\tpop condition : " << (transitions[i].lbs[0]) << " <= age(" << int(transitions[i].pp) << ") <= ";
if( (transitions[i].ubs[0]) == INF) if( (transitions[i].ubs[0]) == INF)
cout << "inf" << endl; cout << "inf" << endl;
else else
cout << (transitions[i].ubs[0]) << endl; cout << (transitions[i].ubs[0]) << endl;
} }
else if( (guard & 1) && (reset & 1) ) { else if( (guard & 1) && (reset & 1) ) {
cout << "pop & push" << endl; cout << "pop & push" << endl;
cout << "\t\tpop symbol : " << int(transitions[i].pp) << endl ; cout << "\t\tpop symbol : " << int(transitions[i].pp) << endl ;
cout << "\t\tpop condition : " << (transitions[i].lbs[0]) << " <= age(" << int(transitions[i].pp) << ") <= "; cout << "\t\tpop condition : " << (transitions[i].lbs[0]) << " <= age(" << int(transitions[i].pp) << ") <= ";
if( (transitions[i].ubs[0]) == INF) if( (transitions[i].ubs[0]) == INF)
cout << "inf" << endl; cout << "inf" << endl;
else else
cout << (transitions[i].ubs[0]) << endl; cout << (transitions[i].ubs[0]) << endl;
cout << "\t\tpush symbol : " << int(transitions[i].ps) << endl ; cout << "\t\tpush symbol : " << int(transitions[i].ps) << endl ;
} }
cout << endl << endl; cout << endl << endl;
} }
/* /*
cout << endl << "Printing source and target transitions:" << endl; cout << endl << "Printing source and target transitions:" << endl;
for(i=0; i <= S; i++) { for(i=0; i <= S; i++) {
cout << "State " << i << ":" << endl; cout << "State " << i << ":" << endl;
cout << "\t Previous transitions: " ; cout << "\t Previous transitions: " ;
for(j = 0 ; j < prevtrans[i].size(); j++) for(j = 0 ; j < prevtrans[i].size(); j++)
cout << prevtrans[i][j] << ","; cout << prevtrans[i][j] << ",";
cout << "\n\t Next transitions: " ; cout << "\n\t Next transitions: " ;
for(j = 0 ; j < nexttrans[i].size(); j++) for(j = 0 ; j < nexttrans[i].size(); j++)
cout << nexttrans[i][j] << ","; cout << nexttrans[i][j] << ",";
cout << endl << endl; cout << endl << endl;
} }
cout << endl << "Printing reset transitions for clocks:" << endl; cout << endl << "Printing reset transitions for clocks:" << endl;
for(i=1; i <= X; i++) { for(i=1; i <= X; i++) {
cout << "Clock " << int(i) << ": "; cout << "Clock " << int(i) << ": ";
for(j=0; j < resettrans[i].size(); j++) for(j=0; j < resettrans[i].size(); j++)
cout << resettrans[i][j] << ","; cout << resettrans[i][j] << ",";
cout << endl; cout << endl;
} }
cout << endl << endl; cout << endl << endl;
cout << endl << "Printing check transitions for clocks:" << endl; cout << endl << "Printing check transitions for clocks:" << endl;
for(i=1; i <= X; i++) { for(i=1; i <= X; i++) {
cout << "Clock " << int(i) << ": "; cout << "Clock " << int(i) << ": ";
for(j=0; j < checktrans[i].size(); j++) for(j=0; j < checktrans[i].size(); j++)
cout << checktrans[i][j] << ","; cout << checktrans[i][j] << ",";
cout << endl; cout << endl;
} }
*/ */
cout << endl << endl; cout << endl << endl;
} }
// is clock x has been reset at transition d // is clock x has been reset at transition d
bool isReset(char x, short int d) { bool isReset(char x, short int d) {
if( (transitions[d].reset) & a32[x]) if( (transitions[d].reset) & a32[x])
return true; return true;
return false; return false;
} }
// is clock x has been checked at transition delta // is clock x has been checked at transition delta
bool isChecked(char x, short int d) { bool isChecked(char x, short int d) {
if( (transitions[d].guard) & a32[x]) if( (transitions[d].guard) & a32[x])
return true; return true;
return false; return false;
} }
// is there a push at transition delta // is there a push at transition delta
bool isPush(short int d) { bool isPush(short int d) {
if( (transitions[d].guard) & a32[0]) if( (transitions[d].guard) & a32[0])
return true; return true;
return false; return false;
} }
// is there a pop at transition delta // is there a pop at transition delta
bool isPop(short int d) { bool isPop(short int d) {
if( (transitions[d].reset) & a32[0]) if( (transitions[d].reset) & a32[0])
return true; return true;
return false; return false;
} }
// return a mod b(always return a +ve number unlike c % operator) // DONE // return a mod b(always return a +ve number unlike c % operator) // DONE
short int mod(short int a, short int b) { short int mod(short int a, short int b) {
short int r = a % b; short int r = a % b;
if(r < 0) if(r < 0)
return (r+b); return (r+b);
return r; return r;
} }
src/tpdaCGPP.cpp
View file @ e4eea6fc
...@@ -19,38 +19,38 @@ vector<pair<stateGCPP*, trackCGPP*> > allStates; ...@@ -19,38 +19,38 @@ vector<pair<stateGCPP*, trackCGPP*> > allStates;
// return 1 iff state vs was not found earlier or vs is new state // return 1 iff state vs was not found earlier or vs is new state
bool identity(stateGCPP *vs) { bool identity(stateGCPP *vs) {
string os=""; // output string string os=""; // output string
char i; // looper char i; // looper
for( i=0; i < (vs->P); i++ ) // add transitions to the string os for( i=0; i < (vs->P); i++ ) // add transitions to the string os
os += (vs->del[i]); os += (vs->del[i]);
for(i=0; i < (vs->P); i++ ) // add tsm values to the string os for(i=0; i < (vs->P); i++ ) // add tsm values to the string os
os += (vs->w[i]); os += (vs->w[i]);
os += char(vs->f); // add the rightmost 8 bits of vs->f to os os += char(vs->f); // add the rightmost 8 bits of vs->f to os
os += char( (vs->f) >> 8 ) ; // add the leftmost 8 bits of vs->f to os os += char( (vs->f) >> 8 ) ; // add the leftmost 8 bits of vs->f to os
os += (vs->L); // add left point to os os += (vs->L); // add left point to os
// return true if os inserted in the set 'tpdaGCPPtrie' successfully // return true if os inserted in the set 'tpdaGCPPtrie' successfully
//return (tpdaGCPPtrie.insert(os) ).second; //return (tpdaGCPPtrie.insert(os) ).second;
// using hashmap : if os key was not there then mapGCPP[os]==false // using hashmap : if os key was not there then mapGCPP[os]==false
if( mapGCPP[os] ) // 'os' is there in hashmap if( mapGCPP[os] ) // 'os' is there in hashmap
return false; return false;
else{ // 'os' is not there in hashmap else{ // 'os' is not there in hashmap
mapGCPP[os] = true; mapGCPP[os] = true;
return true;; return true;;
} }
} }
// return distance between point i to point j // return distance between point i to point j
short stateGCPP::dist(char i, char j) { short stateGCPP::dist(char i, char j) {
short dis=0; // distance between i to j, initially 0 short dis=0; // distance between i to j, initially 0
for(char k=i; k < j; k++) // sum up the distances between consecutive points for(char k=i; k < j; k++) // sum up the distances between consecutive points
dis += mod( w[k] - w[k-1], M); dis += mod( w[k] - w[k-1], M);
return dis; return dis;
...@@ -71,521 +71,521 @@ bool stateGCPP::big(char i, char j) { ...@@ -71,521 +71,521 @@ bool stateGCPP::big(char i, char j) {
// reduce the #points after shuffle by using forget operation if possible and return the new state // reduce the #points after shuffle by using forget operation if possible and return the new state
stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) { stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
char *del2 = s2->del, *w2 = s2->w; char *del2 = s2->del, *w2 = s2->w;
char P2 = s2->P, L2 = s2->L; char P2 = s2->P, L2 = s2->L;
short f2 = s2->f; short f2 = s2->f;
short curReset, reset, tempReset; // temp variables to keep reset for a range of points short curReset, reset, tempReset; // temp variables to keep reset for a range of points
char count=0; // used for storing #points in new state char count=0; // used for storing #points in new state
char i, j; // loopers char i, j; // loopers
// we have to take all the points from s2->L+1 to s2->P, point s2->L may not be there // we have to take all the points from s2->L+1 to s2->P, point s2->L may not be there
// all the points from 1 to L of first state will be there in new state, last point P may not be there // all the points from 1 to L of first state will be there in new state, last point P may not be there
// take union of resets for points between s2->L+1(including) and s2->P(including) // take union of resets for points between s2->L+1(including) and s2->P(including)
curReset = 0; curReset = 0;
for(i=L2; i < P2; i++) for(i=L2; i < P2; i++)
curReset |= ( transitions[ del2[i] ].reset ); curReset |= ( transitions[ del2[i] ].reset );
tempReset = curReset; // store this value for later use tempReset = curReset; // store this value for later use
for( i=P-1; i >= L; i--) { for( i=P-1; i >= L; i--) {
reset = ( transitions[ del[i] ].reset ); reset = ( transitions[ del[i] ].reset );
/* there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock /* there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
reset at (i+1) point of 1st state which has not reset to any of its right points for both state */ reset at (i+1) point of 1st state which has not reset to any of its right points for both state */
if( reset & (~curReset) & (~1) ) { // (~) : ignore the 0-th bit, used for stack operation if( reset & (~curReset) & (~1) ) { // (~) : ignore the 0-th bit, used for stack operation
count++; // this point should be in new state, so increase the counter count++; // this point should be in new state, so increase the counter
curReset |= reset; // union reset set at this point with earlier set curReset |= reset; // union reset set at this point with earlier set
} }
} }
// addition of 'L' below comes from the fact that all point from 1 to L of first state is there in new state // addition of 'L' below comes from the fact that all point from 1 to L of first state is there in new state
// (s2->P - s2-> L) comes from : all points s2->L+1 to s2->P are there in new state // (s2->P - s2-> L) comes from : all points s2->L+1 to s2->P are there in new state
count += L + (P2 - L2); // #points in new state count += L + (P2 - L2); // #points in new state
stateGCPP *vs = new stateGCPP(); // new TA state stateGCPP *vs = new stateGCPP(); // new TA state
vs->del = new char[count]; // allocate memory vs->del = new char[count]; // allocate memory
vs->w = new char[count]; vs->w = new char[count];
vs->L = L; vs->L = L;
short nf = 0; // initially flag is zero short nf = 0; // initially flag is zero
short dis; // distance variable short dis; // distance variable
j = count - 1; // index of the rightmost point of new state j = count - 1; // index of the rightmost point of new state
// Here we are copying points from s2->L+1 to s2->P of 2nd state to new state // Here we are copying points from s2->L+1 to s2->P of 2nd state to new state
for(i=P2 - 1; i >= L2; i--, j--) { for(i=P2 - 1; i >= L2; i--, j--) {
vs->del[j] = del2[i]; // copy (i+1)-th transition to (j+1) transition of new state vs->del[j] = del2[i]; // copy (i+1)-th transition to (j+1) transition of new state
vs->w[j] = w2[i]; // copy (i+1)-th tsm to (j+1) tsm of new state vs->w[j] = w2[i]; // copy (i+1)-th tsm to (j+1) tsm of new state
// if distance (i+1)->(i+2) of 2nd state is accurate, then distance (j+1)->(j+2) of new state is accurate // if distance (i+1)->(i+2) of 2nd state is accurate, then distance (j+1)->(j+2) of new state is accurate
if( f2 & a32[i+1] ) if( f2 & a32[i+1] )
nf |= a32[j+1]; nf |= a32[j+1];
} }
// Here we are copying points from 1 to L-1 of 1st state to new state // Here we are copying points from 1 to L-1 of 1st state to new state
for(j=0; j < (L-1); j++) { for(j=0; j < (L-1); j++) {
vs->del[j] = del[j]; vs->del[j] = del[j];
vs->w[j] = w[j]; vs->w[j] = w[j];
// if distance (j+1)->(j+2) of 1st state is accurate, then distance (j+1)->(j+2) of new state is accurate // if distance (j+1)->(j+2) of 1st state is accurate, then distance (j+1)->(j+2) of new state is accurate
nf |= ( f & a32[j+1] ); nf |= ( f & a32[j+1] );
} }
//copy the point L, doing it separately because of the flag variable which is not applicable for L-th point //copy the point L, doing it separately because of the flag variable which is not applicable for L-th point
vs->del[L-1] = del[L-1]; vs->del[L-1] = del[L-1];
vs->w[L-1] = w[L-1]; vs->w[L-1] = w[L-1];
// Now we watch out for points from L+1 to P of 1st state // Now we watch out for points from L+1 to P of 1st state
char lastindex = P;// last index of the point we have taken so far, although P might not be included char lastindex = P;// last index of the point we have taken so far, although P might not be included
curReset = tempReset; //get the union of resets for points between s2->L+1 and s2->P curReset = tempReset; //get the union of resets for points between s2->L+1 and s2->P
// current indices j of new state we have to take care // current indices j of new state we have to take care
j = (count - 1) - (P2 - L2); j = (count - 1) - (P2 - L2);
for(i=P-1; i >= L; i--) { for(i=P-1; i >= L; i--) {
reset = ( transitions[ del[i] ].reset ); // current point reset set reset = ( transitions[ del[i] ].reset ); // current point reset set
if( reset & (~curReset) & (~1) ) { // if current point has more reset then seen earlier if( reset & (~curReset) & (~1) ) { // if current point has more reset then seen earlier
vs->del[j] = del[i]; vs->del[j] = del[i];
vs->w[j] = w[i]; vs->w[j] = w[i];
if( lastindex == P ) { // if (i+1) is the first point we are considering after starting the loop if( lastindex == P ) { // if (i+1) is the first point we are considering after starting the loop
// In if : first check is for accuracy check from L to P of left state // In if : first check is for accuracy check from L to P of left state
// In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen // In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen
if( !big(i+1, P) && ( i == (P-1) || (f2 & a32[L2]) ) ) { if( !big(i+1, P) && ( i == (P-1) || (f2 & a32[L2]) ) ) {
dis = dist(i+1, P) + mod( w2[L2] - w[P-1], M); dis = dist(i+1, P) + mod( w2[L2] - w[P-1], M);
if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
nf |= a32[j+1]; nf |= a32[j+1];
} }
} }
else { else {
if( !big(i+1, lastindex+1) ) if( !big(i+1, lastindex+1) )
nf |= a32[j+1]; nf |= a32[j+1];
} }
curReset |= reset; curReset |= reset;
j--; j--;
lastindex = i; lastindex = i;
} }
} }
// one accuracy we yet have to compute which starts from L-th point of first state // one accuracy we yet have to compute which starts from L-th point of first state
if( lastindex == P ) { // if we have not taken any point from L+1 to P of 1st state if( lastindex == P ) { // if we have not taken any point from L+1 to P of 1st state
// In if : first check is for accuracy check from L to P of left state // In if : first check is for accuracy check from L to P of left state
// In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen // In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen
if( !big(L, P) && (f2 & a32[L2] ) ) { // if distance between L and R of 1st state is accurate if( !big(L, P) && (f2 & a32[L2] ) ) { // if distance between L and R of 1st state is accurate
dis = dist(L, P) + mod( w2[L2] - w[P-1], M); dis = dist(L, P) + mod( w2[L2] - w[P-1], M);
if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
nf |= a32[L]; nf |= a32[L];
} }
} }
else{ else{
// if distance from L-th point to lastindex+1-th of 1st state is accurate // if distance from L-th point to lastindex+1-th of 1st state is accurate
if( !big(L, lastindex+1) ) if( !big(L, lastindex+1) )
nf |= a32[L]; nf |= a32[L];
} }
if(f & 1) // push info from left state will be same if(f & 1) // push info from left state will be same
nf |= 1; nf |= 1;
nf |= a3215; // pop at right(R) is done nf |= a3215; // pop at right(R) is done
vs->f = nf; // add the flag variable also vs->f = nf; // add the flag variable also
vs->P = count; // #points in new state vs->P = count; // #points in new state
return vs; return vs;
} }
// check if shuffle of this state with s2 is possible // check if shuffle of this state with s2 is possible
bool stateGCPP::shuffleCheck(stateGCPP *s2) { bool stateGCPP::shuffleCheck(stateGCPP *s2) {
if( L == P || (s2->L) == (s2->P) ) // both state should have non-trival block if( L == P || (s2->L) == (s2->P) ) // both state should have non-trival block
return false; return false;
if( !isPush(del[P-1]) ) // there should be a push at last transition of left state if( !isPush(del[P-1]) ) // there should be a push at last transition of left state
return false; return false;
// there should be a push at L of s2 and pop at R of s2, note : del[P-1] = del2[P2-1] // there should be a push at L of s2 and pop at R of s2, note : del[P-1] = del2[P2-1]
if( !isPush( s2->del[s2->L-1] ) || !isPop( s2->del[s2->P-1] ) ) if( !isPush( s2->del[s2->L-1] ) || !isPop( s2->del[s2->P-1] ) )
return false; return false;
if( !( (s2->f) & 1 ) || !( (s2->f) & a3215 ) ) // push-pop edge should be connected in right state if( !( (s2->f) & 1 ) || !( (s2->f) & a3215 ) ) // push-pop edge should be connected in right state
return false; return false;
if( getKeyLeft() != (s2->getKeyRight() ) ) if( getKeyLeft() != (s2->getKeyRight() ) )
return false; return false;
return true; return true;
} }
// shuffle of this state with state s2 and return the new state // shuffle of this state with state s2 and return the new state
stateGCPP* stateGCPP::shuffle(stateGCPP *s2){ // shuffle with state s2 stateGCPP* stateGCPP::shuffle(stateGCPP *s2){ // shuffle with state s2
if(! shuffleCheck(s2) ) if(! shuffleCheck(s2) )
return NULL; return NULL;
return reduceShuffle(s2); return reduceShuffle(s2);
} }
// add transition 'dn' to current state and then forget some points if possible, return the new state // add transition 'dn' to current state and then forget some points if possible, return the new state
stateGCPP* stateGCPP::reduce(char dn){ stateGCPP* stateGCPP::reduce(char dn){
short reset; // variable for reset bit vector short reset; // variable for reset bit vector
short nf = 0; // flag variable for new state short nf = 0; // flag variable for new state
char count = 0; // #points in new state char count = 0; // #points in new state
char i; // looper char i; // looper
short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn' short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
for( i=P-1; i >= L; i-- ) { for( i=P-1; i >= L; i-- ) {
reset = transitions[ del[i] ].reset; // reset at transition at the (i+1)-th point 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 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' curReset |= reset; // the 'curReset' will have more bit with value '1'
count++; // we have to take (i+1)-th point count++; // we have to take (i+1)-th point
} }
} }
// all the hanging points and point L and point for transition 'dn' also be there // all the hanging points and point L and point for transition 'dn' also be there
count += (L+1); // number of points in new state count += (L+1); // number of points in new state
// pointer to the new state // pointer to the new state
stateGCPP* vs = new stateGCPP(); stateGCPP* vs = new stateGCPP();
vs->P = count; // #points in new state vs->P = count; // #points in new state
vs->L = L; // left point remain same vs->L = L; // left point remain same
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
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];
} }
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
nf |= ( f & a32[i] ); nf |= ( f & a32[i] );
} }
vs->del[count-1] = dn; // trans at last point, till now we don't know the weight vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
char lastindex = P; // 'lastindex' used for accuracy between two points in new state char lastindex = P; // 'lastindex' used for accuracy between two points in new state
char firstindex; char firstindex;
char j = count-2; // assgin trans and tsm from index count-2 upto L char j = count-2; // assgin trans and tsm from index count-2 upto L
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'
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
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
} }
// store the accuracy from last point(active in new state) before dn and P in i+1-th bit of nf // 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] // 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 // we yet don't know the tsm for 'dn', so full calculation is not done in this function
else{ else{
firstindex = i; firstindex = i;
if( !big(i+1, P) ) if( !big(i+1, P) )
nf |= a32[j+1]; nf |= a32[j+1];
vs->w[count-1] = dist(i+1, P); vs->w[count-1] = dist(i+1, P);
} }
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
} }
} }
// 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) ) {
// vs->w[count-1] = dist(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 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 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] // 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 // 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** else{ // if you have not choosed any point in the middle starting from point P**
if( !big(L, P) ) if( !big(L, P) )
nf |= a32[L]; nf |= a32[L];
vs->w[count-1] = dist(L, P); vs->w[count-1] = dist(L, P);
} }
if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively
nf |= (1 | a3215) ; nf |= (1 | a3215) ;
else else
nf |= (f & 1) ; // previous push information remain same nf |= (f & 1) ; // previous push information remain same
// last distance accuracy // last distance accuracy
vs->f = nf; // add partial flag variable to new state vs->f = nf; // add partial flag variable to new state
return vs; // return the partially new state, **** last tsm missing with partial nf as given 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 // 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, short *clockDis, bool *clockAcc) { bool stateGCPP::consSatisfied(char dn, char wn, short *clockDis, bool *clockAcc) {
short dis; short dis;
for(char x=1; x <= X; x++) { for(char x=1; x <= X; x++) {
if( isChecked(x, dn) ) { // if there is a check for clock x if( isChecked(x, dn) ) { // if there is a check for clock x
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 ) ;
if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) ) if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) )
return false; return false;
} }
else if( (transitions[dn].ubs[x]) != INF ) else if( (transitions[dn].ubs[x]) != INF )
return false; return false;
} }
} }
return true; return true;
} }
// 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, short dlr, bool aclr) { bool stateGCPP::stackCheck(char dn, char wn, short dlr, bool aclr) {
int ub = transitions[dn].ubs[0]; int ub = transitions[dn].ubs[0];
if(aclr) { // if distance from L to R is small if(aclr) { // if distance from L to R is small
short dis = dlr + mod( wn - w[P-1], M ); short dis = dlr + mod( wn - w[P-1], M );
if( ( dis < transitions[dn].lbs[0] ) || dis > ub ) if( ( dis < transitions[dn].lbs[0] ) || dis > ub )
return false; return false;
else else
return true; return true;
} }
else if(ub == INF) // if distance from L to R is big else if(ub == INF) // if distance from L to R is big
return true; return true;
return false; // distance is big, but upper bound is not infinity return false; // distance is big, but upper bound is not infinity
} }
// Add all possible upcoming transition just after the last transition of this state if all clock and stack constraints are satisfied // Add all possible upcoming transition just after the last transition of this state if all clock and stack constraints are satisfied
vector<stateGCPP*> stateGCPP::addNextTPDA() { vector<stateGCPP*> stateGCPP::addNextTPDA() {
vector<stateGCPP*> v; // will contain all the states generated by adding a new transition vector<stateGCPP*> v; // will contain all the states generated by adding a new transition
if( L < P && isPush( del[P-1] ) ) // there should not be any push at R if there is a non-trivial block(L < R) if( L < P && isPush( del[P-1] ) ) // there should not be any push at R if there is a non-trivial block(L < R)
return v; // return empty vector return v; // return empty vector
// we actually will not call for the below case // we actually will not call for the below case
// if there is a push at L and there is a pop at R, then first shuffle, then for the shuffled state, add new transitions // if there is a push at L and there is a pop at R, then first shuffle, then for the shuffled state, add new transitions
if( isPush( del[L-1] ) && isPop( del[P-1] ) && (f & 1) && (f & a3215) ) if( isPush( del[L-1] ) && isPop( del[P-1] ) && (f & 1) && (f & a3215) )
return v; return v;
short dlr = dist(L, P); // distance between point L to R short dlr = dist(L, P); // distance between point L to R
bool aclr = !big(L, P); // accuracy between point L to R bool aclr = !big(L, P); // accuracy between point L to R
char dn; // variable for new upcoming transition char dn; // variable for new upcoming transition
char wn; // variable contain TSM for the upcoming transition char wn; // variable contain TSM for the upcoming transition
bool popflag; // 1 iff there is pop at the new transition 'dn' bool popflag; // 1 iff there is pop at the new transition 'dn'
bool pushAtL = isPush( del[L-1] ); // if there is a push at L of this state bool pushAtL = isPush( del[L-1] ); // if there is a push at L of this state
char i, j; // loooper char i, j; // loooper
short dis; // distance calculation variable short dis; // distance calculation variable
char q = transitions[ del[P-1] ].target; // target state of last transition char q = transitions[ del[P-1] ].target; // target state of last transition
// iterate through all the upcoming transitions // iterate through all the upcoming transitions
for(i=0; i < nexttrans[q].size(); i++) { for(i=0; i < nexttrans[q].size(); i++) {
dn = nexttrans[q][i]; // i-th upcoming transition dn = nexttrans[q][i]; // i-th upcoming transition
popflag = isPop(dn); // popflag = 1 iff there is a pop at transition 'dn' popflag = isPop(dn); // popflag = 1 iff there is a pop at transition 'dn'
// if there is a pop at 'dn', but no push at L in this state, don't do anything // if there is a pop at 'dn', but no push at L in this state, don't do anything
if( popflag && !pushAtL ) { } if( popflag && !pushAtL ) { }
// if there is a pop at 'dn', but push is already done at L, do nothing(push must come before pop) // if there is a pop at 'dn', but push is already done at L, do nothing(push must come before pop)
else if( popflag && (f & 1) ) { } else if( popflag && (f & 1) ) { }
// push-pop symbol is not same, do nothing // push-pop symbol is not same, do nothing
else if( popflag && ( (transitions[ del[L-1] ].ps) != (transitions[dn].pp) ) ) { } else if( popflag && ( (transitions[ del[L-1] ].ps) != (transitions[dn].pp) ) ) { }
// o.w try to add new transtitions to the right // o.w try to add new transtitions to the right
else{ else{
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]
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]
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--) {
if( isReset( x, del[j] ) ) { // if there is a reset for clock x at (j+1)-th point if( isReset( x, del[j] ) ) { // if there is a reset for clock x at (j+1)-th point
if( big(j+1, P) ) // if distance is big from last reset point for clock x to point P if( big(j+1, P) ) // if distance is big from last reset point for clock x to point P
clockAcc[x] = false; clockAcc[x] = false;
else { else {
clockAcc[x] = true; clockAcc[x] = true;
clockDis[x] = dist(j+1, P); clockDis[x] = dist(j+1, P);
} }
j = -1; //Stop the inner loop beacuse last reset point for clock x found j = -1; //Stop the inner loop beacuse last reset point for clock x found
} }
} }
} }
// 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
for(wn=0; wn < M; wn++) { for(wn=0; wn < M; wn++) {
// if clock constraint not satisfied // if clock constraint not satisfied
if( !consSatisfied( dn, wn, clockDis, clockAcc) ) { } if( !consSatisfied( dn, wn, clockDis, clockAcc) ) { }
// if stack constraint not satisfied // if stack constraint not satisfied
else if( ( popflag && ( !stackCheck(dn, wn, dlr, aclr) ) ) ) { } else if( ( popflag && ( !stackCheck(dn, wn, dlr, aclr) ) ) ) { }
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();
rs->L = L; // left point remain same rs->L = L; // left point remain same
rs-> P = vs->P; // #points in new state rs-> P = vs->P; // #points in new state
rs->del = vs->del; // transitions are same as vs returned in reduce operation rs->del = vs->del; // transitions are same as vs returned in reduce operation
rs->w = new char[vs->P]; // last tsm value different, so change the whole array of tsm's rs->w = new char[vs->P]; // last tsm value different, so change the whole array of tsm's
for(j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs for(j=0; j < (vs->P - 1); j++) { // tsm values before last point remain same as vs
rs->w[j] = vs->w[j]; rs->w[j] = vs->w[j];
} }
rs->w[vs->P - 1] = wn; // new tsm value for last point rs->w[vs->P - 1] = wn; // new tsm value for last point
rs->f = (vs->f) & ( ~a32[vs->P - 1] ); // flag value comes from vs except for last point rs->f = (vs->f) & ( ~a32[vs->P - 1] ); // flag value comes from vs except for last point
// if distance from the active point just before 'dn'(in new state) to point P(in old state) is accurate, (vs->P) > 1 means that we have taken at least one point from old state // if distance from the active point just before 'dn'(in new state) to point P(in old state) is accurate, (vs->P) > 1 means that we have taken at least one point from old state
if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) { if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) {
// calculate distance from 2nd last point to last point in new state // calculate distance from 2nd last point to last point in new state
dis = vs->w[vs->P - 1] + mod(wn - w[P-1], M); dis = vs->w[vs->P - 1] + mod(wn - w[P-1], M);
if(dis < M) { // reset vs->P-1 bit to 0 if(dis < M) { // reset vs->P-1 bit to 0
rs->f |= (a32[vs->P - 1]); rs->f |= (a32[vs->P - 1]);
} }
} }
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
} }
} }
} }
} }
return v; return v;
} }
// Return template successor state whose descendent states will be right states for shuffle operation with this state // Return template successor state whose descendent states will be right states for shuffle operation with this state
stateGCPP* stateGCPP::sucState(){ stateGCPP* stateGCPP::sucState(){
short curReset, reset; // temp vars for keeping reset bit vector short curReset, reset; // temp vars for keeping reset bit vector
char count; // will contain #points in the new state char count; // will contain #points in the new state
char i,j; // counters char i,j; // counters
// iterate through all points right to left except the last point // iterate through all points right to left except the last point
curReset = transitions[ del[P-1] ].reset; curReset = transitions[ del[P-1] ].reset;
count = 1; //we have to take the last point, so initialize 'count' to 1 count = 1; //we have to take the last point, so initialize 'count' to 1
for(i=P-2; i >= 0; i--) { for(i=P-2; i >= 0; i--) {
reset = transitions[ del[i] ].reset; // reset bit vector for point i+1 reset = transitions[ del[i] ].reset; // reset bit vector for point i+1
if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has additional reset for some clock if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has additional reset for some clock
count++; count++;
curReset |= reset; curReset |= reset;
} }
} }
stateGCPP* vs = new stateGCPP(); // new template state stateGCPP* vs = new stateGCPP(); // new template state
vs->P = count; //#points vs->P = count; //#points
vs->L = count; // no non-trivial block is there vs->L = count; // no non-trivial block is there
vs->del = new char[count]; vs->del = new char[count];
vs->w = new char[count]; vs->w = new char[count];
vs->del[count-1] = del[P-1]; vs->del[count-1] = del[P-1];
vs->w[count-1] = w[P-1]; vs->w[count-1] = w[P-1];
// copy the necessary points into the template state // copy the necessary points into the template state
char lastindex = P-1; char lastindex = P-1;
short nf = 0; // flag variable for new state short nf = 0; // flag variable for new state
curReset = transitions[ del[P-1] ].reset; curReset = transitions[ del[P-1] ].reset;
for(i=P-2, j = count-2; i >= 0; i--) { for(i=P-2, j = count-2; i >= 0; i--) {
reset = transitions[ del[i] ].reset; // reset bit vector for point i+1 reset = transitions[ del[i] ].reset; // reset bit vector for point i+1
if(reset & (~curReset) & (~1) ) { // found a new necessary point, copy this point to new state if(reset & (~curReset) & (~1) ) { // found a new necessary point, copy this point to new state
vs->del[j] = del[i]; vs->del[j] = del[i];
vs->w[j] = w[i]; vs->w[j] = w[i];
if( !big(i+1, lastindex+1) ) //from current needy point to the last found needy point distance small if( !big(i+1, lastindex+1) ) //from current needy point to the last found needy point distance small
nf |= a32[j+1]; // distance (j+1->(j+2)) is small nf |= a32[j+1]; // distance (j+1->(j+2)) is small
curReset |= reset; curReset |= reset;
j--; j--;
lastindex = i; // this point is the last point selected till now lastindex = i; // this point is the last point selected till now
} }
} }
vs->f = nf; // copy flag information, no stack info is there till now for the template state vs->f = nf; // copy flag information, no stack info is there till now for the template state
return vs; return vs;
} }
// print a validity state // print a validity state
void stateGCPP::print() { void stateGCPP::print() {
char i; char i;
cout << endl << "Abstract state of the on the fly tree automata(TA):" << endl; cout << endl << "Abstract state of the on the fly tree automata(TA):" << endl;
cout << "\tPoints in the automaton:\n\t\t"; cout << "\tPoints in the automaton:\n\t\t";
cout << 1 ; cout << 1 ;
for(i=2; i <= L; i++) for(i=2; i <= L; i++)
cout << " " << int(i) ; cout << " " << int(i) ;
for(i=L+1; i <= P; i++) for(i=L+1; i <= P; i++)
cout << "----" << int(i) ; cout << "----" << int(i) ;
cout << endl; cout << endl;
cout << "\t\tL : " << int(L) << endl; cout << "\t\tL : " << int(L) << endl;
cout << "\tTransitions:"; cout << "\tTransitions:";
cout << "\t"; cout << "\t";
for(i=0; i < P; i++) for(i=0; i < P; i++)
cout << int(del[i]) << "\t"; cout << int(del[i]) << "\t";
cout << endl; cout << endl;
cout << "\tAccuracy: " << "\t "; cout << "\tAccuracy: " << "\t ";
for(i=1; i < P; i++) { for(i=1; i < P; i++) {
cout << ( (a32[i] & f) ? 1 : 0) << "\t "; cout << ( (a32[i] & f) ? 1 : 0) << "\t ";
} }
cout << endl; cout << endl;
cout << "\tTSM : \t"; cout << "\tTSM : \t";
cout << "\t"; cout << "\t";
for(i=0; i < P; i++) for(i=0; i < P; i++)
cout << int(w[i]) << "\t"; cout << int(w[i]) << "\t";
cout << endl; cout << endl;
cout << endl << endl; cout << endl << endl;
cout << "\tPush done at L : " << ( (f & 1)? 1 : 0 ) << endl; cout << "\tPush done at L : " << ( (f & 1)? 1 : 0 ) << endl;
cout << "\tPop done at R : " << ( (f & a3215) ? 1 : 0) << endl; cout << "\tPop done at R : " << ( (f & a3215) ? 1 : 0) << endl;
} }
// if this state is a final state // if this state is a final state
...@@ -593,216 +593,216 @@ bool stateGCPP::isFinal(){ ...@@ -593,216 +593,216 @@ bool stateGCPP::isFinal(){
if(L != 1) // there should not be any hanging point if(L != 1) // there should not be any hanging point
return false; return false;
// transition at first point must be 0-th transition // transition at first point must be 0-th transition
if( del[0] != 0) if( del[0] != 0)
return false; return false;
// there will not any push at the last transition // there will not any push at the last transition
if( isPush( del[P-1] ) ) if( isPush( del[P-1] ) )
return false; return false;
// target state of the transiton at point R should be the final state // target state of the transiton at point R should be the final state
if( transitions[del[P-1]].target != SF ) if( transitions[del[P-1]].target != SF )
return false; return false;
return true; return true;
} }
// return the partial run corresponding the tree automata state 'vs', ignore the hanging points // return the partial run corresponding the tree automata state 'vs', ignore the hanging points
// copy only transitions between L(left) and R(right) // copy only transitions between L(left) and R(right)
runCGPP* getRun(stateGCPP* vs) { runCGPP* getRun(stateGCPP* vs) {
runCGPP *pr = new runCGPP(); // new partial run stored in variable pr runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
pr->P = vs->P - vs->L + 1 ; // transitions in new partial run will be from left(L) point to right(R) point pr->P = vs->P - vs->L + 1 ; // transitions in new partial run will be from left(L) point to right(R) point
// allocate memory for transitions and tsm vlaues for new run // allocate memory for transitions and tsm vlaues for new run
pr->del = new char[pr->P]; pr->del = new char[pr->P];
pr->w = new char[pr->P]; pr->w = new char[pr->P];
// loopers : i used to index transition of the tree automata state and j is used to index trans in the run // loopers : i used to index transition of the tree automata state and j is used to index trans in the run
char i = vs->L - 1, j=0; char i = vs->L - 1, j=0;
// copy transitions and tsm values from earlier partial run to new partial run // copy transitions and tsm values from earlier partial run to new partial run
for(; i < (vs->P); i++, j++) { for(; i < (vs->P); i++, j++) {
pr->del[j] = vs->del[i]; pr->del[j] = vs->del[i];
pr->w[j] = vs->w[i]; pr->w[j] = vs->w[i];
} }
return pr; // return the new run return pr; // return the new run
} }
// GIVEN the current partial run, append the transition 'dn' with tsm value 'wn' // GIVEN the current partial run, append the transition 'dn' with tsm value 'wn'
runCGPP* runCGPP::addNext(char dn, char wn) { runCGPP* runCGPP::addNext(char dn, char wn) {
runCGPP *pr = new runCGPP(); // new partial run stored in variable pr runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
pr->P = P + 1; // #transitions in new partial run will be one more than the earlier pr->P = P + 1; // #transitions in new partial run will be one more than the earlier
// allocate memory for transitions and tsm vlaues for new run // allocate memory for transitions and tsm vlaues for new run
pr->del = new char[pr->P]; pr->del = new char[pr->P];
pr->w = new char[pr->P]; pr->w = new char[pr->P];
// copy transitions and tsm values from earlier partial run to new partial run // copy transitions and tsm values from earlier partial run to new partial run
for(char i=0; i < P; i++) { for(char i=0; i < P; i++) {
pr->del[i] = del[i]; pr->del[i] = del[i];
pr->w[i] = w[i]; pr->w[i] = w[i];
} }
pr->del[P] = dn; // add the new transition and tsm value to the last position of new partial run pr->del[P] = dn; // add the new transition and tsm value to the last position of new partial run
pr->w[P] = wn; pr->w[P] = wn;
return pr; // return the new run return pr; // return the new run
} }
// shuffle two partial runs and return the new partial run // shuffle two partial runs and return the new partial run
runCGPP* runCGPP::shuffle(runCGPP *s2) { runCGPP* runCGPP::shuffle(runCGPP *s2) {
runCGPP *pr = new runCGPP(); // new partial run stored in variable pr runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
/* rightmost transition of left state is equal to leftmost transition of right state /* rightmost transition of left state is equal to leftmost transition of right state
so new run will be concatenation of two runs and #points in new run is calculated as below*/ so new run will be concatenation of two runs and #points in new run is calculated as below*/
pr->P = P + (s2->P) - 1; pr->P = P + (s2->P) - 1;
// allocate memory for transitions and tsm vlaues for new run // allocate memory for transitions and tsm vlaues for new run
pr->del = new char[pr->P]; pr->del = new char[pr->P];
pr->w = new char[pr->P]; pr->w = new char[pr->P];
char i, j; // loopers char i, j; // loopers
// copy the transitions and tsm values of first run except for the last position // copy the transitions and tsm values of first run except for the last position
for(i=0, j=0; i < (P-1); i++, j++) { for(i=0, j=0; i < (P-1); i++, j++) {
pr->w[j] = w[i]; pr->w[j] = w[i];
pr->del[j] = del[i]; pr->del[j] = del[i];
} }
// copy the transitions and tsm values of 2nd run // copy the transitions and tsm values of 2nd run
for(i=0; i < (s2->P); i++, j++) { for(i=0; i < (s2->P); i++, j++) {
pr->w[j] = s2->w[i]; pr->w[j] = s2->w[i];
pr->del[j] = s2->del[i]; pr->del[j] = s2->del[i];
} }
return pr; // return the new run return pr; // return the new run
} }
// this will return a state with only 0-th transition with tsm value 0 // this will return a state with only 0-th transition with tsm value 0
stateGCPP* getZeroState() { stateGCPP* getZeroState() {
stateGCPP* vs = new stateGCPP(); stateGCPP* vs = new stateGCPP();
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->del = new char[1]; // memory allocation vs->del = new char[1]; // memory allocation
vs->w = new char[1]; vs->w = new char[1];
vs->del[0] = 0; // 0th transition has tsm value 0 vs->del[0] = 0; // 0th transition has tsm value 0
vs->w[0] = 0; vs->w[0] = 0;
return vs; return vs;
} }
// return unique string for last reset points of current state participating in a combine operation as a left state // return unique string for last reset points of current state participating in a combine operation as a left state
string stateGCPP::getKeyLeft() { string stateGCPP::getKeyLeft() {
string s = ""; // return this string string s = ""; // return this string
short resetSoFar, reset; // used for calculating union of resets short resetSoFar, reset; // used for calculating union of resets
s += del[P-1]; // include rightmost transition in the string s += del[P-1]; // include rightmost transition in the string
s += w[P-1]; // tsm value also be part of the key s += w[P-1]; // tsm value also be part of the key
char lastindex = P-1; // last index we have taken char lastindex = P-1; // last index we have taken
char nf = 0; // distance info char nf = 0; // distance info
char i=P-2; char i=P-2;
char j=0; char j=0;
resetSoFar = transitions[ del[P-1] ].reset; // set of clocks reset at rightmost point resetSoFar = transitions[ del[P-1] ].reset; // set of clocks reset at rightmost point
for(; i >= 0; i--) { for(; i >= 0; i--) {
reset = transitions[ del[i] ].reset; // take (i+1)-th point transition reset set reset = transitions[ del[i] ].reset; // take (i+1)-th point transition reset set
if( reset & (~resetSoFar) & (~1) ) { // if there are some new clocks reset at point (i+1) if( reset & (~resetSoFar) & (~1) ) { // if there are some new clocks reset at point (i+1)
s += del[i]; s += del[i];
s += w[i]; s += w[i];
resetSoFar |= reset; resetSoFar |= reset;
if( !big(i+1, lastindex+1) ) if( !big(i+1, lastindex+1) )
nf |= a32[j]; nf |= a32[j];
j++; j++;
} }
} }
s += nf; s += nf;
return s; // return the key return s; // return the key
} }
// return unique string for hanging points of a state participating in a combine operation as a right state // return unique string for hanging points of a state participating in a combine operation as a right state
string stateGCPP::getKeyRight() { string stateGCPP::getKeyRight() {
string s = ""; // return this string as a key for current state string s = ""; // return this string as a key for current state
// take the transition at point L and all hanging points // take the transition at point L and all hanging points
char nf = 0; // this contains distance information between points char nf = 0; // this contains distance information between points
s+= del[L-1]; // L-th poiint transition s+= del[L-1]; // L-th poiint transition
s+= w[L-1]; // L-th point tsm s+= w[L-1]; // L-th point tsm
char j = 0; // used for distance counter char j = 0; // used for distance counter
char i = L-2; // counter for points from right to left starting from L-1 point char i = L-2; // counter for points from right to left starting from L-1 point
for(; i >= 0; i--, j++) { for(; i >= 0; i--, j++) {
s += del[i]; s += del[i];
s += w[i]; s += w[i];
if(f & a32[i+1] ) if(f & a32[i+1] )
nf |= a32[j]; nf |= a32[j];
} }
// add distance info in the key // add distance info in the key
s+= nf; s+= nf;
return s; return s;
} }
// print a run as witness of the given TPDA if the language is non-empty // print a run as witness of the given TPDA if the language is non-empty
void runCGPP::print() { void runCGPP::print() {
short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps
cout << endl << "A run of the automation as a witness for the language to be non-empty.\nThe run given as a sequence of pairs (Transition, Time stamp) : " << endl; cout << endl << "A run of the automation as a witness for the language to be non-empty.\nThe run given as a sequence of pairs (Transition, Time stamp) : " << endl;
for(char i=0; i < P; i++) { for(char i=0; i < P; i++) {
if( w[i] < lt ) // if current time stamps less than last time stamps
ct = M + ct + (w[i] - lt);
else
ct = ct + (w[i] - lt);
lt = w[i];
cout << "(" << int(del[i]) << ", " << int(ct) << ".0" << "), ";
}
cout << endl << endl; if( w[i] < lt ) // if current time stamps less than last time stamps
ct = M + ct + (w[i] - lt);
else
ct = ct + (w[i] - lt);
lt = w[i];
cout << "(" << int(del[i]) << ", " << int(ct) << ".0" << "), ";
}
cout << endl << endl;
} }
// return a backtracking state with the info given in the parameters // return a backtracking state with the info given in the parameters
trackCGPP* getTrack(char t, int l, int r) { trackCGPP* getTrack(char t, int l, int r) {
trackCGPP* xrs = new trackCGPP(); trackCGPP* xrs = new trackCGPP();
xrs->type = t; // this string is empty because vs is atomic state xrs->type = t; // this string is empty because vs is atomic state
xrs->left = l; xrs->left = l;
xrs->right = r; // this value is 0 for atomic state vs xrs->right = r; // this value is 0 for atomic state vs
return xrs; return xrs;
} }
...@@ -810,225 +810,225 @@ trackCGPP* getTrack(char t, int l, int r) { ...@@ -810,225 +810,225 @@ trackCGPP* getTrack(char t, int l, int r) {
// if sm == "", this means. we are backtracking from the state reside in i-th index of main vector 'allStates' // if sm == "", this means. we are backtracking from the state reside in i-th index of main vector 'allStates'
// if sm != "", then sm string is the key for shuffle operation of the state reside in i-th index of allStates // if sm != "", then sm string is the key for shuffle operation of the state reside in i-th index of allStates
runCGPP* printRun(int i) { runCGPP* printRun(int i) {
stateGCPP* vs; // tree automata state variable stateGCPP* vs; // tree automata state variable
trackCGPP *bp; // back tracking state trackCGPP *bp; // back tracking state
vs = allStates[i].first; vs = allStates[i].first;
bp = allStates[i].second; bp = allStates[i].second;
runCGPP *rs, *rs1, *rs2; runCGPP *rs, *rs1, *rs2;
// if the i-th state is an atomic state // if the i-th state is an atomic state
if( (bp->type) == 0 ) { if( (bp->type) == 0 ) {
//cout << endl << i << ":"; //cout << endl << i << ":";
//vs->print(); //vs->print();
return getRun(vs); // return the run generated from atomic state return getRun(vs); // return the run generated from atomic state
} }
// if the considerted state is generated by an addNext operation from a state in the main vector // if the considerted state is generated by an addNext operation from a state in the main vector
else if( (bp->type) == 1 ) { else if( (bp->type) == 1 ) {
rs1 = printRun( bp->left ); rs1 = printRun( bp->left );
rs = rs1->addNext(vs->del[vs->P - 1], vs->w[vs->P - 1]); rs = rs1->addNext(vs->del[vs->P - 1], vs->w[vs->P - 1]);
//cout << endl << i << " : " << (bp->left); //cout << endl << i << " : " << (bp->left);
//vs->print(); //vs->print();
return rs; return rs;
} }
else{ else{
rs1 = printRun( bp->left); rs1 = printRun( bp->left);
rs2 = printRun(bp->right); rs2 = printRun(bp->right);
rs = rs1->shuffle(rs2); rs = rs1->shuffle(rs2);
//cout << endl << i << " : " << (bp->left) << ", " << (bp->right); //cout << endl << i << " : " << (bp->left) << ", " << (bp->right);
//vs->print(); //vs->print();
return rs; return rs;
} }
} }
// return true iff language recognized by the TPDA is empty // return true iff language recognized by the TPDA is empty
bool isEmptyGCPP() { bool isEmptyGCPP() {
/* /*
// we are assuming that non-emptiness for a TPDA means there is a non-trivial run(length of the run is non-zero) // we are assuming that non-emptiness for a TPDA means there is a non-trivial run(length of the run is non-zero)
if(SI == SF) { if(SI == SF) {
cout << "Initial state is same as final state " << endl; cout << "Initial state is same as final state " << endl;
return false; return false;
} }
*/ */
int count=0; //count point to the index of the state currently being processed in the vector 'allStates' declared as global variable int count=0; //count point to the index of the state currently being processed in the vector 'allStates' declared as global variable
int N=0; // total number of unique states generated so far int N=0; // total number of unique states generated so far
int i,j; // counters int i,j; // counters
string s; // temporary string for finding a unique key corresponding to a TA state, the key points to compatible states for combine operation string s; // temporary string for finding a unique key corresponding to a TA state, the key points to compatible states for combine operation
// pointer to a vector where each element is a pair of two things : (1) TA state and (2) back track info for that state // pointer to a vector where each element is a pair of two things : (1) TA state and (2) back track info for that state
//vector<pair<stateGCPP*, trackCGPP*> > *vshuffle; //vector<pair<stateGCPP*, trackCGPP*> > *vshuffle;
vector<stateGCPP*> v; // temporary vector for keeping a set of states vector<stateGCPP*> v; // temporary vector for keeping a set of states
stateGCPP *rs, *vs, *vs1, *vs2; // some state variables stateGCPP *rs, *vs, *vs1, *vs2; // some state variables
trackCGPP *xrs; // back propagarion state variable trackCGPP *xrs; // back propagarion state variable
runCGPP *prs; // variable for partial run of the TPDA runCGPP *prs; // variable for partial run of the TPDA
char *del, *w, P, L; // variables for keeping current state transitions, tsm values, #points and left point char *del, *w, P, L; // variables for keeping current state transitions, tsm values, #points and left point
short f; // flag variable short f; // flag variable
// pushl=1 iff push at L, pushr=1 iff push at R, popl=1 iff pop at L , popr=1 iff pop at R, ppDone : iff push-pop done // pushl=1 iff push at L, pushr=1 iff push at R, popl=1 iff pop at L , popr=1 iff pop at R, ppDone : iff push-pop done
bool pushl, pushr, popl, popr, ppDone; bool pushl, pushr, popl, popr, ppDone;
// for a given key size1 is #(left states) participated in combine operation and size2 is #(right states) participated in combine operation // for a given key size1 is #(left states) participated in combine operation and size2 is #(right states) participated in combine operation
int size1, size2; int size1, size2;
vs = getZeroState(); // 'vs' state is the first Tree automata state with only 0-th transition with tsm value 0 vs = getZeroState(); // 'vs' state is the first Tree automata state with only 0-th transition with tsm value 0
identity(vs); // insert this state in the hashmap identity(vs); // insert this state in the hashmap
// first empty string "" and third 0 denotes that this TA state is atomic // first empty string "" and third 0 denotes that this TA state is atomic
xrs = getTrack(0, -1, -1); // create a backtracking state for generating partial run xrs = getTrack(0, -1, -1); // create a backtracking state for generating partial run
allStates.push_back( make_pair(vs, xrs) ); // insert the state into the main vector along with its back tracking information allStates.push_back( make_pair(vs, xrs) ); // insert the state into the main vector along with its back tracking information
N++; // increment #states N++; // increment #states
// iterate through all the generated states and process them to generate new state // iterate through all the generated states and process them to generate new state
for(count = 0; count < N; count++) { for(count = 0; count < N; count++) {
if( count %5000 == 0 ) // Below of this string, #states will be shown
cout << "#States" << endl;
if( (count % 100) == 0 || count <= 200) // print state number currently being processed(note : all numbers will not be printed)
cout << count << endl;
rs = allStates[count].first; // get the state at index count, process this state now
// printing the current state information and its parents
//rs->print();
xrs = allStates[count].second;
// priting parents :
// shuffle : left and right index shows left and right parent
// add : first index is the real parent, second index is -1
// atomic(generated by sucState()) : right index is the real parent
// atomic(0-th state) : both index are -1
//cout << "Parents: " << (xrs->left) << ", " << (xrs->right) << endl << "--------------" << endl;
// store current state info in variables for shortcut use
del = rs->del;
P = rs->P;
L = rs->L;
f = rs->f;
pushl = isPush( del[L - 1] ); // pushl = 1 iff there is a push at L
pushr = isPush( del[P - 1] ); // pushr = 1 iff there is a push at R
popl = isPop( del[L - 1] ); // popl = 1 iff there is a pop at L
popr = isPop( del[P - 1] ); // popr = 1 iff there is a pop at R
ppDone = (f & 1) && (f & a3215) ; // if push at L and pop at R is done in rs
// state rs is eligible for participating in combine operation as a left state(rs should have a non-trivial block)
if( L < P && pushr ) {
for(i=0; i < count; i++) {
// shuffle, considering rs as left state
vs = rs->shuffle( allStates[i].first );
if(vs != NULL) { // if new state is valid
if( identity(vs) ) {
xrs = getTrack(2, count, i); // key for the new state
allStates.push_back( make_pair(vs, xrs) );
N++;
if( vs->isFinal() ) {
vs->print();
prs = printRun(N-1);
prs->print();
//cout << "N :" << N << endl;
return false;
}
}
}
}
// we are creating a template state(vs) from rs, 'vs' generate some states later, those states will participate in combine operation with state rs
vs = rs->sucState(); // get the template state
if( identity(vs) ) { // if we have not found this template earlier
xrs = getTrack(0, -1, count); // back track info for vs which is a atomic state
// insert the state into the main vector along with its back tracking information
allStates.push_back( make_pair(vs, xrs) );// note : every state must be in the main vector
N++; // increment #states
}
}
// state rs is eligible for participating in combine operation as a right state
else if( L < P && pushl && popr && ppDone) {
for(i=0; i < count; i++) {
// shuffle, considering rs as right state
vs = (allStates[i].first)->shuffle(rs);
if(vs != NULL) { // if new state is valid
if( identity(vs) ) {
xrs = getTrack(2, i, count); // key for the new state
allStates.push_back( make_pair(vs, xrs) );
N++;
if( vs->isFinal() ) {
vs->print();
prs = printRun(N-1);
prs->print();
//cout << "N :" << N << endl;
return false;
}
}
}
}
}
//state rs might be eligible for adding a new transition to its right
else{
v = rs->addNextTPDA(); // get set of states after doing the add operation
for(i=0; i < v.size(); i++) {
if( identity(v[i]) ) { // if the i-th state is new
xrs = getTrack(1, count, -1);
allStates.push_back(make_pair( v[i], xrs ) );
N++;
if( v[i]->isFinal() ) { // if this state is final
v[i]->print();
prs = printRun(N-1);
prs->print();
//cout << "N :" << N << endl;
return false;
}
}
}
}
}
// vs1 = (allStates[8]).first; if( count %5000 == 0 ) // Below of this string, #states will be shown
// vs1->print(); cout << "#States" << endl;
// vs2 = vs1->sucState();
//
// vs2->print();
// vs = vs1->shuffle(vs2);
// vs->print();
//v = (allStates[2].first)->addNextTPDA();
// cout << v.size() << endl;
// for(i=0;i < v.size(); i++)
// v[i]->print();
//cout << "\"" << (allStates[1].first)->shuffleCheck((allStates[6].first)) << "\"";
if( (count % 100) == 0 || count <= 200) // print state number currently being processed(note : all numbers will not be printed)
cout << count << endl;
return true;
rs = allStates[count].first; // get the state at index count, process this state now
// printing the current state information and its parents
//rs->print();
xrs = allStates[count].second;
// priting parents :
// shuffle : left and right index shows left and right parent
// add : first index is the real parent, second index is -1
// atomic(generated by sucState()) : right index is the real parent
// atomic(0-th state) : both index are -1
//cout << "Parents: " << (xrs->left) << ", " << (xrs->right) << endl << "--------------" << endl;
// store current state info in variables for shortcut use
del = rs->del;
P = rs->P;
L = rs->L;
f = rs->f;
pushl = isPush( del[L - 1] ); // pushl = 1 iff there is a push at L
pushr = isPush( del[P - 1] ); // pushr = 1 iff there is a push at R
popl = isPop( del[L - 1] ); // popl = 1 iff there is a pop at L
popr = isPop( del[P - 1] ); // popr = 1 iff there is a pop at R
ppDone = (f & 1) && (f & a3215) ; // if push at L and pop at R is done in rs
// state rs is eligible for participating in combine operation as a left state(rs should have a non-trivial block)
if( L < P && pushr ) {
for(i=0; i < count; i++) {
// shuffle, considering rs as left state
vs = rs->shuffle( allStates[i].first );
if(vs != NULL) { // if new state is valid
if( identity(vs) ) {
xrs = getTrack(2, count, i); // key for the new state
allStates.push_back( make_pair(vs, xrs) );
N++;
if( vs->isFinal() ) {
vs->print();
prs = printRun(N-1);
prs->print();
//cout << "N :" << N << endl;
return false;
}
}
}
}
// we are creating a template state(vs) from rs, 'vs' generate some states later, those states will participate in combine operation with state rs
vs = rs->sucState(); // get the template state
if( identity(vs) ) { // if we have not found this template earlier
xrs = getTrack(0, -1, count); // back track info for vs which is a atomic state
// insert the state into the main vector along with its back tracking information
allStates.push_back( make_pair(vs, xrs) );// note : every state must be in the main vector
N++; // increment #states
}
}
// state rs is eligible for participating in combine operation as a right state
else if( L < P && pushl && popr && ppDone) {
for(i=0; i < count; i++) {
// shuffle, considering rs as right state
vs = (allStates[i].first)->shuffle(rs);
if(vs != NULL) { // if new state is valid
if( identity(vs) ) {
xrs = getTrack(2, i, count); // key for the new state
allStates.push_back( make_pair(vs, xrs) );
N++;
if( vs->isFinal() ) {
vs->print();
prs = printRun(N-1);
prs->print();
//cout << "N :" << N << endl;
return false;
}
}
}
}
}
//state rs might be eligible for adding a new transition to its right
else{
v = rs->addNextTPDA(); // get set of states after doing the add operation
for(i=0; i < v.size(); i++) {
if( identity(v[i]) ) { // if the i-th state is new
xrs = getTrack(1, count, -1);
allStates.push_back(make_pair( v[i], xrs ) );
N++;
if( v[i]->isFinal() ) { // if this state is final
v[i]->print();
prs = printRun(N-1);
prs->print();
//cout << "N :" << N << endl;
return false;
}
}
}
}
}
// vs1 = (allStates[8]).first;
// vs1->print();
// vs2 = vs1->sucState();
//
// vs2->print();
// vs = vs1->shuffle(vs2);
// vs->print();
//v = (allStates[2].first)->addNextTPDA();
// cout << v.size() << endl;
// for(i=0;i < v.size(); i++)
// v[i]->print();
//cout << "\"" << (allStates[1].first)->shuffleCheck((allStates[6].first)) << "\"";
return true;
} }
......
src/tpdaZone.cpp
View file @ e4eea6fc
...@@ -11,11 +11,11 @@ using namespace std; ...@@ -11,11 +11,11 @@ using namespace std;
// Considering w is edge weight matrix of a graph, find if there is any negative cycle in the graph after applying floyd warshal algorithm // Considering w is edge weight matrix of a graph, find if there is any negative cycle in the graph after applying floyd warshal algorithm
bool isNegCycle(short **w, bool **open, int n) { bool isNegCycle(short **w, bool **open, int n) {
for(char i=0; i < n; i++) { for(char i=0; i < n; i++) {
if( w[i][i] < 0 || open[i][i] ) // if diagonal weights are strictly less than zero if( w[i][i] < 0 || open[i][i] ) // if diagonal weights are strictly less than zero
return true; return true;
} }
return false; return false;
} }
...@@ -26,48 +26,48 @@ bool **open1, **open2; // temporary variable for storing some edge is open inter ...@@ -26,48 +26,48 @@ bool **open1, **open2; // temporary variable for storing some edge is open inter
// apply all pair shortest path algorithms for the graph with n number of nodes(edge weights given in 1d array w) // apply all pair shortest path algorithms for the graph with n number of nodes(edge weights given in 1d array w)
void allPairSP(int n) { void allPairSP(int n) {
char i,j,k; // counters char i,j,k; // counters
// n iterations for floyd warshal algorithm // n iterations for floyd warshal algorithm
for(k=0; k < n; k++) { for(k=0; k < n; k++) {
for(i=0; i < n; i++) { for(i=0; i < n; i++) {
for(j=0; j < n; j++){ for(j=0; j < n; j++){
if(k & 1) { // if k is odd, transfer weights from WT2 to WT1 if(k & 1) { // if k is odd, transfer weights from WT2 to WT1
if( ( WT2[i][k] + WT2[k][j] ) < WT2[i][j] ) { // if using node k, we update distance from i to j if( ( WT2[i][k] + WT2[k][j] ) < WT2[i][j] ) { // if using node k, we update distance from i to j
WT1[i][j] = WT2[i][k] + WT2[k][j]; WT1[i][j] = WT2[i][k] + WT2[k][j];
open1[i][j] = open2[i][k] || open2[k][j] ; open1[i][j] = open2[i][k] || open2[k][j] ;
} }
else if( ( WT2[i][k] + WT2[k][j] ) == WT2[i][j]) { // if any distance is open, then the new distance is also open else if( ( WT2[i][k] + WT2[k][j] ) == WT2[i][j]) { // if any distance is open, then the new distance is also open
WT1[i][j] = WT2[i][j]; WT1[i][j] = WT2[i][j];
open1[i][j] = open2[i][k] || open2[k][j] || open2[i][j] ; open1[i][j] = open2[i][k] || open2[k][j] || open2[i][j] ;
} }
else { else {
WT1[i][j] = WT2[i][j]; WT1[i][j] = WT2[i][j];
open1[i][j] = open2[i][j] ; open1[i][j] = open2[i][j] ;
} }
} }
else{ // if k is even , transfer weights from WT1 to WT2 else{ // if k is even , transfer weights from WT1 to WT2
if( ( WT1[i][k] + WT1[k][j] ) < WT1[i][j] ) { if( ( WT1[i][k] + WT1[k][j] ) < WT1[i][j] ) {
WT2[i][j] = WT1[i][k] + WT1[k][j]; WT2[i][j] = WT1[i][k] + WT1[k][j];
open2[i][j] = open1[i][k] || open1[k][j] ; open2[i][j] = open1[i][k] || open1[k][j] ;
} }
else if( ( WT1[i][k] + WT1[k][j] ) == WT1[i][j]) { else if( ( WT1[i][k] + WT1[k][j] ) == WT1[i][j]) {
WT2[i][j] = WT1[i][j]; WT2[i][j] = WT1[i][j];
open2[i][j] = open1[i][k] || open1[k][j] || open1[i][j] ; open2[i][j] = open1[i][k] || open1[k][j] || open1[i][j] ;
} }
else{ else{
WT2[i][j] = WT1[i][j]; WT2[i][j] = WT1[i][j];
open2[i][j] = open1[i][j] ; open2[i][j] = open1[i][j] ;
} }
} }
} }
} }
} }
} }
...@@ -81,208 +81,256 @@ vector<pair<stateZone*, trackZone*> > allStatesZone; ...@@ -81,208 +81,256 @@ vector<pair<stateZone*, trackZone*> > allStatesZone;
// return 1 iff state vs was not found earlier or vs is new state // return 1 iff state vs was not found earlier or vs is new state
bool identity(stateZone *vs) { bool identity(stateZone *vs) {
string os=""; // output string string os=""; // output string
short i; // looper short i; // looper
short P = vs->P; short P = vs->P;
for( i=0; i < P; i++ ) { // add transitions to the string os for( i=0; i < P; i++ ) { // add transitions to the string os
//cout << "i:" << int(i) << endl; //cout << "i:" << int(i) << endl;
os += (vs->del[i]); os += (vs->del[i]);
} }
P = P*P - P; P = P*P - P;
//cout << P << endl; //cout << P << endl;
for(i=0; i < P; i++ ){ for(i=0; i < P; i++ ){
os += char(vs->w[i]); os += char(vs->w[i]);
os += char( (vs->w[i]) >> 8 ) ; //why this? os += char( (vs->w[i]) >> 8 ) ; //why this?
} }
//cout << "ILIAS" << int(vs->f) << endl; //cout << "ILIAS" << int(vs->f) << endl;
os += char(vs->f); // L is also included in f os += char(vs->f); // L is also included in f
// using hashmap : if os key was not there then mapGCPP[os]==false // using hashmap : if os key was not there then mapGCPP[os]==false
if( mapZone[os] ) // 'os' is there in hashmap if( mapZone[os] ) // 'os' is there in hashmap
return false; return false;
else{ // 'os' is not there in hashmap else{ // 'os' is not there in hashmap
mapZone[os] = true; mapZone[os] = true;
return true;; return true;;
} }
} }
// reduce the #points after shuffle by using forget operation if possible and return the new state // reduce the #points after shuffle by using forget operation if possible and return the new state
stateZone* stateZone::reduceShuffle(stateZone* s2) { stateZone* stateZone::reduceShuffle(stateZone* s2) {
char *del2 = s2->del, *w2 = s2->w;
char P2 = s2->P;
short f2 = s2->f;
short L = f&127;
short L2 = f2 & 127;
short curReset, reset, tempReset; // temp variables to keep reset for a range of points
char count=0; // used for storing #points in new state
char i, j; // loopers
// we have to take all the points from s2->L+1 to s2->P, point s2->L may not be there
// all the points from 1 to L of first state will be there in new state, last point P may not be there
// take union of resets for points between s2->L+1(including) and s2->P(including)
curReset = 0;
for(i=L2; i < P2; i++)
curReset |= ( transitions[ del2[i] ].reset ); //this contain union of the resets in the second state
tempReset = curReset; // store this value for later use
for( i=P-1; i >= L; i--) {
reset = ( transitions[ del[i] ].reset );
// there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
//reset at (i+1) point of 1st state which has not reset to any of its right points for both state
if( reset & (~curReset) & (~1) ) { // (~1) : ignore the 0-th bit, used for stack operation
count++; // this point should be in new state, so increase the counter
curReset |= reset; // union reset set at this point with earlier set
}
}
// addition of 'L' below comes from the fact that all point from 1 to L of first state is there in new state
// (s2->P - s2-> L) comes from : all points s2->L+1 to s2->P are there in new state
count += L + (P2 - L2); // #points in new state
stateZone *vs = new stateZone(); // new TA state
vs->del = new char[count]; // allocate memory
vs->w = new char[count*(count-1)]; //this will hold the matrix without the diagonal element
vs->f = f; //f contains the push complete command flag bit along with the value of L
//short nf = 0; // initially flag is zero
//short dis; // distance variable
/*copying the transitions for both the states to this new state*/
j = count - 1; // index of the rightmost point of new state
// Here we are copying points from s2->L+1 to s2->P of 2nd state to new state
for(i=P2 - 1; i >= L2; i--, j--) {
vs->del[j] = del2[i]; // copy (i+1)-th transition to (j+1) transition of new state
//vs->w[j] = w2[i]; // copy (i+1)-th tsm to (j+1) tsm of new state
//for zone the W contains the details of matrix which we need to copy and check for negetive cycle
// if distance (i+1)->(i+2) of 2nd state is accurate, then distance (j+1)->(j+2) of new state is accurate
//if( f2 & a32[i+1] )
// nf |= a32[j+1];
}
// Here we are copying points from 1 to L-1 of 1st state to new state
for(j=0; j < (L-1); j++) {
vs->del[j] = del[j];
//vs->w[j] = w[j];
// same reasons as above
// if distance (j+1)->(j+2) of 1st state is accurate, then distance (j+1)->(j+2) of new state is accurate
//nf |= ( f & a32[j+1] ); // here f means some thing different
}
//copy the point L, doing it separately because of the flag variable which is not applicable for L-th point
vs->del[L-1] = del[L-1];
//vs->w[L-1] = w[L-1]; w doesnot contains time stamps any more it contains the matrix
/*copying transition details done*/
//Here goes the logic of creating the matrix altogether with given values.
/*copying matrix details to the new state*/
// copy weights of first state to WT1
for(i=0; i < P; i++) {
for(j=0; j < P; j++) {
if(i==j) { //same transition points
WT1[i][i] = 0;
open1[i][i] = false;
}
else if(i < j) {
WT1[i][j] = w[index(i, j, P)] & (~a32[15]); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
else
open1[i][j] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index(i, j, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] )
open1[i][j] = true;
else
open1[i][j] = false;
}
}
}
//copy weights of second state to WT1
// copy weights of current state to WT1
for(i=P; i < count; i++) {
for(j=P; j < count; j++) {
if(i==j) { //same transition points
WT1[i][i] = 0;
open1[i][i] = false;
}
else if(i < j) {
WT1[i][j] = w[index((i-P), (j-P), P2)] & (~a32[15]); // 15-TH bit is used for open or not
if( w[index((i-P), (j-P), P2)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
else
open1[i][j] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index((i-P), (j-P), P2)] & (~a32[15]) ); // 15-TH bit is used for open or not
if( w[index((i-P), (j-P), P2)] & a32[15] )
open1[i][j] = true;
else
open1[i][j] = false;
}
}
}
//both the matrices is copied to the variable,
//here P = L2 Now we have to check the check points and their
//recent reset points
//now there are some hangng edges which are
// Now we watch out for points from L+1 to P of 1st state
char lastindex = P;// last index of the point we have taken so far, although P might not be included
curReset = tempReset; //get the union of resets for points between s2->L+1 and s2->P
int lb,ub,openl,openu;
// current indices j of new state we have to take care
j = (count - 1) - (P2 - L2);//this is the start of hanging points of state 2
//for(i=P-1; i >= L; i--) { //iterating on the points of the first state
// current point reset set
for(int k = L2 -1; k < count ; k++) //iterating through the points of second state to find any clock constraint check
{
for(int x=1; x <= X; x++) { // iterate for every clocks
if( isChecked(x, k) ) { // if there is a constraint for clock x in the transition k of second state
lb = transitions[k].lbs[x];
ub = transitions[k].ubs[x];
openl = (transitions[k].openl) & a32[x]; // lower bound for clock x is open or not
openu = (transitions[k].openu) & a32[x];
for(i=P-1; i >= L; i--) { // find reset point for clock x in the first state
reset = ( transitions[ del[i] ].reset );
if( reset & (~curReset) & (~1) && isReset(x, del[i]) ) { // if current point has more reset then seen earlier
//if the current
vs->del[j] = del[i]; //copy the transition number
//if( ) { // if clock x is reset at point i+1
// tighten the lower and upper bounds
if( (-lb) < WT1[P][i] ) {
WT1[P][i] = -lb;
open1[P][i] = (openl & a32[x]);
}
else if( (-lb) == WT1[i][P] )
open1[P][i] |= (openl & a32[x]);
if(ub != INF) {
if(ub < WT1[i][P]) {
WT1[i][P] = ub;
open1[i][P] = (openu & a32[x]);
}
else if( ub == WT1[i][P] )
open1[i][P] |= (openu & a32[x]);
}
i = -1;
}
curReset |= reset;
j--;
lastindex = i;
}
}
}
}
/* //vs->w[j] = w[i];
// if( lastindex == P ) { // if (i+1) is the first point we are considering after starting the loop
// // In if : first check is for accuracy check from L to P of left state
// // In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen
// if( !big(i+1, P) && ( i == (P-1) || (f2 & a32[L2]) ) ) {
// dis = dist(i+1, P) + mod( w2[L2] - w[P-1], M);
// if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
// nf |= a32[j+1];
// }
// }
// else {
// if( !big(i+1, lastindex+1) )
// nf |= a32[j+1];
// } */
vs->P = count; // #points in new state
return vs;
}
char *del2 = s2->del, *w2 = s2->w;
char P2 = s2->P;
short f2 = s2->f;
short L = f&127;
short L2 = f2 & 127;
short curReset, reset, tempReset; // temp variables to keep reset for a range of points
char count=0; // used for storing #points in new state
char i, j; // loopers
// we have to take all the points from s2->L+1 to s2->P, point s2->L may not be there
// all the points from 1 to L of first state will be there in new state, last point P may not be there
// take union of resets for points between s2->L+1(including) and s2->P(including)
curReset = 0;
for(i=L2; i < P2; i++)
curReset |= ( transitions[ del2[i] ].reset ); //this contain union of the resets in the second state
tempReset = curReset; // store this value for later use
for( i=P-1; i >= L; i--) {
reset = ( transitions[ del[i] ].reset );
// there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
//reset at (i+1) point of 1st state which has not reset to any of its right points for both state
if( reset & (~curReset) & (~1) ) { // (~1) : ignore the 0-th bit, used for stack operation
count++; // this point should be in new state, so increase the counter
curReset |= reset; // union reset set at this point with earlier set
}
}
// addition of 'L' below comes from the fact that all point from 1 to L of first state is there in new state
// (s2->P - s2-> L) comes from : all points s2->L+1 to s2->P are there in new state
count += L + (P2 - L2); // #points in new state
stateZone *vs = new stateZone(); // new TA state
vs->del = new char[count]; // allocate memory
vs->w = new char[count*(count-1)]; //this will hold the matrix without the diagonal element
vs->f = f; //f contains the push complete command flag bit along with the value of L
//short nf = 0; // initially flag is zero
//short dis; // distance variable
/*copying the transitions for both the states to this new state*/
j = count - 1; // index of the rightmost point of new state
// Here we are copying points from s2->L+1 to s2->P of 2nd state to new state
for(i=P2 - 1; i >= L2; i--, j--) {
vs->del[j] = del2[i]; // copy (i+1)-th transition to (j+1) transition of new state
//vs->w[j] = w2[i]; // copy (i+1)-th tsm to (j+1) tsm of new state
//for zone the W contains the details of matrix which we need to copy and check for negetive cycle
// if distance (i+1)->(i+2) of 2nd state is accurate, then distance (j+1)->(j+2) of new state is accurate
//if( f2 & a32[i+1] )
// nf |= a32[j+1];
}
// Here we are copying points from 1 to L-1 of 1st state to new state
for(j=0; j < (L-1); j++) {
vs->del[j] = del[j];
//vs->w[j] = w[j];
// same reasons as above
// if distance (j+1)->(j+2) of 1st state is accurate, then distance (j+1)->(j+2) of new state is accurate
//nf |= ( f & a32[j+1] ); // here f means some thing different
}
//copy the point L, doing it separately because of the flag variable which is not applicable for L-th point
vs->del[L-1] = del[L-1];
//vs->w[L-1] = w[L-1]; w doesnot contains time stamps any more it contains the matrix
/*copying transition details done*/
//Here goes the logic of creating the matrix altogether with given values.
/*copying matrix details to the new state*/
// copy weights of first state to WT1
for(i=0; i < P; i++) {
for(j=0; j < P; j++) {
if(i==j) { //same transition points
WT1[i][i] = 0;
open1[i][i] = false;
}
else if(i < j) {
WT1[i][j] = w[index(i, j, P)] & (~a32[15]); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
else
open1[i][j] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index(i, j, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] )
open1[i][j] = true;
else
open1[i][j] = false;
}
}
}
//copy weights of second state to WT1
// copy weights of current state to WT1
for(i=P; i < count; i++) {
for(j=P; j < count; j++) {
if(i==j) { //same transition points
WT1[i][i] = 0;
open1[i][i] = false;
}
else if(i < j) {
WT1[i][j] = w[index((i-P), (j-P), P2)] & (~a32[15]); // 15-TH bit is used for open or not
if( w[index((i-P), (j-P), P2)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
else
open1[i][j] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index((i-P), (j-P), P2)] & (~a32[15]) ); // 15-TH bit is used for open or not
if( w[index((i-P), (j-P), P2)] & a32[15] )
open1[i][j] = true;
else
open1[i][j] = false;
}
} // one accuracy we yet have to compute which starts from L-th point of first state
}
//both the matrices is copied to the variable,
//here P = L2 Now we have to check the check points and their
//recent reset points
//now there are some hangng edges which are
// Now we watch out for points from L+1 to P of 1st state
char lastindex = P;// last index of the point we have taken so far, although P might not be included
curReset = tempReset; //get the union of resets for points between s2->L+1 and s2->P
// current indices j of new state we have to take care
j = (count - 1) - (P2 - L2);//this is the start of hanging points of state 2
for(i=P-1; i >= L; i--) { //iterating on the points of the first state
reset = ( transitions[ del[i] ].reset ); // current point reset set
if( reset & (~curReset) & (~1) ) { // if current point has more reset then seen earlier
//if the current
vs->del[j] = del[i]; //copy the transition number
/* //vs->w[j] = w[i];
// if( lastindex == P ) { // if (i+1) is the first point we are considering after starting the loop
// // In if : first check is for accuracy check from L to P of left state
// // In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen
// if( !big(i+1, P) && ( i == (P-1) || (f2 & a32[L2]) ) ) {
// dis = dist(i+1, P) + mod( w2[L2] - w[P-1], M);
// if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
// nf |= a32[j+1];
// }
// }
// else {
// if( !big(i+1, lastindex+1) )
// nf |= a32[j+1];
// } */
curReset |= reset;
j--;
lastindex = i;
}
}
// one accuracy we yet have to compute which starts from L-th point of first state
// if( lastindex == P ) { // if we have not taken any point from L+1 to P of 1st state // if( lastindex == P ) { // if we have not taken any point from L+1 to P of 1st state
// // In if : first check is for accuracy check from L to P of left state // // In if : first check is for accuracy check from L to P of left state
// // In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen // // In if : second check is for cheking accuracy from L2 to L2+1 of right state, L2 is not choosen
...@@ -305,818 +353,817 @@ stateZone* stateZone::reduceShuffle(stateZone* s2) { ...@@ -305,818 +353,817 @@ stateZone* stateZone::reduceShuffle(stateZone* s2) {
// nf |= a3215; // pop at right(R) is done // nf |= a3215; // pop at right(R) is done
// //
// vs->f = nf; // add the flag variable also // vs->f = nf; // add the flag variable also
vs->P = count; // #points in new state
return vs;
}
// check if shuffle of this state with s2 is possible // check if shuffle of this state with s2 is possible
bool stateZone::shuffleCheck(stateZone *s2) { bool stateZone::shuffleCheck(stateZone *s2) {
if( (f&127) == P || ((s2->f)&127) == ((s2->f)&127) ) // both state should have non-trival block if( (f&127) == P || ((s2->f)&127) == ((s2->f)&127) ) // both state should have non-trival block
return false; return false;
if( !isPush(del[P-1]) ) // there should be a push at last transition of left state if( !isPush(del[P-1]) ) // there should be a push at last transition of left state
return false; return false;
// there should be a push at L of s2 and pop at R of s2, note : del[P-1] = del2[P2-1] // there should be a push at L of s2 and pop at R of s2, note : del[P-1] = del2[P2-1]
if( !isPush( s2->del[((s2->f)&127)-1] ) || !isPop( s2->del[((s2->f)&127)-1] ) ) if( !isPush( s2->del[((s2->f)&127)-1] ) || !isPop( s2->del[((s2->f)&127)-1] ) )
return false; return false;
//why this condition? //why this condition?
//if( !( (s2->f) & 1 ) || !( (s2->f) & a3215 ) ) // push-pop edge should be connected in right state //if( !( (s2->f) & 1 ) || !( (s2->f) & a3215 ) ) // push-pop edge should be connected in right state
// return false; // return false;
if( getKeyLeft() != (s2->getKeyRight() ) ) if( getKeyLeft() != (s2->getKeyRight() ) )
return false; return false;
return true; return true;
} }
// shuffle of this state with state s2 and return the new state // shuffle of this state with state s2 and return the new state
stateZone* stateZone::shuffle(stateZone *s2){ // shuffle with state s2 stateZone* stateZone::shuffle(stateZone *s2){ // shuffle with state s2
if(! shuffleCheck(s2) ) if(! shuffleCheck(s2) )
return NULL; return NULL;
return reduceShuffle(s2); return reduceShuffle(s2);
} }
/* /*
// add transition 'dn' to current state and then forget some points if possible, return the new state // add transition 'dn' to current state and then forget some points if possible, return the new state
stateGCPP* stateGCPP::reduce(char dn){ stateGCPP* stateGCPP::reduce(char dn){
short reset; // variable for reset bit vector short reset; // variable for reset bit vector
short nf = 0; // flag variable for new state short nf = 0; // flag variable for new state
char count = 0; // #points in new state char count = 0; // #points in new state
char i; // looper char i; // looper
short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn' short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
for( i=P-1; i >= L; i-- ) { for( i=P-1; i >= L; i-- ) {
reset = transitions[ del[i] ].reset; // reset at transition at the (i+1)-th point 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 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' curReset |= reset; // the 'curReset' will have more bit with value '1'
count++; // we have to take (i+1)-th point count++; // we have to take (i+1)-th point
} }
} }
// all the hanging points and point L and point for transition 'dn' also be there // all the hanging points and point L and point for transition 'dn' also be there
count += (L+1); // number of points in new state count += (L+1); // number of points in new state
// pointer to the new state // pointer to the new state
stateGCPP* vs = new stateGCPP(); stateGCPP* vs = new stateGCPP();
vs->P = count; // #points in new state vs->P = count; // #points in new state
vs->L = L; // left point remain same vs->L = L; // left point remain same
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
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];
} }
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
nf |= ( f & a32[i] ); nf |= ( f & a32[i] );
} }
vs->del[count-1] = dn; // trans at last point, till now we don't know the weight vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
char lastindex = P; // 'lastindex' used for accuracy between two points in new state char lastindex = P; // 'lastindex' used for accuracy between two points in new state
char firstindex; char firstindex;
char j = count-2; // assgin trans and tsm from index count-2 upto L char j = count-2; // assgin trans and tsm from index count-2 upto L
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'
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
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
} }
// store the accuracy from last point(active in new state) before dn and P in i+1-th bit of nf // 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] // 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 // we yet don't know the tsm for 'dn', so full calculation is not done in this function
else{ else{
firstindex = i; firstindex = i;
if( !big(i+1, P) ) if( !big(i+1, P) )
nf |= a32[j+1]; nf |= a32[j+1];
vs->w[count-1] = dist(i+1, P); vs->w[count-1] = dist(i+1, P);
} }
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
} }
} }
// 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) ) {
// vs->w[count-1] = dist(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 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 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] // 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 // 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** else{ // if you have not choosed any point in the middle starting from point P**
if( !big(L, P) ) if( !big(L, P) )
nf |= a32[L]; nf |= a32[L];
vs->w[count-1] = dist(L, P); vs->w[count-1] = dist(L, P);
} }
if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively if(isPop(dn) ) // if dn has a pop, then push-pop has been added to L and R repectively
nf |= (1 | a3215) ; nf |= (1 | a3215) ;
else else
nf |= (f & 1) ; // previous push information remain same nf |= (f & 1) ; // previous push information remain same
// last distance accuracy // last distance accuracy
vs->f = nf; // add partial flag variable to new state vs->f = nf; // add partial flag variable to new state
return vs; // return the partially new state, **** last tsm missing with partial nf as given return vs; // return the partially new state, **** last tsm missing with partial nf as given
} }
*/ */
// Add all possible upcoming transition just after the last transition of this state if all clock and stack constraints are satisfied // Add all possible upcoming transition just after the last transition of this state if all clock and stack constraints are satisfied
stateZone* stateZone::addNextTPDA(char dn) { stateZone* stateZone::addNextTPDA(char dn) {
char i, j; // counters char i, j; // counters
char x; // used for clocks char x; // used for clocks
char L = f & 127; //the left point the 7th bit of f is used to denote if push is done in the L. char L = f & 127; //the left point the 7th bit of f is used to denote if push is done in the L.
// copy weights of current state to WT1 // copy weights of current state to WT1
for(i=0; i < P; i++) { for(i=0; i < P; i++) {
for(j=0; j < P; j++) { for(j=0; j < P; j++) {
if(i==j) { //same transition points if(i==j) { //same transition points
WT1[i][i] = 0; WT1[i][i] = 0;
open1[i][i] = false; open1[i][i] = false;
} }
else if(i < j) { else if(i < j) {
WT1[i][j] = w[index(i, j, P)] & (~a32[15]); // 15-TH bit is used for open or not WT1[i][j] = w[index(i, j, P)] & (~a32[15]); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] ) // as 15th bit is used for open and close interval
open1[i][j] = true;
else
open1[i][j] = false;
}
else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index(i, j, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
if( w[index(i, j, P)] & a32[15] )
open1[i][j] = true;
else
open1[i][j] = false;
}
}
}
// the temporary new state has P+1 points as of now before applying forget operations
for(i=0; i <= P; i++) {
WT1[i][P] = INF16; // forward edge weight from point i to point P is infinite
WT1[P][i] = 0; // backward edge weight from point i to point P is zero
open1[i][P] = false;
open1[P][i] = false;
}
int lb, ub; // lower and upper bounds temprary variables
bool openl, openu; // lower and upper bound is open or not
// *** TODO : change weight using pop constraint also
// according to the constraint of every clocks, change the weight of the edges
for(x=1; x <= X; x++) { // iterate for every clocks
if( isChecked(x, dn) ) { // if there is a constraint for clock x in the transition dn
if( w[index(i, j, P)] & a32[15] ) // as 15th bit is used for open and close interval
lb = transitions[dn].lbs[x]; open1[i][j] = true;
ub = transitions[dn].ubs[x]; else
openl = (transitions[dn].openl) & a32[x]; // lower bound for clock x is open or not open1[i][j] = false;
openu = (transitions[dn].openu) & a32[x]; }
for(i=P-1; i >= 0; i--) { // find reset point for clock x else{ ///when i > j i.e the edges coming from j to i it must be negetive.
WT1[i][j] = - ( w[index(i, j, P)] & (~a32[15]) ); // 15-TH bit is used for open or not
if( isReset(x, del[i]) ) { // if clock x is reset at point i+1
if( w[index(i, j, P)] & a32[15] )
// tighten the lower and upper bounds open1[i][j] = true;
if( (-lb) < WT1[P][i] ) { else
WT1[P][i] = -lb; open1[i][j] = false;
open1[P][i] = (openl & a32[x]); }
}
}
else if( (-lb) == WT1[i][P] ) }
open1[P][i] |= (openl & a32[x]);
if(ub != INF) { // the temporary new state has P+1 points as of now before applying forget operations
if(ub < WT1[i][P]) { for(i=0; i <= P; i++) {
WT1[i][P] = ub; WT1[i][P] = INF16; // forward edge weight from point i to point P is infinite
open1[i][P] = (openu & a32[x]); WT1[P][i] = 0; // backward edge weight from point i to point P is zero
} open1[i][P] = false;
open1[P][i] = false;
else if( ub == WT1[i][P] ) }
open1[i][P] |= (openu & a32[x]);
}
i = -1;
} int lb, ub; // lower and upper bounds temprary variables
} bool openl, openu; // lower and upper bound is open or not
}
} // *** TODO : change weight using pop constraint also
// according to the constraint of every clocks, change the weight of the edges
/* for(x=1; x <= X; x++) { // iterate for every clocks
cout << "Before" << endl;
for(i=0; i <= P; i++){ if( isChecked(x, dn) ) { // if there is a constraint for clock x in the transition dn
for(j=0; j <= P; j++) {
cout << WT1[i][j] << "." << open1[i][j] << "\t";
} lb = transitions[dn].lbs[x];
cout << endl << endl; ub = transitions[dn].ubs[x];
} openl = (transitions[dn].openl) & a32[x]; // lower bound for clock x is open or not
openu = (transitions[dn].openu) & a32[x];
*/
for(i=P-1; i >= 0; i--) { // find reset point for clock x
allPairSP(P+1); //this is the Floyd–Warshall algorithm implementation
if( isReset(x, del[i]) ) { // if clock x is reset at point i+1
// tighten the lower and upper bounds
short **WT; if( (-lb) < WT1[P][i] ) {
bool **open; WT1[P][i] = -lb;
open1[P][i] = (openl & a32[x]);
if(P & 1) { // if P is odd, the shortest path stored in WT1 and open1 }
WT = WT1;
open = open1; else if( (-lb) == WT1[i][P] )
} open1[P][i] |= (openl & a32[x]);
else{ // if P is even, the shortest path stored in WT2 and open2
WT = WT2; if(ub != INF) {
open = open2; if(ub < WT1[i][P]) {
} WT1[i][P] = ub;
open1[i][P] = (openu & a32[x]);
/* }
cout << "After" << endl;
for(i=0; i <= P; i++){ else if( ub == WT1[i][P] )
for(j=0; j <= P; j++) { open1[i][P] |= (openu & a32[x]);
cout << WT[i][j] << "." << open[i][j] << "\t"; }
} i = -1;
cout << endl << endl; }
} }
*/ }
}
// checking if there is any negative cycle by applying floyd warshal algorithm
for(i=0; i <= P; i++){ /*
cout << "Before" << endl;
if(WT[i][i] < 0 || open[i][i]) for(i=0; i <= P; i++){
return NULL; for(j=0; j <= P; j++) {
} cout << WT1[i][j] << "." << open1[i][j] << "\t";
}
cout << endl << endl;
}
short count = 1; // var for storing #points in new state after applying forget operation
int forgetFlag = 0; // i-th bit of forgetFlag is 1 iff i-th point is forgotten */
int curReset = 0, reset = 0; allPairSP(P+1); //this is the Floyd–Warshall algorithm implementation
curReset = transitions[dn].reset;
for( i=P-1; i >= L; i--) {
reset = ( transitions[ del[i] ].reset ); short **WT;
bool **open;
/* there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
reset at (i+1) point of 1st state which has not reset to any of its right points for both state */ if(P & 1) { // if P is odd, the shortest path stored in WT1 and open1
if( reset & (~curReset) & (~1) ) { // (~) : ignore the 0-th bit, used for stack operation WT = WT1;
count++; // this point should be in new state, so increase the counter open = open1;
curReset |= reset; // union reset set at this point with earlier set }
} else{ // if P is even, the shortest path stored in WT2 and open2
else{ WT = WT2;
forgetFlag |= a32[i+1]; // i+1-th point will be forgotten in new state open = open2;
} }
}
/*
count += L; // all points from 1 to L will be there cout << "After" << endl;
char *newToOldRef = new char[count]; for(i=0; i <= P; i++){
for(j=0; j <= P; j++) {
i = 0; cout << WT[i][j] << "." << open[i][j] << "\t";
j = 0; }
for(; i < P; i++) { // find the reference from old point to new point cout << endl << endl;
if( (forgetFlag & a32[i+1] ) == 0 ) { }
newToOldRef[j] = i; */
j++;
} // checking if there is any negative cycle by applying floyd warshal algorithm
} for(i=0; i <= P; i++){
if(WT[i][i] < 0 || open[i][i])
newToOldRef[count-1] = P; // last point in the new state refer to new point return NULL;
}
stateZone *vs = new stateZone(); // new TA state
vs->del = new char[count]; // allocate memory
vs->w = new short[count*count - count]; short count = 1; // var for storing #points in new state after applying forget operation
vs->f = f; // **** must edit this for tpda int forgetFlag = 0; // i-th bit of forgetFlag is 1 iff i-th point is forgotten
vs->P = count;
int curReset = 0, reset = 0;
curReset = transitions[dn].reset;
for(i=0; i < (count-1); i++) {
vs->del[i]= del[newToOldRef[i]]; for( i=P-1; i >= L; i--) {
} reset = ( transitions[ del[i] ].reset );
vs->del[count-1] = dn;
/* there is a bit '1' of 'reset' but '0' of 'curReset' at same position => there is a clock
reset at (i+1) point of 1st state which has not reset to any of its right points for both state */
if( reset & (~curReset) & (~1) ) { // (~) : ignore the 0-th bit, used for stack operation
for(i=0;i < count; i++){ count++; // this point should be in new state, so increase the counter
for(j=0; j < count; j++){ curReset |= reset; // union reset set at this point with earlier set
if(i < j) { }
vs->w[index(i, j, count)] = WT[ newToOldRef[i] ][ newToOldRef[j] ]; else{
//cout << int(newToOldRef[i]) << "," << int(newToOldRef[j]) << endl; forgetFlag |= a32[i+1]; // i+1-th point will be forgotten in new state
if( open[ newToOldRef[i] ][ newToOldRef[j] ] ) }
vs->w[index(i, j, count)] |= a32[15]; }
}
else if(i > j) { count += L; // all points from 1 to L will be there
vs->w[index(i, j, count)] = - WT[ newToOldRef[i] ][ newToOldRef[j] ]; char *newToOldRef = new char[count];
//cout << int(newToOldRef[i]) << "," << int(newToOldRef[j]) << endl;
if( open[ newToOldRef[i] ][ newToOldRef[j] ] ) i = 0;
vs->w[index(i, j, count)] |= a32[15]; j = 0;
} for(; i < P; i++) { // find the reference from old point to new point
} if( (forgetFlag & a32[i+1] ) == 0 ) {
} newToOldRef[j] = i;
j++;
}
// ***TO DO : }
// Take open guard as input
//vs->print();
return vs; newToOldRef[count-1] = P; // last point in the new state refer to new point
stateZone *vs = new stateZone(); // new TA state
vs->del = new char[count]; // allocate memory
vs->w = new short[count*count - count];
vs->f = f; // **** must edit this for tpda
vs->P = count;
for(i=0; i < (count-1); i++) {
vs->del[i]= del[newToOldRef[i]];
}
vs->del[count-1] = dn;
for(i=0;i < count; i++){
for(j=0; j < count; j++){
if(i < j) {
vs->w[index(i, j, count)] = WT[ newToOldRef[i] ][ newToOldRef[j] ];
//cout << int(newToOldRef[i]) << "," << int(newToOldRef[j]) << endl;
if( open[ newToOldRef[i] ][ newToOldRef[j] ] )
vs->w[index(i, j, count)] |= a32[15];
}
else if(i > j) {
vs->w[index(i, j, count)] = - WT[ newToOldRef[i] ][ newToOldRef[j] ];
//cout << int(newToOldRef[i]) << "," << int(newToOldRef[j]) << endl;
if( open[ newToOldRef[i] ][ newToOldRef[j] ] )
vs->w[index(i, j, count)] |= a32[15];
}
}
}
// ***TO DO :
// Take open guard as input
//vs->print();
return vs;
} }
// not applied by ilias // not applied by ilias
/*// Return template successor state whose descendent states will be right states for shuffle operation with this state /*// Return template successor state whose descendent states will be right states for shuffle operation with this state
stateGCPP* stateZone::sucState(){ stateGCPP* stateZone::sucState(){
short curReset, reset; // temp vars for keeping reset bit vector short curReset, reset; // temp vars for keeping reset bit vector
char count; // will contain #points in the new state char count; // will contain #points in the new state
char i,j; // counters char i,j; // counters
// iterate through all points right to left except the last point // iterate through all points right to left except the last point
curReset = transitions[ del[P-1] ].reset; curReset = transitions[ del[P-1] ].reset;
count = 1; //we have to take the last point, so initialize 'count' to 1 count = 1; //we have to take the last point, so initialize 'count' to 1
for(i=P-2; i >= 0; i--) { for(i=P-2; i >= 0; i--) {
reset = transitions[ del[i] ].reset; // reset bit vector for point i+1 reset = transitions[ del[i] ].reset; // reset bit vector for point i+1
if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has additional reset for some clock if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has additional reset for some clock
count++; count++;
curReset |= reset; curReset |= reset;
} }
} }
stateZone* vs = new stateZone(); // new template state stateZone* vs = new stateZone(); // new template state
vs->P = count; //#points vs->P = count; //#points
//vs->L = count; // no non-trivial block is there there is no L in the zone class //vs->L = count; // no non-trivial block is there there is no L in the zone class
vs->del = new char[count]; //allocate space for transition vs->del = new char[count]; //allocate space for transition
vs->w = new char[count]; // allocate space for the upper and lower limits vs->w = new char[count]; // allocate space for the upper and lower limits
vs->del[count-1] = del[P-1]; // the last point is the last transition vs->del[count-1] = del[P-1]; // the last point is the last transition
//vs->w[count-1] = w[P-1]; // have to apply the upper and lower bounds //vs->w[count-1] = w[P-1]; // have to apply the upper and lower bounds
// copy the necessary points into the template state // copy the necessary points into the template state
char lastindex = P-1; char lastindex = P-1;
short nf = 0; // flag variable for new state short nf = 0; // flag variable for new state
curReset = transitions[ del[P-1] ].reset; curReset = transitions[ del[P-1] ].reset;
for(i=P-2, j = count-2; i >= 0; i--) { for(i=P-2, j = count-2; i >= 0; i--) {
reset = transitions[ del[i] ].reset; // reset bit vector for point i+1 reset = transitions[ del[i] ].reset; // reset bit vector for point i+1
if(reset & (~curReset) & (~1) ) { // found a new necessary point, copy this point to new state if(reset & (~curReset) & (~1) ) { // found a new necessary point, copy this point to new state
vs->del[j] = del[i]; vs->del[j] = del[i];
vs->w[j] = w[i]; vs->w[j] = w[i];
if( !big(i+1, lastindex+1) ) //from current needy point to the last found needy point distance small if( !big(i+1, lastindex+1) ) //from current needy point to the last found needy point distance small
nf |= a32[j+1]; // distance (j+1->(j+2)) is small nf |= a32[j+1]; // distance (j+1->(j+2)) is small
curReset |= reset; curReset |= reset;
j--; j--;
lastindex = i; // this point is the last point selected till now lastindex = i; // this point is the last point selected till now
} }
} }
vs->f = nf; // copy flag information, no stack info is there till now for the template state vs->f = nf; // copy flag information, no stack info is there till now for the template state
return vs; return vs;
} }
* */ * */
// print a validity state // print a validity state
void stateZone::print() { void stateZone::print() {
char i, j; char i, j;
char L = f & 127; // 7-th bit is used for push pop operation char L = f & 127; // 7-th bit is used for push pop operation
cout << endl << "Abstract state of the on the fly tree automata(TA):" << endl; cout << endl << "Abstract state of the on the fly tree automata(TA):" << endl;
cout << "\tPoints in the automaton:\n\t\t"; cout << "\tPoints in the automaton:\n\t\t";
cout << 1 ; cout << 1 ;
for(i=2; i <= L; i++) for(i=2; i <= L; i++)
cout << " " << int(i) ; cout << " " << int(i) ;
for(i=L+1; i <= P; i++) for(i=L+1; i <= P; i++)
cout << "----" << int(i) ; cout << "----" << int(i) ;
cout << endl; cout << endl;
cout << "\t\tL : " << int(L) << endl; cout << "\t\tL : " << int(L) << endl;
cout << "\tTransitions:"; cout << "\tTransitions:";
cout << "\t"; cout << "\t";
for(i=0; i < P; i++) for(i=0; i < P; i++)
cout << int(del[i]) << "\t"; cout << int(del[i]) << "\t";
cout << endl; cout << endl;
cout << "\tWeight Matrix : " << endl << "\t"; cout << "\tWeight Matrix : " << endl << "\t";
//for(i=0; i < P; i++) //for(i=0; i < P; i++)
//cout << int(i+1) << "\t"; //cout << int(i+1) << "\t";
cout << endl; cout << endl;
for(i=0;i < P; i++) { for(i=0;i < P; i++) {
cout << "\t\t\t"; cout << "\t\t\t";
for(j=0; j < P; j++) { for(j=0; j < P; j++) {
if(i==j) if(i==j)
cout << "0,0" << "\t"; cout << "0,0" << "\t";
else if(i < j) else if(i < j)
cout << (w[index(i, j, P)] & (~a32[15]) ) << "," << bool((w[index(i, j, P)] & (a32[15]) )) << "\t"; cout << (w[index(i, j, P)] & (~a32[15]) ) << "," << bool((w[index(i, j, P)] & (a32[15]) )) << "\t";
else else
cout << ( -short(w[index(i, j, P)] & (~a32[15]) ) ) << "," << bool((w[index(i, j, P)] & (a32[15]) )) << "\t"; cout << ( -short(w[index(i, j, P)] & (~a32[15]) ) ) << "," << bool((w[index(i, j, P)] & (a32[15]) )) << "\t";
} }
cout << endl; cout << endl;
} }
cout << endl << endl; cout << endl << endl;
cout << "\tPush done at L : " << ( (f & 128)? 1 : 0 ) << endl; cout << "\tPush done at L : " << ( (f & 128)? 1 : 0 ) << endl;
} }
// if this state is a final state // if this state is a final state
bool stateZone::isFinal(){ bool stateZone::isFinal(){
char L = f & 127 ; // ignore the leftmost bit char L = f & 127 ; // ignore the leftmost bit
if(L != 1) // there should not be any hanging point if(L != 1) // there should not be any hanging point
return false; return false;
// transition at first point must be 0-th transition // transition at first point must be 0-th transition
if( del[0] != 0) if( del[0] != 0)
return false; return false;
// there will not any push at the last transition // there will not any push at the last transition
if( isPush( del[P-1] ) ) if( isPush( del[P-1] ) )
return false; return false;
// target state of the transiton at point R should be the final state // target state of the transiton at point R should be the final state
if( transitions[del[P-1]].target != SF ) if( transitions[del[P-1]].target != SF )
return false; return false;
return true; return true;
} }
/* /*
// return the partial run corresponding the tree automata state 'vs', ignore the hanging points // return the partial run corresponding the tree automata state 'vs', ignore the hanging points
// copy only transitions between L(left) and R(right) // copy only transitions between L(left) and R(right)
runCGPP* getRun(stateGCPP* vs) { runCGPP* getRun(stateGCPP* vs) {
runCGPP *pr = new runCGPP(); // new partial run stored in variable pr runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
pr->P = vs->P - vs->L + 1 ; // transitions in new partial run will be from left(L) point to right(R) point pr->P = vs->P - vs->L + 1 ; // transitions in new partial run will be from left(L) point to right(R) point
// allocate memory for transitions and tsm vlaues for new run // allocate memory for transitions and tsm vlaues for new run
pr->del = new char[pr->P]; pr->del = new char[pr->P];
pr->w = new char[pr->P]; pr->w = new char[pr->P];
// loopers : i used to index transition of the tree automata state and j is used to index trans in the run // loopers : i used to index transition of the tree automata state and j is used to index trans in the run
char i = vs->L - 1, j=0; char i = vs->L - 1, j=0;
// copy transitions and tsm values from earlier partial run to new partial run // copy transitions and tsm values from earlier partial run to new partial run
for(; i < (vs->P); i++, j++) { for(; i < (vs->P); i++, j++) {
pr->del[j] = vs->del[i]; pr->del[j] = vs->del[i];
pr->w[j] = vs->w[i]; pr->w[j] = vs->w[i];
} }
return pr; // return the new run return pr; // return the new run
} }
// GIVEN the current partial run, append the transition 'dn' with tsm value 'wn' // GIVEN the current partial run, append the transition 'dn' with tsm value 'wn'
runCGPP* runCGPP::addNext(char dn, char wn) { runCGPP* runCGPP::addNext(char dn, char wn) {
runCGPP *pr = new runCGPP(); // new partial run stored in variable pr runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
pr->P = P + 1; // #transitions in new partial run will be one more than the earlier pr->P = P + 1; // #transitions in new partial run will be one more than the earlier
// allocate memory for transitions and tsm vlaues for new run // allocate memory for transitions and tsm vlaues for new run
pr->del = new char[pr->P]; pr->del = new char[pr->P];
pr->w = new char[pr->P]; pr->w = new char[pr->P];
// copy transitions and tsm values from earlier partial run to new partial run // copy transitions and tsm values from earlier partial run to new partial run
for(char i=0; i < P; i++) { for(char i=0; i < P; i++) {
pr->del[i] = del[i]; pr->del[i] = del[i];
pr->w[i] = w[i]; pr->w[i] = w[i];
} }
pr->del[P] = dn; // add the new transition and tsm value to the last position of new partial run pr->del[P] = dn; // add the new transition and tsm value to the last position of new partial run
pr->w[P] = wn; pr->w[P] = wn;
return pr; // return the new run return pr; // return the new run
} }
// shuffle two partial runs and return the new partial run // shuffle two partial runs and return the new partial run
runCGPP* runCGPP::shuffle(runCGPP *s2) { runCGPP* runCGPP::shuffle(runCGPP *s2) {
runCGPP *pr = new runCGPP(); // new partial run stored in variable pr runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
// rightmost transition of left state is equal to leftmost transition of right state // rightmost transition of left state is equal to leftmost transition of right state
so new run will be concatenation of two runs and #points in new run is calculated as below// so new run will be concatenation of two runs and #points in new run is calculated as below//
pr->P = P + (s2->P) - 1; pr->P = P + (s2->P) - 1;
// allocate memory for transitions and tsm vlaues for new run // allocate memory for transitions and tsm vlaues for new run
pr->del = new char[pr->P]; pr->del = new char[pr->P];
pr->w = new char[pr->P]; pr->w = new char[pr->P];
char i, j; // loopers char i, j; // loopers
// copy the transitions and tsm values of first run except for the last position // copy the transitions and tsm values of first run except for the last position
for(i=0, j=0; i < (P-1); i++, j++) { for(i=0, j=0; i < (P-1); i++, j++) {
pr->w[j] = w[i]; pr->w[j] = w[i];
pr->del[j] = del[i]; pr->del[j] = del[i];
} }
// copy the transitions and tsm values of 2nd run // copy the transitions and tsm values of 2nd run
for(i=0; i < (s2->P); i++, j++) { for(i=0; i < (s2->P); i++, j++) {
pr->w[j] = s2->w[i]; pr->w[j] = s2->w[i];
pr->del[j] = s2->del[i]; pr->del[j] = s2->del[i];
} }
return pr; // return the new run return pr; // return the new run
} }
*/ */
// this will return a state with only 0-th transition with tsm value 0 // this will return a state with only 0-th transition with tsm value 0
stateZone* getZeroStateZone() { stateZone* getZeroStateZone() {
stateZone* vs = new stateZone(); //initialize a stateZone object stateZone* vs = new stateZone(); //initialize a stateZone object
vs->P = 1; //the first point vs->P = 1; //the first point
vs->f = 1; // no push pop info yet and L = 1 cause the last bit of the flag denotes the push complete information vs->f = 1; // no push pop info yet and L = 1 cause the last bit of the flag denotes the push complete information
vs->del = new char[1]; // memory allocation for the transitions vs->del = new char[1]; // memory allocation for the transitions
vs->w = NULL; //the 2-dimentional array projected in to one dimentional arry initially empty vs->w = NULL; //the 2-dimentional array projected in to one dimentional arry initially empty
vs->del[0] = 0; // 0th transition has tsm value 0 vs->del[0] = 0; // 0th transition has tsm value 0
return vs; return vs;
} }
// return unique string for last reset points of current state participating in a combine operation as a left state // return unique string for last reset points of current state participating in a combine operation as a left state
string stateZone::getKeyLeft() { string stateZone::getKeyLeft() {
string s = ""; // return this string string s = ""; // return this string
short resetSoFar, reset; // used for calculating union of resets short resetSoFar, reset; // used for calculating union of resets
s += del[P-1]; // include rightmost transition in the string s += del[P-1]; // include rightmost transition in the string
//sparsa's editing
//s += w[P-1]; // tsm value also be part of the key in zone we dont have any tsm values
char lastindex = P-1; // last index we have taken
//char nf = 0; // distance info DO we need it??
char i=P-2; //list
char j=0;
resetSoFar = transitions[ del[P-1] ].reset; // set of clocks reset at rightmost point
for(; i >= 0; i--) {
reset = transitions[ del[i] ].reset; // take (i+1)-th point transition reset set
//sparsa's editing if( reset & (~resetSoFar) & (~1) ) { // if there are some new clocks reset at point (i+1)
//s += w[P-1]; // tsm value also be part of the key in zone we dont have any tsm values s += del[i]; //then add the transition to the string
char lastindex = P-1; // last index we have taken //s += w[i]; // but we dont have
resetSoFar |= reset;
//char nf = 0; // distance info DO we need it?? //if( !big(i+1, lastindex+1) )
char i=P-2; //list // nf |= a32[j];
char j=0; j++;
}
resetSoFar = transitions[ del[P-1] ].reset; // set of clocks reset at rightmost point }
for(; i >= 0; i--) { //s += nf;
reset = transitions[ del[i] ].reset; // take (i+1)-th point transition reset set return s; // return the key
if( reset & (~resetSoFar) & (~1) ) { // if there are some new clocks reset at point (i+1)
s += del[i]; //then add the transition to the string
//s += w[i]; // but we dont have
resetSoFar |= reset;
//if( !big(i+1, lastindex+1) )
// nf |= a32[j];
j++;
}
}
//s += nf;
return s; // return the key
} }
// return unique string for hanging points of a state participating in a combine operation as a right state // return unique string for hanging points of a state participating in a combine operation as a right state
string stateZone::getKeyRight() { string stateZone::getKeyRight() {
string s = ""; // return this string as a key for current state string s = ""; // return this string as a key for current state
// take the transition at point L and all hanging points // take the transition at point L and all hanging points
//char nf = 0; // this contains distance information between points distance information not needed //char nf = 0; // this contains distance information between points distance information not needed
s+= del[(f&127)-1]; // L-th poiint transition s+= del[(f&127)-1]; // L-th poiint transition
//s+= w[L-1]; // L-th point tsm dont need in Zone //s+= w[L-1]; // L-th point tsm dont need in Zone
//char j = 0; // used for distance counter no distance in zone //char j = 0; // used for distance counter no distance in zone
char i = (f&127)-2; // counter for points from right to left starting from L-1 point char i = (f&127)-2; // counter for points from right to left starting from L-1 point
for(; i >= 0; i--, j++) { for(; i >= 0; i--) //j++)
s += del[i]; {
//s += w[i]; not needed in zone cause for zone it is not a time stamp s += del[i];
//s += w[i]; not needed in zone cause for zone it is not a time stamp
//if(f & a32[i+1] )
//nf |= a32[j]; //if(f & a32[i+1] )
} //nf |= a32[j];
}
// add distance info in the key
//s+= nf; // add distance info in the key
//s+= nf;
return s;
return s;
} }
/* /*
// print a run as witness of the given TPDA if the language is non-empty // print a run as witness of the given TPDA if the language is non-empty
void runCGPP::print() { void runCGPP::print() {
short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps
cout << endl << "A run of the automation as a witness for the language to be non-empty.\nThe run given as a sequence of pairs (Transition, Time stamp) : " << endl; cout << endl << "A run of the automation as a witness for the language to be non-empty.\nThe run given as a sequence of pairs (Transition, Time stamp) : " << endl;
for(char i=0; i < P; i++) { for(char i=0; i < P; i++) {
if( w[i] < lt ) // if current time stamps less than last time stamps if( w[i] < lt ) // if current time stamps less than last time stamps
ct = M + ct + (w[i] - lt); ct = M + ct + (w[i] - lt);
else else
ct = ct + (w[i] - lt); ct = ct + (w[i] - lt);
lt = w[i]; lt = w[i];
cout << "(" << int(del[i]) << ", " << int(ct) << ".0" << "), "; cout << "(" << int(del[i]) << ", " << int(ct) << ".0" << "), ";
} }
cout << endl << endl; cout << endl << endl;
} }
*/ */
// return a backtracking state with the info given in the parameters // return a backtracking state with the info given in the parameters
trackZone* getTrackZone(char t, int l, int r) { trackZone* getTrackZone(char t, int l, int r) {
trackZone* xrs = new trackZone(); trackZone* xrs = new trackZone();
xrs->type = t; // this string is empty because vs is atomic state type of state, if = 0 then atomic or child xrs->type = t; // this string is empty because vs is atomic state type of state, if = 0 then atomic or child
// 1 if its add operation // 1 if its add operation
//2 if its generated by shuffle //2 if its generated by shuffle
xrs->left = l; // if no left parameter then -1 xrs->left = l; // if no left parameter then -1
xrs->right = r; // if no right parameter then -1 xrs->right = r; // if no right parameter then -1
return xrs; return xrs;
} }
/* /*
// get the run of the timed system // get the run of the timed system
// if sm == "", this means. we are backtracking from the state reside in i-th index of main vector 'allStates' // if sm == "", this means. we are backtracking from the state reside in i-th index of main vector 'allStates'
// if sm != "", then sm string is the key for shuffle operation of the state reside in i-th index of allStates // if sm != "", then sm string is the key for shuffle operation of the state reside in i-th index of allStates
runCGPP* printRun(int i) { runCGPP* printRun(int i) {
stateGCPP* vs; // tree automata state variable stateGCPP* vs; // tree automata state variable
trackCGPP *bp; // back tracking state trackCGPP *bp; // back tracking state
vs = allStates[i].first; vs = allStates[i].first;
bp = allStates[i].second; bp = allStates[i].second;
runCGPP *rs, *rs1, *rs2; runCGPP *rs, *rs1, *rs2;
// if the i-th state is an atomic state // if the i-th state is an atomic state
if( (bp->type) == 0 ) { if( (bp->type) == 0 ) {
cout << endl << i << ":"; cout << endl << i << ":";
vs->print(); vs->print();
return getRun(vs); // return the run generated from atomic state return getRun(vs); // return the run generated from atomic state
} }
// if the considerted state is generated by an addNext operation from a state in the main vector // if the considerted state is generated by an addNext operation from a state in the main vector
else if( (bp->type) == 1 ) { else if( (bp->type) == 1 ) {
rs1 = printRun( bp->left ); rs1 = printRun( bp->left );
rs = rs1->addNext(vs->del[vs->P - 1], vs->w[vs->P - 1]); rs = rs1->addNext(vs->del[vs->P - 1], vs->w[vs->P - 1]);
cout << endl << i << " : " << (bp->left); cout << endl << i << " : " << (bp->left);
vs->print(); vs->print();
return rs; return rs;
} }
else{ else{
rs1 = printRun( bp->left); rs1 = printRun( bp->left);
rs2 = printRun(bp->right); rs2 = printRun(bp->right);
rs = rs1->shuffle(rs2); rs = rs1->shuffle(rs2);
cout << endl << i << " : " << (bp->left) << ", " << (bp->right); cout << endl << i << " : " << (bp->left) << ", " << (bp->right);
vs->print(); vs->print();
return rs; return rs;
} }
} }
*/ */
// return true iff language recognized by the TPDA is empty // return true iff language recognized by the TPDA is empty
bool isEmptyZone() { bool isEmptyZone() {
// we are assuming that non-emptiness for a TPDA means there is a non-trivial run(length of the run is non-zero) // we are assuming that non-emptiness for a TPDA means there is a non-trivial run(length of the run is non-zero)
if(SI == SF) { if(SI == SF) {
cout << "Initial state is same as final state " << endl; cout << "Initial state is same as final state " << endl;
return false; return false;
} }
int i,j; // counters int i,j; // counters
bool pushl, pushr, popl, popr, ppDone; bool pushl, pushr, popl, popr, ppDone;
// allocate memory for two weight matrix and their corresponding open vars used shortest path operations // allocate memory for two weight matrix and their corresponding open vars used shortest path operations
// K : maximum #points in a state // K : maximum #points in a state
WT1 = new short*[K+2]; // size is K(tree-width), so that we can use for any #points in a state WT1 = new short*[K+2]; // size is K(tree-width), so that we can use for any #points in a state
WT2 = new short*[K+2]; WT2 = new short*[K+2];
open1 = new bool*[K+2]; // size is K(tree-width), so that we can use for any #points in a state open1 = new bool*[K+2]; // size is K(tree-width), so that we can use for any #points in a state
open2 = new bool*[K+2]; open2 = new bool*[K+2];
for(i=0; i < (K+2); i++) { // allocate memory for inner 1d arrays for(i=0; i < (K+2); i++) { // allocate memory for inner 1d arrays
WT1[i] = new short[K+2]; WT1[i] = new short[K+2];
WT2[i] = new short[K+2]; WT2[i] = new short[K+2];
open1[i] = new bool[K+2]; open1[i] = new bool[K+2];
open2[i] = new bool[K+2]; open2[i] = new bool[K+2];
} }
int count=0; //count point to the index of the state currently being processed in the vector 'allStates' declared as global variable int count=0; //count point to the index of the state currently being processed in the vector 'allStates' declared as global variable
int N=0; // total number of unique states generated so far int N=0; // total number of unique states generated so far
string s; // temporary string for finding a unique key corresponding to a TA state, the key points to compatible states for combine operation string s; // temporary string for finding a unique key corresponding to a TA state, the key points to compatible states for combine operation
stateZone *rs, *vs, *vs1, *vs2; // some state variables required for track stateZone *rs, *vs, *vs1, *vs2; // some state variables required for track
trackZone *xrs; // back propagation state variable trackZone *xrs; // back propagation state variable
runZone *prs; // variable for partial run of the TPDA runZone *prs; // variable for partial run of the TPDA
char *del, *w, P, L; // variables for keeping current state transitions, tsm values, #points and left point char *del, *w, P, L; // variables for keeping current state transitions, tsm values, #points and left point
char dn; // var for upcoming transition might be added to the right of a state char dn; // var for upcoming transition might be added to the right of a state
char f; // flag variable char f; // flag variable
//for(int k= 0; k < 12870; k++) { //for(int k= 0; k < 12870; k++) {
vs = getZeroStateZone(); // 'vs' state is the first Tree automata state with only 0-th transition with tsm value 0 vs = getZeroStateZone(); // 'vs' state is the first Tree automata state with only 0-th transition with tsm value 0
identity(vs); // insert this state in the hashmap identity(vs); // insert this state in the hashmap
xrs = getTrackZone(0, -1, -1); xrs = getTrackZone(0, -1, -1);
allStatesZone.push_back( make_pair(vs, xrs) ); // insert the state into the main vector along with its back tracking information allStatesZone.push_back( make_pair(vs, xrs) ); // insert the state into the main vector along with its back tracking information
N++; // increment #states N++; // increment #states
//cout << k << endl; //cout << k << endl;
for(count = 0; count < 0; count++) { //start looping on the vector of transtions
//if( count %5000 == 0 ) // Below of this string, #states will be shown
//cout << "#States" << endl;
if( (count % 100) == 0 || count <= 200) // print state number currently being processed(note : all numbers will not be printed)
cout << count << endl;
rs = allStatesZone[count].first; // get the state at index count, process this state now
// printing the current state information and its parents
//rs->print();
xrs = allStatesZone[count].second;
// priting parents :
// shuffle : left and right index shows left and right parent
// add : first index is the real parent, second index is -1
// atomic(generated by sucState()) : right index is the real parent
// atomic(0-th state) : both index are -1
//cout << "Parents: " << (xrs->left) << ", " << (xrs->right) << endl << "--------------" << endl;
for(count = 0; count < 0; count++) { //start looping on the vector of transtions
//if( count %5000 == 0 ) // Below of this string, #states will be shown
//cout << "#States" << endl;
if( (count % 100) == 0 || count <= 200) // print state number currently being processed(note : all numbers will not be printed)
cout << count << endl;
rs = allStatesZone[count].first; // get the state at index count, process this state now
// printing the current state information and its parents
//rs->print();
xrs = allStatesZone[count].second;
// priting parents :
// shuffle : left and right index shows left and right parent
// add : first index is the real parent, second index is -1
// atomic(generated by sucState()) : right index is the real parent
// atomic(0-th state) : both index are -1
//cout << "Parents: " << (xrs->left) << ", " << (xrs->right) << endl << "--------------" << endl;
del = rs->del; del = rs->del;
P = rs->P; P = rs->P;
f = rs->f; f = rs->f;
...@@ -1130,7 +1177,7 @@ bool isEmptyZone() { ...@@ -1130,7 +1177,7 @@ bool isEmptyZone() {
if(L < P && pushr) if(L < P && pushr)
{ {
} }
else if (L < P && pushl && ppDone) else if (L < P && pushl && ppDone)
{ {
...@@ -1138,69 +1185,69 @@ bool isEmptyZone() { ...@@ -1138,69 +1185,69 @@ bool isEmptyZone() {
} }
else else
{ {
char q = transitions[ del[P-1] ].target; // target state of last transition char q = transitions[ del[P-1] ].target; // target state of last transition
// iterate through all the upcoming transitions // iterate through all the upcoming transitions
//this is only add operations we have to find way to suffle and //this is only add operations we have to find way to suffle and
for(i=0; i < nexttrans[q].size(); i++) {
for(i=0; i < nexttrans[q].size(); i++) { dn = nexttrans[q][i]; // i-th upcoming transition
vs = rs->addNextTPDA(dn); // get set of states after doing the add operation
dn = nexttrans[q][i]; // i-th upcoming transition
vs = rs->addNextTPDA(dn); // get set of states after doing the add operation if(vs != NULL) { // if new state is valid
//vs->print();
if(vs != NULL) { // if new state is valid if( identity(vs) ) {
//vs->print(); xrs = getTrackZone(1, count, -1); // key for the new state
if( identity(vs) ) { allStatesZone.push_back( make_pair(vs, xrs) );
xrs = getTrackZone(1, count, -1); // key for the new state N++;
allStatesZone.push_back( make_pair(vs, xrs) ); if( vs->isFinal() ) {
N++; vs->print();
if( vs->isFinal() ) { //prs = printRun(N-1);
vs->print(); //prs->print();
//prs = printRun(N-1); return false;
//prs->print(); }
return false;
} }
}
} }
}
}
} }
} }
// vs = allStatesZone[0].first; // vs = allStatesZone[0].first;
//N = 0' //N = 0'
//mapZone.clear(); //mapZone.clear();
//} //}
/* /*
vs = allStatesZone[0].first; vs = allStatesZone[0].first;
rs = vs->addNextTPDA(1); rs = vs->addNextTPDA(1);
rs->print(); rs->print();
vs = rs->addNextTPDA(2); vs = rs->addNextTPDA(2);
vs->print(); vs->print();
rs= vs->addNextTPDA(3); rs= vs->addNextTPDA(3);
rs->print(); rs->print();
rs->f = 3; rs->f = 3;
rs->print(); rs->print();
vs = rs->addNextTPDA(4); vs = rs->addNextTPDA(4);
vs->print(); vs->print();
rs = vs->addNextTPDA(5); rs = vs->addNextTPDA(5);
rs->print(); rs->print();
vs = rs->addNextTPDA(6); vs = rs->addNextTPDA(6);
rs = vs->addNextTPDA(7); rs = vs->addNextTPDA(7);
vs = rs->addNextTPDA(8); vs = rs->addNextTPDA(8);
rs = vs->addNextTPDA(9); rs = vs->addNextTPDA(9);
rs->print(); rs->print();
*/ */
return true; return true;
} }
......
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