Skip to content

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

17/10/17: 

1. Bugs Resolved
2. Logical Bug Exists
3. tp63 is one good example.
4. Drawsystem is up
5. Circuit is detecting but logical bug still persists.
parent 380b617a
Hide whitespace changes
Inline Side-by-side
Showing with 7843 additions and 55 deletions
dot/sample.out
View file @ aa910b64
......@@ -5,7 +5,7 @@ digraph finite_state_machine {
qi0 -> 0;
0 -> 1 [ label = "{tn:0,x1:=0,x2:=0}" ];
1 -> 2 [ label = "{tn:1,2<=x2<=3,x1:=0,ps_1}" ];
1 -> 4 [ label = "{tn:2,pp_2:2<=ag(2)<=2}" ];
2 -> 3 [ label = "{tn:3,0<=x1<=2,1<=x2<=2,pp_1:0<=ag(1)<=2,ps_2}" ];
1 -> 4 [ label = "{tn:2,pp_2,2<=x3<=2}" ];
2 -> 3 [ label = "{tn:3,0<=x1<=2,1<=x2<=2,pp_1,0<=x3<=2,ps_2}" ];
3 -> 1 [ label = "{tn:4,x1:=0,x2:=0}" ];
}
\ No newline at end of file
dot/tpg0.out
View file @ aa910b64
......@@ -4,10 +4,10 @@ digraph finite_state_machine {
node [shape=circle];
qi0 -> 0;
0 -> 1 [ label = "{tn:0,x1:=0,x2:=0}" ];
1 -> 2 [ label = "{tn:1,3<=x1<=11,x2:=0}" ];
2 -> 3 [ label = "{tn:2,2<=x2<=13,x2:=0}" ];
3 -> 4 [ label = "{tn:3,1<=x2<=15,ps_1}" ];
4 -> 5 [ label = "{tn:4,0<=x2<=10,x1:=0,ps_1}" ];
5 -> 6 [ label = "{tn:5,x1:=0,pp_1:2<=ag(1)<=6}" ];
6 -> 7 [ label = "{tn:6,0<=x2<=inf,x2:=0,pp_1:3<=ag(1)<=9}" ];
1 -> 2 [ label = "{tn:1,3<=x1<=2,x2:=0,pp_0,1<=x3<=2,ps_13}" ];
2 -> 0 [ label = "{tn:2,1<=x1<=5}" ];
0 -> 1 [ label = "{tn:3,1<=x1<=0,6<=x2<=7,x2:=0,pp_1,3<=x3<=0}" ];
1 -> 1 [ label = "{tn:4,3<=x1<=0,x1:=0,ps_1}" ];
1 -> 1 [ label = "{tn:5,3<=x1<=0,x1:=0,ps_1}" ];
1 -> 1 [ label = "{tn:6,3<=x1<=0,x1:=0,ps_1}" ];
}
\ No newline at end of file
drawsystem
View file @ aa910b64
No preview for this file type
images/sample.png
View replaced file @ 380b617a View file @ aa910b64
images/sample.png

41.9 KB | W: | H:

images/sample.png

35.2 KB | W: | H:

images/sample.png
images/sample.png
images/sample.png
images/sample.png
  • 2-up
  • Swipe
  • Onion skin
images/tpg0.png
View replaced file @ 380b617a View file @ aa910b64
images/tpg0.png

50.1 KB | W: | H:

images/tpg0.png

48.7 KB | W: | H:

images/tpg0.png
images/tpg0.png
images/tpg0.png
images/tpg0.png
  • 2-up
  • Swipe
  • Onion skin
