/*************************************************************************
 * This file is part of the Distributed Computation feature
 *
 * Project created in conformity with the requirements for the Degree of
 * Master of Engineering in Software Engineering, Computing and Software
 * Department, McMaster University 2012
 *
 * Author:	David Kirby
 * Supervisor: Dr. Ryan Leduc
 ************************************************************************/
#include "DistHandler.h"

#ifdef __ENABLE_DIST__

namespace DESpot
{
	DistHandler::DistHandler(DesProject* project):
		m_project(*project)
	{
		// Record the project path in a static string
		wstring fileName = m_project.getFileName();
		projectPath.assign(fileName.begin(), fileName.end());

		// replace any '///' in the path with '/' before encoding the spaces as '///'
		int loc = projectPath.find("///");
		while (loc != string::npos)
		{
			projectPath.replace(loc, 3, "/");
			loc = projectPath.find("///");
		}

		// encode any spaces in the projectPath
		loc = projectPath.find(" ");
		while (loc != string::npos)		
		{
			projectPath.replace(loc, 1, "///");
			loc = projectPath.find(" ");
		} 
	}

//______________________________________________________________________________________________

	DistHandler::~DistHandler()
	{
		CommHandler com = CommHandler(false, -1);
		com.terminateSlaves();
	}

//______________________________________________________________________________________________

	// Return a remoteCheck object containing the result
	void* runNonBlock(void* args)
	{
		// arg[0] = subsystem : -1 = flat system		
		// arg[1] = isBDD : ignored for flat
		// arg[2] = isHighLevel : ignored for flat
		int* par = (int*)args;
				
		if (par[0] < 0)
		{
			// Flat system
			CommHandler com = CommHandler(false, 2);

			stringstream ss;
			ss << projectPath << " " << FlatNB;
			
			remoteCheck* rc = com.sendRecv(ss.str());

			return (void*)rc;
		}
		else // HISC system
		{
			CommHandler com = CommHandler(false, -1);

			// Build string to be sent
			stringstream ss;

			// Add project path
			ss << projectPath << " ";

			// Add command
			// isBDD?
			if (par[1] == 1)
			{
				// BDD
				// isHighLevel?
				ss << (par[2] == 1 ? BDDHighNB : BDDLowNB);
			}
			else
			{
				// not BDD
				// isHighLevel?
				ss << (par[2] == 1 ? HISCHighNB : HISCLowNB);
			}

			// Add subsystem index
			ss << " " << par[0];

			remoteCheck* rc = new remoteCheck;

			if (rc == null)
				throw new EX("Out of memory error");

			rc = com.sendRecv(ss.str());
	
			// update the count of free slots
			pthread_mutex_lock(&distHandlerMutex);
			freeSlots += 1;
			pthread_cond_signal(&distHandlerCond);
			pthread_mutex_unlock(&distHandlerMutex);

			return (void*)rc;
		}
	}

//______________________________________________________________________________________________

	// Return a remoteCheck object containing the result
	void* runCtrl(void* args)
	{
		// arg[0] = subsystem : -1 = flat system
		// arg[1] = isBDD : ignored for flat
		// arg[2] = isHighLevel : ignored for flat
		int* par = (int*)args;
		
		if (par[0] < 0)
		{
			// Flat system
			CommHandler com = CommHandler(false, 2);

			stringstream ss;
			ss << projectPath << " " << FlatCtrl;
			
			remoteCheck* rc = com.sendRecv(ss.str());

			return (void*)rc;
		}
		else // HISC system
		{
			CommHandler com = CommHandler(false, -1);

			// Build string to be sent
			stringstream ss;

			// Add project path
			ss << projectPath << " ";

			// Add command
			// isBDD?
			if (par[1] == 1)
			{
				// BDD
				// isHighLevel?
				ss << (par[2] == 1 ? BDDHighCtrl : BDDLowCtrl);
			}
			else
			{
				// not BDD
				// isHighLevel?
				ss << (par[2] == 1 ? HISCHighCtrl : HISCLowCtrl);
			}

			// Add subsystem index
			ss << " " << par[0];

			remoteCheck* rc = new remoteCheck;

			if (rc == null)
				throw new EX("Out of memory error");

			rc = com.sendRecv(ss.str());

			// update the count of free slots
			pthread_mutex_lock(&distHandlerMutex);
			freeSlots += 1;
			pthread_cond_signal(&distHandlerCond);
			pthread_mutex_unlock(&distHandlerMutex);

			return (void*)rc;
		}
	}

//______________________________________________________________________________________________

