/*	Author:		Magdin Stoica
	Supervisor: Dr. Ryan Leduc
	
	Project created in conformity with the requirements for the Degree of Master of Engineering in Software Engineering, 
	Computing and Software Department, 
	McMaster University
	2003 - 2007
*/

#pragma once

#include "ProjectEditor.h"
#include "FlatProjectWorkspace.h"


namespace DESpot
{
	class MainForm;
	class DesFlatProject;

	class FlatProjectEditor: public ProjectEditor
	{
		Q_OBJECT

		public:
			FlatProjectEditor(const QString& projName, MainForm* pMainForm);
			FlatProjectEditor(DesProject* project, MainForm* pMainForm);
			virtual ~FlatProjectEditor(void);
		
		// Added by RJL - remove when bddsd
		//integrated with despot
		//Implementation methods
		protected:
			bool attemptExportToBDDsd();

		// remove to here - RJL

		protected slots:
			virtual void onAddDes();
			virtual void onCheckProjectIntegrity();			
			virtual void onCheckProject();
			
			//Added by Adam for bddExport
			void onExportToBDDsd();

			//Added by Adam for BDD Tools
			#ifdef __ENABLE_BDD__
			void onRunBddCheckAllTool();
			void onRunBddNonblockingTool();
			void onRunBddControllabilityTool();
			void onRunBddNBControllabilityTool();
			void onRunBddTDESControllabilityTool();
			void onRunBddSDControllabilityTool();
			void onRunBddProperTimebehaviorTool();
			void onRunBddSSingularProhibitableBehaviorTool();
			void onRunBddPlantCompletenessTool();
			void onRunBddALFTool();
                        #endif

		private:
			DesFlatProject* project();
			FlatProjectWorkspace* workspace();

			void setupConnections();
	};

} //end of namespace DESpot
