/*
 * Copyright (C)  2021
 *
 * This program is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
 */

package logic;

import java.util.HashSet;
import java.util.Set;

import model.TransitionSystem;

/**
 * This class represents a CTL formula that is a conjunction (and) of two formulas.
 * 
 * @author Neena Govindhan
 * @author Jonas Laya
 * @author Jessie Leung
 * @author Paul Sison
 * @author Franck van Breugel
 * @author Anto Nanah Ji
 */
public class And extends Formula {
	private Formula left;
	private Formula right;

	/**
	 * Initializes this CTL formula as the conjunction (and) of the given {@code left} and {@code right} subformulas.
	 * 
	 * @param left the left subformula of this and formula
	 * @param right the right subformula of this and formula
	 */
	public And(Formula left, Formula right) {
		this.left = left;
		this.right = right;
	}

	@Override
	public int hashCode() {
		final int prime = 31;
		return this.left.hashCode() + prime * this.right.hashCode();
	}

	@Override
	public boolean equals(Object object) {
		if (object != null && this.getClass() == object.getClass()) {
			And other = (And) object;
			return this.left.equals(other.left) && this.right.equals(other.right);
		} else {
			return false;
		}
	}

	@Override
	public String toString() {
		return "(" + this.left + " && " + this.right + ")";
	}

	@Override
	public Set<Integer> sat(TransitionSystem system) {
		Set<Integer> leftSat = this.left.sat(system);
		Set<Integer> rightSat = this.right.sat(system);
		
		Set<Integer> sat = new HashSet<Integer>();
		for (int state = 0; state < system.getStates(); state++) {
			if (leftSat.contains(state) && rightSat.contains(state)) {
				sat.add(state);
			}
		}
		return sat;
	}  
}