#include "taskMap.h"


void initSystem( System *system, unsigned mP, 
					unsigned mD, boolean preemt, boolean sR )
{
	delayed->length = 0;
	listInitialise(delayed _(ghost (enum xListType)PQ) );
	_(ghost system->\owns+=\embedding(&delayed) )
	_(ghost system->\owns+=delayed )

	oDelayed->length = 0;
	listInitialise(oDelayed _(ghost (enum xListType)PQ) );
	_(ghost system->\owns+=\embedding(&oDelayed) )
	_(ghost system->\owns+=oDelayed )

	blocked->length = 0;
	listInitialise(blocked _(ghost (enum xListType)PQ) );
	_(ghost system->\owns+=\embedding(&blocked) )
	_(ghost system->\owns+=blocked )

	suspended->length = 0;
	listInitialise(suspended _(ghost (enum xListType)PQ) );
	_(ghost system->\owns+=\embedding(&suspended) )
	_(ghost system->\owns+=suspended )

	deleted->length = 0;
	listInitialise(deleted _(ghost (enum xListType)PQ) );
	_(ghost system->\owns+=\embedding(&deleted) )
	_(ghost system->\owns+=deleted )

	maxPrio = mP;
	maxNumVal = mD;
	preemption = preemt;
	schedulerRunning = sR;
	xTickCount = 0;
	_(wrap \embedding(&maxPrio) )
	_(wrap \embedding(&maxNumVal) )
	_(wrap \embedding(&preemption) )
	_(wrap \embedding(&schedulerRunning) )
	_(wrap \embedding(&xTickCount) )
	_(ghost system->\owns+=\embedding(&maxPrio) )
	_(ghost system->\owns+=\embedding(&maxNumVal) )
	_(ghost system->\owns+=\embedding(&preemption) )
	_(ghost system->\owns+=\embedding(&schedulerRunning) )
	_(ghost system->\owns+=\embedding(&xTickCount) )

	//_(wrap system )
}


void vTaskDelay( unsigned xTicksToDelay )
{
	unsigned xTimeToWake;
	unsigned xAlreadyYielded = 0; 
	_(unwrap &sstm )
	_(ghost (&sstm)->\owns -= pxCurrentTCB )
	if( xTicksToDelay > 0 ) 
	{
		//vTaskSuspendAll();
		/*	Suspending the scheduler is not considered in 
			this verification as we are not verifying 
			port specific functionality. In particular 
			interrupt processing.
		*/
		//traceTASK_DELAY();
		_(ghost (&sstm)->\owns -= rdyLists )
		_(unwrap rdyLists)
		_(ghost rdyLists->\owns -= 
				rdyLists->ready[pxCurrentTCB->uxPriority] )
		//xTimeToWake = xTickCount + xTicksToDelay ;
		/*	For the above statement, developer seems to have 
			assumed modulo 'maxNumVal+1' addition. But it is not 
			very clear whether the addition is always modulo for 
			unsigned numbers as per the C standard.
			In spite of this, VCC will allow addition
			only if it knows that the result is within the 
			limit. 
			Hence we rewrite the above statement to an equivalent
			block as below to ensure addition modulo 'maxNumVal+1'
			such that result of all sub expressions are within 
			the limit of the data type.
		*/
		if( xTicksToDelay <= ( maxNumVal - xTickCount ) )
		{
			xTimeToWake = xTickCount + xTicksToDelay ;	
		}
		else
		{
			xTimeToWake =  xTicksToDelay - ( maxNumVal - xTickCount ) - 1;	
		}
		listRemove(rdyLists->ready[pxCurrentTCB->uxPriority],
									pxCurrentTCB->pvGenericListItem);
		/*	The above statement fails to restore the invariant on 
			'topReadyPriority' if the current task is the only task 
			at this index in ready queue.
			The following ghost code (assume statement) just assumes 
			the invariant on 'topReadyPriority'.
			This assume statement can be removed by 
			adding a loop to decrement 'topReadyPriority'
			until it goes to a nonempty list.
			Such a nonempty list is assured by an invariant 
			in readyLists.
		*/
		//////////////////////////////////
		_(assume !isListEmpty(rdyLists->
							ready[rdyLists->topReadyPriority]))
		//////////////////////////////////
		_(ghost rdyLists->\owns += 
				rdyLists->ready[pxCurrentTCB->uxPriority] ) 
		_(wrap rdyLists)
		_(ghost (&sstm)->\owns += rdyLists )
		setItemValue(pxCurrentTCB->pvGenericListItem, xTimeToWake);	
		/*	The condition in the following if statement is 
			rewritten to an equivalent condition to 
			avoid the overflow problem in VCC
		*/
		if( xTicksToDelay <= ( maxNumVal - xTickCount ) )
		{
			_(ghost (&sstm)->\owns -= delayed )
			listInsert(delayed, pxCurrentTCB->pvGenericListItem);
			_(ghost (&sstm)->\owns += delayed )
		}
		else
		{
			_(ghost (&sstm)->\owns -= oDelayed )
			listInsert(oDelayed, pxCurrentTCB->pvGenericListItem);
			_(ghost (&sstm)->\owns += oDelayed )
		}
		//xAlreadyYielded = xTaskResumeAll();
	}
	/*	Following segment is commented as we are not verifying the 
		port specific functionality
	*/
	/* Force a reschedule if xTaskResumeAll has not already done so, 
		we may have put ourselves to sleep. 
	if( !xAlreadyYielded )
		{
			portYIELD_WITHIN_API();
		}
	*/
	_(assume InvariantOnRunningTask(rdyLists,pxCurrentTCB) )
	_(ghost (&sstm)->\owns += pxCurrentTCB )
	_(wrap &sstm )
	//_(assert \false )
}


