// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The following module checks whether a given graph has cycles. This is done // // essentially by computing the transitive hull of the graph, thus O(log(N)) // // time using O(N^3) processors is sufficient. // // ************************************************************************** // macro N = 9; module CyclicByTransHull([N][N]bool ?a,event hasCycle,!rdy) { [N][N]bool t; // compute the transitive hull in graph scc TransHull_OlogN(a,t,rdy); // check whether there is cycle in the graph for(i=0..N-1) for(j=i..N-1) if(t[i][j] & t[j][i]) hasCycle = true; } drivenby g1 { // the assignments below construct the following graph: // // 3 // / \ // v v // 0 -> 1 <-> 2-> 4 <-> 5 <-> 6 // | | // v v // 7<| 8 // |_| // a[0][1] = true; a[1][2] = true; a[2][1] = true; a[2][4] = true; a[2][7] = true; a[3][2] = true; a[3][4] = true; a[4][5] = true; a[5][4] = true; a[5][6] = true; a[5][8] = true; a[6][5] = true; a[7][7] = true; await(rdy); assert(hasCycle); } drivenby g2 { // worst case example: a chain of length N a[0][1] = true; a[1][2] = true; a[2][3] = true; a[3][4] = true; a[4][5] = true; a[5][6] = true; a[6][7] = true; await(rdy); assert(!hasCycle); }