#include <vcc.h>
#include "xListMap.h" 




enum boolean {tru,fls};

 _(logic \bool isListEmpty(xMap *xList) = ( (xList->length==0) ? 1 : 0  ) )

_(dynamic_owns)
typedef struct rdyLsts{
	/*	ith element in the following array 
		is the pointer to the FIFO queue of 
		tasks with priority i 
	*/
	xMap *ready[MAXSIZE];

	/*	Following field gives the index of 
		the highest index nonempty FIFO list
	*/
	unsigned topReadyPriority;

	/*	Following ghost field represents the 
		maximum priority value, which is same 
		as the value of the global variable 
		'maxPrio' and is asserted as an invariant 
		in the structure 'System'.
	*/
	_(ghost unsigned  mP)

	/*	INV-0: Maximum priority is within the 
		array MAXSIZE
	*/
	_(invariant mP<MAXSIZE )

	/*INV-1: each list in ready is a FIFO queue*/
	_(invariant \forall unsigned i; 
		( i<mP ) ==>
			( \mine(ready[i]) && (ready[i]->type==FIFO) )
	 )

	/*	INV-2: priority of tasks in each list 
		same as  the index
	*/
	 _(invariant \forall unsigned i;
			( i<mP )  ==> 
				( ( ready[i]->type==FIFO) && \mine(ready[i]) 
					&& (ready[i]->priority == i) 
				)
	  )

	/*	INV-3a : topReadyPriority gives the index of 
		a nonempty ready list
	*/
	_(invariant (	(topReadyPriority<mP) && 
					\mine(ready[topReadyPriority]) &&
					( !isListEmpty(ready[topReadyPriority] ) ) 
				)
	 )

	/*	INV-3b : topReadyPriority gives the index of 
		the highest nonempty ready list
	*/
	_(invariant \forall unsigned i; 
			( (i>topReadyPriority) && (i<mP) ) ==>
			( \mine(ready[i]) && ( isListEmpty(ready[i]) ) ) 
	 )

	/*	INV-4 : ready lists are distinct
	*/
	_(invariant \forall unsigned i,j; 
			(	( i < mP ) && ( j < mP ) && ( i != j ) && 
				\mine(ready[i]) && \mine(ready[j]) 
			) ==> ( ready[i] != ready[j] )
	 )
}readyLists;

////////////////////////////////
//Global data strucures


/*	Following variable represents the global variable 
	'maxPrio', can be initialised by the user.
	(for parameterized verification)
*/
unsigned maxPrio;

/*	Following variable represents the global variable 
	'maxNumVal', can be initialised by the user.
	(for parameterized verification)
*/
unsigned maxNumVal;

/*	Following variable represents the global variable 
	'preemption', can be initialised by the user.
	(for parameterized verification)
*/
boolean preemption;

/*	Following variable represents the global variable 
	'schedulerRunning', can be initialised by the user.
	(for parameterized verification)
*/
boolean schedulerRunning;

//	Following variable represents the system clock
unsigned xTickCount;

/*	Following pointer variable represents the 
	running task in the system.
*/
TCB *pxCurrentTCB;

//	Following variable represents the number of tasks in the system
unsigned uxCurrentNumberOfTasks;


/*	Following pointer variable represents the 
	idle task in the system.
*/
TCB *pxIdleTCB;

/*	Following pointer variable represents the set 
	of ready lists
*/
readyLists *rdyLists;

/*	Following pointer variable represents the list 
	of delayed tasks in the system, where value of 
	time to awake is less than maxNumVal
*/
xMap *delayed;

/*	Following pointer variable represents the list 
	of delayed tasks in the system, where the 
	value of time to awake is less than or equal to 
	the current value of clock.
*/
xMap *oDelayed;

/*	Following pointer variable represents a list of 
	blocked tasks in the system
*/
xMap *blocked;

/*	Following pointer variable represents a list of 
	suspended tasks in the system.
*/
xMap *suspended;

/*	Following pointer variable represents a list of 
	deleted tasks in the system
*/
xMap *deleted;

////////////////////////////////


/*	Following structure owns the global data objects 
	in the system. Properties on global objects are 
	specified as invariants in this structure.
*/
 _(dynamic_owns)
typedef struct systm{

	/*	Following field represents the number of tasks 
		in the system 
	*/
	unsigned size;

	/*	Following map represent the ordered set of 
		tasks in the system, for a given index say i 
		between 1 and size, 'taskSet' maps 'i' to the 
		task 't' in the system such that 't' is the 
		ith task in 'taskSet' .
	*/
	_(ghost TCB *taskSet[unsigned] )

	/*	Following map gives the index of a given task 
		in the oerdered set, for a given task 't' in 
		the system, 'position' maps 't' to a unique 
		index 'i' between 1 and 'size' such that 't' 
		is the ith task in 'taskSet'. 
	*/
	_(ghost unsigned position[TCB*] )

	//	System owns the global varaible 'maxPrio'
	_(invariant \mine(\embedding(&maxPrio)) )
	_(invariant maxPrio < MAXSIZE )

	//	System owns the global varaible 'maxNumVal'
	_(invariant \mine(\embedding(&maxNumVal)) )
	_(invariant maxNumVal <= MAXSIZE )

	//	System owns the global varaible 'schedulerRunning'
	_(invariant \mine(\embedding(&preemption)) )

	//	System owns the global varaible 'schedulerRunning'
	_(invariant \mine(\embedding(&schedulerRunning)) )

	//	System owns the global varaible 'xTickCount'
	_(invariant \mine(\embedding(&xTickCount)) )
	_(invariant xTickCount <= maxNumVal )

	/*	System owns in the set of ready 
		lists 'rdyLists'.
	*/
	_(invariant \mine(\embedding(&rdyLists)) )
	_(invariant \mine(rdyLists) )
	
	/*	The filed 'mP' in the set of ready  lists 
		owned by  the system agrees with the value 
		of the global variable 'maxPrio'.
	*/
	_(invariant \mine(rdyLists) ==> 
					rdyLists->mP==maxPrio 
	 )

	//	System owns the running task
	_(invariant \mine(\embedding(&pxCurrentTCB)) )
	_(invariant \mine(pxCurrentTCB) )

	//	System owns the idle task
	_(invariant \mine(\embedding(&pxIdleTCB)) )
	_(invariant \mine(pxIdleTCB) )

	//	System owns the global variable 'uxCurrentNumberOfTasks'
	_(invariant \mine(\embedding(&uxCurrentNumberOfTasks)) )

	//	System owns the the list of delayed tasks
	_(invariant \mine(\embedding(&delayed)) )
	_(invariant \mine(delayed) )

	/*	System owns the the list of overflow 
		delayed tasks
	*/
	_(invariant \mine(\embedding(&oDelayed)) )
	_(invariant \mine(oDelayed) )

	//	System owns the the list of blocked tasks 
	_(invariant \mine(\embedding(&blocked)) )
	_(invariant \mine(blocked) )

	//	System owns the the list of suspended tasks 
	_(invariant \mine(\embedding(&suspended)) )
	_(invariant \mine(suspended) )

	//	System owns the the list of deleted tasks 
	_(invariant \mine(\embedding(&deleted)) )
	_(invariant \mine(deleted) )

	//	'delayed' is a priority queue
	_(invariant delayed->type == PQ ) 
	
	//	'oDelayed' is a priority queue
	_(invariant oDelayed->type == PQ )

	//	'blocked' is a priority queue
	_(invariant blocked->type == PQ )

	/*	'suspended' is a priority queue (here the 
		type is irrelevant and assumed as PQ )
	*/
	_(invariant suspended->type == PQ )

	//	'deleted' is a priority queue
	_(invariant deleted->type == PQ )

	//	Maximum number of tasks is bounded by MAXSIZE
	_(invariant size <= MAXSIZE )

	//	System owns all valid tasks in the system 
	_(invariant \forall unsigned i;
		( ( i > 0 ) && (i <= size ) ) ==> 
			( ( taskSet[i] != NULL ) && 
				\mine(taskSet[i]) 
			)
	 )

	//	All invalid position contains NULL value 
	_(invariant \forall unsigned i;
		( ( i == 0 ) || (i > size ) ) ==> 
			( ( taskSet[i] == NULL ) && 
			  !\mine(taskSet[i]) 
			)
	 )

	 //	Each valid tasks has a right index in taskSet 
	_(invariant \forall TCB *t;
		( \mine(t) ) ==> 
			( ( position[t] > 0 ) && 
			  ( position[t] <= size ) 
			)	
	 )

	 //	'position' and 'taskSet' are in sync 
	_(invariant \forall TCB *t;
		( \mine(t) ) ==> ( taskSet[position[t]] == t )	
	 )

	 //	'position' and 'taskSet' are in sync 
	_(invariant \forall unsigned i;
		( ( i > 0 ) && (i <= size ) ) ==> 
				( position[taskSet[i]] == i )
	 )

	// tasks are distinct 
	_(invariant \forall TCB *T1,*T2;
		(	\mine(T1) && \mine(T2) && 
			( position[ T1 ] != position[ T2 ] ) 
		) ==>  ( T1 != T2 ) 
	 )

	// position of an invalid task is zero 
	_(invariant \forall TCB *t;
		( !\mine(t) )	<==> ( position[t] == 0 ) 
	 )

	// All task have priority value within the limit
	_(invariant \forall TCB *t;
		( \mine(t) )	==> ( t->uxPriority <= maxPrio ) 
	 )

	//	Task lists are distinct
	_(invariant ( delayed != oDelayed ) )
	_(invariant ( delayed != blocked ) )
	_(invariant ( oDelayed != blocked ) )
	_(invariant ( delayed != suspended ) )
	_(invariant ( oDelayed != suspended ) )
	_(invariant ( blocked != suspended ) )
	_(invariant ( delayed != deleted ) )
	_(invariant ( oDelayed != deleted ) )
	_(invariant ( blocked != deleted ) )
	_(invariant ( suspended != deleted ) )
}System;

