Using a simple data abstraction

We will turn our attention back to the main frame of the BUI. If you look at the code in the main method of class PipeInt, you will see that the for loop sends integers from 1 to 100 through the pipeline, and this relatively wide range of values will cause the model-check of the given property to run for many hours. In fact, because a zero value is used to indicate shutdown, proving the given property only requires distinguishing zero from non-zero queue values.

To dramatically reduce the cost of checking this property, we will abstract the queue values to three abstract tokens neg, zero, and pos using the Abstraction Manager. This abstraction is called the Signs abstraction.

• Click on the Typer option on the tool-bar of the main window. This will bring out the Abstraction Manager window. Expand the Default Package by double-clicking on it. Then double-click on PipeInt, then expand main method to see the variables used in the method.
• We need to use the abstraction for the integer i. Go to the Abstraction column of the i's row and left-click there. You should see the menu with different options pop up, as shown in Figure 12.

   

   

  
  Figure 12: Abstraction Manager Window
  

• Choose the Signs abstraction, then click on the running man at the left upper corner of the Abstraction Manager window to run the type inference. This will bring out another window that will let you know whether the type inference failed or succeeded. You should get an OK message this time. Dismiss the little window.
• You can save the abstractions you used to a file by clicking on the Save option next to the running man. This will bring out the window that will let you save the abstraction selection in your working directory. Navigate through the hierarchy of directories to save the file in the directory of your choice. You should use the extension .abstraction for your file. You can close the Abstraction Manager window now.

To finish this session check the SLABS option on the upper tool-bar of the main window to enable the use of abstractions.

To pick the model checker you want to use at the back end of Bandera, bring out the Session Manager window by clicking on the Session option of the main window. Click on the Checker tab at the top of the Session Manager window and pick the model checker Spin.

Enable the Checker on the top tool-bar and Run Bandera again. After some period of time, you should get a confirmation that your property is verified as shown in Figure 13.

 

 

Figure 13: Pipeline Verified