first commit

.directory

+[Dolphin]
+Timestamp=2017,6,30,14,26,53
+Version=4
+
+[Settings]
+HiddenFilesShown=true

README

+INSTALLATION GUIDE :
+
+  1. Install c++ compiler g++ .
+
+  2. Install the graph drawing tool 'graphviz' using the following command in the terminal
+	sudo apt-get install graphviz
+
+BUILD THE SOURCE FILES :
+
+	1.Come to the project folder 'mtp2' in the terminal
+	2. Execute the following command :
+		make
+	3. executable fileS named 'tree' and 'drawsystem' should be created
+
+
+HOW TO RUN THE TOOL :
+
+1. First write an input file corresponding the timed system. Sample example with explanation has been given in the file 'input/sample'. Let us consider you have created a file named 'automata.txt' in the folder './input'.
+
+2. Run the following command in the terminal to see the automaton graphically :
+	./draw.sh input/automata.txt
+		
+3. Check for emptiness of the timed sytem by running the follwing command in the terminal:
+		./tree <input_file_path> <optional_param>
+		Example :
+			./tree input/automata.txt
+
+
+Congrats, You have just done your job.

benchmarks

+
+Example 	#stacks	#clocks	#states	#tran  	Max Cons	run time	uppaal run time	
+p1			1		0		5		5		5			0.004 sec		NA
+
+p2			1		0		3		3		5			0.013 sec		NA
+
+p3			1		0		5		6		5			0.072 sec		NA		
+
+p4			1		0		4		6		50			50 sec			NA
+		
+p5			1		0		5		7		5			0.034 sec		NA
+
+t1			0		2		5		5		5			5.52 sec		0.002 sec
+
+t2			0		2		2		3		9			84 sec			0.002 sec
+
+t3			0		1		3		3		1			0.02 sec		0.002 sec
+
+t4			0		2		3		4		5			3.13 sec		0.004 sec
+
+t5			0		2		3		3		2			1.99 sec		0.004 sec
+
+t6			0		1		3		4		2			0.05 sec		0.004 sec
+
+t7			0		2		2		4		2			0.04 sec		0.004 sec
+
+t8 			0		2		4		6		2			2.64 sec		0.004 sec
+
+t9			0		2		4		6		1			1.34 sec		.004 sec
+
+t10			0		3		6		8		6			279 sec			0.008 sec
+
+t11			0		4		6		8		5			228 sec
+
+tp1			1		2		3		4		2			538.892 sec		NA
+
+tp2			1		1		3		3		1			34.1568 sec		NA
+
+tp3			1		1		3		2		2			0.2379 sec		NA
+
+tp4			1		1		4		2		1			0.582661 sec	NA
+
+tp5			1		1		5		4		1			3.20973			NA
+
+tp6			1		2		6		8		4			1.5 hours		NA
+
+
+
+Example		|X|		Transitions		Maximum constants		Run time
+tp9			1		1				1						0.000437 seconds
+
+tp10		1		1				2						0.00025 seconds
+
+tp11		1		1				3						0.016949 seconds
+
+tp12		1		1				4						0.015443 seconds
+
+tp13		1		1				5						0.035402 seconds
+
+tp14		1		1				10						0.105494 seconds
+
+tp15		1		1				20						0.420387 seconds
+
+tp16		1		1				50						2.0639 seconds
+
+tp17		1		1				100						8.08796 seconds
+
+tp17		1		1				120						11.4239 seconds
+
+
+tp19		1		2				1						0.209932 seconds
+
+tp20		1		2				2						0.692367 seconds
+
+tp21		1		2				3						2.24773 seconds
+
+tp22		1		2				4						8.06586 seconds
+
+tp23		1		2				5						19.6632 seconds
+
+tp24		1		2				6						36.236 seconds
+
+tp25		1		2				7						141.894 seconds
+
+tp26		1		2				8						290.82 seconds
+
+tp27		1		2				9						428.632 seconds
+
+
+tp28		1		3				1						0.264313 seconds
+
+tp29		1		3				2						2.85213 seconds
+
+tp30		1		3				3						8.32226 seconds
+
+tp31		1		3				4						18.5062 seconds
+
+tp33		1		3				5						35.0779 seconds
+
+tp34		1		3				6						99.1919 seconds
+
+tp35		1		3				7						234.359 seconds
+
+tp36		1		3				8						370.326 seconds
+
+tp37		1		3				9						966.927 seconds
+
+
+tp38		1		4				1						(not completed in 20 min time with full color)
+
+tp38		1		4				1						0.741028(4-colors)
+
+tp39		1		4				2						6.90133(4-colors)
+
+tp40		1		4				2						34.6366(4-colors)
+
+tp41		1		4				3						42.9276(4-colors)
+
+tp42		1		4				4						197.58(4-colors)
+
+
+tp42		2		1				1						0.044485
+
+tp43		2		1				2						0.048453
+
+tp45		2		1				20						4.10182
+
+tp46		2		1				50						21.0796
+
+tp47		2		1				100						21.1479
+
+
+tp48		2		2				1						0.950384
+
+tp49		2		2				2						5.49052						
+
+tp49		2		2				3						13.1378
+
+tp50		2		2				4						30.5954
+
+tp51		2		2				5						47.9801
+
+
+tp52		2		3				1						0.967496		
+
+tp53		2		3				2						4.23774
+
+tp54		2		3				3						10.7196
+
+tp55		2		3				4						22.2556
+
+tp56		2		3				5						
+
+
+pushdown system :
+#trans 	M 	time
+6		0	0.000275
+6		1	0.003488
+6		2	0.010188
+6		3	0.005319
+6 		4	0.022071	
+6		5	0.066717
+6		6	0.023303
+6		7	0.039065
+6		8	0.067187	
+6		10	0.135559
+		15	0.572183
+		20	1.64088
+		25	3.78623
+		30	7.95845
+		35	15.8334
+		40	24.1085
+		45	37.6506
+		
+		
+		
+#trans	run time
+0	0.000243
+1	0.001314
+2	0.002179
+3	0.002127
+4	0.014129
+5	0.024787
+6	0.030262
+7	0.034
+14	2.98399
+15	5.09424
+25	16.6489
+26	20.2956
+29	23.9509
+Ram in the machine : 8 gb
+#cpus : 4
+cpu model :     Intel(R) Core(TM) i5-4690 CPU @ 3.50GHz
+
+
+
+
+
+**********
+New code : general one clock + one stack:
+Eg.		#trans	M		(sec)run time
+tp17	1		120		0.000519
+tp27	2		9		0.000172
+tp61	2		10		0.000126
+tp61	2		120		0.000368
+tp37	3		9		0.001152
+tp37	3		120		0.077424
+tp42	4		4		0.00064
+tp42	4		120		0.180572
+***********
+
+New code : general one clock + one stack:
+Experiments done on tpg2(#tran = 6)
+M 	time
+1	0.000887
+2	0.005571
+3	0.03677
+4	0.18576
+5	0.732166
+6	2.41135
+7	6.72983
+8	17.3284
+9	45.1559	
+10	104.982
+11 	196.923
+
+New code : general one clock + one stack:
+Experiments done on (M == 5)
+e.g.	#trans	time
+1		0.000262
+2		0.000318
+3		0.000468
+4		0.000758
+5		0.001677
+8		0.004263
+9		0.00814
+
+
+one stack + one clock(consecutive reset and transitions) :
+e.g tps4(#transitions = 6)
+
+M		Run time
+1		0.000343
+3		0.00043
+5		0.000517
+7		0.000591
+9		0.000918
+10		0.001131
+11		0.001349
+12		0.001527
+13		0.001925
+14		0.002434
+20		0.006207
+25		0.014641
+30		0.022661
+35		0.039456
+40		0.063975
+50		0.146298
+55		0.209322
+60		0.29141
+70		0.524645
+80		0.935695
+90		1.41289
+100		2.11851
+110		3.09092
+120		4.33606
+
+one stack + one clock(consecutive reset and transitions) tricky example(tps5) (#transitions=8) :
+M 	Runtime
+6	0.00295
+7	0.004041
+8	0.005887
+10	0.009491
+12 	0.022176
+15	0.045263
+20	0.130269
+25	0.231522
+30	0.289782
+40	0.776147
+50	1.7009
+70	5.93762
+100	23.0724
+
+one stack + one clock(consecutive reset and transitions) :
+M = 10
+E.G 	#trans		Runtime
+tps6		1		0.000176
+tps7		2		0.000366
+tps8		3		0.000295
+tps9		4		0.000329
+tps10		5		0.000335
+why the graph is not smooth : Run time depdend on the particular structure of the automation. We are considering only timed system recognizes empty language. If the
+language is empty, then all possible tree automata states will be generated.
+(i) Maximal Constant
+(ii) Depends on the constraints. As the number and constraints increases, less number of tree automata states will be generated.
+(iii) How many possibility are there for the next transition coming and what are the possible tsm values.
+(iv) How many push or pops are there. As the number of push pop increases, less number of possible tree automata states generated.
+(v) Depends on the os scheduling(how much time given to this process)
+
+Constraints :
+1. GLobal time bound : [3,3]
+2. Time bound on staying on junction 9 : [1,1]
+
+3.
+(i) After starting journey, bound on visiting time of place 1 : [2,3]
+(ii) After starting journey, bound on visiting time of place 2 : [1,2]
+(iii) After starting journey, bound on visiting time of place 3 : [1,1]
+(iv) After visiting place 2, bound on visiting time of place 4 : [1,2]
+(v) After visiting place 2, bound on visiting time of place 5 : [0,1]
+(vi) After visiting place 2, bound on visiting time of place 6 : [0,1]
+(vii) After visiting place 5, bound on visiting time of place 7 : [2,3]
+(viii) After visiting place 5, bound on visiting time of place 8 : [0,1]
+
+
+
+
+Automata Construction process :
+1. Constraints (1) and (2) is similiar to earliar approach we discussed
+2. For constraints (3), if the constraint is :
+	After visiting place i, bound on visiting time of place j : [a,b]
+	
+	In this construction pop of symbol i denotes : visit  of place i
+	Then, after popping symbol i, push the symbol j. When popping symbol j the bound is [a,b]
+	
+	
+	
+	
+Experiments on nested maze : p26(#transitions 39) :
+
+M	run_time(sec)
+0	0.106245
+1	0.977339
+2	4.40974
+3	12.786
+4	30.6616
+5	65.925
+6	130.821
+7	232.286
+8	382.595
+9	574.995
+
+
+(34, 0.0), (35, 0.0), (26, 0.0), (3, 0.0), (28, 0.0), (23, 0.0), (16, 0.0), (2, 0.0), (36, 0.0), (37, 0.0), (17, 0.0), (13, 0.0), (10, 0.0), (20, 0.0), (6, 0.0), (22, 0.0), (11, 0.0), (29, 0.0), (5, 0.0), (38, 0.0), (31, 0.0), (23, 0.0), (17, 0.0), (12, 0.0), (8, 0.0), (13, 0.0), (10, 0.0), (21, 0.0), (7, 0.0), (22, 0.0), (9, 0.0), (15, 0.0), (18, 0.0), (24, 0.0), (27, 0.0), (4, 0.0), (28, 0.0), (23, 0.0), (17, 0.0)
+
+32 34 35 3 36 37 5 38 (22 13 30) 39
+14 16 26 27 29 20 21 12 (9 10 11) 33

clean

+rm tree drawsystem main.o obj/*.o src/*.cpp~ include/*.h~

clean.sh

+rm tree drawsystem main.o obj/*.o src/*.cpp~ include/*.h~

cleanImage.sh

+rm newinput/*.png newinput/*.out
+rm input/*.png input/*.out

draw.sh

+#!/bin/bash
+
+name=$1
+#echo $name
+./drawsystem "$name" "$name.out"
+dot  -Tpng   "$name.out" -o "$name.png" 

drawloop.sh

+for i in {1..67}
+do
+ ./draw.sh "input/tp$i"
+ done

include/continuoustpda.h

+/*This file is for one clock and one stack general tpda*/
+#include<vector>
+#include<set>
+#include<string>
+using namespace std;
+
+// state info for one clock and one stack general tpda
+class tpdastate{
+	public:
+	char gc; /*0-th bit of gc is 1 iff push edge added to L, 7-th bit is 1 iff pop edge added to R, 1st bit is 1 iff gap between d1 and d2 is small, 2nd bit is 1 iff gap between d2 and d3 is small, 3rd bit is 1 iff gap between d3 and d4 is small */
+	
+	char d1, d2, d3, d4; /* d1 : hanging reset trans for clock x1, d2 : trans at L, d3 : trans between L and R(reset trans for clock x1), d4 : trans at R
+	d1 == -1 if no hanging clock, d3 == -1 if only two points are there or there is a reset at R
+	  */
+	
+	char w1, w2, w3, w4; // tsm values corresponding to trans d1,d2,d3 and d4 resp.
+	
+	bool big(char i, char j); // distance between point i to point j is big
+	short int dist(char i, char j); // distance between point i to point j
+	
+	// check if pop condition satisfied by the new transitions
+	bool popTest(char d5, char w5, int lb, int ub);
+	
+	
+	// check if after adding trans d5 with tsm w5, the clock constraint [lbc, ubc ] is satisfied or not
+	bool clockTest(char d5, char w5, int lbc, int ubc);
+	
+	char getGc(char d5, char w5); // get new accuracy flag after adding trans d5 with tsm w5
+	
+	// add next transition to the state rs
+	vector<tpdastate*> addNextTPDA();
+	
+	// shuffle of two states
+	tpdastate* shuffle(tpdastate *s2);
+	
+	tpdastate* copyState(); // create a copy of this state and return
+
+	bool isFinal(); // return true if this state is final
+	
+	void print(); // print a state of tree automation
+};
+
+
+// run of the  timed system
+class gtpda_run{
+	public : 
+	char P; // #points
+	char *del; // transitions
+	//char *ac; // accuracy between two consecutive points
+	char *w; // tsm values
+	
+	gtpda_run* add_next(char d5, char w5); // new run after adding trans d5 of tsm w5
+	gtpda_run* shuffle(gtpda_run *s2);
+	void print();
+};
+
+
+// info to keep track which states generates which states
+class bp_gtpda{
+	public :
+	char type; // type of operation : atomic : 0, add_stack : 1, shuffle : 2
+	int left; // shuffle left state index of all the states generated bottom-up
+	int right; // shuffle right state index of all the states generated bottom-up
+};
+
+extern set<string> gtpdatrie;
+
+
+// atomic state
+tpdastate* atomictpda(char d1, char d2, char d3, char d4, char w1, char w2, char w3, char w4, char gc);
+
+bool identity(tpdastate *vs); // return 1 iff vs is a new state
+
+// check if a tpda of one clock is empty or not
+bool isEmptyTPDA();
+
+gtpda_run* getatomicrunpds(tpdastate*); // get run for an atomic states

include/drawsystem.h

+typedef unsigned char weighttype;
+typedef unsigned char deltatype; // type used depending on the #transitions in the automation
+
+extern weighttype B;
+
+class transition{
+	public:
+	unsigned short int source; // source state
+	unsigned short int target; // target state
+	
+	char a; // action in this transition
+	//char op; // stack operation in this transition
+	char as; // stack symbol in this transition
+	char ps; // push 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 reset; // Let i-th bit of reset from right hand is r_i
+	/*
+	0-th bit of gurad and reset is for stack operation
+	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
+	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=1 && r_0=0 : stack push 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
+	*/
+	
+	int *lbs; // constraint lower bounds
+	int *ubs; // constraint upper bounds
+	
+	/*
+		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[i](1<=i<=15) : lower bound for i-th clock
+		
+		ubs[0] : upper bound for pop operation
+		ubs[i](1<=i<=15) : upper bound for i-th clock
+	*/
+	
+	bool isReset(char i);
+};
+
+
+extern char inputfilename[100]; // input file name for timed push-down system
+
+extern int M; // maximum constant+1 in the timed system
+
+extern unsigned short int S; // number of states in the timed system
+extern unsigned short int T; // number of transitions in the timed system
+extern unsigned short int SI; // initial state
+extern unsigned short int SF; // final state
+
+extern char X; // number of clocks in the timed system
+extern char A; // number of events or actions in the timed system
+extern char AS; // number of stack symbols in the timed system
+
+extern transition *transitions; // transitions of the timed system
+
+void inputSystem(); // get the input timed system given as a file(file name stored in the global variable 'inputfilename')
+
+void print_system();
+

include/pds.h

+#include<iostream>
+#include<vector>
+#include<set>
+
+using namespace std;
+
+extern set<string> pstrie;
+
+// datatype for a state of final tree automation
+class pds_state{
+
+	public:
+	char del1; // transition at first active color
+	char del2; // transition at second active color
+	char w1;
+	char w2;
+	char gc;
+	 
+	pds_state* add_stack();
+	pds_state* shuffle(pds_state *s2); // shuffle  with state s2
+	bool isFinal(); // check if this state is a final state
+	void print(); // print a state
+};
+
+bool identity(pds_state *vs);
+pds_state* atomic(char del1, char del2, char w1, char w2, char gc);
+bool pdsempty();
+
+
+
+class pds_run{
+	public : 
+	char P; // #points
+	char *del; // transitions
+	char *ac; // accuracy between two consecutive points
+	char *w; // tsm values
+	
+	pds_run* add_stack();
+	pds_run* shuffle(pds_run *s2);
+	void print();
+};
+
+
+class bp_pds{
+	public :
+	char type; // type of operation : atomic : 0, add_stack : 1, shuffle : 2
+	int left; // shuffle left state index of all the states generated bottom-up
+	int right; // shuffle right state index of all the states generated bottom-up
+};
+
+
+pds_run* getatomicrunpds(pds_state*);

include/timePushDown.h

+#include<vector>
+using namespace std;
+
+class transition{
+	public:
+	short source; // source state
+	short target; // target state
+	
+	char a; // action in this transition
+	
+	char as; // stack symbol in this transition, **** this variable is obsolete in new version of code
+
+	char ps; // push 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 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 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
+	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
+	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=1 && r_0=0 : stack push 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
+	*/
+	
+	int *lbs; // constraint lower bounds
+	int *ubs; // constraint upper bounds
+	
+	/*
+		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[i](1<=i<=15) : lower bound for i-th clock
+		
+		ubs[0] : upper bound for pop operation
+		ubs[i](1<=i<=15) : upper bound for i-th clock
+	*/
+	
+};
+
+
+extern char inputfilename[100]; // input file name for timed push-down system
+
+extern int M; // maximum constant+1 in the timed system
+
+extern short S; // number of states in the timed system
+extern short T; // number of transitions in the timed system
+extern short SI; // initial state
+extern short SF; // final state
+
+extern char X; // number of clocks in the timed system
+extern char A; // number of events or actions in the timed system
+extern char AS; // number of stack symbols in the timed system
+
+extern transition *transitions; // transitions of the timed system
+
+extern vector<vector<short> > prevtrans; // prevtrans[i] : list of previous transitions for state i
+extern vector<vector<short> > nexttrans; // nexttrans[i] : list of next transitions for state i
+
+
+extern vector<vector<short> > resettrans; // resettrans[i] : list of reset transitions for clock i
+extern vector<vector<short> > checktrans; // checktrans[i] : list of check transitions for clock i
+
+extern vector<vector<pair<short, short> > > resecktrans; // resecktrans[i] : list of reset-check transitions for clock i
+
+// this applies for one clock TPDA
+extern vector<vector<short> > possibleresets; // possibleresets[t] : list of reset transitions for clock x_1 possible for the check transition t of clock x_1
+
+// pushDone[t][w] : 1 iff atomic state generated with starting trans t with tsm w
+extern bool** pushDone;
+
+// 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);
+
+void getresecktrans(); // get all the reset-check pair of transition for some clock
+
+void inputSystem(); // get the input timed system given as a file(file name stored in the global variable 'inputfilename')
+
+void print_system(); // print system details
+
+
+// is clock x has been reset at transition delta
+bool isReset(char x, short int delta);
+
+// is clock x has been checked at transition delta
+bool isChecked(char x, short int delta);
+
+// is there a push at transition delta
+bool isPush(short int delta);
+
+// is there a pop at transition delta
+bool isPop(short int delta);
+
+// return a mod b(always return a +ve number unlike c % operator)
+short int mod(short int a, short int b);
+

include/tpda2.h

+/*This file is for one clock and one stack special(contiguous reset and check of the clock) tpda*/
+#include<vector>
+#include<set>
+#include<string>
+using namespace std;
+
+// state info for one clock and one stack general tpda
+class stpdastate{
+	public:
+	char gc; /*0-th bit of gc is 1 iff push edge added to L, 7-th bit is 1 iff pop edge added to R, 1st bit is 1 iff gap between d1 and d2 is small, 2nd bit is 1 iff gap between d2 and d3 is small, 3rd bit is 1 iff gap between d3 and d4 is small */
+	
+	char d1, d2; /* d1 : hanging reset trans for clock x1, d2 : trans at L, d3 : trans between L and R(reset trans for clock x1), d4 : trans at R
+	d1 == -1 if no hanging clock, d3 == -1 if only two points are there or there is a reset at R
+	  */
+	char w1, w2; // tsm values corresponding to trans d1,d2,d3 and d4 resp.
+	
+	// add next transition to the state rs
+	vector<stpdastate*> addNextTPDA();
+	
+	// shuffle of two states
+	stpdastate* shuffle(stpdastate *s2);
+
+	bool isFinal(); // return true if this state is final
+	
+	void print(); // print a state of tree automation
+};
+
+
+// run of the  timed system
+class stpda_run{
+	public : 
+	char P; // #points
+	char *del; // transitions
+	char *w; // tsm values
+	
+	stpda_run* add_next(char d5, char w5); // new run after adding trans d5 of tsm w5
+	stpda_run* shuffle(stpda_run *s2);
+	void print();
+};
+
+
+// info to keep track which states generates which states
+class bp_stpda{
+	public :
+	char type; // type of operation : atomic : 0, add_stack : 1, shuffle : 2
+	int left; // shuffle left state index of all the states generated bottom-up
+	int right; // shuffle right state index of all the states generated bottom-up
+};
+
+extern set<string> gtpdatrie;
+
+// atomic state
+stpdastate* atomicstpda(char d1, char d2, char w1, char w2, char gc);
+
+bool identity(stpdastate *vs); // return 1 iff vs is a new state
+
+// check if a tpda of one clock is empty or not
+bool isEmptySTPDA();
+
+stpda_run* getatomicrunstpda(stpdastate*); // get run for an atomic states

include/tpdaCGPP.h

+// This file is for general TPDA emptiness checking with continuous implementation, pop and push also can happen at the same transition
+
+#include<vector>
+#include<set>
+#include<string>
+#include <unordered_map>
+
+using namespace std;
+
+#define a3215  32768 // 2^15 shortcut
+
+
+// state for general TPDA with pop ande push happens at the same time
+class stateGCPP{
+	public:
+	char P; // number of points in this state
+	
+	short f; // flag variable contain accuracy between consecutive points and push-pop edge information
+	
+	char *del; // transitions in this state
+	
+	char *w; // tsm values in this state
+	
+	char L; // left point of the non-trivial block
+	
+	bool big(char i, char j); // return true iff distance between point i to point j is big
+	
+	short int dist(char i, char j); // return distance between point i to point j
+	
+	// add next transition to this state if possible and return all generated states by doing this operation
+	vector<stateGCPP*> addNextTPDA();
+	
+	// add transition 'dn' to this state and then forget some points if possible, return the new state, tsm value of last point not decided yet
+	stateGCPP* reduce(char dn);
+	
+	// return true iff clock gurards on new transition 'dn' with tsm value 'wn' is satisfied
+	bool consSatisfied(char dn, char wn, short *clockDis, bool *clockAcc);
+	
+	// check for stack constraint where 'dlr' and 'aclr' are distance and accuracy resp. from L to R
+	bool stackCheck(char dn, char wn, short dlr, bool aclr);
+	
+	// reduce the #points after shuffle operation by using forget operation if possible
+	stateGCPP* reduceShuffle(stateGCPP* vs);
+	
+	// check if shuffle of this state with s2 is possible
+	bool shuffleCheck(stateGCPP *s2);
+	
+	// return shuffle of this state with s2
+	stateGCPP* shuffle(stateGCPP *s2);
+	
+	// Return the first successor state whoose childrens will be right state for shuffle with current state
+	stateGCPP* sucState();
+
+	bool isFinal(); // return true iff this state is final
+	
+	void print(); // print this state
+	
+	// return unique string for last reset points of a state participating in a combine operation as a left state
+	string getKeyLeft();
+	
+	// return unique string for hanging points of a state participating in a combine operation as a right state
+	string getKeyRight();
+};
+
+
+// partial run of the  timed system as a sequence of pairs: (1) transition and (2) tsm value
+class runCGPP{
+	public : 
+	char P; // #points
+	char *del; // transitions
+	char *w; // tsm values
+	
+	runCGPP* addNext(char dn, char wn); // new run after adding transition 'dn' of tsm value 'wn'
+	
+	runCGPP* shuffle(runCGPP *s2); // concatenation of two partial runs
+	
+	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
+class trackCGPP{
+	public :
+	char type; //***** type of operation : atomic : 0, addNextTPDA : 1, shuffle or combine : 2
+  	int left; // *****shuffle left 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
+//extern set<string> tpdaGCPPtrie;
+
+// alternative : this is used for checking if newly generated state was already generated earlier or not
+extern unordered_map<string,bool> mapGCPP;
+
+// this vector contains all the states generated for a TPDA with corresponding tracking information
+extern vector<pair<stateGCPP*, trackCGPP*> > allStates;
+
+// get the partial run corresponding the tree automata state vs, ignore the hanging points
+runCGPP* getRun(stateGCPP* vs); 
+
+// return true iff language recognized by the TPDA is empty
+bool isEmptyGCPP();

include/tpdaZone.h

+// This file is for general TPDA emptiness checking with continuous implementation, pop and push also can happen at the same transition
+
+#include<vector>
+#include<string>
+#include <unordered_map>
+
+
+using namespace std;
+
+
+// index is a function from 2d array index to 1d array index considering all diagonal elements are 0
+#define index(i, j, n)  ( i*n + j - i - (j < i ? 0 : 1) )
+
+extern short **WT1, **WT2; // used as temporary storage for weight matrix in floyd warshal algorithm
+extern bool **open1, **open2; // temporary variables for storing some edge weight is strictly less than some integer or not
+
+
+// state for timed automata
+class stateZone{
+	public:
+	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 *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
+	
+	// add next transition to this state if possible and return all generated states by doing this operation
+	stateZone* addNextTPDA(char dn);
+	
+	// check if shuffle of this state with s2 is possible
+	bool shuffleCheck(stateZone *s2);
+	
+	// return shuffle of this state with s2
+	stateZone* shuffle(stateZone *s2);
+	
+	// Return the first successor state whoose childrens will be right state for shuffle with current state
+	stateZone* sucState();
+
+	bool isFinal(); // return true iff this state is final
+	
+	void print(); // print this state
+	
+	// return unique string for last reset points of a state participating in a combine operation as a left state
+	string getKeyLeft();
+	
+	// return unique string for hanging points of a state participating in a combine operation as a right state
+	string getKeyRight();
+};
+
+
+// partial run of the  timed system as a sequence of pairs: (1) transition and (2) tsm value
+class runZone{
+	public : 
+	short P; // #points
+	char *del; // transitions
+	short **w; // weight matrix
+	
+	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
+	
+	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
+class trackZone{
+	public :
+	char type; //***** type of operation : atomic : 0, addNextTPDA : 1, shuffle or combine : 2
+  	int left; // *****shuffle left 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
+extern unordered_map<string,bool> mapZone;
+
+// this vector contains all the states generated for a TPDA with corresponding tracking information
+extern vector<pair<stateZone*, trackZone*> > allStatesZone;
+
+// get the partial run corresponding the tree automata state vs, ignore the hanging points
+runZone* getRun(stateZone* vs); 
+
+// return true iff language recognized by the TPDA is empty
+bool isEmptyZone();
+
+// apply all pair shortest path algorithms for the graph with n number of nodes(edge weight given in w) 
+void  allPairSP(int n);
\ No newline at end of file

include/treeBitOperations.h

+#include<string>
+#include<limits.h>
+
+using namespace std;
+
+
+typedef unsigned short int usint;
+
+typedef unsigned int uint;
+
+typedef unsigned long long int ullint;
+
+typedef unsigned char uchar;
+
+
+//TINDEX : given two pair of integers, find the position in 1d array
+#define BY2(i) (i >> 1) // divide by 2 ...
+#define BY4(i) (i >> 2)
+#define BY8(i) (i >> 3)
+#define BY16(i) (i >> 4)
+#define INF (INT_MAX >> 1) //now infinity value is maximum integer divided by 2
+#define INF16 (a32[14])
+
+
+
+extern unsigned   int a32[]; /* a contains all the binary strings where only one bit is '1'
+ a[i] contains binary number where only (i-1)-th from right side is '1'(bit position starts from 0 from right hand side) */
+
+extern unsigned   int b32[];/*b[i] contains an integer where all bits are '1' from zeroth bit position upto (i-1)-th bit position
+For example, b[4] contains binary number 00..01111 or integer 15
+*/
+extern unsigned   int c32[];/*c[i] contains an integer where all bits are '1' from i+1-th bit position upto  last bit position
+For example, c[4] contains binary number 11..10000 or integer -16
+*/
+
+extern unsigned   int d32[]; /* a contains all the binary strings where only one bit is '1'
+ a[i] contains binary number where only (i-1)-th from right side is '1'(bit position starts from 0 from right hand side) */
+
+
+extern char K; // this denote number of maximum active colors
+
+void setBits(); // set all the global bit variables
+
+int noofones(unsigned   int x, int B); // #ones upto B bits
+
+string inttobinary(int x); // return binary string corresponding to number x
+

input/pd1

+8 7 0 0 2
+
+1
+8
+
+1 2 0 0 0
+0
+
+2 3 0 0 0
+1 1
+
+3 4 0 0 0
+3 1 1 1 2
+
+4 5 0 0 0
+2 2 1 -1
+
+5 6 0 0 0
+0
+
+6 7 0 0 0
+1 1
+
+7 8 0 0 0
+2 1 1 -1
+
+
+ 0 0 0
+
+ 0 0 0

input/rep1

+5 5 2 0 1
+
+1
+
+5
+
+1 2 0 0 1
+1
+0
+
+2 3 0 0 1
+2
+0
+
+3 4 0 1 1
+1 0 2
+2
+0
+
+4 2 0 1 0
+2 1 1
+1 1
+
+4 1 0 0 1
+2
+2 1 0 -1

input/rep2

+4 11 2 9 1
+
+1
+
+4
+
+
+1 2 1 0 0
+0
+
+2 3 2 1 1
+1 1 2
+2
+0
+
+3 4 3 1 0
+2 0 1
+1 1
+
+4 2 4 1 0
+1 1 2
+0
+
+2 4 5 1 2
+2 1 2
+1 2
+0
+
+4 3 6 0 1
+1
+0
+
+3 2 7 0 0
+2 1 2 2
+
+2 1 8 0 0
+0
+
+1 4 9 2 0
+1 0 2
+2 1 1
+0
+
+1 1 0 0 1
+2
+0
+
+3 3 0 0 1
+1
+0
+
+
+
+
+
+//TPDA corresponding to this file used to demonstrate the example in the report

input/sample

+4 4 2 0 2
+
+1
+
+4
+
+1 2 0 1 1
+2 2 3
+1
+1 1
+
+1 4 0 0 0
+2 2 2 2
+
+2 3 0 2 0
+1 0 2
+2 1 2
+3 1 0 2 2
+
+3 1 0 0 2
+1 2
+0
+
+******CORRESPONDING TO THE ABOVE INPUT REFER TO THE TIMED SYSTEM GIVEN IN THE PICTURE 'sample.png'  *******
+Transition description of the automaton :
+	Each transition contain four information : 
+		(i) Transition number(Transition number 3 shown as : 'tn:3')
+		(ii) Clock constraint(x1>=2 && x2==3 is shown as : '2 <= x1 <= inf, 3<=x2<=3')(for tpda and timed automation)
+		(iii) Update or reset of clocks(x1:=0,x2:=0 is shown as : 'x1:=0,x2:=0')(for tpda and timed automation)
+		(iv) Stack Operations :(for tpda and pushdown system with age checking while popping)
+			(a) Nop(No operation) : shown as : 'np'.
+			(b) push symbol 2 : shown as 'ps_2'.
+			(c) Pop symbol 2 with age between 2 and 5 shown as : 'pp_2:2<=ag(2)<=5'
+			
+			
+			
+			
+
+INPUT FORMAT(Ignore blank lines and spaces) :
+
+1. First line of the input(5 space separated integers) : <#states> <#transitions> <#clocks> <#actions> <#stack_symbols>
+
+	In the above example, Input for the first line is : 3 3 2 0 2
+	Number of states is 3( they are numbered as 1, 2 and 3)
+	Number of transitions is 3( they are numbered as 1, 2 and 3)
+	Two clocks are there( they are numbered as x_1 and x_2 )
+	Actions are not important for us, So simply enter 0 in place of 'number of actions'
+	Number of stack symbols is 2( they are numbered as 1 and 2)
+
+2. Second line : Initial state number(1 is the initial state for the above example)
+
+3. Third line : Final state number(4 is  the final state for the above example)
+
+4. For each transitions, there can be variable number of lines.
+	First line of each transition(5 space separated integers) : <source_state> <target_state> <action> <#guards> <#resets>
+		For the above example, in the first transition :
+			source state : 1
+			target state : 2
+			action : 0(action is not important for us, just put 0 in place of action)
+			#guards : number of clock checks are there
+			#resets : number of clock reset at this transition
+	If number of clock check(#guards) is m, then each of the next m lines will have three space separated intergers : <clock_number> <lower_bound> <upper_bound>
+		clock_number : clock(x) for which there is a check in this transition
+		lower bound : x >= lower_bound is the lower bound constraint
+		upper bound : x <= upper_bound is the upper bound constraint
+		overall the constraint is lower_bound <= x <= upper_bound
+
+	If number of clock reset at this transition is n, then the next line has n space separated integers : Each integer is a clocks_number has been reset in this transition
+
+	Last line of the input can contain maximum 5 space separated integers : <stack_op> 
+	The value of first integer determine the stack operation
+	First interger is 0 : no stack operation
+	First interger is 1 : Only stack push operation, This integer will be followed by another integer : <stack_symbol_2>
+	First interger is 2 : Only stack pop operation, This integer will be followed by another three space separated integers : <stack_symbol> <lower_bound> <upper_bound>
+	First interger is 3 : Both pop and push happens at this transition, This integer will be followed by another four space separated integers : <stack_symbol> <lower_bound> <upper_bound> <stack_symbol_2>
+	where
+		<stack_symbol> : stack symbol number popped in this transition
+		<lower_bound> : lower bound on the age of the stack symbol currently popped in this transition
+		<upper_bound> : lower bound on the age of the stack symbol currently popped in this transition
+		<stack_symbol_2> : stack symbol number pushed in this transition		
+

input/t1

+6 5 2 3 0
+
+1
+
+6
+
+1 2 1 1 1
+2 5 -1
+2
+0
+
+2 3 0 1 0
+1 0 4
+0
+
+5 4 1 1 0
+1 0 4
+0
+
+1 5 0 1 1
+1 2 -1
+2
+0
+
+4 3 0 1 0
+2 5 -1
+0
+
+
+// edit the ages for checking emptiness

input/t10

+6 8 3 3 0
+
+1
+
+5
+
+1 2 0 1 0
+1 4 -1
+0
+
+1 3 1 1 1
+3 1 1
+2
+0
+
+2 6 0 2 0
+1 1 6
+2 0 1
+0
+
+3 4 1 0 2
+3 1
+0
+
+3 5 0 1 0
+1 0 0
+0
+
+4 5 2 2 0
+1 1 1
+2 0 0
+0
+
+6 3 3 1 0
+1 1 1
+0
+
+6 5 0 2 0
+1 0 1
+2 1 -1
+0
+
+00 00
+

input/t11

+7 8 4 3 0
+
+1
+
+7
+
+1 2 0 1 1
+2 5 -1
+1
+0
+
+1 3 1 1 2
+3 3 -1
+2 3
+0
+
+2 3 0 1 1
+1 2 2
+2
+0
+
+3 4 1 2 1
+3 0 5
+2 0 2
+3
+0
+
+4 5 0 1 1
+4 3 3
+4
+0
+
+4 6 2 1 2
+3 0 1
+3 4
+0
+
+5 6 3 2 1
+1 2 2
+2 2 2
+4
+0
+
+6 3 0 1 1
+4 1 1
+1
+0
+
+00 00
+

input/t13

+6 7 3 3 0
+
+1
+
+3
+
+1 4 0 2 2
+1 1 3
+2 2 2
+1 2
+0
+
+1 2 1 1 1
+3 3 -1
+2
+0
+
+2 3 2 1 1
+1 1 2
+3
+0
+
+2 5 3 1 1
+2 1 3
+3
+0
+
+4 3 2 1 1
+3 0 0
+1
+0
+
+
+5 6 1 2 0
+1 1 1
+3 2 2
+0
+
+
+6 1 0 1 1
+3 1 3
+2
+0
+
+
+00 00
+

input/t8

+4 6 2 4 0
+
+4
+
+3
+
+4 1 1 1 1
+1 0 -1
+2
+0
+
+1 2 2 1 0
+2 1 1
+0
+
+1 3 1 2 0
+1 0 0
+2 1 -1
+0
+
+2 3 3 1 0
+1 0 0
+0
+
+3 3 4 1 0
+1 2 -1
+0
+
+3 1 1 1 1
+2 0 0
+2
+0
+
+http://computerscience.unicam.it/tesei/pubdownload/T04Phd.pdf
+fig 2.5

input/tp2_0

+10 9 2 0 1
+
+1
+
+10
+
+1 2 0 0 1
+1
+0
+
+2 3 0 0 2
+1 2
+0
+
+3 4 0 0 1
+2
+0
+
+4 5 0 0 0
+1 1
+
+5 6 0 0 0
+0
+
+6 7 0 0 2
+1 2
+0
+
+7 8 0 1 0
+1 10 18
+0
+
+8 9 0 0 1
+1
+0
+
+9 10 0 0 0
+2 1 0 9
+
+
+M	Run_time
+1	0.000565
+2	0.001978
+3	0.008165
+4	0.023927
+5	0.083782
+6	0.15712
+7	0.375192
+8	0.672718
+9	1.28486
+10	2.00171
+12	4.94463
+14	10.8798
+16	21.9186
+18	bad memory allocation(#states : 5716700 )
\ No newline at end of file

input/tp38

+4 4 1 2 1
+
+4
+
+1
+
+1 2 1 1 0
+1 1 1
+0
+
+2 3 2 0 1
+1
+2 1 1 -1
+
+3 4 0 1 0
+1 0 0
+0
+
+
+4 1 0 0 1
+1
+1 1
+
+
+
+00 00
+
+|X| = 1
+|T| = 4
+|M| = 1
+

input/tp3_0

+10 9 3 0 1
+
+1
+
+10
+
+1 2 0 0 2
+2 3
+0
+
+2 3 0 0 1
+2
+0
+
+3 4 0 0 0
+1 1
+
+4 5 0 0 0
+0
+
+5 6 0 0 2
+1 2
+0
+
+6 7 0 0 2
+2 3
+0
+
+7 8 0 1 0
+1 7 12
+0
+
+8 9 0 0 1
+3
+0
+
+9 10 0 0 0
+2 1 0 6
+
+
+
+M	Run_time
+1	0.004453
+2	0.010471
+3	0.031199
+4	0.152298
+5	0.451474
+6	1.0779
+7	2.67533
+8	5.42333
+9	11.2027
+10	20.8801
+11	35.6042
+12 bad mem allocation(#states : 3526500)
\ No newline at end of file

input/tp6

+6 8 2 3 2
+
+1
+
+5
+
+1 2 0 1 0
+1 1 -1
+1 1
+
+1 3 1 1 1
+1 1 1
+2
+0
+
+2 6 0 2 0
+1 1 1
+2 0 3
+0
+
+3 4 1 0 2
+2 1
+0
+
+3 5 0 1 0
+1 0 0
+0
+
+4 5 2 2 0
+1 1 1
+2 0 0
+0
+
+6 3 3 1 0
+1 1 1
+0
+
+6 5 0 2 0
+1 0 1
+2 1 -1
+2 1 1 1
+
+00 00
+

input/tp60

+5 6 1 0 1
+
+1
+
+4
+
+1 2 0 1 0
+1 0 0
+0
+
+2 3 0 0 0
+1 1
+
+3 4 0 0 0
+0
+
+4 1 0 1 1
+1 0 2
+1
+2 1 0  -1
+
+3 5 0 0 1
+1
+0
+
+5 4 0 1 0
+1 0 0
+2 1 0 0
+
+
+00 00
+
+|X| = 1
+|T| = 3
+|M| = 5
+

input/tp62

+5 6 1 0 1
+
+1
+
+5
+
+1 2 0 0 1
+1
+1 1
+
+1 3 0 1 0
+1 3 -1
+0
+
+2 3 0 1 0
+1 1 -1
+0
+
+3 4 0 1 0
+1 3 100
+0
+
+3 5 0 1 0
+1 0 2
+0
+
+4 5 0 0 0
+2 1 2 3
+
+
+
+00 00
+
+|X| = 1
+|T| = 2
+|M| = 9
+

input/tp63

+5 8 1 2 2
+
+1
+
+5
+
+1 2 0 0 0
+1 2
+
+1 5 0 1 0 
+1 1 2
+2 2 6 8
+
+2 1 0 0 0
+0
+
+2 2 0 1 1
+1 1 1
+1
+1 1
+
+2 3 0 1 0
+1 0 1
+0
+
+3 4 0 0 0
+0
+
+4 2 0 1 0
+1 0 2
+0
+
+4 4 0 0 0
+2 1 1 2

input/tp64

+5 4 1 1 1
+
+1
+
+5
+
+1 2 0 0 0
+0
+
+2 3 0 0 0
+1 1
+
+3 4 0 0 0
+2 1 1 2
+
+4 5 0 0 0
+3 1 0 -1 1
+
+

input/tp67

+14 26 1 1 2
+
+1
+
+1
+
+
+1 2 0 0 0
+1 1
+
+2 3 0 0 0
+0
+
+3 2 0 0 0
+0
+
+3 4 0 0 0
+0
+
+4 3 0 0 0
+0
+
+4 5 0 0 0
+0
+
+5 4 0 0 0
+0
+
+5 6 0 0 0
+0
+
+6 5 0 0 0
+0
+
+6 7 0 0 0
+0
+
+7 6 0 0 0
+0
+
+7 8 0 0 0
+0
+
+8 7 0 0 0
+0
+
+8 9 0 0 0
+0
+
+9 8 0 0 0
+0
+
+9 10 0 0 0
+0
+
+10 9 0 0 0
+0
+
+10 11  0 0 0
+0
+
+11 10 0 0 0
+0
+
+11  12 0 0 0
+0
+
+12 11 0 0 0
+0
+
+12 13 0 0 0
+0
+
+13 12 0 0 0
+0
+
+13 14 0 0 0
+0
+
+14 13 0 0 0
+0
+
+2 1 0 1 0
+1 6 10
+2 1 11 15
+
+
+
+
+T 	Time
+2	0.000355
+4	0.134996
+6	0.223448
+8	0.281873
+10	0.381145
+12	0.526717
+14	0.650515
+16	0.772484
+18	0.836541
+20	1.01429
+22	1.04948
+24	1.15572
+26	1.26705

input/tpd1

+8 7 1 0 2
+
+1
+8
+
+1 2 0 0 1
+1
+0
+
+2 3 0 0 0
+1 1
+
+3 4 0 0 1
+1
+3 1 1 1 2
+
+4 5 0 0 0
+2 2 1 -1
+
+5 6 0 0 1
+1
+0
+
+6 7 0 0 0
+1 1
+
+7 8 0 0 0
+2 1 1 -1
+
+
+ 0 0 0
+
+ 0 0 0

input/tpdis0

+26 24 16 0 0
+
+1
+
+26
+
+1 2 0 0 1
+1
+0
+
+2 3 0 0 1
+2
+0
+
+3 4 0 0 1
+3
+0
+
+4 5 0 0 1
+4
+0
+
+5 6 0 0 1
+5
+0
+
+6 7 0 0 1
+6
+0
+
+7 8 0 0 1
+7
+0
+
+8 9 0 0 1
+8
+0
+
+9 10 0 0 1
+9
+0
+
+10 11 0 0 1
+10
+0
+
+11 12 0 0 1
+11
+0
+
+12 13 0 0 1
+12
+0
+
+13 14 0 0 1
+13
+0
+
+14 15 0 0 1
+14
+0
+
+15 16 0 0 1
+15
+0
+
+16 17 0 0 1
+16
+0
+
+17 18 0 2 0
+9 1 1
+1 2 2
+0
+
+18 19 0 2 0
+10 1 1
+2 2 2
+0
+
+19 20 0 2 0
+11 1 1
+3 2 2
+0
+
+20 21 0 2 0
+12 1 1
+4 2 2
+0
+
+21 22 0 2 0
+13 1 1
+5 2 2
+0
+
+22 23 0 2 0
+14 1 1
+6 2 2
+0
+
+23 24 0 2 0
+15 1 1
+7 2 2
+0
+
+24 25 0 2 0
+16 1 1
+8 2 2
+0
+

input/tpg0

+8 6 2 0 1
+
+1
+
+8
+
+
+1 2 0 1 1
+1 3 11
+2
+0
+
+2 3 0 1 1
+2 2 13
+2
+0
+
+3 4 0 1 0
+2 1 15
+1 1
+
+4 5 0 1 1 
+2 0 10
+1
+1 1
+
+5 6 0 0 1
+1
+2 1 2 6
+
+6 7 0 1 1
+2 0 -1
+2
+2 1 3 9
+

input/tpg1

+12 11 2 0 2
+
+1
+
+12
+
+1 2 0 1 1
+1 0 0
+1
+0
+
+2 3 0 1 0
+1 0 0
+1 1
+
+3 4 0 1 1
+2 0 0
+2
+0
+
+4 5 0 0 0
+1 1
+
+5 6 0 1 0
+1 0 0
+0
+
+6 7 0 1 2
+2 0 0
+1 2
+2 1 0 0
+
+7 8 0 0 0
+3 1 0 0 2
+
+8 9 0 1 1
+1 0 0
+2
+0
+
+9 10 0 1 2
+2 0 0
+1 2
+0
+
+10 11 0 1 1
+1 0 0
+1
+0
+
+11 12 0 1 0
+1 0 0
+2 2 0 0

input/tpg11

+8 8 1 1 2
+
+1
+
+8
+
+1 2 0 0 0
+1 2
+
+2 3 0 1 0
+1 0 -1
+1 1
+
+3 4 0 0 1
+1
+2 1 1 2
+
+4 5 0 0 0
+1 1
+
+
+5 6 0 1 0
+1 1 1
+2 1 0 -1
+
+6 1 0 1 1
+1 0 1
+1
+2 2 0 1
+
+2 7 0 1 1
+1 1 2
+1
+1 2
+
+7 3 0 1 1
+1 1 2
+1
+2 2 2 2

input/tpg2

+6 6 1 1 2
+
+1
+
+1
+
+1 2 0 0 0
+1 2
+
+2 3 0 1 0
+1 0 -1
+1 1
+
+3 4 0 0 1
+1
+2 1 1 5
+
+4 5 0 0 0
+1 1
+
+
+5 6 0 1 0
+1 1 1
+2 1 0 -1
+
+6 1 0 1 1
+1 0 1
+1
+2 2 0 1

input/tpg9

+10 14 1 1 3
+
+1
+
+6
+
+1 2 0 0 1
+1
+1 1
+
+1 9 0 0 0
+1 2
+
+2 8 0 1 0
+1 4 5
+0
+
+3 2 0 0 1
+1
+0
+
+4 3 0 1 0
+1 3 5
+0
+
+4 5 0 1 0
+1 1 2
+0
+
+5 6 0 0 0
+2 2 1 2
+
+6 7 0 0 0
+1 3
+
+7 10 0 0 1
+1
+2 3 0 5
+
+8 4 0 1 0
+1 3 4
+0
+
+8 6 0 0 0
+2 1 2 3
+
+9 7 0 1 0
+1 4 5
+0
+
+9 8 0 0 1
+1
+0
+
+10 1 0 1 1
+1 1 -1
+1
+0
+

input/tps10

+4 5 1 1 2
+
+1
+
+1
+
+1 2 0 1 1
+1 0 2
+1
+1 1
+
+1 3 0 1 1
+1 1 1
+1
+1 2
+
+2 3 0 1 1
+1 3 4
+1
+1 2
+
+3 4 0 1 1
+1 2 6
+1
+2 2 3 7
+
+4 1 0 1 1
+1 6 8
+1
+2 1 5 10

input/tps11

+5 6 1 1 2
+
+1
+
+1
+
+1 2 0 1 1
+1 0 2
+1
+1 1
+
+1 5 0 1 1
+1 2 4
+1
+1 1
+
+2 3 0 1 1
+1 3 4
+1
+1 2
+
+3 4 0 1 1
+1 2 6
+1
+2 2 3 7
+
+4 1 0 1 1
+1 6 8
+1
+2 1 5 10
+
+5 3 0 1 1
+1 1 4
+1
+1 2

input/tps2

+4 6 1 0 2
+
+1
+
+4
+
+1 2 0 1 1
+1 0 0
+1
+1 2
+
+2 2 0 1 1
+1 0 0
+1
+1 1
+
+2 3 0 1 1
+1 0 0
+1
+0
+
+3 2 0 1 1
+1 0 0 
+1
+0
+
+3 3 0 1 1
+1 1 1
+1
+2 1 0 -1
+
+3 4 0 1 1
+1 0 0
+1
+2 2 2 2

input/tps4

+6 6 1 0 2
+
+1
+
+6
+
+1 2 0 0 1
+1
+1 1
+
+2 3 0 1 1
+1 1 1
+1
+1 2
+
+3 4 0 0 0
+2 2 0 1
+
+4 1 0 0 0
+2 1 1 1
+
+1 5 0 0 1
+1
+0
+
+5 3 0 1 0
+1 0 1
+0
+
+

input/tps5

+5 8 1 1 2
+
+1
+5
+
+1 1 0 1 1
+1 0 0
+1
+1 1
+
+1 2 0 1 1
+1 0 0
+1
+1 2
+
+2 1 0 1 1
+1 1 2
+1
+0
+
+2 3 0 1 1
+1 3 3
+1
+0
+
+3 1 0 1 1
+1 0 0
+1
+0
+
+3 4 0 1 1
+1 0 0
+1
+2 2 0 -1
+
+4 3 0 1 1
+1 1 1
+1
+0
+
+1 5 0 1 1
+1 0 0
+1
+2 1 6 6

input/tps9

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

main.cpp

+#include<math.h> // c headers
+#include<string.h>
+#include <time.h>
+
+#include <string> // c++ headers
+#include<vector>
+
+#include"timePushDown.h" // TPDA file processing, representation(all info about the TPDA is in this file)
+#include"treeBitOperations.h" // bit wise operations
+
+#include"pds.h" // system with no extra clocks
+#include"tpda2.h" // one clock special kind of TPDA
+#include<continuoustpda.h> // one clock TPDA
+#include<tpdaCGPP.h> // general TPDA
+#include<tpdaZone.h> // general TPDA with zone
+
+
+using namespace std;
+
+
+// process the input TPDA file and set all the global variables according to the TPDA
+void setGlobal(char *filename) {
+
+	setBits(); // set variables for bitwise operations(defined in "treeBitOperations.h")
+	
+	M = 0; // set maximum constant to 0, we update it when reading the system
+	
+	strcpy(inputfilename, filename); // copy the input timed system input file name to the variable 'inputfilename'
+	
+	inputSystem(); // process the input TPDA(defined in "timePushDown.h")
+	
+	if(X != 0)
+		getresecktrans(); // which are the compatible reset transition with some check transition
+	
+	M = M + 1; // maximum constant for the system(computed M in the function inputSystem() + 1 )
+	
+	if(X == 0) // no clock, push-down system, tree-width 2, so #colors = 3
+		K = 3;
+	else if(AS == 0) // #stack symbols = 0, timed automata, tree-width X+1, #colors = X+2
+		K = X+2;
+	else // TIMED push-down system, tree width 3K+2
+		K = 3*X + 3; 
+}
+
+
+// calculate 2^x
+inline unsigned int p2(unsigned int x) {
+	return (1 << x);
+}
+
+
+// string to integer conversion
+int str_to_int(string s) {
+	int sum = 0;
+	for(int i=0; i < s.size(); i++) {
+		sum = sum*10 + s[i]-'0';
+	}
+	return sum;
+}
+
+
+
+
+// MAIN PROGRAM
+int main(int argc, char *argv[]) {
+	
+	// Command line arguments : 
+		// first argument(argv[1]) : input TPDA text file with specific format
+		/* Second argument(argv[2]) : 
+				1 : TPDA with no extra clock, but there can be constraints on ages of stack symbols
+				2 : special kind of TPDA with one clock x(x must be reset in all transitions just before some check transitoin on clock x )
+				3 : general TPDA with one clock
+				No arg : general TPDA with one or more clocks
+		*/
+	
+	
+	if(argc < 2) {
+		cout << "Input TPDA file must be given !" << endl;
+		return 0;
+	}
+	
+	clock_t start = clock(); // Start measuring time
+	
+	////**********////
+	setGlobal(argv[1]); // set all the global variables
+	
+	bool b;
+	
+	if(argc >= 3) { // If there is any arguments for special kind of TPDA
+	
+		int x = str_to_int(argv[2]);
+		
+		if(x == 1) //TPDA with no extra clock, but there can be constraints on ages of stack symbols
+			b = pdsempty();
+			
+		else if(x == 2) // special kind of TPDA with one clock x(x must be reset in all transitions just before some check transitoin on clock x )
+			b = isEmptySTPDA();
+			
+		else if(x == 3) // general TPDA with one clock
+			b = isEmptyTPDA();
+		else if(x == 4)
+			b = isEmptyZone();
+	}
+	
+	else // general TPDA with one or more clocks
+		b = isEmptyGCPP();
+	
+	// the returned value b will be true iff the language is empty
+	
+	if(b)
+		cout << "The language recognized by the TPDA is EMPTY!" << endl;
+		
+	else
+		cout << "The language recognized by the TPDA is NOT EMPTY!" << endl;
+	
+	cout << endl;
+	
+	if(AS == 0) // no stacks
+		cout << "#stacks : " << 0 << endl;
+	else // one stack
+		cout << "#stacks : " << 1 << endl;
+		
+	cout << "#clocks : " << int(X) << endl;
+	cout << "#states : " << int(S) << endl;
+	cout << "#transitions : " << int(T) << endl;
+	cout << "Maximum constant(M) : " << int(M) << endl;
+	cout << "Tree-Width(K) : " << int(K-1) << endl;
+	
+	cout << endl << "---END OF EXECUTION---" << endl << endl;
+	
+	clock_t stop = clock(); // end of time calculation
+	
+	double elapsed = (double)(stop - start) * 1000.0 / CLOCKS_PER_SEC; // Time elapsed calculation 
+	  
+	cout << "Execution time : " << (elapsed/1000) << " seconds." << endl << endl;
+	
+	/*
+	short **w;
+	bool **open;
+	int n;
+	cout << "n : ";
+	cin >> n;
+	w = new short*[n];
+	open = new bool*[n];
+	for(char i=0; i < n; i++) {
+		w[i] = new short[n];
+		open[i] = new bool[n];
+		for(char j=0; j < n; j++) {
+			cin >> w[i][j];
+		}
+	}
+
+	for(char i=0; i < n; i++) {
+		for(char j=0; j < n; j++) {
+			cout << w[i][j] << "\t";
+		}
+		cout << endl;
+	}
+
+	allPairSP(w, open, n);
+
+
+	for(char i=0; i < n; i++) {
+		for(char j=0; j < n; j++) {
+			cout << w[i][j] << "\t";
+		}
+		cout << endl;
+	}
+	*/
+	
+	return 0;
+}

makefile

+CC  :=  g++
+CFLAG := -lm -std=c++11
+SRC := ./src
+OBJ := ./obj
+INC := ./include
+EXE := tree
+GDB := -g
+
+
+tree : main.o $(OBJ)/treeBitOperations.o $(OBJ)/timePushDown.o $(OBJ)/continuoustpda.o $(OBJ)/pds.o $(OBJ)/tpdaCGPP.o $(OBJ)/tpdaZone.o $(OBJ)/tpda2.o drawsystem
+	g++ $(GDB) main.o $(OBJ)/treeBitOperations.o $(OBJ)/timePushDown.o $(OBJ)/continuoustpda.o $(OBJ)/pds.o $(OBJ)/tpdaCGPP.o $(OBJ)/tpdaZone.o $(OBJ)/tpda2.o -o $(EXE) $(CFLAG)
+
+main.o : main.cpp
+	g++ $(GDB) -I $(INC) -c main.cpp -o main.o $(CFLAG)
+	
+$(OBJ)/tpdaZone.o : $(SRC)/tpdaZone.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/tpdaZone.cpp -o $(OBJ)/tpdaZone.o $(CFLAG)
+	
+$(OBJ)/tpdaCGPP.o : $(SRC)/tpdaCGPP.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/tpdaCGPP.cpp -o $(OBJ)/tpdaCGPP.o $(CFLAG)
+	
+$(OBJ)/continuoustpda.o : $(SRC)/continuoustpda.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/continuoustpda.cpp -o $(OBJ)/continuoustpda.o $(CFLAG)
+	
+$(OBJ)/tpda2.o : $(SRC)/tpda2.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/tpda2.cpp -o $(OBJ)/tpda2.o $(CFLAG)
+	
+$(OBJ)/pds.o : $(SRC)/pds.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/pds.cpp -o $(OBJ)/pds.o $(CFLAG)
+
+drawsystem : $(OBJ)/drawsystem.o $(OBJ)/treeBitOperations.o
+	g++ $(GDB) $(OBJ)/drawsystem.o $(OBJ)/treeBitOperations.o -o drawsystem $(CFLAG)
+	
+$(OBJ)/drawsystem.o : $(SRC)/drawsystem.cpp 
+	g++ $(GDB) -I $(INC) -c $(SRC)/drawsystem.cpp -o $(OBJ)/drawsystem.o $(CFLAG)	
+	
+$(OBJ)/timePushDown.o : $(SRC)/timePushDown.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/timePushDown.cpp -o $(OBJ)/timePushDown.o $(CFLAG)
+	
+$(OBJ)/treeBitOperations.o : $(SRC)/treeBitOperations.cpp
+	g++ $(GDB) -I $(INC) -c $(SRC)/treeBitOperations.cpp -o $(OBJ)/treeBitOperations.o $(CFLAG)

nbproject/configurations.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<configurationDescriptor version="100">
+  <logicalFolder name="root" displayName="root" projectFiles="true" kind="ROOT">
+    <df root="." name="0">
+      <df name="src">
+        <in>continuoustpda.cpp</in>
+        <in>drawsystem.cpp</in>
+        <in>pds.cpp</in>
+        <in>timePushDown.cpp</in>
+        <in>tpda2.cpp</in>
+        <in>tpdaCGPP.cpp</in>
+        <in>tpdaZone.cpp</in>
+        <in>treeBitOperations.cpp</in>
+      </df>
+      <in>main.cpp</in>
+    </df>
+    <logicalFolder name="ExternalFiles"
+                   displayName="Important Files"
+                   projectFiles="false"
+                   kind="IMPORTANT_FILES_FOLDER">
+      <itemPath>nbproject/private/launcher.properties</itemPath>
+      <itemPath>makefile</itemPath>
+    </logicalFolder>
+  </logicalFolder>
+  <sourceFolderFilter>^(nbproject)$</sourceFolderFilter>
+  <sourceRootList>
+    <Elem>.</Elem>
+  </sourceRootList>
+  <projectmakefile>makefile</projectmakefile>
+  <confs>
+    <conf name="Default" type="0">
+      <toolsSet>
+        <compilerSet>default</compilerSet>
+        <dependencyChecking>false</dependencyChecking>
+        <rebuildPropChanged>false</rebuildPropChanged>
+      </toolsSet>
+      <flagsDictionary>
+        <element flagsID="0" commonFlags="-std=c++11"/>
+      </flagsDictionary>
+      <codeAssistance>
+      </codeAssistance>
+      <makefileType>
+        <makeTool>
+          <buildCommandWorkingDir>.</buildCommandWorkingDir>
+          <buildCommand>${MAKE} -f makefile</buildCommand>
+          <cleanCommand>${MAKE} -f makefile clean</cleanCommand>
+          <executablePath></executablePath>
+          <ccTool>
+            <incDir>
+              <pElem>include</pElem>
+            </incDir>
+          </ccTool>
+        </makeTool>
+        <preBuild>
+          <preBuildCommandWorkingDir>.</preBuildCommandWorkingDir>
+          <preBuildCommand></preBuildCommand>
+        </preBuild>
+      </makefileType>
+      <folder path="0/src">
+        <ccTool>
+          <incDir>
+            <pElem>.</pElem>
+          </incDir>
+        </ccTool>
+      </folder>
+      <item path="main.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/continuoustpda.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/drawsystem.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/pds.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/timePushDown.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/tpda2.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/tpdaCGPP.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/tpdaZone.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+      <item path="src/treeBitOperations.cpp" ex="false" tool="1" flavor2="8">
+        <ccTool flags="0">
+        </ccTool>
+      </item>
+    </conf>
+  </confs>
+</configurationDescriptor>

nbproject/private/CodeAssistancePathMapper.properties

+# Automatic path mapper. CRC = 1

nbproject/private/Default-build.log

+g++ -g -I ./include -c main.cpp -o main.o -lm -std=c++11
+g++ -g -I ./include -c ./src/treeBitOperations.cpp -o ./obj/treeBitOperations.o -lm -std=c++11
+g++ -g -I ./include -c ./src/timePushDown.cpp -o ./obj/timePushDown.o -lm -std=c++11
+g++ -g -I ./include -c ./src/continuoustpda.cpp -o ./obj/continuoustpda.o -lm -std=c++11
+g++ -g -I ./include -c ./src/pds.cpp -o ./obj/pds.o -lm -std=c++11
+g++ -g -I ./include -c ./src/tpdaCGPP.cpp -o ./obj/tpdaCGPP.o -lm -std=c++11
+g++ -g -I ./include -c ./src/tpdaZone.cpp -o ./obj/tpdaZone.o -lm -std=c++11
+g++ -g -I ./include -c ./src/tpda2.cpp -o ./obj/tpda2.o -lm -std=c++11
+g++ -g -I ./include -c ./src/drawsystem.cpp -o ./obj/drawsystem.o -lm -std=c++11	
+g++ -g ./obj/drawsystem.o ./obj/treeBitOperations.o -o drawsystem -lm -std=c++11
+g++ -g main.o ./obj/treeBitOperations.o ./obj/timePushDown.o ./obj/continuoustpda.o ./obj/pds.o ./obj/tpdaCGPP.o ./obj/tpdaZone.o ./obj/tpda2.o -o tree -lm -std=c++11

nbproject/private/Default-exec.log

+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	main.cpp
+	-o
+	main.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/treeBitOperations.cpp
+	-o
+	./obj/treeBitOperations.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/timePushDown.cpp
+	-o
+	./obj/timePushDown.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/continuoustpda.cpp
+	-o
+	./obj/continuoustpda.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/pds.cpp
+	-o
+	./obj/pds.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/tpdaCGPP.cpp
+	-o
+	./obj/tpdaCGPP.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/tpdaZone.cpp
+	-o
+	./obj/tpdaZone.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/tpda2.cpp
+	-o
+	./obj/tpda2.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	-I
+	./include
+	-c
+	./src/drawsystem.cpp
+	-o
+	./obj/drawsystem.o
+	-lm
+	-std=c++11
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	./obj/drawsystem.o
+	./obj/treeBitOperations.o
+	-o
+	drawsystem
+	-lm
+	-std=c++11
+
+called: /usr/bin/ld
+	/home/sparsa/Programming/mtp
+	/usr/bin/ld
+	-plugin
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/liblto_plugin.so
+	-plugin-opt=/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/lto-wrapper
+	-plugin-opt=-fresolution=/tmp/cciKZpSO.res
+	-plugin-opt=-pass-through=-lgcc_s
+	-plugin-opt=-pass-through=-lgcc
+	-plugin-opt=-pass-through=-lc
+	-plugin-opt=-pass-through=-lgcc_s
+	-plugin-opt=-pass-through=-lgcc
+	--build-id
+	--eh-frame-hdr
+	--hash-style=gnu
+	-m
+	elf_x86_64
+	-dynamic-linker
+	/lib64/ld-linux-x86-64.so.2
+	-o
+	drawsystem
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib/crt1.o
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib/crti.o
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/crtbegin.o
+	-L/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1
+	-L/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib
+	-L/lib/../lib
+	-L/usr/lib/../lib
+	-L/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../..
+	./obj/drawsystem.o
+	./obj/treeBitOperations.o
+	-lstdc++
+	-lm
+	-lgcc_s
+	-lgcc
+	-lc
+	-lgcc_s
+	-lgcc
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/crtend.o
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib/crtn.o
+
+called: g++
+	/home/sparsa/Programming/mtp
+	g++
+	-g
+	main.o
+	./obj/treeBitOperations.o
+	./obj/timePushDown.o
+	./obj/continuoustpda.o
+	./obj/pds.o
+	./obj/tpdaCGPP.o
+	./obj/tpdaZone.o
+	./obj/tpda2.o
+	-o
+	tree
+	-lm
+	-std=c++11
+
+called: /usr/bin/ld
+	/home/sparsa/Programming/mtp
+	/usr/bin/ld
+	-plugin
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/liblto_plugin.so
+	-plugin-opt=/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/lto-wrapper
+	-plugin-opt=-fresolution=/tmp/cctG1Nkd.res
+	-plugin-opt=-pass-through=-lgcc_s
+	-plugin-opt=-pass-through=-lgcc
+	-plugin-opt=-pass-through=-lc
+	-plugin-opt=-pass-through=-lgcc_s
+	-plugin-opt=-pass-through=-lgcc
+	--build-id
+	--eh-frame-hdr
+	--hash-style=gnu
+	-m
+	elf_x86_64
+	-dynamic-linker
+	/lib64/ld-linux-x86-64.so.2
+	-o
+	tree
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib/crt1.o
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib/crti.o
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/crtbegin.o
+	-L/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1
+	-L/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib
+	-L/lib/../lib
+	-L/usr/lib/../lib
+	-L/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../..
+	main.o
+	./obj/treeBitOperations.o
+	./obj/timePushDown.o
+	./obj/continuoustpda.o
+	./obj/pds.o
+	./obj/tpdaCGPP.o
+	./obj/tpdaZone.o
+	./obj/tpda2.o
+	-lstdc++
+	-lm
+	-lgcc_s
+	-lgcc
+	-lc
+	-lgcc_s
+	-lgcc
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/crtend.o
+	/usr/lib/gcc/x86_64-pc-linux-gnu/7.1.1/../../../../lib/crtn.o
+

nbproject/private/Default.properties

+/home/sparsa/Programming/mtp/src/tpdaCGPP.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/tpdaCGPP.cpp -o ./obj/tpdaCGPP.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/timePushDown.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/timePushDown.cpp -o ./obj/timePushDown.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/tpda2.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/tpda2.cpp -o ./obj/tpda2.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/drawsystem.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/drawsystem.cpp -o ./obj/drawsystem.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/continuoustpda.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/continuoustpda.cpp -o ./obj/continuoustpda.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/tpdaZone.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/tpdaZone.cpp -o ./obj/tpdaZone.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/treeBitOperations.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/treeBitOperations.cpp -o ./obj/treeBitOperations.o -lm -std=c++11
+/home/sparsa/Programming/mtp/src/pds.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c ./src/pds.cpp -o ./obj/pds.o -lm -std=c++11
+/home/sparsa/Programming/mtp/main.cpp=/home/sparsa/Programming/mtp#-g -I ./include -c main.cpp -o main.o -lm -std=c++11

nbproject/private/c_standard_headers_indexer.c

+/*
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS HEADER.
+ *
+ * Copyright (c) 2016 Oracle and/or its affiliates. All rights reserved.
+ *
+ * Oracle and Java are registered trademarks of Oracle and/or its affiliates.
+ * Other names may be trademarks of their respective owners.
+ *
+ * The contents of this file are subject to the terms of either the GNU
+ * General Public License Version 2 only ("GPL") or the Common
+ * Development and Distribution License("CDDL") (collectively, the
+ * "License"). You may not use this file except in compliance with the
+ * License. You can obtain a copy of the License at
+ * http://www.netbeans.org/cddl-gplv2.html
+ * or nbbuild/licenses/CDDL-GPL-2-CP. See the License for the
+ * specific language governing permissions and limitations under the
+ * License.  When distributing the software, include this License Header
+ * Notice in each file and include the License file at
+ * nbbuild/licenses/CDDL-GPL-2-CP.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the GPL Version 2 section of the License file that
+ * accompanied this code. If applicable, add the following below the
+ * License Header, with the fields enclosed by brackets [] replaced by
+ * your own identifying information:
+ * "Portions Copyrighted [year] [name of copyright owner]"
+ *
+ * If you wish your version of this file to be governed by only the CDDL
+ * or only the GPL Version 2, indicate your decision by adding
+ * "[Contributor] elects to include this software in this distribution
+ * under the [CDDL or GPL Version 2] license." If you do not indicate a
+ * single choice of license, a recipient has the option to distribute
+ * your version of this file under either the CDDL, the GPL Version 2 or
+ * to extend the choice of license to its licensees as provided above.
+ * However, if you add GPL Version 2 code and therefore, elected the GPL
+ * Version 2 license, then the option applies only if the new code is
+ * made subject to such option by the copyright holder.
+ *
+ * Contributor(s):
+ */
+
+// List of standard headers was taken in http://en.cppreference.com/w/c/header
+
+#include <assert.h> 	 // Conditionally compiled macro that compares its argument to zero
+#include <ctype.h> 	 // Functions to determine the type contained in character data
+#include <errno.h> 	 // Macros reporting error conditions
+#include <float.h> 	 // Limits of float types
+#include <limits.h> 	 // Sizes of basic types
+#include <locale.h> 	 // Localization utilities
+#include <math.h> 	 // Common mathematics functions
+#include <setjmp.h> 	 // Nonlocal jumps
+#include <signal.h> 	 // Signal handling
+#include <stdarg.h> 	 // Variable arguments
+#include <stddef.h> 	 // Common macro definitions
+#include <stdio.h> 	 // Input/output
+#include <string.h> 	 // String handling
+#include <stdlib.h> 	 // General utilities: memory management, program utilities, string conversions, random numbers
+#include <time.h> 	 // Time/date utilities
+#include <iso646.h>      // (since C95) Alternative operator spellings
+#include <wchar.h>       // (since C95) Extended multibyte and wide character utilities
+#include <wctype.h>      // (since C95) Wide character classification and mapping utilities
+#ifdef _STDC_C99
+#include <complex.h>     // (since C99) Complex number arithmetic
+#include <fenv.h>        // (since C99) Floating-point environment
+#include <inttypes.h>    // (since C99) Format conversion of integer types
+#include <stdbool.h>     // (since C99) Boolean type
+#include <stdint.h>      // (since C99) Fixed-width integer types
+#include <tgmath.h>      // (since C99) Type-generic math (macros wrapping math.h and complex.h)
+#endif
+#ifdef _STDC_C11
+#include <stdalign.h>    // (since C11) alignas and alignof convenience macros
+#include <stdatomic.h>   // (since C11) Atomic types
+#include <stdnoreturn.h> // (since C11) noreturn convenience macros
+#include <threads.h>     // (since C11) Thread library
+#include <uchar.h>       // (since C11) UTF-16 and UTF-32 character utilities
+#endif

nbproject/private/configurations.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<configurationDescriptor version="100">
+  <logicalFolder name="root" displayName="root" projectFiles="true" kind="ROOT">
+    <df root="." name="0">
+      <df name="include">
+        <in>continuoustpda.h</in>
+        <in>drawsystem.h</in>
+        <in>pds.h</in>
+        <in>timePushDown.h</in>
+        <in>tpda2.h</in>
+        <in>tpdaCGPP.h</in>
+        <in>tpdaZone.h</in>
+        <in>treeBitOperations.h</in>
+      </df>
+      <df name="input">
+      </df>
+      <df name="obj">
+      </df>
+      <df name="src">
+        <in>continuoustpda.cpp</in>
+        <in>drawsystem.cpp</in>
+        <in>pds.cpp</in>
+        <in>timePushDown.cpp</in>
+        <in>tpda2.cpp</in>
+        <in>tpdaCGPP.cpp</in>
+        <in>tpdaZone.cpp</in>
+        <in>treeBitOperations.cpp</in>
+      </df>
+      <in>main.cpp</in>
+    </df>
+  </logicalFolder>
+  <projectmakefile>makefile</projectmakefile>
+  <confs>
+    <conf name="Default" type="0">
+      <toolsSet>
+        <developmentServer>localhost</developmentServer>
+        <platform>2</platform>
+      </toolsSet>
+      <compile>
+        <compiledirpicklist>
+          <compiledirpicklistitem>.</compiledirpicklistitem>
+          <compiledirpicklistitem>${AUTO_FOLDER}</compiledirpicklistitem>
+        </compiledirpicklist>
+        <compiledir>${AUTO_FOLDER}</compiledir>
+        <compilecommandpicklist>
+          <compilecommandpicklistitem>${MAKE} ${ITEM_NAME}.o</compilecommandpicklistitem>
+          <compilecommandpicklistitem>${AUTO_COMPILE}</compilecommandpicklistitem>
+        </compilecommandpicklist>
+        <compilecommand>${AUTO_COMPILE}</compilecommand>
+      </compile>
+      <dbx_gdbdebugger version="1">
+        <gdb_pathmaps>
+        </gdb_pathmaps>
+        <gdb_interceptlist>
+          <gdbinterceptoptions gdb_all="false" gdb_unhandled="true" gdb_unexpected="true"/>
+        </gdb_interceptlist>
+        <gdb_options>
+          <DebugOptions>
+          </DebugOptions>
+        </gdb_options>
+        <gdb_buildfirst gdb_buildfirst_overriden="false" gdb_buildfirst_old="false"/>
+      </dbx_gdbdebugger>
+      <nativedebugger version="1">
+        <engine>gdb</engine>
+      </nativedebugger>
+      <runprofile version="9">
+        <runcommandpicklist>
+          <runcommandpicklistitem>"${OUTPUT_PATH}"</runcommandpicklistitem>
+        </runcommandpicklist>
+        <runcommand>"${OUTPUT_PATH}"</runcommand>
+        <rundir>.</rundir>
+        <buildfirst>false</buildfirst>
+        <terminal-type>0</terminal-type>
+        <remove-instrumentation>0</remove-instrumentation>
+        <environment>
+        </environment>
+      </runprofile>
+    </conf>
+  </confs>
+</configurationDescriptor>

nbproject/private/cpp_standard_headers_indexer.cpp

+/*
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS HEADER.
+ *
+ * Copyright (c) 2016 Oracle and/or its affiliates. All rights reserved.
+ *
+ * Oracle and Java are registered trademarks of Oracle and/or its affiliates.
+ * Other names may be trademarks of their respective owners.
+ *
+ * The contents of this file are subject to the terms of either the GNU
+ * General Public License Version 2 only ("GPL") or the Common
+ * Development and Distribution License("CDDL") (collectively, the
+ * "License"). You may not use this file except in compliance with the
+ * License. You can obtain a copy of the License at
+ * http://www.netbeans.org/cddl-gplv2.html
+ * or nbbuild/licenses/CDDL-GPL-2-CP. See the License for the
+ * specific language governing permissions and limitations under the
+ * License.  When distributing the software, include this License Header
+ * Notice in each file and include the License file at
+ * nbbuild/licenses/CDDL-GPL-2-CP.  Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the GPL Version 2 section of the License file that
+ * accompanied this code. If applicable, add the following below the
+ * License Header, with the fields enclosed by brackets [] replaced by
+ * your own identifying information:
+ * "Portions Copyrighted [year] [name of copyright owner]"
+ *
+ * If you wish your version of this file to be governed by only the CDDL
+ * or only the GPL Version 2, indicate your decision by adding
+ * "[Contributor] elects to include this software in this distribution
+ * under the [CDDL or GPL Version 2] license." If you do not indicate a
+ * single choice of license, a recipient has the option to distribute
+ * your version of this file under either the CDDL, the GPL Version 2 or
+ * to extend the choice of license to its licensees as provided above.
+ * However, if you add GPL Version 2 code and therefore, elected the GPL
+ * Version 2 license, then the option applies only if the new code is
+ * made subject to such option by the copyright holder.
+ *
+ * Contributor(s):
+ */
+
+// List of standard headers was taken in http://en.cppreference.com/w/cpp/header
+
+#include <cstdlib> 	    // General purpose utilities: program control, dynamic memory allocation, random numbers, sort and search
+#include <csignal> 	    // Functions and macro constants for signal management
+#include <csetjmp> 	    // Macro (and function) that saves (and jumps) to an execution context
+#include <cstdarg> 	    // Handling of variable length argument lists
+#include <typeinfo> 	    // Runtime type information utilities
+#include <bitset> 	    // std::bitset class template
+#include <functional> 	    // Function objects, designed for use with the standard algorithms
+#include <utility> 	    // Various utility components
+#include <ctime> 	    // C-style time/date utilites
+#include <cstddef> 	    // typedefs for types such as size_t, NULL and others
+#include <new> 	            // Low-level memory management utilities
+#include <memory> 	    // Higher level memory management utilities
+#include <climits>          // limits of integral types
+#include <cfloat> 	    // limits of float types
+#include <limits> 	    // standardized way to query properties of arithmetic types
+#include <exception> 	    // Exception handling utilities
+#include <stdexcept> 	    // Standard exception objects
+#include <cassert> 	    // Conditionally compiled macro that compares its argument to zero
+#include <cerrno>           // Macro containing the last error number
+#include <cctype>           // functions to determine the type contained in character data
+#include <cwctype>          // functions for determining the type of wide character data
+#include <cstring> 	    // various narrow character string handling functions
+#include <cwchar> 	    // various wide and multibyte string handling functions
+#include <string> 	    // std::basic_string class template
+#include <vector> 	    // std::vector container
+#include <deque> 	    // std::deque container
+#include <list> 	    // std::list container
+#include <set> 	            // std::set and std::multiset associative containers
+#include <map> 	            // std::map and std::multimap associative containers
+#include <stack> 	    // std::stack container adaptor
+#include <queue> 	    // std::queue and std::priority_queue container adaptors
+#include <algorithm> 	    // Algorithms that operate on containers
+#include <iterator> 	    // Container iterators
+#include <cmath>            // Common mathematics functions
+#include <complex>          // Complex number type
+#include <valarray>         // Class for representing and manipulating arrays of values
+#include <numeric>          // Numeric operations on values in containers
+#include <iosfwd>           // forward declarations of all classes in the input/output library
+#include <ios>              // std::ios_base class, std::basic_ios class template and several typedefs
+#include <istream>          // std::basic_istream class template and several typedefs
+#include <ostream>          // std::basic_ostream, std::basic_iostream class templates and several typedefs
+#include <iostream>         // several standard stream objects
+#include <fstream>          // std::basic_fstream, std::basic_ifstream, std::basic_ofstream class templates and several typedefs
+#include <sstream>          // std::basic_stringstream, std::basic_istringstream, std::basic_ostringstream class templates and several typedefs
+#include <strstream>        // std::strstream, std::istrstream, std::ostrstream(deprecated)
+#include <iomanip>          // Helper functions to control the format or input and output
+#include <streambuf>        // std::basic_streambuf class template
+#include <cstdio>           // C-style input-output functions
+#include <locale>           // Localization utilities
+#include <clocale>          // C localization utilities
+#include <ciso646>          // empty header. The macros that appear in iso646.h in C are keywords in C++
+#if __cplusplus >= 201103L
+#include <typeindex>        // (since C++11) 	std::type_index
+#include <type_traits>      // (since C++11) 	Compile-time type information
+#include <chrono>           // (since C++11) 	C++ time utilites
+#include <initializer_list> // (since C++11) 	std::initializer_list class template
+#include <tuple>            // (since C++11) 	std::tuple class template
+#include <scoped_allocator> // (since C++11) 	Nested allocator class
+#include <cstdint>          // (since C++11) 	fixed-size types and limits of other types
+#include <cinttypes>        // (since C++11) 	formatting macros , intmax_t and uintmax_t math and conversions
+#include <system_error>     // (since C++11) 	defines std::error_code, a platform-dependent error code
+#include <cuchar>           // (since C++11) 	C-style Unicode character conversion functions
+#include <array>            // (since C++11) 	std::array container
+#include <forward_list>     // (since C++11) 	std::forward_list container
+#include <unordered_set>    // (since C++11) 	std::unordered_set and std::unordered_multiset unordered associative containers
+#include <unordered_map>    // (since C++11) 	std::unordered_map and std::unordered_multimap unordered associative containers
+#include <random>           // (since C++11) 	Random number generators and distributions
+#include <ratio>            // (since C++11) 	Compile-time rational arithmetic
+#include <cfenv>            // (since C++11) 	Floating-point environment access functions
+#include <codecvt>          // (since C++11) 	Unicode conversion facilities
+#include <regex>            // (since C++11) 	Classes, algorithms and iterators to support regular expression processing
+#include <atomic>           // (since C++11) 	Atomic operations library
+#include <ccomplex>         // (since C++11)(deprecated in C++17) 	simply includes the header <complex>
+#include <ctgmath>          // (since C++11)(deprecated in C++17) 	simply includes the headers <ccomplex> (until C++17)<complex> (since C++17) and <cmath>: the overloads equivalent to the contents of the C header tgmath.h are already provided by those headers
+#include <cstdalign>        // (since C++11)(deprecated in C++17) 	defines one compatibility macro constant
+#include <cstdbool>         // (since C++11)(deprecated in C++17) 	defines one compatibility macro constant
+#include <thread>           // (since C++11) 	std::thread class and supporting functions
+#include <mutex>            // (since C++11) 	mutual exclusion primitives
+#include <future>           // (since C++11) 	primitives for asynchronous computations
+#include <condition_variable> // (since C++11) 	thread waiting conditions
+#endif
+#if __cplusplus >= 201300L
+#include <shared_mutex>     // (since C++14) 	shared mutual exclusion primitives
+#endif
+#if __cplusplus >= 201500L
+#include <any>              // (since C++17) 	std::any class template
+#include <optional>         // (since C++17) 	std::optional class template
+#include <variant>          // (since C++17) 	std::variant class template
+#include <memory_resource>  // (since C++17) 	Polymorphic allocators and memory resources
+#include <string_view>      // (since C++17) 	std::basic_string_view class template
+#include <execution>        // (since C++17) 	Predefined execution policies for parallel versions of the algorithms
+#include <filesystem>       // (since C++17) 	std::path class and supporting functions
+#endif

nbproject/private/launcher.properties

+# Launchers File syntax:
+#
+# [Must-have property line] 
+# launcher1.runCommand=<Run Command>
+# [Optional extra properties] 
+# launcher1.displayName=<Display Name, runCommand by default>
+# launcher1.hide=<true if lancher is not visible in menu, false by default>
+# launcher1.buildCommand=<Build Command, Build Command specified in project properties by default>
+# launcher1.runDir=<Run Directory, ${PROJECT_DIR} by default>
+# launcher1.runInOwnTab=<false if launcher reuse common "Run" output tab, true by default>
+# launcher1.symbolFiles=<Symbol Files loaded by debugger, ${OUTPUT_PATH} by default>
+# launcher1.env.<Environment variable KEY>=<Environment variable VALUE>
+# (If this value is quoted with ` it is handled as a native command which execution result will become the value)
+# [Common launcher properties]
+# common.runDir=<Run Directory>
+# (This value is overwritten by a launcher specific runDir value if the latter exists)
+# common.env.<Environment variable KEY>=<Environment variable VALUE>
+# (Environment variables from common launcher are merged with launcher specific variables)
+# common.symbolFiles=<Symbol Files loaded by debugger>
+# (This value is overwritten by a launcher specific symbolFiles value if the latter exists)
+#
+# In runDir, symbolFiles and env fields you can use these macroses:
+# ${PROJECT_DIR}    -   project directory absolute path
+# ${OUTPUT_PATH}    -   linker output path (relative to project directory path)
+# ${OUTPUT_BASENAME}-   linker output filename
+# ${TESTDIR}        -   test files directory (relative to project directory path)
+# ${OBJECTDIR}      -   object files directory (relative to project directory path)
+# ${CND_DISTDIR}    -   distribution directory (relative to project directory path)
+# ${CND_BUILDDIR}   -   build directory (relative to project directory path)
+# ${CND_PLATFORM}   -   platform name
+# ${CND_CONF}       -   configuration name
+# ${CND_DLIB_EXT}   -   dynamic library extension
+#
+# All the project launchers must be listed in the file!
+#
+# launcher1.runCommand=...
+# launcher2.runCommand=...
+# ...
+# common.runDir=...
+# common.env.KEY=VALUE
+
+# launcher1.runCommand=<type your run command here>
\ No newline at end of file

nbproject/private/private.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<project-private xmlns="http://www.netbeans.org/ns/project-private/1">
+    <code-assistance-data xmlns="http://www.netbeans.org/ns/make-project-private/1">
+        <code-model-enabled>true</code-model-enabled>
+    </code-assistance-data>
+    <data xmlns="http://www.netbeans.org/ns/make-project-private/1">
+        <activeConfTypeElem>0</activeConfTypeElem>
+        <activeConfIndexElem>0</activeConfIndexElem>
+    </data>
+    <editor-bookmarks xmlns="http://www.netbeans.org/ns/editor-bookmarks/2" lastBookmarkId="0"/>
+    <open-files xmlns="http://www.netbeans.org/ns/projectui-open-files/2">
+        <group>
+            <file>file:/home/sparsa/Programming/mtp/src/tpdaZone.cpp</file>
+        </group>
+    </open-files>
+</project-private>

nbproject/project.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://www.netbeans.org/ns/project/1">
+    <type>org.netbeans.modules.cnd.makeproject</type>
+    <configuration>
+        <data xmlns="http://www.netbeans.org/ns/make-project/1">
+            <name>mtp</name>
+            <c-extensions/>
+            <cpp-extensions>cpp</cpp-extensions>
+            <header-extensions>h</header-extensions>
+            <sourceEncoding>UTF-8</sourceEncoding>
+            <make-dep-projects/>
+            <sourceRootList>
+                <sourceRootElem>.</sourceRootElem>
+            </sourceRootList>
+            <confList>
+                <confElem>
+                    <name>Default</name>
+                    <type>0</type>
+                </confElem>
+            </confList>
+            <formatting>
+                <project-formatting-style>false</project-formatting-style>
+            </formatting>
+        </data>
+    </configuration>
+</project>

src/continuoustpda.cpp

+#include<continuoustpda.h>
+#include"timePushDown.h"
+#include"treeBitOperations.h"
+#include<iostream>
+#include<sstream>
+
+
+using namespace std;
+
+// construction of state with given trans and tsm values
+tpdastate* atomictpda(char d1, char d2, char d3, char d4, char w1, char w2, char w3, char w4, char gc){
+	tpdastate *vs = new tpdastate();
+	
+	vs->d1 = d1;
+	vs->d2 = d2;
+	vs->d3 = d3;
+	vs->d4 = d4;
+	
+	vs->w1 = w1;
+	vs->w2 = w2;
+	vs->w3 = w3;
+	vs->w4 = w4;
+	
+	vs->gc = gc;
+	
+	return vs;
+}
+
+
+// distance between point i to point j
+short int tpdastate::dist(char i, char j)  {
+	if(i == 2 && j == 3) {
+		return ( mod(w3-w2, M) );
+	}
+	
+	if( i == 2 && j == 4 ) { 
+		if( d3 == (-1) ) {
+			return ( mod(w4-w2, M) );
+		}
+		return ( mod(w3-w2, M) + mod(w4-w3, M) );	
+	}
+	
+	if(i == 1 && j == 2) {
+		return ( mod(w2-w1, M) );
+	}
+	
+	if(i == 1 && j == 3) {
+		return ( mod(w2-w1, M) + mod(w3-w2, M) );
+	}
+	
+	if(i == 1 && j == 4) {
+		if( d3 == (-1) ) {
+			return ( mod(w2-w1, M) + mod(w4-w2, M) ); 
+		}
+		
+		return ( mod(w2-w1, M) + mod(w3-w2, M) + mod(w4-w3, M) ); 
+	}
+	
+	if(i == 3 && j == 4) {
+		return ( mod(w4-w3, M) );
+	}
+}
+
+
+// if distance between point i to point j is big, return 1, always assume that i and j exits(di != (-1) and dj != (-1))
+bool tpdastate::big(char i, char j){
+
+	// two consecutive points
+	if( (i+1) == j )  {
+		if( gc & a32[i] )
+			return false;
+		return true;
+	}
+
+	// d2->d4
+	if( i == 2 && j == 4 ) { 
+		if( d3 == (-1) ) {
+			if( gc & 4 ) // 2nd bit of gc
+				return false;
+			return true;
+		}
+		if( (gc & 4) && (gc & 8) && dist(2,4) < M ) // 2nd and 3rd bits of gc are 1 and distance d2->d4 is small
+			return false;
+		return true;	
+	}
+	
+	// d1->d3
+	if(i == 1 && j == 3) {
+		if( (gc & 2) && (gc & 4) && dist(1,3) < M )
+			return false;
+		return true;
+	}
+	
+	// d1->d4
+	if(i == 1 && j == 4) {
+		if( d3 == (-1) ) {
+			if( (gc & 2) && (gc & 4) && dist(1,4) < M )
+			return false;
+		return true;
+		}
+		
+		if( (gc & 2) && (gc & 4) && (gc & 8) && dist(1,4) < M )
+			return false;
+		return true;
+	}
+}
+
+
+// shuffle of two states
+tpdastate* tpdastate::shuffle(tpdastate *s2) {
+
+	// trans at L of s2 should be same as trans at R of this state
+	if( d4 != (s2->d2) || w4 != (s2->w2) )
+		return NULL;
+		
+	// there should be a push at L and pop at R of state s2
+	if( !isPush(s2->d2) || !isPop(s2->d4) )
+		return NULL;
+		
+	// push and pop symbol must be same
+	if( (transitions[s2->d2].as) != (transitions[s2->d4].as) )
+		return NULL;
+		
+	// push-pop edge between L and R of s2 should be added
+	if( ( (s2->gc) & 1 ) == 0 || ( (s2->gc) & 128 ) == 0 ) // push-pop edge not added yet
+		return NULL;
+		
+	char gcn; // flag for the new state
+	char d0, w0; // d1 and w1 for the new state
+		
+	gcn = (gc & 1) | ( (s2->gc) & 128); // push info of first state and pop info of 2nd state
+	
+	short int d23, d23_2, d34, dis; // dij : distance between di and dj(or distance between points i and j)
+	short int d24 = dist(2, 4); 
+	short int d24_2 = s2->dist(2, 4); 
+	
+	bool ac14, ac23, ac34, ac23_2; // acij : accuracy of distance between di and dj
+	bool ac24 = !big(2, 4);
+	bool ac24_2 = !( s2->big(2, 4) ); 
+		
+	// if there is a hanging point of state s2
+	if( (s2->d1) != (-1) ) {
+	
+		// if d3 of this state has a reset of clock x1
+		if( d3 != (-1) ) {
+		 	if( d3 != (s2->d1) || w3 != (s2->w1) ) // hanging trans and tsm should be same as d3 and w3 resp.
+				return NULL;
+				
+			// accuracy between d3->d4 and s2->d1 -> s2->d2 should be same
+			if( (gc & 8) == 0 && ( (s2->gc) & 2) != 0 ) 
+				return NULL;
+				
+			if( (gc & 8) != 0 && ( (s2->gc) & 2) == 0 )
+				return NULL;
+				
+			d0 = d1; // new hanging points comes from first state
+			w0 = w1;
+			
+			if(gc & 2) // accuracy of new hanging point comes from first state
+				gcn |= 16;
+			else
+				gcn |= 32; 
+		}
+		
+		// if d2 of this state has a reset of clock x1
+		else if(isReset(1, d2) ) {
+		
+		 	if( d2 != (s2->d1) || w2 != (s2->w1) )
+				return NULL;
+				
+			if( ac24 && ( (s2->gc) & 2) == 0 )
+				return NULL;
+				
+			if( !ac24 && ( (s2->gc) & 2) != 0 )
+				return NULL;
+				
+			d0 = d1;
+			w0 = w1;
+			
+			if(gc & 2)
+				gcn |= 16;
+			else
+				gcn |= 32;
+		}
+		
+		// if d1 of this state has a reset of clock x1
+		else if(d1 != (-1) ) {
+		
+		 	if( d1 != (s2->d1) || w1 != (s2->w1) ) 
+				return NULL;
+				
+			ac14 = !big(1, 4); // accuracy between points d1 and d4 of first state
+			
+			if( ac14 && ( (s2->gc) & 2) == 0 )
+				return NULL;
+				
+			if( !ac14 && ( (s2->gc) & 2) != 0 )
+				return NULL;
+				
+			d0 = d1;
+			w0 = w1;
+			
+			if(gc & 2)
+				gcn |= 16;
+			else
+				gcn |= 32;
+		}
+		
+		// there is no reset points in first state(inc hanging point)
+		// we don't know new hanging point accuracy, bit 16 and 32 is used for this(both are possible)
+		else{
+		
+			d0 = s2->d1; // first trans and tsm of new state comes from 2nd state
+			w0 = s2->w1;
+			
+			if( (s2->gc) & 2) { // hanging distance of 2nd state is small
+			
+				if(!ac24) // if distance between d2 and d4 is big for first state
+					return NULL;
+					
+				dis = mod(w1-w0, M) + d24;
+				if(dis >= M) // if distance between d2 and d4 is big for first state,
+					return NULL;
+					
+				gcn |= 16; // accuracy between d0 to d1 can be small
+			}
+
+			else{ // hanging distance is big
+				gcn |= 32; // we can always assume new hanging distance to to be big
+				
+				if(ac24) { // d24 is small, but new sum distance can be big
+					dis = mod(w1, w0) + d24;
+					if(dis >= M)
+						gcn |= 16;
+				}
+				else
+					gcn |= 16;
+			}
+		}
+	}
+	
+	// if there is no a hanging point of state s2
+	else {
+		d0 = d1;
+		w0 = w1;
+		if(gc & 2)
+			gcn |= 16;
+		else
+			gcn |= 32;
+	}
+		
+		
+	// now we are constructing the shuffled state
+	// till now we have computed 
+	//	(i) hanging clock accuracy
+	//	(ii) d1, d2 and d4 of the new state
+	// now we compute d3 and 2nd and 3rd bit of accuracy
+	
+	if( isReset(1, s2->d4) ) { // if d4 of s2 has a reset
+	
+		if(ac24 && ac24_2) { // if accuracy d2->d4 and (s2->d2)->(s2->d4) are true
+			dis = d24 + d24_2;
+			if(dis < M)
+				gcn = gcn | 4;
+		}
+		return atomictpda(d0, d2, -1, s2->d4, w0, w2, -1, s2->w4, gcn);
+	}
+	
+	else if( (s2->d3) != (-1) ) { // if d3 of s2 has a reset
+		d23_2 = s2->dist(2, 3);
+		ac23_2 = !( s2->big(2, 3) );
+		
+		if(ac24 && ac23_2) {
+			dis = d24 + d23_2;
+			if(dis < M)
+				gcn = gcn | 4;
+		}
+		gcn |= ( (s2->gc) & 8);
+		return atomictpda(d0, d2, s2->d3, s2->d4, w0, w2, s2->w3, s2->w4, gcn);
+	}
+	
+	else if(isReset(1, d4) ) { // reset at d2 of state 2(d4 of state 1)
+		if(ac24)
+			gcn = gcn | 4;
+		if( (s2->gc) & 4) // note that there was no d3 of state 2
+			gcn |= 8;
+		return atomictpda(d0, d2, d4, s2->d4, w0, w2, w4, s2->w4, gcn);
+	}
+	
+	else if(d3 != (-1) ) { // reset at d3 of state 1
+		gcn = gcn | (gc & 4); // 2nd bit comes from first state 2nd bit
+		
+		d34 = dist(3, 4);
+		ac34 = !big(3, 4);
+		
+		if(ac34 && ac24_2) {
+			dis = d34 + d24_2;
+			if(dis < M)
+				gcn |= 8;
+		}
+		return atomictpda(d0, d2, d3, s2->d4, w0, w2, w3, s2->w4, gcn);
+	}
+	
+	else{
+		if(ac24 && ac24_2) { // if accuracy d2->d4 and (s2->d2)->(s2->d4) are true
+			dis = d24 + d24_2;
+			if(dis < M)
+				gcn = gcn | 4;
+		}
+		return atomictpda(d0, d2, -1, s2->d4, w0, w2, -1, s2->w4, gcn);
+	}
+}
+
+
+// check if pop condition satisfied by the new transitions
+bool tpdastate::popTest(char d5, char w5, int lb, int ub) {
+	if( !isPop(d5) ) // no pop => condition already satisfied
+		return true;
+		
+	if( !big(2, 4) ) { // distance between 2 and 4 is accurate
+		short int d25 = dist(2, 4) + mod(w5-w4, M);
+		if(d25 >= lb && d25 <= ub)
+			return true;
+		else
+			return false;
+	}
+	else if(ub == INF)
+		return true;
+		
+	return false;
+}
+
+
+// calculate new gc flag after adding trans d5 of tsm w5
+char tpdastate::getGc(char d5, char w5) {
+	char gcn = (gc & 2); // hanging clock accuracy
+	
+	if( isReset(1, d5) ) {
+		if( !big(2, 4) ) {
+			short int d25 = dist(2, 4) + mod(w5-w4, M);
+			if(d25 < M)
+				gcn |= 4;
+			return gcn;
+		}
+		return gcn;
+	}
+	
+	else if( isReset(1, d4) ) { // note : d3 == -1 in this case
+		gcn |= (gc & 4) | 8;
+		return gcn;
+	}
+	
+	else if( d3 != (-1) ) {
+		gcn |= (gc & 4);
+		
+		if(gc & 8) {
+			short int d35 = mod(w4-w3, M) + mod(w5-w4, M);
+			if(d35 < M)
+				gcn |= 8;
+			return gcn;
+		}
+		return gcn;
+	}
+	
+	else{
+		if(gc & 4) {
+			short int d25 = dist(2, 4) + mod(w5-w4, M);
+			if(d25 < M)
+				gcn |= 4;
+			return gcn;
+		}
+		return gcn;
+	}
+}
+
+// if We add new trans d5, if clock constraints are satisfied
+bool tpdastate::clockTest(char d5, char w5, int lbc, int ubc) {
+
+	if( isReset(1, d4) ) {
+		char d45 = mod(w5-w4, M);
+		if(d45 >= lbc && d45 <= ubc)
+			return true;
+		return false;
+	}
+	
+	else if( d3 != (-1) ) {
+		if(gc & 8) {
+			short int d35 = mod(w4-w3, M) + mod(w5-w4, M);
+			if(d35 >= lbc && d35 <= ubc)
+				return true;
+			return false;
+		}
+		else if(ubc == INF)
+			return true;
+			
+		return false;
+	}
+	
+	else if( isReset(1, d2) ){
+		if( !big(2, 4) ) {
+			short int d25 = dist(2, 4) + mod(w5-w4, M);
+			if(d25 >= lbc && d25 <= ubc)
+				return true;
+			return false;
+		}
+		
+		else if(ubc == INF)
+			return true;
+		return false;
+	}
+	
+	else{ // d1 has a reset point, ignore the case when d1 also not a reset point
+		if( !big(1, 4) ) {
+			short int d15 = dist(1, 4) + mod(w5-w4, M);
+			if(d15 >= lbc && d15 <= ubc)
+				return true;
+			return false;
+		}
+		
+		else if(ubc == INF)
+			return true;
+		return false;
+	}
+}
+
+
+// given trans 0 or a push trans d1(with tsm w1), find the next possible trans d2(with tsm w2)
+vector<tpdastate*> getAtomics(char d1, char w1) {
+	vector<tpdastate*> v; // vector contains all the generated states
+	
+	char q = transitions[d1].target; // target state of trans d4
+	
+	char d2, w2; // next trans and tsm value
+	char d0, w0; // previous reset trans and tsm value(if d2 has a check, but d1 has no reset);
+	char gcn; // new flag variable for state
+	
+	int lb, ub; // pop bounds
+	int lbc, ubc; // clock bounds
+	
+	bool checkflag; // true : there is a check at d2
+	bool popflag; // true : there is a pop at d2
+	short int d12, d02; // distance d1 to d2 and distance d0 to d2
+	
+	// iterate through all the upcoming transitions
+	for(char i=0; i < nexttrans[q].size(); i++) {
+		d2 = nexttrans[q][i]; // i-th upcoming transition
+		
+		lb = transitions[d2].lbs[0]; // lower bound for stack
+		ub = transitions[d2].ubs[0]; // upper bound for stack 
+		
+		lbc = transitions[d2].lbs[1]; // lower bound for clock
+		ubc = transitions[d2].ubs[1]; // upper bound for clock
+		
+		checkflag = isChecked(1, d2); // true : there is a check at d2
+		popflag = isPop(d2); // true : there is a pop at d2
+		
+		// note  : distance between d1 and d2 is always accurate
+		if(popflag)
+			gcn = 1 | 128 | 4;
+		else
+			gcn = 4;
+		
+		// if there is a pop at d2, there must a push at d1
+		if( popflag && !isPush(d1) ) { }
+		
+		// push-pop symbol must be same
+		else if( popflag && ( transitions[d1].as != transitions[d2].as) ) { }
+		
+		// there is a check at d2, but no reset at d1
+		else if( checkflag && !isReset(1, d1) ) {
+		
+			// consider d0 to d1 distance to be big
+			if(ubc == INF) {
+				for(w2 = 0; w2 < M; w2++) {
+					d12 = mod(w2-w1, M);
+					if( !popflag || (d12 >= lb && d12 <= ub) ) { // pop test
+						for(w0 = 0; w0 < M; w0++) { // all possible w0 can happen
+							for(i = 0; i < possibleresets[d2].size(); i++) {
+								d0 = possibleresets[d2][i];
+								v.push_back( atomictpda(d0, d1, -1, d2, w0, w1, -1, w2, gcn) );
+							}
+						}
+					}
+				}
+			}
+			
+			// consider d0 to d1 distance to be accurate
+			for(w2 = 0; w2 < M; w2++) {
+				d12 = mod(w2-w1, M);
+				gcn |= 2; // d0 to d1 is accurate
+				if( !popflag || (d12 >= lb && d12 <= ub) ) {
+					for(w0 = 0; w0 < M; w0++) {
+						d02 = mod(w1-w0, M) + d12;
+						if( !checkflag || (d02 >= lbc && d02 <= ubc) ) {
+							for(i = 0; i < possibleresets[d2].size(); i++) {
+								d0 = possibleresets[d2][i];
+								v.push_back(atomictpda(d0, d1, -1, d2, w0, w1, -1, w2, gcn));
+							}
+						}
+					}
+				}
+			}
+			
+		}
+		
+		else{
+			for(w2 = 0; w2 < M; w2++) {
+				d12 = mod(w2-w1, M);
+				if( ( !checkflag || (d12 >= lbc && d12 <= ubc) ) && ( !popflag || (d12 >= lb && d12 <= ub) ) ){
+					v.push_back( atomictpda(-1, d1, -1, d2, -1, w1, -1, w2, gcn) );
+				}
+			}
+		}
+	}
+	return v;
+}
+
+
+/*Add the next transition to the current state*/
+/*if there is a push at R, then don't call here*******/
+vector<tpdastate*> tpdastate::addNextTPDA() {
+	vector<tpdastate*> v; // set of states generated by adding a new transition
+	
+	if( isPush(d4) ) // there should not be any push at R
+		return v; // return empty vector
+		
+	if( isPop(d4) && ( gc & 128 ) == 0 ) // there is a pop at d4, but pop edge not added yet
+		return v;
+		
+	// if there is a push at L and there is a pop at R, then first shuffle, then add new transitions
+	if( isPush(d2) && isPop(d4) && (gc & 128) &&  (gc & 1) )
+		return v;
+	
+	char d0, w0; // trans and tsm at hanging point
+	char d5, w5; // trans and tsm at newly added rightmost point
+	char dn3, wn3; // newly created trans and tsm for reset point
+	char gc2, gcn; // gc2 : temp flag, gcn : new state flag
+
+	short int d05, d12, d25;
+	short int d24 = dist(2,4);
+	
+	bool ac24 = !big(2,4);
+	
+	char cnd; // case variable
+
+	bool checkflag = false;
+	bool popflag = false;
+	
+	int lbc, ubc; // clock constraint's bound
+	int lb, ub; // lower and upper bound for stack
+	
+
+	char q = transitions[d4].target; // target state of trans d4
+	
+	// iterate through all the upcoming transitions
+	for(char i=0; i < nexttrans[q].size(); i++) {
+	
+		d5 = nexttrans[q][i]; // i-th upcoming transition
+		
+		lb = transitions[d5].lbs[0]; // lower bound for stack
+		ub = transitions[d5].ubs[0]; // upper bound for stack 
+		
+		lbc = transitions[d5].lbs[1]; // lower bound for clock
+		ubc = transitions[d5].ubs[1]; // upper bound for clock
+		
+		checkflag = isChecked(1, d5);
+		popflag = isPop(d5);
+		
+		gc2 = 0; // temp flag variable for a FTA state
+		
+		if( isReset(1, d5) ) { // if there is a reset at transition d5
+			cnd = 5;
+			d0 = d1;
+			w0 = w1;
+			dn3 = -1;
+		}
+		else if( isReset(1, d4) ) { // if there is a reset at transition d4
+			cnd = 4;
+			d0 = d1;
+			w0 = w1;
+			dn3 = d4;
+			wn3 = w4;
+		}
+		else if( d3 != (-1) ) { // if there is a reset at transition d3
+			cnd = 3;
+			d0 = d1;
+			w0 = w1;
+			dn3 = d3;
+			wn3 = w3;
+		}
+		else if( isReset(1, d2) ) { // if there is a reset at transition d2
+			cnd = 2;
+			d0 = d1;
+			w0 = w1;
+			dn3 = -1;
+			wn3 = -1;
+		}
+		else if( isReset(1, d1) ) { // if there is a reset at transition d2
+			cnd = 1;
+			d0 = d1;
+			w0 = w1;
+			dn3 = -1;
+		}
+		else {
+			cnd = 0;
+			dn3 = -1;
+		}
+		
+		
+		if( d1 != (-1) ) {
+			d12 = dist(1, 2);
+		}
+		
+		// if there is a pop at d5, but no push at d2
+		if( popflag && !isPush(d2) ) { }
+		
+		// if there is a pop at d5, but  push is already done at d2
+		else if( popflag && (gc & 1) ) { }
+		
+		// push-pop symbol is not same
+		else if( popflag && ( transitions[d2].as != transitions[d5].as) ) { }
+		
+		// o.w add new transtitions to the right
+		else{
+			// if there is a reset at transition d5
+			if( popflag ) { // push pop both are being done
+				gc2 = 1 | 128;
+			}
+			else // push info of previous state
+				gc2 = (gc & 1);
+				
+			// if there is a check at 
+			if( checkflag && cnd == 0) {
+			
+				// consider new hanging distance to be big, we can do this only if upper bound is inf
+				if(ubc == INF) { 
+					if(ac24) { // if distance between d2 and d4 is accurate
+						for(w5=0; w5 < M; w5++) {
+							d25 = d24 + mod(w5-w4, M);
+							if(d25 < M) // d0->d2 distance is big and d2->d5 distance is small
+								gcn = gc2 | 4;
+							else // d0->d2 distance is big and d2->d5 distance is also big
+								gcn = gc2;
+								
+							if( !popflag || d25 >= lb && d25 <= ub) {
+								for(w0 = 0; w0 < M; w0++) {
+									for(i = 0; i < possibleresets[d5].size(); i++) {
+										d0 = possibleresets[d5][i];
+										v.push_back(atomictpda(d0, d2, -1, d5, w0, w2, -1, w5, gcn));
+									}
+								}
+							} 
+						}
+					}
+				
+					else if(!popflag || ub == INF){ // if distance between d2 and d4 is big
+						gcn = gc2; // all distance are big, only push info is there
+						for(w0 = 0; w0 < M; w0++) {
+							for(w5=0; w5 < M; w5++) {
+								for(i = 0; i < possibleresets[d5].size(); i++) {
+									d0 = possibleresets[d5][i];
+									v.push_back(atomictpda(d0, d2, -1, d5, w0, w2, -1, w5, gcn));
+								}
+							}
+						}
+					}
+				}
+			
+				// consider new hanging distance to be small
+				gc2 = gc2 | 2;	 // // consider new hanging distance to be small, now d0->d2 distance is small
+				if(ac24) {
+					for(w5=0; w5 < M; w5++) {
+						d25 = d24 + mod(w5-w4, M);
+						if(d25 < M) // d0->d2 distance is small and d2->d5 distance is also small
+							gcn = gc2 | 4;
+						else	// d0->d2 distance is small and d2->d5 distance is big
+							gcn = gc2;
+						if( !popflag || ( d25 >= lb && d25 <= ub ) ) {
+							for(w0 = 0; w0 < M; w0++) {
+								d05 = mod(w2-w0, M) + d25;
+								if( d05 >= lbc && d05 <= ubc ) {
+									for(i = 0; i < possibleresets[d5].size(); i++) {
+										d0 = possibleresets[d5][i];
+										v.push_back(atomictpda(d0, d2, -1, d5, w0, w2, -1, w5, gcn));
+									}
+								}
+							}
+						}
+					}
+				}
+		
+				else if(ubc == INF && ( !popflag || ub == INF ) ) {
+					gcn = gc2; // // d0->d2 distance is small and d2->d5 distance is big
+					for(w0 = 0; w0 < M; w0++) {
+						for(w5=0; w5 < M; w5++) {
+							for(i = 0; i < possibleresets[d5].size(); i++) {
+								d0 = possibleresets[d5][i];
+								v.push_back(atomictpda(d0, d2, -1, d5, w0, w2, -1, w5, gcn));
+							}
+					
+						}
+					}
+				}
+			}
+				
+			else { 
+				for(w5 = 0; w5 < M; w5++) {
+					if( ( !checkflag || clockTest(d5, w5, lbc, ubc) ) && (!popflag || popTest(d5, w5, lb, ub))){
+						gcn = gc2 | getGc(d5, w5);
+						v.push_back( atomictpda(d0, d2, dn3, d5, w0, w2, wn3, w5, gcn) );
+					}
+				}
+			}
+		}
+	}
+	return v;
+}
+
+
+set<string> gtpdatrie;
+
+bool identity(tpdastate *vs) {
+	ostringstream os; // output stream
+	
+	os << (vs->d1) << (vs->d2) << (vs->d3) << (vs->d4);
+	os << (vs->w1) << (vs->w2) << (vs->w3) << (vs->w4);
+	os << (vs->gc);
+
+	// return true if os.str() inserted in the set 'strie' successfully 
+	return (gtpdatrie.insert(os.str())).second; 
+}
+
+// print a state of tree automation
+void tpdastate::print() {
+	cout << "\nAbstarct tree automation state:\n";
+	
+	cout << "\tTransitions : " << int(d1) << ",  " << int(d2) << ",  " << int(d3) << ",  " << int(d4) << endl;
+	
+	cout << "\tTSM : " << int(w1) << ",  " << int(w2) << ",  " << int(w3) << ",  " << int(w4) << endl;
+	
+	cout << "\tPush edge added to L : ";
+	if(gc & 1)
+		cout << 1 << endl;
+	else
+		cout << 0 << endl;
+		
+	cout << "\tPop edge added to R : ";
+	if(gc & 128)
+		cout << 1 << endl;
+	else
+		cout << 0 << endl;
+	
+	cout << "\tAccuracy : " << bool(gc & 2) << ",  " << bool(gc & 4) << ",  " << bool(gc & 8) << endl;
+	
+	cout << "\tFlag : " << bool(gc & 128) <<bool(gc & 64) <<bool(gc & 32) <<bool(gc & 16) <<bool(gc & 8) <<bool(gc & 4) <<bool(gc & 2) <<bool(gc & 1) <<endl; 
+	cout << endl;
+}
+
+
+// return true : if current state is final
+bool tpdastate::isFinal() {
+	//if( d2 != 0 || d4 != SF ) // d2 : initial trans, d4 : final trans
+		//return false;
+		
+	if( d1 != (-1) ) // no hanging clock
+		return false;
+		
+	if(isPush(d4))
+		return false;
+		
+	if( isPop(d4) &&  (gc & 128) == 0) // there is a pop at d4, but not added yet
+		return false;
+		
+	// 0 is initial state for a tpda
+	if( transitions[d2].source != 0) // remember 0  is the new initial state
+		return false;
+		
+	if(w2 != 0) // first time stamp must be 0
+		return false;
+	
+	//if( transitions[del1].source != SI) // remember 0  is the new initial state
+		//return false;
+		
+	// target state of the transiton at point R should be a final state
+	if( transitions[d4].target != SF) 
+		return false;
+		
+	return true;
+}
+
+
+// return xerox copy of this state
+tpdastate* tpdastate::copyState() {
+	tpdastate *vs = new tpdastate();
+	
+	vs->d1 = d1;
+	vs->d2 = d2;
+	vs->d3 = d3;
+	vs->d4 = d4;
+	vs->w1 = w1;
+	vs->w2 = w2;
+	vs->w3 = w3;
+	vs->w4 = w4;
+	vs->gc = gc;
+	
+	return vs;
+}
+
+
+// given a atomic tree automation state give a run of the TPDA
+gtpda_run* getatomicrunpds(tpdastate* vs) {
+	gtpda_run *rs = new gtpda_run();
+	
+	if( (vs->d3) == (-1) ) {
+		rs->P = 2;
+		rs->del = new char[2];
+		rs->w = new char[2];
+		
+		rs->del[0] = vs->d2;
+		rs->del[1] = vs->d4;
+		
+		rs->w[0] = vs->w2;
+		rs->w[1] = vs->w4;
+	}
+	
+	else {
+		rs->P = 3;
+		rs->del = new char[3];
+		rs->w = new char[3];
+		
+		rs->del[0] = vs->d2;
+		rs->del[1] = vs->d3;
+		rs->del[2] = vs->d4;
+		
+		rs->w[0] = vs->w2;
+		rs->w[1] = vs->w3;
+		rs->w[2] = vs->w4;
+	}
+	
+	return rs;
+}
+
+
+// GIVEN the current run, append the trans d5 with tsm w5
+gtpda_run* gtpda_run::add_next(char d5, char w5) {
+	gtpda_run *pr = new gtpda_run();
+	
+	pr->P =  P + 1;
+	pr->del = new char[pr->P];
+	pr->w = new char[pr->P];
+	
+	for(char i=0; i < P; i++) {
+		pr->del[i] = del[i];
+		pr->w[i] = w[i];
+		//pr->ac[j] = ac[i];
+	}
+	
+	pr->del[P] = d5;
+	pr->w[P] = w5;
+	
+	return pr;
+}
+
+
+// shuffle two runs
+gtpda_run* gtpda_run::shuffle(gtpda_run *s2) {
+	gtpda_run *pr = new gtpda_run();
+	
+	pr->P =  P + (s2->P) - 1;
+	
+	pr->del = new char[pr->P];
+	pr->w = new char[pr->P];
+	//pr->ac = new char[pr->P];
+	
+	char i, j;
+	
+	for(i=0, j=0; i < (P-1); i++, j++) {
+		pr->w[j] = w[i];
+		pr->del[j] = del[i];
+		//pr->ac[j] = ac[i];
+	}
+	
+	for(i=0; i < (s2->P); i++, j++) {
+		pr->w[j] = s2->w[i];
+		pr->del[j] = s2->del[i];
+		//pr->ac[j] = s2->ac[i];
+	}
+	
+	return pr;
+}
+
+
+// print a run of the given TPDA
+void gtpda_run::print() {
+	short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps
+	//bool lac = true; // last accuracy
+	cout << endl << "A run of the automation as a proof that the language is non-empty, the run given as a sequence of pairs (transition, time stamp) : " << endl;
+	//cout << "Left:" << int(L) << ",#points : " << int(P) << endl;
+	//cout << "L:" << int(act[L-1]) << ",R:" << int(act[P-1]) << endl;
+	
+	for(char i=0; i < P; i++) {
+	
+		// this two line changes for accuracy
+		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);
+			
+		//if(!lac)
+			//ct += M;
+		//lac = ac[i];
+			
+		lt = w[i];
+			
+		cout << "(" << int(del[i]) << ", " << int(ct)  << ".0" << "), ";
+	}
+	
+	cout << endl << endl;
+}
+
+
+
+// get the run of the timed system starting from i-th index state of all states 'states'
+gtpda_run* printRun(vector<tpdastate*> &states, vector<bp_gtpda> &v, int i) {
+	bp_gtpda bp = v[i]; // backpropagation information for i-th index state
+	
+	gtpda_run *rs, *rs1, *rs2;
+		
+	if( (bp.type) == 0) { // if the i-th state is an atomic state
+		cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << endl;
+		states[i]->print();
+
+		return getatomicrunpds(states[i]);
+	}
+	
+	if( (bp.type) == 1) { // if state states[i] is obtained by forgetting color 'bp.f' from state states[bp.left]
+		rs = printRun(states, v, bp.left);
+		rs = rs->add_next(char(bp.right), char( (bp.right) >> 8) );
+		cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << ", " << ( (bp.right) >> 8) << endl;
+		states[i]->print();
+
+		return rs;
+	}
+	
+	
+	
+	rs1 = printRun(states, v, bp.left); // get run for the state states[bp.left]
+	rs2 = printRun(states, v, bp.right);// get run for the state states[bp.right]
+	rs = rs1->shuffle(rs2); // shuffle two runs rs1 and rs2 with accuracy given by bp.ac
+	
+	cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << endl;
+	states[i]->print();
+
+	return rs;
+}
+
+// check if a tpda of one clock is empty or not
+bool isEmptyTPDA() {
+	
+	int N=0,count=0;
+	vector<tpdastate*> states;
+	vector<tpdastate*> v;
+	
+	tpdastate *rs, *vs, *rs1, *rs2;
+	
+	vector<bp_gtpda> vrs; // vector for keeping track of connection between current states with previous states
+	bp_gtpda xrs; // bac
+	
+	gtpda_run *prs, *prs1, *prs2;
+	
+	
+	int i, m, t, d5, w5;
+	char w;
+	
+	xrs.type = 0; // atomic state type
+	
+	
+	v = getAtomics(0, 0);
+	for(i=0; i < v.size(); i++) {
+		if( identity(v[i]) ) {
+			states.push_back(v[i]);
+			vrs.push_back(xrs);
+			N++;
+			if( v[i]->isFinal() ) {
+				v[i]->print();
+				prs = printRun(states, vrs, N-1);
+				prs->print();
+				return false;
+			}
+		}
+	}
+	
+	/*
+	for(t=1; t <= T; t++) {
+		if(isPush(t) ) {
+			for(w=0; w < M; w++) {
+				v = getAtomics(t, w);
+				for(i=0; i < v.size(); i++) {
+					if( identity(v[i]) ) {
+						states.push_back(v[i]);
+						vrs.push_back(xrs);
+						N++;
+						if( v[i]->isFinal() ) {
+							v[i]->print();
+							prs = printRun(states, vrs, N-1);
+							prs->print();
+							return false;
+						}
+					}
+				}
+			}	
+		}
+	}
+	*/
+	
+	/*
+	for(i=0; i < N; i++) {
+		cout << "state " << i << ":" << endl;
+		states[i]->print();
+	}
+	*/
+	
+	
+	// iterate through all the states
+	for(count=0; count < N; count++) {
+	
+		if(count %5000 == 0)
+			cout << "#states" << endl;
+	
+		if( (count % 100) == 0 || count <= 100) // print #iterations
+			cout << count << endl;
+			
+		rs = states[count]; // get the state at index count
+		//rs->print();
+		
+		// *****
+		xrs.type = 0;
+		if( isPush(rs->d4) && !pushDone[rs->d4][rs->w4] ) {
+			v = getAtomics(rs->d4, rs->w4);
+			for(i=0; i < v.size(); i++) {
+				if( identity(v[i]) ) {
+					states.push_back(v[i]);
+					vrs.push_back(xrs);
+					N++;
+					if( v[i]->isFinal() ) {
+						v[i]->print();
+						prs = printRun(states, vrs, N-1);
+						prs->print();
+						return false;
+					}
+				}
+			}
+			pushDone[rs->d4][rs->w4] = true;	
+		}
+		//****
+		
+		xrs.type = 1; // add_stack type
+		xrs.left = count;
+		// try to add new trans to the state rs
+		v = rs->addNextTPDA();
+		for(i=0; i < v.size(); i++) {
+			if( identity(v[i]) ) { // if the i-th state is new
+				d5 = (v[i]->d4); w5 = (v[i]->w4);
+				xrs.right = d5 + (w5 << 8);
+				
+				states.push_back(v[i]);
+				vrs.push_back(xrs);
+				N++;
+				if( v[i]->isFinal() ) { // if this state is final
+					v[i]->print();
+					prs = printRun(states, vrs, N-1);
+					prs->print();
+					return false;
+				}
+				
+			}
+		}
+		
+		
+		xrs.type = 2; // add_stack type
+		
+		// try to do shuffle with all the previous(as left as well as right state)
+		if( isPush(rs->d4) || ( isPush(rs->d2) && isPop(rs->d4) ) ) {
+			for(i=0; i <= count; i++) {
+				xrs.left = count;
+				xrs.right = i;
+				// shuffle, considering rs as left state
+				vs = rs->shuffle( states[i] );
+				if(vs != NULL) { // if new state is valid
+				
+					if( (vs->gc) & 16) { // if hanging distance is accurate
+						rs1 = vs->copyState();
+						rs1->gc = ( (rs1->gc) & (~16) & (~32) ) | 2;
+						if( identity(rs1) ) {
+							states.push_back(rs1);
+							vrs.push_back(xrs);
+							N++;
+							if( rs1->isFinal() ) {
+								rs1->print();
+								prs = printRun(states, vrs, N-1);
+								prs->print();
+								return false;
+							}
+							
+						}
+					}
+					
+					else if((vs->gc) & 32) { // if hanging distance is big(big and small both can happen)
+						vs->gc = (vs->gc) & (~16) & (~32) & (~2);
+						if(identity(vs)) {
+							states.push_back(vs);
+							vrs.push_back(xrs);
+							N++;
+							if( vs->isFinal() ) {
+								vs->print();
+								prs = printRun(states, vrs, N-1);
+								prs->print();
+								return false;
+							}
+							
+						}
+					}
+				}
+				
+				
+				xrs.left = i;
+				xrs.right = count;
+				
+				// shuffle, considering rs as right state
+				vs = states[i]->shuffle(rs);
+				
+				if(vs != NULL) { // if new state is valid
+					
+					if( (vs->gc) & 16) { // if hanging distance is accurate
+						rs1 = vs->copyState();
+						rs1->gc = ( (rs1->gc) & (~16) & (~32) ) | 2;
+						if( identity(rs1) ) {
+							states.push_back(rs1);
+							vrs.push_back(xrs);
+							N++;
+							if( rs1->isFinal() ) {
+								rs1->print();
+								prs = printRun(states, vrs, N-1);
+								prs->print();
+								return false;
+							}
+							
+						}
+					}
+					
+					else if((vs->gc) & 32) { // if hanging distance is big(big and small both can happen)
+						vs->gc = (vs->gc) & (~16) & (~32) & (~2);
+						if(identity(vs)) {
+							states.push_back(vs);
+							vrs.push_back(xrs);
+							N++;
+							if( vs->isFinal() ) {
+								vs->print();
+								prs = printRun(states, vrs, N-1);
+								prs->print();
+								return false;
+							}
+						}
+					}
+				}
+			}
+		}
+		
+	}
+	/*
+	*/
+	
+	return true;
+	
+}

src/drawsystem.cpp

+#include<fstream>
+#include<iostream>
+#include<stdlib.h>
+
+#include"drawsystem.h"
+#include"treeBitOperations.h"
+
+
+
+
+//using namespace std;
+
+
+//char inputfilename[100]; // input file name for timed push-down system
+
+weighttype B;
+int M; // maximum constant+1 in the timed system
+
+unsigned short int S; // number of states in the timed system
+unsigned short int SI; // initial state
+unsigned short int SF; // final state
+
+unsigned short int T; // number of transitions in the timed system
+char X; // number of clocks in the timed system
+char A; // number of events or actions in the timed system
+char AS; // number of stack symbols in the timed system
+
+transition *transitions; // transitions of the timed system
+
+inline bool transition::isReset(char i) {
+	return (a32[i] & reset);
+}
+
+
+void showsystem(char *outfile) {
+	int source,ns;
+	int i,j,k;
+	int guard,reset;
+	int action, ub, lb, ps, pp;
+	
+	ofstream tiimeoutfile(outfile); // timed automata output file for showing the automata 		
+	tiimeoutfile << "digraph finite_state_machine {\n";
+ 	//tiimeoutfile << "ratio=\"fill\";\nsize=\"10,10!\";\n";
+ 	
+ 	for(i=0; i <= S; i++) {
+ 		//tiimeoutfile << i << " [label=\""<<i<<"\"];\n";
+ 	}
+
+	tiimeoutfile << "\tnode [shape = point ]; qi" << 0 << ";\n";
+	tiimeoutfile << "\tnode [shape = doublecircle];" << SF << ";\n";
+	tiimeoutfile << "\tnode [shape=circle];\n"; // all the states other than final states are labelled in a circle
+	tiimeoutfile << "\tqi" << "0" << " -> " << SI << ";\n";
+	
+	for(i=0; i <= T; i++) { // take input for all the transitions 		
+		source = transitions[i].source; // previous and next state of the i-th transition 		
+		ns = transitions[i].target; 		
+		tiimeoutfile << "\t" << source << " -> " << ns << " [ label = \"{tn:" << (i); // output transition between two states 
+			
+		guard = transitions[i].guard; 		
+		reset = transitions[i].reset; 	
+		
+		action = transitions[i].a; 
+				
+		for(j=1; j <= X; j++) { // save all the conjunction of a constraint 			
+			
+			if(guard & a32[j]) {
+				lb = transitions[i].lbs[j];
+				ub = transitions[i].ubs[j];
+				//if (ub == 0 && lb == 0) {} //***this line will not be active other than maze, only else part will remain****
+				//else{
+				if(ub == INF) 				
+					tiimeoutfile << "," <<  lb << "<=" << "x" << j << "<=" << "inf"; 			
+				else 				
+					tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub; 
+				//}		
+			}
+		} 		
+			
+		//tiimeoutfile << ",a" << action; // output action number
+			 		
+		for(j=1;j <= X; j++) { // reset clocks for i-th transition 'transitions[i]' 
+			if(reset & a32[j]) {
+				tiimeoutfile << ",x" << j << ":=0"; 	//***this line will be active other than maze****
+			}				
+			
+		}
+		
+		//stack_symbol = transitions[i].as ;
+		ps = transitions[i].ps ;
+		pp = transitions[i].pp ;
+			 
+		if( (reset & 1) == 0 && (guard & 1) == 0 ) { // nop stack operation
+			//tiimeoutfile << ",np"; //***this line will be active other than maze****
+		}
+		
+		else if( (reset & 1) == 0 && (guard & 1) == 1 ) { // push operation
+			tiimeoutfile << ",ps_" << ps;
+		}
+		
+		else if( (reset & 1) == 1 && (guard & 1) == 0 ) { // pop operation
+			tiimeoutfile << ",pp_" << pp;
+			lb = transitions[i].lbs[0];
+			ub = transitions[i].ubs[0];
+			if(ub == INF) 					
+				tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << "inf"; 									
+			else 					
+				tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << ub;
+		}
+		
+		else if( (reset & 1) && (guard & 1) ) { // pop operation
+			tiimeoutfile << ",pp_" << pp;
+			lb = transitions[i].lbs[0];
+			ub = transitions[i].ubs[0];
+			if(ub == INF) 					
+				tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << "inf"; 									
+			else 					
+				tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << ub;
+			tiimeoutfile << ",ps_" << ps;
+		}
+		tiimeoutfile << "}\" ];\n"; 
+		
+	}
+		
+		
+	tiimeoutfile << "}"; // output the last closing brace 	// graph complete for the automata 	tiimeoutfile.close();
+}
+
+
+
+// get the input timed system given as a file(file name stored in the global variable 'inputfilename')
+int main(int argc, char *argv[]) {
+
+	setBits();
+
+	int x; // temporary variable
+	short int i, j; // loopers
+	int lb, ub; // used as lower and upper bound
+	short int noofguards, noofresets; // #gurads and #reset clocks in a transition
+	int guard, reset;
+	
+	if(argc < 2) {
+		cout << "You must give the timed system input file!" << endl;
+		return 0;
+	}
+	
+	//ifstream tiimeinfile (argv[1]); // timed system input file stream
+	
+	ifstream tiimeinfile (argv[1]); // timed system input file stream
+	
+	//cout << "ilias" << endl;
+	
+	// if there is any error opening the file 		
+	if( !(tiimeinfile.is_open()) )  { 
+		cout << "\n****INPUT TIMED PUSH-DOWN FILE NOT FOUND ! ****\n"; 		
+		exit(1);
+	}
+	
+	tiimeinfile >> S; // #states in origianl automata
+	
+	tiimeinfile >> T; // #transitions
+	transitions = new transition[T+1]; // allocate memory for transitions
+	
+	tiimeinfile >> x; // #clocks 
+	X = x;	
+	
+	tiimeinfile >> x; // #actions
+	A = x;	
+	 	
+	tiimeinfile >> x; // #stack_symbols
+	AS = x;	
+	
+	tiimeinfile >> SI;  // input initial state
+	tiimeinfile >> SF;  // input final state
+	
+	transitions[0].source = 0;
+	transitions[0].target = SI;
+	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].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].reset = (~0) ^ 1;	
+	
+	SI = 0;
+	
+		
+	
+	// get all the transitions
+	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);
+			}
+			
+			transitions[i].lbs[x] = lb; // lower bound for clock x
+			
+			if(ub == (-1)) { // upper bound -1 means infinity 				
+				transitions[i].ubs[x] = INF;
+			}	
+			
+			else {
+				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
+		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].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].pp = x;
+			
+			tiimeinfile >> lb >> ub; // read stack pop bounds
+			
+			
+			transitions[i].lbs[0] = lb; // lower bound for clock x
+			
+			if(ub == (-1)) // upper bound -1 means infinity 				
+				transitions[i].ubs[0] = INF;
+			
+			else
+				transitions[i].ubs[0] = ub; 
+		}
+		
+		else if(x == 3) { // pop operation
+			reset |= 1; // set 0-th bit of reset to '1'
+			guard |= 1; // set 0-th bit of reset to '1'
+			
+			tiimeinfile >> x; // stack pop symbol
+			transitions[i].pp = x;
+			
+			tiimeinfile >> lb >> ub; // read stack pop bounds
+			
+			
+			transitions[i].lbs[0] = lb; // lower bound for clock x
+			
+			if(ub == (-1)) // upper bound -1 means infinity 				
+				transitions[i].ubs[0] = INF;
+			
+			else
+				transitions[i].ubs[0] = ub; 
+				
+			tiimeinfile >> x; // stack pop symbol
+			transitions[i].ps = x;
+		}
+		
+		else {
+			cout << "Invalid stack operation!" << endl;
+			exit(1);
+		}
+		
+		transitions[i].guard = guard;
+		transitions[i].reset = reset;
+	}
+	tiimeinfile.close();
+	showsystem(argv[2]);
+	return 0;
+}
+

src/pds.cpp

+#include<pds.h>
+#include"timePushDown.h"
+#include"treeBitOperations.h"
+#include<sstream>
+
+set<string> pstrie;
+
+bool identity(pds_state *vs) {
+	ostringstream os; // output stream
+	
+	os << (vs->del1) << (vs->del2);
+	os << (vs->w1) << (vs->w2);
+	os << (vs->gc);
+
+	// return true if os.str() inserted in the set 'strie' successfully 
+	return (pstrie.insert(os.str())).second; 
+}
+
+
+// make a atomic state with transitions del1 and del2, tsm's w1 and w2 and with 'gc' flag
+pds_state* atomic(char del1, char del2, char w1, char w2, char gc){
+	pds_state *vs = new pds_state(); // allocate memory for new state
+
+	vs->w1 = w1;
+	vs->w2 = w2;
+		
+	vs->del1 = del1;
+	vs->del2 = del2;
+	
+	vs->gc = gc;
+	
+	return vs;
+} 
+
+
+
+pds_state* pds_state::add_stack() {
+
+	// if push edge already added to left point(bit 1) or pop edge already added to right point(bit 2)
+	if(gc & 6) // looking at 1st and 2nd bit from right side(bit position starts from 0)
+		return NULL;
+
+	if( !isPush(del1) || !isPop(del2) ) // there must be a push at first point and pop at 2nd point
+		return NULL;
+		
+	if(transitions[del1].as != transitions[del2].as) // push and pop stack symbol must be same
+		return NULL;
+	
+	int lb = transitions[del2].lbs[0]; // lower bound for symbol age
+	int ub = transitions[del2].ubs[0];// upper bound
+	
+	// if distance between two points is big, but upper bound is not infinity
+	if( (gc & 1) == 0 && ub != INF)
+		return NULL;
+		
+	//if distance between two points is accurate
+	if(gc & 1) {
+		int dis = mod(w2-w1, M);
+		if(dis < lb || dis > ub) // distance must be compatible with the bounds
+			return NULL;
+	}
+	
+	
+	// create the new state	
+	pds_state *vs = new pds_state(); // allocate memory for new state
+	
+	vs->w1 = w1;
+	vs->w2 = w2;
+		
+	vs->del1 = del1;
+	vs->del2 = del2;
+	
+	vs->gc = gc | 6; // distance remain same but push pop edge added
+	
+	return vs;
+
+}
+
+
+
+// shuffle of two system states
+pds_state* pds_state::shuffle(pds_state *s2){ // shuffle  with state s2{
+	
+	if( del2 != (s2->del1) || w2 != (s2->w1) )
+		return NULL;
+		
+	if( isPush(s2->del1) && ( (s2->gc) & 2 ) == 0 ) // if there is a push of first point of 2nd state, but not yet done
+		return NULL;
+		
+	if( isPop(del2) && (gc & 4) == 0 ) // if there is a pop of second point of 1st state, but not yet done
+		return NULL;
+		
+	pds_state *vs = new pds_state(); // allocate memory for new state
+
+	vs->w1 = w1;
+	vs->w2 = s2->w2;
+		
+	vs->del1 = del1;
+	vs->del2 = s2->del2;
+	
+	// push info of first state and pop info of second state
+	vs->gc = (gc & 2) | ( (s2->gc) & 4 );
+	
+	// if both distance is accurate
+	if( (gc & 1) && ( (s2->gc) & 1) ) {
+		short int dis = mod(w2-w1, M) + mod(s2->w2 - s2->w1, M);
+		//if(del1 == 1 && del2 == 3 && (s2->del1) == 3 && (s2->del2) == 4 && w1 )
+		if(dis < M)
+			vs->gc |= 1; // distance between two points of new state is accurate
+	}
+	
+	return vs;
+}	
+	
+
+
+// if this state is a final state // DONE
+bool pds_state::isFinal(){
+	
+	if( isPush(del1) && (gc & 2) == 0 ) // if there is a push at left point, but not done yet
+		return false;
+		
+	if( isPop(del2) &&  (gc & 4) == 0) // if there is a pop at left point, but not done yet
+		return false;
+	
+	if( transitions[del1].source != SI) // remember 0  is the new initial state
+		return false;
+		
+	// target state of the transiton at point R should be a final state
+	if( transitions[del2].target != SF) 
+		return false;
+		
+	return true;
+}
+
+
+
+// print a validity state
+void pds_state::print() {
+	cout << "Abstract state of the on the fly tree automata:" << endl;
+	cout << "\tTransitions : " << int(del1) << ", " << int(del2) << endl;
+	cout << "\tTSM : " << int(w1) << ", " << int(w2) << endl;
+	cout << "\tPush done at first transition : " << bool(gc & 2) << endl;
+	cout << "\tPop done at second transition : " << bool(gc & 4) << endl;
+	cout << "\tAccuracy : " << bool(gc & 1) << endl;
+}
+
+
+
+
+pds_run* getatomicrunpds(pds_state* vs) {
+	pds_run *pr = new pds_run();
+	pr->P = 2;
+	pr->del = new char[2];
+	pr->w = new char[2];
+	pr->ac = new char[2];
+	
+	pr->del[0] = vs->del1;
+	pr->del[1] = vs->del2;
+	
+	pr->w[0] = vs->w1;
+	pr->w[1] = vs->w2;
+	
+	if( (vs->gc) & 1)
+		pr->ac[0] = 1;
+	else
+		pr->ac[1] = 0;
+	
+	return pr;
+}
+
+
+pds_run* pds_run::add_stack() {
+	return this;
+}
+
+
+void pds_run::print() {
+	short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps
+	bool lac = true; // last accuracy
+	cout << endl << "A run of the automation as a proof that the language is non-empty, the run given as a sequence of pairs (transition, time stamp) : " << endl;
+	//cout << "Left:" << int(L) << ",#points : " << int(P) << endl;
+	//cout << "L:" << int(act[L-1]) << ",R:" << int(act[P-1]) << endl;
+	
+	for(char i=0; i < P; i++) {
+	
+		// this two line changes for accuracy
+		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);
+			
+		if(!lac)
+			ct += M;
+		lac = ac[i];
+			
+		lt = w[i];
+			
+		cout << "(" << int(del[i]) << ", " << int(ct)  << ".0" << "), ";
+	}
+	
+	cout << endl << endl;
+}
+
+
+pds_run* pds_run::shuffle(pds_run *s2) {
+	pds_run *pr = new pds_run();
+	pr->P =  P + (s2->P) - 1;
+	
+	pr->del = new char[pr->P];
+	pr->w = new char[pr->P];
+	pr->ac = new char[pr->P];
+	
+	char i, j;
+	
+	for(i=0, j =0; i < (P-1); i++, j++) {
+		pr->w[j] = w[i];
+		pr->del[j] = del[i];
+		pr->ac[j] = ac[i];
+	}
+	
+	for(i=0; i < (s2->P); i++, j++) {
+		pr->w[j] = s2->w[i];
+		pr->del[j] = s2->del[i];
+		pr->ac[j] = s2->ac[i];
+	}
+	
+	return pr;
+}
+
+// get the run of the timed system starting from i-th index state of all states 'states'
+pds_run* printRun(vector<pds_state*> &states, vector<bp_pds> &v, int i) {
+	bp_pds bp = v[i]; // backpropagation information for i-th index state
+	
+	pds_run *rs, *rs1, *rs2;
+		
+	if( (bp.type) == 0) { // if the i-th state is an atomic state
+		//cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << endl;
+		//states[i]->print();
+
+		return getatomicrunpds(states[i]);
+	}
+	
+	if( (bp.type) == 1) { // if state states[i] is obtained by forgetting color 'bp.f' from state states[bp.left]
+		rs = printRun(states, v, bp.left);
+		rs = rs->add_stack();
+		//cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << endl;
+		//states[i]->print();
+
+		return rs;
+	}
+	
+	
+	
+	rs1 = printRun(states, v, bp.left); // get run for the state states[bp.left]
+	rs2 = printRun(states, v, bp.right);// get run for the state states[bp.right]
+	rs = rs1->shuffle(rs2); // shuffle two runs rs1 and rs2 with accuracy given by bp.ac
+	
+	//cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << endl;
+	//states[i]->print();
+
+	return rs;
+}
+
+
+
+bool pdsempty() {
+	// for all the transitions, take prev and next transitions
+	int i,j, d1, d2;
+	int w1, w2;
+	int N=0, count;
+	int dis;
+	vector<pds_state*> states;
+	pds_state* vs, rs;
+	vector<bp_pds> vrs; // vector for keeping track of connection between current states with previous states
+	bp_pds xrs; // bac
+	
+	pds_run *prs, *prs1, *prs2;
+	
+	xrs.type = 0; // atomic state type
+	
+	for(short int q = 1; q <= S; q++) {
+		for(i = 0; i < prevtrans[q].size(); i++) {
+		
+			d1 = prevtrans[q][i];
+			for(j=0; j < nexttrans[q].size(); j++) {
+				d2 = nexttrans[q][j];
+				
+				for(w1=0; w1 < M; w1++) {
+					for(w2=0; w2  < M; w2++) {
+					
+						vs = atomic(d1, d2, w1, w2, 1); // atomic state with distance accurate
+						if(vs != NULL && identity(vs) ) {
+							
+							states.push_back(vs);
+							vrs.push_back(xrs);
+							N++;
+							
+							if(vs->isFinal()) {
+								vs->print();
+								prs = printRun(states, vrs, N-1);
+								prs->print();
+								return false;
+							}
+							
+							
+						}
+						
+						vs = atomic(d1, d2, w1, w2, 0); // atomic state with distance big
+						if(vs != NULL && identity(vs) ) {
+							
+							
+							states.push_back(vs);
+							vrs.push_back(xrs);
+							N++;
+							
+							if(vs->isFinal()) {
+								vs->print();
+								prs = printRun(states, vrs, N-1);
+								prs->print();
+								return false;
+							}
+						}
+					}
+				}
+			}
+		}
+	}
+	
+	//cout << "PASS" << N  << endl;
+	
+	// iterate through all the states and generate new state
+	for(count = 0; count < N; count++) {
+	
+		if(count %5000 == 0)
+			cout << "#states" << endl;
+	
+		if( (count % 100) == 0 || count <= 100) // print #iterations
+			cout << count << endl;
+			
+		//if(count <= 648 && (states[count]->w1) == 0 && (states[count]->w2) == 0 )
+			//states[count]->print();
+			
+		vs = states[count]->add_stack();
+		if(vs != NULL && identity(vs) ) {
+			xrs.type = 1; // add_stack type
+			xrs.left = count;
+			
+			states.push_back(vs);
+			vrs.push_back(xrs);
+			N++;
+			
+			if(vs->isFinal()) {
+				vs->print();
+				prs = printRun(states, vrs, N-1);
+				prs->print();
+				return false;
+			}
+			
+		}
+		
+		
+		for(i=0; i <= count; i++) {
+			xrs.type = 2; // shuffle type
+			
+			vs = states[count]->shuffle(states[i]);
+			if(vs != NULL && identity(vs) ) {
+				xrs.left = count;
+				xrs.right = i;
+				
+				states.push_back(vs);
+				vrs.push_back(xrs);
+				N++;
+				
+				if(vs->isFinal()) {
+					vs->print();
+					prs = printRun(states, vrs, N-1);
+					prs->print();
+					return false;
+				}
+				
+			}
+			
+			// shuffle i-th state with 'count'-th state
+			vs = states[i]->shuffle(states[count]);
+			
+			if(vs != NULL && identity(vs) ) {
+				xrs.left = i;
+				xrs.right = count;
+				
+				states.push_back(vs);
+				vrs.push_back(xrs);
+				N++;
+				
+				if(vs->isFinal()) {
+					prs = printRun(states, vrs, N-1);
+					prs->print();
+					vs->print();
+					return false;
+				}
+				
+			}
+		}
+						
+	}
+	return true;
+}

src/timePushDown.cpp

+#include<fstream>
+#include<iostream>
+#include<stdlib.h>
+#include"timePushDown.h"
+#include"treeBitOperations.h"
+
+
+using namespace std;
+
+
+
+char inputfilename[100]; // input file name for timed push-down system
+
+
+int M; // maximum constant+1 in the timed system
+int MN; // maximum constant by the user
+bool allac; // all consecutive distance accurate or not
+
+short S; // number of states in the timed system
+short SI; // initial state
+short SF; // final state
+
+short T; // number of transitions in the timed system
+char X; // number of clocks in the timed system
+char A; // number of events or actions in the timed system
+char AS; // number of stack symbols in the timed system
+
+transition *transitions; // transitions of the timed system
+vector<vector<short int> > prevtrans; // prevtrans[i] : list of previous transitions for state i
+vector<vector<short int> > nexttrans; // nexttrans[i] : list of next transitions for state i
+
+
+vector<vector<short int> > resettrans; // resettrans[i] : list of reset transitions for clock i
+vector<vector<short int> > checktrans; // checktrans[i] : list of check transitions for clock i
+vector<vector<pair<short int, short int> > > resecktrans; // resecktrans[i] : list of reset-check transitions for clock i
+
+// this applies for one clock TPDA
+vector<vector<short int> > possibleresets; // possibleresets[t] : list of reset transitions for clock x_1 possible for the check transition t of clock x_1
+
+
+// pushDone[t][w] : 1 iff atomic state generated with starting trans t with tsm w
+bool** pushDone;
+
+// 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) {
+	short int s = transitions[i].target;
+	for(int j=0; j < nexttrans[s].size(); j++) {
+		short int t = nexttrans[s][j];
+		
+		if( isChecked(x, t) && !(*flag) && acttran == t) {
+			resecktrans[x].push_back(make_pair(acttran, t));
+			*flag = true;
+		}
+		
+		if( !visit[t] ) { // if transition t is not visited yet
+			visit[t] = true;
+			if(isChecked(x, t)) { // if x is reset at transition t
+				resecktrans[x].push_back(make_pair(acttran, t));
+			}
+			
+			if(!isReset(x, t)) { // if clock x is not reset at transition t
+				getChecker(acttran, visit, t, x, flag);
+			}
+		}
+		
+	}
+}
+
+
+// get all the reset-check pair of transition for some clock
+void getresecktrans() {
+
+	bool *visit = new bool[T+1];
+	int i,j;
+	resecktrans.resize(X+1);
+	bool flag = false;
+	
+	for(char x=1; x <= X; x++) { // iterate through all clocks
+		for(i=0; i <= T; i++) { // for all transitions
+			if( (transitions[i].target) == (transitions[i].source) && isReset(x, i) && isChecked(x, i)) {
+				resecktrans[x].push_back(make_pair(i, i));
+				flag = true;
+			}
+			if(isReset(x, i)) { //  if clock x is reset at transition i
+				for(j=0; j <= T; j++)
+					visit[j] = false;
+				visit[i] = true;
+				getChecker(i, visit, i, x, &flag);
+			}
+		}
+	}
+	
+	// for each clock x and each check(x # c) transition t, find the reset transitions(x:=0)
+	possibleresets.resize(T+1);	
+	for(i=0; i < resecktrans[1].size(); i++) {
+		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)
+bool isPossibleReset(char d1, char d2){
+	for(char i=0; i < possibleresets[d2].size(); i++) {
+		if(d1 == (possibleresets[d2][i]) )
+			return true;
+	}
+	return false;
+}
+
+// get the input timed system given as a file(file name stored in the global variable 'inputfilename')
+void inputSystem() {
+
+	int x; // temporary variable
+	int i, j; // loopers
+	int lb, ub; // used as lower and upper bound
+	int noofguards, noofresets; // #gurads and #reset clocks in a transition
+	int guard, reset;
+	
+	
+	//ifstream tiimeinfile ("in"); // timed system input file stream
+	ifstream tiimeinfile (inputfilename); // timed system input file stream
+	
+	
+	// if there is any error opening the file 		
+	if( !(tiimeinfile.is_open()) )  { 
+		cout << "\n****INPUT TIMED PUSH-DOWN FILE NOT FOUND ! ****\n"; 		
+		exit(1);
+	}
+	
+	tiimeinfile >> S; // #states in origianl automata
+	
+	tiimeinfile >> T; // #transitions
+	transitions = new transition[T+1]; // allocate memory for transitions
+	
+	tiimeinfile >> x; // #clocks 
+	X = x;	
+	
+	tiimeinfile >> x; // #actions
+	A = x;	
+	 	
+	tiimeinfile >> x; // #stack_symbols
+	AS = x;	
+	
+	tiimeinfile >> SI;  // input initial state
+	tiimeinfile >> SF;  // input final state
+	
+	// 0-th transition
+	transitions[0].source = 0;
+	transitions[0].target = SI;
+	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].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
+
+	// Reset all clocks at 0-th transition
+	transitions[0].reset = ( b32[X] & (~1) );
+	
+	resettrans.resize(X+1); // used for earlier code
+	checktrans.resize(X+1); // used for earlier
+
+	// all clock has been reset at 0-th transition
+	for(j=1; j <= X; j++) {
+		resettrans[j].push_back(0);
+	}
+	
+	// get all the transitions
+	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;
+		}
+	}
+	
+}
+
+
+void print_system() {
+	cout << "#States :" << S << endl;
+	cout << "#Transitions :" << T << endl;
+	cout << "Initial state :" << SI << endl;
+	cout << "Final state :" << SF << endl;
+	cout << "#Clocks :" << int(X) << endl;
+	cout << "#actions :" << int(A) << endl;
+	cout << "#Stack symbols :" << int(AS) << endl << endl;
+	
+	cout << "Showing the transitions:" << endl << endl;
+	
+	int reset, guard;
+	
+	
+	int i,j;
+	for(i = 0; i < T; i++) {
+		reset = transitions[i].reset;
+		guard = transitions[i].guard;
+		
+		cout << i << "-th transition :\n";
+		cout << "\tGurad bit vector : " << inttobinary(transitions[i].guard) << endl;
+		cout << "\tClock Constraints:\n";
+		for(j=1; j <= X; j++) {
+			if( (transitions[i].guard) & a32[j]) {
+				cout << "\t\t" << (transitions[i].lbs[j]) << " <= x" << j ;
+				if( (transitions[i].ubs[j]) == INF) 
+					cout << " <= inf" << endl;
+				else
+					cout << " <= " << (transitions[i].ubs[j]) << endl;
+			}
+		}
+		//cout << endl << endl;
+		cout << "\tReset bit vector : " << inttobinary(transitions[i].reset) << endl;
+		cout << "\tReset = {";
+		for(j=1; j <= X; j++) {
+			if( (transitions[i].reset) & a32[j])
+				cout << " x" << j ;
+		}
+		
+		cout << "}" << endl;
+		
+		cout << "\tStack operation : ";
+		 
+		if( !(guard & 1) && !(reset & 1) ) {
+			cout << "nop" << endl;
+		}
+		
+		else if( (guard & 1) && !(reset & 1) ) {
+			cout << "push" << endl;
+			cout << "\t\tstack symbol : " << int(transitions[i].ps) << endl ;
+		}
+		
+		else if( !(guard & 1) && (reset & 1) ) {
+			cout << "pop" << endl;
+			cout << "\t\tstack symbol : " << int(transitions[i].pp) << endl ;
+			cout << "\t\tpop condition : " << (transitions[i].lbs[0]) << " <= age(" << int(transitions[i].pp) << ") <= ";
+			if( (transitions[i].ubs[0]) == INF) 
+					cout << "inf" << endl;
+			else
+				cout << (transitions[i].ubs[0]) << endl;
+		}
+		
+		else if( (guard & 1) && (reset & 1) ) {
+			cout << "pop & push" << endl;
+			cout << "\t\tpop symbol : " << int(transitions[i].pp) << endl ;
+			cout << "\t\tpop condition : " << (transitions[i].lbs[0]) << " <= age(" << int(transitions[i].pp) << ") <= ";
+			if( (transitions[i].ubs[0]) == INF) 
+					cout << "inf" << endl;
+			else
+				cout << (transitions[i].ubs[0]) << endl;
+			cout << "\t\tpush symbol : " << int(transitions[i].ps) << endl ;
+		}
+		
+		
+		cout << endl << endl;
+	}
+	
+	
+	/*
+	cout << endl << "Printing source and target transitions:" << endl;
+	for(i=0; i <= S; i++) {
+		cout << "State " << i << ":" << endl;
+		cout << "\t Previous transitions: " ;
+		for(j = 0 ; j < prevtrans[i].size(); j++)
+			cout << prevtrans[i][j] << ",";
+		cout << "\n\t Next transitions: " ;
+		for(j = 0 ; j < nexttrans[i].size(); j++)
+			cout << nexttrans[i][j] << ",";
+		cout << endl << endl; 
+	}
+
+	cout << endl << "Printing reset transitions for clocks:" << endl;
+	for(i=1; i <= X; i++) {
+		cout << "Clock " << int(i) << ": ";
+		for(j=0; j < resettrans[i].size(); j++)
+			cout << resettrans[i][j] << ",";
+		cout << endl;
+	}
+	cout << endl << endl;
+
+	cout << endl << "Printing check transitions for clocks:" << endl;
+	for(i=1; i <= X; i++) {
+		cout << "Clock " << int(i) << ": ";
+		for(j=0; j < checktrans[i].size(); j++)
+			cout << checktrans[i][j] << ",";
+		cout << endl;
+	}
+	*/
+	cout << endl << endl;
+}
+
+
+
+// is clock x has been reset at transition d
+bool isReset(char x, short int d) {
+	if( (transitions[d].reset) & a32[x])
+		return true;
+	return false;
+}
+
+
+// is clock x has been checked at transition delta
+bool isChecked(char x, short int d) {
+	if( (transitions[d].guard) & a32[x])
+		return true;
+	return false;
+}
+
+// is there a push at transition delta
+bool isPush(short int d) {
+	if( (transitions[d].guard) & a32[0])
+		return true;
+	return false;
+}
+
+// is there a pop at transition delta
+bool isPop(short int d) {
+	if( (transitions[d].reset) & a32[0])
+		return true;
+	return false;
+}
+
+
+// return a mod b(always return a +ve number unlike c % operator) // DONE
+short int mod(short int a, short int b) {
+	short int r = a % b;
+	if(r < 0)
+		return (r+b);
+	return r;
+}