include/circuitfinder.h
View file @ aa910b64
......@@ -19,6 +19,7 @@
#include <vector>
using namespace std;
typedef enum {z,les,leq,que} relation;
//extern relation comparison[4][4];
extern relation addition[4][4];
typedef list<int> NodeList;
......
input1/tp63.out 0 → 100644
View file @ aa910b64
digraph finite_state_machine {
node [shape = point ]; qi0;
node [shape = doublecircle];5;
node [shape=circle];
qi0 -> 0;
0 -> 1 [ label = "{tn:0,x1:=0}" ];
1 -> 2 [ label = "{tn:1,ps_2}" ];
1 -> 5 [ label = "{tn:2,1<=x1<=2,pp_2,6<=x2<=8}" ];
2 -> 1 [ label = "{tn:3}" ];
2 -> 2 [ label = "{tn:4,1<=x1<=1,x1:=0,ps_1}" ];
2 -> 3 [ label = "{tn:5,0<=x1<1}" ];
3 -> 4 [ label = "{tn:6}" ];
4 -> 2 [ label = "{tn:7,0<=x1<=2}" ];
4 -> 4 [ label = "{tn:8,pp_1,1<=x2<=2}" ];
}
\ No newline at end of file
output.txt 0 → 100644
View file @ aa910b64
This source diff could not be displayed because it is too large. You can view the blob instead.
src/circuitfinder.cpp
View file @ aa910b64
......@@ -4,6 +4,7 @@
* and open the template in the editor.
*/
#include "circuitfinder.h"
string sarr[4] = {"0","<","<=","?"};
void CircuitFinder::unblock(int U)
{
Blocked[U - 1] = false;
......@@ -58,16 +59,21 @@ bool CircuitFinder::cycleCheck() //here we need to check if there exists any cyc
{ // with <+<=* regex. return 1 if there is a cycle and return 0 if not.
//cout << "circuit: ";
int countles=0;
bool flag = true;
for (auto I = Stack.begin(), E = Stack.end(); I != E; ++I) {
//checking of if the cycle have a < along with other <=
//cout << *I << " -> ";
// if(I+1 != E)
// cout << *I << sarr[relmatrix[*I -1][*(I+1) -1]];
// else
// cout << *I << sarr[relmatrix[*I-1][*Stack.begin()-1]] ;
if(I+1 != E)
{
if(relmatrix[(*I)-1][(*(I+1))-1] != leq && relmatrix[(*I)-1][(*(I+1))-1] != les)
{
return false;
flag = false;
}
else if(relmatrix[(*I)-1][(*(I+1))-1] == les)
countles++;
......@@ -77,19 +83,24 @@ bool CircuitFinder::cycleCheck() //here we need to check if there exists any cyc
if(relmatrix[(*I)-1][(*Stack.begin())-1] != leq && relmatrix[(*I)-1][(*Stack.begin())-1] != les)
{
return false;
flag = false;
}
else if (relmatrix[(*I)-1][(*Stack.begin())-1] == les)
countles ++;
}
if( countles == 1)
}
//cout << *Stack.begin() << std::endl;
if( countles == 1 && flag == true)
{// if this true then the circuit is bad
cout << "Found a Circuit BANG!!" << endl;
return true;
}
else
return false;
}
//cout << *Stack.begin() << std::endl;
}
......
src/drawsystem.cpp
View file @ aa910b64
......@@ -81,9 +81,9 @@ void showsystem(char *outfile) {
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
}
}
else
......@@ -91,9 +91,9 @@ void showsystem(char *outfile) {
if(openu &a32[j])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
}
else
{
......@@ -146,9 +146,9 @@ void showsystem(char *outfile) {
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
}
}
else
......@@ -156,9 +156,9 @@ void showsystem(char *outfile) {
if(openu &a32[0])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
}
else
{
......@@ -188,9 +188,9 @@ void showsystem(char *outfile) {
else
{
if(ub == INF)
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
else
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
}
}
else
......@@ -198,9 +198,9 @@ void showsystem(char *outfile) {
if(openu &a32[0])
{
if(ub == INF)
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << "inf";
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << "inf";
else
tiimeoutfile << "," << lb << "<" << "x" << j << "<=" << ub;
tiimeoutfile << "," << lb << "<=" << "x" << j << "<" << ub;
}
else
{
......@@ -316,7 +316,7 @@ int main(int argc, char *argv[]) {
tiimeinfile >> opnl; // bounds on the guard
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
if((opnl != 1 && opnl!= 0 )|| (opnu!=0 && opnu!=1))
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
......@@ -380,7 +380,7 @@ int main(int argc, char *argv[]) {
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
if((opnl != 1 && opnl!= 0 )|| (opnu!=0 && opnu!=1))
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
......@@ -412,7 +412,7 @@ int main(int argc, char *argv[]) {
tiimeinfile>> ub; // bounds on the guard
tiimeinfile >> opnu;
if(opnl != 1 || opnl!= 0 || opnu!=0 || opnu!=1)
if((opnl != 1 && opnl!= 0 )|| (opnu!=0 && opnu!=1))
{
cout << "The value of openl and openu must be 0 or 1" << endl;
}
......@@ -442,6 +442,8 @@ int main(int argc, char *argv[]) {
transitions[i].guard = guard;
transitions[i].reset = reset;
transitions[i].openl = openl;
transitions[i].openu = openu;
}
tiimeinfile.close();
showsystem(argv[2]);
......
src/tpdaCGPP.cpp
View file @ aa910b64
......@@ -25,6 +25,7 @@ void print_r_matrix(relation** r_matrix,char p)
cout << r_matrix[i][j] << '\t' ;
cout << endl;
}
cout << endl;
}
// return 1 iff state vs was not found earlier or vs is new state
bool identity(stateGCPP *vs) {
......@@ -393,14 +394,15 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b
relation **store_matrix = allocate_r_matrix(vs->P);
//cout <<"Hi I am called" << endl;
// cout << dn << wn << endl;
for(int i = 0 ;i < vs->P; i++)
for(char i = 0 ;i < vs->P; i++)
{
for(int j = 0; j < vs->P; j++)
for(char j = 0; j < vs->P; j++)
{
store_matrix[i][j] = vs->r_matrix[i][j]; //storing values of the relation matrix to detect any cycle with single les symbol in it.
//cout << store_matrix[i][j] << endl;
}
}
// bool flag1;
#pragma openmp parallel for
for(char x=1; x <= X; x++) {
if( isChecked(x, dn) ) { // if there is a check for clock x
......@@ -437,13 +439,14 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b
{
if((openu & a32[x])) // this condition is open
{
if(store_matrix[t][vs->P-1]> les)
store_matrix[t][vs->P-1] = les;
if(store_matrix[vs->P-1][t]> les)
store_matrix[vs->P-1][t] = les;
//flag1 = true;
}
else // this condition is closed.
{
if(store_matrix[t][vs->P-1] > leq)
store_matrix[t][vs->P-1] = leq;
if(store_matrix[vs->P-1][t] > leq)
store_matrix[vs->P-1][t] = leq;
}
}
......@@ -451,17 +454,21 @@ bool stateGCPP::consSatisfied(stateGCPP* vs,char dn, char wn, short *clockDis, b
{
store_matrix[vs->P-2][vs->P-1] = leq;
}
cout << dn << endl;
cout << endl;
cout << endl;
print_r_matrix(store_matrix,vs->P);
// if(flag1)
// print_r_matrix(store_matrix,vs->P);
pairWiseTightestRelation(store_matrix,vs->P);
print_r_matrix(store_matrix,vs->P);
// if(flag1)
// print_r_matrix(store_matrix,vs->P);
CircuitFinder cf(store_matrix,vs->P);
bool b = cf.run();
if(b)
if(b){
print_r_matrix(store_matrix,vs->P);
//cout << b <<endl;
delete_r_matrix(store_matrix,vs->P);
return false;
}
}
else if( (transitions[dn].ubs[x]) != INF )
{
......@@ -518,7 +525,7 @@ bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr)
}
if(aclr) { // if distance from L to R is small
short dis = dlr + mod( wn - w[P-1], M ); // mark
char t = vs->L; //the source of push must be L.
char t = vs->L-1; //the source of push must be L.
if( ( dis < transitions[dn].lbs[0] ) || dis > ub )
{// check if d(source,destination) \in I
delete_r_matrix(store_matrix,vs->P);
......@@ -545,13 +552,13 @@ bool stateGCPP::stackCheck(stateGCPP* vs,char dn, char wn, short dlr, bool aclr)
{
if(openu & 1)
{
if(store_matrix[t][vs->P-1]> les)
store_matrix[t][vs->P-1] = les;
if(store_matrix[vs->P-1][t]> les)
store_matrix[vs->P-1][t] = les;
}
else
{
if(store_matrix[t][vs->P-1] > leq)
store_matrix[t][vs->P-1] = leq;
if(store_matrix[vs->P-1][t] > leq)
store_matrix[vs->P-1][t] = leq;
}
//here we have to check the relationship of the fractional parts of the source and target
//Here the relation must be {tsm(j) } < {tsm(i)}
......@@ -600,19 +607,19 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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
//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
//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
#pragma openmp parallel for
for(i=0; i < nexttrans[q].size(); i++) {
for(char i=0; i < nexttrans[q].size(); i++) {
dn = nexttrans[q][i]; // i-th upcoming transition
......@@ -638,7 +645,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
for(char x=1; x <= X; x++) { // calculate the distances and accuracy from last reset point to point P for each clock
for(j=P-1; j >= 0; j--) {
for(char 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
......@@ -656,7 +663,7 @@ 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++) {
for(char wn=0; wn < M; wn++) {
//is it checking after adding the point to the state returned by reduce?
// if clock constraint not satisfied
......@@ -674,7 +681,7 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
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
for(char 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
......@@ -695,11 +702,11 @@ vector<stateGCPP*> stateGCPP::addNextTPDA() {
//assume the relation of fraction part with respect to the new system.
//first assume it to be \leq
rs->allocate_r_matrix();// do we need to allocate? or it is sufficent to just point?
for(int i = 0 ;i < vs->P; i++)
for(int a = 0 ;a < vs->P; a++)
{
for(int j = 0; j < vs->P; j++)
for(int b = 0; b < vs->P; b++)
{
rs->r_matrix[i][j]=vs->r_matrix[i][j]; //restoring computed values to the matrix
rs->r_matrix[a][b]=vs->r_matrix[a][b]; //restoring computed values to the matrix
}
}
//I have to allocate because this is changing
......
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