	// Return a remoteCheck object containing the result
	void* runIConsist(void* args)
	{
		// arg[0] = subsystem number
		// arg[1] = isBDD
		// arg[2] = isHighLevel
		int* par = (int*)args;
		
		CommHandler com = CommHandler(false, -1);

		// Build string to be sent
		stringstream ss;

		// Add project path
		ss << projectPath << " ";

		// Add command
		// isBDD?
		if (par[1] == 1)
		{
			// BDD
			// isHighLevel?
			ss << (par[2] == 1 ? BDDHighIConsis : BDDLowIConsis);
		}
		else
		{
			// not BDD
			// isHighLevel?
			ss << (par[2] == 1 ? HISCHighInterf : HISCLowInterf);
		}

		// Add subsystem index
		ss << " " << par[0];

		remoteCheck* rc = new remoteCheck;

		if (rc == null)
				throw new EX("Out of memory error");

		rc = com.sendRecv(ss.str());

		// update the count of free slots and signal the main process to spawn another thread (if waiting)
		pthread_mutex_lock(&distHandlerMutex);
		freeSlots += 1;
		pthread_cond_signal(&distHandlerCond);
		pthread_mutex_unlock(&distHandlerMutex);

		return (void*)rc;
	}
//______________________________________________________________________________________________

	// Return a remoteCheck object containing the result
	void* runIValid(void* args)
	{
		// arg[0] = subsystem number
		// arg[1] = isBDD
		int* par = (int*)args;
		
		CommHandler com = CommHandler(false, -1);

		// Build string to be sent
		stringstream ss;

		// Add project path
		ss << projectPath << " ";

		// Add command
		// isBDD?
		ss << (par[1] == 1 ? BDDICheck : HISCInterfLDConsist);

		// Add subsystem index
		ss << " " << par[0];

		remoteCheck* rc = new remoteCheck;

		if (rc == null)
				throw new EX("Out of memory error");

		rc = com.sendRecv(ss.str());

		// update the count of free slots
		pthread_mutex_lock(&distHandlerMutex);
		freeSlots += 1;
		pthread_cond_signal(&distHandlerCond);
		pthread_mutex_unlock(&distHandlerMutex);

		return (void*)rc;
	}

//______________________________________________________________________________________________

	// Return a resultStruct object containing the results
	void* runBDDCheckAll(void* args)
	{
		// arg[0] = subsystem number
		// arg[1] = isBDD
		// arg[2] = isHighLevel
		int* par = (int*)args;

		CommHandler com = CommHandler(false, -1);

		// build the string to be send
		stringstream ss;

		// Add project path
		ss << projectPath << " ";

		// Add command
		// isHighLevel?
		ss << (par[2] == 1 ? BDDHighAll : BDDLowAll);		

		// Add subsystem index
		ss << " " << par[0];

		remoteCheck* rc = new remoteCheck;
		if (rc == null)
				throw new EX("Out of memory error");

		rc = com.sendRecv(ss.str());

		resultStruct* rs = new resultStruct;
		if (rs == null)
			throw new EX("Out of memory error");

		// determine what the outcome was specifically by performing additions.
		// 
		// Result | Meaning
		//    0   | All Pass
		//    1   | NB Failed
		//    2   | Controllable Failed
		//    3   | Interface Consistent Failed
		switch (rc->result)
		{
			case 0:
				rs->NBChecked = 
				rs->ctrlChecked = 
				rs->iConsistChecked = true;			

				rs->nonBlocking = 0;
				rs->controllable = 0;
				rs->iConsistent = 0;

				rs->SucList = DesAlgo::ErrorList();
				while (!rc->errList.empty())
				{	
					rs->SucList.push_back(rc->errList.front());
					rc->errList.pop_front();
				}
				break;
			case 1:
				rs->NBChecked = true;
				rs->ctrlChecked = false;
				rs->iConsistChecked = false;

				rs->nonBlocking = -1;		

				rs->NBList = DesAlgo::ErrorList();
				while (!rc->errList.empty())
				{	
					rs->NBList.push_back(rc->errList.front());
					rc->errList.pop_front();
				}	
				break;

			case 2:
				rs->NBChecked = false;
				rs->ctrlChecked = true;
				rs->iConsistChecked = false;

				rs->controllable = -1;		

				rs->CtrlList = DesAlgo::ErrorList();
				while (!rc->errList.empty())
				{	
					rs->CtrlList.push_back(rc->errList.front());
					rc->errList.pop_front();
				}	
				break;

			case 3:
				rs->NBChecked = false;
				rs->ctrlChecked = false;
				rs->iConsistChecked = true;

				rs->iConsistent = -1;

				rs->iConsList = DesAlgo::ErrorList();
				while (!rc->errList.empty())
				{	
					rs->iConsList.push_back(rc->errList.front());
					rc->errList.pop_front();
				}
				break;
		}

		// free memory
		delete(rc);

		// update the count of free slots and signal the main process to spawn another thread (if waiting)
		pthread_mutex_lock(&distHandlerMutex);
		freeSlots += 1;
		pthread_cond_signal(&distHandlerCond);
		pthread_mutex_unlock(&distHandlerMutex);

		// return result
		return rs;
	}

//______________________________________________________________________________________________