System sstm;



void initSystem( System *system, unsigned mP, 
				unsigned mD, boolean preempt, boolean sR )
	_(requires \program_entry_point() )
	_(requires system->\owns=={} )
	_(requires \mutable(system))

	_(requires ( delayed != oDelayed ) )
	_(requires ( delayed != blocked ) )
	_(requires ( oDelayed != blocked ) )
	_(requires ( delayed != suspended ) )
	_(requires ( oDelayed != suspended ) )
	_(requires ( blocked != suspended ) )
	_(requires ( delayed != deleted ) )
	_(requires ( oDelayed != deleted ) )
	_(requires ( blocked != deleted ) )
	_(requires ( suspended != deleted ) )

	_(requires mP < MAXSIZE )
	_(requires mD <= MAXSIZE )

	_(writes \span(system) )


	_(writes \span(delayed) )
	_(writes \span(oDelayed) )
	_(writes \span(blocked) )
	_(writes \span(suspended) )
	_(writes \span(deleted) )

	_(writes &maxPrio )
	_(writes &maxNumVal )
	_(writes &preemption )
	_(writes &schedulerRunning )
	_(writes &xTickCount )
	_(writes \embedding(&maxPrio) )
	_(writes \embedding(&maxNumVal) )
	_(writes \embedding(&preemption) )
	_(writes \embedding(&schedulerRunning) )
	_(writes \embedding(&xTickCount) )

	_(writes pxCurrentTCB )
	
	_(ensures ( maxPrio == mP ) )
	_(ensures ( maxNumVal == mD ) )
	_(ensures ( preemption == preempt ) )
	_(ensures ( schedulerRunning == sR ) )
	//_(ensures \false )
	;



_( logic \bool containedIn(xMap *ready,  xListItem *xli ) =
	(
		( xli \in ready->\owns )  ? 1 : 0
	)
 )

 _( logic \bool presentIn(xMap *list,  xListItem *xli ) =
	(
		( xli->pvContainer == list ) ? 1 : 0
	)
 )

 
 _( logic \bool InvariantOnRunningTask(readyLists *rl,  
									TCB *pxCurrntTCB ) =
	(
		\forall unsigned i; ( (i>rl->topReadyPriority) && 
				(i<rl->mP) ) ==> ( isListEmpty(rl->ready[i]) )
	)
  )


 _( logic \bool indexMatchesPriority( xMap *xList, 
			unsigned index ) = 
		( \forall unsigned j; ( j<xList->length ) ==> 
			( xList->list[j]->pvOwner->uxPriority == index )  
		)
  )
/*  
	In xList there is no MAXSIZE on the number of nodes. 
	But it is in fact bounded by the amount of memory.
	Hence assuming a MAXSIZE for the maximum number of 
	elements in xListMap is not really a restrion.
	Such a MAXSIZE is demanded by the map based 
	modelling of lists.
*/

////////////////////////////////////////////////////////////////////////////////////
 void vTaskDelay( unsigned xTicksToDelay )
	_(requires schedulerRunning == tru )
 	_(requires xTicksToDelay <= maxNumVal )
	_(requires pxCurrentTCB != pxIdleTCB )

	/*	The following requirements are ownership related or
		to satisfy the MAXSIZE for array or, 
		to ensure that there is enough room 
		in the list for inserting a new element or
		to ensure the invariants on the concerned 
		list in the post state.
	*/
	_(requires \wrapped(&sstm) )

	_(requires pxCurrentTCB->pvEventListItem 
							\in (&sstm)->\owns  )

	_(requires pxCurrentTCB->uxPriority < maxPrio )

	_(requires 
		( xTicksToDelay <= ( maxNumVal - xTickCount ) ) ==>
			(	\forall unsigned i; ( i < delayed->length ) ==> 
					( delayed->list[i]->pvOwner != 
						pxCurrentTCB->pvGenericListItem->pvOwner 
					) 
			)
	 )
	 _(requires ( xTicksToDelay <= ( maxNumVal - xTickCount ) ) ==> 
			( delayed->length < MAXSIZE ) )

	_(requires ( xTicksToDelay > ( maxNumVal - xTickCount ) ) ==>
			(	\forall unsigned i; 
				( i < oDelayed->length ) ==> 
					( oDelayed->list[i]->pvOwner != 
					  pxCurrentTCB->pvGenericListItem->pvOwner 
					) 
			)
	 )
	 _(requires ( xTicksToDelay > ( maxNumVal - xTickCount ) ) ==> 
			( oDelayed->length < MAXSIZE ) )

	_(requires 
		pxCurrentTCB->pvGenericListItem->pvOwner->uxPriority <= 
		MAXSIZE 
	)

	_(requires containedIn( rdyLists->ready[pxCurrentTCB->uxPriority], 
				pxCurrentTCB->pvGenericListItem ) )

	_(requires pxCurrentTCB->pvGenericListItem \in 
				rdyLists->ready[pxCurrentTCB->uxPriority]->\owns  )

	_(writes &sstm )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )

	_(ensures ( xTicksToDelay == 0 ) ==> 
					(	\forall unsigned i; ( i < maxPrio )  ==> 
							( rdyLists->ready[i] == 
								\old(rdyLists->ready[i]) 
							)
					)
	 )

	_(ensures ( xTicksToDelay == 0 ) ==> 
					(	\forall unsigned i; ( i < maxPrio )  ==> 
							(	\forall unsigned j; 
								( j < rdyLists->ready[i]->length ) ==>
									( rdyLists->ready[i]->list[j] == 
									\old(rdyLists->ready[i]->list[j]) ) 
							)
					)
	 )

	/*	Following 3 conditions ensures the correct update on 
		ready lists when the task needs to be delayed
	*/
	_(ensures ( xTicksToDelay > 0 ) ==>
		( !containedIn(rdyLists->ready[pxCurrentTCB->uxPriority],
			pxCurrentTCB->pvGenericListItem) 
		) 
	 )

	_(ensures ( xTicksToDelay > 0 ) ==>
		(	rdyLists->ready[pxCurrentTCB->uxPriority]->length ==
			(\old(rdyLists->ready[pxCurrentTCB->uxPriority]->length) - 1)
		) 
	 )

	_(ensures \forall unsigned i; 
		( i<\old(rdyLists->ready[pxCurrentTCB->uxPriority]->
			     position[pxCurrentTCB->pvGenericListItem]) ) ==> 
		( rdyLists->ready[pxCurrentTCB->uxPriority]->list[i] == 
			\old(rdyLists->ready[pxCurrentTCB->uxPriority]->list[i]) 
		)
	 )

	_(ensures \forall unsigned i; 
		( xTicksToDelay > 0 ) ==>
			(	( ( i >= \old(rdyLists->ready[pxCurrentTCB->uxPriority]->
						  position[\old(pxCurrentTCB->pvGenericListItem)]) ) &&
					   ( i < rdyLists->ready[pxCurrentTCB->uxPriority]->length ) 
				) ==> ( rdyLists->ready[pxCurrentTCB->uxPriority]->list[i] == 
						\old(rdyLists->ready[pxCurrentTCB->uxPriority]->list[i+1]) 
					  ) 
			)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( xTicksToDelay == 0 ) ==> ( delayed == \old(delayed)	) )
	_(ensures ( xTicksToDelay == 0 ) ==> ( oDelayed == \old(oDelayed) ) )

	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> ( oDelayed == \old(oDelayed) ) 
	 )

	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> ( delayed == \old(delayed) ) 
	 )

