Ddsv.java

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);
    }
}