	// Return a resultStruct object containing the results
	void* checkSubsystem(void* args)
	{

		// arg[0] = subsystem number
		// arg[1] = isBDD
		// arg[2] = isHighLevel
		int* par = (int*)args;

		remoteCheck* results[3];

		pthread_t tasks[3];

		// Create threads for tasks
		pthread_create(&tasks[0], NULL, runNonBlock, (void*) par);
		pthread_create(&tasks[1], NULL, runCtrl, (void*) par);
		pthread_create(&tasks[2], NULL, runIConsist, (void*) par);		

		// Collect the results
		for (int i = 0; i < 3; i++)
		{
			pthread_join(tasks[i], (void**)&results[i]);
		}

		// Record the results
		resultStruct* rs = new resultStruct;

		if (rs == null)
				throw new EX("Out of memory error");
		
		rs->nonBlocking = results[0]->result;
		rs->controllable = results[1]->result;
		rs->iConsistent = results[2]->result;
		
		rs->SucList = DesAlgo::ErrorList();

		// Record any messages
		if (results[0]->result < 0)
		{	
			rs->NBList = DesAlgo::ErrorList();		
			while (!results[0]->errList.empty())
			{	
				rs->NBList.push_back(results[0]->errList.front());
				results[0]->errList.pop_front();
			}
		}
		if (results[1]->result < 0)
		{		
			rs->CtrlList = DesAlgo::ErrorList();	
			while (!results[1]->errList.empty())
			{	
				rs->CtrlList.push_back(results[1]->errList.front());
				results[1]->errList.pop_front();
			}
		}
		if (results[2]->result < 0)
		{	
			rs->iConsList = DesAlgo::ErrorList();
			while (!results[2]->errList.empty())
			{	
				rs->iConsList.push_back(results[2]->errList.front());
				results[2]->errList.pop_front();
			}
		}

		// Free up memory allocated in threads
		free(results[0]);
		free(results[1]);
		free(results[2]);

		rs->NBChecked = 
		rs->ctrlChecked = 
		rs->iConsistChecked = true;

		// don't need to signal here because each property check algorithm will signal itself

		return (void*)rs;
	}

//______________________________________________________________________________________________

	// Return a remoteCheck object containing the result
	void* runSynthesis(void* args)
	{
		// arg[0] = subsystem number
		// arg[1] = synth choice (0 = BDD, 1 = DES, 2 = Both)
		// arg[2] = isHighLevel
		int* par = (int*)args;

		CommHandler com = CommHandler(false, -1);

		// Build string to be sent
		stringstream ss;

		// Add project path
		ss << projectPath << " ";
				
		// Add command
		// Check synth type choice
		switch (par[1])
		{
			// BDD
			case 0:
				ss << (par[2] == 1 ? BDDHighSynthb : BDDLowSynthb);
				break;

			// DES
			case 1:
				ss << (par[2] == 1 ? BDDHighSynthd : BDDLowSynthd);
				break;

			// Both
			case 2:
				ss << (par[2] == 1 ? BDDHighSyntho : BDDLowSyntho);
				break;
		}
		

		// Add subsystem index
		ss << " " << par[0];

		remoteCheck* rc = new remoteCheck;

		if (rc == null)
				throw new EX("Out of memory error");

		rc = com.sendRecv(ss.str());

		return (void*)rc;
	}

//______________________________________________________________________________________________

	resultStruct DistHandler::runFlatCheck(bool incremental)
	{
		
		remoteCheck* results[2];

		pthread_t tasks[2];

		// used to indicate which threads are actually created and, thus, need to be joined.
		// needed to accomodate incremental checking
		bool joinThreads[2] = { false };
		
		int arg[1] = { -1 };
		if (!incremental || !m_project.isNonBlocking())
		{
			pthread_create(&tasks[0], NULL, runNonBlock, (void*) arg);
			joinThreads[0] = true;
		}
		if (!incremental || !m_project.isControllable())
		{
			pthread_create(&tasks[1], NULL, runCtrl, (void*) arg);
			joinThreads[1] = true;
		}

		for (int i = 0; i < 2; i++)
		{
			if (joinThreads[i])
			{
				pthread_join(tasks[i], (void**)&results[i]);
			}
		}		

		//build return structure
		resultStruct rs;
		rs.ctrlChecked = rs.NBChecked = true;
		rs.nonBlocking = results[0]->result == 0 ? eNonBlockYes : eNonBlockNo;
		rs.controllable = results[1]->result == 0 ? eCtrlYes : eCtrlNo;

		// build error message
		rs.NBList = DesAlgo::ErrorList();
		rs.CtrlList = DesAlgo::ErrorList();
		while (!results[0]->errList.empty())
		{
			rs.NBList.push_back(results[0]->errList.front());
			results[0]->errList.pop_front();
		}

		while (!results[1]->errList.empty())
		{
			rs.CtrlList.push_back(results[1]->errList.front());
			results[1]->errList.pop_front();
		}

		// set flags
		dynamic_cast<DesFlatProject*>(&m_project)->setFlags(rs);

		free(results[0]);
		free(results[1]);

		return rs;
	}

//______________________________________________________________________________________________
		