void vTaskDelayUntil( unsigned *pxPreviousWakeTime, 
								unsigned xTimeIncrement )
{
	unsigned xTimeToWake,xShouldDelay = 0;
	unsigned xAlreadyYielded = 0; 
	unsigned pWT;
	/*	To store the current value of '*pxPreviousWakeTime'
		which is required after modifying '*pxPreviousWakeTime'
	*/
	pWT = *pxPreviousWakeTime;
	_(unwrap (&sstm) )
	_(ghost (&sstm)->\owns -= pxCurrentTCB )
	//vTaskSuspendAll();
	//xTimeToWake = *pxPreviousWakeTime + xTimeIncrement;
	/*	For the above statement, developer seems to have 
		assumed modulo 'maxNumVal+1' addition. But it is not 
		very clear whether the addition is always modulo for 
		unsigned numbers as per the C standard.
		In spite of this, VCC will allow addition
		only if it knows that the result is within the 
		limit. 
		Hence we rewrite the above statement to an equivalent
		block as below to ensure addition modulo 'maxNumVal+1'
		such that result of all sub expressions are within 
		the limit of the data type.
	*/
	if( xTimeIncrement <= ( maxNumVal - *pxPreviousWakeTime ) )
	{
		xTimeToWake = *pxPreviousWakeTime + xTimeIncrement ;	
	}
	else
	{
		xTimeToWake =  xTimeIncrement - 
						( maxNumVal - *pxPreviousWakeTime ) - 1;	
	}
	if( xTickCount < *pxPreviousWakeTime )
	{
		if( ( xTimeToWake < *pxPreviousWakeTime ) && 
							( xTimeToWake > xTickCount ) )
		{
			xShouldDelay = 1;
		}
	}
	else
	{
		if( ( xTimeToWake < *pxPreviousWakeTime ) || 
							( xTimeToWake > xTickCount ) )
		{
			xShouldDelay = 1;
		}
	}
	/* Update the wake time ready for the next call. */
	*pxPreviousWakeTime = xTimeToWake;
	if(xShouldDelay) 
	{
		//traceTASK_DELAY();
		_(ghost (&sstm)->\owns -= rdyLists )
		_(unwrap rdyLists)
		_(ghost rdyLists->\owns -= 
				rdyLists->ready[pxCurrentTCB->uxPriority] )
		listRemove(rdyLists->ready[pxCurrentTCB->uxPriority],
								pxCurrentTCB->pvGenericListItem);
		/*	The above statement fails to restore the invariant on 
			'topReadyPriority' if the current task is the only task 
			at this index in ready queue.
			The following ghost code (assume statement) just assumes 
			the invariant on 'topReadyPriority'.
			This assume statement can be removed by 
			adding a loop to decrement 'topReadyPriority'
			until it goes to a nonempty list.
			Such a nonempty list is assured by an invariant 
			in readyLists.
		*/
		//////////////////////////////////
		_(assume !isListEmpty(rdyLists->
							ready[rdyLists->topReadyPriority]))
		//////////////////////////////////
		_(ghost rdyLists->\owns += 
					rdyLists->ready[pxCurrentTCB->uxPriority] ) 
		_(wrap rdyLists)	
		_(ghost (&sstm)->\owns += rdyLists )
		setItemValue(pxCurrentTCB->pvGenericListItem, xTimeToWake);	

		if( xTickCount < xTimeToWake )
		{
			_(ghost (&sstm)->\owns -= delayed )
			listInsert(delayed, pxCurrentTCB->pvGenericListItem);
			_(ghost (&sstm)->\owns += delayed )
		}
		else 
		{
			_(ghost (&sstm)->\owns -= oDelayed )
			listInsert(oDelayed, pxCurrentTCB->pvGenericListItem);
			_(ghost (&sstm)->\owns += oDelayed )
		}
	}
	//xAlreadyYielded = xTaskResumeAll();
	/*	Following segment is commented as we are not verifying the 
		port specific functionality
	*/
	/* Force a reschedule if xTaskResumeAll has not already done so, 
		we may have put ourselves to sleep.
		if( !xAlreadyYielded )
		{
			portYIELD_WITHIN_API();
		}
	 */
	_(assume InvariantOnRunningTask(rdyLists,pxCurrentTCB) )
	_(ghost (&sstm)->\owns += pxCurrentTCB )
	_(wrap (&sstm))
}



