--------------------------------------- 3 Threads  -----------------------------------------

With hash-compact!

 Property						Result		Depth	State vector	Total time    Total memory   States
 --------						------		-----	------------	----------	  -----------    ------
[]!(read_A[0] && write_A[0])	Success		191			64				0.047		543.592		  33189
[]!(read_A[1] && write_A[1])	Success		191			64				0.046		543.592		  33189
[]!(read_A[2] && write_A[2])	Success		191			64				0.047		543.592		  33189



Verification (without hash-compact) for termination and non-deadlock 

 Property						Result		Depth	State vector	Total time    Total memory   States
 --------						------		-----	------------	----------	  -----------    ------
<> fin0 						Success		194			60				0.203		4.747		  67296
<> fin1 						Success		192			60				0.203		4.747		  67278
<> fin2 						Success		190			60				0.203		4.747		  67278


Verification with hash-compact:

 Property						Result		Depth	State vector	Total time    Total memory   States
 --------						------		-----	------------	----------	  -----------    ------
<> fin0 						Success		194			60				0.109		3.379		  67296
<> fin1 						Success		192			60				0.125		3.379		  67278
<> fin2 						Success		190			60				0.125		3.379		  67278


--------------------------------------- 4 Threads  -----------------------------------------

With hash-compact!

 Property						Result		Depth	State vector	Total time    Total memory   States
 --------						------		-----	------------	----------	  -----------    ------
[]!(read_A[0] && write_A[0])	Success		255			80				5.11		613.611		  2656001
[]!(read_A[1] && write_A[1])	Success		255			80				5.11		613.611		  2656001
[]!(read_A[2] && write_A[2])	Success		255			80				5.11		613.611		  2656001
[]!(read_A[3] && write_A[3])	Success		255			80				5.12		613.611		  2656001


Verification (with hash-compact) for termination and non-deadlock 

 Property						Result		Depth	State vector	Total time    Total memory   States
 --------						------		-----	------------	----------	  -----------    ------
<> fin0 						Success		260			72				12.4		111.739		  2681440
<> fin1 						Success		258			72				12.4		111.739		  2681444
<> fin2 						Success		256			72				12.3		111.739		  2681508
<> fin3 						Success		254			72				12.4		111.739		  2682532


--------------------------------------- 5 Threads  -----------------------------------------

With hash-compact! out of memory both for data race-freedom and deadlock-freedom