//////////////////////////////////
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> 
			  (
					delayed->length == ( \old(delayed->length) + 1 )
			  )
	 )	

	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> ( delayed->position[pxCurrentTCB->pvGenericListItem] <
					  delayed->length
					) 

	 )	

	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> 
			  (
					\forall unsigned i; 
						( i<delayed->position[pxCurrentTCB->pvGenericListItem] ) 							
						   ==> ( delayed->list[i]==\old(delayed->list[i]) )
			  )
	 )	
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> ( delayed->list[delayed->position[pxCurrentTCB->pvGenericListItem]]==
						pxCurrentTCB->pvGenericListItem 
					) 

	 )	
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> 
			  (
					\forall unsigned i; 
						( ( i>delayed->position[pxCurrentTCB->pvGenericListItem] ) && 
						  ( i<delayed->length ) 
						) ==> ( delayed->list[i]==\old(delayed->list[i-1] ) )
			  )
	 )	
	_(ensures ( ( xTicksToDelay > 0 ) && 
				( xTicksToDelay <= ( maxNumVal - xTickCount ) ) 
			  ) ==> (	pxCurrentTCB->pvGenericListItem->xItemValue == 
						(xTicksToDelay+xTickCount) 
					) 
	 )

//////////////////////////////////
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> 
			  (
					oDelayed->length == ( \old(oDelayed->length) + 1 )
			  )
	 )	
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> ( oDelayed->position[pxCurrentTCB->pvGenericListItem] <
					  oDelayed->length 
					) 
	 )

	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> 
			  (
					\forall unsigned i; 
						( i<oDelayed->position[pxCurrentTCB->pvGenericListItem] ) 
						  ==> ( oDelayed->list[i]==\old(oDelayed->list[i]) )
			  )
	 )	
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> ( oDelayed->list[oDelayed->position[pxCurrentTCB->pvGenericListItem]]==
						pxCurrentTCB->pvGenericListItem 
					) 

	 )	
	_(ensures ( 	( xTicksToDelay > 0 ) && 
					( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> 
			  (
					\forall unsigned i; 
						( ( i>oDelayed->position[pxCurrentTCB->pvGenericListItem] ) && 
						  ( i<oDelayed->length ) 
						) ==> ( oDelayed->list[i]==\old(oDelayed->list[i-1] ) )
			  )
	 )	
	_(ensures ( ( xTicksToDelay > 0 ) && 
				( xTicksToDelay > ( maxNumVal - xTickCount ) ) 
			  ) ==> (	pxCurrentTCB->pvGenericListItem->xItemValue == 
						( xTicksToDelay - ( maxNumVal - xTickCount ) - 1 ) 
					) 
	 )
//////////////////////////////////

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i]->uxPriority == \old((&sstm)->taskSet[i]->uxPriority) )
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )
	/*	Property on 'topReadyPriority' is assured by the invariant 
		'rdyLists' which is assured by '\wrapped(&sstm)'.
	*/
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	//Following are conditions to ensure the ownership in VCC
	_(ensures pxCurrentTCB->pvGenericListItem->pvOwner == 
					\old(pxCurrentTCB->pvGenericListItem->pvOwner) )
	_(ensures rdyLists \in (&sstm)->\owns )
	_(ensures \wrapped(&sstm) )
	_(ensures pxCurrentTCB \in (&sstm)->\owns )
	_(ensures pxCurrentTCB->pvEventListItem \in (&sstm)->\owns  )
	//_(ensures \false ) 
	;


_( logic \bool needToDelay(unsigned xTC,  unsigned pWT, 
	unsigned xTI, unsigned maxNumVal ) =
	(
		( ( pWT <= xTC ) && ( xTI > ( xTC - pWT ) ) ) ||
		( ( pWT > xTC  ) && ( xTI > ( maxNumVal - ( pWT - xTC ) + 1 ) ) )
	)
 )

_( logic \bool needNoDelay(unsigned xTC,  unsigned pWT, 
	unsigned xTI, unsigned maxNumVal ) =
	(
		( ( pWT <= xTC ) && ( xTI <= ( xTC - pWT ) ) ) ||
		( ( pWT > xTC  ) && ( xTI <= ( maxNumVal - ( pWT - xTC ) + 1 ) ) )
	)
 )

_( logic \bool toDelayed(unsigned xTC,  unsigned pWT, 
	unsigned xTI, unsigned maxNumVal ) =
	(
		(	
			( pWT <= xTC ) &&  
			( xTI <= ( maxNumVal - pWT ) )
		) ||		
		(	
			( pWT > xTC ) 
		) 
	)
 )

 _( logic \bool toODelayed(unsigned xTC,  unsigned pWT, 
	unsigned xTI, unsigned maxNumVal ) =
	(
		(	
			( pWT <= xTC ) &&  
			( xTI > ( maxNumVal - pWT ) )
		) 
	)
 )


void vTaskDelayUntil( unsigned *pxPreviousWakeTime, unsigned xTimeIncrement )
	_(requires \mutable(pxPreviousWakeTime) )
	_(requires *pxPreviousWakeTime <= maxNumVal )
	_(requires xTimeIncrement <= maxNumVal )
	/*	The following requirements are ownership related and
		other ghost code related.
	*/
	_(requires \wrapped((&sstm)) )
	_(requires pxCurrentTCB->pvEventListItem \in (&sstm)->\owns  )
	_(requires pxCurrentTCB->uxPriority < maxPrio )
	_(requires containedIn( rdyLists->ready[pxCurrentTCB->uxPriority], 
										pxCurrentTCB->pvGenericListItem ) )
	_(requires pxCurrentTCB->pvGenericListItem \in 
				rdyLists->ready[pxCurrentTCB->uxPriority]->\owns  )

	_(requires	(   needToDelay(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) 
				) ==>	(	\forall unsigned i; ( i < delayed->length ) ==> 
							(	delayed->list[i]->pvOwner != 
								pxCurrentTCB->pvGenericListItem->pvOwner 
							) 
						)
	 )
	_(requires	(   needToDelay(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) 	
				) ==> ( delayed->length < MAXSIZE ) )
	_(requires	(   needToDelay(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal )
				) ==>	(	\forall unsigned i; ( i < oDelayed->length ) ==> 
							(	oDelayed->list[i]->pvOwner != 
								pxCurrentTCB->pvGenericListItem->pvOwner 
							) 
						)
	 )
	_(requires	(  needToDelay(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal )
				) ==> 
					( oDelayed->length < MAXSIZE ) )
	_(requires pxCurrentTCB->pvGenericListItem->pvOwner->uxPriority <= MAXSIZE )
	_(requires \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( &( (&sstm)->taskSet[i]->uxPriority ) != pxPreviousWakeTime )
			)
	 )
	_(writes (&sstm) )
	_(writes pxPreviousWakeTime )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures needNoDelay( xTickCount, \old(*pxPreviousWakeTime), 
				xTimeIncrement, maxNumVal ) ==> 
					(	\forall unsigned i; ( i< maxPrio )  ==> 
							( rdyLists->ready[i] == 
								\old(rdyLists->ready[i]) 
							)
					)
	 )
	_(ensures needNoDelay( xTickCount, \old(*pxPreviousWakeTime), 
				xTimeIncrement, maxNumVal ) ==> 
					(	\forall unsigned i;\forall unsigned j; ( i < maxPrio )  ==> 
							(	
								( j < rdyLists->ready[i]->length ) ==>
									( rdyLists->ready[i]->list[j] == 
									\old(rdyLists->ready[i]->list[j]) ) 
							)
					)
	 )
	//Following 3 conditions ensures the correct update on ready lists
	_(ensures needToDelay(xTickCount, \old(*pxPreviousWakeTime),
				xTimeIncrement, maxNumVal ) ==>
		(	rdyLists->ready[pxCurrentTCB->uxPriority]->length ==
			(\old(rdyLists->ready[pxCurrentTCB->uxPriority]->length) - 1)
		) 
	 )
	_(ensures 
		needToDelay(xTickCount, \old(*pxPreviousWakeTime), xTimeIncrement, maxNumVal )
			==>		!containedIn( rdyLists->ready[pxCurrentTCB->uxPriority],
											pxCurrentTCB->pvGenericListItem ) 
	 )
	_(ensures \forall unsigned i; 
		(	i<\old(rdyLists->ready[pxCurrentTCB->uxPriority]->
						position[pxCurrentTCB->pvGenericListItem]) 
		) ==>	(		rdyLists->ready[pxCurrentTCB->uxPriority]->list[i] == 
						\old(rdyLists->ready[pxCurrentTCB->uxPriority]->list[i]) 
				)
	 )
	_(ensures 
		needToDelay(xTickCount, \old(*pxPreviousWakeTime), xTimeIncrement, maxNumVal ) 
			==>		(	\forall unsigned i; 
						(	( i >= \old(rdyLists->ready[pxCurrentTCB->uxPriority]
								->position[\old(pxCurrentTCB->pvGenericListItem)]) 
							) &&
							( i < rdyLists->ready[pxCurrentTCB->uxPriority]->length ) 
						) ==> (		rdyLists->ready[pxCurrentTCB->uxPriority]->list[i] 
										== \old(rdyLists->ready[pxCurrentTCB->
												uxPriority]->list[i+1]) 
							  ) 
					)
	 )