TCB* vTaskSwitchContext(  )
{
	unsigned index,preempt = 1;
	TCB *result;
	 /*	The following part is commenetd because we are 
		not modelling the case for suspending the scheduler 
		and we are not verifying the amount of processor 
		time used by a task etc
	 */
////////////////////////////////////////////////////////////
/*
	if( uxSchedulerSuspended != 
		( unsigned portBASE_TYPE ) pdFALSE )
	{
		/*	The scheduler is currently suspended - 
			do not allow a context
			switch. STAR/
		xMissedYield = pdTRUE;
		return;
	}

	traceTASK_SWITCHED_OUT();

	#if ( configGENERATE_RUN_TIME_STATS == 1 )
	{
		unsigned long ulTempCounter = 
				portGET_RUN_TIME_COUNTER_VALUE();
	}
	#endif

	taskFIRST_CHECK_FOR_STACK_OVERFLOW();
	taskSECOND_CHECK_FOR_STACK_OVERFLOW();
*/
////////////////////////////////////////////////////////////

	/*	The following loop is commented because nonempty 
		list at index 'topReadyPriority' is assured by 
		an invariant in readyLists.
	*/
///////////////////////////////////////////////////////////
	/*	Find the highest priority queue that 
		contains ready tasks. 
	while( listLIST_IS_EMPTY( 
		&( pxReadyTasksLists[ uxTopReadyPriority ] ) ) )
	{
		--uxTopReadyPriority;
	}
	*/
/////////////////////////////////////////////////////////////
	//listGET_OWNER_OF_NEXT_ENTRY( pxCurrentTCB, 
    //			&( pxReadyTasksLists[ uxTopReadyPriority ] ) );

	/*	Call to the above xList operation is replaced with the 
		call to the newly introduced function below.
		This is because, the above function fails in 
		getting longest waiting task at index 'topReadyPriority'
	*/
	_(unwrap (&sstm) )
	_(ghost (&sstm)->\owns -= rdyLists )
	_(unwrap rdyLists)
	_(ghost rdyLists->\owns -= 
			rdyLists->ready[rdyLists->topReadyPriority] )
	_(ghost (&sstm)->\owns -= \embedding(&pxCurrentTCB) )
	_(ghost (&sstm)->\owns -= pxCurrentTCB )
	_(assert \wrapped(pxCurrentTCB) )
	_(unwrap pxCurrentTCB )
	_(assert \writable(pxCurrentTCB) )
	if ( 	( pxCurrentTCB->uxPriority == rdyLists->topReadyPriority ) && 
			( listIsEmpty( rdyLists->ready[rdyLists->topReadyPriority] ) ) 
	   )
	{
		preempt = 0;
	}
	if ( preempt )
	{
		rotateLeft( rdyLists->ready[rdyLists->topReadyPriority] );
	}
	result = getOwnerOfFirstEntry(rdyLists->ready
						[rdyLists->topReadyPriority]);
	_(wrap pxCurrentTCB )
	_(ghost (&sstm)->\owns += pxCurrentTCB )
	_(ghost (&sstm)->\owns += \embedding(&pxCurrentTCB) )
	_(ghost rdyLists->\owns += 
			rdyLists->ready[rdyLists->topReadyPriority] )
	_(wrap rdyLists)
	_(ghost (&sstm)->\owns += rdyLists )
	//traceTASK_SWITCHED_IN();
	//vWriteTraceToBuffer();
	_(wrap (&sstm))
	
	return result;
}



void prvAddTaskToReadyQueue( TCB *pxTCB )
{
	_(unwrap (&sstm))
	_(ghost (&sstm)->\owns -= rdyLists )
	_(unwrap rdyLists)
	if( pxTCB->uxPriority > rdyLists->topReadyPriority )
	{
		rdyLists->topReadyPriority = pxTCB->uxPriority;
	}
	_(ghost rdyLists->\owns -= rdyLists->ready[pxTCB->uxPriority])
	_(ghost (&sstm)->\owns -= pxTCB )
	_(unwrap pxTCB )
	_(ghost pxTCB->\owns -= pxTCB->pvGenericListItem )
	listInsertEnd(rdyLists->ready[pxTCB->uxPriority], 
								pxTCB->pvGenericListItem);
	_(wrap pxTCB )
	_(ghost (&sstm)->\owns += pxTCB )
	_(ghost rdyLists->\owns += rdyLists->ready[pxTCB->uxPriority])
	_(wrap rdyLists )
	_(ghost (&sstm)->\owns += rdyLists )
	_(wrap (&sstm))
}




