This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import java.util.*; | |
import java.io.*; | |
public class Ddsv | |
{ | |
abstract class Transition | |
{ | |
int target; | |
String label; | |
abstract boolean guard(SharedVars s); | |
abstract SharedVars action(SharedVars s); | |
} | |
class State | |
{ | |
State(int n) { trans = new Transition[n]; } | |
Transition[] trans; | |
} | |
class Process | |
{ | |
Process(int n) { state = new State[n]; } | |
State[] state; | |
} | |
class SharedVars | |
{ | |
int x; | |
int t1; | |
int t2; | |
SharedVars() { | |
x = 0; | |
t1 = 0; | |
t2 = 0; | |
} | |
SharedVars(SharedVars s) { | |
x = s.x; | |
t1 = s.t1; | |
t2 = s.t2; | |
} | |
public int hashCode() { | |
return x + t1 + t2; | |
} | |
public boolean equals(Object o) { | |
SharedVars s = (SharedVars)o; | |
return x == s.x && t1 == s.t1 && t2 == s.t2; | |
} | |
String printString() { | |
return String.format("x=%d t1=%d t2=%d", x, t1, t2); | |
} | |
} | |
class P_read extends Transition | |
{ | |
P_read() { | |
target = 1; | |
label = "P.read"; | |
} | |
boolean guard(SharedVars s) { | |
return true; | |
} | |
SharedVars action(SharedVars s) { | |
SharedVars r = new SharedVars(s); | |
r.t1 = s.x; | |
return r; | |
} | |
} | |
class P_inc extends Transition | |
{ | |
P_inc() { | |
target = 2; | |
label = "P.inc"; | |
} | |
boolean guard(SharedVars s) { | |
return true; | |
} | |
SharedVars action(SharedVars s) { | |
SharedVars r = new SharedVars(s); | |
r.t1 = s.t1 + 1; | |
return r; | |
} | |
} | |
class P_write extends Transition | |
{ | |
P_write() { | |
target = 3; | |
label = "P.write"; | |
} | |
boolean guard(SharedVars s) { | |
return true; | |
} | |
SharedVars action(SharedVars s) { | |
SharedVars r = new SharedVars(s); | |
r.x = s.t1; | |
return r; | |
} | |
} | |
class Q_read extends Transition | |
{ | |
Q_read() { | |
target = 1; | |
label = "Q.read"; | |
} | |
boolean guard(SharedVars s) { | |
return true; | |
} | |
SharedVars action(SharedVars s) { | |
SharedVars r = new SharedVars(s); | |
r.t2 = s.x; | |
return r; | |
} | |
} | |
class Q_inc extends Transition | |
{ | |
Q_inc() { | |
target = 2; | |
label = "Q.inc"; | |
} | |
boolean guard(SharedVars s) { | |
return true; | |
} | |
SharedVars action(SharedVars s) { | |
SharedVars r = new SharedVars(s); | |
r.t2 = s.t2 + 1; | |
return r; | |
} | |
} | |
class Q_write extends Transition | |
{ | |
Q_write() { | |
target = 3; | |
label = "Q.write"; | |
} | |
boolean guard(SharedVars s) { | |
return true; | |
} | |
SharedVars action(SharedVars s) { | |
SharedVars r = new SharedVars(s); | |
r.x = s.t2; | |
return r; | |
} | |
} | |
class Trans | |
{ | |
String label; | |
SysState target; | |
Trans(String l, SysState t) { label = l; target = t; } | |
} | |
class SysState | |
{ | |
int[] state; | |
SharedVars sharedvars; | |
int id; | |
LinkedList<Trans> trans; | |
SysState() { trans = new LinkedList<Trans>(); } | |
public int hashCode() { | |
int hv = 0; | |
for (int i = 0; i < state.length; ++i) { | |
hv += state[i]; | |
} | |
return hv + sharedvars.hashCode(); | |
} | |
public boolean equals(Object o) { | |
SysState s = (SysState)o; | |
for (int i = 0; i < state.length; ++i) { | |
if (state[i] != s.state[i]) | |
return false; | |
} | |
return sharedvars.equals(s.sharedvars); | |
} | |
SysState copy() { | |
SysState t = new SysState(); | |
t.state = new int[state.length]; | |
for (int i = 0; i < state.length; ++i) { | |
t.state[i] = state[i]; | |
} | |
return t; | |
} | |
String printString() { | |
return sharedvars.printString(); | |
} | |
} | |
public Hashtable<SysState, SysState> bfs(Process[] pv, SysState s0) { | |
Hashtable<SysState, SysState> visited = | |
new Hashtable<SysState, SysState>(); | |
LinkedList<SysState> frontier = new LinkedList<SysState>(); | |
frontier.addLast(s0); | |
visited.put(s0, s0); | |
while (!frontier.isEmpty()) { | |
SysState s = frontier.removeFirst(); | |
// for each process | |
for (int i = 0; i < pv.length; ++i) { | |
Transition[] trans = pv[i].state[s.state[i]].trans; | |
// for each transition | |
for (int j = 0; j < trans.length; ++j) { | |
if (trans[j].guard(s.sharedvars)) { | |
SysState t = s.copy(); | |
t.state[i] = trans[j].target; // interleave | |
t.sharedvars = trans[j].action(s.sharedvars); | |
if (!visited.contains(t)) { | |
t.id = visited.size(); | |
visited.put(t, t); | |
frontier.addLast(t); | |
} else { | |
t = visited.get(t); | |
} | |
s.trans.addLast(new Trans(trans[j].label, t)); | |
} | |
} | |
} | |
} | |
return visited; | |
} | |
Process[] define_processes() { | |
Process[] pv = new Process[2]; | |
pv[0] = new Process(4); | |
pv[1] = new Process(4); | |
pv[0].state[0] = new State(1); | |
pv[0].state[1] = new State(1); | |
pv[0].state[2] = new State(1); | |
pv[0].state[3] = new State(0); | |
pv[1].state[0] = new State(1); | |
pv[1].state[1] = new State(1); | |
pv[1].state[2] = new State(1); | |
pv[1].state[3] = new State(0); | |
pv[0].state[0].trans[0] = new P_read(); | |
pv[0].state[1].trans[0] = new P_inc(); | |
pv[0].state[2].trans[0] = new P_write(); | |
pv[1].state[0].trans[0] = new Q_read(); | |
pv[1].state[1].trans[0] = new Q_inc(); | |
pv[1].state[2].trans[0] = new Q_write(); | |
return pv; | |
} | |
SysState make_initial_state() { | |
SysState s = new SysState(); | |
s.state = new int[2]; | |
s.state[0] = 0; | |
s.state[1] = 0; | |
s.sharedvars = new SharedVars(); | |
s.trans = new LinkedList<Trans>(); | |
return s; | |
} | |
Hashtable<SysState, SysState> dd() { | |
Process[] pv = define_processes(); | |
SysState s0 = make_initial_state(); | |
return bfs(pv, s0); | |
} | |
void viz(Hashtable<SysState, SysState> ss) { | |
PrintStream ps; | |
try { | |
ps = new PrintStream(new File("x.dot")); | |
ps.printf("digraph {\n"); | |
for (Enumeration<SysState> e = ss.keys(); e.hasMoreElements(); ) { | |
SysState s = e.nextElement(); | |
ps.printf("%d [label=\"%s\"];\n", s.id, s.printString()); | |
} | |
for (Enumeration<SysState> e = ss.keys(); e.hasMoreElements(); ) { | |
SysState s = e.nextElement(); | |
for (Iterator<Trans> i = s.trans.descendingIterator(); | |
i.hasNext(); ) { | |
Trans tr = i.next(); | |
ps.printf("%d -> %d [label=\"%s\"];\n", | |
s.id, tr.target.id, tr.label); | |
} | |
} | |
ps.printf("}\n"); | |
} catch (Exception e) { | |
} | |
} | |
public static void main(String[] args) { | |
Ddsv ddsv = new Ddsv(); | |
Hashtable<SysState, SysState> ss = ddsv.dd(); | |
ddsv.viz(ss); | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment