#include <vcc.h>
#include <limits.h>

#define NULL 0

//	A task is represented by a unique unsigned interger
typedef unsigned taskID;

/*	Following structure defines the type for the 
	object to be returned from the function 'vTaskDelayUntil'.
*/
typedef struct taskAndPWT{
	_( ghost taskID running )
	_( ghost \natural pWT )
	/*	Following is a dummy field to 
		satisfy the requirement that 
		"every structure must contain 
		at least one physical field".

	*/
	unsigned dummy;
}runningAndPWTZ1;

/*	Following structure defines the type for the 
	object to be returned from the function 'vTaskDelayUntil'.
*/
typedef struct taskAndpWT{
	_( ghost taskID running )
	_( ghost \natural pWT )
	unsigned dummy;
}runningAndPWTZ2;

/*	Following structure models the set of 
	tasks in the system
*/
_(dynamic_owns)
typedef struct task{
	/*	Following map models the set of tasks in
		the system, given the ID of a task, the 
		value under this map tells whether 
		the given task is present in the system 
		(value 'true') or not (value 'false').
	*/
	_( ghost \bool member[ taskID ] )
	
	/*	Following is a dummy field to 
		satisfy the requirement that 
		"every structure must contain 
		at least one physical field".

	*/
	unsigned dummy;

	/*	Let 0 be the task ID for 'idle' task and 
		UINT_MAX be the task ID for 'null' task
	*/
	/*INV-1:	'idle' and 'null' tasks are present 
				in the system at any valid state.
	*/
	_( invariant (	( member[ 0 ] == \true ) &&
					( member[ UINT_MAX ] == \true )
				)
	 )
} Task;




/*	Following structure models the sequence
	'iseq TASK' in the Z models.
*/
_(dynamic_owns)
typedef struct iseq{
	/*	Following map models a sequence of task IDs,
		the value for a given natural number 'i' gives 
		the ID of the ith task in the sequence.
	*/
	_( ghost taskID list[ \natural ] )

	/*	Following map gives the index ( between 
		'0' and 'length - 1' )of the given taskID in 
		the above sequence. This field allows 
		easy specification of 
		some properties like membership.
	*/
	_( ghost \natural index[ taskID ] )

	/*	Following field gives the number of 
		valid tasks in the sequence
	*/
	_( ghost \natural length )


	/*	Following is a dummy field to 
		satisfy the requirement that 
		"every structure must contain 
		at least one physical field".

	*/
	unsigned dummy;

	/*INV-1:	The Task IDs in the sequence are
				distinct.
	*/
	_( invariant \forall \natural i,j;
				(	(	( i < length ) && 
						( j < length ) && 
						( i != j )  
					)
						 ==> ( list[ i ] != list[ j ] ) 
				)
	 )

	/*INV-2:	The sequence 'list' contains valid taskIDs
				( '0' to 'UINT_MAX - 1') from '0' to 'length - 1'.
				'UINT_MAX' is the ID for the task 'null'.
	*/
	_( invariant \forall \natural i;
				( i < length )  ==>
					( list[ i ] < UINT_MAX ) 
	 )

	/*INV-3:	The sequence 'list' contains 'null' task
				beyond 'length - 1'.
				This allows easy and consistent 
				update on this map.
	*/
	_( invariant \forall \natural i;
				( i >= length )  ==>
					( list[ i ] == UINT_MAX ) 
	 )

	/*INV-4:	The maps 'index' and 'list' are in sync 
				up to the position 'lngth - 1'.
	*/
	_( invariant \forall \natural i;
				( i < length )  ==>
					( index[ list[ i ] ] == i ) 
	 )


	/*INV-5:	If the index value  for a task
				is valid then the task is present 
				in the list at the concerned position.
	*/
	_( invariant \forall taskID t;
				( index[ t ] < length )  ==>
					( list[ index[ t ] ] == t ) 
	 )
} iSeq;


/*	Following structure models different task lists
	in the system
*/
_(dynamic_owns)
typedef struct lists{
	/*	Following field models the set of 
		ready tasks in the system.
		There is one sequence of tasks 
		for each priority ( from 1 to maximum 
		priority value ).
		The order of the tasks in each 
		sequence is decided by the 
		time of insertion into the sequence.
	*/
	_( ghost iSeq ready[ UINT_MAX ] )

	/*	Following map models whether 
		a given task ( ID ) is present 
		in ready lists, and is ensured by an 
		invariant in the structure 'system'.
	*/
	_( ghost \bool isInReady[ taskID ] )

	/*	Following field models the sequence
		of blocked tasks in the system.
		The order of the tasks in this 
		sequence is decided by the 
		priority of the tasks present.
		This order is ensured by 
		an invariant in the structure 
		'system'.
	*/
	_( ghost iSeq blocked )

	/*	Following map models the sequence of 
		delayed tasks in the system.
		The order of the tasks in this 
		sequence is decided by the 
		time to awake for each task and 
		which is modelled by the field/map
		'timeToAwake'.
	*/
	_( ghost taskID delayed[ \natural ] )

	/*	Following map gives the index ( between 
		'0' and 'delayedLength - 1' )of the given 
		taskID in the above sequence. This field allows 
		easy specification of 
		some properties like membership.
	*/
	_( ghost \natural indexDelayed[ taskID ] )

	/*	Following field models the length 
		of the sequence 'delayed' 
		(same as the length of the 
		sequence 'timeToAwake')
	*/
	_( ghost \natural delayedLength )

	/*	Following map models the sequence 
		of values representing the time
		to awake for the tasks present 
		in the list 'delayed'.
	*/
	_( ghost \natural timeToAwake[ \natural ] )

	/*	Following map models the sequence of 
		delayed tasks in the system Z2.
		The order of the tasks in this 
		sequence is decided by the 
		time to awake for each task and 
		which is modelled by the field/map
		'timeToAwakeZ2'.
	*/
	_( ghost taskID delayedZ2[ \natural ] )

	/*	Following field models the length 
		of the sequence 'delayedZ2' 
		(same as the length of the 
		sequence 'timeToAwakeZ2').
	*/
	_( ghost \natural delayedLengthZ2 )

	/*	Following map gives the index ( between 
		'0' and 'delayedLengthZ2 - 1' )of the given 
		taskID in the above sequence. This field allows 
		easy specification of 
		some properties like membership.
	*/
	_( ghost \natural indexDelayedZ2[ taskID ] )

	/*	Following map models the sequence 
		of values representing the time
		to awake for the tasks present 
		in the list 'delayedZ2'.
	*/
	_( ghost \natural timeToAwakeZ2[ \natural ] )

	/*	Following map models the sequence of 
		delayed tasks in the model Z2 for which the 
		value of time to awake is greater than 
		than the maximum possible value for 'tickCount'.
		The order of the tasks in this 
		sequence is decided by the 
		time to awake for each task and 
		which is modelled by the field/map
		'timeToAwakeOD'.
	*/
	_( ghost taskID oDelayed[ \natural ] )

	/*	Following field models the length 
		of the sequence 'oDelayed' 
		(same as the length of the 
		sequence 'timeToAwakeOD')
	*/
	_( ghost \natural oDelayedLength )

	/*	Following map gives the index ( between 
		'0' and 'oDelayedLength - 1' )of the given 
		taskID in the above list. This field allows 
		easy specification of 
		some properties like membership.
	*/
	_( ghost \natural indexODelayed[ taskID ] )

	/*	Following map models the sequence 
		of values representing the time
		to awake for the tasks present 
		in the list 'oDelayed'.
	*/
	_( ghost \natural timeToAwakeOD[ \natural ] )

	/*	Following map models the set of 
		suspended tasks in the system, 
		given the ID of a task, the 
		value under this map represents whether 
		the given task is present in the list 
		'suspended'(value 'true') or 
		not (value 'false').
	*/
	_( ghost \bool suspended[ taskID ] )
	
	/*	Following map models the sequence of 
		suspended tasks in the system.
		This is required for bounding the 
		cardinality of the set 'suspended'.
	*/
	_( ghost taskID suspendedTasks[ \natural ] )

	/*	Following field models the cardinality 
		of the set 'suspended', defined/constrained 
		in terms of the sequence and index corresponding 
		to the set if suspended tasks.
	*/
	_( ghost \natural suspendedLength )

	/*	Following map gives the index ( between 
		'0' and 'suspendedLength - 1' )of the given 
		taskID in the above sequence. .
		This is also required for bounding the 
		cardinality of the set 'suspended'.
	*/
	_( ghost \natural indexSuspended[ taskID ] )

	/*	Following is a dummy field to 
		satisfy the requirement that 
		"every structure must contain 
		at least one physical field".
	*/
	unsigned dummy;

	/*INV-1:	If a task is in 'delayed' list then it cannot be 
	  (3 in Z1)	present in 'suspended' list.
	*/
	_( invariant \forall taskID t;
			( indexDelayed[ t ] < delayedLength ) ==>	!( suspended[ t ] )
	 )

	/*INV-2:	If a task is in 'delayedZ2' or 'oDelayed' list then 
	  (3 in Z2) it cannot be present in 'suspended' list
	*/
	_( invariant \forall taskID t;
			(	( indexODelayed[ t ] < oDelayedLength ) ||
				( indexDelayedZ2[ t ] < delayedLengthZ2 )
			) ==>	!( suspended[ t ] )
	 )

	/*INV-3:	A task cannot be in both 'delayedZ2' and 'oDelayed'.
	  (4 in Z2)
	*/
	_( invariant \forall taskID t;
			!(	( indexDelayedZ2[ t ] < delayedLengthZ2 ) &&
				( indexODelayed[ t ] < oDelayedLength )
			 )
	 )

	/*INV-4:	List of delayed task is sorted in the nondecreasing 
	  (4 in Z1)	order of time to awake.
				(The value of time to awake for the 
				ith task in the list 'delayed' is the 
				value for 'i' under the map 'timeToAwake')
	*/
	_( invariant \forall \natural i,j;
					(	( i < delayedLength ) &&
						( j < delayedLength ) &&
						( i < j )				
					) ==> ( timeToAwake[ i ] <= timeToAwake[ j ] )
	 )

	/*INV-5:	List of delayed task is sorted in the nondecreasing 
	  (5 in Z2)	order of time to awake.
				The value of time to awake for the 
				ith task in the list 'delayedZ2' is the 
				value for 'i' under the map 'timeToAwakeZ2'.
	*/
	_( invariant \forall \natural i,j;
					(	( i < delayedLengthZ2 ) &&
						( j < delayedLengthZ2 ) &&
						( i < j )				
					) ==> ( timeToAwakeZ2[ i ] <= timeToAwakeZ2[ j ] )
	 )

	/*INV-6:	List of overflow delayed task is sorted in the 
	  (6 in Z2)	nondecreasing order of time to awake.
				The value of time to awake for the 
				ith task in the list 'oDelayed' is the 
				value for 'i' under the map 'timeToAwakeOD'.
	*/
	_( invariant \forall \natural i,j;
					(	( i < oDelayedLength ) &&
						( j < oDelayedLength ) &&
						( i < j )				
					) ==> ( timeToAwakeOD[ i ] <= timeToAwakeOD[ j ] )
	 )
	 
	/*INV-7:	The list 'delayed' contains 
	  (5 in Z1)	distinct Task IDs
	*/
	_( invariant \forall \natural i,j;
				(	(	( i < delayedLength ) && 
						( j < delayedLength ) && 
						( i != j )  
					) ==> ( delayed[ i ] != delayed[ j ] ) 
				)
	 )

	/*INV-8:	The list 'delayedZ2' contains 
	  (7 in Z2)	distinct Task IDs
	*/
	_( invariant \forall \natural i,j;
				(	(	( i < delayedLengthZ2 ) && 
						( j < delayedLengthZ2 ) && 
						( i != j )  
					) ==> ( delayedZ2[ i ] != delayedZ2[ j ] ) 
				)
	 )

	/*INV-9:	The list 'oDelayed' contains 
	  (8 in Z2)	distinct Task IDs
	*/
	_( invariant \forall \natural i,j;
				(	(	( i < oDelayedLength ) && 
						( j < oDelayedLength ) && 
						( i != j )  
					) ==> ( oDelayed[ i ] != oDelayed[ j ] ) 
				)
	 )
	 
	/*INV-10:	The list 'delayed' contains valid 
	  (7 in Z1)	task IDs at a valid index ( from 
				'0' to 'delayedLength - 1' )
	*/
	_( invariant \forall \natural i;
				( i < delayedLength )  ==>
					( delayed[ i ] < UINT_MAX ) 
	 )
	 
	/*INV-11:	The list 'delayedZ2' contains valid 
	  (10 in Z2)task IDs at a valid index ( from 
				'0' to 'delayedLengthZ2 - 1' )
	*/
	_( invariant \forall \natural i;
				( i < delayedLengthZ2 )  ==>
					( delayedZ2[ i ] < UINT_MAX ) 
	 )	 

	/*INV-12:	The list 'oDelayed' contains valid 
	  (11 in Z2)task IDs at a valid index ( from 
				'0' to 'oDelayedLength - 1' )
	*/
	_( invariant \forall \natural i;
				( i < oDelayedLength )  ==>
					( oDelayed[ i ] < UINT_MAX ) 
	 )
	 
	/*INV-13:	The list 'delayed' contains 'null' 
	  (8 in Z1)	task beyond index 'delayedLength - 1'
	*/
	_( invariant \forall \natural i;
				( i >= delayedLength )  ==>
					( delayed[ i ] == UINT_MAX ) 
	 )	 

	/*INV-14:	The list 'delayedZ2' contains 'null' 
	  (12 in Z2)task beyond index 'delayedLengthZ2 - 1'
	*/
	_( invariant \forall \natural i;
				( i >= delayedLengthZ2 )  ==>
					( delayedZ2[ i ] == UINT_MAX ) 
	 )	 
	 
	/*INV-15:	The list 'oDelayed' contains 'null' 
	  (13 in Z2)task beyond index 'oDelayedLength - 1'
	*/
	_( invariant \forall \natural i;
				( i >= oDelayedLength )  ==>
					( oDelayed[ i ] == UINT_MAX ) 
	 )

	/*INV-16:	'indexDelayed' and 'delayed' are in sync 
	  (9 in Z1)	up to the position 'delayedLength - 1'*/
	_( invariant \forall \natural i;
				( i < delayedLength )  ==>
					( indexDelayed[ delayed[ i ] ] == i ) 
	 )

	/*INV-17:	'indexDelayedZ2' and 'delayedZ2' are in sync 
	  (14 in Z2)up to the position 'delayedLengthZ2 - 1'*/
	_( invariant \forall \natural i;
				( i < delayedLengthZ2 )  ==>
					( indexDelayedZ2[ delayedZ2[ i ] ] == i ) 
	 )

	/*INV-18:	'indexODelayed' and 'oDelayed' are in sync 
	  (15 in Z2)up to the position 'oDelayedLength - 1'*/
	_( invariant \forall \natural i;
				( i < oDelayedLength )  ==>
					( indexODelayed[ oDelayed[ i ] ] == i ) 
	 )

	/*INV-19:	If the index value ( in 'delayed' )  for a task
	  (10 in Z1)is valid then the task is present 
				in 'delayed' at the concerned position.
	*/
	_( invariant \forall taskID t;
				( indexDelayed[ t ] < delayedLength )  ==>
					( delayed[ indexDelayed[ t ] ] == t ) 
	 )
	 
	/*INV-20:	If the index value ( in 'delayedZ2' )  for a task
	  (16 in Z2)is valid then the task is present 
				in 'delayedZ2' at the concerned position.
	*/
	_( invariant \forall taskID t;
				( indexDelayedZ2[ t ] < delayedLengthZ2 )  ==>
					( delayedZ2[ indexDelayedZ2[ t ] ] == t ) 
	 )

	/*INV-21:	If the index value ( in 'oDelayed' )  for a task
	  (17 in Z2)is valid then the task is present 
				in 'oDelayed' at the concerned position.
	*/
	_( invariant \forall taskID t;
				( indexODelayed[ t ] < oDelayedLength )  ==>
					( oDelayed[ indexODelayed[ t ] ] == t ) 
	 )

	/*INV-22:	The sequence 'suspendedTasks' contains valid 
				task IDs at a valid index ( from 
				'0' to 'suspendedLength - 1' )
	*/
	_( invariant \forall \natural i;
				( i < suspendedLength )  ==>
					( suspendedTasks[ i ] < UINT_MAX ) 
	 )

	/*INV-23:	The list 'suspendedTasks' contains 'null' 
				task beyond index 'suspendedLength - 1'
	*/
	_( invariant \forall \natural i;
				( i >= suspendedLength )  ==>
					( suspendedTasks[ i ] == UINT_MAX ) 
	 )

	/*INV-24:	'indexSuspended' and 'suspendedTasks' are in sync 
				up to the position 'suspendedLength - 1'*/
	_( invariant \forall \natural i;
				( i < suspendedLength )  ==>
					( indexSuspended[ suspendedTasks[ i ] ] == i ) 
	 )

	/*INV-25:	If the index value ( in 'delayed' )  for a task
				is valid then the task is present 
				in 'delayed' at the concerned position.
	*/
	_( invariant \forall taskID t;
				( indexSuspended[ t ] < suspendedLength )  ==>
					( suspendedTasks[ indexSuspended[ t ] ] == t ) 
	 )

	/*INV-26:	Relatioship between the set 'suspended' 
				and the sequence 'suspendedTasks'.
	*/
	_( invariant \forall taskID t;
				( suspended[ t ] )  <==>
					( indexSuspended[ t ] < suspendedLength ) 
	 )

	 
////////////////////////////////////Gluing relation between Z1 and Z2	 
	/*INV-Z1RZ2-1:	Length of the sequence 'delayed' is the 
				sum of the lengths of the sequences 'delayedZ2' 
				and 'oDelayed'.
	*/
	_( invariant 
		( delayedLength == delayedLengthZ2 + oDelayedLength )
	 )

	/*INV-Z1RZ2-2:	The sequence 'delayedZ2' is same as the 
				prefix of the sequence 'delayed' up to index  
				'delayedLengthZ2 - 1'.
	*/
	_( invariant \forall \natural i;
		( i < delayedLengthZ2 ) ==> 
			( delayed[ i ] == delayedZ2[ i ] )
	 )

	/*INV-Z1RZ2-3:	All tasks in the sequence 'oDelayed' 
				is contained in the suffix of the 
				sequence 'delayed'.
	*/
	_( invariant \forall \natural i;
		( i < oDelayedLength ) ==> 
			( delayed[ i + delayedLengthZ2 ] == oDelayed[ i ] )
	 )

	/*	The relationship between the time to awake values is 
		given in the strcuture 'System' as 
		it needs to  use the value if 'maxNumVal'.
	*/
} Lists;


/*	Following structure models the priorities of 
	tasks in the system
*/
_(dynamic_owns)
typedef struct prio{
	/*	Following map models the priorities of 
		tasks in the system. The value for 
		a given task ID is the priotiy.
	*/
	_( ghost unsigned value[ taskID ] )
 
	/*	Following is a dummy field to 
		satisfy the requirement that 
		"every structure must contain 
		at least one physical field".

	*/
	unsigned dummy;
} Prio;

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

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


/*	Following variable represents the global variable 
	'maxNumVal', can be initialised by the user.
	(for parameterized verification)
*/
_( ghost \natural maxNumVal )

/*	Following variable represents the global variable 
	'preemption', can be initialised by the user.
	(for parameterized verification)
*/
_( ghost \bool preemption )

/*	Following pointer variable models the set 
	of tasks in the system
*/
_( ghost Task *tasks )

/*	Following pointer variable models the priorities 
	of tasks in the system
*/
_( ghost Prio *priority )

/*	Following pointer variable models the task 
	lists in the system
*/
_( ghost Lists *lsts )

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




/*	Following structure models the system state
*/
_(dynamic_owns)
typedef struct system{
	/*	Following field models the highest index
		nonempty ready list
	*/
	_( ghost unsigned topReadyPriority )

	/*	Following field models the status of the 
		scheduler - running or not.
	*/
	_( ghost \bool schedulerRunning )

	/*	Following is a dummy field to 
		satisfy the requirement that 
		"every structure must contain 
		at least one physical field".
	*/
	unsigned dummy;

	//	Following variable models the system clock in Z1
	_(ghost \natural tickCount )
 
	/*	Following variable models the currently
		running task
	*/
	_( ghost taskID currentTask )

///////////////////////////////////////
	_( ghost \natural ovrFlwCount )
///////////////////////////////////////

	/*INV-1:	Idle task ( ID = 0 )
				is always ready to run
	*/
	_( invariant lsts->isInReady[ 0 ] )

	/*INV-2:	'topReadyPriority' is a valid index 
				to the array of ready task lists.
	*/
	_( invariant 
			( ( topReadyPriority >= 1 ) && ( topReadyPriority <= maxPrio ) )
	 )

	 /*INV-3:	The sequence of tasks at index 'topReadyPriority' 
				in the array 'ready' is nonempty.
	*/
	_( invariant 
			(	\mine( &( lsts->ready[topReadyPriority] ) )&&
				( lsts->ready[ topReadyPriority ].length > 0 ) 
			)
	 )

	/*INV-4:	Every non empty sequence of ready tasks
				is at an index less than or equal to
				'topReadyPriority'.
	*/
	_( invariant 
			(	\forall unsigned i; 
					(	\mine( &( lsts->ready[ i ] ) ) &&
						( lsts->ready[ i ].length > 0 ) 
					) ==> 	( i <= topReadyPriority ) 
			)
	 )

	/*INV-5:	Running task is at the head of the 
				ready list at index
				'topReadyPriority'
				when the scheduler is active.
	*/
	_( invariant 
		schedulerRunning ==> 
			(	//\mine( &( lsts->ready[ topReadyPriority ] ) ) &&
				( lsts->ready[ topReadyPriority ].list[ 0 ] == currentTask ) 
			)
	 )

	/*INV-6:	Running task is the null task ( ID = UINT_MAX )
				when the scheduler is not active
	*/
	_( invariant !schedulerRunning ==> ( currentTask == UINT_MAX ) )

	/*INV-7:	The set of tasks in the system is the 
				union of the tasks present in different task 
				lists in the system. There is a special task 
				called null (ID = UINT_MAX) which is not present 
				in any of the task lists.
	 */
	_( invariant 
		(	\forall taskID t; 
				( tasks->member[t] ) <==>
					(	( lsts->isInReady[ t ] )	||
						( lsts->indexDelayed[ t ] < lsts->delayedLength ) ||
						( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2 ) ||
						( lsts->indexODelayed[ t ] < lsts->oDelayedLength ) ||
						( lsts->blocked.index[ t ] < lsts->blocked.length ) ||
						( lsts->suspended[ t ] ) ||
						( t == UINT_MAX )
					)	
		)
	 )

	/*INV-8:	The special task in the system - 'null' ( ID = UINT_MAX)
				is not present in any task 
				lists in the system
	 */
	_( invariant	!(	
					( lsts->isInReady[ UINT_MAX ] )	||
					( lsts->indexDelayed[ UINT_MAX ] < lsts->delayedLength ) ||
					( lsts->indexDelayedZ2[ UINT_MAX ] < lsts->delayedLengthZ2 ) ||
					( lsts->indexODelayed[ UINT_MAX ] < lsts->oDelayedLength ) ||
					( lsts->blocked.index[ UINT_MAX ] < lsts->blocked.length ) ||
					( lsts->suspended[ UINT_MAX ] ) 	
				 )	
	 )

	/*INV-9a:	Prioriy is defined for all valid 
				tasks in the system.
				A valid task will have a priority 
				value in the interval
				[ 1,maxPrio ].
	 */
	_( invariant 
		(	\forall taskID t; 
				(	( tasks->member[ t ] ) &&
					( t != UINT_MAX ) 
				) <==>	(	( priority->value[ t ] >= 1 ) &&
							( priority->value[ t ] <= maxPrio ) 
						)	
		)
	 )


	/*INV-9b:	Null task will have the priority 
				value zero.
	*/
	_( invariant  ( priority->value[ UINT_MAX ] == 0 ) )

	/*INV-10:	The value of time to awake for each 
	  (10 in Z1)delayed task is greater than the value 
				of 'tickCount'
	 */
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->delayedLength )
					==> ( lsts->timeToAwake[ i ] > tickCount ) 
		)
	 )

	/*INV-11:	The value of time to awake for each 
	  (10 in Z2)delayedZ2 task is greater than the value 
				of 'tickCount'
	 */
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->delayedLengthZ2 )
					==> ( lsts->timeToAwakeZ2[ i ] > tickCount ) 
		)
	 )

	/*INV-12:	The value of time to awake for each 
	  (11 in Z2)task in the sequence 'oDelayed' is 
				less than or equal to 'tickCount'.
	 */
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->oDelayedLength )
					==> ( lsts->timeToAwakeOD[ i ] <= tickCount ) 
		)
	 )

	/*INV-13:	The value of time to awake for each 
	  (12 in Z2)task in the sequence 'delayedZ2' is 
				less than or equal to 'maxNumVal'.
	 */
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->delayedLengthZ2 )
					==> ( lsts->timeToAwakeZ2[ i ] <= maxNumVal ) 
		)
	 )


	/*INV-14:	The value of time to awake for each 
	  (13 in Z2)task in the sequence 'oDelayed' is 
				less than or equal to 'maxNumVal'.
	*/
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->oDelayedLength )
					==> ( lsts->timeToAwakeOD[ i ] <= maxNumVal ) 
		)
	 )

	/*INV-15:	The priority of tasks present in the 
				ready sequence at index say 'i' 
				is 'i'
	 */
	_( invariant 
		(	\forall taskID t; 
				(	\forall unsigned i;
						(	( i >= 1 ) &&
							( i <= maxPrio ) &&
							\mine( &( lsts->ready[ i ] ) ) &&
							( lsts->ready[ i ].index[ t ] < lsts->ready[ i ].length )
						) ==> ( priority->value[ t ] == i )		
				)
		)
	 )

	/*INV-16:	The task list 'blocked' is 
	  (15 in Z2)sorted in the non increasing order of 
				priority values. 
				This is equivalent to to inv no. 12 in Z1.
	 */
	_( invariant 
		(	\forall taskID t1,t2; 
				(	
						(	( lsts->blocked.index[ t1 ] < lsts->blocked.index[ t2 ] ) &&
							( lsts->blocked.index[ t1 ] < lsts->blocked.length ) &&
							( lsts->blocked.index[ t2 ] < lsts->blocked.length )
						) ==> (		( maxPrio - priority->value[ t1 ] ) <= 
									( maxPrio - priority->value[ t2 ] )		
							  )
				)
		)
	 )

	/*INV-17:	The value of tickCount is bounded by 
				'maxNumVal".
	*/
	_( invariant ( tickCount <= maxNumVal ) )

	/*INV-18:	Length of each ready list is bounded 
				by 'maxNumVal".
	*/
	_( invariant \forall unsigned i;
		(	( i >= 1 ) &&	
			( i <= maxPrio ) 
		) ==>	(	\mine( &( lsts->ready[ i ] ) ) &&
					( lsts->ready[ i ].length <= maxNumVal )
				)					
	 )
	
	/*INV-19:	Length of blocked list is bounded 
				by 'maxNumVal".
	*/
	_( invariant ( lsts->blocked.length <= maxNumVal ) )

	/*INV-20:	Length of the sequence 'delayedZ2' is bounded 
				by 'maxNumVal".
	*/
	_( invariant ( lsts->delayedLengthZ2 <= maxNumVal ) )

	/*INV-21:	Length of the sequence 'oDelayed' is bounded 
				by 'maxNumVal".
	*/
	_( invariant ( lsts->oDelayedLength <= maxNumVal ) )

	/*INV-22:	Length of the task set  suspended is bounded 
				by 'maxNumVal".
	*/
	_( invariant ( lsts->suspendedLength <= maxNumVal ) )

//////////////////////////////////////////////////
	/*INV-lists-auxiliary:	membership in ready */
	_( invariant \forall taskID t;
		lsts->isInReady[t] <==> (	\exists unsigned i;
									(	( i >= 1 ) && ( i <= maxPrio )   && 
										\mine( &( lsts->ready[ i ] ) ) &&
										( lsts->ready[ i ].index[ t ] < lsts->ready[ i ].length )
									)
								)
	 )

	/*INV-lists-1:	If a task is in ready[ i ] then it cannot be 
				present in 'delayed', 'delayedZ2', 'oDelayed',  
				'blocked' or 'suspended'.
	*/
	_( invariant \forall taskID t;
			lsts->isInReady[ t ] ==>	!(	( lsts->indexDelayed[ t ] < lsts->delayedLength ) ||
											( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2 ) ||
											( lsts->indexODelayed[ t ] < lsts->oDelayedLength ) ||
											(	\mine( &( lsts->blocked ) ) && 
												( lsts->blocked.index[ t ] < lsts->blocked.length ) ) ||
											( lsts->suspended[ t ] ) 
										 )
	 )


 	/*INV-lists-2:	If a task is in ready[ i ] then it cannot be 
				present in ready[ j ] when i != j.
	*/ 
	_( invariant \forall taskID t;
			(	\forall unsigned i,j;
					(	( i >= 1 )  &&
						( i <= maxPrio ) &&
						( j >= 1 )  &&
						( j <= maxPrio ) &&
						( i != j )				
					) ==> !(	(	\mine( &( lsts->ready[ i ] ) ) &&
									( lsts->ready[ i ].index[ t ] < lsts->ready[ i ].length ) 
								) &&
								(	\mine( &( lsts->ready[ j ] ) ) &&
									( lsts->ready[ j ].index[ t ] < lsts->ready[ j ].length ) 
								)
						   )
			)
	 )

	/*INV-lsts-9a:	This structure owns the sequences of 
				ready tasks for all valid index ( 1 -> maxPrio ).
				To support INV-12 etc..
	*/
	_( invariant \forall unsigned i;
			(	( i >= 1 ) &&	
				( i <= maxPrio ) 
			) ==> \mine( &( lsts->ready[ i ] ) )
	 )

	/*INV-lsts-9b:	This structure does not own the sequences of 
				ready tasks at invalid indices.
	*/
	_( invariant \forall unsigned i;
			(	( i == 0 ) ||	
				( i > maxPrio ) 
			) ==> !\mine( &( lsts->ready[ i ] ) )
	 )

	/*INV-lsts-auxiliary:	This structure owns the sequence of blocked
				tasks - 'blocked'
	*/
	_( invariant \mine( &( lsts->blocked ) )	 )
//////////////////////////////////////////////////

	/*INV-23:	System owns the global varaible 
				'maxPrio'
	*/
	_( invariant \mine( \embedding( &maxPrio ) ) )

	/*INV-24:	System owns the global varaible 
				'maxNumVal'
	*/
	_( invariant \mine(\embedding(&maxNumVal)) )

	/*INV-25:	System owns the global varaible 
				'preemption'
	*/
	_( invariant \mine( \embedding( &preemption ) ) )


	/*INV-26:	System owns the global pointer 
				varaible 'tasks'.
	*/
	_( invariant \mine( \embedding( &tasks ) ) )
	_( invariant \mine( tasks ) )

	/*INV-27:	System owns the global pointer 
				varaible 'priority'.
	*/
	_( invariant \mine( \embedding( &priority ) ) )
	_( invariant \mine( priority ) )

	/*INV-28:	System owns the global pointer 
				varaible 'lsts'.
	*/
	_( invariant \mine( \embedding( &lsts ) ) )
	_( invariant \mine( lsts ) )


	////////////////////////////////////Gluing relation between Z1 and Z2	 
	/*INV-Z1RZ2-5:	The value of time to awake for 
				the tasks in the sequence 'delayed' 
				is value for time to awake for the correspodnig  
				in the sequence 'delayedZ2'.
	*/	
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->delayedLengthZ2 )
					==> ( lsts->timeToAwake[ i ] == lsts->timeToAwakeZ2[ i ] )
		)
	 )

	/*INV-Z1RZ2-5:	The value of time to awake for 
				the tasks in the sequence 'delayed' 
				is value for time to awake for the correspodnig  
				in the sequence 'oDelayed' plus 
				'( ovrFlwCount + 1 )'.
	*/	
	_( invariant 
		(	\forall \natural i; 
				( i < lsts->oDelayedLength )
					==> (	lsts->timeToAwake[ i + lsts->delayedLengthZ2 ] == 
							( lsts->timeToAwakeOD[ i ] + ( maxNumVal + 1 ) )
						)
		)
	 )

} System;

System sstm;

void startScheduler()
	_( requires ( sstm.schedulerRunning == \false ) )
	_( requires ( lsts->ready[sstm.topReadyPriority].length > 0 ) )
	_( requires ( lsts->blocked.length == 0 ) )
	_( requires ( lsts->delayedLength == 0 ) )
	_( requires \wrapped( &sstm ) )
	_( requires \inv( &sstm ) )

	_( writes &( sstm ) )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )
	;

void taskDelayUntil1(  _( ghost \natural pWT )
									_( ghost \natural delay )
							 )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= maxNumVal ) )
	_( requires ( pWT <= sstm.tickCount ) )
	_( requires ( ( delay + pWT ) <= sstm.tickCount ) )

	_( requires \wrapped( &sstm ) )

	_( writes &( sstm ) )

//	_(ensures \false )
	;

void taskDelayUntil2(  _( ghost \natural pWT )
						_( ghost \natural delay )
					)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= maxNumVal ) )
	_( requires ( pWT > sstm.tickCount ) )
	_( requires ( ( delay + pWT ) <= maxNumVal ) )

	_( requires \wrapped( &sstm ) )

	_( writes &( sstm ) )

	_( ensures \wrapped( &sstm ) )

//	_(ensures \false )
	;

void taskDelayUntil3	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= maxNumVal ) )
	_( requires ( pWT > sstm.tickCount ) )
	_( requires ( ( delay + pWT ) > maxNumVal ) )
	_( requires ( ( delay + pWT ) < ( sstm.tickCount + ( maxNumVal + 1 ) ) ) )

	_( requires \wrapped( &sstm ) )

	_( writes &( sstm ) )

	_( ensures \wrapped( &sstm ) )

//	_(ensures \false )
	;

void taskDelayUntil4	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= sstm.tickCount ) )
	_( requires ( sstm.tickCount < ( delay + pWT ) ) )
	_( requires ( ( delay + pWT ) <= maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length > 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires \wrapped(&sstm) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )
	;

void taskDelayUntil5(	_( ghost \natural pWT )
						_( ghost \natural delay )
				    )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= sstm.tickCount ) )
	_( requires ( sstm.tickCount < ( delay + pWT ) ) )
	_( requires ( ( delay + pWT ) <= maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length == 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires \exists unsigned i;
				(	( i >= 1 ) &&
					( i < sstm.topReadyPriority ) &&
					( lsts->ready[ i ].length > 0 ) 
				)
	 )

	_( requires \wrapped( &sstm ) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )	
	;

void taskDelayUntil6	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= sstm.tickCount ) )
	_( requires ( ( delay + pWT ) > maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length > 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires \wrapped(&sstm) )

	_( writes &sstm  )


	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )
	;

void taskDelayUntil7	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= sstm.tickCount ) )
	_( requires ( ( delay + pWT ) > maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length == 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires \exists unsigned i;
				(	( i >= 1 ) &&
					( i < sstm.topReadyPriority ) &&
					( lsts->ready[ i ].length > 0 ) 
				)
	 )

	_( requires \wrapped( &sstm ) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )	
	;

void taskDelayUntil8	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= maxNumVal ) )
	_( requires ( pWT > sstm.tickCount ) )	// tickCount overflowed after pWT
	_( requires ( ( sstm.tickCount + ( maxNumVal + 1 ) ) < ( delay + pWT ) ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length > 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires \wrapped(&sstm) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )
	;

void taskDelayUntil9	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( pWT <= maxNumVal ) )
	_( requires ( pWT > sstm.tickCount ) )
	_( requires ( ( sstm.tickCount + ( maxNumVal + 1 ) ) < ( delay + pWT ) ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length == 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires \exists unsigned i;
				(	( i >= 1 ) &&
					( i < sstm.topReadyPriority ) &&
					( lsts->ready[ i ].length > 0 ) 
				)
	 )

	_( requires \wrapped( &sstm ) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )	
	;

void taskDelay1( _( ghost \natural delay ) )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay == 0 ) )

	_( requires \wrapped( &sstm ) )

	_( writes &( sstm ) )

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

void taskDelay2A( _( ghost \natural delay ) )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay > 0 ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length > 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )
	_( requires ( ( sstm.tickCount + delay ) <= maxNumVal ) )
							// Other case is considered in taskDelay2B
	_( requires \wrapped(&sstm) )

	_( writes &sstm  )

	//_(ensures \false )
	;

void taskDelay2B( _( ghost \natural delay ) )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay > 0 ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length > 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )
	_( requires ( ( sstm.tickCount + delay ) > maxNumVal ) )
							// Other case is considered in taskDelay2A
	_( requires \wrapped(&sstm) )

	_( writes &sstm  )

	//_(ensures \false )
	;

void taskDelay3A( _( ghost \natural delay ) )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay > 0 ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length == 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires ( ( sstm.tickCount + delay ) <= maxNumVal ) )
							// Other case is considered in taskDelay3B
	_( requires \exists unsigned i;
				(	( i >= 1 ) &&
					( i < sstm.topReadyPriority ) &&
					( lsts->ready[ i ].length > 0 ) 
				)
	 )

	_( requires \wrapped( &sstm ) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )	
	;

void taskDelay3B( _( ghost \natural delay ) )
	_( requires ( sstm.schedulerRunning == \true ) )
	_( requires ( delay > 0 ) )
	_( requires ( delay <= maxNumVal ) )
	_( requires ( sstm.currentTask != 0 ) )// ID zero means idle task
	_( requires ( lsts->ready[ sstm.topReadyPriority ].length == 1 ) )
	_( requires ( lsts->delayedLength < maxNumVal ) )

	_( requires ( ( sstm.tickCount + delay ) > maxNumVal ) )
							// Other case is considered in taskDelay3A
	_( requires \exists unsigned i;
				(	( i >= 1 ) &&
					( i < sstm.topReadyPriority ) &&
					( lsts->ready[ i ].length > 0 ) 
				)
	 )

	_( requires \wrapped( &sstm ) )

	_( writes &sstm  )

	_( ensures \wrapped( &sstm ) )

	//_(ensures \false )	
	;