unsigned taskPrioritySet( TCB *pxTCB, unsigned newPrio )
{
	unsigned yieldRequired=0;
	unsigned currentPriority ;
	/*	We need teh above to remember the old priority 
		when pxTCB (task represented) in ready list.
		Because we need pass the list in which the 
		the operation is requested unlike in xList
	*/
	_(unwrap (&sstm) )
	_(ghost (&sstm)->\owns -= pxCurrentTCB )
	currentPriority = pxTCB->uxPriority;
	if( newPrio > currentPriority )
	{
		if( pxTCB != pxCurrentTCB )
		{
			yieldRequired = 1;
		}
	}
	else if( pxTCB == pxCurrentTCB )
	{
		yieldRequired = 1;
	}
	_(unwrap pxTCB )
	pxTCB->uxPriority = newPrio;
	//The following statement in the code is failed in the verification.
	/*This is because - the item whose value change is requested 
	  may be in some blocked queues, in such a case the statement 
	  if allowed will result in
	  the voilation of the invariant on blocked queue /
	//setItemValue(pxTCB->pvGenericListItem,newPrio);
	//Following is a possible solution to update it correctly.				*/
	//_(unwrap pxTCB )
	_(ghost (&sstm)->\owns -= blocked )
	if( containedWithin(blocked,pxTCB->pvEventListItem ) )
	{
		
		listRemove(blocked,pxTCB->pvEventListItem );
		setItemValue(pxTCB->pvEventListItem,newPrio);
		listInsert(blocked, pxTCB->pvEventListItem);
	}
	_(ghost (&sstm)->\owns += blocked )
	_(wrap pxTCB )
	_(ghost (&sstm)->\owns -= rdyLists )
	_(unwrap rdyLists)
	_(ghost rdyLists->\owns -= rdyLists->ready[currentPriority])
	if( containedWithin(rdyLists->ready[currentPriority],
			pxTCB->pvGenericListItem) )
	{
		listRemove(rdyLists->ready[currentPriority], 
								pxTCB->pvGenericListItem);
		_(unwrap pxTCB->pvGenericListItem )
		pxTCB->pvGenericListItem->ownersPriority = newPrio;
		_(wrap pxTCB->pvGenericListItem )
		_(ghost rdyLists->\owns += rdyLists->ready[currentPriority] )
		//	Without the following assume this function fails to satisfy the 
		//	invariant on topReadyPriotiy
		_(assume !isListEmpty(rdyLists->ready[rdyLists->topReadyPriority]))
		_(wrap rdyLists )
		_(unwrap pxTCB )
		_(ghost pxTCB->\owns += pxTCB->pvGenericListItem )
		setItemValue(pxTCB->pvGenericListItem, newPrio);
		_(wrap pxTCB )
		_(ghost (&sstm)->\owns += rdyLists )
		_(ghost (&sstm)->\owns += pxCurrentTCB )
		//_(ghost (&sstm)->\owns += pxTCB )
		_(wrap (&sstm))
		prvAddTaskToReadyQueue( pxTCB ) ;
	}
	else
	{
		_(ghost rdyLists->\owns += rdyLists->ready[currentPriority] )
		_(wrap rdyLists )
		_(ghost (&sstm)->\owns += rdyLists )
		_(ghost (&sstm)->\owns += pxCurrentTCB )
		_(wrap (&sstm))
	}
}





unsigned vTaskSuspend( TCB *pxTCB )
{
	unsigned yield = 0;
	//portENTER_CRITICAL();
	{
		/*	Ensure a yield is performed if the current task is being
			suspended. */
		if( pxTCB == pxCurrentTCB )
		{
			yield = 1;
		}
		/* If null is passed in here then we are suspending ourselves. */
		//pxTCB = prvGetTCBFromHandle( pxTaskToSuspend );
		//traceTASK_SUSPEND( pxTCB );
		/* Remove task from the ready/delayed list and place in the	suspended list. */
		_(unwrap (&sstm) )
		_(ghost (&sstm)->\owns -= rdyLists )
		_(unwrap rdyLists)
		_(ghost rdyLists->\owns -= rdyLists->ready[pxTCB->uxPriority])
		listRemove(rdyLists->ready[pxTCB->uxPriority],pxTCB->pvGenericListItem);
		_(ghost rdyLists->\owns += rdyLists->ready[pxTCB->uxPriority])
		//	Without the following assume this function fails to satisfy the 
		//	invariant on topReadyPriotiy
		_(assume !isListEmpty(rdyLists->ready[rdyLists->topReadyPriority]))
		_(wrap rdyLists)
		_(ghost (&sstm)->\owns += rdyLists )
		/*	Following code is commented because it has no effect 
			according to the added precondition, without which
			suspend can lead to some problems
		*/
		/*
		if( containedWithin(blocked,pxTCB->pvEventListItem ) )
		{
			listRemove(blocked,pxTCB->pvEventListItem );
		}
		*/
		_(ghost (&sstm)->\owns -= suspended )
		listInsert(suspended, pxTCB->pvGenericListItem);
		_(ghost (&sstm)->\owns += suspended )
		_(wrap (&sstm) )
	}
	//portEXIT_CRITICAL();
}



