/* 
 * Copyright (C) 2017, Rockwell Collins
 * All rights reserved.
 *
 * This software may be modified and distributed under the terms
 * of the 3-clause BSD license.  See the LICENSE file for details.
 * 
 */
package fuzzm.engines.messages;

import fuzzm.engines.EngineName;
import fuzzm.lustre.BooleanCtx;
import fuzzm.lustre.evaluation.FunctionLookupEV;
import fuzzm.solver.SolverResults;
import fuzzm.util.RatSignal;

/**
 * The Counter Example message contains a specific solution to the
 * constraint.
 * 
 * Generated by the Solver Engine.
 * Consumed by the Generalization Engine.
 */
public class CounterExampleMessage extends FeatureMessage {

    public final double time;
    public final RatSignal counterExample;
	public final FunctionLookupEV fns;
	public final BooleanCtx   hyp;
	public final BooleanCtx   prop;
	public final RatSignal generalizationTarget;
	
	public CounterExampleMessage(EngineName source, FeatureID id, String name, BooleanCtx hyp, BooleanCtx  prop, RatSignal generalizationTarget, SolverResults sr, long sequence) {
		super(source,QueueName.CounterExampleMessage,id,name,sequence);
		//assert(target.size() > 0);
		this.counterExample = sr.cex;
		this.fns = sr.fns;
		this.hyp = hyp;
		this.prop = prop;
		this.generalizationTarget = generalizationTarget;
		this.time = sr.time;
	}
	
	public CounterExampleMessage(EngineName source, ConstraintMessage m, SolverResults sr) {
		this(source, m.id,m.name,m.hyp,m.prop,m.generalizationTarget,sr,m.sequence);
	}
	
	@Override
	public void handleAccept(MessageHandler handler) {
		handler.handleMessage(this);
	}
	
	@Override
	public String toString() {
		return "Message: [CeX] " + sequence + ":" + id + " Time = " + time/1000.0 + " s"; // + " :\n" + counterExample.toString();
	}

	@Override
	public int bytes() {
		return 1 + counterExample.bytes();
	}

}