	resultStruct DistHandler::runHISCCheck(checkType type, bool isBDD, bool incremental)
	{

		// determine maximum number of simultaneous threads we want to allow
		CommHandler com = CommHandler(false, -1);
		freeSlots = 1.5 * com.getSlaveCount(); // a bit more than the number of nodes so that there will
						       // be a job ready to be sent as soon as once finishes

		if (freeSlots == 0)
			throw new EX("No nodes available before processing started");

		vector<pthread_t> subsystems;
		vector<pthread_t> interfaces;
		vector<resultStruct*> subResults;
		vector<remoteCheck*> iResults;
		vector<remoteCheck*> rcResults;

		vector<int> subNumber;

		vector<int*> args;

		int BDD = (isBDD ? 1 : 0);
		int isHighLevel;

		DesHierProject& h_project = *(dynamic_cast<DesHierProject*>(&m_project));

		DesHierProject::SubsysIteratorPtr subsysIt = h_project.createSubsysIterator();
		DesHierProject::InterfIteratorPtr interfIt = h_project.createInterfIterator();
		unsigned int i;

		// Set flags
		int isIConsist = eIConsYes;
		int isNonBlocking = eLwNonBlockYes;
		int isControllable = eLwCtrlYes;
		
		bool subSysPassed;

		resultStruct rs;

		// since BDD tasks return a message on both sucess and failure,
		// we need to record both and then determine which list to return
		DesAlgo::ErrorList NBErrList = DesAlgo::ErrorList();
		DesAlgo::ErrorList CtrlErrList = DesAlgo::ErrorList();
		DesAlgo::ErrorList iConsErrList = DesAlgo::ErrorList();
		DesAlgo::ErrorList SuccList = DesAlgo::ErrorList();

		switch(type)
		{
			case All:
				i = 0;
				// Create subsystem threads
				for (subsysIt->first(); subsysIt->notDone(); i++)
				{
					// Determine if current subsystem is high level
					isHighLevel = (subsysIt->currentItem().getLevel() == 0 ? 1 : 0);

					// add subsystem to list
					subsystems.push_back(pthread_t());

					// Create args for thread
					args.push_back((int*)malloc(sizeof(int)*3));

					if (args.back() == null)
						throw new EX("Out of memory error");

					args.back()[0] = i;
					args.back()[1] = BDD;
					args.back()[2] = isHighLevel;

					// ensure we have enough free slots before spawning the thread
					pthread_mutex_lock(&distHandlerMutex);
					while (freeSlots <= 0)
						pthread_cond_wait(&distHandlerCond, &distHandlerMutex);
					

					// remove the number of slots we will need
					if (BDD == 1)
						freeSlots -= 1;	// all 3 BDD checks are performed on a single node
					else
						freeSlots -= 3; // each task is sent to a seperate node
					
					// release lock
					pthread_mutex_unlock(&distHandlerMutex);					

					// Create thread
					if (BDD == 1)
					{
						// BDD
						pthread_create(&subsystems[i], NULL, runBDDCheckAll, (void*)args.back());
					}
					else
					{
						// Non BDD
						pthread_create(&subsystems[i], NULL, checkSubsystem, (void*)args.back());
					}
					
					// Next subsystem!
					subsysIt->next();
				}
				
				// check the interfaces directly if not BDD; BDD handles the checks as part of iConsis
				if (!BDD)
				{
					i = 0;
					for (interfIt->first(); interfIt->notDone(); i++)
					{
						// add interface to list
						interfaces.push_back(pthread_t());

						// Create args for thread
						args.push_back((int*)malloc(sizeof(int)*2));

						if (args.back() == null)
							throw new EX("Out of memory error");

						args.back()[0] = i;
						args.back()[1] = BDD;

						// ensure we have enough free slots before spawning the thread
						pthread_mutex_lock(&distHandlerMutex);
						while (freeSlots <= 0)
							pthread_cond_wait(&distHandlerCond, &distHandlerMutex);					

						// remove the number of slots we will need
						freeSlots -= 1;	

						// release lock
						pthread_mutex_unlock(&distHandlerMutex);
					
						// create thread
						pthread_create(&interfaces[i], NULL, runIValid, (void*)args.back());

						interfIt->next();
					}
				}
				

				// Collect results
				subResults = vector<resultStruct*>(subsystems.size());
				for (i = 0; i < subsystems.size(); i++)
				{	
					pthread_join(subsystems[i], (void**)&subResults[i]);
				}

				if (!BDD)
				{
					iResults = vector<remoteCheck*>(interfaces.size());
					for (i = 0; i < interfaces.size(); i++)
					{	
						pthread_join(interfaces[i], (void**)&iResults[i]);
					}
				}				

				// Deallocate args
				for (i = 0; i < args.size(); i++)
				{
					free(args[i]);
				}
				
				// start building return structure
				rs.NBChecked = rs.ctrlChecked = rs.iConsistChecked = false;

				// set flags
				subsysIt->first();
				for (i = 0; i < subResults.size(); i++)
				{
					subSysPassed = true;

					rs.NBChecked |= subResults[i]->NBChecked;
					rs.ctrlChecked |= subResults[i]->ctrlChecked;
					rs.iConsistChecked |= subResults[i]->iConsistChecked;

					// build top level flags and local DES flags					
					if (subResults[i]->NBChecked)
					{
						if (isNonBlocking == eLwNonBlockNotVerified) // if one of the subsystems has not checked a property
						{
							// only record the result if it failed
							if (subResults[i]->nonBlocking != 0)
								isNonBlocking = eLwNonBlockNo;
						}
						else
							// if every subsystem so far has checked the property, record as normal
							isNonBlocking &= (subResults[i]->nonBlocking == 0);

						subsysIt->currentItem().setNonBlocking(subResults[i]->nonBlocking == 0);

						// record any messages
						if (subResults[i]->nonBlocking != 0)
						{
							while (!subResults[i]->NBList.empty())
							{
								NBErrList.push_back(subResults[i]->NBList.front());
								subResults[i]->NBList.pop_front();
							}

							subSysPassed = false;
						}
					}
					else
					{
						if (isNonBlocking != eLwNonBlockNo) // only record a property as unchecked if no other subsytem has failed
							isNonBlocking = eLwNonBlockNotVerified;

						subSysPassed = false;
					}

					if (subResults[i]->ctrlChecked)
					{
						if (isControllable == eLwCtrlNotVerified) // if one of the subsystems has not checked a property
						{
							// only record the result if it failed
							if (subResults[i]->controllable != 0)
								isControllable = eLwCtrlNo;
						}
						else
							// if every subsystem so far has checked the property, record as normal
							isControllable &= (subResults[i]->controllable == 0);

						subsysIt->currentItem().setControllable(subResults[i]->controllable == 0);

						// record any messages
						if (subResults[i]->nonBlocking != 0)
						{
							while (!subResults[i]->CtrlList.empty())
							{
								CtrlErrList.push_back(subResults[i]->CtrlList.front());
								subResults[i]->CtrlList.pop_front();
							}

							subSysPassed = false;
						}
					}
					else
					{
						if (isControllable != eLwCtrlNo) // only record a property as unchecked if no other subsytem has failed
							isControllable = eLwCtrlNotVerified;

						subSysPassed = false;
					}

					if (subResults[i]->iConsistChecked)
					{
						if (isIConsist == eIConsNotVerified) // if one of the subsystems has not checked a property
						{
							// only record the result if it failed
							if (subResults[i]->iConsistent != 0)
								isIConsist = eIConsNo;
						}
						else
							// if every subsystem so far has checked the property, record as normal
							isIConsist &= (subResults[i]->iConsistent == 0);

						subsysIt->currentItem().setInterfConsist(subResults[i]->iConsistent == 0);

						// record any messages
						if (subResults[i]->nonBlocking != 0)
						{
							while (!subResults[i]->iConsList.empty())
							{
								iConsErrList.push_back(subResults[i]->iConsList.front());
								subResults[i]->iConsList.pop_front();
							}

							subSysPassed = false;
						}
					}
					else
					{
						if (isIConsist != eIConsNo) // only record a property as unchecked if no other subsytem has failed
							isIConsist = eIConsNotVerified;

						subSysPassed = false;
					}
					
					if (subSysPassed)
					{
						while (!subResults[i]->SucList.empty())
						{
							SuccList.push_back(subResults[i]->SucList.front());
							subResults[i]->SucList.pop_front();
						}
					}

					subsysIt->next();

					// deallocate memory
					free(subResults[i]);
				}	

				if (!BDD)
				{
					interfIt->first();
					for (i = 0; i < iResults.size(); i++)
					{	
						rs.iConsistChecked = true;

						isIConsist &= (iResults[i]->result == 0);						
	
						interfIt->currentItem().setInterfConsist(iResults[i]->result == 0);

						// failure
						while (!iResults[i]->errList.empty())
						{
							iConsErrList.push_back(iResults[i]->errList.front());
							iResults[i]->errList.pop_front();						
						}

						interfIt->next();
					}
				}
								
								
				rs.controllable = isControllable;
				rs.nonBlocking = isNonBlocking;
				rs.iConsistent = isIConsist;

				rs.SucList = DesAlgo::ErrorList();
				rs.NBList = DesAlgo::ErrorList();
				rs.CtrlList = DesAlgo::ErrorList();
				rs.iConsList = DesAlgo::ErrorList();

				// copy appropriate message list
				if (isControllable && isNonBlocking && isIConsist)
				{
					while (!SuccList.empty())
					{
						// Only BDD has a message returned on success. Ensure that the High-level
						// messages appear before the Low-Level messages
						if (SuccList.front().find(L"High-level") != string::npos)
							rs.SucList.push_front(SuccList.front());
						else
							rs.SucList.push_back(SuccList.front());

						SuccList.pop_front();
					}
				}
				else
				{
					while (!NBErrList.empty())
					{
						rs.NBList.push_back(NBErrList.front());
						NBErrList.pop_front();
					}

					while (!CtrlErrList.empty())
					{
						rs.CtrlList.push_back(CtrlErrList.front());
						CtrlErrList.pop_front();
					}

					while (!iConsErrList.empty())
					{
						rs.iConsList.push_back(iConsErrList.front());
						iConsErrList.pop_front();
					}
				}

				// update project flags
				dynamic_cast<DesHierProject*>(&m_project)->setFlags(rs);	
				
				return rs;
				break;
			
			case nonBlocking:
				i = 0;
				// Create subsystem threads
				for (subsysIt->first(); subsysIt->notDone(); i++)
				{
					// Check if this subsystem needs to be checked
					if (!incremental || !subsysIt->currentItem().isNonBlocking())
					{
						// Determine if current subsystem is high level
						isHighLevel = (subsysIt->currentItem().getLevel() == 0 ? 1 : 0);

						// add subsystem to list
						subsystems.push_back(pthread_t());
						subNumber.push_back(i);

						// Create args for thread
						args.push_back((int*)malloc(sizeof(int)*3));

						if (args.back() == null)
							throw new EX("Out of memory error");

						args.back()[0] = i;
						args.back()[1] = BDD;
						args.back()[2] = isHighLevel;

						// ensure we have enough free slots before spawning the thread
						pthread_mutex_lock(&distHandlerMutex);

						while (freeSlots <= 0)
							pthread_cond_wait(&distHandlerCond, &distHandlerMutex);

						// remove the number of slots we will need
						freeSlots -= 1;		

						// release lock
						pthread_mutex_unlock(&distHandlerMutex);

						// Create thread
						pthread_create(&subsystems[i], NULL, runNonBlock, (void*)args.back());
					}

					// Next subsystem!
					subsysIt->next();					
				}

				// Collect results	
				rcResults = vector<remoteCheck*>(subsystems.size());
				for (i = 0; i < subsystems.size(); i++)
				{
					pthread_join(subsystems[i], (void**)&rcResults[i]);	
				}				

				// Deallocate args
				for (i = 0; i < args.size(); i++)
				{
					free(args[i]);
				}
				
				// set flags
				subsysIt->first();

				// i is the index into the subNumber vector, which keeps track of which subsystems were checked.
				// when j (the loop counter) reaches the next subsystem index, we set the flags, free the memory, and increment i
				i = 0;
				for (int j = 0; subsysIt->notDone(); subsysIt->next(), j++)
				{
					if (j == subNumber[i])
					{
						// build top level flag
						isNonBlocking &= (rcResults[i]->result == 0);

						// look for subsystem indicated by subNumber[i]
						// set nonblocking status
						subsysIt->currentItem().setNonBlocking(rcResults[i]->result == 0);

						// build error list
						if (rcResults[i]->result == 0)
						{
							while (!rcResults[i]->errList.empty())
							{
								SuccList.push_back(rcResults[i]->errList.front());
								rcResults[i]->errList.pop_front();
							}
						}
						else
						{
							while (!rcResults[i]->errList.empty())
							{
								NBErrList.push_back(rcResults[i]->errList.front());
								rcResults[i]->errList.pop_front();
							}
						}

						// deallocate memory
						free(rcResults[i]);

						i++;
					}
				}	

				rs.ctrlChecked = rs.iConsistChecked = false;
				rs.NBChecked = true;
				rs.nonBlocking = isNonBlocking;

				rs.SucList = DesAlgo::ErrorList();
				rs.NBList = DesAlgo::ErrorList();

				if (isNonBlocking)
				{
					while (!SuccList.empty())
					{
						// Only BDD has a message returned on success. Ensure that the High-level
						// messages appear before the Low-Level messages
						if (SuccList.front().find(L"High-level") != string::npos)
							rs.SucList.push_front(SuccList.front());
						else
							rs.SucList.push_back(SuccList.front());

						SuccList.pop_front();
					}
				}
				else
				{
					while (!NBErrList.empty())
					{
						rs.NBList.push_back(NBErrList.front());
						NBErrList.pop_front();
					}
				}

				dynamic_cast<DesHierProject*>(&m_project)->setFlags(rs);	

				return rs;
				break;

			case controllable:
				i = 0;
				// Create subsystem threads
				for (subsysIt->first(); subsysIt->notDone(); i++)
				{
					// Check if this subsystem needs to be checked
					if (!incremental || !subsysIt->currentItem().isControllable())
					{
						// Determine if current subsystem is high level
						isHighLevel = (subsysIt->currentItem().getLevel() == 0 ? 1 : 0);

						// add subsystem to list
						subsystems.push_back(pthread_t());
						subNumber.push_back(i);

						// Create args for thread
						args.push_back((int*)malloc(sizeof(int)*3));

						if (args.back() == null)
							throw new EX("Out of memory error");

						args.back()[0] = i;
						args.back()[1] = BDD;
						args.back()[2] = isHighLevel;

						// ensure we have enough free slots before spawning the thread
						pthread_mutex_lock(&distHandlerMutex);
						while (freeSlots <= 0)
							pthread_cond_wait(&distHandlerCond, &distHandlerMutex);

						// remove the number of slots we will need
						freeSlots -= 1;							
					
						// release lock
						pthread_mutex_unlock(&distHandlerMutex);

						// Create thread
						pthread_create(&subsystems[i], NULL, runCtrl, (void*)args.back());
					}

					// Next subsystem!
					subsysIt->next();					
				}

				// Collect results	
				rcResults = vector<remoteCheck*>(subsystems.size());
				for (i = 0; i < subsystems.size(); i++)
				{
					pthread_join(subsystems[i], (void**)&rcResults[i]);	
				}

				// Deallocate args
				for (i = 0; i < args.size(); i++)
				{
					free(args[i]);
				}
				
				// set flags
				subsysIt->first();

				// i is the index into the subNumber vector, which keeps track of which subsystems were checked.
				// when j (the loop counter) reaches the next subsystem index, we set the flags, free the memory, and increment i
				i = 0;
				for (int j = 0; subsysIt->notDone(); subsysIt->next(), j++)
				{
					if (j == subNumber[i])
					{
						// build top level flag
						isControllable &= (rcResults[i]->result == 0);

						// look for subsystem indicated by subNumber[i]
						// set controllable status
						subsysIt->currentItem().setControllable(rcResults[i]->result == 0);

						// build error list
						if (rcResults[i]->result == 0)
						{
							while (!rcResults[i]->errList.empty())
							{
								SuccList.push_back(rcResults[i]->errList.front());
								rcResults[i]->errList.pop_front();
							}
						}
						else
						{
							while (!rcResults[i]->errList.empty())
							{
								CtrlErrList.push_back(rcResults[i]->errList.front());
								rcResults[i]->errList.pop_front();
							}
						}

						// deallocate memory
						free(rcResults[i]);

						i++;
					}
				}	
				
				rs.NBChecked = rs.iConsistChecked = false;
				rs.ctrlChecked = true;
				rs.controllable = isControllable;

				rs.SucList = DesAlgo::ErrorList();
				rs.CtrlList = DesAlgo::ErrorList();

				if (isControllable)
				{
					while (!SuccList.empty())
					{
						// Only BDD has a message returned on success. Ensure that the High-level
						// messages appear before the Low-Level messages
						if (SuccList.front().find(L"High-level") != string::npos)
							rs.SucList.push_front(SuccList.front());
						else
							rs.SucList.push_back(SuccList.front());

						SuccList.pop_front();
					}
				}
				else
				{
					while (!CtrlErrList.empty())
					{
						rs.CtrlList.push_back(CtrlErrList.front());
						CtrlErrList.pop_front();
					}
				}

				dynamic_cast<DesHierProject*>(&m_project)->setFlags(rs);	

				return rs;
				break;	

			case iConsist:	
				i = 0;
				// Create subsystem threads
				for (subsysIt->first(); subsysIt->notDone(); i++)
				{
					// Check if this subsystem needs to be checked
					if (!incremental || !subsysIt->currentItem().isInterfConsist())
					{
						// Determine if current subsystem is high level
						isHighLevel = (subsysIt->currentItem().getLevel() == 0 ? 1 : 0);

						// add subsystem to list
						subsystems.push_back(pthread_t());
						subNumber.push_back(i);

						// Create args for thread
						args.push_back((int*)malloc(sizeof(int)*3));

						if (args.back() == null)
							throw new EX("Out of memory error");

						args.back()[0] = i;
						args.back()[1] = BDD;
						args.back()[2] = isHighLevel;

						// ensure we have enough free slots before spawning the thread
						pthread_mutex_lock(&distHandlerMutex);
						while (freeSlots <= 0)
							pthread_cond_wait(&distHandlerCond, &distHandlerMutex);

						// remove the number of slots we will need
						freeSlots -= 1;							
					
						// release lock
						pthread_mutex_unlock(&distHandlerMutex);

						// Create thread
						pthread_create(&subsystems[i], NULL, runIConsist, (void*)args.back());
					}

					// Next subsystem!
					subsysIt->next();					
				}

				// check the interfaces directly if not BDD; BDD handles the checks as part of iConsis
				if (!BDD)
				{
					i = 0;
					for (interfIt->first(); interfIt->notDone(); i++)
					{
						// add interface to list
						interfaces.push_back(pthread_t());

						// Create args for thread
						args.push_back((int*)malloc(sizeof(int)*2));

						if (args.back() == null)
							throw new EX("Out of memory error");

						args.back()[0] = i;
						args.back()[1] = BDD;

						// ensure we have enough free slots before spawning the thread
						pthread_mutex_lock(&distHandlerMutex);
						while (freeSlots <= 0)
							pthread_cond_wait(&distHandlerCond, &distHandlerMutex);					

						// remove the number of slots we will need
						freeSlots -= 1;	

						// release lock
						pthread_mutex_unlock(&distHandlerMutex);
					
						// create thread
						pthread_create(&interfaces[i], NULL, runIValid, (void*)args.back());

						interfIt->next();
					}
				}

				// Collect results	
				rcResults = vector<remoteCheck*>(subsystems.size());
				for (i = 0; i < subsystems.size(); i++)
				{
					pthread_join(subsystems[i], (void**)&rcResults[i]);	
				}

				if (!BDD)
				{
					iResults = vector<remoteCheck*>(interfaces.size());
					for (i = 0; i < interfaces.size(); i++)
					{	
						pthread_join(interfaces[i], (void**)&iResults[i]);
					}
				}

				// Deallocate args
				for (i = 0; i < args.size(); i++)
				{
					free(args[i]);
				}

				// set flags
				subsysIt->first();
				bool isIConsist = true;

				// i is the index into the subNumber vector, which keeps track of which subsystems were checked.
				// when j (the loop counter) reaches the next subsystem index, we set the flags, free the memory, and increment i
				i = 0;
				for (int j = 0; subsysIt->notDone(); subsysIt->next(), j++)
				{
					if (j == subNumber[i])
					{
						// build top level flag
						isIConsist &= (rcResults[i]->result == 0);

						// look for subsystem indicated by subNumber[i]
						// set iConsist status
						subsysIt->currentItem().setInterfConsist(rcResults[i]->result == 0);

						// build error list
						if (rcResults[i]->result == 0)
						{
							while (!rcResults[i]->errList.empty())
							{
								SuccList.push_back(rcResults[i]->errList.front());
								rcResults[i]->errList.pop_front();
							}
						}
						else
						{
							while (!rcResults[i]->errList.empty())
							{
								iConsErrList.push_back(rcResults[i]->errList.front());
								rcResults[i]->errList.pop_front();
							}
						}

						// deallocate memory
						free(rcResults[i]);

						i++;
					}
				}	

				if (!BDD)
				{
					interfIt->first();
					for (i = 0; i < iResults.size(); i++)
					{	
						rs.iConsistChecked = true;

						isIConsist &= (iResults[i]->result == 0);						
	
						interfIt->currentItem().setInterfConsist(iResults[i]->result == 0);

						// failure
						while (!iResults[i]->errList.empty())
						{
							iConsErrList.push_back(iResults[i]->errList.front());
							iResults[i]->errList.pop_front();						
						}

						interfIt->next();
					}
				}			

				rs.ctrlChecked = rs.NBChecked = false;
				rs.iConsistChecked = true;
				rs.iConsistent = isIConsist;

				rs.SucList = DesAlgo::ErrorList();
				rs.iConsList = DesAlgo::ErrorList();

				if (isIConsist)
				{
					while (!SuccList.empty())
					{
						// Only BDD has a message returned on success. Ensure that the High-level
						// messages appear before the Low-Level messages
						if (SuccList.front().find(L"High-level") != string::npos)
							rs.SucList.push_front(SuccList.front());
						else
							rs.SucList.push_back(SuccList.front());

						SuccList.pop_front();
					}
				}
				else
				{
					while (!iConsErrList.empty())
					{
						rs.iConsList.push_back(iConsErrList.front());
						iConsErrList.pop_front();
					}
				}

				dynamic_cast<DesHierProject*>(&m_project)->setFlags(rs);	

				return rs;

				break;
		}

		return rs;
	}
	
//______________________________________________________________________________________________