////////////////////////////////////////////////////
	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )
	_(ensures needNoDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) ==> ( delayed == \old(delayed)	) )
	_(ensures needNoDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) ==> ( oDelayed == \old(oDelayed)	) )

	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) 	
			  ) ==> ( oDelayed == \old(oDelayed) ) 
	 )
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) &&
					toODelayed(xTickCount, *pxPreviousWakeTime, 
					xTimeIncrement, maxNumVal ) 	
			  ) ==> ( delayed == \old(delayed) ) 
	 )
////////////////////////////////////////////////////
//////////////////////////////////
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> 
			  (
					delayed->length == ( \old(delayed->length) + 1 )
			  )
	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> ( delayed->position[pxCurrentTCB->pvGenericListItem] <
					  delayed->length 
					) 

	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> 
			  (
					\forall unsigned i; 
						( i<delayed->position[pxCurrentTCB->pvGenericListItem] ) 
						  ==> ( delayed->list[i]==\old(delayed->list[i]) )
			  )
	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> ( delayed->list[delayed->position[pxCurrentTCB->pvGenericListItem]]==
						pxCurrentTCB->pvGenericListItem 
					) 

	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toDelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) 
			  ) ==> 
			  (
					\forall unsigned i; 
						( ( i>delayed->position[pxCurrentTCB->pvGenericListItem] ) && 
						  ( i<delayed->length ) 
						) ==> ( delayed->list[i]==\old(delayed->list[i-1] ) )
			  )
	 )	
	 _(ensures	
		(	needToDelay(xTickCount, \old(*pxPreviousWakeTime), xTimeIncrement, maxNumVal ) && 
			(  xTimeIncrement <= ( maxNumVal - \old(*pxPreviousWakeTime) ) )
		) ==>	( pxCurrentTCB->pvGenericListItem->xItemValue == 
					( xTimeIncrement+\old(*pxPreviousWakeTime) ) 
				) 
	 )
//////////////////////////////////
//////////////////////////////////
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> 
			  (
					oDelayed->length == ( \old(oDelayed->length) + 1 )
			  )
	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> ( oDelayed->position[pxCurrentTCB->pvGenericListItem] <
						oDelayed->length
					) 

	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> 
			  (
					\forall unsigned i; 
						( i<oDelayed->position[pxCurrentTCB->pvGenericListItem] ) 
						  ==> ( oDelayed->list[i]==\old(oDelayed->list[i]) )
			  )
	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal )
			  ) ==> ( oDelayed->list[oDelayed->position[pxCurrentTCB->pvGenericListItem]]==
						pxCurrentTCB->pvGenericListItem 
					) 

	 )	
	_(ensures ( 	needToDelay(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) && 
					toODelayed(xTickCount, \old(*pxPreviousWakeTime), 
					xTimeIncrement, maxNumVal ) 
			  ) ==> 
			  (
					\forall unsigned i; 
						( ( i>oDelayed->position[pxCurrentTCB->pvGenericListItem] ) && 
						  ( i<oDelayed->length ) 
						) ==> ( oDelayed->list[i]==\old(oDelayed->list[i-1] ) )
			  )
	 )	
	 _(ensures	
		(	needToDelay(xTickCount, \old(*pxPreviousWakeTime), xTimeIncrement, maxNumVal ) && 
			(  xTimeIncrement > ( maxNumVal - \old(*pxPreviousWakeTime) ) )
		) ==>	( pxCurrentTCB->pvGenericListItem->xItemValue == 
					( xTimeIncrement - ( maxNumVal - \old(*pxPreviousWakeTime) ) - 1 ) 
				) 
	 )
//////////////////////////////////
	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i]->uxPriority == \old((&sstm)->taskSet[i]->uxPriority) )
			)
	 )
	_(ensures ( xTickCount == \old(xTickCount) ) )
	/*	Property on 'topReadyPriority' is assured by the invariant 
		'rdyLists' which is assured by '\wrapped(&sstm)'.
	*/
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	_(ensures pxCurrentTCB->pvGenericListItem->pvOwner == 
					\old(pxCurrentTCB->pvGenericListItem->pvOwner) )
	_(ensures \wrapped((&sstm)) )
	_(ensures pxCurrentTCB \in (&sstm)->\owns )
	_(ensures pxCurrentTCB->pvEventListItem \in (&sstm)->\owns  )
	//_(ensures \false ) 
	;





/*


///////////////////////////////////////////////////////////
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						(	\forall unsigned j; 
							( j < rdyLists->ready[i]->length ) ==>
							( rdyLists->ready[i]->list[j] == 
								\old(rdyLists->ready[i]->list[j]) )				
						)
				)
	 )


	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )
	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )
	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )
	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i]->uxPriority == \old((&sstm)->taskSet[i]->uxPriority) )
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )

	_(ensures ( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) )


///////////////////////////////////////////////////////////
*/										
										

TCB* vTaskSwitchContext(  )
	_(requires \wrapped((&sstm)) )
	_(requires pxCurrentTCB \in (&sstm)->\owns )
	_(requires pxCurrentTCB != 
		rdyLists->ready[rdyLists->topReadyPriority]->list[0]->pvOwner )
	_(requires rdyLists->topReadyPriority < maxPrio ) 
	_(requires 
		( rdyLists->ready[rdyLists->topReadyPriority]->type==FIFO ) ==> 
			(\forall unsigned i; 
				( i<rdyLists->ready[rdyLists->topReadyPriority]->length ) ==> 
					(	rdyLists->ready[rdyLists->topReadyPriority]->
										list[i]->pvOwner->uxPriority	==	
						rdyLists->ready[rdyLists->topReadyPriority]->priority 
					) 
		) 		
	 )

	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 	
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) //Need to change this

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i; ( i < maxPrio )  ==> 
			(	\forall unsigned j; 
				( 	( pxCurrentTCB->uxPriority == rdyLists->topReadyPriority ) && 
					( rdyLists->ready[rdyLists->topReadyPriority]->length == 0  )  
				) ==> (	( j < rdyLists->ready[i]->length ) ==>
							(	rdyLists->ready[i]->list[j] == 
								\old(rdyLists->ready[i]->list[j]) 
						) 
					)
			)
	 )
	_(ensures
		!( 	( pxCurrentTCB->uxPriority == rdyLists->topReadyPriority ) && 
			( rdyLists->ready[rdyLists->topReadyPriority]->length == 0  )  
		 ) ==>  \forall unsigned i; 
				(	( i < rdyLists->ready[rdyLists->topReadyPriority]->length-1 ) 
					==>	(	rdyLists->ready[rdyLists->topReadyPriority]->list[i] == 
							\old(rdyLists->ready[rdyLists->topReadyPriority]->list[i+1]) 
						) 
				)
	 )
	_(ensures
		!( 	( pxCurrentTCB->uxPriority == rdyLists->topReadyPriority ) && 
			( rdyLists->ready[rdyLists->topReadyPriority]->length == 0  )  
		 ) ==> (	rdyLists->ready[rdyLists->topReadyPriority]->list[ 
								rdyLists->ready[rdyLists->topReadyPriority
								]->length-1 ] == 
					\old(rdyLists->ready[rdyLists->topReadyPriority]->list[0]) 
			   ) 
	 )
	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )
	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )
	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )
	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )
	_(ensures ( xTickCount == \old(xTickCount) ) )
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	_(ensures ( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) )
	_(ensures \result == 
			rdyLists->ready[rdyLists->topReadyPriority]->list[0]->pvOwner ) 
//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
			
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		
		( L->length  == \old(L->length) )
	 )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;