unsigned vTaskDelete( TCB *pxTCB )
{
	unsigned xSchedulerRunning,portYield;
	//portENTER_CRITICAL();
	{
		//vListRemove( &( pxTCB->xGenericListItem ) );
		//The abvove operaton is implemented with the 
		//llowing conditional operations in the 
		//map version of xList
		////////////////////
		_(unwrap (&sstm) )
		_(ghost (&sstm)->\owns -= rdyLists )
		_(unwrap rdyLists)
		_(ghost rdyLists->\owns -= rdyLists->ready[pxTCB->uxPriority])
	
		if( containedWithin(rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem) )
		{
			listRemove(rdyLists->ready[pxTCB->uxPriority],
									pxTCB->pvGenericListItem );
		}
	
		_(ghost rdyLists->\owns += rdyLists->ready[pxTCB->uxPriority])
		//	Without the following assume this function fails to satisfy the 
		//	invariant on topReadyPriotiy
		_(assume !isListEmpty(rdyLists->ready[rdyLists->topReadyPriority]))
		_(wrap rdyLists)
		_(ghost (&sstm)->\owns += rdyLists )
		_(ghost (&sstm)->\owns -= suspended )
		if( containedWithin(suspended,pxTCB->pvGenericListItem ) )
		{
			_(assert \thread_local(pxTCB->pvEventListItem) )
			listRemove(suspended,pxTCB->pvGenericListItem );
			//_(assert \thread_local(pxTCB->pvEventListItem) )
		}
		_(ghost (&sstm)->\owns += suspended )
		_(ghost (&sstm)->\owns -= delayed )
		if( containedWithin(delayed,pxTCB->pvGenericListItem ) )
		{
			listRemove(delayed,pxTCB->pvGenericListItem );
		}
		_(ghost (&sstm)->\owns += delayed )
		////////////////////
		_(ghost (&sstm)->\owns -= blocked )
		_(assume \thread_local(pxTCB->pvEventListItem) )
		if( containedWithin(blocked,pxTCB->pvEventListItem ) )
		{
			listRemove(blocked,pxTCB->pvEventListItem );
			_(assert !presentIn(blocked, pxTCB->pvEventListItem) )
		}
		_(ghost (&sstm)->\owns += blocked )
		_(ghost (&sstm)->\owns -= deleted )
		listInsert(deleted, pxTCB->pvGenericListItem);
		_(ghost (&sstm)->\owns += deleted )
	
		//++uxTasksDeleted;
		//uxTaskNumber++;
		//traceTASK_DELETE( pxTCB );
	}
	//portEXIT_CRITICAL();
	if( xSchedulerRunning != 0 )
	{
		if( pxTCB == pxCurrentTCB )
		{
			//portYIELD_WITHIN_API();
			portYield = 1;
		}
	}
	_(wrap (&sstm) )
}


TCB* vTaskSwitchContextTerminationProof(  )
{
	unsigned index,preempt = 1,prevTopReadyPriority;
	TCB *result;
	 /*	The following part is commenetd because we are 
		not modelling the case for suspending the scheduler 
		and we are not verifying the amount of processor 
		time used by a task etc
	 */
////////////////////////////////////////////////////////////
/*
	if( uxSchedulerSuspended != 
		( unsigned portBASE_TYPE ) pdFALSE )
	{
		/*	The scheduler is currently suspended - 
			do not allow a context
			switch. STAR/
		xMissedYield = pdTRUE;
		return;
	}

	traceTASK_SWITCHED_OUT();

	#if ( configGENERATE_RUN_TIME_STATS == 1 )
	{
		unsigned long ulTempCounter = 
				portGET_RUN_TIME_COUNTER_VALUE();
	}
	#endif

	taskFIRST_CHECK_FOR_STACK_OVERFLOW();
	taskSECOND_CHECK_FOR_STACK_OVERFLOW();
*/
////////////////////////////////////////////////////////////

	/*	The following loop is commented because nonempty 
		list at index 'topReadyPriority' is assured by 
		an invariant in readyLists.
	*/
///////////////////////////////////////////////////////////
	/*	Find the highest priority queue that 
		contains ready tasks. 
	while( listLIST_IS_EMPTY( 
		&( pxReadyTasksLists[ uxTopReadyPriority ] ) ) )
	{
		--uxTopReadyPriority;
	}
	*/
/////////////////////////////////////////////////////////////
	//listGET_OWNER_OF_NEXT_ENTRY( pxCurrentTCB, 
    //			&( pxReadyTasksLists[ uxTopReadyPriority ] ) );

	/*	Call to the above xList operation is replaced with the 
		call to the newly introduced function below.
		This is because, the above function fails in 
		getting longest waiting task at index 'topReadyPriority'
	*/

///////////////////////////////////////////////////////////
	prevTopReadyPriority = rdyLists->topReadyPriority + 1;
	_(unwrap (&sstm) )
	_(ghost (&sstm)->\owns -= rdyLists )
	_(unwrap rdyLists)
	_(ghost rdyLists->\owns -= 
			rdyLists->ready[rdyLists->topReadyPriority] )	
	while( listIsEmpty( rdyLists->ready[rdyLists->topReadyPriority] ) )
		_(invariant \exists unsigned i;
			(	( i <= rdyLists->topReadyPriority ) &&
				( rdyLists->ready[i]->length!=0 )
			)
		 )
		_(invariant rdyLists->topReadyPriority < maxPrio ) 
		_(invariant \thread_local_array(rdyLists->ready,MAXSIZE) )
		_(invariant maxPrio <= MAXSIZE )
		_(invariant rdyLists->topReadyPriority < prevTopReadyPriority )
	{
		_(ghost rdyLists->\owns += 
			rdyLists->ready[rdyLists->topReadyPriority] )	
		prevTopReadyPriority = rdyLists->topReadyPriority;
		--rdyLists->topReadyPriority;
		_(ghost rdyLists->\owns -= 
			rdyLists->ready[rdyLists->topReadyPriority] )
	}
	_(ghost rdyLists->\owns += 
		rdyLists->ready[rdyLists->topReadyPriority] )
	_(wrap rdyLists)
	_(ghost (&sstm)->\owns -= rdyLists )
	_(wrap (&sstm) )
	return result;
/////////////////////////////////////////////////////////////
}


