package logic.ltl;

import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;

import automata.safa.BooleanExpressionFactory;
import automata.safa.SAFA;
import automata.safa.SAFAInputMove;
import automata.safa.booleanexpression.PositiveBooleanExpression;
import theory.BooleanAlgebra;

public class True<P, S> extends LTLFormula<P, S> {

	public True() {
		super();
	}

	@Override
	public int hashCode() {
		return 11;
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (!(obj instanceof True))
			return false;
		return true;
	}

	@Override
	protected PositiveBooleanExpression accumulateSAFAStatesTransitions(
			HashMap<LTLFormula<P, S>, PositiveBooleanExpression> formulaToState, Collection<SAFAInputMove<P, S>> moves,
			Collection<Integer> finalStates, BooleanAlgebra<P, S> ba, HashSet<Integer> states) {
		BooleanExpressionFactory<PositiveBooleanExpression> boolexpr = SAFA.getBooleanExpressionFactory();

		// If I already visited avoid recomputing
		if (formulaToState.containsKey(this))
			return formulaToState.get(this);

		// Update hash tables
		int id = states.size();
		states.add(id);
		PositiveBooleanExpression initialState = boolexpr.MkState(id);
		formulaToState.put(this, initialState);
		
		int id2 = states.size();
		states.add(id2);
		PositiveBooleanExpression toState = boolexpr.MkState(id2);

		// delta(True, true) = True
		moves.add(new SAFAInputMove<>(id, toState, ba.True()));
		moves.add(new SAFAInputMove<>(id2, toState, ba.True()));

		// True is a final state
		finalStates.add(id2);

		return initialState;
	}

	@Override
	protected LTLFormula<P, S> pushNegations(boolean isPositive, BooleanAlgebra<P, S> ba,
			HashMap<String, LTLFormula<P, S>> posHash, HashMap<String, LTLFormula<P, S>> negHash) {
		if (isPositive) {
			return this;
		} else {
			String key = this.toString();
			if (negHash.containsKey(key)) {
				return negHash.get(key);
			} else {
				LTLFormula<P, S> out = new False<>();
				negHash.put(key, out);
				return out;
			}
		}
	}

	@Override
	public void toString(StringBuilder sb) {
		sb.append("true");
	}

	@Override
	public int getSize() {
		return 1;
	}
}

@@ -1305,316 +1305,105 @@
 te);
-%0A
 %09%09%0A
-%09%09int id2 = states.size();%0A%09%09states.add(id2);%0A%09%09PositiveBooleanExpression toState = boolexpr.MkState(id2);%0A%0A%09%09// delta(True, true) = True%0A%09%09moves.add(new SAFAInputMove%3C%3E(id, toState, ba.True()));%0A%09%09moves.add(new SAFAInputMove%3C%3E(id2, toState, ba.True()));%0A%0A%09%09// True is a final state%0A%09%09finalStates.add(id2
+%0A%09%09// delta(True, true) = True%0A%09%09moves.add(new SAFAInputMove%3C%3E(id, boolexpr.True(), ba.True())
 );%0A%0A

simplified True