text:
/**
 *
 */
package automata.svpa;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Stack;

import org.sat4j.specs.TimeoutException;

import automata.AutomataException;
import theory.BooleanAlgebra;
import utilities.BitVecUtil;
import utilities.Pair;

public class SVPA extends VPAutomaton {

	// Constants
	/**
	 * Returns the empty SVPA for the boolean algebra ba
	 */
	public static  SVPA getEmptySVPA(BooleanAlgebra ba) {
		SVPA aut = new SVPA();
		aut.states = new HashSet<Integer>();
		aut.states.add(0);
		aut.finalStates = new HashSet<Integer>();
		aut.initialStates = new HashSet<Integer>(aut.states);
		aut.isDeterministic = true;
		aut.isEpsilonFree = true;
		aut.isEmpty = true;
		aut.isTotal = true;
		aut.stateCount = 1;
		aut.maxStateId = 0;
		aut.maxStackStateId = 0;
		return aut;
	}

	/**
	 * Returns the SVPA accepting every list for the boolean algebra
	 * ba
	 */
	public static  SVPA getFullSVPA(BooleanAlgebra ba) {
		SVPA aut = new SVPA();
		aut.states = new HashSet<Integer>();
		aut.states.add(0);
		aut.finalStates = new HashSet<Integer>(aut.states);
		aut.initialStates = new HashSet<Integer>(aut.states);
		aut.isDeterministic = true;
		aut.isEmpty = false;
		aut.isEpsilonFree = true;
		aut.stateCount = 1;
		aut.maxStateId = 0;
		aut.maxStackStateId = 0;
		aut.isTotal = true;
		try {
			aut.addTransition(new Internal(0, 0, ba.True()), ba, true);
			aut.addTransition(new Call(0, 0, 0, ba.True()), ba, true);
			aut.addTransition(new Return(0, 0, 0, ba.True()), ba, true);
			aut.addTransition(new ReturnBS(0, 0, ba.True()), ba, true);
		} catch (TimeoutException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		return aut;
	}

	protected Collection<Integer> states;
	protected Collection<Integer> stackStates;

	protected Collection<Integer> initialStates;
	protected Collection<Integer> finalStates;

	protected Map<Integer, Collection<SVPAEpsilon>> epsilonsFrom;
	protected Map<Integer, Collection<Internal>> internalsFrom;
	protected Map<Integer, Collection<Call>> callsFrom;
	protected Map<Pair<Integer, Integer>, Collection<Return>> returnsFrom;
	protected Map<Integer, Collection<ReturnBS>> returnBSFrom;

	protected Map<Integer, Collection<SVPAEpsilon>> epsilonsTo;
	protected Map<Integer, Collection<Internal>> internalsTo;
	protected Map<Integer, Collection<Call>> callsTo;
	protected Map<Pair<Integer, Integer>, Collection<Return>> returnsTo;
	protected Map<Integer, Collection<ReturnBS>> returnBSTo;

	public Integer stateCount;
	public Integer maxStateId;
	public Integer maxStackStateId;
	public Integer transitionCount;

	protected SVPA() {
		super();

		initialStates = new HashSet<Integer>();
		finalStates = new HashSet<Integer>();
		states = new HashSet<Integer>();
		stackStates = new HashSet<Integer>();

		epsilonsFrom = new HashMap<Integer, Collection<SVPAEpsilon>>();
		internalsFrom = new HashMap<Integer, Collection<Internal>>();
		callsFrom = new HashMap<Integer, Collection<Call>>();
		returnsFrom = new HashMap<Pair<Integer, Integer>, Collection<Return>>();
		returnBSFrom = new HashMap<Integer, Collection<ReturnBS>>();

		epsilonsTo = new HashMap<Integer, Collection<SVPAEpsilon>>();
		internalsTo = new HashMap<Integer, Collection<Internal>>();
		callsTo = new HashMap<Integer, Collection<Call>>();
		returnsTo = new HashMap<Pair<Integer, Integer>, Collection<Return>>();
		returnBSTo = new HashMap<Integer, Collection<ReturnBS>>();

		stateCount = 0;
		maxStateId = 0;
		maxStackStateId = 0;
		transitionCount = 0;
	}

	/*
	 * Create an automaton (removes unreachable states)
	 */
	public static <T, S1> SVPA<T, S1> MkSVPA(
			Collection<SVPAMove<T, S1>> transitions,
			Collection<Integer> initialStates, Collection<Integer> finalStates,
			BooleanAlgebra<T, S1> ba) throws AutomataException, TimeoutException {

		// Sanity checks
		if (initialStates.size() == 0)
			throw new AutomataException("No initial states");

		SVPA<T, S1> aut = new SVPA<T, S1>();

		aut.states = new HashSet<Integer>(initialStates);
		aut.states.addAll(finalStates);

		aut.initialStates = initialStates;
		aut.finalStates = finalStates;

		for (SVPAMove<T, S1> t : transitions)
			aut.addTransition(t, ba, false);

		// remove unreachable states
		return removeUnreachableStates(aut, ba);
	}

	public boolean accepts(List<TaggedSymbol<S>> input, BooleanAlgebra ba) throws TimeoutException {

		Collection<Pair<Integer, Stack<Pair<Integer, S>>>> currConf = new HashSet<Pair<Integer, Stack<Pair<Integer, S>>>>();

		for (Integer state : initialStates)
			currConf.add(new Pair<Integer, Stack<Pair<Integer, S>>>(state,
					new Stack<Pair<Integer, S>>()));

		currConf = getConfigurationEpsClosure(currConf, ba);
		for (TaggedSymbol<S> el : input) {
			currConf = getNextState(currConf, el, ba);
			currConf = getConfigurationEpsClosure(currConf, ba);
			if (currConf.isEmpty())
				return false;
		}

		for (Pair<Integer, Stack<Pair<Integer, S>>> state : currConf)
			if (isFinalState(state.first))
				return true;

		return false;
	}

	private Collection<Pair<Integer, Stack<Pair<Integer, S>>>> getConfigurationEpsClosure(
			Collection<Pair<Integer, Stack<Pair<Integer, S>>>> currConf,
			BooleanAlgebra ba) {

		Collection<Pair<Integer, Stack<Pair<Integer, S>>>> currConfEps = currConf;
		LinkedList<Pair<Integer, Stack<Pair<Integer, S>>>> toVisit = new LinkedList<Pair<Integer, Stack<Pair<Integer, S>>>>(
				currConf);

		while (toVisit.size() > 0) {
			Pair<Integer, Stack<Pair<Integer, S>>> visState = toVisit.remove();

			for (SVPAEpsilon t : getEpsilonsFrom(visState.first)) {
				Pair<Integer, Stack<Pair<Integer, S>>> newEl = new Pair<Integer, Stack<Pair<Integer, S>>>(
						t.to, visState.second);
				if (!currConfEps.contains(newEl)) {
					currConfEps.add(newEl);
					toVisit.add(newEl);
				}
			}
		}
		return currConfEps;
	}

	private Collection<Integer> getEpsClosure(Integer state,
			BooleanAlgebra ba) {

		HashSet<Integer> st = new HashSet<Integer>();
		st.add(state);
		return getEpsClosure(st, ba);
	}

	private Collection<Integer> getEpsClosure(Collection<Integer> fronteer,
			BooleanAlgebra ba) {

		Collection<Integer> reached = new HashSet<Integer>(fronteer);
		LinkedList<Integer> toVisit = new LinkedList<Integer>(fronteer);

		while (toVisit.size() > 0) {
			for (SVPAEpsilon t : getEpsilonsFrom(toVisit.removeFirst())) {
				if (!reached.contains(t.to)) {
					reached.add(t.to);
					toVisit.add(t.to);
				}
			}
		}
		return reached;
	}

	public Collection<Pair<Integer, Stack<Pair<Integer, S>>>> getNextState(
			Collection<Pair<Integer, Stack<Pair<Integer, S>>>> currConf,
			TaggedSymbol<S> input, BooleanAlgebra ba) throws TimeoutException {

		Collection<Pair<Integer, Stack<Pair<Integer, S>>>> nextState = new HashSet<Pair<Integer, Stack<Pair<Integer, S>>>>();

		for (Pair<Integer, Stack<Pair<Integer, S>>> conf : currConf) {

			Pair<Integer, Stack<Pair<Integer, S>>> newState = null;
			for (SVPAMove t : getTransitionsFrom(conf)) {
				newState = t.getNextState(conf, input, ba);
				if (newState != null)
					nextState.add(newState);
			}
		}
		return nextState;
	}

	/**
	 * return an equivalent copy without epsilon moves
	 * @throws TimeoutException
	 */
	public SVPA removeEpsilonMoves(BooleanAlgebra ba) throws TimeoutException {
		return removeEpsilonMovesFrom(this, ba);
	}

	/**
	 * return an equivalent copy without epsilon moves
	 * @throws TimeoutException
	 */
	@SuppressWarnings("unchecked")
	public static  SVPA removeEpsilonMovesFrom(SVPA aut,
			BooleanAlgebra ba) throws TimeoutException {

		if (aut.isEpsilonFree)
			return (SVPA) aut.clone();

		SVPA epsFree = new SVPA();

		HashMap<Collection<Integer>, Integer> reachedStates = new HashMap<Collection<Integer>, Integer>();
		LinkedList<Collection<Integer>> toVisitStates = new LinkedList<Collection<Integer>>();

		// Add initial states
		for (Integer st1 : aut.initialStates) {
			Collection<Integer> p = aut.getEpsClosure(st1, ba);
			int nextId = reachedStates.size();

			epsFree.initialStates.add(nextId);
			epsFree.states.add(nextId);

			reachedStates.put(p, nextId);
			toVisitStates.add(p);
		}

		while (!toVisitStates.isEmpty()) {
			Collection<Integer> currState = toVisitStates.removeFirst();
			int currStateId = reachedStates.get(currState);

			if (aut.isFinalConfiguration(currState))
				epsFree.finalStates.add(currStateId);

			for (SVPAMove t1 : aut.getTransitionsFrom(currState)) {
				if (t1.type != Tag.Epsilon) {

					Collection<Integer> nextState = aut
							.getEpsClosure(t1.to, ba);

					Integer nextStateId = reachedStates.get(nextState);

					if (nextStateId == null) {
						int index = reachedStates.size();
						reachedStates.put(nextState, index);
						toVisitStates.add(nextState);
						nextStateId = index;
					}

					SVPAMove tnew = (SVPAMove) t1.clone();
					tnew.from = currStateId;
					tnew.to = nextStateId;

					epsFree.addTransition(tnew, ba, true);
				}
			}
		}

		return removeUnreachableStates(epsFree, ba);
	}

	/**
	 * Computes the intersection with aut as a new SVPA
	 * @throws TimeoutException
	 */
	public SVPA intersectionWith(SVPA aut, BooleanAlgebra ba) throws TimeoutException {
		return intersection(this, aut, ba);
	}

	/**
	 * Computes the intersection with aut as a new SVPA
	 * @throws TimeoutException
	 */
	public static  SVPA intersection(SVPA aut1,
			SVPA aut2, BooleanAlgebra ba) throws TimeoutException {

		SVPA inters = new SVPA();

		Map<Pair<Integer, Integer>, Integer> reachedStackStates = new HashMap<Pair<Integer, Integer>, Integer>();

		Map<Pair<Integer, Integer>, Integer> reachedStates = new HashMap<Pair<Integer, Integer>, Integer>();
		LinkedList<Pair<Integer, Integer>> toVisitStates = new LinkedList<Pair<Integer, Integer>>();

		// Add initial states
		for (Integer st1 : aut1.initialStates)
			for (Integer st2 : aut2.initialStates) {
				Pair<Integer, Integer> p = new Pair<Integer, Integer>(st1, st2);
				int nextId = reachedStates.size();

				inters.initialStates.add(nextId);
				inters.states.add(nextId);

				reachedStates.put(p, nextId);
				toVisitStates.add(p);
			}

		// DFS to discover next states and transitions
		while (!toVisitStates.isEmpty()) {
			Pair<Integer, Integer> currState = toVisitStates.removeFirst();
			int currStateId = reachedStates.get(currState);

			// Consider epsilon closure
			Collection<Integer> epsClose1 = aut1.getEpsClosure(currState.first,
					ba);
			Collection<Integer> epsClose2 = aut2.getEpsClosure(
					currState.second, ba);

			boolean isFin = false;
			for (Integer st : epsClose1)
				if (aut1.isFinalState(st)) {
					isFin = true;
					break;
				}
			if (isFin) {
				isFin = false;
				for (Integer st : epsClose2)
					if (aut2.isFinalState(st)) {
						isFin = true;
						break;
					}
				if (isFin)
					inters.finalStates.add(currStateId);
			}

			for (Return t1 : aut1.getReturnsFrom(epsClose1))
				for (Return t2 : aut2.getReturnsFrom(epsClose2)) {
					A intersGuard = ba.MkAnd(t1.guard, t2.guard);
					if (ba.IsSatisfiable(intersGuard)) {

						Pair<Integer, Integer> nextState = new Pair<Integer, Integer>(
								t1.to, t2.to);
						Pair<Integer, Integer> nextStackState = new Pair<Integer, Integer>(
								t1.stackState, t2.stackState);

						int nextStateId = addStateBinOpHelper(inters,
								reachedStates, toVisitStates, nextState, 0);
						int nextStackStateId = addStackStateBinOpHelper(inters,
								reachedStackStates, nextStackState, 0);

						Return newTrans = new Return(currStateId,
								nextStateId, nextStackStateId, intersGuard);

						inters.addTransition(newTrans, ba, true);
					}
				}

			for (Call t1 : aut1.getCallsFrom(epsClose1))
				for (Call t2 : aut2.getCallsFrom(epsClose2)) {
					A intersGuard = ba.MkAnd(t1.guard, t2.guard);
					if (ba.IsSatisfiable(intersGuard)) {

						Pair<Integer, Integer> nextState = new Pair<Integer, Integer>(
								t1.to, t2.to);
						Pair<Integer, Integer> nextStackState = new Pair<Integer, Integer>(
								t1.stackState, t2.stackState);

						int nextStateId = addStateBinOpHelper(inters,
								reachedStates, toVisitStates, nextState, 0);
						int nextStackStateId = addStackStateBinOpHelper(inters,
								reachedStackStates, nextStackState, 0);

						Call newTrans = new Call(currStateId,
								nextStateId, nextStackStateId, intersGuard);

						inters.addTransition(newTrans, ba, true);
					}
				}

			for (ReturnBS t1 : aut1.getReturnBSFrom(epsClose1))
				for (ReturnBS t2 : aut2.getReturnBSFrom(epsClose2)) {
					A intersGuard = ba.MkAnd(t1.guard, t2.guard);
					if (ba.IsSatisfiable(intersGuard)) {
						Pair<Integer, Integer> nextState = new Pair<Integer, Integer>(
								t1.to, t2.to);
						int nextStateId = addStateBinOpHelper(inters,
								reachedStates, toVisitStates, nextState, 0);
						ReturnBS newTrans = new ReturnBS(
								currStateId, nextStateId, intersGuard);

						inters.addTransition(newTrans, ba, true);
					}
				}

			for (Internal t1 : aut1.getInternalsFrom(epsClose1))
				for (Internal t2 : aut2.getInternalsFrom(epsClose2)) {
					A intersGuard = ba.MkAnd(t1.guard, t2.guard);
					if (ba.IsSatisfiable(intersGuard)) {
						Pair<Integer, Integer> nextState = new Pair<Integer, Integer>(
								t1.to, t2.to);
						int nextStateId = addStateBinOpHelper(inters,
								reachedStates, toVisitStates, nextState, 0);
						Internal newTrans = new Internal(
								currStateId, nextStateId, intersGuard);
						inters.addTransition(newTrans, ba, true);
					}
				}

		}

		return removeUnreachableStates(inters, ba);
	}

	private static  int addStateBinOpHelper(SVPA binAut,
			Map<Pair<Integer, Integer>, Integer> reachedStates,
			LinkedList<Pair<Integer, Integer>> toVisitStates,
			Pair<Integer, Integer> state, int offSet) {
		if (!reachedStates.containsKey(state)) {
			int index = reachedStates.size() + offSet;
			reachedStates.put(state, index);
			toVisitStates.add(state);
			binAut.states.add(index);
			return index;
		} else {
			return reachedStates.get(state);
		}
	}

	private static  int addStackStateBinOpHelper(SVPA binAut,
			Map<Pair<Integer, Integer>, Integer> reachedStates,
			Pair<Integer, Integer> stackState, int offSet) {
		if (!reachedStates.containsKey(stackState)) {
			int index = reachedStates.size() + offSet;
			reachedStates.put(stackState, index);
			binAut.stackStates.add(index);
			for (Integer state : binAut.states) {
				binAut.returnsFrom.put(
						new Pair<Integer, Integer>(state, index),
						new HashSet<Return>());
				binAut.returnsTo.put(new Pair<Integer, Integer>(state, index),
						new HashSet<Return>());
			}
			return index;
		} else {
			return reachedStates.get(stackState);
		}
	}

	/**
	 * Computes the union with aut as a new SVPA
	 * @throws TimeoutException
	 */
	public SVPA unionWith(SVPA aut1, BooleanAlgebra ba) throws TimeoutException {
		return union(this, aut1, ba);
	}

	/**
	 * Computes the union with aut as a new SVPA
	 * @throws TimeoutException
	 */
	public static  SVPA union(SVPA aut1, SVPA aut2,
			BooleanAlgebra ba) throws TimeoutException {

		if (aut1.isEmpty && aut2.isEmpty)
			return getEmptySVPA(ba);

		SVPA union = new SVPA();
		union.isEmpty = false;

		int offSet = aut1.maxStateId + 2;
		union.maxStateId = aut2.maxStateId + offSet;

		for (Integer state : aut1.states)
			union.states.add(state + 1);

		for (Integer state : aut2.states)
			union.states.add(state + offSet);

		union.initialStates.add(0);

		for (SVPAMove t : aut1.getTransitions()) {
			@SuppressWarnings("unchecked")
			SVPAMove newMove = (SVPAMove) t.clone();
			newMove.from++;
			newMove.to++;
			union.addTransition(newMove, ba, true);
		}

		for (SVPAMove t : aut2.getTransitions()) {
			@SuppressWarnings("unchecked")
			SVPAMove newMove = (SVPAMove) t.clone();
			newMove.from += offSet;
			newMove.to += offSet;
			union.addTransition(newMove, ba, true);
		}

		for (Integer state : aut1.initialStates)
			union.addTransition(new SVPAEpsilon(0, state + 1), ba, true);

		for (Integer state : aut2.initialStates)
			union.addTransition(new SVPAEpsilon(0, state + offSet), ba, true);

		for (Integer state : aut1.finalStates)
			union.finalStates.add(state + 1);

		for (Integer state : aut2.finalStates)
			union.finalStates.add(state + offSet);

		return union;
	}

	/**
	 * Computes this minus aut2
	 * @throws TimeoutException
	 */
	public SVPA minus(SVPA aut, BooleanAlgebra ba) throws TimeoutException {
		return differnce(this, aut, ba);
	}

	/**
	 * Computes aut1 minus aut2
	 * @throws TimeoutException
	 */
	public static  SVPA differnce(SVPA aut1, SVPA aut2,
			BooleanAlgebra ba) throws TimeoutException {

		SVPA diff = aut1.intersectionWith(aut2.complement(ba), ba);
		return removeUnreachableStates(diff, ba);
	}

	/**
	 * return the complement of the current SVPA
	 * @throws TimeoutException
	 */
	public SVPA complement(BooleanAlgebra ba) throws TimeoutException {
		return complementOf(this, ba);
	}

	/**
	 * return the complement of the current SVPA
	 * @throws TimeoutException
	 */
	public static  SVPA complementOf(SVPA aut,
			BooleanAlgebra ba) throws TimeoutException {
		SVPA comp = aut.mkTotal(ba);

		Collection<Integer> finStateCopy = new HashSet<Integer>(
				comp.finalStates);
		comp.finalStates = new HashSet<Integer>();

		for (Integer st : comp.states)
			if (!finStateCopy.contains(st))
				comp.finalStates.add(st);

		return comp;
	}

	/**
	 * return the total version of the current SVPA
	 * @throws TimeoutException
	 */
	public SVPA mkTotal(BooleanAlgebra ba) throws TimeoutException {
		return mkTotal(this, ba);
	}

	/**
	 * return the total version of aut
	 * @throws TimeoutException
	 */
	@SuppressWarnings("unchecked")
	public static  SVPA mkTotal(SVPA aut,
			BooleanAlgebra ba) throws TimeoutException {

		if (aut.isTotal)
			return (SVPA) aut.clone();

		SVPA svpa = aut;
		if (!aut.isDeterministic(ba))
			svpa = determinize(aut, ba);

		SVPA total = new SVPA();
		total.initialStates = new HashSet<Integer>(svpa.initialStates);
		total.finalStates = new HashSet<Integer>(svpa.finalStates);

		int newState = svpa.maxStateId + 1;
		for (Integer state : svpa.states) {
			// INTERNAL MOVES
			A totGuard = null;
			for (Internal move : svpa.getInternalsFrom(state)) {
				total.addTransition(move, ba, true);
				if (totGuard == null)
					totGuard = ba.MkNot(move.guard);
				else
					totGuard = ba.MkAnd(totGuard, ba.MkNot(move.guard));
			}
			if (totGuard != null)
				total.addTransition(new Internal(state, newState,
						totGuard), ba, false);
			else
				total.addTransition(
						new Internal(state, newState, ba.True()), ba,
						false);

			// RETURNBS MOVES
			totGuard = null;
			for (ReturnBS move : svpa.getReturnBSFrom(state)) {
				total.addTransition(move, ba, true);
				if (totGuard == null)
					totGuard = ba.MkNot(move.guard);
				else
					totGuard = ba.MkAnd(totGuard, ba.MkNot(move.guard));
			}
			if (totGuard != null)
				total.addTransition(new ReturnBS(state, newState,
						totGuard), ba, false);
			else
				total.addTransition(
						new ReturnBS(state, newState, ba.True()), ba,
						false);

			// CALL MOVES
			totGuard = null;
			for (Call move : svpa.getCallsFrom(state)) {
				total.addTransition(move, ba, true);
				if (totGuard == null)
					totGuard = ba.MkNot(move.guard);
				else
					totGuard = ba.MkAnd(totGuard, ba.MkNot(move.guard));
			}
			if (totGuard != null)
				total.addTransition(
						new Call(state, newState, 0, totGuard), ba, false);
			else
				total.addTransition(
						new Call(state, newState, 0, ba.True()), ba,
						false);

			// RETURNS MOVES
			for (Integer stackState : svpa.stackStates) {
				totGuard = null;
				for (Return move : svpa.getReturnsFrom(state, stackState)) {
					total.addTransition(move, ba, true);
					if (totGuard == null)
						totGuard = ba.MkNot(move.guard);
					else
						totGuard = ba.MkAnd(totGuard, ba.MkNot(move.guard));
				}
				if (totGuard != null)
					total.addTransition(new Return(state, newState,
							stackState, totGuard), ba, false);
				else
					total.addTransition(new Return(state, newState,
							stackState, ba.True()), ba, false);
			}
		}
		if (total.states.contains(newState)) {
			total.addTransition(
					new Internal(newState, newState, ba.True()), ba, true);
			total.addTransition(
					new ReturnBS(newState, newState, ba.True()), ba, true);
			total.addTransition(
					new Call(newState, newState, 0, ba.True()), ba, true);
			for (Integer stSt : total.stackStates) {
				total.addTransition(new Return(newState, newState, stSt,
						ba.True()), ba, true);
			}
		}

		total.isTotal = true;
		total.stateCount = total.states.size();
		return total;
	}

	/**
	 * return the complement of the current SVPA
	 * @throws TimeoutException
	 */
	public boolean isEquivalentTo(SVPA aut, BooleanAlgebra ba) throws TimeoutException {
		return areEquivalent(this, aut, ba);
	}

	/**
	 * return the complement of the current SVPA
	 * @throws TimeoutException
	 */
	public static  boolean areEquivalent(SVPA aut1,
			SVPA aut2, BooleanAlgebra ba) throws TimeoutException {
		if (!differnce(aut1, aut2, ba).isEmpty)
			return false;
		return differnce(aut2, aut1, ba).isEmpty;
	}

	/**
	 * return the determinization of the current SVPA
	 * @throws TimeoutException
	 */
	public SVPA determinize(BooleanAlgebra ba) throws TimeoutException {
		return determinize(this, ba);
	}

	/**
	 * return the determinization of aut
	 * @throws TimeoutException
	 */
	public static  SVPA determinize(SVPA aut1,
			BooleanAlgebra ba) throws TimeoutException {

		// Remove epsilon before starting
		SVPA aut = aut1;
		if (!aut1.isEpsilonFree)
			aut = removeEpsilonMovesFrom(aut1, ba);

		if (aut1.isDeterministic(ba))
			return aut1;

		SVPA deter = new SVPA();

		HashMap<Collection<Pair<Integer, Integer>>, Integer> reachedStates = new HashMap<Collection<Pair<Integer, Integer>>, Integer>();
		LinkedList<Collection<Pair<Integer, Integer>>> toVisitStates = new LinkedList<Collection<Pair<Integer, Integer>>>();

		HashMap<Pair<Collection<Pair<Integer, Integer>>, A>, Integer> reachedStackStates = new HashMap<Pair<Collection<Pair<Integer, Integer>>, A>, Integer>();

		// Add initial state
		Collection<Pair<Integer, Integer>> currState = new HashSet<Pair<Integer, Integer>>();
		for (Integer st : aut.initialStates)
			currState.add(new Pair<Integer, Integer>(st, st));
		deter.initialStates.add(0);
		deter.states.add(0);

		reachedStates.put(currState, 0);
		toVisitStates.add(currState);

		Collection<Collection<Pair<Integer, Integer>>> previouslyVisited = new HashSet<Collection<Pair<Integer, Integer>>>();

		while (toVisitStates.size() > 0) {

			// pop first state from tVisit and add to visited
			currState = toVisitStates.removeFirst();
			int currStateId = reachedStates.get(currState);
			previouslyVisited.add(currState);

			// for every stackState discovered so far, add (currState,
			// stackState) to the those to be visited for creating the returns
			Collection<Pair<Collection<Pair<Integer, Integer>>, Pair<Collection<Pair<Integer, Integer>>, A>>> toVisitPairStateStackStates = new HashSet<Pair<Collection<Pair<Integer, Integer>>, Pair<Collection<Pair<Integer, Integer>>, A>>>();
			for (Pair<Collection<Pair<Integer, Integer>>, A> stackState : reachedStackStates
					.keySet())
				toVisitPairStateStackStates
						.add(new Pair<Collection<Pair<Integer, Integer>>, Pair<Collection<Pair<Integer, Integer>>, A>>(
								currState, stackState));

			// take all the second components of the pairs in currState
			Collection<Integer> secondComp = projectSecondComponents(currState);

			// if any pair has a final state as second component the current
			// state is final
			if (aut.isFinalConfiguration(secondComp))
				deter.finalStates.add(currStateId);

			// INTERNAL out of currState
			ArrayList<Internal> internalMovesFromCS = new ArrayList<Internal>(
					aut.getInternalsFrom(secondComp));

			// Start at 1 to avoid case in which they are all false (we are not
			// building a total SVPA
			for (int i = 1; i < Math.pow(2, internalMovesFromCS.size()); i++) {
				A guard = null;

				Collection<Pair<Integer, Integer>> toState = new HashSet<Pair<Integer, Integer>>();

				for (int bit = 0; bit < internalMovesFromCS.size(); bit++) {
					Internal currMove = internalMovesFromCS.get(bit);

					if (BitVecUtil.get_nth_bit(i, bit) == 1) {
						guard = intersectGuards(guard, currMove.guard, ba);

						for (Pair<Integer, Integer> pair : secondIs(currState,
								currMove.from))
							toState.add(new Pair<Integer, Integer>(pair.first,
									currMove.to));

					} else {
						guard = intersectGuards(guard,
								ba.MkNot(currMove.guard), ba);
					}
				}

				// If guard satisfiable add move to deterministic version
				if (ba.IsSatisfiable(guard)) {
					Integer toStateId = reachedStates.get(toState);
					if (toStateId == null) {
						toStateId = reachedStates.size();
						reachedStates.put(toState, toStateId);
						toVisitStates.add(toState);
					}
					deter.addTransition(new Internal(currStateId,
							toStateId, guard), ba, true);
				}
			}

			// RETURNBS out of currState
			ArrayList<ReturnBS> returnBSMovesFromCS = new ArrayList<ReturnBS>(
					aut.getReturnBSFrom(secondComp));

			// Start at 1 to avoid case in which they are all false
			for (int i = 1; i < Math.pow(2, returnBSMovesFromCS.size()); i++) {
				A guard = null;

				Collection<Pair<Integer, Integer>> toState = new HashSet<Pair<Integer, Integer>>();

				for (int bit = 0; bit < returnBSMovesFromCS.size(); bit++) {
					ReturnBS currMove = returnBSMovesFromCS.get(bit);

					if (BitVecUtil.get_nth_bit(i, bit) == 1) {
						guard = intersectGuards(guard, currMove.guard, ba);

						for (Pair<Integer, Integer> pair : secondIs(currState,
								currMove.from))
							toState.add(new Pair<Integer, Integer>(pair.first,
									currMove.to));

					} else {
						guard = intersectGuards(guard,
								ba.MkNot(currMove.guard), ba);
					}
				}

				// If guard satisfiable add move to deterministic version
				if (ba.IsSatisfiable(guard)) {
					Integer toStateId = reachedStates.get(toState);
					if (toStateId == null) {
						toStateId = reachedStates.size();
						reachedStates.put(toState, toStateId);
						toVisitStates.add(toState);
					}
					deter.addTransition(new ReturnBS(currStateId,
							toStateId, guard), ba, true);
				}
			}

			// CALLS out of currState
			ArrayList<Call> callsFromCurrState = new ArrayList<Call>(
					aut.getCallsFrom(secondComp));

			// Start at 1 to avoid case in which they are all false
			for (int i = 1; i < Math.pow(2, callsFromCurrState.size()); i++) {
				A a = null;

				// delta_C(S,a)=(S',(S,a)) where
				// S'={(q'',q'') | (q,q') in S and delta_c(q',a)=q'',p}

				// Compute the guard of new move and target state
				Collection<Pair<Integer, Integer>> sPrime = new HashSet<Pair<Integer, Integer>>();
				for (int bit = 0; bit < callsFromCurrState.size(); bit++) {
					// get the ith call in the list
					Call currMove = callsFromCurrState.get(bit);

					// use the predicate positively if i-th bit of i is 1
					if (BitVecUtil.get_nth_bit(i, bit) == 1) {
						a = intersectGuards(a, currMove.guard, ba);

						sPrime.add(new Pair<Integer, Integer>(currMove.to,
								currMove.to));
					} else
						a = intersectGuards(a, ba.MkNot(currMove.guard), ba);
				}

				// If guard satisfiable add move to deterministic version
				if (ba.IsSatisfiable(a)) {

					// Pick the state id
					Integer toStateId = reachedStates.get(sPrime);
					if (toStateId == null) {
						toStateId = reachedStates.size();
						reachedStates.put(sPrime, toStateId);
						toVisitStates.add(sPrime);
					}

					// Add stack states to be visited by returns
					Pair<Collection<Pair<Integer, Integer>>, A> currStackState = new Pair<Collection<Pair<Integer, Integer>>, A>(
							currState, a);

					Integer stackStateId = reachedStackStates
							.get(currStackState);
					if (stackStateId == null) {
						stackStateId = reachedStackStates.size();
						reachedStackStates.put(currStackState, stackStateId);

						// Add new discovered stack states to those to be
						// visited by returns
						for (Collection<Pair<Integer, Integer>> visitedState : previouslyVisited)
							toVisitPairStateStackStates
									.add(new Pair<Collection<Pair<Integer, Integer>>, Pair<Collection<Pair<Integer, Integer>>, A>>(
											visitedState, currStackState));
					}

					deter.addTransition(new Call(currStateId, toStateId,
							stackStateId, a), ba, true);
				}
			}

			// RETURNS out of every pair in to visit PairStateStackStates
			for (Pair<Collection<Pair<Integer, Integer>>, Pair<Collection<Pair<Integer, Integer>>, A>> stPair : toVisitPairStateStackStates) {

				// adding delta_r(S,(S',a),b)
				Collection<Pair<Integer, Integer>> S = stPair.first;
				Pair<Collection<Pair<Integer, Integer>>, A> stackState = stPair.second;
				Collection<Pair<Integer, Integer>> Sprime = stackState.first;
				A a = stackState.second;

				//These transitions are independent from currStateId
				currStateId = reachedStates.get(S);

				// Calls and returns causing the match
				// (q,q'') such that,
				// 1) (q,q') in S',
				// 2) delta_c(q',a)=(q1,p)
				// 3) (q1,q2) in S,
				// 4) delta_r(q2,b,p)=q''

				HashSet<Pair<A, Pair<Call, Return>>> callRetGuardTripletHS = new HashSet<Pair<A, Pair<Call, Return>>>();
				for (Call call : aut
						.getCallsFrom(projectSecondComponents(Sprime))) {
					A callRetGuard = ba.MkAnd(a, call.guard);
					//if I store all the calls in the stack triplet i can avoid this satisfiability check
					if (ba.IsSatisfiable(callRetGuard))
						for (Return ret : aut.getReturnsFrom(
								projectSecondComponents(firstIs(S, call.to)),
								call.stackState))
							if (ba.IsSatisfiable(ba.MkAnd(callRetGuard,
									ret.guard)))
								callRetGuardTripletHS
										.add(new Pair<A, Pair<Call, Return>>(
												ba.MkAnd(call.guard, ret.guard),
												new Pair<Call, Return>(
														call, ret)));
				}

				ArrayList<Pair<A, Pair<Call, Return>>> callRetGuardTriplet = new ArrayList<Pair<A, Pair<Call, Return>>>(callRetGuardTripletHS);

				// Start at 1 to avoid case in which they are all false
				for (int i = 1; i < Math.pow(2, callRetGuardTriplet.size()); i++) {
					A b = a;

					Collection<Pair<Integer, Integer>> toState = new HashSet<Pair<Integer, Integer>>();

					for (int bit = 0; bit < callRetGuardTriplet.size(); bit++) {
						Pair<A, Pair<Call, Return>> currTriplet = callRetGuardTriplet
								.get(bit);

						A callRetGuard = currTriplet.first;
						Call currCall = currTriplet.second.first;
						Return currRet = currTriplet.second.second;

						if (BitVecUtil.get_nth_bit(i, bit) == 1) {

							b = intersectGuards(b, callRetGuard, ba);

							for (Pair<Integer, Integer> fst : secondIs(Sprime,
									currCall.from))
								if (S.contains(new Pair<Integer, Integer>(
										currCall.to, currRet.from)))
									toState.add(new Pair<Integer, Integer>(
											fst.first, currRet.to));
						} else {
							b = intersectGuards(b, ba.MkNot(callRetGuard), ba);
						}
					}

					// If guard satisfiable add move to deterministic
					// version
					if (ba.IsSatisfiable(b)) {

						Integer toStateId = reachedStates.get(toState);
						if (toStateId == null) {
							toStateId = reachedStates.size();
							reachedStates.put(toState, toStateId);
							toVisitStates.add(toState);
						}

						Integer toStackStateId = reachedStackStates
								.get(stackState);

						if (toStackStateId == null)
							System.out.println("shouldn't be null");

						deter.addTransition(new Return(currStateId,
								toStateId, toStackStateId, b), ba, true);
					}
				}

			}

		}

		deter.isDeterministic = true;
		return deter;
	}

	private static  A intersectGuards(A guard, A conjunct,
			BooleanAlgebra ba) throws TimeoutException {
		if (guard == null)
			return conjunct;
		else
			return ba.MkAnd(guard, conjunct);
	}

	@SuppressWarnings("unused")
	private static Collection<Integer> projectFirstComponents(
			Collection<Pair<Integer, Integer>> state) {
		HashSet<Integer> fc = new HashSet<Integer>();
		for (Pair<Integer, Integer> st : state)
			fc.add(st.first);
		return fc;
	}

	private static Collection<Integer> projectSecondComponents(
			Collection<Pair<Integer, Integer>> state) {
		HashSet<Integer> sc = new HashSet<Integer>();
		for (Pair<Integer, Integer> st : state)
			sc.add(st.second);
		return sc;
	}

	private static Collection<Pair<Integer, Integer>> firstIs(
			Collection<Pair<Integer, Integer>> state, Integer fst) {
		HashSet<Pair<Integer, Integer>> sc = new HashSet<Pair<Integer, Integer>>();
		for (Pair<Integer, Integer> st : state)
			if (st.first == fst)
				sc.add(st);
		return sc;
	}

	private static Collection<Pair<Integer, Integer>> secondIs(
			Collection<Pair<Integer, Integer>> state, Integer sec) {
		HashSet<Pair<Integer, Integer>> sc = new HashSet<Pair<Integer, Integer>>();
		for (Pair<Integer, Integer> st : state)
			if (st.second == sec)
				sc.add(st);
		return sc;
	}

	// /////////////////////////////////////////////////////////////////////////////

	// Accessory methods

	@SuppressWarnings("unchecked")
	private static  SVPA removeUnreachableStates(SVPA aut,
			BooleanAlgebra ba) throws TimeoutException {

		Map<Integer, Collection<Integer>> reachRel = aut.getReachRel(ba).fourth;

		SVPA clean = new SVPA();

		HashSet<Integer> fromInitial = new HashSet<Integer>();
		for (Integer state : aut.initialStates)
			fromInitial.addAll(reachRel.get(state));

		if (!aut.isFinalConfiguration(fromInitial))
			return getEmptySVPA(ba);

		// compute states
		for (Integer state : fromInitial) {
			if (clean.maxStateId < state)
				clean.maxStateId = state;

			clean.states.add(state);
			if (aut.isFinalState(state))
				clean.finalStates.add(state);
			if (aut.initialStates.contains(state))
				clean.initialStates.add(state);

		}

		// add transitions
		for (Integer state : clean.states)
			for (SVPAMove t : aut.getTransitionsFrom(state))
				if (clean.states.contains(t.to))
					clean.addTransition((SVPAMove) t.clone(), ba, true);

		clean.stateCount = clean.states.size();

		return clean;
	}

	/**
	 * Checks whether the automaton is deterministic
	 *
	 * @return true iff the automaton is deterministic
	 * @throws TimeoutException
	 */
	public boolean isDeterministic(BooleanAlgebra ba) throws TimeoutException {

		// Check if we set it before
		if (isDeterministic)
			return isDeterministic;

		// check only one initial state
		if (initialStates.size() != 1)
			return false;

		// check only one initial state
		if (!isEpsilonFree)
			return false;

		// Check transitions out of a state are mutually exclusive
		for (Integer state : states) {
			List<SVPAMove> movesFromState = new ArrayList<SVPAMove>(
					getTransitionsFrom(state));

			for (int i = 0; i < movesFromState.size(); i++) {
				SVPAMove t1 = movesFromState.get(i);
				for (int j = i + 1; j < movesFromState.size(); j++)
					if (!t1.isDisjointFrom(movesFromState.get(j), ba))
						return false;
			}
		}

		isDeterministic = true;
		return isDeterministic;
	}

	// Transitions accessors

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Return> getReturnsFrom(Pair<Integer, Integer> state) {
		Collection<Return> trset = returnsFrom.get(state);
		if (trset == null) {
			trset = new HashSet<Return>();
			returnsFrom.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<Return> getReturnsTo(Pair<Integer, Integer> state) {
		Collection<Return> trset = returnsTo.get(state);
		if (trset == null) {
			trset = new HashSet<Return>();
			returnsTo.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Return> getReturnsFrom(Integer state,
			Integer stackState) {
		return getReturnsFrom(new Pair<Integer, Integer>(state, stackState));
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<Return> getReturnsTo(Integer state,
			Integer stackState) {
		return getReturnsTo(new Pair<Integer, Integer>(state, stackState));
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Return> getReturnsFrom(Integer state) {
		Collection<Return> returns = new HashSet<Return>();
		for (Integer ss : stackStates)
			returns.addAll(getReturnsFrom(state, ss));
		return returns;
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<Return> getReturnsTo(Integer state) {
		Collection<Return> returns = new HashSet<Return>();
		for (Integer ss : stackStates)
			returns.addAll(getReturnsTo(state, ss));
		return returns;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Return> getReturnsFrom(Collection<Integer> stateSet) {
		Collection<Return> returns = new HashSet<Return>();
		for (Integer st : stateSet)
			returns.addAll(getReturnsFrom(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions starting in a state in
	 * stateSet with stack state stackState
	 */
	public Collection<Return> getReturnsFrom(
			Collection<Integer> stateSet, Integer stackState) {
		Collection<Return> output = new HashSet<Return>();
		for (Integer st : stateSet)
			output.addAll(getReturnsFrom(st, stackState));

		return output;
	}

	/**
	 * Returns the set of return transitions to a state in stateSet
	 */
	public Collection<Return> getReturnsTo(Collection<Integer> stateSet) {
		Collection<Return> returns = new HashSet<Return>();
		for (Integer st : stateSet)
			returns.addAll(getReturnsTo(st));
		return returns;
	}

	/**
	 * Returns the set of call transitions starting a state state
	 */
	public Collection<Call> getCallsFrom(Integer state) {
		Collection<Call> trset = callsFrom.get(state);
		if (trset == null) {
			trset = new HashSet<Call>();
			callsFrom.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of call transitions starting in state state
	 * with stack state stackState
	 */
	public Collection<Call> getCallsFrom(Integer state, Integer stackState) {
		Collection<Call> trset = callsFrom.get(state);
		if (trset == null) {
			trset = new HashSet<Call>();
			callsFrom.put(state, trset);
		}

		Collection<Call> output = new HashSet<Call>();
		for (Call call : trset)
			if (call.stackState == stackState)
				output.add(call);
		return output;
	}

	/**
	 * Returns the set of call transitions starting in a state in
	 * stateSet with stack state stackState
	 */
	public Collection<Call> getCallsFrom(Collection<Integer> stateSet,
			Integer stackState) {
		Collection<Call> output = new HashSet<Call>();
		for (Integer st : stateSet)
			output.addAll(getCallsFrom(st, stackState));

		return output;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Call> getCallsTo(Integer state) {
		Collection<Call> trset = callsTo.get(state);
		if (trset == null) {
			trset = new HashSet<Call>();
			callsTo.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Call> getCallsFrom(Collection<Integer> stateSet) {
		Collection<Call> returns = new HashSet<Call>();
		for (Integer st : stateSet)
			returns.addAll(getCallsFrom(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<Call> getCallsTo(Collection<Integer> stateSet) {
		Collection<Call> returns = new HashSet<Call>();
		for (Integer st : stateSet)
			returns.addAll(getCallsTo(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<ReturnBS> getReturnBSFrom(Integer state) {
		Collection<ReturnBS> trset = returnBSFrom.get(state);
		if (trset == null) {
			trset = new HashSet<ReturnBS>();
			returnBSFrom.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<ReturnBS> getReturnBSTo(Integer state) {
		Collection<ReturnBS> trset = returnBSTo.get(state);
		if (trset == null) {
			trset = new HashSet<ReturnBS>();
			returnBSTo.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<ReturnBS> getReturnBSFrom(
			Collection<Integer> stateSet) {
		Collection<ReturnBS> returns = new HashSet<ReturnBS>();
		for (Integer st : stateSet)
			returns.addAll(getReturnBSFrom(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<ReturnBS> getReturnBSTo(Collection<Integer> stateSet) {
		Collection<ReturnBS> returns = new HashSet<ReturnBS>();
		for (Integer st : stateSet)
			returns.addAll(getReturnBSTo(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<SVPAEpsilon> getEpsilonsFrom(Integer state) {
		Collection<SVPAEpsilon> trset = epsilonsFrom.get(state);
		if (trset == null) {
			trset = new HashSet<SVPAEpsilon>();
			epsilonsFrom.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<SVPAEpsilon> getEpsilonsTo(Integer state) {
		Collection<SVPAEpsilon> trset = epsilonsTo.get(state);
		if (trset == null) {
			trset = new HashSet<SVPAEpsilon>();
			epsilonsTo.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<SVPAEpsilon> getEpsilonsFrom(
			Collection<Integer> stateSet) {
		Collection<SVPAEpsilon> returns = new HashSet<SVPAEpsilon>();
		for (Integer st : stateSet)
			returns.addAll(getEpsilonsFrom(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<SVPAEpsilon> getEpsilonsTo(Collection<Integer> stateSet) {
		Collection<SVPAEpsilon> returns = new HashSet<SVPAEpsilon>();
		for (Integer st : stateSet)
			returns.addAll(getEpsilonsTo(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Internal> getInternalsFrom(Integer state) {
		Collection<Internal> trset = internalsFrom.get(state);
		if (trset == null) {
			trset = new HashSet<Internal>();
			internalsFrom.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Internal> getInternalsTo(Integer state) {
		Collection<Internal> trset = internalsTo.get(state);
		if (trset == null) {
			trset = new HashSet<Internal>();
			internalsTo.put(state, trset);
		}
		return trset;
	}

	/**
	 * Returns the set of return transitions starting a state s
	 */
	public Collection<Internal> getInternalsFrom(
			Collection<Integer> stateSet) {
		Collection<Internal> returns = new HashSet<Internal>();
		for (Integer st : stateSet)
			returns.addAll(getInternalsFrom(st));
		return returns;
	}

	/**
	 * Returns the set of return transitions to state s
	 */
	public Collection<Internal> getInternalsTo(
			Collection<Integer> stateSet) {
		Collection<Internal> returns = new HashSet<Internal>();
		for (Integer st : stateSet)
			returns.addAll(getInternalsTo(st));
		return returns;
	}

	/**
	 * Returns the set of transitions starting a state s
	 */
	public Collection<SVPAMove> getTransitionsFrom(
			Pair<Integer, Stack<Pair<Integer, S>>> configuration) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();

		Integer state = configuration.first;
		Stack<Pair<Integer, S>> stack = configuration.second;

		transitions.addAll(getCallsFrom(state));
		transitions.addAll(getEpsilonsFrom(state));
		transitions.addAll(getInternalsFrom(state));
		transitions.addAll(getReturnBSFrom(state));

		if (stack.size() > 0) {
			Pair<Integer, S> stackTop = stack.peek();
			transitions.addAll(getReturnsFrom(state, stackTop.first));
		}
		return transitions;
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitionsFrom(
			HashSet<Pair<Integer, Stack<Pair<Integer, S>>>> configurationSet) {
		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();

		for (Pair<Integer, Stack<Pair<Integer, S>>> configuration : configurationSet)
			transitions.addAll(getTransitionsFrom(configuration));
		return transitions;
	}

	/**
	 * Returns the set of transitions starting a state s
	 */
	public Collection<SVPAMove> getTransitionsTo(
			Pair<Integer, Stack<Pair<Integer, S>>> configuration) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();

		Integer state = configuration.first;
		Stack<Pair<Integer, S>> stack = configuration.second;

		transitions.addAll(getCallsTo(state));
		transitions.addAll(getEpsilonsTo(state));
		transitions.addAll(getInternalsTo(state));

		if (stack.size() > 0) {
			Pair<Integer, S> stackTop = stack.peek();
			transitions.addAll(getReturnsTo(state, stackTop.first));
		} else {
			transitions.addAll(getReturnBSTo(state));
		}
		return transitions;
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitionsTo(
			Collection<Integer> stateSet) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();
		for (Integer state : stateSet)
			transitions.addAll(getTransitionsTo(state));

		return transitions;
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitionsTo(Integer state) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();

		transitions.addAll(getEpsilonsTo(state));
		transitions.addAll(getInternalsTo(state));
		transitions.addAll(getCallsTo(state));
		transitions.addAll(getReturnBSTo(state));
		transitions.addAll(getReturnsTo(state));

		return transitions;
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitionsTo(
			HashSet<Pair<Integer, Stack<Pair<Integer, S>>>> configurationSet) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();
		for (Pair<Integer, Stack<Pair<Integer, S>>> configuration : configurationSet)
			transitions.addAll(getTransitionsTo(configuration));
		return transitions;
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitionsFrom(
			Collection<Integer> stateSet) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();
		for (Integer state : stateSet)
			transitions.addAll(getTransitionsFrom(state));

		return transitions;
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitions() {
		return getTransitionsFrom(states);
	}

	/**
	 * Returns the set of transitions starting set of states
	 */
	public Collection<SVPAMove> getTransitionsFrom(Integer state) {

		Collection<SVPAMove> transitions = new LinkedList<SVPAMove>();

		transitions.addAll(getEpsilonsFrom(state));
		transitions.addAll(getInternalsFrom(state));
		transitions.addAll(getCallsFrom(state));
		transitions.addAll(getReturnBSFrom(state));
		transitions.addAll(getReturnsFrom(state));

		return transitions;
	}

	private boolean isFinalConfiguration(Collection<Integer> conf) {
		for (Integer state : conf)
			if (isFinalState(state))
				return true;
		return false;
	}

	private boolean isFinalState(Integer state) {
		return finalStates.contains(state);
	}

	/**
	 * Add Transition
	 * @throws TimeoutException
	 */
	private void addTransition(SVPAMove transition,
			BooleanAlgebra ba, boolean skipSatCheck) throws TimeoutException {

		if (transition.isEpsilonTransition()) {
			if (transition.to == transition.from)
				return;
			isEpsilonFree = false;
		}

		if (skipSatCheck || transition.isSatisfiable(ba)) {

			transitionCount++;

			states.add(transition.from);
			if (maxStateId < transition.from)
				maxStateId = transition.from;
			states.add(transition.to);
			if (maxStateId < transition.to)
				maxStateId = transition.to;

			switch (transition.type) {
			case Call: {

				Call ct = (Call) transition;
				stackStates.add(ct.stackState);
				if (maxStackStateId < ct.stackState)
					maxStackStateId = ct.stackState;

				getCallsFrom(transition.from).add(ct);
				getCallsTo(transition.to).add(ct);
				break;
			}

			case Return: {
				Return ct = (Return) transition;
				stackStates.add(ct.stackState);
				if (maxStackStateId < ct.stackState)
					maxStackStateId = ct.stackState;

				getReturnsFrom(ct.from, ct.stackState).add(ct);
				getReturnsTo(ct.to, ct.stackState).add(ct);
				break;
			}

			case Internal: {
				Internal ct = (Internal) transition;
				getInternalsFrom(transition.from).add(ct);
				getInternalsTo(transition.to).add(ct);
				break;
			}
			case Epsilon: {
				SVPAEpsilon ct = (SVPAEpsilon) transition;
				getEpsilonsFrom(transition.from).add(ct);
				getEpsilonsTo(transition.to).add(ct);
				break;
			}
			case ReturnBS: {
				ReturnBS ct = (ReturnBS) transition;
				getReturnBSFrom(transition.from).add(ct);
				getReturnBSTo(transition.to).add(ct);
				break;
			}
			}
		}
	}

	@Override
	public Collection<SVPAMove> getMovesFrom(Integer state) {
		Collection<SVPAMove> moves = new LinkedList<SVPAMove>();
		moves.addAll(getTransitionsFrom(state));
		return moves;
	}

	@Override
	public Collection<SVPAMove> getMovesTo(Integer state) {
		Collection<SVPAMove> moves = new LinkedList<SVPAMove>();
		moves.addAll(getTransitionsTo(state));
		return moves;
	}

	@Override
	public Collection<Integer> getStates() {
		return states;
	}

	@Override
	public Collection<Integer> getInitialStates() {
		return initialStates;
	}

	@Override
	public Collection<Integer> getFinalStates() {
		return finalStates;
	}

	@Override
	public Object clone() {
		SVPA cl = new SVPA();

		cl.isDeterministic = isDeterministic;
		cl.isTotal = isTotal;
		cl.isEmpty = isEmpty;
		cl.isEpsilonFree = isEpsilonFree;

		cl.stateCount = stateCount;
		cl.maxStateId = maxStateId;
		cl.maxStackStateId = maxStackStateId;
		cl.transitionCount = transitionCount;

		cl.states = new HashSet<Integer>(states);
		cl.stackStates = new HashSet<Integer>(stackStates);
		cl.initialStates = new HashSet<Integer>(initialStates);
		cl.finalStates = new HashSet<Integer>(finalStates);

		cl.internalsFrom = new HashMap<Integer, Collection<Internal>>(
				internalsFrom);
		cl.internalsTo = new HashMap<Integer, Collection<Internal>>(
				internalsTo);
		cl.epsilonsFrom = new HashMap<Integer, Collection<SVPAEpsilon>>(
				epsilonsFrom);
		cl.epsilonsTo = new HashMap<Integer, Collection<SVPAEpsilon>>(
				epsilonsTo);
		cl.callsFrom = new HashMap<Integer, Collection<Call>>(callsFrom);
		cl.callsTo = new HashMap<Integer, Collection<Call>>(callsTo);
		cl.returnsFrom = new HashMap<Pair<Integer, Integer>, Collection<Return>>(
				returnsFrom);
		cl.returnsTo = new HashMap<Pair<Integer, Integer>, Collection<Return>>(
				returnsTo);
		cl.returnBSFrom = new HashMap<Integer, Collection<ReturnBS>>(
				returnBSFrom);
		cl.returnBSTo = new HashMap<Integer, Collection<ReturnBS>>(
				returnBSTo);

		return cl;
	}

}


text:
{:W('SendWeibo',array('title'=>L('PUBLIC_SENTWEIBO'),'post_event'=>'post_feed_box','initHtml'=>$initHtml,'prompt'=>'发布成功'))}

<script type="text/javascript">
var boxmodule = function() {
	M(document.getElementById('tsbox'));
};

if("undefined" == typeof(loadmore) || loadmore == 0) {
	var loadmore = '0';
	var loadnew = '0';
	core.loadFile(THEME_URL+'/js/module.weibo.js',boxmodule);
} else {
	boxmodule();
}
</script>

redpajama_set_name: RedPajamaGithub


text:
from sklearn.pipeline import Pipeline
from sklearn.preprocessing import FunctionTransformer
import numpy as np
import scipy.sparse as sparse

def select_random_features(X, sample_size = 0.9, random_state= None):
	if random_state is None:
		rg = np.random.RandomState()
	elif type(random_state) is int:
		rg = np.random.RandomState(seed = random_state)
	else:
		rg = random_state
	p = X.shape[1]
	k = int(sample_size*p)
	#print (k)
	seq = rg.choice(p, k)
	#print (seq)
	if sparse.issparse(X):
		return X.tocsc()[:, seq]
	else:
		return X[:, seq]

from sklearn.preprocessing import FunctionTransformer

rg = np.random.RandomState(seed=42)
selector = FunctionTransformer(lambda x: select_random_features(x, sample_size=0.9, random_state=rg), accept_sparse=True)

def random_features_clfs(clf, n_estimators= 5, sample_size=0.9, random_state= None):
	if random_state is None:
		random_state = 0
	clfs = []
	for i in range(n_estimators):
		clfs.append(
			Pipeline([('random_selector', FunctionTransformer(lambda x: select_random_features(x
									, sample_size=sample_size
									, random_state=random_state+i))),
                    ('clf', clf) ])
			)
	return clfs


text:
package price

import (
	"net/http"

	stripe "github.com/stripe/stripe-go/v74"
	"github.com/stripe/stripe-go/v74/form"
)

// Client is used to invoke /prices APIs.
type Client struct {
	B   stripe.Backend
	Key string
}

// New creates a new price.
func New(params *stripe.PriceParams) (*stripe.Price, error) {
	return getC().New(params)
}

// New creates a new price.
func (c Client) New(params *stripe.PriceParams) (*stripe.Price, error) {
	price := &stripe.Price{}
	err := c.B.Call(http.MethodPost, "/v1/prices", c.Key, params, price)
	return price, err
}

// Get returns the details of a price.
func Get(id string, params *stripe.PriceParams) (*stripe.Price, error) {
	return getC().Get(id, params)
}

// Get returns the details of a price.
func (c Client) Get(id string, params *stripe.PriceParams) (*stripe.Price, error) {
	path := stripe.FormatURLPath("/v1/prices/%s", id)
	price := &stripe.Price{}
	err := c.B.Call(http.MethodGet, path, c.Key, params, price)
	return price, err
}

// Update updates a price's properties.
func Update(id string, params *stripe.PriceParams) (*stripe.Price, error) {
	return getC().Update(id, params)
}

// Update updates a price's properties.
func (c Client) Update(id string, params *stripe.PriceParams) (*stripe.Price, error) {
	path := stripe.FormatURLPath("/v1/prices/%s", id)
	price := &stripe.Price{}
	err := c.B.Call(http.MethodPost, path, c.Key, params, price)
	return price, err
}

// List returns a list of prices.
func List(params *stripe.PriceListParams) *Iter {
	return getC().List(params)
}

// List returns a list of prices.
func (c Client) List(listParams *stripe.PriceListParams) *Iter {
	return &Iter{
		Iter: stripe.GetIter(listParams, func(p *stripe.Params, b *form.Values) ([]interface{}, stripe.ListContainer, error) {
			list := &stripe.PriceList{}
			err := c.B.CallRaw(http.MethodGet, "/v1/prices", c.Key, b, p, list)

			ret := make([]interface{}, len(list.Data))
			for i, v := range list.Data {
				ret[i] = v
			}

			return ret, list, err
		}),
	}
}

// Iter is an iterator for prices.
type Iter struct {
	*stripe.Iter
}

// Price returns the price which the iterator is currently pointing to.
func (i *Iter) Price() *stripe.Price {
	return i.Current().(*stripe.Price)
}

// PriceList returns the current list object which the iterator is
// currently using. List objects will change as new API calls are made to
// continue pagination.
func (i *Iter) PriceList() *stripe.PriceList {
	return i.List().(*stripe.PriceList)
}

// Search returns a search result containing prices.
func Search(params *stripe.PriceSearchParams) *SearchIter {
	return getC().Search(params)
}

// Search returns a search result containing prices.
func (c Client) Search(params *stripe.PriceSearchParams) *SearchIter {
	return &SearchIter{
		SearchIter: stripe.GetSearchIter(params, func(p *stripe.Params, b *form.Values) ([]interface{}, stripe.SearchContainer, error) {
			list := &stripe.PriceSearchResult{}
			err := c.B.CallRaw(http.MethodGet, "/v1/prices/search", c.Key, b, p, list)

			ret := make([]interface{}, len(list.Data))
			for i, v := range list.Data {
				ret[i] = v
			}

			return ret, list, err
		}),
	}
}

// SearchIter is an iterator for prices.
type SearchIter struct {
	*stripe.SearchIter
}

// Price returns the price which the iterator is currently pointing to.
func (i *SearchIter) Price() *stripe.Price {
	return i.Current().(*stripe.Price)
}

// PriceSearchResult returns the current list object which the iterator is
// currently using. List objects will change as new API calls are made to
// continue pagination.
func (i *SearchIter) PriceSearchResult() *stripe.PriceSearchResult {
	return i.SearchResult().(*stripe.PriceSearchResult)
}

func getC() Client {
	return Client{stripe.GetBackend(stripe.APIBackend), stripe.Key}
}


text:
var App, Server,
  hasProp = {}.hasOwnProperty;

Server = class Server {
  constructor() {}

  init(app) {
    var channels;
    this.channels = channels = {
      general: {
        history: [
          {
            author: 'Welcome',
            message: 'Welcome to #general channel'
          }
        ]
      }
    };
    return this.api = new Reqs({
      events: {
        syncPing: function(time) {
          var now;
          now = Date.now();
          return this.methods.pong(now - time, now);
        },
        asyncPing: function(time) {
          var now;
          now = Date.now();
          // throw new Error 'Some error'
          return [now - time, now];
        },
        message: function(channel, author, message) {
          var c;
          c = channels[channel];
          if (c) {
            c.history.push({
              author: author,
              message: message
            });
            return this.methods.message(channel, author, message);
          }
        },
        createChannel: function(channel) {
          var c, history;
          c = channels[channel];
          if (c) {
            return this.sendError('Channel already exists', 422, 'test id');
          } else {
            history = [
              {
                author: 'Welcome',
                message: `Welcome to #${channel} channel`
              }
            ];
            channels[channel] = {history};
            return this.methods.channelCreated(channel, history);
          }
        },
        history: function(cb) {
          if (cb) {
            return cb(channels);
          }
        },
        channelHistory: function(channel, cb) {
          var c;
          c = channels[channel];
          if (c && cb) {
            return cb(c.history);
          }
        }
      },
      methods: ['pong', 'message', 'channelCreated'],
      send: function(data) {
        console.log('<== RECEIVE local:', data);
        app.api.parse(data);
      },
      // coder:
      //     name: 'Coder'
      //     arguments: ['example key']
      key: 'example key',
      mode: 'sync' // By default all methods are sync
    });
  }

};

App = class App {
  constructor($1) {
    this.$ = $1;
    this.server = 'local';
    this.channels = {};
    this.$.send.click((e) => {
      var msg;
      msg = this.$.textbox.val();
      if (msg.length === 0) {
        return;
      }
      this.api.methods.message(this.selectedChannel, this.$.nickname.val(), msg);
      return this.$.textbox.val('');
    });
    this.$.createChannel.click((e) => {
      var name;
      name = this.$.channelName.val();
      if (name.length === 0) {
        return;
      }
      this.api.methods.createChannel(name);
      return this.$.channelName.val('');
    });
    this.$.server.change((e) => {
      this.server = this.$.server.val();
      if (this.server === 'ws') {
        return this.wsConnect();
      } else {
        return this.connect();
      }
    });
  }

  init(srv) {
    var app;
    app = this;
    this.api = new Reqs({
      events: {
        pong: function(t1, time) {
          var t2;
          t2 = Date.now() - time;
          return console.log(`Event: 'Pong'. Ping ${t1} + ${t2} = ${t1 + t2}`);
        },
        message: (channel, author, msg) => {
          // console.log "New message: <##{channel} [#{author}]: #{msg}>"
          return app.message(channel, author, msg);
        },
        channelCreated: function(channel, history) {
          return app.addChannel(channel, history);
        }
      },
      methods: [
        {
          cbPing: function() {
            return [
              Date.now(),
              function(t1,
              time) {
                var t2;
                t2 = Date.now() - time;
                return console.log(`Ping with callback result: ping ${t1} + ${t2} = ${t1 + t2}`);
              }
            ];
          },
          syncPing: {
            method: function() {
              return [Date.now()]; // Return array with arguments for method. Return result of 'send' function
            }
          },
          asyncPing: {
            mode: 'async',
            method: function() {
              return [Date.now()]; // Return array with arguments for method. Return promise.
            },
            // Optional function for promise.then() method
            then: function(result) {
              var t1,
        t2,
        time;
              t1 = result[0];
              time = result[1];
              t2 = Date.now() - time;
              return console.log(`asyncPing result: ${t1} + ${t2} = ${t1 + t2}`);
            },
            // Optional function for promise.catch() method
            catch: function(err) {
              return console.error('asyncPing error:',
        err);
            }
          },
          longMethodA: {
            mode: 'async',
            method: function() {
              console.log('Long method A started');
              return [];
            },
            then: function(result) {
              return console.log('Long method A result:',
        result);
            },
            catch: function(err) {
              return console.error('Long method A error:',
        err);
            }
          },
          longMethodB: function() {
            console.log('Long method B started');
            return [
              function(result) {
                return console.log('Long method B result:',
              result);
              }
            ];
          },
          // Example use:
          // app.api.methods.asyncPing()
          //   .then(function(result) {
          //       var t1 = result[0], time = result[1], t2 = Date.now()-time;
          //       console.log(`asyncPing result: ${t1} + ${t2} = ${t1 + t2}`);
          //   }).catch(function(err) { console.error('asyncPing error:', err) })
          history: function() {
            return [
              function(channels) {
                return app.setHistory(channels);
              }
            ];
          }
        },
        'message',
        'createChannel'
      ],
      send: function(data) { // Function for sending data
        console.log('==> SEND:', data);
        if (app.server === 'ws') {
          // Send data via WebSockets
          if (app.ws && app.ws.readyState === 1) {
            app.ws.send(data);
          }
        } else if (app.server === 'local') {
          // Send data to local server
          srv.api.parse(data);
        }
      },
      // coder:
      //     name: 'Coder'
      //     arguments: ['example key']
      key: 'example key',
      mode: 'sync' // Methods call mode for all methods whithout async/sync flag
    });
    srv.init(this);
    this.connect();
    return this;
  }

  connect() {
    this.api.methods.history();
    return this;
  }

  addChannel(channel, history = []) {
    var $c;
    if (this.channels[channel]) {
      return;
    }
    this.channels[channel] = {
      history: history
    };
    $c = $(`<div class='channel'>#${channel}</div>`);
    $c.click((e) => {
      return this.selectChannel(channel);
    });
    this.$.channels.append($c);
    return this;
  }

  setHistory(channels) {
    var c, name;
    this.$.channels.empty();
    this.channels = {};
    this.selectedChannel = null;
    for (name in channels) {
      if (!hasProp.call(channels, name)) continue;
      c = channels[name];
      this.addChannel(name, c.history);
      if (this.selectedChannel === null) {
        this.selectChannel(name);
      }
    }
    return this;
  }

  selectChannel(channel) {
    var c, i, len, m, msgs, ref;
    this.selectedChannel = channel;
    this.$.messages.empty();
    c = this.channels[channel];
    msgs = [];
    ref = c.history;
    for (i = 0, len = ref.length; i < len; i++) {
      m = ref[i];
      msgs.push(this.createMessage(m.author, m.message));
    }
    this.$.messages.html(msgs);
    return this;
  }

  createMessage(author, message) {
    return $(`<div class='message'>[<span class='author'>${author}</span>]: <span class='text'>${message}</span></div>`);
  }

  message(channel, author, message) {
    if (!this.channels[channel]) {
      this.addChannel(channel);
    }
    this.channels[channel].history.push({
      author: author,
      message: message
    });
    if (this.selectedChannel === channel) {
      this.$.messages.append(this.createMessage(author, message));
    }
    return this;
  }

  wsConnect() {
    var app, port;
    app = this;
    port = 3001;
    console.log('Connecting to WebSockets: ', port);
    if (this.ws) {
      this.ws.close();
    }
    return this.ws = new WS({
      host: 'localhost',
      port: port,
      open: function(e) {
        console.log('WS Connected to:', port);
        app.connect();
      },
      msg: function(e) {
        console.log('<== RECEIVE ws:', e.data);
        app.api.parse(e.data);
      },
      error: function(e) {
        console.error('WS connection error', e);
      },
      close: function(e) {
        delete app.session;
      }
    });
  }

};

$(function() {
  var srv;
  srv = window.SRV = new Server();
  return window.APP = new App({
    channels: $('.channels'),
    messages: $('.messages'),
    textbox: $('.textbox'),
    send: $('.send'),
    nickname: $('.nickname'),
    channelName: $('.channelName'),
    createChannel: $('.createChannel'),
    server: $('.server'),
    useHttpApi: $('#useHttpApi')
  }).init(srv);
});

// r = new Reqs(

//     send:
//         ws: (data) ->
//         ajax: (data) ->
// )

//# sourceMappingURL=client.js.map


text:
package eu.smartenit.unada.db.dao;

import java.util.Iterator;
import java.util.List;

import org.skife.jdbi.v2.sqlobject.Bind;
import org.skife.jdbi.v2.sqlobject.SqlBatch;
import org.skife.jdbi.v2.sqlobject.SqlQuery;
import org.skife.jdbi.v2.sqlobject.SqlUpdate;
import org.skife.jdbi.v2.sqlobject.customizers.BatchChunkSize;
import org.skife.jdbi.v2.sqlobject.customizers.Mapper;

import eu.smartenit.unada.db.dao.binders.BindVideoInfo;
import eu.smartenit.unada.db.dao.mappers.VideoInfoMapper;
import eu.smartenit.unada.db.dto.VideoInfo;

/**
 * The AbstractVideoInfoDAO class.
 *
 * @authors George Petropoulos
 * @version 2.0
 *
 */
public abstract class AbstractVideoInfoDAO {

	@SqlUpdate("CREATE TABLE IF NOT EXISTS videoinfo  "
			+ "(contentid BIGINT PRIMARY KEY, "
			+ "viewsnumber BIGINT, "
			+ "publishdate BIGINT)")
	public abstract void createTable();

	@SqlUpdate("DROP TABLE IF EXISTS videoinfo")
	public abstract void deleteTable();

	@SqlUpdate("MERGE INTO videoinfo (contentid, viewsnumber, publishdate) "
			+ "VALUES (:v.contentid, :v.viewsnumber, :v.publishdate)")
	public abstract void insert(@BindVideoInfo("v") VideoInfo v);

	@SqlBatch("MERGE INTO videoinfo (contentid, viewsnumber, publishdate) "
			+ "VALUES (:v.contentid, :v.viewsnumber, :v.publishdate)")
	@BatchChunkSize(1000)
	public abstract void insertAll(@BindVideoInfo("v") Iterator<VideoInfo> vList);

	@SqlUpdate("UPDATE videoinfo "
			+ "SET viewsnumber = :v.viewsnumber, "
			+ "publishdate = :v.publishdate "
			+ "WHERE contentid = :v.contentid")
	public abstract void update(@BindVideoInfo("v") VideoInfo v);

	@SqlQuery("SELECT * FROM videoinfo")
	@Mapper(VideoInfoMapper.class)
	public abstract List<VideoInfo> findAll();

	@SqlQuery("SELECT * FROM videoinfo WHERE contentid = :contentid ")
	@Mapper(VideoInfoMapper.class)
	public abstract VideoInfo findById(@Bind("contentid") long contentid);

	@SqlUpdate("DELETE FROM videoinfo")
	public abstract void deleteAll();

	@SqlUpdate("DELETE FROM videoinfo WHERE contentid = :contentid")
	public abstract void delete(@Bind("contentid") long contentid);

}


text:
using namespace std;

#include <boost/iterator/counting_iterator.hpp>

#include <boost/iterator/transform_iterator.hpp>
using namespace boost;

///////////////////////////////////////

void case1()
{
    typedef counting_iterator<int> ci_t;

    vector<int> v;
    std::copy(ci_t(0), ci_t(10), back_inserter(v));

    using std::placeholders::_1;

    auto f = bind(plus<int>(), _1, 5);

    std::copy(
        make_transform_iterator(v.begin(), f),
        make_transform_iterator(v.end(), f),
        ostream_iterator<int>(cout, " "));
}

///////////////////////////////////////

int main()
{
    std::cout << "hello transform_iterator" << std::endl;

    case1();
}


text:
@interface MVJsonValueParser : NSObject

+ (NSString *)stringValueFromObject:(id)obj;
+ (BOOL)boolValueFromObject:(id)obj;
+ (NSInteger)integerValueFromObject:(id)obj;
+ (CGFloat)floatValueFromObject:(id)obj;
+ (NSArray *)arrayValueFromObject:(id)obj withCreateObjectBlock:(MVBaseDataModel *(^)(NSDictionary *dic))createObjectBlock;

@end


text:
export const getListStyles = theme => ({
  display: 'block',
  margin: [0, 0, theme.margin, theme.margin],
  padding: 0,

  '& dl, & ul, & ol': {
    marginBottom: 0
  }
});

export const getULStyles = theme => ({
  marginLeft: theme.margin + theme.padding / 2,

  '& li': {
    display: 'block',
    listStyle: 'none',
    paddingLeft: theme.padding
  },
  '& li:before': {
    position: 'relative',
    left: -(theme.padding / 2),
    display: 'inline-block',
    marginLeft: -theme.padding,
    content: '">>"',
    color: theme.color.primary.light
  }
});

export const getOLStyles = theme => ({
  marginLeft: theme.padding,
  paddingLeft: theme.typography.fontSize,

  '& ol': {
    marginLeft: 0
  }
});

export const getDLStyles = theme => ({
  '& dt': {
    fontStyle: 'italic',
    fontWeight: 'bold'
  },
  '& dd': {
    marginLeft: theme.typography.fontSize
  }
});

export default theme => ({
  root: {
    ...getListStyles(theme),
    'ul&': getULStyles(theme),
    'ol&': getOLStyles(theme),
    'dl&': getDLStyles(theme)
  }
});


text:
package ch.trivadis.com.sensors;

import com.pi4j.io.i2c.I2CBus;
import com.pi4j.io.i2c.I2CDevice;
import com.pi4j.io.i2c.I2CFactory;

import java.io.IOException;
import java.nio.ByteBuffer;

/**
 * Core class to work with the GrovePi board.
 *
 * Use this class together with the {@link GroveSensors} class to create
 * instances for the sensors connected to your GrovePi:
 *
 * <pre>
 * GrovePi grovePi = new GrovePi();
 * GroveSensors sensors = new GroveSensors(grovePi);
 * Ultrasonic ultrasonic = sensors.createUltrasonic(4);
 * Button button = sensors.createButton(3);
 * </pre>
 *
 * @author Johannes Bergmann
 */
public class GrovePi {

	// Arduino I2C Address
	private static final byte ADDRESS = 0x04;

	private static final int DIGITAL_READ_COMMAND = 1;
	private static final int DIGITAL_WRITE_COMMAND = 2;

	private static final byte PIN_MODE_COMMAND = 5;
	private static final byte PIN_MODE_OUTPUT = 1;
	private static final byte PIN_MODE_INPUT = 0;

	private static final byte RTC_GET_TIME_COMMAND = 30;

	private static final byte UNUSED = 0;

	private final I2CDevice device;

	public GrovePi() throws IOException {
		final I2CBus bus = I2CFactory.getInstance(I2CBus.BUS_1);
		device = bus.getDevice(GrovePi.ADDRESS);
	}

	// --- Factory methods for creating different kinds of pin implementations

	// --- Other operations

	public byte[] getRtcTime() throws IOException {

		writeI2c(RTC_GET_TIME_COMMAND, UNUSED, UNUSED, UNUSED);
		sleep(100);
		return readI2c(4);
	}

	public DigitalInputPin createDigitalInputPin(int pin) throws IOException {
		return new DigitalInputPin(this, pin);
	}

	public DigitalOutputPin createDigitalOutputPin(int pin) throws IOException {
		return new DigitalOutputPin(this, pin);
	}

	public I2cPin createI2cPin(int pin) throws IOException {
		return new I2cPin(this, pin);
	}

	// --- Operations used by the pin implementations

	void setPinModeInput(int pin) throws IOException {
		setPinMode(pin, PIN_MODE_INPUT);
	}

	void setPinModeOutput(int pin) throws IOException {
		setPinMode(pin, PIN_MODE_OUTPUT);
	}

	private void setPinMode(int pin, int pinModeInputOrOutput)
			throws IOException {
		writeI2c(PIN_MODE_COMMAND, pin, pinModeInputOrOutput, UNUSED);
	}

	int digitalRead(int pin) throws IOException {
		writeI2c(DIGITAL_READ_COMMAND, pin, UNUSED, UNUSED);
		return device.read() & 0xff;
	}

	void digitalWrite(int pin, int value) throws IOException {
		writeI2c(DIGITAL_WRITE_COMMAND, pin, value, UNUSED);
	}

	byte[] readI2c(int numberOfBytes) throws IOException {
		byte[] buffer = new byte[numberOfBytes];
		device.read(1, buffer, 0, buffer.length);
		return buffer;
	}

	void writeI2c(int... bytes) throws IOException {
		// Convert array: int[] to byte[]
		final ByteBuffer byteBuffer = ByteBuffer.allocate(bytes.length);
		for (int i = 0; i < bytes.length; i++) {
			byteBuffer.put((byte) bytes[i]);
		}
		device.write(1, byteBuffer.array(), 0, byteBuffer.limit());
	}

	public static void sleep(int msec) {
		try {
			Thread.sleep(msec);
		} catch (InterruptedException e) {
			throw new IllegalStateException(e);
		}
	}

	/**
	 * Base class for a pin of the GrovePi.
	 *
	 * The implementations support different kinds interactions with this pin
	 * (e.g. reading digital values only with {@link DigitalInputPin}.
	 *
	 * @author Johannes Bergmann
	 */
	protected static class Pin {

		protected final GrovePi grovePi;
		protected final int pin;

		protected Pin(GrovePi grovePi, int pin) throws IOException {
			this.grovePi = grovePi;
			this.pin = pin;
		}
	}
}


text:
from __future__ import (absolute_import, division)

from .utils import get_nodes, NodeTestCase, only_python2, only_python3

from .test_expr import TestExpr
from .test_misc import TestMisc
from .test_stmt import TestStmt
from .test_mod import TestMod
from .test_extra import TestExtra


text:
// Copyright 2015 Cloudera Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
package com.cloudera.impala.util;

import java.util.Arrays;
import java.util.List;

import org.apache.avro.Schema;
import org.apache.hadoop.hive.metastore.api.FieldSchema;
import org.codehaus.jackson.node.IntNode;

import com.cloudera.impala.analysis.ColumnDef;
import com.cloudera.impala.catalog.ArrayType;
import com.cloudera.impala.catalog.Column;
import com.cloudera.impala.catalog.MapType;
import com.cloudera.impala.catalog.ScalarType;
import com.cloudera.impala.catalog.StructField;
import com.cloudera.impala.catalog.StructType;
import com.cloudera.impala.catalog.Table;
import com.cloudera.impala.catalog.Type;
import com.google.common.collect.Lists;

/**
 * Utility class to generate an Impala-compatible Avro Schema from other schemas, e.g.,
 * an Impala table, a list of Impala columns, a list of Hive field schemas, etc.
 *
 * Error behavior: These functions throw an UnsupportedOperationException when failing
 * to generate an Impala-compatible Avro schema, e.g., because of an unknown type or a
 * type not supported by Impala.
 */
public class AvroSchemaConverter {
  // Arbitrarily chosen schema name and record prefix. Note that
  // record names must be unique within an Avro schema.
  private static final String DEFAULT_SCHEMA_NAME = "baseRecord";
  private static final String RECORD_NAME_PREFIX = "record_";

  // Constants for Avro logical types, in particular, for DECIMAL.
  private static final String AVRO_LOGICAL_TYPE = "logicalType";
  private static final String PRECISION_PROP_NAME = "precision";
  private static final String SCALE_PROP_NAME = "scale";
  private static final String AVRO_DECIMAL_TYPE = "decimal";

  // Used to generate unique record names as required by Avro.
  private int recordCounter_ = 0;

  public static Schema convertColumns(
      List<Column> columns, String schemaName) {
    AvroSchemaConverter converter = new AvroSchemaConverter();
    return converter.convertColumnsImpl(columns, schemaName);
  }

  public static Schema convertColumnDefs(
      List<ColumnDef> colDefs, String schemaName) {
    AvroSchemaConverter converter = new AvroSchemaConverter();
    return converter.convertColumnDefsImpl(colDefs, schemaName);
  }

  public static Schema convertFieldSchemas(
      List<FieldSchema> fieldSchemas, String schemaName) {
    AvroSchemaConverter converter = new AvroSchemaConverter();
    return converter.convertFieldSchemasImpl(fieldSchemas, schemaName);
  }

  public static Schema convertTable(Table impalaTable) {
    return convertColumns(impalaTable.getColumns(), impalaTable.getFullName());
  }

  private Schema convertColumnsImpl(List<Column> columns, String schemaName) {
    List<Schema.Field> avroFields = Lists.newArrayList();
    for (Column column: columns) {
      final Schema.Field avroField = new Schema.Field(column.getName(),
          createAvroSchema(column.getType()), column.getComment(), null);
      avroFields.add(avroField);
    }
    return createAvroRecord(avroFields, schemaName);
  }

  private Schema convertColumnDefsImpl(List<ColumnDef> colDefs, String schemaName) {
    List<Schema.Field> avroFields = Lists.newArrayList();
    for (ColumnDef colDef: colDefs) {
      final Schema.Field avroField = new Schema.Field(colDef.getColName(),
          createAvroSchema(colDef.getType()), colDef.getComment(), null);
      avroFields.add(avroField);
    }
    return createAvroRecord(avroFields, schemaName);
  }

  private Schema convertFieldSchemasImpl(
      List<FieldSchema> fieldSchemas, String schemaName) {
    List<Schema.Field> avroFields = Lists.newArrayList();
    for (FieldSchema fs: fieldSchemas) {
      Type impalaType = Type.parseColumnType(fs.getType());
      if (impalaType == null) {
        throw new UnsupportedOperationException(
            fs.getType() + " is not a suppported Impala type");
      }
      final Schema.Field avroField = new Schema.Field(fs.getName(),
          createAvroSchema(impalaType), fs.getComment(), null);
      avroFields.add(avroField);
    }
    return createAvroRecord(avroFields, schemaName);
  }

  private Schema createAvroRecord(List<Schema.Field> avroFields, String schemaName) {
    // Name is a required property for an Avro Record.
    if (schemaName == null || schemaName.isEmpty()) schemaName = DEFAULT_SCHEMA_NAME;
    Schema schema = Schema.createRecord(schemaName, null, null, false);
    schema.setFields(avroFields);
    return schema;
  }

  private Schema createAvroSchema(Type impalaType) {
    Schema schema = null;
    if (impalaType.isScalarType()) {
      schema = createScalarSchema((ScalarType) impalaType);
    } else if (impalaType.isArrayType()) {
      schema = createArraySchema((ArrayType) impalaType);
    } else if (impalaType.isMapType()) {
      schema = createMapSchema((MapType) impalaType);
    } else if (impalaType.isStructType()) {
      schema = createRecordSchema((StructType) impalaType);
    } else {
      throw new UnsupportedOperationException(
          impalaType.toSql() + " cannot be converted to an Avro type");
    }
    // Make the Avro schema nullable.
    Schema nullSchema = Schema.create(Schema.Type.NULL);
    return Schema.createUnion(Arrays.asList(schema, nullSchema));
  }

  private Schema createScalarSchema(ScalarType impalaScalarType) {
    switch (impalaScalarType.getPrimitiveType()) {
      case STRING: return Schema.create(Schema.Type.STRING);
      case CHAR: return Schema.create(Schema.Type.STRING);
      case VARCHAR: return Schema.create(Schema.Type.STRING);
      case TINYINT: return Schema.create(Schema.Type.INT);
      case SMALLINT: return Schema.create(Schema.Type.INT);
      case INT: return Schema.create(Schema.Type.INT);
      case BIGINT: return Schema.create(Schema.Type.LONG);
      case BOOLEAN: return Schema.create(Schema.Type.BOOLEAN);
      case FLOAT: return Schema.create(Schema.Type.FLOAT);
      case DOUBLE: return Schema.create(Schema.Type.DOUBLE);
      case TIMESTAMP: return Schema.create(Schema.Type.STRING);
      case DECIMAL: return createDecimalSchema(impalaScalarType);
      default:
        throw new UnsupportedOperationException(
            impalaScalarType.toSql() + " cannot be converted to an Avro type");
    }
  }

  private Schema createDecimalSchema(ScalarType impalaDecimalType) {
    Schema decimalSchema = Schema.create(Schema.Type.BYTES);
    decimalSchema.addProp(AVRO_LOGICAL_TYPE, AVRO_DECIMAL_TYPE);
    // precision and scale must be integer values
    decimalSchema.addProp(PRECISION_PROP_NAME,
        new IntNode(impalaDecimalType.decimalPrecision()));
    decimalSchema.addProp(SCALE_PROP_NAME,
        new IntNode(impalaDecimalType.decimalScale()));
    return decimalSchema;
  }

  private Schema createArraySchema(ArrayType impalaArrayType) {
    Schema elementSchema = createAvroSchema(impalaArrayType.getItemType());
    return Schema.createArray(elementSchema);
  }

  private Schema createMapSchema(MapType impalaMapType) {
    // Map keys are always STRING according to the Avro spec.
    Schema valueSchema = createAvroSchema(impalaMapType.getValueType());
    return Schema.createMap(valueSchema);
  }

  private Schema createRecordSchema(StructType impalaStructType) {
    List<Schema.Field> schemaFields = Lists.newArrayList();
    for (StructField structField : impalaStructType.getFields()) {
      Schema.Field avroField = new Schema.Field(structField.getName(),
          createAvroSchema(structField.getType()), structField.getComment(), null);
      schemaFields.add(avroField);
    }
    // All Avro records in a table must have the name property.
    Schema structSchema = Schema.createRecord(
        RECORD_NAME_PREFIX + recordCounter_, null, null, false);
    ++recordCounter_;
    structSchema.setFields(schemaFields);
    return structSchema;
  }
}


text:
package msgraph

import "time"

// Journal undocumented
type Journal struct {
	// Entity is the base model of Journal
	Entity
	// Code undocumented
	Code *string `json:"code,omitempty"`
	// DisplayName undocumented
	DisplayName *string `json:"displayName,omitempty"`
	// LastModifiedDateTime undocumented
	LastModifiedDateTime *time.Time `json:"lastModifiedDateTime,omitempty"`
	// BalancingAccountID undocumented
	BalancingAccountID *UUID `json:"balancingAccountId,omitempty"`
	// BalancingAccountNumber undocumented
	BalancingAccountNumber *string `json:"balancingAccountNumber,omitempty"`
	// Account undocumented
	Account *Account `json:"account,omitempty"`
	// JournalLines undocumented
	JournalLines []JournalLine `json:"journalLines,omitempty"`
}

// JournalLine undocumented
type JournalLine struct {
	// Entity is the base model of JournalLine
	Entity
	// JournalDisplayName undocumented
	JournalDisplayName *string `json:"journalDisplayName,omitempty"`
	// LineNumber undocumented
	LineNumber *int `json:"lineNumber,omitempty"`
	// AccountID undocumented
	AccountID *UUID `json:"accountId,omitempty"`
	// AccountNumber undocumented
	AccountNumber *string `json:"accountNumber,omitempty"`
	// PostingDate undocumented
	PostingDate *Date `json:"postingDate,omitempty"`
	// DocumentNumber undocumented
	DocumentNumber *string `json:"documentNumber,omitempty"`
	// ExternalDocumentNumber undocumented
	ExternalDocumentNumber *string `json:"externalDocumentNumber,omitempty"`
	// Amount undocumented
	Amount *int `json:"amount,omitempty"`
	// Description undocumented
	Description *string `json:"description,omitempty"`
	// Comment undocumented
	Comment *string `json:"comment,omitempty"`
	// LastModifiedDateTime undocumented
	LastModifiedDateTime *time.Time `json:"lastModifiedDateTime,omitempty"`
	// Account undocumented
	Account *Account `json:"account,omitempty"`
}


text:
import React from "react";

export default Copy;

function Copy(props) {
  return
{props.children}
;
}


text:
package com.jivesoftware.os.amza.sync.deployable;

import com.jivesoftware.os.amza.sync.api.AmzaSyncPartitionConfig;
import com.jivesoftware.os.amza.sync.api.AmzaSyncPartitionTuple;
import java.util.Map;

/**
 * Created by jonathan.colt on 12/22/16.
 */
public interface AmzaSyncPartitionConfigProvider {

     Map<AmzaSyncPartitionTuple, AmzaSyncPartitionConfig> getAll(String senderName) throws Exception;
}


text:
package me.codeboy.android.cycleviewpager.example.vh;

import android.support.v7.widget.RecyclerView;
import android.view.View;
import android.widget.TextView;

import me.codeboy.android.cycleviewpager.example.R;

/**
 * vh
 * Created by yuedong.lyd on 2017-01-16.
 */
public class Menu extends RecyclerView.ViewHolder {
    public TextView menu;

    public Menu(View itemView) {
        super(itemView);
        menu = (TextView) itemView.findViewById(R.id.menu);
    }
}