[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

A doubt..records and functions(2 dump files).




Respected Sir,

	I am mailing two dump files, first containing the buffercache_t
	defined in function form and second containing buffercache_t 
	defined in record form.

	Thanks a lot for looking into the problem.

with regards,

Niranjan S. Pendharkar.
(nsp@csa.iisc.ernet.in).

> 
> Hi,
> 
> It should be possible to develop your specification using either
> records or arrays.  To find out what's going wrong, you'll need to
> provide more details: send a dump file (created by M-x dump) of a small
> example that works using records but not using arrays.
> 
> I suggest you send followup messages to pvs-help@csl.sri.com, rather
> than the entire PVS list.
> 
> John
> -------
> 

---------------START OF DUMP FILE 1--------------------------------------


%Patch files loaded: (patch2) version 2.399

$$$bc_func.pvs

bc_func  % [ parameters ]
		: THEORY

  BEGIN

	blk_t : TYPE = { BLK1, BLK2 }
	pc_t : TYPE = { INIT, TRYING, SLEEP_ANY, SLEEP_BLK, GOT_BUF }
	
	buffer_t : TYPE = [#
		blk : blk_t,
		valid : bool,
		locked : bool
		#]

	index_t : TYPE = { i : nat | i = 1 } CONTAINING 1

	buffercache_t : TYPE = ARRAY [ index_t -> buffer_t ]

	one : index_t

	state : TYPE = [#
		
		pcA : pc_t,
		pcB : pc_t,
		blkA : blk_t,
		blkB : blk_t,
		buffercache : buffercache_t

		#]
	
	   IMPORTING state[state], compose[state], ctlops[state]

	s, s0, s1, s2 : VAR state

	hashed?(bl : blk_t, bc : buffercache_t, i : index_t) : bool = 

 		(valid(bc(i)) AND (blk(bc(i)) = bl))

	locked_buf?(b1 : blk_t, bc : buffercache_t, i : index_t) : bool = 


		(valid(bc(i)) AND (blk(bc(i)) = b1) AND locked(bc(i)))


	cache_with_locked_buf(b1 : blk_t, bc : buffercache_t, i : index_t) 
	: buffercache_t = 


		bc WITH [(i) := bc(i) WITH [(locked) := TRUE]]


	update_cache(b1 : blk_t, bc : buffercache_t, i : index_t) 
	: buffercache_t = 

	bc WITH [(i) := bc(i) WITH [(blk) := b1, (locked) := TRUE, 
									(valid) := TRUE]]


	any_free?(bc : buffercache_t, i : index_t) : bool = 

		(NOT locked(bc(i)) OR NOT valid(bc(i)))

	this_buf_locked?(b1 : blk_t, bc : buffercache_t, i : index_t) : bool = 

		(valid(bc(i)) AND (blk(bc(i)) = b1) AND locked(bc(i)))

	cache_with_unlocked_buf(b1 : blk_t, bc : buffercache_t, i : index_t) 
	: buffercache_t =
	
		bc WITH [(i) := bc(i) WITH [(locked) := FALSE]]

	% process A intialization.


	I_A(s) : bool = 
		( 
			(pcA(s) = INIT) AND
			(NOT valid((buffercache(s)(one))))
		)

	G_A(s,s1) : bool = 
		(

			((pcA(s) = INIT) AND (s1 = s WITH [(pcA) := TRYING]))

		OR

			((pcA(s) = TRYING) AND

				IF (hashed?(blkA(s), buffercache(s), one)) THEN
					
					IF locked_buf?(blkA(s), buffercache(s), one) THEN
	
						(s1 = s WITH [(pcA) := SLEEP_BLK])

					ELSE (s1 = s WITH [(pcA) := GOT_BUF,

				(buffercache) := cache_with_locked_buf(blkA(s), 
											buffercache(s), one)])
			
					ENDIF

				ELSE

					IF(NOT any_free?(buffercache(s), one)) THEN

						(s1 = s WITH [(pcA) := SLEEP_ANY])

					ELSE

						( s1 = s WITH [(pcA) := GOT_BUF,
					(buffercache) := update_cache(blkA(s), buffercache(s), 
													one)])

					ENDIF
				
				ENDIF)

		OR

			( (pcA(s) = SLEEP_ANY) AND 
		
				IF( any_free?(buffercache(s), one)) THEN

					s1 = s WITH [(pcA) := TRYING]

				ELSE

					s1 = s

				ENDIF )

		OR

			( (pcA(s) = SLEEP_BLK) AND

				IF (NOT this_buf_locked?(blkA(s), buffercache(s), one)) THEN
				
					s1 = s WITH [(pcA) := TRYING]

				ELSE

					s1 = s

				ENDIF)

		OR

			( (pcA(s) = GOT_BUF) AND

				(s1 = s WITH [ (pcA) := INIT,

				(buffercache) := 

				cache_with_unlocked_buf(blkA(s), buffercache(s), one)]))

		)


	R_A(s,s1) : bool = 
		
		(
			(pcA(s1) = pcA(s)) AND (blkA(s1) = blkA(s)) AND 

			(blkB(s1) = blkB(s)) AND

			( (pcB(s) = TRYING AND ((buffercache(s1) = 
					cache_with_locked_buf(blkB(s), buffercache(s), one))
						OR
					(buffercache(s1) = buffercache(s))) )
				
				OR

			  	(pcB(s) = TRYING AND ((buffercache(s1) = 
					update_cache(blkB(s), buffercache(s), one))
						OR
					(buffercache(s1) = buffercache(s))))
		
				OR

			  (pcB(s) = GOT_BUF AND (buffercache(s1) = 
					cache_with_unlocked_buf(blkB(s), buffercache(s), one)))

				OR
				
			  (pcB(s) = SLEEP_BLK AND
				(buffercache(s1) = buffercache(s)))
				
				OR

			  (pcB(s) = SLEEP_ANY AND
				(buffercache(s1) = buffercache(s))) )
				
		)



	% process B initialization.

	I_B(s) : bool = 
		( 
			(pcB(s) = INIT) AND
			(NOT valid(buffercache(s)(one)))
		)


	G_B(s,s1) : bool = 
		(

			((pcB(s) = INIT) AND (s1 = s WITH [(pcB) := TRYING]))

		OR

			((pcB(s) = TRYING) AND

				IF (hashed?(blkB(s), buffercache(s), one)) THEN
					
					IF locked_buf?(blkB(s), buffercache(s), one) THEN
	
						(s1 = s WITH [(pcB) := SLEEP_BLK])

					ELSE (s1 = s WITH [(pcB) := GOT_BUF,

				(buffercache) := cache_with_locked_buf(blkB(s), 
											buffercache(s), one)])
			
					ENDIF

				ELSE

					IF(NOT any_free?(buffercache(s), one)) THEN

						(s1 = s WITH [(pcB) := SLEEP_ANY])

					ELSE

						( s1 = s WITH [(pcB) := GOT_BUF,
					(buffercache) := update_cache(blkB(s), buffercache(s), 
										one)])

					ENDIF
				
				ENDIF)

		OR

			( (pcB(s) = SLEEP_ANY) AND 
		
				IF( any_free?(buffercache(s), one)) THEN

					s1 = s WITH [(pcB) := TRYING]

				ELSE

					s1 = s

				ENDIF )

		OR

			( (pcB(s) = SLEEP_BLK) AND

				IF (NOT this_buf_locked?(blkB(s), buffercache(s), one)) THEN
				
					s1 = s WITH [(pcB) := TRYING]

				ELSE

					s1 = s

				ENDIF)

		OR

			( (pcB(s) = GOT_BUF) AND

				(s1 = s WITH [ (pcB) := INIT,

				(buffercache) := 

				cache_with_unlocked_buf(blkB(s), buffercache(s), one)]))

		)


	R_B(s,s1) : bool = 
		
		(
			(pcB(s1) = pcB(s)) AND (blkB(s1) = blkB(s)) AND 

			(blkA(s1) = blkA(s)) AND

			( (pcA(s) = TRYING AND ((buffercache(s1) = 
					cache_with_locked_buf(blkA(s), buffercache(s), one))
						OR
					(buffercache(s1) = buffercache(s))) )
				
				OR

			  	(pcA(s) = TRYING AND ((buffercache(s1) = 
					update_cache(blkA(s), buffercache(s), one))
						OR
					(buffercache(s1) = buffercache(s))))
		
				OR

			  (pcA(s) = GOT_BUF AND (buffercache(s1) = 
					cache_with_unlocked_buf(blkA(s), buffercache(s), one)))

				OR
				
			  (pcA(s) = SLEEP_BLK AND
				(buffercache(s1) = buffercache(s)))
				
				OR

			  (pcA(s) = SLEEP_ANY AND
				(buffercache(s1) = buffercache(s))) )
				
		)




	buffer2prog: Program =
    Compose((# init := I_A, G := G_A, R := R_A#),
            (# init := I_B, G := G_B, R := R_B#))


	mutex : LEMMA
		init(buffer2prog)(s0) IMPLIES
		AG((LAMBDA s,s1 : G(buffer2prog)(s,s1) OR R(buffer2prog)(s,s1)),
			(LAMBDA s: NOT (pcA(s) = GOT_BUF AND pcB(s) = GOT_BUF)))(s0)


  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  

  END bc_func

$$$bc_func.prf
(|bc_func|
 (|mutex| "" (MODEL-CHECK)
  (("" (EXPAND "Compose")
    (("" (MODEL-CHECK) (("" (MODEL-CHECK) (("" (POSTPONE) NIL))))))))))

-----------------END OF DUMP FILE 1-------------------------------------


%Patch files loaded: (patch2) version 2.399

$$$bc_record.pvs

bc_record  % [ parameters ]
		: THEORY

  BEGIN

	blk_t : TYPE = { BLK1, BLK2 }
	pc_t : TYPE = { INIT, TRYING, SLEEP_ANY, SLEEP_BLK, GOT_BUF }
	
	buffer_t : TYPE = [#
		blk : blk_t,
		valid : bool,
		locked : bool
		#]


	buffercache_t : TYPE = [#

		buffer1 : buffer_t
		
		#]

	state : TYPE = [#
		
		pcA : pc_t,
		pcB : pc_t,
		blkA : blk_t,
		blkB : blk_t,
		buffercache : buffercache_t

		#]
	
	   IMPORTING state[state], compose[state], ctlops[state]

	s, s0, s1, s2 : VAR state

	hashed?(bl : blk_t, bc : buffercache_t) : bool = 

 		(valid(buffer1(bc)) AND (blk(buffer1(bc)) = bl))

	locked_buf?(b1 : blk_t, bc : buffercache_t) : bool = 

		(valid(buffer1(bc)) AND blk(buffer1(bc)) = b1 AND locked(buffer1(bc)))


	cache_with_locked_buf(b1 : blk_t, bc : buffercache_t) : buffercache_t = 

		bc WITH [(buffer1) := buffer1(bc) WITH [(locked) := TRUE]]


	update_cache(b1 : blk_t, bc : buffercache_t) : buffercache_t = 

	bc WITH [(buffer1) := buffer1(bc) WITH [(blk) := b1, (locked) := TRUE,
														(valid) := TRUE]]



	any_free?(bc : buffercache_t) : bool = 

		(NOT locked(buffer1(bc)) OR NOT valid(buffer1(bc)))

	this_buf_locked?(b1 : blk_t, bc : buffercache_t) : bool = 

	(valid(buffer1(bc)) AND (blk(buffer1(bc)) = b1) AND locked(buffer1(bc)))

	cache_with_unlocked_buf(b1 : blk_t, bc : buffercache_t) : buffercache_t =
	
		bc WITH [(buffer1) := buffer1(bc) WITH [(locked) := FALSE]]

	% process A intialization.


	I_A(s) : bool = 
		( 
			(pcA(s) = INIT) AND
			(NOT valid(buffer1(buffercache(s))))
		)

	G_A(s,s1) : bool = 
		(

			((pcA(s) = INIT) AND (s1 = s WITH [(pcA) := TRYING]))

		OR

			((pcA(s) = TRYING) AND

				IF (hashed?(blkA(s), buffercache(s))) THEN
					
					IF locked_buf?(blkA(s), buffercache(s)) THEN
	
						(s1 = s WITH [(pcA) := SLEEP_BLK])

					ELSE (s1 = s WITH [(pcA) := GOT_BUF,
								(buffercache) := 
						cache_with_locked_buf(blkA(s), buffercache(s))])

			
					ENDIF

				ELSE

					IF(NOT any_free?(buffercache(s))) THEN

						(s1 = s WITH [(pcA) := SLEEP_ANY])

					ELSE

						( s1 = s WITH [(pcA) := GOT_BUF,
					(buffercache) := update_cache(blkA(s), buffercache(s))])

					ENDIF
				
				ENDIF)

		OR

			( (pcA(s) = SLEEP_ANY) AND 
		
				IF( any_free?(buffercache(s))) THEN

					s1 = s WITH [(pcA) := TRYING]

				ELSE

					s1 = s

				ENDIF )

		OR

			( (pcA(s) = SLEEP_BLK) AND

				IF (NOT this_buf_locked?(blkA(s), buffercache(s))) THEN
				
					s1 = s WITH [(pcA) := TRYING]

				ELSE

					s1 = s

				ENDIF)

		OR

			( (pcA(s) = GOT_BUF) AND

				(s1 = s WITH [ (pcA) := INIT,

				(buffercache) := 
				cache_with_unlocked_buf(blkA(s), buffercache(s))])) 

		)



	R_A(s,s1) : bool = 
		
		(
			(pcA(s1) = pcA(s)) AND (blkA(s1) = blkA(s)) AND 

			(blkB(s1) = blkB(s)) AND

			( (pcB(s) = TRYING AND ((buffercache(s1) = 
					cache_with_locked_buf(blkB(s), buffercache(s)))
						OR
					(buffercache(s1) = buffercache(s))) )
				
				OR

			  	(pcB(s) = TRYING AND ((buffercache(s1) = 
					update_cache(blkB(s), buffercache(s)))
						OR
					(buffercache(s1) = buffercache(s))))
		
				OR

			  (pcB(s) = GOT_BUF AND (buffercache(s1) = 
					cache_with_unlocked_buf(blkB(s), buffercache(s))))

				OR
				
			  (pcB(s) = SLEEP_BLK AND
				(buffercache(s1) = buffercache(s)))
				
				OR

			  (pcB(s) = SLEEP_ANY AND
				(buffercache(s1) = buffercache(s))) )
				
		)


	% process B initialization.

	I_B(s) : bool = 
		( 
			(pcB(s) = INIT) AND
			(NOT valid(buffer1(buffercache(s))))
		)

	G_B(s,s1) : bool = 
		(

			((pcB(s) = INIT) AND (s1 = s WITH [(pcB) := TRYING]))

		OR

			((pcB(s) = TRYING) AND

				IF (hashed?(blkB(s), buffercache(s))) THEN
					
					IF locked_buf?(blkB(s), buffercache(s)) THEN
	
						(s1 = s WITH [(pcB) := SLEEP_BLK])

					ELSE (s1 = s WITH [(pcB) := GOT_BUF,
								(buffercache) := 
						cache_with_locked_buf(blkB(s), buffercache(s))])

			
					ENDIF

				ELSE

					IF(NOT any_free?(buffercache(s))) THEN

						(s1 = s WITH [(pcB) := SLEEP_ANY])

					ELSE

						( s1 = s WITH [(pcB) := GOT_BUF,
					(buffercache) := update_cache(blkB(s), buffercache(s))])

					ENDIF
				
				ENDIF)

		OR

			( (pcB(s) = SLEEP_ANY) AND 
		
				IF( any_free?(buffercache(s))) THEN

					s1 = s WITH [(pcB) := TRYING]

				ELSE

					s1 = s

				ENDIF )

		OR

			( (pcB(s) = SLEEP_BLK) AND

				IF (NOT this_buf_locked?(blkB(s), buffercache(s))) THEN
				
					s1 = s WITH [(pcB) := TRYING]

				ELSE

					s1 = s

				ENDIF)

		OR

			( (pcB(s) = GOT_BUF) AND

				(s1 = s WITH [ (pcB) := INIT,

				(buffercache) := 
				cache_with_unlocked_buf(blkB(s), buffercache(s))])) 

		)


	R_B(s,s1) : bool = 
		
		(
			(pcB(s1) = pcB(s)) AND (blkB(s1) = blkB(s)) AND 

			(blkA(s1) = blkA(s)) AND

			( (pcA(s) = TRYING AND ((buffercache(s1) = 
					cache_with_locked_buf(blkA(s), buffercache(s)))
						OR
					(buffercache(s1) = buffercache(s))) )
				
				OR

			  	(pcA(s) = TRYING AND ((buffercache(s1) = 
					update_cache(blkA(s), buffercache(s)))
						OR
					(buffercache(s1) = buffercache(s))))
		
				OR

			  (pcA(s) = GOT_BUF AND (buffercache(s1) = 
					cache_with_unlocked_buf(blkA(s), buffercache(s))))

				OR
				
			  (pcA(s) = SLEEP_BLK AND
				(buffercache(s1) = buffercache(s)))

				OR

			  (pcA(s) = SLEEP_ANY AND
				(buffercache(s1) = buffercache(s))) )
				
		)





	buffer2prog: Program =
    Compose((# init := I_A, G := G_A, R := R_A#),
            (# init := I_B, G := G_B, R := R_B#))


	mutex : LEMMA
		init(buffer2prog)(s0) IMPLIES
		AG((LAMBDA s,s1 : G(buffer2prog)(s,s1) OR R(buffer2prog)(s,s1)),
			(LAMBDA s: NOT (pcA(s) = GOT_BUF AND pcB(s) = GOT_BUF)))(s0)


  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  

  END bc_record

$$$bc_record.prf
(|bc_record|
 (|mutex| "" (MODEL-CHECK) (("" (EXPAND "Compose") (("" (MODEL-CHECK) NIL))))))

 ---------------------END OF DUMP FILE 2----------------------------