/**
 * Copyright (c) 2004-2005, Regents of the University of California
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 *
 * Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimer.
 *
 * Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 *
 * Neither the name of the University of California, Los Angeles nor the
 * names of its contributors may be used to endorse or promote products
 * derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */

package avrora.stack;

import avrora.core.Program;
import cck.text.Printer;
import cck.text.StringUtil;
import cck.util.Util;
import java.util.Iterator;

/**
 * @author Ben L. Titzer
 */
public class StateTransitionGraph {

    public static class StateList {
        public final StateCache.State state;
        public final StateList next;

        StateList(StateCache.State tar, StateList n) {
            state = tar;
            next = n;
        }
    }

    public static class EdgeList {
        public final Edge edge;
        public final EdgeList next;

        EdgeList(Edge tar, EdgeList n) {
            edge = tar;
            next = n;
        }
    }

    /**
     * The <code>Edge</code> inner class represents a bidirectional edge between two states. It is contained
     * on two linked lists: the forward edge list of the source node and the backward edge list of the target
     * node.
     */
    public static class Edge {
        public final StateCache.State source;
        public final StateCache.State target;
        public final Edge forwardLink;
        public final Edge backwardLink;
        public final int type;
        public final int weight;

        Edge(StateCache.State source, StateCache.State target, Edge fl, Edge bl, int type, int weight) {
            this.source = source;
            this.target = target;
            this.forwardLink = fl;
            this.backwardLink = bl;
            this.type = type;
            this.weight = weight;
        }
    }

    /**
     * The <code>StateInfo</code> class is a representation of both the forward and backward edge list
     * corresponding to a node in the state transition graph. It also stores a cache of reachable return
     * states (based on backwards reachability search).
     */
    public static class StateInfo {
        public final StateCache.State state;
        public StateCache.Set stateSet;
        public Edge forwardEdges;
        public Edge backwardEdges;

        StateInfo(StateCache.State s) {
            state = s;
        }

        public Edge addEdge(int type, int weight, StateCache.State target) {
            Edge nedge = new Edge(state, target, forwardEdges, target.info.backwardEdges, type, weight);

            this.forwardEdges = nedge;
            target.info.backwardEdges = nedge;
            return nedge;
        }
    }

    /**
     * The <code>frontierList</code> field stores a simple linked list of the current states on the frontier.
     */
    private StateList frontierList;

    /**
     * The <code>cache</code> field stores a cache of all states; it guarantees that object equality for
     * states implies reference equality and vice versa.
     */
    private StateCache cache;

    private long edgeCount;
    private long frontierCount;
    private long exploredCount;

    private final StateCache.State edenState;

    /**
     * The constructor for the <code>StateTransitionGraph</code> class constructs a new state transition
     * graph, with a state cache. The program passed is used as an approximation of the possible size of the
     * state space.
     *
     * @param p the program to create a state transition graph for.
     */
    public StateTransitionGraph(Program p) {
        cache = new StateCache(p);
        edenState = cache.getEdenState();
        edenState.info = new StateInfo(edenState);
        addFrontierState(edenState);
    }


    /**
     * The <code>getCachedState()</code> method looks for the a cached, immutable state that corresponds to
     * the given mutable state. If there is no cached state yet, it will create and return a new one.
     *
     * @param s the mutable state to look for
     * @return an instance of the <code>StateCache.LegacyState</code> class
     */
    public StateCache.State getCachedState(MutableState s) {
        StateCache.State ns = cache.getStateFor(s);
        if (ns.info == null) ns.info = new StateInfo(ns);
        return ns;
    }

    /**
     * The <code>addEdge()</code> method adds an edge between two states in the state transition graph. The
     * edge has a type and a weight.
     *
     * @param s      the source node of the edge
     * @param type   the type of the edge as an integer
     * @param weight the weight of the edge as an integer
     * @param t      the target node of the edge
     */
    public Edge addEdge(StateCache.State s, int type, int weight, StateCache.State t) {
        if (s.info == null)
            throw Util.failure("No edge info for: " + s.getUniqueName());
        if (t.info == null)
            throw Util.failure("No edge info for: " + t.getUniqueName());
        edgeCount++;
        return s.info.addEdge(type, weight, t);
    }

    /**
     * The <code>getNextFrontierState()</code> chooses a state off of the state frontier, removes it from the
     * state frontier, and returns it. If there are no states left on the state frontier, this method returns
     * null. Note that initially only the eden state is on the frontier.
     *
     * @return one of the states on the current state frontier; null if there are none.
     */
    public StateCache.State getNextFrontierState() {
        if (frontierList == null) return null;
        StateList l = frontierList;
        frontierList = frontierList.next;

        StateCache.State state = l.state;
        if (state.info == null)
            throw Util.failure("LegacyState on frontier has no edge info: " + state.getUniqueName());

        state.onFrontier = false;
        frontierCount--;
        return state;
    }