src/tpda2.cpp

+#include<tpda2.h>
+#include"timePushDown.h"
+#include"treeBitOperations.h"
+#include<iostream>
+#include<sstream>
+
+
+using namespace std;
+
+// construction of state with given trans and tsm values
+stpdastate* atomicstpda(char d1, char d2, char w1, char w2, char gc){
+
+	stpdastate *vs = new stpdastate();
+	
+	vs->d1 = d1;
+	vs->d2 = d2;
+	
+	vs->w1 = w1;
+	vs->w2 = w2;
+	
+	vs->gc = gc;
+	
+	return vs;
+}
+
+
+// shuffle of two states
+stpdastate* stpdastate::shuffle(stpdastate *s2) {
+
+	// transion at L of s2 should be same as transion at R of this state, tsm values as well better be equal
+	if( d2 != (s2->d1) || w2 != (s2->w1) )
+		return NULL;
+		
+	
+		
+	// there should be a push at L and pop at R of state s2
+	if( !isPush(s2->d1) || !isPop(s2->d2) )
+		return NULL;
+		
+	
+	/*	******** THIS IS A HUGE MISTAKE , IN OTHER FILES ALSO *****************, REMOVE THIS
+	// push and pop symbol must be same
+	if( (transitions[s2->d1].ps) != (transitions[s2->d2].pp) )
+		return NULL;
+	*/
+		
+	//cout << "ilias" << endl;
+		
+	// push-pop edge between L and R of s2 should be added
+	if( ( (s2->gc) & 1 ) == 0 ) // push-pop edge not added yet
+		return NULL;
+		
+	char gcn; // flag for the new state
+	
+	// if distance between two end points is accurate in both the states
+	if( (gc & 2) && ( (s2->gc) & 2 ) ) {
+		short d13 = mod(w2-w1, M) + mod(s2->w2 - s2->w1, M);
+		if(d13 < M)
+			gcn = (gc & 1) | ( (s2->gc) & 128) | 2;
+		else
+			gcn = (gc & 1) | ( (s2->gc) & 128);
+			
+	}
+	
+	else
+		gcn = (gc & 1) | ( (s2->gc) & 128);
+		
+	return	atomicstpda(d1, s2->d2, w1, s2->w2, gcn);
+}
+
+
+
+// given trans 0 or a push trans d1(with tsm w1), find the next possible trans d2(with tsm w2)
+vector<stpdastate*> getAtomicsSTPDA(char d1, char w1) {
+	vector<stpdastate*> v;//vector contains states by adding a upcoming transition to right side
+	
+	char q = transitions[d1].target; // target state of trans d4
+	
+	char d2, w2; // next trans and tsm value
+	char gcn; // new flag variable for state
+	
+	int lb, ub; // pop bounds
+	int lbc, ubc; // clock bounds
+	
+	bool checkflag; // true : there is a check at d2
+	bool popflag; // true : there is a pop at d2
+	
+	// iterate through all the upcoming transitions
+	for(char i=0; i < nexttrans[q].size(); i++) {
+		d2 = nexttrans[q][i]; // i-th upcoming transition
+		
+		lb = transitions[d2].lbs[0]; // lower bound for stack
+		ub = transitions[d2].ubs[0]; // upper bound for stack 
+		
+		lbc = transitions[d2].lbs[1]; // lower bound for clock
+		ubc = transitions[d2].ubs[1]; // upper bound for clock
+		
+		checkflag = isChecked(1, d2); // true : there is a check at d2
+		popflag = isPop(d2); // true : there is a pop at d2
+		
+		// note  : distance between d1 and d2 is always accurate
+		if(popflag) {
+			if( isPush(d2) )
+				gcn = 1 | 2;	// push edge added, but pop edge not added(add before a push)
+			else
+				gcn = 1 | 128 | 2; // push and pop both edges added
+		}	
+
+		else
+			gcn = 2;
+		
+		// if there is a pop at d2, there must a push at d1
+		if( popflag && !isPush(d1) ) { }
+		
+		// push symbol at d1 must be same as pop symbol at d2
+		else if( popflag && ( transitions[d1].ps != transitions[d2].pp) ) { }
+
+		
+		else{
+			short int d12;
+			for(w2 = 0; w2 < M; w2++) {
+				d12 = mod(w2-w1, M);
+				if( ( !checkflag || (d12 >= lbc && d12 <= ubc) ) && ( !popflag || (d12 >= lb && d12 <= ub) ) ){
+					v.push_back( atomicstpda(d1, d2, w1, w2, gcn) );
+				}
+			}
+		}
+	}
+	return v;
+}
+
+
+/*Add the next transition to the current state*/
+/*if there is a push at R, then don't call here*******/
+vector<stpdastate*> stpdastate::addNextTPDA() {
+	vector<stpdastate*> v; // set of states generated by adding a new transition to the right side
+	
+	if( isPush(d2) ) // there should not be any push at R
+		return v; // return empty vector
+	
+	/*	// In new technique, pop and push can be at the same time, this check is not needed
+	if( isPop(d2) && ( gc & 128 ) == 0 ) // there is a pop at d2, but pop edge not added yet
+		return v;
+	*/
+		
+	// if there is a push at L and there is a pop at R, then first shuffle, then add new transitions
+	if( isPush(d1) && isPop(d2) &&  (gc & 1) )
+		return v;
+	
+	char d3, w3; // transion and tsm at newly added rightmost point
+	char gc2, gcn; // gc2 : temp flag, gcn : new state flag
+
+	bool checkflag;
+	bool popflag;
+	
+	int lbc, ubc; // clock constraint's bound
+	int lb, ub; // lower and upper bound for stack
+	short d13, d23;
+
+	char q = transitions[d2].target; // target state of trans d4
+	
+	// iterate through all the upcoming transitions
+	for(char i=0; i < nexttrans[q].size(); i++) {
+	
+		d3 = nexttrans[q][i]; // i-th upcoming transition
+		
+		lb = transitions[d3].lbs[0]; // lower bound for stack
+		ub = transitions[d3].ubs[0]; // upper bound for stack 
+		
+		lbc = transitions[d3].lbs[1]; // lower bound for clock
+		ubc = transitions[d3].ubs[1]; // upper bound for clock
+		
+		checkflag = isChecked(1, d3);
+		popflag = isPop(d3);
+		
+		if( popflag ) { // push pop both are being done
+			if( isPush(d3) )
+				gc2 = 1;
+			else
+				gc2 = 1 | 128;
+		}
+		else // push info of previous state
+			gc2 = (gc & 1);
+		
+		// if there is a pop at d5, but no push at d2
+		if( popflag && !isPush(d1) ) { }
+		
+		// if there is a pop at d3, but  push is already done at d1
+		else if( popflag && (gc & 1) ) { }
+		
+		// push-pop symbol is not same
+		else if( popflag && ( transitions[d1].ps != transitions[d3].pp) ) { }
+		
+		// o.w add new transtitions to the right
+		else{
+			if(gc & 2) {
+				for(w3 = 0; w3 < M; w3++) {
+					d23 = mod(w3-w2, M);
+					d13 = mod(w2-w1, M) + d23;
+					if(d13 < M)
+						gcn = gc2 | 2;
+					else
+						gcn = gc2;
+						
+					if( ( !checkflag || ( d23 >= lbc && d23 <= ubc ) ) && ( !popflag || ( d13 >= lb && d13 <= ub ) ) )
+						v.push_back( atomicstpda(d1, d3, w1, w3, gcn) );
+				}
+			}
+			
+			else if(ub == INF) {
+				gcn = gc2;
+				for(w3 = 0; w3 < M; w3++) {
+					d23 = mod(w3-w2, M);
+					if( !checkflag || (d23 >= lbc && d23 <= ubc) )
+						v.push_back( atomicstpda(d1, d3, w1, w3, gcn) );
+				}
+				
+			}
+		}
+	}
+	
+	return v;
+}
+
+
+set<string> stpdatrie;
+
+bool identity(stpdastate *vs) {
+	ostringstream os; // output stream
+	
+	os << (vs->d1) << (vs->d2);
+	os << (vs->w1) << (vs->w2);
+	os << (vs->gc);
+
+	// return true if os.str() inserted in the set 'strie' successfully 
+	return (stpdatrie.insert(os.str())).second; 
+}
+
+// print a state of tree automation
+void stpdastate::print() {
+	cout << "\nAbstarct tree automation state:\n";
+	
+	cout << "\tTransitions : " << int(d1) << ",  " << int(d2) << endl;
+	
+	cout << "\tTSM : " << int(w1) << ",  " << int(w2) << endl;
+	
+	cout << "\tPush edge added to L : ";
+	if(gc & 1)
+		cout << 1 << endl;
+	else
+		cout << 0 << endl;
+		
+	cout << "\tPop edge added to R : ";
+	if(gc & 128)
+		cout << 1 << endl;
+	else
+		cout << 0 << endl;
+		
+	cout << "\tpush at L : ";
+	if(isPush(d1))
+		cout << int(transitions[d1].ps) << endl;
+	else
+		cout << endl;
+		
+	cout << "\tpop at L : ";
+	if(isPop(d1))
+		cout << int(transitions[d1].pp) << endl;
+	else
+		cout << endl;
+		
+	cout << "\tpush at R : ";
+	if(isPush(d2))
+		cout << int(transitions[d2].ps) << endl;
+	else
+		cout << endl;
+		
+	cout << "\tpop at R : ";
+	if(isPop(d2))
+		cout << int(transitions[d2].pp) << endl;
+	else
+		cout << endl;
+	
+	cout << "\tAccuracy : " << bool(gc & 2) << endl;
+	
+	cout << "\tFlag : " << bool(gc & 128) <<bool(gc & 64) <<bool(gc & 32) <<bool(gc & 16) <<bool(gc & 8) <<bool(gc & 4) <<bool(gc & 2) <<bool(gc & 1) <<endl; 
+	cout << endl;
+}
+
+
+// return true : if current state is final
+bool stpdastate::isFinal() {
+		
+	if(isPush(d2))
+		return false;
+	
+	// this below test can make sure that in the last transition there is no push along with the pop
+	if( isPop(d2) &&  (gc & 128) == 0) // there is a pop at d4, but not added yet
+		return false;
+		
+	// 0 is initial state for a tpda
+	if( transitions[d1].source != 0) // remember 0  is the new initial state
+		return false;
+		
+	if(w1 != 0) // first time stamp must be 0
+		return false;
+		
+	// target state of the transiton at point R should be a final state
+	if( transitions[d2].target != SF) 
+		return false;
+		
+	return true;
+}
+
+
+// given a atomic tree automation state give a run of the TPDA
+stpda_run* getatomicrunstpda(stpdastate* vs) {
+	stpda_run *rs = new stpda_run();
+
+	rs->P = 2;
+	rs->del = new char[2];
+	rs->w = new char[2];
+	
+	rs->del[0] = vs->d1;
+	rs->del[1] = vs->d2;
+	
+	rs->w[0] = vs->w1;
+	rs->w[1] = vs->w2;
+	
+	return rs;
+}
+
+
+// GIVEN the current run, append the trans d5 with tsm w5
+stpda_run* stpda_run::add_next(char d3, char w3) {
+	stpda_run *pr = new stpda_run();
+	
+	pr->P =  P + 1;
+	pr->del = new char[pr->P];
+	pr->w = new char[pr->P];
+	
+	for(char i=0; i < P; i++) {
+		pr->del[i] = del[i];
+		pr->w[i] = w[i];
+	}
+	
+	pr->del[P] = d3;
+	pr->w[P] = w3;
+	
+	return pr;
+}
+
+
+// shuffle two runs
+stpda_run* stpda_run::shuffle(stpda_run *s2) {
+	stpda_run *pr = new stpda_run();
+	
+	pr->P =  P + (s2->P) - 1;
+	
+	pr->del = new char[pr->P];
+	pr->w = new char[pr->P];
+	
+	char i, j;
+	
+	for(i=0, j=0; i < (P-1); i++, j++) {
+		pr->w[j] = w[i];
+		pr->del[j] = del[i];
+	}
+	
+	for(i=0; i < (s2->P); i++, j++) {
+		pr->w[j] = s2->w[i];
+		pr->del[j] = s2->del[i];
+	}
+	
+	return pr;
+}
+
+
+// print a run of the given TPDA
+void stpda_run::print() {
+	short int lt = 0, ct=0; // lt : last timestamps, ct : current time stamps
+	cout << endl << "A run of the automation as a proof that the language is non-empty, the run given as a sequence of pairs (transition, time stamp) : " << endl;
+//cout << "(0, 0.0) ";
+	for(char i=0; i < P; i++) {
+	
+		// this two line changes for accuracy
+		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" << ") -> " << "(" << int(transitions[del[i]].target) << ", " << int(ct) << ".0"  << " ";
+		
+		cout << "(" << int(del[i]) << ", " << int(ct)  << ".0" << ") ->  ";
+//		if( (transitions[del[i]].target) <= 7)
+//			cout << "-> (" << int(transitions[del[i]].target) << ", " << int(ct) << ".0)"  << " ";
+	}
+	
+	cout << endl << endl;
+}
+
+
+
+// get the run of the timed system starting from i-th index state of all states 'states'
+stpda_run* printRun(vector<stpdastate*> &states, vector<bp_stpda> &v, int i) {
+	bp_stpda bp = v[i]; // backpropagation information for i-th index state
+	
+	stpda_run *rs, *rs1, *rs2;
+		
+	if( (bp.type) == 0) { // if the i-th state is an tpda_atomic state
+		//cout << "i:" << i << "," << int(bp.type) <<  endl;
+		//states[i]->print();
+
+		return getatomicrunstpda(states[i]);
+	}
+	
+	if( (bp.type) == 1) { // if state states[i] is obtained by forgetting color 'bp.f' from state states[bp.left]
+		rs1 = printRun(states, v, bp.left);
+		
+		char d = bp.right;
+		int x = bp.right;
+		x = (x >> 8);
+		char w = x; 
+		stpdastate *vs = atomicstpda( rs1->del[rs1->P - 1], d, rs1->w[rs1->P - 1], w, 1 );
+		rs2 = getatomicrunstpda(vs);
+		rs = rs1->shuffle(rs2);
+		//cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << int(d) << "," << int(w) << endl;
+		//states[i]->print();
+
+		return rs;
+	}
+	
+	
+	
+	rs1 = printRun(states, v, bp.left); // get run for the state states[bp.left]
+	rs2 = printRun(states, v, bp.right);// get run for the state states[bp.right]
+	rs = rs1->shuffle(rs2); // shuffle two runs rs1 and rs2 with accuracy given by bp.ac
+	
+	//cout << "i:" << i << "," << int(bp.type) << "," << bp.left << "," << bp.right << endl;
+	//states[i]->print();
+
+	return rs;
+}
+
+
+
+// check if a tpda of one clock is empty or not
+bool isEmptySTPDA() {
+	
+	int N=0,count=0;
+	vector<stpdastate*> states;
+	vector<stpdastate*> v;
+	
+	stpdastate *rs, *vs;
+	
+	vector<bp_stpda> vrs; // vector for keeping track of connection between current states with previous states
+	bp_stpda xrs; // bac
+	
+	stpda_run *prs, *prs1, *prs2;
+	
+	
+	int i, t, d3, w3;
+	char w;
+	
+	xrs.type = 0; // atomic state type
+	
+	
+	v = getAtomicsSTPDA(0, 0);
+	for(i=0; i < v.size(); i++) {
+		if( identity(v[i]) ) {
+			states.push_back(v[i]);
+			vrs.push_back(xrs);
+			N++;
+			if( v[i]->isFinal() ) {
+				v[i]->print();
+				prs = printRun(states, vrs, N-1);
+				prs->print();
+				return false;
+			}
+		}
+	}
+	
+	/*
+	for(t=1; t <= T; t++) {
+		if( isPush(t) ) {
+			for(w=0; w < M; w++) {
+				v = getAtomicsSTPDA(t, w);
+				for(i=0; i < v.size(); i++) {
+					if( identity(v[i]) ) {
+						states.push_back(v[i]);
+						vrs.push_back(xrs);
+						N++;
+						if( v[i]->isFinal() ) {
+							v[i]->print();
+							prs = printRun(states, vrs, N-1);
+							prs->print();
+							return false;
+						}
+					}
+				}
+			}	
+		}
+	}
+	*/
+	
+	/*
+	for(i=0; i < N; i++) {
+		cout << "state " << i << ":" << endl;
+		states[i]->print();
+	}
+	*/
+	
+	
+	// iterate through all the states
+	for(count=0; count < N; count++) {
+	
+		if(count %5000 == 0)
+			cout << "#states" << endl;
+	
+		if( (count % 100) == 0 || count <= 100) // print #iterations
+			cout << count << endl;
+			
+		rs = states[count]; // get the state at index count
+		//rs->print();
+		
+		//***
+		xrs.type = 0;
+		if( isPush(rs->d2) && !pushDone[rs->d2][rs->w2] ) {
+			v = getAtomicsSTPDA(rs->d2, rs->w2);
+			for(i=0; i < v.size(); i++) {
+				if( identity(v[i]) ) {
+					states.push_back(v[i]);
+					vrs.push_back(xrs);
+					N++;
+					if( v[i]->isFinal() ) {
+						v[i]->print();
+						prs = printRun(states, vrs, N-1);
+						prs->print();
+						return false;
+					}
+				}
+			}
+			pushDone[rs->d2][rs->w2] = true;	
+		}
+		//****
+		
+		
+		xrs.type = 1; // add_stack type
+		xrs.left = count;
+		// try to add new trans to the state rs
+		v = rs->addNextTPDA();
+		for(i=0; i < v.size(); i++) {
+			if( identity(v[i]) ) { // if the i-th state is new
+				d3 = (v[i]->d2); w3 = (v[i]->w2);
+				xrs.right = d3 + (w3 << 8);
+				
+				states.push_back(v[i]);
+				vrs.push_back(xrs);
+				N++;
+				if( v[i]->isFinal() ) { // if this state is final
+					v[i]->print();
+					prs = printRun(states, vrs, N-1);
+					prs->print();
+					return false;
+				}
+				
+			}
+		}
+		
+		
+		xrs.type = 2; // add_stack type
+		
+		// try to do shuffle with all the previous(as left as well as right state)
+		if( isPush(rs->d2) || ( isPush(rs->d1) && isPop(rs->d2) ) ) {
+			for(i=0; i <= count; i++) {
+				xrs.left = count;
+				xrs.right = i;
+				// shuffle, considering rs as left state
+				vs = rs->shuffle( states[i] );
+				if(vs != NULL) { // if new state is valid
+					if( identity(vs) ) {
+						states.push_back(vs);
+						vrs.push_back(xrs);
+						N++;
+						if( vs->isFinal() ) {
+							vs->print();
+							prs = printRun(states, vrs, N-1);
+							prs->print();
+							return false;
+						}		
+					}
+				}
+				
+				
+				xrs.left = i;
+				xrs.right = count;
+				
+				// shuffle, considering rs as right state
+				vs = states[i]->shuffle(rs);
+				
+				if(vs != NULL) { // if new state is valid
+					if( identity(vs) ) {
+						states.push_back(vs);
+						vrs.push_back(xrs);
+						N++;
+						if( vs->isFinal() ) {
+							vs->print();
+							prs = printRun(states, vrs, N-1);
+							prs->print();
+							return false;
+						}
+						
+					}
+				}
+			}
+		}
+		
+	}
+	
+	cout << "\n\n------------------------\n" << endl;
+	states[0]->shuffle(states[3]);
+
+	return true;
+}