void prvAddTaskToReadyQueue( TCB *pxTCB )
	_(requires \wrapped((&sstm)) )
	_(requires ( pxTCB \in (&sstm)->\owns ) )
	_(requires pxTCB->pvGenericListItem \in pxTCB->\owns )
	_(requires	( pxTCB->pvEventListItem \in (&sstm)->\owns ) )
	_(requires !containedIn(blocked,pxTCB->pvEventListItem) )
	_(requires pxTCB->pvGenericListItem->ownersPriority==
				rdyLists->ready[pxTCB->uxPriority]->priority  )
	_(requires pxTCB->uxPriority<maxPrio )
	_(requires rdyLists->ready[pxTCB->uxPriority]->length < MAXSIZE )
	_(requires 
		\forall unsigned i;	
		( i<rdyLists->ready[pxTCB->uxPriority]->length 
		) ==>	( rdyLists->ready[pxTCB->uxPriority]->list[i]->pvOwner 
						!= pxTCB->pvGenericListItem->pvOwner )	
	 )
	 _(requires 
		\forall unsigned i;	
			( i<rdyLists->ready[pxTCB->uxPriority]->length ) ==>
			( rdyLists->ready[pxTCB->uxPriority]->list[i]->
						pvOwner->uxPriority == 
							pxTCB->pvGenericListItem->pvOwner->uxPriority 
			)	
	 )
	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )

	_(ensures \forall unsigned i; \forall unsigned j; 
		( i < maxPrio )  ==>
		(	
				(	( j < rdyLists->ready[i]->length ) &&
					( i != pxTCB->uxPriority )
				) ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )
	_(ensures 
		(	\forall unsigned i; 
				( i < \old(rdyLists->ready[pxTCB->uxPriority]->length) ) ==>
					(		rdyLists->ready[pxTCB->uxPriority]->list[i] == 
							\old(rdyLists->ready[pxTCB->uxPriority]->list[i]) 
					) 
		)
	 )
	_(ensures	rdyLists->ready[pxTCB->uxPriority]->length ==
				( \old(rdyLists->ready[pxTCB->uxPriority]->length) + 1 )
	 )
	_(ensures	rdyLists->ready[ pxTCB->uxPriority ]->list
					[\old(rdyLists->ready[pxTCB->uxPriority]->length) ] ==
				pxTCB->pvGenericListItem
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )
	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )
	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )
	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )
	_(ensures ( xTickCount == \old(xTickCount) ) )
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	_(ensures ( pxTCB->uxPriority > \old(rdyLists->topReadyPriority) ) ==>
		( rdyLists->topReadyPriority == pxTCB->uxPriority ) 
	 ) 
	_(ensures ( pxTCB->uxPriority <= \old(rdyLists->topReadyPriority) ) ==>
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )
	_(ensures \wrapped((&sstm)) )
	_(ensures ( pxTCB \in (&sstm)->\owns ) ) 
	_(ensures	( pxTCB->pvEventListItem \in (&sstm)->\owns ) )
	_(ensures !containedIn(blocked,pxTCB->pvEventListItem) )
	_(ensures (		pxTCB->pvEventListItem->xItemValue == 
					\old(pxTCB->pvEventListItem->xItemValue) 
			  ) 
	 )
	_(ensures containedIn(rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem) )
	_(ensures \forall xListItem *xli;
		( xli->xItemValue == \old(xli->xItemValue) )
	 )
	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )
	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )
	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )
//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		( L != rdyLists->ready[pxTCB->uxPriority] ) ==> 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( rdyLists->ready[pxTCB->uxPriority] != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
	_(ensures \forall xListItem *xli; 
		(	( xli != pxTCB->pvGenericListItem  ) &&
			( xli \in rdyLists->ready[pxTCB->uxPriority]->\owns )
		) ==> (		rdyLists->ready[pxTCB->uxPriority]->position[ xli ] == 
					\old(rdyLists->ready[pxTCB->uxPriority]->position[ xli ]) 
			  )
	 )
	_(ensures	rdyLists->ready[pxTCB->uxPriority]->position
										[ pxTCB->pvGenericListItem ] == 
				rdyLists->ready[pxTCB->uxPriority]->length - 1 
	 )
/*
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( L != rdyLists->ready[pxTCB->uxPriority] ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
*/

//////////////////////////////////////////////////////
	//_(ensures \false )
	;