    /**
     * The <code>addFrontierState</code> method adds a state to the frontier.
     *
     * @param s the state to add
     */
    public void addFrontierState(StateCache.State s) {
        if (isExplored(s))
            throw Util.failure("Attempt to re-add state to frontier: " + s.getUniqueName());

        if (!isFrontier(s)) {
            frontierList = new StateList(s, frontierList);
            s.onFrontier = true;
            frontierCount++;
        }
    }

    /**
     * The <code>isExplored()</code> method tests whether a given state has been explored before.
     *
     * @param s the cached state to test whether it is explored
     * @return true if this state has been explored and had its outgoing edges computed; false otherwise
     */
    public boolean isExplored(StateCache.State s) {
        return s.isExplored;
    }

    /**
     * The <code>setExplored()</code> method marks the given state as having been explored. A state cannot
     * both be explored and be on the frontier; thus this method will throw a fatal error if the given state
     * is marked as on the frontier.
     *
     * @param s the state to mark as explored
     */
    public void setExplored(StateCache.State s) {
        if (isFrontier(s))
            throw Util.failure("state cannot be on frontier and explored: " + s.getUniqueName());

        if (!isExplored(s)) {
            s.isExplored = true;
            exploredCount++;
        }
    }

    /**
     * The <code>isFrontier()</code> method tests whether a given state is currently in the frontier list of
     * the state transition graph.
     *
     * @param s the state to test whether it is on the frontier
     * @return true if the state is currently on the frontier of the state transition graph; false otherwise
     */
    public boolean isFrontier(StateCache.State s) {
        return s.onFrontier;
    }

    /**
     * The <code>getStateCache()</code> method gets the cache of all the states in the state space.
     *
     * @return a reference to the cache of all the states in the state transition graph
     */
    public StateCache getStateCache() {
        return cache;
    }

    public StateCache.State getEdenState() {
        return edenState;
    }

    public long getFrontierCount() {
        return frontierCount;
    }

    public long getEdgeCount() {
        return edgeCount;
    }

    public long getExploredCount() {
        return exploredCount;
    }

    public StateCache.Set newSet() {
        return cache.newSet();
    }

    public void deleteStateSets() {
        Iterator<StateCache.State> i = cache.getStateIterator();
        while (i.hasNext()) {
            StateCache.State state = (StateCache.State)i.next();
            state.info.stateSet = null;
        }
    }

    public void dump(Printer p) {
        Iterator<StateCache.State> i = cache.getStateIterator();
        while (i.hasNext()) {
            StateCache.State state = i.next();
            StringBuffer buf = dumpToBuffer(state);
            p.println(buf.toString());
        }

        i = cache.getStateIterator();
        while (i.hasNext()) {
            StateCache.State state = (StateCache.State)i.next();
            for (Edge e = state.info.forwardEdges; e != null; e = e.forwardLink) {
                StringBuffer buf = dumpToBuffer(e);
                p.println(buf.toString());
            }
        }
    }

    private StringBuffer dumpToBuffer(Edge e) {
        StringBuffer buf = new StringBuffer(32);
        buf.append('[');
        buf.append(e.source.getUniqueName());
        buf.append("] --(");
        buf.append(Analyzer.EDGE_NAMES[e.type]);
        buf.append(',');
        buf.append(e.weight);
        buf.append(")--> [");
        buf.append(e.target.getUniqueName());
        buf.append(']');
        return buf;
    }

    private StringBuffer dumpToBuffer(StateCache.State state) {
        StringBuffer buf = new StringBuffer(300);
        buf.append('[');
        buf.append(state.getUniqueName());
        buf.append(':');
        buf.append(state.getType());
        buf.append("] PC=");
        buf.append(StringUtil.addrToString(state.getPC()));
        buf.append(" SREG=");
        buf.append(AbstractArithmetic.toString(state.getSREG()));
        buf.append(" EIMSK=");
        buf.append(AbstractArithmetic.toString(state.getIORegisterAV(IORegisterConstants.EIMSK)));
        buf.append(" TIMSK=");
        buf.append(AbstractArithmetic.toString(state.getIORegisterAV(IORegisterConstants.TIMSK)));
        for (int cntr = 0; cntr < IORegisterConstants.NUM_REGS; cntr++) {
            buf.append(' ');
            buf.append(AbstractInterpreter.toShortString(state.getRegisterAV(cntr)));
        }
        return buf;
    }
}