src/tpdaCGPP.cpp

+// This file is for general TPDA emptiness checking with continuous implementation, pop and push also can happen at the same transition
+
+#include<tpdaCGPP.h>
+#include"timePushDown.h"
+#include"treeBitOperations.h"
+#include<iostream>
+
+using namespace std;
+
+// 'tpdaGCPPtrie' is used for checking if newly generated state was already generated earlier or not
+//set<string> tpdaGCPPtrie;
+
+// 'mapGCPP' is also used for checking if newly generated state was already generated earlier or not
+unordered_map<string,bool> mapGCPP;
+
+// this vector contains all the states generated for a TPDA paried with tracking states
+vector<pair<stateGCPP*, trackCGPP*> > allStates;
+
+
+// return 1 iff state vs was not found earlier or vs is new state
+bool identity(stateGCPP *vs) {
+
+	string os=""; // output string
+	char i; // looper
+	
+	for( i=0; i < (vs->P); i++ ) // add transitions to the string os
+	    os += (vs->del[i]);
+	    
+	for(i=0; i < (vs->P); i++ ) // add tsm values to the string os
+	    os += (vs->w[i]);
+	    
+	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 += (vs->L); // add left point to os
+	
+	// return true if os inserted in the set 'tpdaGCPPtrie' successfully 
+	//return (tpdaGCPPtrie.insert(os) ).second; 
+	
+	// using hashmap : if os key was not there then mapGCPP[os]==false
+	if( mapGCPP[os] ) // 'os' is there in hashmap
+		return false;
+		
+	else{ // 'os' is not there in hashmap
+		mapGCPP[os] = true;
+		return true;;
+	}
+}
+
+
+// return distance between point i to point j
+short stateGCPP::dist(char i, char j) { 
+	short dis=0; // distance between i to j, initially 0
+    for(char k=i; k < j; k++) // sum up the distances between consecutive points
+        dis += mod( w[k] - w[k-1], M);
+    return dis;
+}
+
+
+// return true iff distance between point i to point j is big
+bool stateGCPP::big(char i, char j) { 
+    for(char k=i; k < j; k++) {
+        if( ( f & a32[k] ) == 0 ) // k-th bit of 'f' is 0 => distance  k->(k+1) is big
+            return true;
+    }
+    if( dist(i, j) >= M ) // if total distance is big
+        return true;
+    return false;
+}
+
+
+// reduce the #points after shuffle by using forget operation if possible and return the new state
+stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
+
+	char *del2 = s2->del, *w2 = s2->w;
+	char P2 = s2->P, L2 = s2->L;
+	short f2 = s2->f;
+	
+	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 );
+		
+	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) ) { // (~)  : 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
+	
+	stateGCPP *vs = new stateGCPP(); // new TA state
+	
+	vs->del = new char[count]; // allocate memory
+	vs->w = new char[count];
+	vs->L = L;
+	
+	short nf = 0; // initially flag is zero
+	short dis; // distance variable
+	
+	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
+	    
+	    // 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];
+	    
+	    // 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] );
+	}
+	
+	//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];
+	
+	// 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);
+	for(i=P-1; i >= L; i--) {
+		reset = ( transitions[ del[i] ].reset ); // current point reset set
+		if( reset & (~curReset) & (~1) ) { // if current point has more reset then seen earlier
+			vs->del[j] = del[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];
+	        }
+	        
+			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
+		// 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(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);
+            if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
+                nf |= a32[L];
+        }
+	}
+	
+	else{
+		// if distance from L-th point to lastindex+1-th of 1st state is accurate
+		if( !big(L, lastindex+1) )
+			nf |= a32[L];
+	}
+	
+	if(f & 1) // push info from left state will be same
+		nf |= 1;
+		
+	nf |= a3215; // pop at right(R) is done
+	
+	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
+bool stateGCPP::shuffleCheck(stateGCPP *s2) {
+	if( L == P || (s2->L) == (s2->P) ) // both state should have non-trival block
+		return false;	
+		
+	if( !isPush(del[P-1]) ) // there should be a push at last transition of left state
+		return false;
+		
+	// 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] ) )
+		return false;
+
+	if( !( (s2->f) & 1 ) || !( (s2->f) & a3215 )  ) // push-pop edge should be connected in right state
+		return false;
+		
+	if( getKeyLeft() != (s2->getKeyRight() ) )
+    	return false;
+	
+	return true;	
+}
+
+
+// shuffle of this state with state s2 and return the new state
+stateGCPP* stateGCPP::shuffle(stateGCPP *s2){ // shuffle  with state s2
+
+	if(! shuffleCheck(s2) )	
+		return NULL;
+
+	return reduceShuffle(s2);
+}
+
+
+
+// add transition 'dn' to current state and then forget some points if possible, return the new state
+stateGCPP* stateGCPP::reduce(char dn){
+	
+	short reset; // variable for reset bit vector
+	short nf = 0; // flag variable for new state
+	char count = 0; // #points in new state
+	char i; // looper
+	
+	short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
+	
+	for( i=P-1; i >= L; i-- ) {
+		reset = transitions[ del[i] ].reset; // reset at transition at the (i+1)-th point
+		if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has more reset than found so far at right
+			curReset |= reset; // the 'curReset' will have more bit with value '1'
+			count++; // we have to take (i+1)-th point
+		}
+	}
+	
+	// all the hanging points and point L and point for transition 'dn' also be there 
+	count += (L+1); // number of points in new state
+	
+	// pointer to the new state
+	stateGCPP* vs = new stateGCPP();
+	
+	vs->P = count; // #points in new state
+	vs->L = L; // left point remain same
+	
+	vs->del = new char[count]; // memory allocation for new state transition
+	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
+		vs->del[i] = del[i];
+		vs->w[i] = w[i];
+	}
+	
+	for(i=1; i < L; i++) { // distances between points upto point L remain same
+		nf |= ( f & a32[i] );
+	}
+	
+	vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
+	
+	char lastindex = P; // 'lastindex' used for accuracy between two points in new state
+	char firstindex;
+	char j = count-2; // assgin trans and tsm from index count-2 upto L
+	short dis; // variable for distance calculation
+	// **** edit last bit of accuracy when u know the tsm of dn
+	curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
+	for(i=P-1; i >= L; i--) {
+		reset = transitions[ del[i] ].reset; // reset at i+1-th point
+		
+		if( reset & (~curReset) & (~1) ) {
+			vs->del[j] = del[i]; // i-th index trans will be part of new state at j-th index
+			vs->w[j] = w[i]; // i-th index tsm will be part of new state at j-th index
+			
+			if( lastindex != P ) {			
+				if( !big(i+1, lastindex+1) )
+					nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state
+			}
+			
+			// store the accuracy from last point(active in new state) before dn and P in  i+1-th bit of nf
+			// store the distance from last point(active in new state) before dn and P in vs->w[count-1]
+			// we yet don't know the tsm for 'dn', so full calculation is not done in this function
+			else{ 
+				firstindex = i;
+				if( !big(i+1, P) )
+					nf |= a32[j+1];
+				vs->w[count-1] = dist(i+1, P);
+			}
+			
+			lastindex = i; // this is now the last index
+			j--; // go to previous point
+		}
+	}
+	
+	// we have to set the accuracy for point L to L+1 in new state
+	if( lastindex != P ) {
+		if( !big(L, lastindex+1) ) {
+		//	vs->w[count-1] = dist(L, lastindex+1) ;
+			nf |= a32[L]; // set the accuracy for (j+1)-th bit of new state
+		}
+	}
+	
+	// store the accuracy from last point(active in new state) before dn and P in  i+1-th bit of nf
+	// store the distance from last point(active in new state) before dn and P in vs->w[count-1]
+	// we yet don't know the tsm for 'dn', so full calculation is not done in this function
+	else{  // if you have not choosed any point in the middle starting from point P**
+		if( !big(L, P) )
+			nf |= a32[L];
+			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
+		nf |= (1 | a3215) ;
+	else
+		nf |= (f & 1) ; // previous push information remain same
+		
+	// last distance accuracy
+	vs->f = nf; // add partial flag variable to new state
+	
+	return vs; // return the partially new state, **** last tsm missing with partial nf as given
+}
+
+
+// return true if constraint on new transition dn with tsm wn is satisfied while adding current transiton 'dn' to the right
+bool stateGCPP::consSatisfied(char dn, char wn, short *clockDis, bool *clockAcc) {
+	short dis;
+	for(char x=1; x <= X; 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
+				dis = clockDis[x] + mod( wn - w[P-1], M ) ;
+				if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) )
+					return false;
+			}
+			else if( (transitions[dn].ubs[x]) != INF )
+				return false;
+		}
+	}
+	return true;
+}
+
+
+// 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.
+bool stateGCPP::stackCheck(char dn, char wn, short dlr, bool aclr) {
+	int ub =  transitions[dn].ubs[0];
+	if(aclr) { // if distance from L to R is small
+		short dis = dlr + mod( wn - w[P-1], M );
+		
+		if( ( dis < transitions[dn].lbs[0] ) || dis > ub )
+			return false;
+			
+		else 
+			return true;
+	}
+	
+	else if(ub == INF) // if distance from L to R is big
+		return true;
+		
+	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
+vector<stateGCPP*> stateGCPP::addNextTPDA() {
+
+	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)
+		return v; // return empty vector
+	
+	// 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( isPush( del[L-1] ) && isPop( del[P-1] ) && (f & 1) &&  (f & a3215) )
+		return v;
+		
+	short dlr = dist(L, P); // distance between point L to R
+	bool aclr = !big(L, P); // accuracy between point L to R
+	
+	char dn; // variable for new upcoming transition
+	char wn; // variable contain TSM for the upcoming transition
+	
+	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
+	
+	char i, j; // loooper
+	short dis; // distance calculation variable
+	
+	char q = transitions[ del[P-1] ].target; // target state of last transition
+	
+	// iterate through all the upcoming transitions
+	for(i=0; i < nexttrans[q].size(); i++) {
+	
+		dn = nexttrans[q][i]; // i-th upcoming transition
+		
+		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( popflag && !pushAtL ) { }
+		
+		// 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) ) { }
+		
+		// push-pop symbol is not same, do nothing
+		else if( popflag && ( (transitions[ del[L-1] ].ps) != (transitions[dn].pp) ) ) { }
+		
+		// o.w try to add new transtitions to the right
+		else{
+		
+			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]
+			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(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( big(j+1, P) ) // if distance is big from last reset point for clock x to point P
+							clockAcc[x] = false;
+							
+						else {
+							clockAcc[x] = true;
+							clockDis[x] = dist(j+1, P);
+						}
+						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
+			for(wn=0; wn < M; wn++) {
+			
+				// if clock constraint not satisfied
+				if( !consSatisfied( dn, wn, clockDis, clockAcc)  ) {  }
+			
+				// if stack constraint not satisfied
+				else if( ( popflag && ( !stackCheck(dn, wn, dlr, aclr) ) ) ) {  } 
+				
+				else { // if clock and stack both constraints are satisfied
+					stateGCPP* rs = new stateGCPP();
+					
+					rs->L = L; // left point remain same
+					rs-> P = vs->P; // #points in new state
+					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
+					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[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
+					
+					// 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] ) ) {
+					
+						// calculate distance from 2nd last point to last point in new state
+						dis = vs->w[vs->P - 1] + mod(wn - w[P-1], M); 
+						if(dis < M) { // reset vs->P-1 bit to 0
+							rs->f |= (a32[vs->P - 1]);
+						}
+					}
+					
+					v.push_back(rs); // rs will be a reachable state after add operation
+				}
+			}
+		}
+	}
+		
+	return v;
+}
+
+
+// Return template successor state whose descendent states will be right states for shuffle operation with this state
+stateGCPP* stateGCPP::sucState(){
+
+	short curReset, reset; // temp vars for keeping reset bit vector
+	char count; // will contain #points in the new state
+	char i,j; // counters
+	
+	// iterate through all points right to left except the last point 
+	curReset = transitions[ del[P-1] ].reset;
+	count = 1; //we have to take the last point, so initialize 'count' to 1
+
+	for(i=P-2; i >= 0; i--) {
+		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
+			count++;
+			curReset |= reset;
+		}		
+	}
+
+	
+	stateGCPP* vs = new stateGCPP(); // new template state
+	
+	vs->P = count; //#points
+	vs->L = count; // no non-trivial block is there
+	
+	vs->del = new char[count];
+	vs->w = new char[count];
+	
+	vs->del[count-1] = del[P-1];
+	vs->w[count-1] = w[P-1];
+	
+	// copy the necessary points into the template state
+	char lastindex = P-1;
+	short nf = 0; // flag variable for new state
+	curReset = transitions[ del[P-1] ].reset;
+	
+	for(i=P-2, j = count-2; i >= 0; i--) {
+		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
+			vs->del[j] = del[i];
+			vs->w[j] = w[i];
+			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
+			curReset |= reset;
+			j--;
+			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
+	
+	return vs;
+}
+
+
+
+// print a validity state
+void stateGCPP::print() {
+	char i;
+	
+	cout << endl << "Abstract state of the on the fly tree automata(TA):" << endl;
+	
+	cout << "\tPoints in the automaton:\n\t\t";
+	cout << 1 ;
+	for(i=2; i <= L; i++)
+	    cout <<  "    " << int(i) ;
+	for(i=L+1; i <= P; i++)
+	    cout << "----" << int(i) ;
+	cout << endl;
+	
+	cout << "\t\tL : " << int(L) << endl;
+	 
+	cout << "\tTransitions:";
+	
+	cout << "\t";
+	for(i=0; i < P; i++)
+	    cout << int(del[i]) << "\t";
+	cout << endl;
+	
+	cout << "\tAccuracy: " << "\t    ";
+	for(i=1; i < P; i++) {
+	    cout << ( (a32[i] & f) ? 1 : 0) << "\t    ";
+	}
+	cout << endl;
+	
+	cout << "\tTSM : \t";
+	cout << "\t";
+	for(i=0; i < P; i++)
+	    cout << int(w[i]) << "\t";
+	cout << endl;
+	    
+	
+	cout << endl << endl;
+	
+	cout << "\tPush done at L : " << ( (f & 1)? 1 : 0 ) << endl;
+	cout << "\tPop done at R : " << ( (f & a3215) ? 1 : 0) << endl;
+}
+
+// if this state is a final state
+bool stateGCPP::isFinal(){
+    
+    if(L != 1) // there should not be any hanging point
+        return false;
+        
+    // transition at first point must be 0-th transition
+	if( del[0] != 0)
+		return false;
+		
+	// there will not any push at the last transition
+	if( isPush( del[P-1] ) ) 
+		return false;
+		
+	// target state of the transiton at point R should be the final state
+	if( transitions[del[P-1]].target != SF ) 
+		return false;
+		
+	return true;
+}
+
+
+// return the partial run corresponding the tree automata state 'vs', ignore the hanging points
+// copy only transitions between L(left) and R(right)
+runCGPP* getRun(stateGCPP* vs) {
+
+	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
+	
+	// allocate memory for transitions and tsm vlaues for new run
+	pr->del = 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
+	char i = vs->L - 1, j=0;
+	
+	// copy transitions and tsm values from earlier partial run to new partial run
+	for(; i < (vs->P); i++, j++) {
+		pr->del[j] = vs->del[i];
+		pr->w[j] = vs->w[i];
+	}
+	
+	return pr; // return the new run
+}
+
+
+// GIVEN the current partial run, append the transition 'dn' with tsm value 'wn'
+runCGPP* runCGPP::addNext(char dn, char wn) {
+
+	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
+
+	// allocate memory for transitions and tsm vlaues for new run
+	pr->del = new char[pr->P]; 
+	pr->w = new char[pr->P];
+	
+	// copy transitions and tsm values from earlier partial run to new partial run
+	for(char i=0; i < P; i++) {
+		pr->del[i] = del[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->w[P] = wn;
+	
+	return pr; // return the new run
+}
+
+
+// shuffle two partial runs and return the new partial run
+runCGPP* runCGPP::shuffle(runCGPP *s2) {
+
+	runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
+	
+	/* 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*/
+	pr->P =  P + (s2->P) - 1; 
+	
+	// allocate memory for transitions and tsm vlaues for new run
+	pr->del = new char[pr->P]; 
+	pr->w = new char[pr->P];
+	
+	char i, j; // loopers
+	
+	// copy the transitions and tsm values of first run except for the last position
+	for(i=0, j=0; i < (P-1); i++, j++) {
+		pr->w[j] = w[i];
+		pr->del[j] = del[i];
+	}
+	
+	// copy the transitions and tsm values of 2nd run
+	for(i=0; i < (s2->P); i++, j++) {
+		pr->w[j] = s2->w[i];
+		pr->del[j] = s2->del[i];
+	}
+	
+	return pr; // return the new run
+}
+
+
+// this will return a state with only 0-th transition with tsm value 0
+stateGCPP* getZeroState() {
+
+	stateGCPP* vs = new stateGCPP();
+	
+	vs->L = 1; // only one point is there
+	vs->P = 1;
+	vs->f = 0; // no push pop info yet, no accuracy info yet
+	
+	vs->del = new char[1]; // memory allocation
+	vs->w = new char[1];
+	
+	vs->del[0] = 0; // 0th transition has tsm value 0
+	vs->w[0] = 0;
+	
+	return vs;
+}
+
+
+// return unique string for last reset points of current state participating in a combine operation as a left state
+string stateGCPP::getKeyLeft() {
+
+	string s = ""; // return this string
+	
+	short resetSoFar, reset; // used for calculating union of resets
+	
+	s += del[P-1]; // include rightmost transition in the string
+	s += w[P-1]; // tsm value also be part of the key
+	char lastindex = P-1; // last index we have taken
+	
+	char nf = 0; // distance info
+	char i=P-2;
+	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
+		
+		if( reset & (~resetSoFar) & (~1) ) { // if there are some new clocks reset at point (i+1)
+			s += del[i];
+			s += w[i];
+			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
+string stateGCPP::getKeyRight() {
+
+	string s = ""; // return this string as a key for current state
+	
+	// take the transition at point L and all hanging points
+	
+	char nf = 0; // this contains distance information between points
+	
+	s+= del[L-1]; // L-th poiint transition
+	s+= w[L-1]; // L-th point tsm
+	
+	char j = 0; // used for distance counter
+	char i = L-2; // counter for points from right to left starting from L-1 point
+	
+	for(; i >= 0; i--, j++) {
+		s += del[i];
+		s += w[i];
+
+		if(f & a32[i+1] )
+			nf |= a32[j];
+	}
+	
+	// add distance info in the key
+	s+= nf;
+	
+	return s;
+}
+
+
+// print a run as witness of the given TPDA if the language is non-empty
+void runCGPP::print() {
+	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;
+	
+	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;
+}
+
+
+// return a backtracking state with the info given in the parameters
+trackCGPP* getTrack(char t, int l, int r) {
+	trackCGPP* xrs = new trackCGPP();
+	xrs->type = t; // this string is empty because vs is atomic state
+	xrs->left = l;
+	xrs->right = r; // this value is 0 for atomic state vs
+	return xrs;
+}
+
+
+// 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 != "", then sm string is the key for shuffle operation of the state reside in i-th index of allStates
+runCGPP* printRun(int i) {
+
+	stateGCPP* vs; // tree automata state variable
+	trackCGPP *bp; // back tracking state
+	
+	vs = allStates[i].first;
+	bp = allStates[i].second;
+	
+	runCGPP *rs, *rs1, *rs2;
+		
+	// if the i-th state is an atomic state
+	if( (bp->type) == 0 ) {
+		//cout << endl << i << ":";
+		//vs->print();
+		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
+	else if( (bp->type) == 1 ) {
+		rs1 = printRun( bp->left );
+		rs = rs1->addNext(vs->del[vs->P - 1], vs->w[vs->P - 1]);
+		
+		//cout << endl << i << " : " << (bp->left);
+		//vs->print();
+		
+		return rs;
+	}
+	
+	else{
+		rs1 = printRun( bp->left);
+		rs2 = printRun(bp->right);
+		rs = rs1->shuffle(rs2);
+		
+		//cout << endl << i << " : " << (bp->left) << ", " << (bp->right);
+		//vs->print();
+	
+		return rs;
+	}
+}
+
+
+// return true iff language recognized by the TPDA is empty
+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)
+	if(SI == SF) {
+		cout << "Initial state is same as final state " << endl;
+		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 N=0; // total number of unique states generated so far
+	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
+	
+	// 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<stateGCPP*> v; // temporary vector for keeping a set of states
+	
+	stateGCPP *rs, *vs, *vs1, *vs2; // some state variables
+	
+	trackCGPP *xrs; // back propagarion state variable
+	
+	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
+	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
+	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  
+	int size1, size2;
+	
+	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
+	
+	// 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
+	allStates.push_back( make_pair(vs, xrs) ); // insert the state into the main vector along with its back tracking information
+	N++; // increment #states
+	
+	// iterate through all the generated states and process them to generate new state
+	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;
+//		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

+// This file is for general TPDA zone based emptiness checking with continuous implementation, pop and push also can happen at the same transition
+
+#include<tpdaZone.h>
+#include"timePushDown.h"
+#include"treeBitOperations.h"
+#include<iostream>
+
+
+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
+bool isNegCycle(short **w, bool **open, int n) {
+	for(char i=0; i < n; i++) {
+		if( w[i][i] < 0 || open[i][i] ) // if diagonal weights are strictly less than zero
+			return true;
+	}
+	return false;
+}
+
+
+short **WT1, **WT2; // used as temporary storage for weight matrix in floyd warshal algorithm
+bool **open1, **open2; // temporary variable for storing some edge is open interval or not
+
+
+
+// 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) {
+	char i,j,k; // counters
+	
+	// n iterations for floyd warshal algorithm
+	for(k=0; k < n; k++) {
+		for(i=0; i < n; i++) {
+			for(j=0; j < n; j++){
+				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
+						WT1[i][j] = WT2[i][k] + WT2[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
+						WT1[i][j] = WT2[i][j];
+						open1[i][j] = open2[i][k] || open2[k][j] || open2[i][j] ;
+					}
+
+					else {
+						WT1[i][j] = WT2[i][j];
+						open1[i][j] = open2[i][j] ;
+					}
+				}
+				
+				else{ // if k is even , transfer weights from WT1 to WT2
+					if( ( WT1[i][k] + WT1[k][j] ) < WT1[i][j] ) {
+						WT2[i][j] = WT1[i][k] + WT1[k][j];
+						open2[i][j] = open1[i][k] || open1[k][j] ;
+					}
+
+					else if( ( WT1[i][k] + WT1[k][j] ) == WT1[i][j]) {
+						WT2[i][j] = WT1[i][j];
+						open2[i][j] = open1[i][k] || open1[k][j] || open1[i][j] ;
+					}
+
+					else{
+						WT2[i][j] = WT1[i][j];
+						open2[i][j] = open1[i][j] ;
+					}
+				}
+			}
+		}
+	}
+}
+
+
+
+// used for checking if newly generated state was already generated earlier or not
+unordered_map<string,bool> mapZone;
+
+// this vector contains all the states generated for a TPDA paried with tracking states
+vector<pair<stateZone*, trackZone*> > allStatesZone;
+
+
+// return 1 iff state vs was not found earlier or vs is new state
+bool identity(stateZone *vs) {
+
+	string os=""; // output string
+	short i; // looper
+	short P = vs->P;
+	
+	
+	for( i=0; i < P; i++ ) { // add transitions to the string os
+		//cout << "i:" << int(i) << endl;
+	    os += (vs->del[i]);
+	}
+
+	P = P*P - P;
+	  //cout << P << endl;
+	for(i=0; i < P; i++ ){
+		
+	    os += char(vs->w[i]);
+	    os += char( (vs->w[i]) >> 8 ) ; //why this?
+	}
+	  
+	//cout << "ILIAS" <<  int(vs->f) << endl;
+	os += char(vs->f); // L is also included in f
+	
+	// using hashmap : if os key was not there then mapGCPP[os]==false
+	if( mapZone[os] ) // 'os' is there in hashmap
+		return false;
+		
+	else{ // 'os' is not there in hashmap
+		mapZone[os] = true;
+		return true;;
+	}
+}
+
+
+
+// reduce the #points after shuffle by using forget operation if possible and return the new state
+stateZone* stateZone::reduceShuffle(stateZone* s2) {
+
+	char *del2 = s2->del, *w2 = s2->w;
+	char P2 = s2->P, L2 = s2->L;
+	short f2 = s2->f;
+	
+	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 );
+		
+	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) ) { // (~)  : 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
+	
+	stateGCPP *vs = new stateGCPP(); // new TA state
+	
+	vs->del = new char[count]; // allocate memory
+	vs->w = new char[count];
+	vs->L = L;
+	
+	short nf = 0; // initially flag is zero
+	short dis; // distance variable
+	
+	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
+	    
+	    // 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];
+	    
+	    // 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] );
+	}
+	
+	//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];
+	
+	// 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);
+	for(i=P-1; i >= L; i--) {
+		reset = ( transitions[ del[i] ].reset ); // current point reset set
+		if( reset & (~curReset) & (~1) ) { // if current point has more reset then seen earlier
+			vs->del[j] = del[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];
+	        }
+	        
+			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
+		// 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(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);
+            if( dis < M ) // if total distance from i+1-th point to s2->L+1 is accurate
+                nf |= a32[L];
+        }
+	}
+	
+	else{
+		// if distance from L-th point to lastindex+1-th of 1st state is accurate
+		if( !big(L, lastindex+1) )
+			nf |= a32[L];
+	}
+	
+	if(f & 1) // push info from left state will be same
+		nf |= 1;
+		
+	nf |= a3215; // pop at right(R) is done
+	
+	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
+bool stateZone::shuffleCheck(stateZone *s2) {
+	if( (f&127) == P || ((s2->f)&127) == ((s2->f)&127) ) // both state should have non-trival block
+		return false;	
+		
+	if( !isPush(del[P-1]) ) // there should be a push at last transition of left state
+		return false;
+		
+	// 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] ) )
+		return false;
+        
+        
+        //why this condition?
+	//if( !( (s2->f) & 1 ) || !( (s2->f) & a3215 )  ) // push-pop edge should be connected in right state
+	//	return false;
+		
+	if( getKeyLeft() != (s2->getKeyRight() ) )
+    	return false;
+	
+	return true;	
+}
+
+
+// shuffle of this state with state s2 and return the new state
+stateGCPP* stateGCPP::shuffle(stateGCPP *s2){ // shuffle  with state s2
+
+	if(! shuffleCheck(s2) )	
+		return NULL;
+
+	return reduceShuffle(s2);
+}
+
+
+
+/*
+// add transition 'dn' to current state and then forget some points if possible, return the new state
+stateGCPP* stateGCPP::reduce(char dn){
+	
+	short reset; // variable for reset bit vector
+	short nf = 0; // flag variable for new state
+	char count = 0; // #points in new state
+	char i; // looper
+	
+	short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
+	
+	for( i=P-1; i >= L; i-- ) {
+		reset = transitions[ del[i] ].reset; // reset at transition at the (i+1)-th point
+		if( reset & (~curReset) & (~1) ) { // if (i+1)-th point has more reset than found so far at right
+			curReset |= reset; // the 'curReset' will have more bit with value '1'
+			count++; // we have to take (i+1)-th point
+		}
+	}
+	
+	// all the hanging points and point L and point for transition 'dn' also be there 
+	count += (L+1); // number of points in new state
+	
+	// pointer to the new state
+	stateGCPP* vs = new stateGCPP();
+	
+	vs->P = count; // #points in new state
+	vs->L = L; // left point remain same
+	
+	vs->del = new char[count]; // memory allocation for new state transition
+	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
+		vs->del[i] = del[i];
+		vs->w[i] = w[i];
+	}
+	
+	for(i=1; i < L; i++) { // distances between points upto point L remain same
+		nf |= ( f & a32[i] );
+	}
+	
+	vs->del[count-1] = dn; // trans at last point, till now we don't know the weight
+	
+	char lastindex = P; // 'lastindex' used for accuracy between two points in new state
+	char firstindex;
+	char j = count-2; // assgin trans and tsm from index count-2 upto L
+	short dis; // variable for distance calculation
+	// **** edit last bit of accuracy when u know the tsm of dn
+	curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
+	for(i=P-1; i >= L; i--) {
+		reset = transitions[ del[i] ].reset; // reset at i+1-th point
+		
+		if( reset & (~curReset) & (~1) ) {
+			vs->del[j] = del[i]; // i-th index trans will be part of new state at j-th index
+			vs->w[j] = w[i]; // i-th index tsm will be part of new state at j-th index
+			
+			if( lastindex != P ) {			
+				if( !big(i+1, lastindex+1) )
+					nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state
+			}
+			
+			// store the accuracy from last point(active in new state) before dn and P in  i+1-th bit of nf
+			// store the distance from last point(active in new state) before dn and P in vs->w[count-1]
+			// we yet don't know the tsm for 'dn', so full calculation is not done in this function
+			else{ 
+				firstindex = i;
+				if( !big(i+1, P) )
+					nf |= a32[j+1];
+				vs->w[count-1] = dist(i+1, P);
+			}
+			
+			lastindex = i; // this is now the last index
+			j--; // go to previous point
+		}
+	}
+	
+	// we have to set the accuracy for point L to L+1 in new state
+	if( lastindex != P ) {
+		if( !big(L, lastindex+1) ) {
+		//	vs->w[count-1] = dist(L, lastindex+1) ;
+			nf |= a32[L]; // set the accuracy for (j+1)-th bit of new state
+		}
+	}
+	
+	// store the accuracy from last point(active in new state) before dn and P in  i+1-th bit of nf
+	// store the distance from last point(active in new state) before dn and P in vs->w[count-1]
+	// we yet don't know the tsm for 'dn', so full calculation is not done in this function
+	else{  // if you have not choosed any point in the middle starting from point P**
+		if( !big(L, P) )
+			nf |= a32[L];
+			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
+		nf |= (1 | a3215) ;
+	else
+		nf |= (f & 1) ; // previous push information remain same
+		
+	// last distance accuracy
+	vs->f = nf; // add partial flag variable to new state
+	
+	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
+stateZone* stateZone::addNextTPDA(char dn) {
+	char i, j; // counters
+	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.
+
+
+	// copy weights of current 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;
+			}
+
+		}
+	}
+
+
+	// 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
+                
+
+			lb = transitions[dn].lbs[x];
+			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
+
+				if( isReset(x, del[i]) ) { // 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;
+				}
+			}
+		}
+	}
+
+	/*
+	cout << "Before" << endl;
+	for(i=0; i <= P; i++){
+		for(j=0; j <= P; j++) {
+			cout << WT1[i][j] << "." << open1[i][j] << "\t";
+		}
+		cout << endl << endl;
+	}
+
+	*/
+
+	allPairSP(P+1); //this is the Floyd–Warshall algorithm implementation
+
+
+
+	short **WT;
+	bool **open;
+
+	if(P & 1) { // if P is odd, the shortest path stored in WT1 and open1
+		WT = WT1;
+		open = open1;
+	}
+	else{ // if P is odd, the shortest path stored in WT1 and open1
+		WT = WT2;
+		open = open2;
+	}
+
+	/*
+	cout << "After" << endl;
+	for(i=0; i <= P; i++){
+		for(j=0; j <= P; j++) {
+			cout << WT[i][j] << "." << open[i][j] << "\t";
+		}
+		cout << endl << endl;
+	}
+	*/	
+
+	// 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])
+			return NULL;
+	}
+
+
+
+	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;
+	curReset = transitions[dn].reset;
+	
+	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) ) { // (~)  : 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
+		}
+		else{
+			forgetFlag |= a32[i+1]; // i+1-th point will be forgotten in new state
+		}
+	}
+
+	count += L; // all points from 1 to L will be there
+	char *newToOldRef = new char[count];
+
+	i = 0;
+	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++;
+		}
+	}
+
+
+	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 
+
+/*// Return template successor state whose descendent states will be right states for shuffle operation with this state
+stateGCPP* stateZone::sucState(){
+
+	short curReset, reset; // temp vars for keeping reset bit vector
+	char count; // will contain #points in the new state
+	char i,j; // counters
+	
+	// iterate through all points right to left except the last point 
+	curReset = transitions[ del[P-1] ].reset;
+	count = 1; //we have to take the last point, so initialize 'count' to 1
+
+	for(i=P-2; i >= 0; i--) {
+		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
+			count++;
+			curReset |= reset;
+		}		
+	}
+
+	
+	stateZone* vs = new stateZone(); // new template state
+	
+	vs->P = count; //#points
+	//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->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->w[count-1] = w[P-1]; // have to apply the upper and lower bounds
+	
+	// copy the necessary points into the template state
+	char lastindex = P-1;
+	short nf = 0; // flag variable for new state
+	curReset = transitions[ del[P-1] ].reset;
+	
+	for(i=P-2, j = count-2; i >= 0; i--) {
+		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
+			vs->del[j] = del[i];
+			vs->w[j] = w[i];
+			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
+			curReset |= reset;
+			j--;
+			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
+	
+	return vs;
+}
+ * */
+
+
+
+// print a validity state
+void stateZone::print() {
+	char i, j;
+	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 << "\tPoints in the automaton:\n\t\t";
+	cout << 1 ;
+	for(i=2; i <= L; i++)
+	    cout <<  "    " << int(i) ;
+	for(i=L+1; i <= P; i++)
+	    cout << "----" << int(i) ;
+	cout << endl;
+	
+	cout << "\t\tL : " << int(L) << endl;
+	 
+	cout << "\tTransitions:";
+	
+	cout << "\t";
+	for(i=0; i < P; i++)
+	    cout << int(del[i]) << "\t";
+	cout << endl;
+	
+	cout << "\tWeight Matrix : " << endl << "\t";
+	//for(i=0; i < P; i++)
+		//cout << int(i+1) << "\t";
+	cout << endl;
+
+	for(i=0;i < P; i++) {
+		cout << "\t\t\t";
+		for(j=0; j < P; j++) {
+			if(i==j)
+				cout << "0,0" << "\t";
+			else if(i < j)
+				cout << (w[index(i, j, P)] & (~a32[15]) ) << "," << bool((w[index(i, j, P)] & (a32[15]) )) << "\t";
+			else
+				cout << ( -short(w[index(i, j, P)] & (~a32[15]) ) ) << "," << bool((w[index(i, j, P)] & (a32[15]) )) << "\t";
+		}
+		cout << endl;
+	}
+	    
+	
+	cout << endl << endl;
+	
+	cout << "\tPush done at L : " << ( (f & 128)? 1 : 0 ) << endl;
+}
+
+
+// if this state is a final state
+bool stateZone::isFinal(){
+    char L = f & 127 ; // ignore the leftmost bit
+
+    if(L != 1) // there should not be any hanging point
+        return false;
+        
+    // transition at first point must be 0-th transition
+	if( del[0] != 0)
+		return false;
+		
+	// there will not any push at the last transition
+	if( isPush( del[P-1] ) ) 
+		return false;
+		
+	// target state of the transiton at point R should be the final state
+	if( transitions[del[P-1]].target != SF ) 
+		return false;
+		
+	return true;
+}
+
+
+/*
+// return the partial run corresponding the tree automata state 'vs', ignore the hanging points
+// copy only transitions between L(left) and R(right)
+runCGPP* getRun(stateGCPP* vs) {
+
+	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
+	
+	// allocate memory for transitions and tsm vlaues for new run
+	pr->del = 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
+	char i = vs->L - 1, j=0;
+	
+	// copy transitions and tsm values from earlier partial run to new partial run
+	for(; i < (vs->P); i++, j++) {
+		pr->del[j] = vs->del[i];
+		pr->w[j] = vs->w[i];
+	}
+	
+	return pr; // return the new run
+}
+
+
+// GIVEN the current partial run, append the transition 'dn' with tsm value 'wn'
+runCGPP* runCGPP::addNext(char dn, char wn) {
+
+	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
+
+	// allocate memory for transitions and tsm vlaues for new run
+	pr->del = new char[pr->P]; 
+	pr->w = new char[pr->P];
+	
+	// copy transitions and tsm values from earlier partial run to new partial run
+	for(char i=0; i < P; i++) {
+		pr->del[i] = del[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->w[P] = wn;
+	
+	return pr; // return the new run
+}
+
+
+// shuffle two partial runs and return the new partial run
+runCGPP* runCGPP::shuffle(runCGPP *s2) {
+
+	runCGPP *pr = new runCGPP(); // new partial run stored in variable pr
+	
+	// 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//
+	pr->P =  P + (s2->P) - 1; 
+	
+	// allocate memory for transitions and tsm vlaues for new run
+	pr->del = new char[pr->P]; 
+	pr->w = new char[pr->P];
+	
+	char i, j; // loopers
+	
+	// copy the transitions and tsm values of first run except for the last position
+	for(i=0, j=0; i < (P-1); i++, j++) {
+		pr->w[j] = w[i];
+		pr->del[j] = del[i];
+	}
+	
+	// copy the transitions and tsm values of 2nd run
+	for(i=0; i < (s2->P); i++, j++) {
+		pr->w[j] = s2->w[i];
+		pr->del[j] = s2->del[i];
+	}
+	
+	return pr; // return the new run
+}
+
+*/
+
+// this will return a state with only 0-th transition with tsm value 0
+stateZone* getZeroStateZone() {
+
+	stateZone* vs = new stateZone();
+	
+	vs->P = 1;
+	vs->f = 1; // no push pop info yet and L = 1
+	
+	vs->del = new char[1]; // memory allocation
+	vs->w = NULL;
+	
+	vs->del[0] = 0; // 0th transition has tsm value 0
+	
+	return vs;
+}
+
+
+// return unique string for last reset points of current state participating in a combine operation as a left state
+string stateZone::getKeyLeft() {
+
+	string s = ""; // return this string
+	
+	short resetSoFar, reset; // used for calculating union of resets
+	
+	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
+		
+		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
+string stateZone::getKeyRight() {
+
+	string s = ""; // return this string as a key for current state
+	
+	// take the transition at point L and all hanging points
+	
+	//char nf = 0; // this contains distance information between points distance information not needed
+	
+	s+= del[(f&127)-1]; // L-th poiint transition
+	//s+= w[L-1]; // L-th point tsm dont need 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
+	
+	for(; i >= 0; i--, j++) {
+		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];
+	}
+	
+	// add distance info in the key
+	//s+= nf;
+	
+	return s;
+}
+
+/*
+// print a run as witness of the given TPDA if the language is non-empty
+void runCGPP::print() {
+	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;
+	
+	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;
+}
+*/
+
+// return a backtracking state with the info given in the parameters
+trackZone* getTrackZone(char t, int l, int r) {
+	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
+                        // 1 if its add operation
+                         //2 if its generated by shuffle
+	xrs->left = l;  // if no left parameter then -1
+	xrs->right = r; // if no right parameter then -1
+	return xrs;
+}
+
+/*
+// 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 != "", then sm string is the key for shuffle operation of the state reside in i-th index of allStates
+runCGPP* printRun(int i) {
+
+	stateGCPP* vs; // tree automata state variable
+	trackCGPP *bp; // back tracking state
+	
+	vs = allStates[i].first;
+	bp = allStates[i].second;
+	
+	runCGPP *rs, *rs1, *rs2;
+		
+	// if the i-th state is an atomic state
+	if( (bp->type) == 0 ) {
+		cout << endl << i << ":";
+		vs->print();
+		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
+	else if( (bp->type) == 1 ) {
+		rs1 = printRun( bp->left );
+		rs = rs1->addNext(vs->del[vs->P - 1], vs->w[vs->P - 1]);
+		
+		cout << endl << i << " : " << (bp->left);
+		vs->print();
+		
+		return rs;
+	}
+	
+	else{
+		rs1 = printRun( bp->left);
+		rs2 = printRun(bp->right);
+		rs = rs1->shuffle(rs2);
+		
+		cout << endl << i << " : " << (bp->left) << ", " << (bp->right);
+		vs->print();
+	
+		return rs;
+	}
+}
+*/
+
+
+// return true iff language recognized by the TPDA is empty
+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)
+	if(SI == SF) {
+		cout << "Initial state is same as final state " << endl;
+		return false;
+	}
+	
+	int i,j; // counters
+        bool pushl, pushr, popl, popr, ppDone;
+	// allocate memory for two weight matrix and their corresponding open vars used shortest path operations
+	// 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
+	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
+	open2 = new bool*[K+2];
+	
+	for(i=0; i < (K+2); i++) { // allocate memory for inner 1d arrays
+		WT1[i] = new short[K+2];
+		WT2[i] = new short[K+2];
+
+		open1[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 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
+	
+	stateZone *rs, *vs, *vs1, *vs2; // some state variables required for track 
+	
+	trackZone *xrs; // back propagarion state variable
+	
+	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 dn; // var for upcoming transition might be added to the right of a state
+	char f; // flag variable
+
+	//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 
+	identity(vs); // insert this state in the hashmap
+	
+	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
+	N++; // increment #states
+	
+	//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;
+		
+
+	del = rs->del;
+	P = rs->P;
+	f = rs->f;
+	L = f & 127;
+        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) ; // if push at L and pop at R is done in rs
+	// iterate through all the generated states and process them to generate new state
+        
+        if(L < P && pushr)
+        {
+                
+        }
+        else if (L < P && pushl && ppDone)
+        {
+            
+        }
+        else
+        {
+
+		char q = transitions[ del[P-1] ].target; // target state of last transition
+	
+		// iterate through all the upcoming transitions
+                //this is only add operations we have to find way to suffle and 
+                
+		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
+
+			if(vs != NULL) { // if new state is valid
+				//vs->print();
+				if( identity(vs) ) {
+					xrs = getTrackZone(1, count, -1); // key for the new state
+					allStatesZone.push_back( make_pair(vs, xrs) );
+					N++;
+					if( vs->isFinal() ) {
+						vs->print();
+						//prs = printRun(N-1);
+						//prs->print();
+						return false;
+					}
+					
+				}
+			}
+		}
+        }
+		
+	}
+
+//	vs = allStatesZone[0].first; 
+	//N = 0'
+//mapZone.clear();
+//}
+/*
+	vs = allStatesZone[0].first;
+	rs = vs->addNextTPDA(1);
+	rs->print();
+
+	vs = rs->addNextTPDA(2);
+	vs->print();
+
+	rs= vs->addNextTPDA(3);
+	rs->print();
+	
+	rs->f = 3;
+	rs->print();
+
+	vs = rs->addNextTPDA(4);
+	vs->print();
+
+	rs = vs->addNextTPDA(5);
+	rs->print();
+
+	vs = rs->addNextTPDA(6);
+	rs = vs->addNextTPDA(7);
+	vs = rs->addNextTPDA(8);
+	rs = vs->addNextTPDA(9);
+
+	rs->print();
+*/	
+	return true;
+}
+
+
+
+