TCB* vTaskSwitchContextT( unsigned arr[MAXSIZE], unsigned topReadyPriority )
{
	unsigned index;
	TCB *result;
	 /*	The following part is commenetd because we are 
		not modelling the case for suspending the scheduler 
		and we are not verifying the amount of processor 
		time used by a task etc
	 */
////////////////////////////////////////////////////////////
/*
	if( uxSchedulerSuspended != 
		( unsigned portBASE_TYPE ) pdFALSE )
	{
		/*	The scheduler is currently suspended - 
			do not allow a context
			switch. STAR/
		xMissedYield = pdTRUE;
		return;
	}

	traceTASK_SWITCHED_OUT();

	#if ( configGENERATE_RUN_TIME_STATS == 1 )
	{
		unsigned long ulTempCounter = 
				portGET_RUN_TIME_COUNTER_VALUE();
	}
	#endif

	taskFIRST_CHECK_FOR_STACK_OVERFLOW();
	taskSECOND_CHECK_FOR_STACK_OVERFLOW();
*/
////////////////////////////////////////////////////////////

	/*	The following loop is commented because nonempty 
		list at index 'topReadyPriority' is assured by 
		an invariant in readyLists.
	*/
///////////////////////////////////////////////////////////
	/*	Find the highest priority queue that 
		contains ready tasks. 
	*/
	
	//_(unwrap (&sstm) )
	//_(ghost (&sstm)->\owns -= rdyLists )
	//_(unwrap rdyLists)
	unsigned prevTopReadyPriority = topReadyPriority + 1;
	while( arr[topReadyPriority] == 0 )
		_(invariant \exists unsigned i;
					(( i <= topReadyPriority ) && ( arr[i] != 0 ) )
		 )
		_(invariant topReadyPriority < maxPrio ) 
		_(invariant \thread_local_array(arr,MAXSIZE) )
		_(invariant maxPrio <= MAXSIZE )
		_(invariant topReadyPriority < maxPrio ) 
		_(invariant topReadyPriority < prevTopReadyPriority )
	{	
		prevTopReadyPriority = topReadyPriority;
		--topReadyPriority;

	}

	//_(wrap rdyLists)
	//_(ghost (&sstm)->\owns += rdyLists )
	//_(wrap (&sstm) )
/////////////////////////////////////////////////////////////
	//listGET_OWNER_OF_NEXT_ENTRY( pxCurrentTCB, 
    //			&( pxReadyTasksLists[ uxTopReadyPriority ] ) );

	/*	Call to the above xList operation is replaced with the 
		call to the newly introduced function below.
		This is because, the above function fails in 
		getting longest waiting task at index 'topReadyPriority'
	
	_(unwrap (&sstm) )
	_(ghost (&sstm)->\owns -= rdyLists )
	_(unwrap rdyLists)
	_(ghost rdyLists->\owns -= 
			rdyLists->ready[rdyLists->topReadyPriority] )
	_(ghost (&sstm)->\owns -= \embedding(&pxCurrentTCB) )
	_(ghost (&sstm)->\owns -= pxCurrentTCB )
	_(assert \wrapped(pxCurrentTCB) )
	_(unwrap pxCurrentTCB )
	_(assert \writable(pxCurrentTCB) )
	result = getOwnerOfFirstEntry(rdyLists->ready
						[rdyLists->topReadyPriority]);
	_(wrap pxCurrentTCB )
	_(ghost (&sstm)->\owns += pxCurrentTCB )
	_(ghost (&sstm)->\owns += \embedding(&pxCurrentTCB) )
	_(ghost rdyLists->\owns += 
			rdyLists->ready[rdyLists->topReadyPriority] )
	_(wrap rdyLists)
	_(ghost (&sstm)->\owns += rdyLists )
	//traceTASK_SWITCHED_IN();
	//vWriteTraceToBuffer();
	_(wrap (&sstm))
	*/
	return result;
}

unsigned taskPriorityGet( TCB *pxTCB )
	{
	unsigned result;


//		portENTER_CRITICAL();
		{
			/* If null is passed in here then we are changing the
			priority of the calling function. */
//			pxTCB = prvGetTCBFromHandle( pxTask );
			result = pxTCB->uxPriority;
		}
//		portEXIT_CRITICAL();

		return result;
	}


unsigned isTaskSuspended( TCB *pxTCB )
{
	unsigned xReturn = 0;
//	onst tskTCB * const pxTCB = ( tskTCB * ) xTask;

	/* Is the task we are attempting to resume actually in the
	suspended list? */
	_( unwrap (&sstm) )
	_(ghost (&sstm)->\owns -= suspended )
	if( containedWithinF(suspended, pxTCB->pvGenericListItem) )
	{
		/* Has the task already been resumed from within an ISR? */
//		if( listIS_CONTAINED_WITHIN( &xPendingReadyList, &( pxTCB->xEventListItem ) ) != pdTRUE )
//		{
			/* Is it in the suspended list because it is in the
			Suspended state?  It is possible to be in the suspended
		list because it is blocked on a task with no timeout
			specified. */
//			if( listIS_CONTAINED_WITHIN( NULL, &( pxTCB->xEventListItem ) ) == pdTRUE )
			{
				xReturn = 1;
			}
//		}
	}
	_(ghost (&sstm)->\owns += suspended )
	_( wrap (&sstm) )
	return xReturn;
}


