/*******************************************************************************
 * Copyright (c) 2016 CEA LIST.
 *
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Created on: 27 nov. 2014
 *
 * Contributors:
 *  Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr
 *   - Initial API and implementation
 ******************************************************************************/

#include "TraceChecker.h"

#include <computer/EvaluationEnvironment.h>

#include <fml/expression/AvmCode.h>
#include <fml/expression/BuiltinArray.h>
#include <fml/expression/ExpressionConstructorImpl.h>

#include <fml/runtime/ExecutionConfiguration.h>
#include <fml/runtime/ExecutionContext.h>
#include <fml/runtime/ExecutionData.h>
#include <fml/trace/TracePoint.h>

#include <solver/api/SolverFactory.h>


namespace sep
{


/**
 * TEST
 * TracePoint Nature
 */
bool TraceChecker::isPointNature(const BF & arg,
		ENUM_TRACE_POINT::TRACE_NATURE nature) const
{
	if( arg.is< TracePoint >() )
	{
		return( arg.to_ptr< TracePoint >()->nature == nature );
	}

	return( false );
}


////////////////////////////////////////////////////////////////////////////////
// SAT CHECKING API
////////////////////////////////////////////////////////////////////////////////

bool TraceChecker::isSat(const ExecutionContext & anEC, const BF & arg)
{
	if( arg.is< TracePoint >() )
	{
		if( isSat(anEC, arg.to_ptr< TracePoint >()) )
		{
			return( true );
		}
	}
	else if( arg.is< AvmCode >() )
	{
		return( isSat(anEC, arg.to_ref< AvmCode >()) );
	}

	return( false );
}


bool TraceChecker::isSat(const ExecutionContext & anEC, const AvmCode & aCode)
{
	switch( aCode.getAvmOpCode() )
	{
		case AVM_OPCODE_AND:
		case AVM_OPCODE_STRONG_SYNCHRONOUS:
		case AVM_OPCODE_AND_THEN:
		case AVM_OPCODE_SCHEDULE_AND_THEN:
		{
			AvmCode::const_iterator it = aCode.begin();
			AvmCode::const_iterator endIt = aCode.end();
			for( ; it != endIt ; ++it )
			{
				if( not isSat(anEC, (*it)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_OR:
		case AVM_OPCODE_OR_ELSE:
		case AVM_OPCODE_SCHEDULE_OR_ELSE:
		case AVM_OPCODE_WEAK_SYNCHRONOUS:
		{
			AvmCode::const_iterator it = aCode.begin();
			AvmCode::const_iterator endIt = aCode.end();
			for( ; it != endIt ; ++it )
			{
				if( isSat(anEC, (*it)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_XOR:
		case AVM_OPCODE_EXCLUSIVE:
		{
			avm_size_t passCount = 0;

			AvmCode::const_iterator it = aCode.begin();
			AvmCode::const_iterator endIt = aCode.end();
			for( ; it != endIt ; ++it )
			{
				if( isSat(anEC, (*it)) )
				{
					if( ++passCount > 1 )
					{
						return( false );
					}
				}
			}

			return( passCount == 1 );
		}


		case AVM_OPCODE_NOT:
		{
			return( not isSat(anEC, aCode.first()) );
		}


		case AVM_OPCODE_NAND:
		{
			AvmCode::const_iterator it = aCode.begin();
			AvmCode::const_iterator endIt = aCode.end();
			for( ; it != endIt ; ++it )
			{
				if( not isSat(anEC, (*it)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_NOR:
		{
			AvmCode::const_iterator it = aCode.begin();
			AvmCode::const_iterator endIt = aCode.end();
			for( ; it != endIt ; ++it )
			{
				if( isSat(anEC, (*it)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_XNOR:
		{
			avm_size_t passCount = 0;

			AvmCode::const_iterator it = aCode.begin();
			AvmCode::const_iterator endIt = aCode.end();
			for( ; it != endIt ; ++it )
			{
				if( isSat(anEC, (*it)) )
				{
					if( ++passCount > 1 )
					{
						return( true );
					}
				}
			}

			return( passCount != 1 );
		}

		default:
		{
			return( false );
		}
	}
}


bool TraceChecker::isSat(
		const ExecutionContext & anEC, AVM_OPCODE anOp, const BF & arg)
{
	switch( anOp )
	{
		case AVM_OPCODE_AND:
		case AVM_OPCODE_STRONG_SYNCHRONOUS:
		case AVM_OPCODE_AND_THEN:
		case AVM_OPCODE_SCHEDULE_AND_THEN:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( not isSat(anEC, argArray->at(offset)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_OR:
		case AVM_OPCODE_OR_ELSE:
		case AVM_OPCODE_SCHEDULE_OR_ELSE:
		case AVM_OPCODE_WEAK_SYNCHRONOUS:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( isSat(anEC, argArray->at(offset)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_XOR:
		case AVM_OPCODE_EXCLUSIVE:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			avm_size_t passCount = 0;

			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( isSat(anEC, argArray->at(offset)) )
				{
					if( ++passCount > 1 )
					{
						return( false );
					}
				}
			}

			return( passCount == 1 );
		}


		case AVM_OPCODE_NOT:
		{
			return( not isSat(anEC, arg) );
		}


		case AVM_OPCODE_NAND:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( not isSat(anEC, argArray->at(offset)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_NOR:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( isSat(anEC, argArray->at(offset)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_XNOR:
		{
			avm_size_t passCount = 0;

			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( isSat(anEC, argArray->at(offset)) )
				{
					if( ++passCount > 1 )
					{
						return( true );
					}
				}
			}

			return( passCount != 1 );
		}

		default:
		{
			return( false );
		}
	}
}


bool TraceChecker::isSat(const ExecutionContext & anEC, TracePoint * aTP)
{
AVM_IF_DEBUG_LEVEL_FLAG2( HIGH , PROCESSOR , SOLVING )
	AVM_OS_TRACE << "isSat ? EC:> " << anEC.str_min() << std::endl
			<< "Fired:> " << anEC.getRunnableElementTrace().str() << std::endl
			<< "Trace:> " << anEC.getIOElementTrace().str() << std::endl;
	AVM_OS_TRACE << "Point:>" << str_indent( aTP ) << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG2( HIGH , PROCESSOR , SOLVING )


	switch( aTP->nature )
	{
		case ENUM_TRACE_POINT::TRACE_FORMULA_NATURE:
		case ENUM_TRACE_POINT::TRACE_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_DECISION_NATURE:

		case ENUM_TRACE_POINT::TRACE_PATH_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_PATH_CONDITION_NATURE_LEAF:
		case ENUM_TRACE_POINT::TRACE_PATH_TIMED_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_PATH_TIMED_CONDITION_NATURE_LEAF:

		case ENUM_TRACE_POINT::TRACE_NODE_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_NODE_CONDITION_NATURE_LEAF:
		case ENUM_TRACE_POINT::TRACE_NODE_TIMED_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_NODE_TIMED_CONDITION_NATURE_LEAF:
		{
			return( isSatFormula(anEC, aTP) );
		}

		case ENUM_TRACE_POINT::TRACE_TIME_NATURE:
		{
			if( aTP->op == AVM_OPCODE_ASSIGN_NEWFRESH )
			{
				return( isSatCom(anEC, aTP, anEC.getIOElementTrace()) );
			}
			else
			{
				return( isSatTime(anEC, aTP) );
			}
		}
		case ENUM_TRACE_POINT::TRACE_VARIABLE_NATURE:
		{
			if( aTP->op == AVM_OPCODE_ASSIGN_NEWFRESH )
			{
				return( isSatCom(anEC, aTP, anEC.getIOElementTrace()) );
			}
			else
			{
				return( isSatVariable(anEC, aTP) );
			}
		}

		case ENUM_TRACE_POINT::TRACE_COM_NATURE:
		case ENUM_TRACE_POINT::TRACE_PORT_NATURE:
		case ENUM_TRACE_POINT::TRACE_SIGNAL_NATURE:
		case ENUM_TRACE_POINT::TRACE_MESSAGE_NATURE:
		case ENUM_TRACE_POINT::TRACE_CHANNEL_NATURE:
		{
			return( isSatCom(anEC, aTP, anEC.getIOElementTrace()) );
		}


		case ENUM_TRACE_POINT::TRACE_RUNNABLE_NATURE:
		{
			return( isSatRunnable(anEC, aTP, anEC.getRunnableElementTrace()) );
		}

		case ENUM_TRACE_POINT::TRACE_ROUTINE_NATURE:
		{
			return( isSatRoutine(anEC, aTP, anEC.getRunnableElementTrace()) );
		}

		case ENUM_TRACE_POINT::TRACE_TRANSITION_NATURE:
		{
			return( isSatTransition(anEC, aTP, anEC.getRunnableElementTrace()) );
		}

		case ENUM_TRACE_POINT::TRACE_STATE_NATURE:
		{
			return( isSatState(anEC, aTP, anEC.getRunnableElementTrace()) );
		}

		case ENUM_TRACE_POINT::TRACE_STATEMACHINE_NATURE:
		{
			return( isSatStatemachine(anEC, aTP, anEC.getRunnableElementTrace()) );
		}

		case ENUM_TRACE_POINT::TRACE_MACHINE_NATURE:
		{
			return( isSatMachine(anEC, aTP, anEC.getRunnableElementTrace()) );
		}


		case ENUM_TRACE_POINT::TRACE_COMPOSITE_NATURE:
		{
			return( isSat(anEC, aTP->op, aTP->value) );
		}

		default:
		{
			return( false );
		}
	}
}


bool TraceChecker::isSatFormula(const ExecutionContext & anEC, TracePoint * aTP)
{
	if( ENV.evalFormula(anEC, theLocalExecutableForm, aTP->value) )
	{
		ENV.outVAL = ExpressionConstructorNative::andExpr(
				anEC.refExecutionData().getAllPathCondition(), ENV.outVAL );

		return( SolverFactory::isStrongSatisfiable(theSolverKind, ENV.outVAL) );
	}
	else
	{
		return( false );
	}
}


bool TraceChecker::isSatTime(const ExecutionContext & anEC, TracePoint * aTP)
{
	return( true );
}

bool TraceChecker::isSatVariable(const ExecutionContext & anEC, TracePoint * aTP)
{
	if( aTP->RID.invalid() )
	{
		aTP->updateRID( anEC.refExecutionData() );
	}

	if( ENV.eval(anEC.getAPExecutionData(),
			anEC.refExecutionData().getSystemRID(), aTP->value) )
	{
		const BF & value = ( aTP->RID.valid() )
				? ENV.getRvalue( aTP->RID, aTP->object->to< InstanceOfData >() )
				: ENV.getRvalue( aTP->object->to< InstanceOfData >() );

		switch( aTP->op )
		{
			case AVM_OPCODE_SEQ:
			{
				return( ENV.outVAL.strEQ( value ) );
			}

			case AVM_OPCODE_CHECK_SAT:
			{
				if( ENV.outVAL.isEQ( value ) )
				{
					return( true );
				}

				if( aTP->object->to< InstanceOfData >()->isTypedBoolean() )
				{
					if( ENV.outVAL.isEqualTrue() )
					{
						ENV.outVAL = ExpressionConstructorNative::andExpr(
							value,
							anEC.refExecutionData().getAllPathCondition() );
					}
					else if( ENV.outVAL.isEqualFalse() )
					{
						ENV.outVAL = ExpressionConstructorNative::andExpr(
							ExpressionConstructorNative::notExpr(value),
							anEC.refExecutionData().getAllPathCondition() );
					}
					else
					{
						ENV.outVAL = ExpressionConstructorNative::andExpr(
							ExpressionConstructorNative::eqExpr(ENV.outVAL, value),
							anEC.refExecutionData().getAllPathCondition() );
					}
				}
				else
				{
					ENV.outVAL = ExpressionConstructorNative::andExpr(
						ExpressionConstructorNative::eqExpr(ENV.outVAL, value),
						anEC.refExecutionData().getAllPathCondition() );
				}

				return( SolverFactory::isStrongSatisfiable(
						theSolverKind, ENV.outVAL) );
			}

			case AVM_OPCODE_NOP:
			case AVM_OPCODE_NULL:
			{
				return( true );
			}

			case AVM_OPCODE_EQ:
			case AVM_OPCODE_ASSIGN:
			default:
			{
				return( ENV.outVAL.isEQ( value ) );
			}
		}
	}

	return( false );
}


bool TraceChecker::isSatCom(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTrace.invalid() )
	{
		return( false );
	}
	else if( aTrace.is< ExecutionConfiguration >() )
	{
		ExecutionConfiguration * aConf =
				aTrace.to_ptr< ExecutionConfiguration >();

		if( aConf->getCode().is< AvmCode >() )
		{
			AvmCode * ioCode = aConf->getCode().to_ptr< AvmCode >();

			if( (aTP->object == NULL)
				|| (aTP->object == ioCode->first().raw_pointer()) )
			{
				switch( aTP->op )
				{
					case AVM_OPCODE_INPUT:
					case AVM_OPCODE_INPUT_ENV:
					case AVM_OPCODE_INPUT_FROM:
					case AVM_OPCODE_INPUT_RDV:
					case AVM_OPCODE_INPUT_MULTI_RDV:
					case AVM_OPCODE_INPUT_BUFFER:

					case AVM_OPCODE_OUTPUT:
					case AVM_OPCODE_OUTPUT_ENV:
					case AVM_OPCODE_OUTPUT_TO:
					case AVM_OPCODE_OUTPUT_RDV:
					case AVM_OPCODE_OUTPUT_MULTI_RDV:
					case AVM_OPCODE_OUTPUT_BUFFER:
					{
//						return( ioCode->isOpCode( aTP->op )
//								&& ( (aTP->machine == NULL)
//									|| (not aConf->hasRuntimeID())
//									|| aConf->getRuntimeID().
//											hasAsAncestor(aTP->machine) ) );

						if( ioCode->isOpCode( aTP->op ) )
						{
							if( (aTP->machine != NULL)
								&& aConf->hasRuntimeID() )
							{
								return( aConf->getRuntimeID().
											hasAsAncestor(aTP->machine) );
							}
							return( true );
						}
						return( false );
					}

					case AVM_OPCODE_ASSIGN_NEWFRESH:
					{
						return( ioCode->isOpCode( aTP->op ) );
					}

					case AVM_OPCODE_NULL:
					{
						return( true );
					}

					default:
					{
						return( aTP->op == ioCode->getOptimizedOpCode() );
					}
				}
			}
		}
	}
	else if( aTrace.is< AvmCode >() )
	{
		AvmCode * aCode = aTrace.to_ptr< AvmCode >();

		AvmCode::const_iterator it = aCode->begin();
		AvmCode::const_iterator endCode = aCode->end();
		for( ; it != endCode ; ++it )
		{
			if( isSatCom(anEC, aTP, (*it)) )
			{
				return( true );
			}
		}
	}

	return( false );
}


bool TraceChecker::isSatRunnable(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTrace.invalid() )
	{
		return( false );
	}
	else if( aTrace.is< ExecutionConfiguration >() )
	{
		ExecutionConfiguration * aConf =
				aTrace.to_ptr< ExecutionConfiguration >();

		if( aTP->object != NULL )
		{
			if( aConf->getCode().isnot< AvmProgram >() ||
				(aConf->getCode().to_ptr< AvmProgram >() != aTP->object) )
			{
				return( false );
			}
		}
		else if( aTP->op != AVM_OPCODE_NULL )
		{
			if( aConf->getCode().isnot< Operator >() ||
				aConf->getOperator()->isnotOpCode(aTP->op) )
			{
				return( false );
			}
		}

		RuntimeID aRID = aConf->getRuntimeID();
		while( aRID.valid() && (aRID.getInstance() != aTP->machine) )
		{
			aRID = aRID.getPRID();
		}

		return( aRID.valid() );
	}
	else if( aTrace.is< AvmCode >() )
	{
		AvmCode * aCode = aTrace.to_ptr< AvmCode >();

		AvmCode::const_iterator it = aCode->begin();
		AvmCode::const_iterator endCode = aCode->end();
		for( ; it != endCode ; ++it )
		{
			if( isSatMachine(anEC, aTP, (*it)) )
			{
				return( true );
			}
		}
	}

	return( false );
}


bool TraceChecker::isSatRoutine(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTrace.invalid() )
	{
		return( false );
	}
	else if( aTrace.is< ExecutionConfiguration >() )
	{
		ExecutionConfiguration * aConf =
				aTrace.to_ptr< ExecutionConfiguration >();

		if( aTP->object != NULL )
		{
			if( aConf->getCode().isnot< AvmProgram >() ||
				(aConf->getCode().to_ptr< AvmProgram >() != aTP->object) )
			{
				return( false );
			}
		}
		else if( aTP->op != AVM_OPCODE_NULL )
		{
			if( aConf->getCode().isnot< Operator >() ||
				aConf->getOperator()->isnotOpCode(aTP->op) )
			{
				return( false );
			}
		}

		RuntimeID aRID = aConf->getRuntimeID();
		while( aRID.valid() && (aRID.getInstance() != aTP->machine) )
		{
			aRID = aRID.getPRID();
		}

		return( aRID.valid() );
	}
	else if( aTrace.is< AvmCode >() )
	{
		AvmCode * aCode = aTrace.to_ptr< AvmCode >();

		AvmCode::const_iterator it = aCode->begin();
		AvmCode::const_iterator endCode = aCode->end();
		for( ; it != endCode ; ++it )
		{
			if( isSatMachine(anEC, aTP, (*it)) )
			{
				return( true );
			}
		}
	}

	return( false );
}


bool TraceChecker::isSatTransition(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTrace.invalid() )
	{
		return( false );
	}
	else if( aTrace.is< ExecutionConfiguration >() )
	{
		ExecutionConfiguration * aConf =
				aTrace.to_ptr< ExecutionConfiguration >();

		if( aConf->getCode().is< AvmTransition >() )
		{
			return( aTP->object == aConf->getCode().to_ptr< AvmTransition >() );
		}
	}
	else if( aTrace.is< AvmCode >() )
	{
		AvmCode * aCode = aTrace.to_ptr< AvmCode >();

		AvmCode::const_iterator it = aCode->begin();
		AvmCode::const_iterator endCode = aCode->end();
		for( ; it != endCode ; ++it )
		{
			if( isSatTransition(anEC, aTP, (*it)) )
			{
				return( true );
			}
		}
	}

	return( false );
}


bool TraceChecker::isSatState(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTP->RID.invalid() )
	{
		aTP->updateRID( anEC.refExecutionData() );
	}

	if( aTP->RID.valid() )
	{
		return( anEC.refExecutionData().isIdleOrRunning(aTP->RID) );
	}

	return( isSatMachine(anEC, aTP, aTrace) );
}


bool TraceChecker::isSatStatemachine(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTP->RID.invalid() )
	{
		aTP->updateRID( anEC.refExecutionData() );
	}

	if( aTP->RID.valid() )
	{
		return( anEC.refExecutionData().isIdleOrRunning(aTP->RID) );
	}

	return( isSatMachine(anEC, aTP, aTrace) );
}


bool TraceChecker::isSatMachine(
		const ExecutionContext & anEC, TracePoint * aTP, const BF & aTrace)
{
	if( aTrace.invalid() )
	{
		return( false );
	}
	else if( aTrace.is< ExecutionConfiguration >() )
	{
		ExecutionConfiguration * aConf =
				aTrace.to_ptr< ExecutionConfiguration >();

		if( aConf->getCode().is< Operator >() )
		{
			if( aConf->getCode().to_ptr< Operator >()->
					isOpCode( AVM_OPCODE_RUN ) )
			{
				RuntimeID aRID = aConf->getRuntimeID();
				while( aRID.valid() && (aRID.getInstance() != aTP->object) )
				{
					aRID = aRID.getPRID();
				}
				return( aRID.valid() );
			}
		}
	}
	else if( aTrace.is< AvmCode >() )
	{
		AvmCode * aCode = aTrace.to_ptr< AvmCode >();

		AvmCode::const_iterator it = aCode->begin();
		AvmCode::const_iterator endCode = aCode->end();
		for( ; it != endCode ; ++it )
		{
			if( isSatMachine(anEC, aTP, (*it)) )
			{
				return( true );
			}
		}
	}

	return( false );
}


////////////////////////////////////////////////////////////////////////////////
// WILL NEVER SAT CHECKING API
////////////////////////////////////////////////////////////////////////////////

bool TraceChecker::willNeverSat(const ExecutionContext & anEC, const BF & arg)
{
	if( anEC.isRoot() )
	{
		return( false );
	}

	if( arg.is< TracePoint >() )
	{
		if( willNeverSat(anEC, arg.to_ptr< TracePoint >()) )
		{
			return( true );
		}
	}
	else if( arg.is< AvmCode >() )
	{
		return( willNeverSat(anEC, arg.to_ptr< AvmCode >()) );
	}

	return( false );
}


bool TraceChecker::willNeverSat(const ExecutionContext & anEC, AvmCode * aCode)
{
	switch( aCode->getAvmOpCode() )
	{
		case AVM_OPCODE_AND:
		case AVM_OPCODE_STRONG_SYNCHRONOUS:
		case AVM_OPCODE_AND_THEN:
		case AVM_OPCODE_SCHEDULE_AND_THEN:
		{
			AvmCode::const_iterator it = aCode->begin();
			AvmCode::const_iterator endIt = aCode->end();
			for( ; it != endIt ; ++it )
			{
				if( not willNeverSat(anEC, (*it)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_OR:
		case AVM_OPCODE_OR_ELSE:
		case AVM_OPCODE_SCHEDULE_OR_ELSE:
		case AVM_OPCODE_WEAK_SYNCHRONOUS:
		{
			AvmCode::const_iterator it = aCode->begin();
			AvmCode::const_iterator endIt = aCode->end();
			for( ; it != endIt ; ++it )
			{
				if( willNeverSat(anEC, (*it)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_XOR:
		{
			avm_size_t passCount = 0;

			AvmCode::const_iterator it = aCode->begin();
			AvmCode::const_iterator endIt = aCode->end();
			for( ; it != endIt ; ++it )
			{
				if( willNeverSat(anEC, (*it)) )
				{
					if( ++passCount > 1 )
					{
						return( false );
					}
				}
			}

			return( passCount == 1 );
		}


		case AVM_OPCODE_NOT:
		{
			return( not willNeverSat(anEC, aCode->first()) );
		}


		case AVM_OPCODE_NAND:
		{
			AvmCode::const_iterator it = aCode->begin();
			AvmCode::const_iterator endIt = aCode->end();
			for( ; it != endIt ; ++it )
			{
				if( not willNeverSat(anEC, (*it)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_NOR:
		{
			AvmCode::const_iterator it = aCode->begin();
			AvmCode::const_iterator endIt = aCode->end();
			for( ; it != endIt ; ++it )
			{
				if( willNeverSat(anEC, (*it)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_XNOR:
		{
			avm_size_t passCount = 0;

			AvmCode::const_iterator it = aCode->begin();
			AvmCode::const_iterator endIt = aCode->end();
			for( ; it != endIt ; ++it )
			{
				if( willNeverSat(anEC, (*it)) )
				{
					if( ++passCount > 1 )
					{
						return( true );
					}
				}
			}

			return( passCount != 1 );
		}

		default:
		{
			return( false );
		}
	}
}


bool TraceChecker::willNeverSat(
		const ExecutionContext & anEC, AVM_OPCODE anOp, const BF & arg)
{
	switch( anOp )
	{
		case AVM_OPCODE_AND:
		case AVM_OPCODE_STRONG_SYNCHRONOUS:
		case AVM_OPCODE_AND_THEN:
		case AVM_OPCODE_SCHEDULE_AND_THEN:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( not willNeverSat(anEC, argArray->at(offset)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_OR:
		case AVM_OPCODE_OR_ELSE:
		case AVM_OPCODE_SCHEDULE_OR_ELSE:
		case AVM_OPCODE_WEAK_SYNCHRONOUS:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( willNeverSat(anEC, argArray->at(offset)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_XOR:
		case AVM_OPCODE_EXCLUSIVE:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			avm_size_t passCount = 0;

			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( willNeverSat(anEC, argArray->at(offset)) )
				{
					if( ++passCount > 1 )
					{
						return( false );
					}
				}
			}

			return( passCount == 1 );
		}


		case AVM_OPCODE_NOT:
		{
			return( not willNeverSat(anEC, arg) );
		}


		case AVM_OPCODE_NAND:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( not willNeverSat(anEC, argArray->at(offset)) )
				{
					return( true );
				}
			}

			return( false );
		}

		case AVM_OPCODE_NOR:
		{
			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( willNeverSat(anEC, argArray->at(offset)) )
				{
					return( false );
				}
			}

			return( true );
		}

		case AVM_OPCODE_XNOR:
		{
			avm_size_t passCount = 0;

			ArrayBF * argArray = arg.to_ptr< ArrayBF >();
			avm_size_t endOffset = argArray->size();
			for( avm_size_t offset = 0 ; offset < endOffset ; ++offset )
			{
				if( willNeverSat(anEC, argArray->at(offset)) )
				{
					if( ++passCount > 1 )
					{
						return( true );
					}
				}
			}

			return( passCount != 1 );
		}

		default:
		{
			return( false );
		}
	}
}


bool TraceChecker::willNeverSat(const ExecutionContext & anEC, TracePoint * aTP)
{
AVM_IF_DEBUG_LEVEL_FLAG2( HIGH , PROCESSOR , SOLVING )
	AVM_OS_TRACE << "willNeverSat ? EC:> " << anEC.str_min() << std::endl
			<< "run#trace:> " << anEC.getRunnableElementTrace().str() << std::endl
			<< "io#race  :> " << anEC.getIOElementTrace().str() << std::endl;
	AVM_OS_TRACE << "Point:>" << str_indent( aTP ) << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG2( HIGH , PROCESSOR , SOLVING )


	switch( aTP->nature )
	{
		case ENUM_TRACE_POINT::TRACE_PATH_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_PATH_CONDITION_NATURE_LEAF:
		case ENUM_TRACE_POINT::TRACE_PATH_TIMED_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_PATH_TIMED_CONDITION_NATURE_LEAF:

		case ENUM_TRACE_POINT::TRACE_NODE_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_NODE_CONDITION_NATURE_LEAF:
		case ENUM_TRACE_POINT::TRACE_NODE_TIMED_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_NODE_TIMED_CONDITION_NATURE_LEAF:

		case ENUM_TRACE_POINT::TRACE_FORMULA_NATURE:
		case ENUM_TRACE_POINT::TRACE_CONDITION_NATURE:
		case ENUM_TRACE_POINT::TRACE_DECISION_NATURE:

		case ENUM_TRACE_POINT::TRACE_TIME_NATURE:
		case ENUM_TRACE_POINT::TRACE_VARIABLE_NATURE:
		case ENUM_TRACE_POINT::TRACE_COM_NATURE:
		case ENUM_TRACE_POINT::TRACE_PORT_NATURE:
		case ENUM_TRACE_POINT::TRACE_SIGNAL_NATURE:
		case ENUM_TRACE_POINT::TRACE_MESSAGE_NATURE:
		case ENUM_TRACE_POINT::TRACE_CHANNEL_NATURE:
		{
			return( false );
		}


		case ENUM_TRACE_POINT::TRACE_TRANSITION_NATURE:
		{
			return( willNeverSatTransition(anEC, aTP) );
		}

		case ENUM_TRACE_POINT::TRACE_STATE_NATURE:
		{
			return( willNeverSatState(anEC, aTP) );
		}

		case ENUM_TRACE_POINT::TRACE_STATEMACHINE_NATURE:
		{
			return( willNeverSatStatemachine(anEC, aTP) );
		}

		case ENUM_TRACE_POINT::TRACE_MACHINE_NATURE:
		{
			return( willNeverSatMachine(anEC, aTP) );
		}

		case ENUM_TRACE_POINT::TRACE_COMPOSITE_NATURE:
		{
			return( willNeverSat(anEC, aTP->op, aTP->value) );
		}

		default:
		{
			return( false );
		}
	}
}


bool TraceChecker::willNeverSatTransition(
		const ExecutionContext & anEC, TracePoint * aTP)
{
	ExecutableForm * sourceExecutable =
			aTP->object->as< AvmTransition >()->getExecutableContainer();

	if( not sourceExecutable->hasPossibleDynamicInstanciation() )
	{
		return( false );
	}

	TableOfRuntimeT::const_iterator itRF =
			anEC.refExecutionData().getTableOfRuntime().begin();
	TableOfRuntimeT::const_iterator endRF =
			anEC.refExecutionData().getTableOfRuntime().end();
	for( RuntimeID itRID ; itRF != endRF ; ++itRF )
	{
		itRID = (*itRF)->getRID();

		if( anEC.refExecutionData().isIdleOrRunning(itRID) &&
				itRID.getExecutable()->hasForwardReachableMachine() )
		{
			if( (sourceExecutable == itRID.getExecutable()) ||
				sourceExecutable->getBackwardReachableMachine().
						contains(itRID.getInstance()) )
			{
				return( false );
			}
		}
	}

	return( true );
}

bool TraceChecker::willNeverSatState(
		const ExecutionContext & anEC, TracePoint * aTP)
{
	ExecutableForm * sourceExecutable =
			aTP->object->as< InstanceOfMachine >()->getExecutable();

	if( not sourceExecutable->hasSingleRuntimeInstance() )
	{
		return( false );
	}

	TableOfRuntimeT::const_iterator itRF =
			anEC.refExecutionData().getTableOfRuntime().begin();
	TableOfRuntimeT::const_iterator endRF =
			anEC.refExecutionData().getTableOfRuntime().end();
	for( RuntimeID itRID ; itRF != endRF ; ++itRF )
	{
		itRID = (*itRF)->getRID();

		if( anEC.refExecutionData().isIdleOrRunning(itRID) &&
				itRID.getExecutable()->hasForwardReachableMachine() )
		{
			if( (sourceExecutable == itRID.getExecutable()) ||
				sourceExecutable->getBackwardReachableMachine().
						contains(itRID.getInstance()) )
			{
				return( false );
			}
		}
	}

	return( false );
}


bool TraceChecker::willNeverSatStatemachine(
		const ExecutionContext & anEC, TracePoint * aTP)
{
	return( willNeverSatState(anEC, aTP) );
}


bool TraceChecker::willNeverSatMachine(
		const ExecutionContext & anEC, TracePoint * aTP)
{
	return( willNeverSatState(anEC, aTP) );
}


} /* namespace sep */