unsigned taskPrioritySet( TCB *pxTCB, unsigned newPrio )
	_(requires \wrapped((&sstm)) )
	_(requires (&sstm)->size>0 )
	_(requires ( pxTCB \in (&sstm)->\owns ) )
	_(requires	(	(	pxTCB->pvGenericListItem \in 
						rdyLists->ready[pxTCB->uxPriority]->\owns ) ||
					( pxTCB->pvGenericListItem \in (&sstm)->\owns ) 
				)
	 )
	_(requires	( pxTCB->pvEventListItem \in blocked->\owns ) || 
				( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	_(requires	( pxTCB->pvEventListItem \in blocked->\owns ) ==> 
				!( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	_(requires	( pxTCB->pvEventListItem \in (&sstm)->\owns ) ==> 
				!( pxTCB->pvEventListItem \in blocked->\owns ) 
	 )
	_(requires pxTCB->pvGenericListItem->ownersPriority <= MAXSIZE )
	_(requires pxTCB->pvGenericListItem->pvOwner == pxTCB )
	_(requires pxTCB->pvEventListItem->pvOwner == pxTCB )
	_(requires newPrio != pxTCB->uxPriority )
	_(requires pxTCB->uxPriority < maxPrio )
	_(requires newPrio<maxPrio )
	_(requires 
		\forall unsigned i;	
			( i<rdyLists->ready[newPrio]->length )	==>
			(	rdyLists->ready[newPrio]->list[i]->pvOwner->uxPriority == 
				newPrio 
			)	
	 )
	_(requires 
		\forall unsigned i;	
			( i<rdyLists->ready[newPrio]->length )	==>
			(	rdyLists->ready[newPrio]->list[i]->pvOwner != 
				pxTCB->pvGenericListItem->pvOwner 
			)	
	 )
	_(requires rdyLists->ready[newPrio]->priority == newPrio )
	_(requires rdyLists->ready[newPrio]->length < MAXSIZE )
	_(requires	containedIn(rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem) ==>
			(	!containedIn(blocked,pxTCB->pvEventListItem) &&
				(	\forall unsigned i;
					(	( i < maxPrio ) &&
						( i != pxTCB->uxPriority ) 
					)==> !containedIn(rdyLists->ready[i],pxTCB->pvGenericListItem) 
				)
			)
	 )
	_(requires containedIn(rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem) ==> 
			(	\forall unsigned i; ( i<rdyLists->ready[newPrio]->length ) ==> 
				(	rdyLists->ready[newPrio]->list[i]->pvOwner != 
					pxTCB->pvGenericListItem->pvOwner
				) 
			)
	 )
	_(requires	containedIn(rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem) ==> 
				( rdyLists->ready[newPrio]->length < MAXSIZE ) 
	 )
	_(requires	containedIn(blocked,pxTCB->pvEventListItem) ==>
			(	\forall unsigned i;
				( i < maxPrio ) ==>
				!containedIn( rdyLists->ready[i],pxTCB->pvGenericListItem ) 
			)
	 )
	_(requires  containedIn(blocked,pxTCB->pvEventListItem) ==>
			( \forall unsigned i; ( i<blocked->length ) ==> 
			  ( ( blocked->list[i] != pxTCB->pvEventListItem ) ==>
				( blocked->list[i]->pvOwner != pxTCB->pvEventListItem->pvOwner )
			  )
			)
	 )
	_(requires	(	containedIn( rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem ) ||
					containedIn( blocked,pxTCB->pvEventListItem ) 
				)
	 )
	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	//_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 
	_(ensures	(	\forall unsigned i; 
					(	( i< maxPrio ) &&
						( i != \old(pxTCB->uxPriority) ) 
					)==> ( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures  !containedIn(\old(rdyLists->ready[\old(pxTCB->uxPriority)]),
					pxTCB->pvGenericListItem) ==> 
						(	rdyLists->ready[\old(pxTCB->uxPriority)] == 
							\old(rdyLists->ready[\old(pxTCB->uxPriority)]) 
						)

	 )
//////////////////////////////////////////////////////%
	_(ensures \forall unsigned i; ( i < maxPrio )  ==>
		(	\forall unsigned j; 
				(	( j < rdyLists->ready[i]->length ) &&
					( i != pxTCB->uxPriority ) &&
					!containedIn( \old(rdyLists->ready[\old(pxTCB->uxPriority)]),
												pxTCB->pvGenericListItem ) 
				) ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )
	_(ensures 
		(	\forall unsigned i; 
				( i < \old(rdyLists->ready[pxTCB->uxPriority]->length) ) ==>
					(		rdyLists->ready[pxTCB->uxPriority]->list[i] == 
							\old(rdyLists->ready[pxTCB->uxPriority]->list[i]) 
					) 
		)
	 )
	_(ensures	rdyLists->ready[pxTCB->uxPriority]->length ==
				( \old(rdyLists->ready[pxTCB->uxPriority]->length) + 1 )
	 )
	_(ensures	rdyLists->ready[ pxTCB->uxPriority ]->list
					[\old(rdyLists->ready[pxTCB->uxPriority]->length) ] ==
				pxTCB->pvGenericListItem
	 )

	_(ensures containedIn(\old(rdyLists->ready[\old(pxTCB->uxPriority)]),
						pxTCB->pvGenericListItem) ==> 
						(	rdyLists->ready[ \old(pxTCB->uxPriority) ]->length == 
							\old(rdyLists->ready[ \old(pxTCB->uxPriority) ]->length) - 1	
						) 
	 )
	_(ensures	containedIn(\old(rdyLists->ready[\old(pxTCB->uxPriority)]),
						pxTCB->pvGenericListItem) ==> 
			(	\forall unsigned i;
				( i < \old(rdyLists->ready[ \old(pxTCB->uxPriority) ]
										->position[ pxTCB->pvGenericListItem ]) 
				) ==>
					(	rdyLists->ready[ \old(pxTCB->uxPriority) ]->list[i] == 
						\old(rdyLists->ready[ \old(pxTCB->uxPriority) ]->list[i])
					)
			)
	 )
	_(ensures containedIn(\old(rdyLists->ready[\old(pxTCB->uxPriority)]),
						pxTCB->pvGenericListItem) ==> 
				(	\forall unsigned i;
					(	( i >= \old(rdyLists->ready[ \old(pxTCB->uxPriority) ]
										->position[ pxTCB->pvGenericListItem ]) ) && 
						( i <  rdyLists->ready[ \old(pxTCB->uxPriority) ]->length ) 
					)==>
						(	rdyLists->ready[ \old(pxTCB->uxPriority) ]->list[i] == 
							\old(rdyLists->ready[ \old(pxTCB->uxPriority) ]->list[i+1])
						)
				)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures containedIn(\old(blocked),pxTCB->pvEventListItem) ==> 
		(	containedIn(blocked,pxTCB->pvEventListItem) &&
			pxTCB->pvEventListItem->xItemValue == newPrio 
		)
	 ) 
	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )
	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )
	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )
	_(ensures \forall unsigned i;
		(	( i > 0 ) && (i <= (&sstm)->size ) &&
			( (&sstm)->taskSet[i] != pxTCB )
		
		) ==>	(	(	(&sstm)->taskSet[i]->uxPriority == 
						\old((&sstm)->taskSet[i]->uxPriority) 
					)
				)
	 )
	_(ensures pxTCB->uxPriority == newPrio )
	_(ensures ( xTickCount == \old(xTickCount) ) )
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	_(ensures ( pxTCB->uxPriority > \old(rdyLists->topReadyPriority) ) ==>
		( rdyLists->topReadyPriority == pxTCB->uxPriority ) 
	 ) 
	_(ensures ( pxTCB->uxPriority <= \old(rdyLists->topReadyPriority) ) ==>
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )
//////////////////////////////////////////////////////%

	_(ensures	(	(	pxTCB->pvGenericListItem \in 
							rdyLists->ready[pxTCB->uxPriority]->\owns  ) ||
					( pxTCB->pvGenericListItem \in (&sstm)->\owns ) 
				)
	 )
	_(ensures	( pxTCB->pvEventListItem \in blocked->\owns ) || 
				( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	_(ensures \wrapped((&sstm)) )
	_(ensures ( pxTCB \in (&sstm)->\owns ) )
	//_(ensures \false )
	;



unsigned vTaskSuspend( TCB *pxTCB )
	_(requires ( pxTCB \in (&sstm)->\owns ) )
	_(requires pxTCB->uxPriority < maxPrio )

	_(requires pxTCB->pvGenericListItem->ownersPriority <= MAXSIZE )
	_(requires pxTCB->pvGenericListItem->pvOwner == pxTCB )
	_(requires pxTCB->pvEventListItem->pvOwner == pxTCB )
	//Following pre condition is not there in the code and hence leads  to
	//some problems when the user tries to suspend a blocked or delayed task
	_(requires containedIn(rdyLists->ready[pxTCB->uxPriority],
										pxTCB->pvGenericListItem) )

	_(requires \wrapped((&sstm)) )
	_(requires	( pxTCB->pvEventListItem \in blocked->\owns ) || 
				( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	_(requires	( pxTCB->pvEventListItem \in blocked->\owns ) ==> 
				!( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	_(requires	( pxTCB->pvEventListItem \in (&sstm)->\owns ) ==> 
				!( pxTCB->pvEventListItem \in blocked->\owns ) 
	 )
	_(requires \forall unsigned i; ( i<suspended->length ) ==> 
							( suspended->list[i]->pvOwner!=pxTCB ) )
	_(requires suspended->length < MAXSIZE )
	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	//_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 
	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i; ( i < maxPrio )  ==>
		(	\forall unsigned j; 
				(	( j < rdyLists->ready[i]->length ) &&
					( i != pxTCB->uxPriority )
				) ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )
	_(ensures	rdyLists->ready[pxTCB->uxPriority]->length ==
				( \old(rdyLists->ready[pxTCB->uxPriority]->length) - 1 )
	 )
	_(ensures	
			(	\forall unsigned i;
				( i < \old(rdyLists->ready[ pxTCB->uxPriority ]
										->position[ pxTCB->pvGenericListItem ]) 
				) ==>
					(	rdyLists->ready[pxTCB->uxPriority ]->list[i] == 
						\old(rdyLists->ready[pxTCB->uxPriority]->list[i])
					)
			)
	 )
	_(ensures 
				(	\forall unsigned i;
					(	( i >= \old(rdyLists->ready[ pxTCB->uxPriority ]
										->position[ pxTCB->pvGenericListItem ]) ) && 
						( i <  rdyLists->ready[pxTCB->uxPriority]->length ) 
					)==>
						(	rdyLists->ready[pxTCB->uxPriority]->list[i] == 
							\old(rdyLists->ready[pxTCB->uxPriority]->list[i+1])
						)
				)
	 )
	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )
	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )
	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )
	_(ensures presentIn(suspended, pxTCB->pvGenericListItem) ) 
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )
	_(ensures ( xTickCount == \old(xTickCount) ) )
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	_(ensures	(	rdyLists->topReadyPriority == 
					\old(rdyLists->topReadyPriority) 
				)
	 ) 
	_(ensures \wrapped((&sstm)) )
	_(ensures ( pxTCB \in (&sstm)->\owns ) ) 
//	_(ensures	( pxTCB->pvEventListItem \in pxTCB->\owns ) )
	_(ensures pxTCB->pvEventListItem->pvOwner == pxTCB )

	_(ensures (		pxTCB->pvEventListItem->xItemValue == 
					\old(pxTCB->pvEventListItem->xItemValue) 
			  ) 
	 )
	_(ensures \forall xListItem *xli;
		( xli->xItemValue == \old(xli->xItemValue) )
	 )
	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )
	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )
	_(ensures \wrapped((&sstm)) )
	//_(ensures \false ) 
	;




unsigned vTaskDelete( TCB *pxTCB )
	_(requires ( pxTCB \in (&sstm)->\owns ) )
	_(requires pxTCB->uxPriority < maxPrio )
	_(requires pxTCB->pvGenericListItem->ownersPriority <= MAXSIZE )
	_(requires pxTCB->pvGenericListItem->pvOwner == pxTCB )
	_(requires \thread_local(pxTCB->pvEventListItem) )
	_(requires ( pxTCB->pvEventListItem != pxTCB->pvGenericListItem ) )
	_(requires pxTCB->pvEventListItem->pvOwner == pxTCB )
	_(requires	( pxTCB->pvEventListItem \in blocked->\owns ) || 
				( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	 /*
	_(requires	( pxTCB->pvEventListItem \in blocked->\owns ) ==> 
				!( pxTCB->pvEventListItem \in (&sstm)->\owns ) 
	 )
	_(requires	( pxTCB->pvEventListItem \in (&sstm)->\owns ) ==> 
				!( pxTCB->pvEventListItem \in blocked->\owns ) 
	 )
	 */
	_(requires (	containedIn( rdyLists->ready[pxTCB->uxPriority],
										  pxTCB->pvGenericListItem ) ||
					containedIn(suspended,pxTCB->pvGenericListItem ) ||
					containedIn( delayed,pxTCB->pvGenericListItem  )	
			   )
	 )
	_(requires (	containedIn(rdyLists->ready[pxTCB->uxPriority],
											pxTCB->pvGenericListItem ) ==>
					(	!containedIn(suspended,pxTCB->pvGenericListItem) &&
						!containedIn(delayed,pxTCB->pvGenericListItem)	
					)
			   )
	 )

	_(requires (	containedIn(suspended,pxTCB->pvGenericListItem) ==>
					(	!containedIn(rdyLists->ready[pxTCB->uxPriority],
												pxTCB->pvGenericListItem ) &&
						!containedIn(delayed,pxTCB->pvGenericListItem)	
					)
			   )
	 )
	_(requires (	containedIn(delayed,pxTCB->pvGenericListItem) ==>
					(	!containedIn(rdyLists->ready[pxTCB->uxPriority],
												pxTCB->pvGenericListItem ) &&
						!containedIn(suspended,pxTCB->pvGenericListItem)	
					)
			   )
	 )

	_(requires \wrapped((&sstm)) )

	_(requires \forall unsigned i; ( i<deleted->length ) ==> 
								( deleted->list[i]->pvOwner!=pxTCB ) )
	_(requires deleted->length<MAXSIZE )

	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
//	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i; ( i < maxPrio )  ==>
		(	\forall unsigned j; 
				(	( j < rdyLists->ready[i]->length ) &&
					( i != pxTCB->uxPriority )
				) ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )
	_(ensures \forall unsigned i;
		(	( i > 0 ) && (i <= (&sstm)->size ) &&
			( (&sstm)->taskSet[i] != pxTCB )
		
		) ==>	(	(	(&sstm)->taskSet[i]->uxPriority == 
						\old((&sstm)->taskSet[i]->uxPriority) 
					)
				)
	 )
	_(ensures ( xTickCount == \old(xTickCount) ) )
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )
	_(ensures presentIn(deleted, pxTCB->pvGenericListItem) )
	_(ensures !presentIn(rdyLists->ready[pxTCB->uxPriority],pxTCB->pvGenericListItem) )
	_(ensures !presentIn(suspended, pxTCB->pvGenericListItem) )
	_(ensures !presentIn(delayed, pxTCB->pvGenericListItem) )
	_(ensures \wrapped((&sstm)) )
	//_(ensures \false ) 
	;

TCB* vTaskSwitchContextTerminationProof(  )
	_(requires \wrapped((&sstm)) )
	_(requires \exists unsigned i;
		(	( i <= rdyLists->topReadyPriority ) &&
			( rdyLists->ready[i]->length!=0 )
		)
	 )
	_(requires rdyLists->topReadyPriority < maxPrio ) 
	_(writes (&sstm) )
//////////////////////////////////////////////////////
	//_(ensures \false )
	;

TCB* vTaskSwitchContextT( unsigned arr[MAXSIZE], unsigned topReadyPriority )
	_(requires \thread_local_array(arr,MAXSIZE) )
	_(requires maxPrio <= MAXSIZE )
	_(requires \exists unsigned i;
		(( i <= topReadyPriority ) && ( arr[i] != 0 ) )
	 )
	_(requires topReadyPriority < maxPrio ) 
 	//_(ensures \false )
	;


	/*
	*/

unsigned taskPriorityGet( TCB *pxTCB )
	_(requires \wrapped((&sstm)) )
	_(requires ( pxTCB \in (&sstm)->\owns ) )


//	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i;\forall unsigned j;  ( i < maxPrio )  ==>
		(	
				( j < rdyLists->ready[i]->length ) 
				  ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )

	_(ensures 
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )

	_(ensures ( pxTCB \in (&sstm)->\owns ) ) 

	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )

	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )

	_( ensures ( \result == pxTCB->uxPriority ) )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;


unsigned isTaskSuspended( TCB *pxTCB )
	_(requires \wrapped((&sstm)) )
	_(requires ( pxTCB \in (&sstm)->\owns ) )

	_(writes (&sstm) )

	_( ensures \wrapped( &sstm ) )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i;\forall unsigned j;  ( i < maxPrio )  ==>
		(	
				( j < rdyLists->ready[i]->length ) 
				  ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )

	_(ensures 
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )

	_(ensures ( pxTCB \in (&sstm)->\owns ) ) 

	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )

	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )

	_(ensures ( \result <==> ( pxTCB->pvGenericListItem \in suspended->\owns ) ) )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;


void taskResume( TCB *pxTCB )
	_( requires \wrapped((&sstm)) )
	_( requires ( pxTCB \in (&sstm)->\owns ) )
	_( requires pxCurrentTCB \in (&sstm)->\owns )

	_( requires ( pxTCB != NULL ) && ( pxTCB != pxCurrentTCB ) )
	_( requires containedWithin( suspended, pxTCB->pvGenericListItem ) )
	_( requires ( pxTCB->pvGenericListItem \in suspended->\owns  ) )
	_( requires	( pxTCB->pvEventListItem \in (&sstm)->\owns ) )
	_( requires !containedIn(blocked,pxTCB->pvEventListItem) )
	_( requires pxTCB->pvGenericListItem->ownersPriority==
				rdyLists->ready[pxTCB->uxPriority]->priority  )
	_( requires pxTCB->uxPriority<maxPrio )
	_( requires rdyLists->ready[pxTCB->uxPriority]->length < MAXSIZE )
	_( requires 
		\forall unsigned i;	
		( i<rdyLists->ready[pxTCB->uxPriority]->length 
		) ==>	( rdyLists->ready[pxTCB->uxPriority]->list[i]->pvOwner 
						!= pxTCB->pvGenericListItem->pvOwner )	
	 )
	 _( requires 
		\forall unsigned i;	
			( i<rdyLists->ready[pxTCB->uxPriority]->length ) ==>
			( rdyLists->ready[pxTCB->uxPriority]->list[i]->
						pvOwner->uxPriority == 
							pxTCB->pvGenericListItem->pvOwner->uxPriority 
			)	
	 )	
	
	_( writes (&sstm) )

	_( ensures \wrapped( &sstm ) )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )

///////////////////////////////////////////////////////

	_(ensures \forall unsigned i; \forall unsigned j; 
		(	( i < maxPrio ) && 
			( i != pxTCB->uxPriority ) &&
			( j < rdyLists->ready[i]->length )
		)
			==>
		(	rdyLists->ready[i]->list[j] == 
			\old(rdyLists->ready[i]->list[j]) 
		) 
	 )

	_(ensures 
		(	\forall unsigned i; 
				( i < \old(rdyLists->ready[pxTCB->uxPriority]->length) ) ==>
					(		rdyLists->ready[pxTCB->uxPriority]->list[i] == 
							\old(rdyLists->ready[pxTCB->uxPriority]->list[i]) 
					) 
		)
	 )
	_(ensures	rdyLists->ready[pxTCB->uxPriority]->length ==
				( \old(rdyLists->ready[pxTCB->uxPriority]->length) + 1 )
	 )
	_(ensures	rdyLists->ready[ pxTCB->uxPriority ]->list
					[\old(rdyLists->ready[pxTCB->uxPriority]->length) ] ==
				pxTCB->pvGenericListItem
	 )
///////////////////////////////////////////////////////

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )

	_( ensures \forall unsigned i;
			( i < \old( suspended->position[ \old( pxTCB->pvGenericListItem ) ] ) ) 
				==> 
			( suspended->list[ i ] == \old( suspended->list[ i ] ) )
	 )

	_( ensures \forall unsigned i;
			(	( i >= \old( suspended->position[ \old( pxTCB->pvGenericListItem ) ] ) ) &&
				( i < suspended->length )
			)
				==> 
			( suspended->list[ i ] == \old( suspended->list[ i + 1 ] ) )
	 )

//	_( ensures !containedWithin( suspended, pxTCB->pvGenericListItem ) )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )

	_(ensures 
				( pxTCB->uxPriority > \old( rdyLists->topReadyPriority ) ) 
			    ==>
		( rdyLists->topReadyPriority == pxTCB->uxPriority ) 
	 )

	_(ensures 
				( pxTCB->uxPriority <= \old( rdyLists->topReadyPriority ) ) 
			    ==>
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )

	_(ensures ( pxTCB \in (&sstm)->\owns ) ) 

	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli != pxTCB->pvGenericListItem ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;


void endScheduler(  )
	_(requires \wrapped((&sstm)) )

	_(writes (&sstm) )
	_(writes (&schedulerRunning) )

	_( ensures \wrapped( &sstm ) )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i;\forall unsigned j;  ( i < maxPrio )  ==>
		(	
				( j < rdyLists->ready[i]->length ) 
				  ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == fls ) )

	_(ensures 
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )


	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )

	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;


unsigned getTickCount(  )
	_(requires \wrapped((&sstm)) )

	_(writes (&sstm) )

	_( ensures \wrapped( &sstm ) )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i;\forall unsigned j;  ( i < maxPrio )  ==>
		(	
				( j < rdyLists->ready[i]->length ) 
				  ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old( schedulerRunning ) ) )

	_(ensures 
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )


	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )

	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )

	_( ensures ( \result == xTickCount ) )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;