void taskResume( TCB *pxTCB )
{
//	tskTCB *pxTCB;
	/*	Remove the task from whichever list it is currently in, and place
		it in the ready list. */
//	pxTCB = ( tskTCB * ) pxTaskToResume;

	/*	The parameter cannot be NULL as it is impossible to resume the
		currently executing task. */
	if( ( pxTCB != NULL ) && ( pxTCB != pxCurrentTCB ) )
	{
//		portENTER_CRITICAL();
		{
//			if( isTaskSuspended( pxTCB ) == 1 )
			{
//				traceTASK_RESUME( pxTCB );
				/* As we are in a critical section we can access the ready
				lists even if the scheduler is suspended. */
				_( unwrap ( & sstm ) )
				_(ghost (&sstm)->\owns -= suspended )
				//_(assert \thread_local(pxTCB->pvEventListItem) )
				listRemove(suspended,pxTCB->pvGenericListItem );
				//_(assert \thread_local(pxTCB->pvEventListItem) )
				_(ghost (&sstm)->\owns += suspended )
				_( unwrap pxTCB )
				_( assert ( pxTCB->uxPriority < maxPrio ) )
				_(ghost (&sstm)->\owns -= rdyLists )
				_(unwrap rdyLists )
				if( pxTCB->uxPriority > rdyLists->topReadyPriority )
				{
					rdyLists->topReadyPriority = pxTCB->uxPriority;
				}

				_(ghost rdyLists->\owns -= rdyLists->ready[pxTCB->uxPriority])
				//prvAddTaskToReadyQueue( pxTCB );
				listInsertEnd(rdyLists->ready[pxTCB->uxPriority], 
								pxTCB->pvGenericListItem);


				_(ghost rdyLists->\owns += rdyLists->ready[pxTCB->uxPriority])
				_(wrap rdyLists )
				_(ghost (&sstm)->\owns += rdyLists )
				_( wrap pxTCB )
				/* We may have just resumed a higher priority task. */
				if( pxTCB->uxPriority >= pxCurrentTCB->uxPriority )
				{
					/* This yield may not cause the task just resumed to run, but
					will leave the lists in the correct state for the next yield. */
//					portYIELD_WITHIN_API();
//					_( unwrap pxCurrentTCB )
//					pxCurrentTCB = pxTCB;
//					_( wrap pxCurrentTCB )
				}
				_( wrap ( & sstm ) )
				_( assert ( pxTCB->uxPriority == \old( pxTCB->uxPriority ) ) )
			}
		}
//		portEXIT_CRITICAL();
	}
}


void endScheduler(  )
{
	/* Stop the scheduler interrupts and call the portable scheduler end
	routine so the original ISRs can be restored if necessary.  The port
	layer must ensure interrupts enable	bit is left in the correct state. */
//	portDISABLE_INTERRUPTS();
	_( unwrap ( & sstm ) )
	schedulerRunning = fls;
	_( wrap ( & sstm ) )
	//vPortEndScheduler();
}

unsigned getTickCount(  )
{
unsigned xTicks;

	/* Critical section required if running on a 16 bit processor. */
//	portENTER_CRITICAL();
	{
		xTicks = xTickCount;
	}
//	portEXIT_CRITICAL();

	return xTicks;
}