src/treeBitOperations.cpp

+#include<sstream>
+#include<string>
+#include<iostream>
+#include"treeBitOperations.h"
+
+unsigned  int a32[32]; /* a[i] contains an integer where only one '1' is there in the bit position (i-1)
+For example, a[3] contains binary number 00..01000 or integer 8
+*/
+
+unsigned  int b32[32]; /*b[i] contains an integer where all bits are '1' from zeroth bit position upto i-th bit position
+For example, b[4] contains binary number 00..01111 or integer 15
+*/
+
+unsigned  int c32[32]; /*c[i] contains an integer where all bits are '1' from (i+1)-th bit position upto  last bit position
+For example, c[4] contains binary number 11..10000 or integer -16
+*/
+
+unsigned  int d32[32]; /* d32[i] contains an integer where only one '0' is there in the bit position i
+For example, a[3] contains binary number 11..10111 or integer 8
+*/
+
+char K; // this denote number of maximum active colors
+
+
+// number of 1's in a integer represented in binary
+int noofones(unsigned   int x, int B) {
+  unsigned   int y = 1;
+  int i,count=0;
+  for(i=0; i < B; i++) {
+    if( (y & x) != 0)
+      count++;
+    y = y << 1;
+  }
+  return count;
+}
+
+
+
+// unsigned integer to binary conversion and print(for testing purpose)
+string inttobinary(int x) {
+	unsigned  int y=1;
+	y = y << 31;
+	int i;
+	stringstream ss;
+	for(i=0;i<32;i++){
+		if((y&x) == 0)
+			ss << 0;
+		else
+			ss << 1;
+		y = y >> 1;
+		if((i%4) == 3)
+			ss << " ";
+	}
+	return ss.str();
+}
+
+
+// initialization of the integer arrays a,b and c defined above
+void setBits() {
+	char i;
+	
+	unsigned  int x32=1,y32=1;
+	
+	for(i=0;i<32;i++) { // we are ignoring a[0],b[0] and c[0]
+		a32[i] = x32;
+		d32[i] = ~x32;
+		b32[i] = y32;
+		c32[i] = ~y32;
+		x32 = x32 << 1; // x = 2 * x or left shift the '1' in x one position left
+		y32 = x32 | y32; // If old y = 0011 and x = 0100, then new y = 0011 | 0100 = 0111
+	}
+	
+	/*
+	for(i=0;i<32;i++) {
+		cout << inttobinary(a32[i]) << endl;
+		cout << inttobinary(b32[i]) << endl;
+		cout << inttobinary(c32[i]) << endl;
+		cout << inttobinary(d32[i]) << endl;
+		cout << endl;
+	}
+	cout << endl << endl;
+	
+	*/
+	
+}
+
+