	DesAlgo::ErrorList DistHandler::runSynth(char choice)
	{
		vector<pthread_t> subsystems;
		vector<remoteCheck*> subResults;

		vector<int*> args;

		int isHighLevel;		

		DesHierProject::SubsysIteratorPtr subsysIt = dynamic_cast<DesHierProject*>(&m_project)->createSubsysIterator();
		unsigned int i = 0;
		// Create subsystem threads
		for (subsysIt->first(); subsysIt->notDone(); i++)
		{
			// Determine if current subsystem is high level
			isHighLevel = (subsysIt->currentItem().getLevel() == 0 ? 1 : 0);

			// add subsystem to list
			subsystems.push_back(pthread_t());

			// Create args for thread
			args.push_back((int*)malloc(sizeof(int)*3));

			if (args.back() == null)
				throw new EX("Out of memory error");

			args.back()[0] = i;
			args.back()[1] = (choice == 'b' ? 0 : (choice == 'd' ? 1 : 2));
			args.back()[2] = isHighLevel;

			// Create thread
			pthread_create(&subsystems[i], NULL, runSynthesis, (void*)args.back());

			// Next subsystem!
			subsysIt->next();
		}

		// Collect results
		subResults = vector<remoteCheck*>(subsystems.size());
		for (i = 0; i < subsystems.size(); i++)
		{					
			pthread_join(subsystems[i], (void**)&subResults[i]);					
		}

		// Deallocate args
		for (i = 0; i < args.size(); i++)
		{
			free(args[i]);
		}

		DesAlgo::ErrorList errList = DesAlgo::ErrorList();

		// Build errorList then Deallocate memory
		for (i = 0; i < subResults.size(); i++)
		{		
			while (!subResults[i]->errList.empty())
			{
				errList.push_back(subResults[i]->errList.front());
				subResults[i]->errList.pop_front();
			}

			// Deallocate memory
			free(subResults[i]);
		}

		return errList;
	}
}

#endif