void taskGenericCreate( TCB *pxTCB, unsigned priority )
{
	_( unwrap ( &sstm ) )
	//_( unwrap ( pxTCB ) )
	( &sstm )->size = ( &sstm )->size + 1;
	_( ghost ( &sstm )->taskSet[ ( &sstm )->size ] = pxTCB )
	_( ghost ( &sstm )->position[ ( &sstm )->taskSet[ ( &sstm )->size ] ] = ( &sstm )->size )
	_( ghost ( &sstm )->\owns +=  ( &sstm )->taskSet[ ( &sstm )->size ] )
//	_( wrap ( &sstm ) )

//	portENTER_CRITICAL();
//	uxCurrentNumberOfTasks++; 
//	( &sstm )->size represents this number and already incremented
	_( ghost ( &sstm )->\owns -=  pxCurrentTCB )
	_( unwrap pxCurrentTCB )
	if( ( &sstm )->size  == 1 )
	{
			/* As this is the first task it must also be the current task. */
			pxCurrentTCB =  pxTCB;		
//			prvInitialiseTaskLists(); // Done as a separate initialisation API
	}
	else
	{
		_( assert \writable( pxCurrentTCB  ) )
		/* If the scheduler is not already running, make this task the
		current task if it is the highest priority task to be created
		so far. */
		if( schedulerRunning == fls )
		{
			if( pxCurrentTCB->uxPriority < pxTCB->uxPriority )// Condition changed to verufy the code
			{
				_( assert \writable( pxCurrentTCB  ) )
				pxCurrentTCB = pxTCB;
			}
		}		
	}



	/* Remember the top priority to make context switching faster.  Use
	the priority in pxNewTCB as this has been capped to a valid value. STAR/
	if( pxTCB->uxPriority > rdyLists->topReadyPriority )
	{
		rdyLists->topReadyPriority = pxTCB->uxPriority;
	}
	#if ( configUSE_TRACE_FACILITY == 1 )
	{
		/* Add a counter into the TCB for tracing only. STAR/
		pxNewTCB->uxTCBNumber = uxTaskNumber;
	}
	#endif
	uxTaskNumber++;*/

	_(ghost (&sstm)->\owns -= rdyLists )
	_(unwrap rdyLists )
	_(ghost rdyLists->\owns -= rdyLists->ready[pxTCB->uxPriority])
	listInsertEnd(rdyLists->ready[pxTCB->uxPriority], 
								pxTCB->pvGenericListItem);
	_(ghost rdyLists->\owns += rdyLists->ready[pxTCB->uxPriority])
	_(wrap rdyLists )
	_(ghost (&sstm)->\owns += rdyLists )

/*	
	prvAddTaskToReadyQueue( pxNewTCB );
	xReturn = pdPASS;
	traceTASK_CREATE( pxNewTCB );*/
//		portEXIT_CRITICAL();
	
	_( wrap ( &sstm ) )
/*

	if( xReturn == pdPASS )
	{
		if( ( void * ) pxCreatedTask != NULL )
		{
			/* Pass the TCB out - in an anonymous way.  The calling function/
			task can use this as a handle to delete the task later if
			required.STAR/
			*pxCreatedTask = ( xTaskHandle ) pxNewTCB;
		}

		if( xSchedulerRunning != pdFALSE )
		{
			/* If the created task is of a higher priority than the current task
			then it should run now. STAR/
			if( pxCurrentTCB->uxPriority < uxPriority )
			{
				portYIELD_WITHIN_API();
			}
		}
	}

	return xReturn;
*/
}


void taskPlaceOnEventList( TCB *pxTCB, unsigned xTicksToWait )
{
	unsigned xTimeToWake;
	_( unwrap &sstm )
	_( ghost ( &sstm )->\owns -= blocked )
	/* THIS FUNCTION MUST BE CALLED WITH INTERRUPTS DISABLED OR THE
	SCHEDULER SUSPENDED. */

	/* Place the event list item of the TCB in the appropriate event list.
	This is placed in the list in priority order so the highest priority task
	is the first to be woken by the event. */
	listInsert(blocked, pxTCB->pvEventListItem);
	_( ghost ( &sstm )->\owns += blocked )

	/* We must remove ourselves from the ready list before adding ourselves
	to the blocked list as the same list item is used for both lists.  We have
	exclusive access to the ready lists as the scheduler is locked. */
	_(ghost rdyLists->\owns -= rdyLists )
	_(unwrap rdyLists )
	_(ghost rdyLists->\owns -= rdyLists->ready[pxTCB->uxPriority] )
	listRemove( rdyLists->ready[ pxTCB->uxPriority ],pxTCB->pvGenericListItem );
	_(ghost rdyLists->\owns += rdyLists->ready[pxTCB->uxPriority] )
	_(wrap rdyLists )
	_(ghost rdyLists->\owns += rdyLists )

	if( xTicksToWait == maxNumVal )
	{
		_(ghost (&sstm)->\owns -= suspended )
		listInsert(suspended, pxTCB->pvGenericListItem);
		_(ghost (&sstm)->\owns += suspended )
	}
	else
	{
		/* Calculate the time at which the task should be woken if the event does
		not occur.  This may overflow but this doesn't matter. */
//		xTimeToWake = xTickCount + xTicksToWait;

		/*	For the above statement, developer seems to have 
			assumed modulo 'maxNumVal+1' addition. But it is not 
			very clear whether the addition is always modulo for 
			unsigned numbers as per the C standard.
			In spite of this, VCC will allow addition
			only if it knows that the result is within the 
			limit. 
			Hence we rewrite the above statement to an equivalent
			block as below to ensure addition modulo 'maxNumVal+1'
			such that result of all sub expressions are within 
			the limit of the data type.
		*/
		if( xTicksToWait <= ( maxNumVal - xTickCount ) )
		{
			xTimeToWake = xTickCount + xTicksToWait ;	
		}
		else
		{
			xTimeToWake =  xTicksToWait - ( maxNumVal - xTickCount ) - 1;	
		}
		setItemValue( pxTCB->pvGenericListItem, xTimeToWake );
		/*	The condition in the following if statement is 
			rewritten to an equivalent condition to 
			avoid the overflow problem in VCC
		*/
		if( xTicksToWait <= ( maxNumVal - xTickCount ) )
		{
			_(ghost (&sstm)->\owns -= delayed )
			listInsert(delayed, pxCurrentTCB->pvGenericListItem);
			_(ghost (&sstm)->\owns += delayed )
		}
		else
		{
			_(ghost (&sstm)->\owns -= oDelayed )
			listInsert(oDelayed, pxCurrentTCB->pvGenericListItem);
			_(ghost (&sstm)->\owns += oDelayed )
		}

}

unsigned getNumberOfTasks(  )
{
	return uxCurrentNumberOfTasks;
}




/*
*/