Skip to content

Instantly share code, notes, and snippets.

@hatsugai

hatsugai/Ddsv.java

Created Oct 23, 2019
Embed
What would you like to do?
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
You can’t perform that action at this time.