Skip to content

M
mtp
Commit 0d7183c1 authored by SPARSA ROYCHOWDHURY's avatar SPARSA ROYCHOWDHURY
Browse files
Options

25/9/17: 

1. Output drawing system modified according to the process.
parent 781e10c7
Hide whitespace changes
Inline Side-by-side
Showing with 173 additions and 30 deletions
drawsystem
View file @ 0d7183c1
No preview for this file type
include/drawsystem.h
View file @ 0d7183c1
...@@ -17,8 +17,9 @@ class transition{ ...@@ -17,8 +17,9 @@ class transition{
int guard; // Let i-th bit of guard from right hand is g_i int guard; // Let i-th bit of guard from right hand is g_i
int reset; // Let i-th bit of reset from right hand is r_i int reset; // Let i-th bit of reset from right hand is r_i
/* int openl; // i-th bit openl is 1 iff lower bound of constraint for clock i is open
0-th bit of gurad and reset is for stack operation 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) 1 to 15-th bits are for clock(15 clock supported)
g_i=1(1<=i<=15) : i-th clock is checked in this transition g_i=1(1<=i<=15) : i-th clock is checked in this transition
......
input/sample
View file @ 0d7183c1
...@@ -5,17 +5,17 @@ ...@@ -5,17 +5,17 @@
4 4
1 2 0 1 1 1 2 0 1 1
2 2 3 2 2 0 3 0
1 1
1 1 1 1
1 4 0 0 0 1 4 0 0 0
2 2 2 2 2 2 2 0 2 0
2 3 0 2 0 2 3 0 2 0
1 0 2 1 0 0 2 0
2 1 2 2 1 0 2 0
3 1 0 2 2 3 1 0 0 2 0 2
3 1 0 0 2 3 1 0 0 2
1 2 1 2
...@@ -59,23 +59,27 @@ INPUT FORMAT(Ignore blank lines and spaces) : ...@@ -59,23 +59,27 @@ INPUT FORMAT(Ignore blank lines and spaces) :
action : 0(action is not important for us, just put 0 in place of action) action : 0(action is not important for us, just put 0 in place of action)
#guards : number of clock checks are there #guards : number of clock checks are there
#resets : number of clock reset at this transition #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> 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 clock_number : clock(x) for which there is a check in this transition
lower bound : x >= lower_bound is the lower bound constraint 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 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 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 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> Last line of the input can contain maximum 7 space separated integers : <stack_op>
The value of first integer determine the stack operation The value of first integer determine the stack operation
First interger is 0 : no 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 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 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> 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 where
<stack_symbol> : stack symbol number popped in this transition <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 <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 <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 <stack_symbol_2> : stack symbol number pushed in this transition
src/drawsystem.cpp
View file @ 0d7183c1
...@@ -35,7 +35,7 @@ inline bool transition::isReset(char i) { ...@@ -35,7 +35,7 @@ inline bool transition::isReset(char i) {
void showsystem(char *outfile) { void showsystem(char *outfile) {
int source,ns; int source,ns;
int i,j,k; int i,j,k;
int guard,reset; int guard,reset,openu,openl;
int action, ub, lb, ps, pp; int action, ub, lb, ps, pp;
ofstream tiimeoutfile(outfile); // timed automata output file for showing the automata ofstream tiimeoutfile(outfile); // timed automata output file for showing the automata
...@@ -58,7 +58,8 @@ void showsystem(char *outfile) { ...@@ -58,7 +58,8 @@ void showsystem(char *outfile) {
guard = transitions[i].guard; guard = transitions[i].guard;
reset = transitions[i].reset; reset = transitions[i].reset;
openl = transitions[i].openl;
openu = transitions[i].openu;
action = transitions[i].a; action = transitions[i].a;
for(j=1; j <= X; j++) { // save all the conjunction of a constraint for(j=1; j <= X; j++) { // save all the conjunction of a constraint
...@@ -68,10 +69,40 @@ void showsystem(char *outfile) { ...@@ -68,10 +69,40 @@ void showsystem(char *outfile) {
ub = transitions[i].ubs[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**** //if (ub == 0 && lb == 0) {} //***this line will not be active other than maze, only else part will remain****
//else{ //else{
if(ub == INF) if(openl &a32[j])
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << "inf"; {
else if(openu &a32[j])
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub; {
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << ub;
}
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
}
}
else
{
if(openu &a32[j])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
}
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub;
}
}
//} //}
} }
} }
...@@ -101,20 +132,84 @@ void showsystem(char *outfile) { ...@@ -101,20 +132,84 @@ void showsystem(char *outfile) {
tiimeoutfile << ",pp_" << pp; tiimeoutfile << ",pp_" << pp;
lb = transitions[i].lbs[0]; lb = transitions[i].lbs[0];
ub = transitions[i].ubs[0]; ub = transitions[i].ubs[0];
if(ub == INF) openl = transitions[i].openl;
tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << "inf"; openu = transitions[i].openu;
else if(openl &a32[0])
tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << ub; {
if(openu &a32[0])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << ub;
}
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
}
}
else
{
if(openu &a32[0])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
}
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub;
}
}
} }
else if( (reset & 1) && (guard & 1) ) { // pop operation else if( (reset & 1) && (guard & 1) ) { // pop operation
tiimeoutfile << ",pp_" << pp; tiimeoutfile << ",pp_" << pp;
lb = transitions[i].lbs[0]; lb = transitions[i].lbs[0];
ub = transitions[i].ubs[0]; ub = transitions[i].ubs[0];
if(ub == INF) openl = transitions[i].openl;
tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << "inf"; openu = transitions[i].openu;
else if(openl &a32[0])
tiimeoutfile << ":" << lb << "<=ag(" << pp << ")<=" << ub; {
if(openu &a32[0])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<" << ub;
}
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
}
}
else
{
if(openu &a32[0])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
}
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<=" << ub;
}
}
tiimeoutfile << ",ps_" << ps; tiimeoutfile << ",ps_" << ps;
} }
tiimeoutfile << "}\" ];\n"; tiimeoutfile << "}\" ];\n";
...@@ -204,6 +299,9 @@ int main(int argc, char *argv[]) { ...@@ -204,6 +299,9 @@ int main(int argc, char *argv[]) {
transitions[i].ubs = new int[X+1]; // allocate memory for upper 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; guard = 0;
int opnl,opnu;
int openl=0;
int openu = 0;
for(j=0; j < noofguards; j++) { for(j=0; j < noofguards; j++) {
tiimeinfile >> x; // clock number for guard tiimeinfile >> x; // clock number for guard
...@@ -214,8 +312,20 @@ int main(int argc, char *argv[]) { ...@@ -214,8 +312,20 @@ int main(int argc, char *argv[]) {
} }
guard |= a32[x]; // set i-th bit of guard to '1' guard |= a32[x]; // set i-th bit of guard to '1'
tiimeinfile >> lb >> ub; // bounds on the guard tiimeinfile >> lb;
tiimeinfile >> opnl; // bounds on the guard
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
if(opnl == 1)
{
openl |= a32[x]; //if left value is open then the xth bit of the open is 1
}
if(opnu == 1)
openu |= a32[x]; // similar as above
if(lb < 0 || ub < (-1)) { if(lb < 0 || ub < (-1)) {
cout << "Bounds can't be negative!" << endl; cout << "Bounds can't be negative!" << endl;
exit(1); exit(1);
...@@ -264,9 +374,23 @@ int main(int argc, char *argv[]) { ...@@ -264,9 +374,23 @@ int main(int argc, char *argv[]) {
tiimeinfile >> x; // stack pop symbol tiimeinfile >> x; // stack pop symbol
transitions[i].pp = x; transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds tiimeinfile >> lb;
tiimeinfile >> opnl;
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
if(opnl == 1)
{
openl |= 1; //setting 0th bit of the openl to 1
}
if(opnu == 1)
openu |= 1; // similar as above
transitions[i].lbs[0] = lb; // lower bound for clock x transitions[i].lbs[0] = lb; // lower bound for clock x
if(ub == (-1)) // upper bound -1 means infinity if(ub == (-1)) // upper bound -1 means infinity
...@@ -283,8 +407,21 @@ int main(int argc, char *argv[]) { ...@@ -283,8 +407,21 @@ int main(int argc, char *argv[]) {
tiimeinfile >> x; // stack pop symbol tiimeinfile >> x; // stack pop symbol
transitions[i].pp = x; transitions[i].pp = x;
tiimeinfile >> lb >> ub; // read stack pop bounds tiimeinfile >> lb;
tiimeinfile >> opnl;
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
if(opnl == 1)
{
openl |= 1; //if left value is open then the xth bit of the open is 1
}
if(opnu == 1)
openu |= 1; // similar as above
transitions[i].lbs[0] = lb; // lower bound for clock x transitions[i].lbs[0] = lb; // lower bound for clock x
......
src/tpdaCGPP.cpp
View file @ 0d7183c1
...@@ -495,6 +495,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() { ...@@ -495,6 +495,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
//assume the relation of fraction part with respect to the new system. //assume the relation of fraction part with respect to the new system.
//first assume it to be \leq //first assume it to be \leq
rs->r_matrix = rs->allocate_r_matrix();// do we need to allocate? or it is sufficent to just point? rs->r_matrix = rs->allocate_r_matrix();// do we need to allocate? or it is sufficent to just point?
//I have to allocate because this is changing
//How to propagate values?? //How to propagate values??
//vs->r_matrix; //vs->r_matrix;
......
tree
View file @ 0d7183c1
No preview for this file type
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