void taskGenericCreate( TCB *pxTCB, unsigned priority )
	_( requires ( \wrapped( ( &sstm ) ) ) )
	_( requires ( \wrapped( ( pxTCB ) ) ) )
	_( requires ( pxTCB->uxPriority <= maxPrio ) )
	_( requires (&sstm)->size < MAXSIZE )

	_( requires \forall unsigned i;
		(	( i > 0 ) &&
			( i <= ( &sstm )->size )
		) ==> ( ( &sstm )->taskSet[ i ] != pxTCB )
	 )
	_( writes ( &sstm ) )
	_( writes ( pxTCB ) )


	_( ensures \wrapped( &sstm ) )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == ( \old( ( &sstm )->size ) + 1 ) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i < (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_( ensures ( ( &sstm )->taskSet[ (&sstm)->size ] == pxTCB ) )

	_(ensures	(	( ( &sstm )->size  == 1 ) ||
					(	 ( schedulerRunning == fls ) &&
						 ( pxCurrentTCB->uxPriority < pxTCB->uxPriority )
					) ==> ( pxCurrentTCB == pxTCB ) 
				) 
	 ) 

	_(ensures	(	( ( &sstm )->size  > 1 ) ||
					!(	 ( schedulerRunning == fls ) &&
						 ( pxCurrentTCB->uxPriority < pxTCB->uxPriority )
					 ) ==> ( pxCurrentTCB == \old(pxCurrentTCB) ) 
				) 
	 ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )

	_(ensures \forall unsigned i; \forall unsigned j; 
		(	( i < maxPrio ) && 
			( i != pxTCB->uxPriority ) &&
			( j < rdyLists->ready[i]->length )
		)
			==>
		(	rdyLists->ready[i]->list[j] == 
			\old(rdyLists->ready[i]->list[j]) 
		) 
	 )

	_(ensures 
		(	\forall unsigned i; 
				( i < \old(rdyLists->ready[pxTCB->uxPriority]->length) ) ==>
					(		rdyLists->ready[pxTCB->uxPriority]->list[i] == 
							\old(rdyLists->ready[pxTCB->uxPriority]->list[i]) 
					) 
		)
	 )
	_(ensures	rdyLists->ready[pxTCB->uxPriority]->length ==
				( \old(rdyLists->ready[pxTCB->uxPriority]->length) + 1 )
	 )
	_(ensures	rdyLists->ready[ pxTCB->uxPriority ]->list
					[\old(rdyLists->ready[pxTCB->uxPriority]->length) ] ==
				pxTCB->pvGenericListItem
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i < (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )
	_( ensures ( pxTCB->uxPriority == \old( pxTCB->uxPriority ) ) )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old( schedulerRunning ) ) )

	_(ensures 
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )


	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )

	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )

//	_( ensures ( \result == xTickCount ) )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;


void taskPlaceOnEventList( TCB *pxTCB, unsigned xTicksToWait )
	_(requires ( pxTCB \in (&sstm)->\owns ) )
	_(requires xTicksToWait <= maxNumVal )
	_(requires pxTCB->uxPriority < maxPrio )
	_(requires pxTCB->pvGenericListItem->ownersPriority <= MAXSIZE )
	_(requires pxTCB->pvGenericListItem->pvOwner == pxTCB )
	_(requires \thread_local(pxTCB->pvEventListItem) )
	_(requires ( pxTCB->pvEventListItem != pxTCB->pvGenericListItem ) )
	_(requires pxTCB->pvEventListItem->pvOwner == pxTCB )

	_(requires (	containedIn( rdyLists->ready[pxTCB->uxPriority],
										  pxTCB->pvGenericListItem ) 
			   )
	 )
	_(requires (	
					(	!containedIn(suspended,pxTCB->pvGenericListItem) &&
						!containedIn(delayed,pxTCB->pvGenericListItem)	&&
						!containedIn(blocked,pxTCB->pvGenericListItem)
					)
			   )
	 )

	_(requires \wrapped((&sstm)) )

	_(requires \forall unsigned i; ( i<blocked->length ) ==> 
								( blocked->list[i]->pvOwner!=pxTCB ) )

	_(requires \forall unsigned i; ( i<suspended->length ) ==> 
								( suspended->list[i]->pvOwner!=pxTCB ) )

	_(requires blocked->length<MAXSIZE )
	_(requires suspended->length<MAXSIZE )

	_(writes (&sstm) )
	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 
	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
//	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i; ( i < maxPrio )  ==>
		(	\forall unsigned j; 
				(	( j < rdyLists->ready[i]->length ) &&
					( i != pxTCB->uxPriority )
				) ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )
	_(ensures !presentIn(rdyLists->ready[pxTCB->uxPriority], pxTCB->pvGenericListItem) )

	_(ensures ( xTickCount == \old(xTickCount) ) )
	_(ensures ( schedulerRunning == \old(schedulerRunning) ) )

	_(ensures ( xTicksToWait == maxNumVal ) ==> presentIn(suspended, pxTCB->pvGenericListItem) )
	_(ensures ( xTicksToWait <= ( maxNumVal - xTickCount ) ) ==> 
			presentIn(delayed, pxTCB->pvGenericListItem) 
	 )

	_(ensures ( xTicksToWait > ( maxNumVal - xTickCount ) ) ==> 
			presentIn(oDelayed, pxTCB->pvGenericListItem) 
	 )


	_(ensures \wrapped((&sstm)) )
	//_(ensures \false ) 
	;

unsigned getNumberOfTasks(  )
	_(requires \wrapped((&sstm)) )

	_(writes (&sstm) )

	_( ensures \wrapped( &sstm ) )

	_(ensures ( maxNumVal == \old(maxNumVal) ) )
	_(ensures ( maxPrio == \old(maxPrio) ) ) 
	_(ensures ( preemption == \old(preemption) ) ) 

	//Following 2 conditions ensures that the task set is not changed
	_(ensures (&sstm)->size == \old((&sstm)->size) )
	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			( ( (&sstm)->taskSet[i] == \old((&sstm)->taskSet[i]) )
			)
	 )
	_(ensures ( pxCurrentTCB == \old(pxCurrentTCB) ) ) 

	_(ensures	(	\forall unsigned i; ( i< maxPrio )  ==> 
						( rdyLists->ready[i] == \old(rdyLists->ready[i]) )
				)
	 )
	_(ensures \forall unsigned i;\forall unsigned j;  ( i < maxPrio )  ==>
		(	
				( j < rdyLists->ready[i]->length ) 
				  ==> (		rdyLists->ready[i]->list[j] == 
							\old(rdyLists->ready[i]->list[j]) 
					  ) 
		)
	 )

	_(ensures ( blocked == \old(blocked) ) )
	_(ensures \forall unsigned i;
			( i < blocked->length ) ==>
					( blocked->list[i] == \old(blocked->list[i]) ) 
	 )

	_(ensures ( delayed == \old(delayed) ) )
	_(ensures \forall unsigned i;
			( i < delayed->length ) ==>
					( delayed->list[i] == \old(delayed->list[i]) ) 
	 )

	_(ensures ( oDelayed == \old(oDelayed) ) )
	_(ensures \forall unsigned i;
			( i < oDelayed->length ) ==>
					( oDelayed->list[i] == \old(oDelayed->list[i]) ) 
	 )

	_(ensures ( suspended == \old(suspended) ) )
	_(ensures \forall unsigned i;
			( i < suspended->length ) ==>
					( suspended->list[i] == \old(suspended->list[i]) ) 
	 )

	_(ensures \forall unsigned i;
		( ( i > 0 ) && (i <= (&sstm)->size ) ) ==> 
			(	(	(&sstm)->taskSet[i]->uxPriority == 
					\old((&sstm)->taskSet[i]->uxPriority) 
				)
			)
	 )

	_(ensures ( xTickCount == \old(xTickCount) ) )

	_(ensures ( schedulerRunning == \old( schedulerRunning ) ) )

	_(ensures 
		( rdyLists->topReadyPriority == \old(rdyLists->topReadyPriority) ) 
	 )

	_(ensures \wrapped((&sstm)) )


	_(ensures \forall TCB *tcb;
		( tcb->pvEventListItem == \old(tcb->pvEventListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->pvGenericListItem == \old(tcb->pvGenericListItem) )
	 )

	_(ensures \forall TCB *tcb;
		( tcb->uxPriority == \old(tcb->uxPriority) )
	 )

//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )

	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )

	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )

	_(ensures \forall xMap  *L; L->type==\old(L->type) )

	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )

	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )

	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )

	_( ensures ( \result == uxCurrentNumberOfTasks ) )

//////////////////////////////////////////////////////
	//_(ensures \false )
	;