Skip to content

M
mtp
Commit 380b617a authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY
Browse files
Options

16/10/17: 

1. Bugs Resolved
2. Logical Bug Exists
3. tp63 is one good example.
I can do it.
parent 7639d7a8
Hide whitespace changes
Inline Side-by-side
Showing with 798 additions and 55 deletions
drawsystem
View file @ 380b617a
No preview for this file type
include/tpdaCGPP.h
View file @ 380b617a
......@@ -44,10 +44,10 @@ class stateGCPP{
stateGCPP* reduce(char dn);
// return true iff clock gurards on new transition 'dn' with tsm value 'wn' is satisfied
bool consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char wn, short *clockDis, bool *clockAcc);
bool consSatisfied(stateGCPP* vs,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(stateGCPP* vs,short* transitionMap,char dn, char wn, short dlr, bool aclr);
bool stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr);
//check if the relation between the fractional parts are good or not.
bool relationSatisfied(char dn,char wn,relation r,short *clockDis,bool *clockAcc);
// reduce the #points after shuffle operation by using forget operation if possible
......@@ -65,7 +65,7 @@ class stateGCPP{
bool isFinal(); // return true iff this state is final
void print(); // print this state
char reset_point(char t, char x);//returns the nearest reset point in the state of the clock x checked in transition t.
// return unique string for last reset points of a state participating in a combine operation as a left state
string getKeyLeft();
......
input1/.directory 0 → 100644
View file @ 380b617a
[Dolphin]
Timestamp=2017,10,16,13,56,6
Version=4
[Settings]
HiddenFilesShown=true
input1/pd1 0 → 100755
View file @ 380b617a
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 0 1 0 2
4 5 0 0 0
2 2 1 0 -1 0
5 6 0 0 0
0
6 7 0 0 0
1 1
7 8 0 0 0
2 1 1 0 -1 0
0 0 0
0 0 0
input1/rep1 0 → 100755
View file @ 380b617a
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 0 2 0
2
0
4 2 0 1 0
2 1 0 1 0
1 1
4 1 0 0 1
2
2 1 0 0 -1 0
input1/rep2 0 → 100755
View file @ 380b617a
4 11 2 9 1
1
4
1 2 1 0 0
0
2 3 2 1 1
1 1 0 2 0
2
0
3 4 3 1 0
2 0 0 1 0
1 1
4 2 4 1 0
1 1 0 2 0
0
2 4 5 1 2
2 1 0 2 0
1 2
0
4 3 6 0 1
1
0
3 2 7 0 0
2 1 2 0 2 0
2 1 8 0 0
0
1 4 9 2 0
1 0 0 2 0
2 1 0 1 0
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
input1/sample 0 → 100755
View file @ 380b617a
4 4 2 0 2
1
4
1 2 0 1 1
2 2 0 3 0
1
1 1
1 4 0 0 0
2 2 2 0 2 0
2 3 0 2 0
1 0 0 2 0
2 1 0 2 0
3 1 0 0 2 0 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 5 space separated intergers : <clock_number> <lower_bound> <open/close> <upper_bound> <open/close>
clock_number : clock(x) for which there is a check in this transition
lower bound : x >= lower_bound is the lower bound constraint
open/close: 0 if the bound is close and 1 if the bound is open
upper bound : x <= upper_bound is the upper bound constraint
open/close: 0 if the bound is closed and 1 if the bound is open
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 7 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 five space separated integers : <stack_symbol> <lower_bound> <open/close> <upper_bound> <open/close>
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
<open/close>: openness and closed ness of the bound
<upper_bound> : lower bound on the age of the stack symbol currently popped in this transition
<open/close>: openness and close ness of the bound.
<stack_symbol_2> : stack symbol number pushed in this transition
input1/t1 0 → 100755
View file @ 380b617a
6 5 2 3 0
1
6
1 2 1 1 1
2 5 0 -1 0
2
0
2 3 0 1 0
1 0 0 4 0
0
5 4 1 1 0
1 0 0 4 0
0
1 5 0 1 1
1 2 0 -1 0
2
0
4 3 0 1 0
2 5 0 -1 0
0
// edit the ages for checking emptiness
input1/t10 0 → 100755
View file @ 380b617a
6 8 3 3 0
1
5
1 2 0 1 0
1 4 0 -1 0
0
1 3 1 1 1
3 1 0 1 0
2
0
2 6 0 2 0
1 1 0 6 0
2 0 0 1 0
0
3 4 1 0 2
3 1
0
3 5 0 1 0
1 0 0 0 0
0
4 5 2 2 0
1 1 0 1 0
2 0 0 0 0
0
6 3 3 1 0
1 1 0 1 0
0
6 5 0 2 0
1 0 0 1 0
2 1 0 -1 0
0
00 00
input1/t11 0 → 100755
View file @ 380b617a
7 8 4 3 0
1
7
1 2 0 1 1
2 5 0 -1 0
1
0
1 3 1 1 2
3 3 0 -1 0
2 3
0
2 3 0 1 1
1 2 0 2 0
2
0
3 4 1 2 1
3 0 0 5 0
2 0 0 2 0
3
0
4 5 0 1 1
4 3 0 3 0
4
0
4 6 2 1 2
3 0 0 1 0
3 4
0
5 6 3 2 1
1 2 0 2 0
2 2 0 2 0
4
0
6 3 0 1 1
4 1 0 1 0
1
0
00 00
input1/t13 0 → 100755
View file @ 380b617a
6 7 3 3 0
1
3
1 4 0 2 2
1 1 0 3 0
2 2 0 2 0
1 2
0
1 2 1 1 1
3 3 0 -1 0
2
0
2 3 2 1 1
1 1 0 2 0
3
0
2 5 3 1 1
2 1 0 3 0
3
0
4 3 2 1 1
3 0 0 0 0
1
0
5 6 1 2 0
1 1 0 1 0
3 2 0 2 0
0
6 1 0 1 1
3 1 0 3 0
2
0
00 00
input1/t8 0 → 100755
View file @ 380b617a
4 6 2 4 0
4
3
4 1 1 1 1
1 0 0 -1 0
2
0
1 2 2 1 0
2 1 0 1 0
0
1 3 1 2 0
1 0 0 0 0
2 1 0 -1 0
0
2 3 3 1 0
1 0 0 0 0
0
3 3 4 1 0
1 2 0 -1 0
0
3 1 1 1 1
2 0 0 0 0
2
0
http://computerscience.unicam.it/tesei/pubdownload/T04Phd.pdf
fig 2.5
input1/timeconsuming/tp2_0 0 → 100755
View file @ 380b617a
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 0 18 0
0
8 9 0 0 1
1
0
9 10 0 0 0
2 1 0 0 9 0
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 )
input1/timeconsuming/tp3_0 0 → 100755
View file @ 380b617a
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 0 12 0
0
8 9 0 0 1
3
0
9 10 0 0 0
2 1 0 0 6 0
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)
input1/tp38 0 → 100755
View file @ 380b617a
4 4 1 2 1
4
1
1 2 1 1 0
1 1 0 1 0
0
2 3 2 0 1
1
2 1 1 0 -1 0
3 4 0 1 0
1 0 0 0 0
0
4 1 0 0 1
1
1 1
00 00
|X| = 1
|T| = 4
|M| = 1
input1/tp6 0 → 100755
View file @ 380b617a
6 8 2 3 2
1
5
1 2 0 1 0
1 1 0 -1 0
1 1
1 3 1 1 1
1 1 0 1 0
2
0
2 6 0 2 0
1 1 0 1 0
2 0 0 3 0
0
3 4 1 0 2
2 1
0
3 5 0 1 0
1 0 0 0 0
0
4 5 2 2 0
1 1 0 1 0
2 0 0 0 0
0
6 3 3 1 0
1 1 0 1 0
0
6 5 0 2 0
1 0 0 1 0
2 1 0 -1 0
2 1 1 0 1 0
00 00
input1/tp60 0 → 100755
View file @ 380b617a
5 6 1 0 1
1
4
1 2 0 1 0
1 0 0 0 0
0
2 3 0 0 0
1 1
3 4 0 0 0
0
4 1 0 1 1
1 0 0 2 0
1
2 1 0 0 -1 0
3 5 0 0 1
1
0
5 4 0 1 0
1 0 0 0 0
2 1 0 0 0 0
00 00
|X| = 1
|T| = 3
|M| = 5
input1/tp62 0 → 100755
View file @ 380b617a
5 6 1 0 1
1
5
1 2 0 0 1
1
1 1
1 3 0 1 0
1 3 0 -1 0
0
2 3 0 1 0
1 1 0 -1 0
0
3 4 0 1 0
1 3 0 100 0
0
3 5 0 1 0
1 0 0 2 0
0
4 5 0 0 0
2 1 2 0 3 0
00 00
|X| = 1
|T| = 2
|M| = 9
input1/tp63 0 → 100755
View file @ 380b617a
5 8 1 2 2
1
5
1 2 0 0 0
1 2
1 5 0 1 0
1 1 0 2 0
2 2 6 0 8 0
2 1 0 0 0
0
2 2 0 1 1
1 1 0 1 0
1
1 1
2 3 0 1 0
1 0 0 1 1
0
3 4 0 0 0
0
4 2 0 1 0
1 0 0 2 0
0
4 4 0 0 0
2 1 1 0 2 0
makefile
View file @ 380b617a
CC := g++
CFLAG := -lm -std=c++14
CFLAG := -lm -fopenmp -std=c++14
SRC := ./src
OBJ := ./obj
INC := ./include
......
nbproject/private/configurations.xml
View file @ 380b617a
......@@ -19,6 +19,10 @@
</df>
<df name="input">
</df>
<df name="input1">
<df name="timeconsuming">
</df>
</df>
<df name="obj">
</df>
<df name="output">
......
src/circuitfinder.cpp
View file @ 380b617a
......@@ -56,11 +56,11 @@ bool2 CircuitFinder::circuit(int V)
bool CircuitFinder::cycleCheck() //here we need to check if there exists any cycle
{ // with <+<=* regex. return 1 if there is a cycle and return 0 if not.
cout << "circuit: ";
//cout << "circuit: ";
int countles=0;
for (auto I = Stack.begin(), E = Stack.end(); I != E; ++I) {
//checking of if the cycle have a < along with other <=
cout << *I << " -> ";
//cout << *I << " -> ";
if(I+1 != E)
{
......@@ -90,7 +90,7 @@ bool CircuitFinder::cycleCheck() //here we need to check if there exists any cyc
return false;
}
cout << *Stack.begin() << std::endl;
//cout << *Stack.begin() << std::endl;
}
......
src/timePushDown.cpp
View file @ 380b617a
......@@ -24,8 +24,8 @@ 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
char **recent_matrix;
char* clock_reset;
//char **recent_matrix;
//char* clock_reset;
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
......@@ -136,22 +136,22 @@ void inputSystem() {
tiimeinfile >> x; // #clocks
X = x;
clock_reset = new char[X];
for(int i = 0; i < X; i++)
{
clock_reset[i] = 0; // the first reset points of every clocks is 0th transition.
}
recent_matrix = new char*[T+1]; //allocate rows to the matrix which is the total number of transitions.
for(int i = 0; i < T+1 ; i++)
{
recent_matrix[i] = new char[X]; //for every row we have columns with the number of clocks
}
for(int i = 0; i <X; i++)
{
recent_matrix[0][i] = clock_reset[i];
}
//
// clock_reset = new char[X];
// for(int i = 0; i < X; i++)
// {
// clock_reset[i] = 0; // the first reset points of every clocks is 0th transition.
// }
// recent_matrix = new char*[T+1]; //allocate rows to the matrix which is the total number of transitions.
// for(int i = 0; i < T+1 ; i++)
// {
// recent_matrix[i] = new char[X]; //for every row we have columns with the number of clocks
//
// }
// for(int i = 0; i <X; i++)
// {
// recent_matrix[0][i] = clock_reset[i];
// }
tiimeinfile >> x; // #actions
A = x;
......@@ -263,7 +263,7 @@ void inputSystem() {
exit(1);
}
reset |= a32[x]; // set x-th bit of 'reset' to '1'
clock_reset[x] = i; // the latest transition which resets the clocks x is i.
//clock_reset[x] = i; // the latest transition which resets the clocks x is i.
}
// read stack operation number, 0 : nop, 1 : push, 2 : pop, 3 : pop & push
......@@ -388,12 +388,12 @@ void inputSystem() {
if(reset & a32[j]) // if j-th clock has been reset at i-th transitions // forget this
resettrans[j].push_back(i);
}
for(int m = 0; m <X; m++)
{
recent_matrix[i][m] = clock_reset[m]; //Updating the matrix
}
// for(int m = 0; m <X; m++)
// {
// recent_matrix[i][m] = clock_reset[m]; //Updating the matrix
// }
}
delete clock_reset;
//delete clock_reset;
prevtrans.resize(S+1); // #rows = S+1 in the 2D vector prevtrans and nexttrans // forget this
nexttrans.resize(S+1); // forget this
......
src/tpdaCGPP.cpp
View file @ 380b617a
......@@ -18,7 +18,14 @@ unordered_map<string,bool> mapGCPP;
// this vector contains all the states generated for a TPDA paried with tracking states
vector<pair<stateGCPP*, trackCGPP*> > allStates;
void print_r_matrix(relation** r_matrix,char p)
{
for(char i = 0; i < p; i++){
for(char j =0; j < p; j++)
cout << r_matrix[i][j] << '\t' ;
cout << endl;
}
}
// return 1 iff state vs was not found earlier or vs is new state
bool identity(stateGCPP *vs) {
......@@ -152,8 +159,8 @@ stateGCPP* stateGCPP::reduceShuffle(stateGCPP* s2) {
vs->w[L-1] = w[L-1];
for(int i = 0 ; i < L ;i++)
{
vs->r_matrix[vs->P-1][i] = r_matrix[P][i];
vs->r_matrix[i][vs->P] = r_matrix[i][P];
vs->r_matrix[vs->P-1][i] = r_matrix[P-1][i];
vs->r_matrix[i][vs->P-1] = r_matrix[i][P-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
......@@ -270,7 +277,7 @@ stateGCPP* stateGCPP::reduce(char dn){
short curReset = transitions[dn].reset; // set of clocks reset at transition 'dn'
for( i=P-1; i >= L; i-- ) {
for( char 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'
......@@ -293,7 +300,7 @@ stateGCPP* stateGCPP::reduce(char dn){
vs->allocate_r_matrix(que); //allocating memory for the matrix for open guard checking
//*************ASSIGNING VALUES TO THE DYNAMICALLY ALLOCATED VARIABLES*****************//
for(i=0; i < L; i++) { // hanging points and left point(L) remain same
for(char i=0; i < L; i++) { // hanging points and left point(L) remain same
vs->del[i] = del[i];
vs->w[i] = w[i];
map[i] = i; //copying the map upto L-1
......@@ -301,7 +308,7 @@ stateGCPP* stateGCPP::reduce(char dn){
// vs->r_matrix[i][j] = r_matrix[i][j]; // copying the matrix value for the hanging points
}
for(i=1; i < L; i++) { // distances between points upto point L remain same
for(char i=1; i < L; i++) { // distances between points upto point L remain same
nf |= ( f & a32[i] );
}
......@@ -313,14 +320,14 @@ stateGCPP* stateGCPP::reduce(char dn){
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'
int vslastindex = vs->P -1; //the last index of the new state vs;
for(i=P-1; i >= L; i--) {
//int vslastindex = vs->P -1; //the last index of the new state vs;
for(char 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
map[vslastindex]=i;
map[j]=i;
if( lastindex != P ) {
if( !big(i+1, lastindex+1) )
nf |= a32[j+1]; // set the accuracy for (j+1)-th bit of new state
......@@ -338,12 +345,12 @@ stateGCPP* stateGCPP::reduce(char dn){
lastindex = i; // this is now the last index
j--; // go to previous point
vslastindex--;
//vslastindex--;
}
}
for(int i = 0; i < vs->P-1; i++)// this code may change, later.
for(char i = 0; i < vs->P-1; i++)// this code may change, later.
{
for(int j = 0 ; j< vs->P-1; j++)
for(char j = 0 ; j< vs->P-1; j++)
{
vs->r_matrix[i][j]=r_matrix[map[i]][map[j]]; //copying r_matrix values
}
......@@ -378,7 +385,7 @@ stateGCPP* stateGCPP::reduce(char dn){
// return true if constraint on new transition dn with tsm wn is satisfied while adding current transiton 'dn' to the right
bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char wn, short *clockDis, bool *clockAcc) {
bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, bool *clockAcc) {
short dis,dis_l=1;
int openl,openu;
openl = transitions[dn].openl;
......@@ -394,6 +401,7 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
//cout << store_matrix[i][j] << endl;
}
}
#pragma openmp parallel for
for(char x=1; x <= X; x++) {
if( isChecked(x, dn) ) { // if there is a check for clock x
......@@ -401,9 +409,9 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
dis = clockDis[x] + mod( wn - w[P-1], M ) ;
if( (vs->P) > 1 && ( (vs->f) & a32[vs->P - 1] ) ) {
/*********************#***************/
dis_l = vs->w[vs->P - 2] + mod(wn - w[P-1], M); //distance with the last point
dis_l = vs->w[vs->P - 1] + mod(wn - w[P-1], M); //distance with the last point
}
char t = transitionMap[recent_matrix[dn][x-1]]; //?
char t = vs->reset_point(dn,x); //?
if( dis < (transitions[dn].lbs[x] ) || dis > (transitions[dn].ubs[x] ) )
{//if the distance doesnot belong to the interval
delete_r_matrix(store_matrix,vs->P); // this one added extra
......@@ -443,7 +451,12 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
{
store_matrix[vs->P-2][vs->P-1] = leq;
}
cout << dn << endl;
cout << endl;
cout << endl;
print_r_matrix(store_matrix,vs->P);
pairWiseTightestRelation(store_matrix,vs->P);
print_r_matrix(store_matrix,vs->P);
CircuitFinder cf(store_matrix,vs->P);
bool b = cf.run();
if(b)
......@@ -458,6 +471,7 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
}
}
}
#pragma openmp parallel for
for(int i = 0 ;i < vs->P; i++)
{
for(int j = 0; j < vs->P; j++)
......@@ -465,7 +479,7 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
vs->r_matrix[i][j]=store_matrix[i][j]; //restoring computed values to the matrix
}
}
delete_r_matrix(store_matrix,P); //this one added extra
delete_r_matrix(store_matrix,vs->P); //this one added extra
return true;
}
......@@ -488,12 +502,13 @@ bool stateGCPP::consSatisfied(stateGCPP* vs, short* transitionMap,char dn, char
// 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(stateGCPP* vs,short* transitionMap,char dn, char wn, short dlr, bool aclr) {
bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr) {
int ub = transitions[dn].ubs[0];// the stacks upper bound
int openl,openu; //added extra
openl = transitions[dn].openl;
openu = transitions[dn].openu;
relation **store_matrix = allocate_r_matrix(vs->P);
#pragma openmp parallel for
for(int i = 0 ;i < vs->P; i++)
{
for(int j = 0; j < vs->P; j++)
......@@ -549,6 +564,7 @@ bool stateGCPP::stackCheck(stateGCPP* vs,short* transitionMap,char dn, char wn,
return false;
else
{
#pragma openmp parallel for
for(int i = 0 ;i < vs->P; i++)
{
for(int j = 0; j < vs->P; j++)
......@@ -595,6 +611,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
char q = transitions[ del[P-1] ].target; // target state of last transition
// iterate through all the upcoming transitions
#pragma openmp parallel for
for(i=0; i < nexttrans[q].size(); i++) {
dn = nexttrans[q][i]; // i-th upcoming transition
......@@ -617,9 +634,8 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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]
short *transitionMap = new short[T+1]{-1}; //for a given state and a given transition, which colored point the transition maps into is given by this vector
for(int q = 0 ; q < vs->P; q++)
transitionMap[vs->del[q]] = q; //this gives transitions to clolore point ka map.
for(char x=1; x <= X; x++) { // calculate the distances and accuracy from last reset point to point P for each clock
for(j=P-1; j >= 0; j--) {
......@@ -639,14 +655,15 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
// iterate through all possible TSM value for tranistion 'dn' and check for constraints on clocks and stack
//relation rel[2] = {leq,les};
#pragma openmp parallel for
for(wn=0; wn < M; wn++) {
//is it checking after adding the point to the state returned by reduce?
// if clock constraint not satisfied
if( !consSatisfied( vs,transitionMap,dn, wn, clockDis, clockAcc) ) { }
if( !consSatisfied( vs,dn, wn, clockDis, clockAcc) ) { }
// if stack constraint not satisfied
else if( ( popflag && ( !stackCheck(vs,transitionMap,dn, wn, dlr, aclr) ) ) ) { } //if there is a pop and the constraint on pop is satisfied.
else if( ( popflag && ( !stackCheck(vs,dn, wn, dlr, aclr) ) ) ) { } //if there is a pop and the constraint on pop is satisfied.
//else if(!relationSatisfied(dn,wn))
//else if (( !openGuardConsSat()))
else { // if clock and stack both constraints are satisfied
......@@ -669,7 +686,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
// calculate distance from 2nd last point to last point in new state
/*******************#*****************/
dis = vs->w[vs->P - 2] + mod(wn - w[P-1], M); ///put the change ****
dis = vs->w[vs->P - 1] + mod(wn - w[P-1], M); ///put the change ****
/*******************************************/
if(dis < M) { // reset vs->P-1 bit to 1
rs->f |= (a32[vs->P - 1]);
......@@ -693,7 +710,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
}
//removing after finishing with it
}
delete[] clockDis,clockAcc,transitionMap;
delete[] clockDis,clockAcc;
}
}
......@@ -757,6 +774,7 @@ stateGCPP* stateGCPP::sucState(){
vs->f = nf; // copy flag information, no stack info is there till now for the template state
//we also have to copy the value of the relation matrix for those points.
for(int i = 0; i < count ;i ++)
{
for(int j =0; j < count ; j++)
......@@ -1375,3 +1393,24 @@ void pairWiseTightestRelation (relation **graph,int V) //this function does the
delete[] dist[i];
delete[] dist;
}
char stateGCPP::reset_point(char t, char x)
{
if(!isChecked(x,t))
{
cout <<"The clock " << x << " is not checked in the transition " << t << endl;
exit(0);
}
else
{
for(int i = P-1; i >=0; i --)
{
if(isReset(x,del[i]))
{
return i;
}
}
}
return -1;
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment