Using SpeAR - lgwagner/SpeAR GitHub Wiki
We have provided some examples together with the installation of SpeAR to help the new user get started using the tool. If you are using the default workspace (./workspace), you should already see the ‘examples’ project in the Project Explorer View of SpeAR. If not, follow these steps to import the ‘examples’ project.
First, select File -> Import from the SpeAR menu. Alternatively, right-click in the Project Explorer View and select “Import.”
Select “Existing Projects into Workspace” and click “Next.”
Browse to the ‘examples’ folder in the workspace subfolder of the SpeAR installation and select OK.
Ensure the box is checked for the ‘examples’ project and select “Finish.”
Before running analysis, you must open the file in the SpeAR Editor. This is done by double-clicking on the file in the Project Explorer View. Alternatively, you can right-click on the file and select ‘Open’ or ‘Open With’ -> ‘SpeAR Editor.’ Use one of these two options to open examples -> user-guide -> thermostat -> thermostat.spear in the SpeAR Editor.
In the SpeAR Editor View, you should see the contents of the thermostat.spear file.
Logical entailment analysis is the primary SpeAR analysis. It checks whether each of the properties is logically entailed, or implied, by the conjunction of the assumptions and requirements. See Logical Entailment for further explanation of logical entailment analysis.
There are two ways to run logical entailment analysis. The easiest way is to click the 
button in the menu. The other way to run logical entailment analysis is to select SpeAR -> Check Logical Entailment from the menu. Use one of these two options to run logical entailment analysis on thermostat.spear. The Analysis Results View should appear automatically at the bottom of the SpeAR window.
The green checkmark shows that each property has been proved valid. That is, each of the properties stated in the Properties section of the file is a logical consequence of the set of assumptions and requirements. This is also indicated by the word “Valid” for each property in the “Result” column.
In this subsection, we will walk through how to view a counterexample and how to debug a specification using a counterexample.
Let’s start by running logical entailment analysis on an example with a failed property. Open thermostat_underspecified.spear in the SpeAR Editor.
Run logical entailment analysis on thermostat_underspecified.spear. The Analysis Results should appear as shown below.
Note that for this file, one of the properties (p_elatch) is invalid as shown with the red box and exclamation point, as well as with the word “Invalid” in the “Result” column.
SpeAR provides the user a counterexample for each invalid property to help the user understand the problem. To view the counterexample to p_elatch, right-click on p_elatch in the Analysis Results View and select a viewing method. The “View Counterexample in Eclipse” method is preferred by most users because data is collapsed automatically. The “View Counterexample in Excel” method is useful for saving and sharing counterexamples. We will choose “View Counterexample in Eclipse.”
If you selected “View Counterexample in Eclipse,” you should see the Counterexample View appear as shown below. Note that the actual values in the counterexample you see may differ from those shown below. The tool presents the user with a counterexample, but the counterexample is not unique.
The columns “Step 1” and “Step 2” refer to the first and second timesteps, respectively. SpeAR typically finds a counterexample with a minimum number of steps. As you can see in the p_elatch row of the Counterexample View, the p_elatch property is initially true but then becomes false on the second timestep. To understand this property further, let’s look at the p_elatch statement in the thermostat_underspecified specification (i.e., in thermostat_underspecified.spear). It is as shown below.
This property states that once the heater command is ERROR, it remains equal to ERROR. Reviewing the requirements, we see that r2 specifies the condition under which the heater_command is equal to ERROR.
If the timer is greater than TIMEOUT, then the heater_command is equal to ERROR. The TIMEOUT constant is set to 10 as shown in the ‘Constants’ section of the file.
Looking back at the counterexample, we see that the timer is equal to 11 on Step 1 and is equal to 10 on Step 2. The timer appears to be “counting down,” but requirement r2 seems to indicate the author expected the timer to be counting up to TIMEOUT. Reviewing the thermostat_underspecified specification a second time reveals that no behavior has been specified for the timer.
Add a new requirement r3 to the Requirements section of the file. (If you wish, you may first save the file with a new name by going to File -> Save As in the menu.)
After adding the new requirement, run logical entailment analysis again. All properties should now be proven valid.
Logical entailment is only valid if the captured requirements and assumptions are not conflicting. When there is a conflict among requirements or assumptions, the logical conjunction of the constraints is false, and thus the logical implication of any property is vacuously true.
Let’s run consistency analysis on an example. First, open examples -> user-guide -> consistency -> consistency.spear in the SpeAR editor.
To run consistency analysis, click the 
icon in the menu bar. Alternatively, select SpeAR -> Check Logical Consistency from the menu. The Analysis Results View should appear automatically and show an invalid results for ‘consistent.’
By right-clicking on the word ‘consistent’ and selecting “Show Conflicting Constraints,” you can view a minimum (or near-minimum) set of conflicting constraints. In this case, the assumption a0 that x is positive and the requirement r0 that y is negative conflict with the requirement r1 that y is greater than x.
Consistency analysis can only identify conflicts that occur for all inputs within a finite number of steps (see Logical Consistency). A more powerful check for conflicts is called realizability analysis and is described in the next subsection.
While consistency analysis is useful, it is not sufficient to find all conflicts amongst the assumptions and requirements. In particular, if two requirements are only in conflict for some input values, the consistency check will not identify the conflict. Hence a more powerful check called realizability analysis was added to SpeAR.
A specification is realizable if it is possible to construct an implementation that satisfies all of the assumptions and requirements. Let’s look at an example. Open examples -> user-guide -> realizability -> realizabilityTest1.spear in the SpeAR Editor.
To run realizability analysis, click the 
icon in the menu bar. Alternatively, select SpeAR -> Check Realizability from the menu. The Analysis Results View should pop up, showing an invalid result for “SpeAR Realizability Result.”
Right-click on “SpeAR Realizability Result” and select “View Counterexample in Eclipse.” A realizability counterexample is a trace where two or more of the assumptions and requirements are in conflict. In this case, we have just two requirements and they are both shown to be false for this counterexample.
The input value for a in this example is three. Note that when a is equal to three, requirement r1 says b is equal to two, but requirement r2 says that b is equal to four. This is clearly a conflict.
One possible solution is to change the condition of requirement r1 to be “a < 3.” Make this change, saving the file with a new name if you wish.
Running realizability analysis a second time shows that the specification is now realizable.
Realizability analysis is very important for finding conflicts amongst assumptions and requirements. Without it, the user is likely to prove some properties that are not actually true for all inputs. Note, for example, that without the fix to r1 in realizabilityTest1.spear, the user can prove the property that a is not equal to three, even though there is no such assumption about the input.
Realizability analysis does have its limitations. It will often come back with unknown.
Additional examples have been provided in the realizability folder. These show other kinds of problems that realizability analysis can detect.
So far we have worked with existing files in existing projects. In this subsection, we will describe how to create a new project. In the next subsection, we will walk through how to develop a new specification.
To create a new project, go to File -> New -> Project.
In the New Project Wizard, select General -> Project, and then click “Next.”
Give your project a name and select a location for the project. In this example, we will create an “arithmetic” project. We recommend choosing a permanent location outside the workspace. Then click “Finish."
A new project with your project name should appear in the Project Explorer View.
You can now create new files in this project. That process is described in the next subsection.
Before creating a specification file, you need a project to add the file to. If you do not have an existing project, please see the previous subsection for details on how to do this.
We will now walk through how to create a new specification using the SpeAR File Wizard. First, select (click on) the project you wish to add the new file to, and then select File -> New -> Other from the menu.
From the New File Wizard, select SpeAR -> Create new SpeAR specification file. Then click “Next.”
Confirm that the Container is the project you want the file added to. Give the file a name with the spear extension (we’ll use adder.spear in this example), and then click “Finish.” Note that hyphens are not allowed in SpeAR specification names, so it is best not to use them in the file names either.
If you receive a pop-up asking if you want to convert your project to an Xtext project, select “Yes.”
You should now see your new file in the Project Explorer View if you expand the project. You should also see the file contents in the Editor.
The template file includes all the possible sections of a SpeAR file together with comments that tell you whether each section header is optional or mandatory. See Overview of SpeAR for a brief description of each of the sections of the file. Note that the last two sections are ‘DerivedRequirements’ and ‘Requirements.’ These are the default section headers. We have used ‘Requirements’ and ‘Properties’ until now in this User Guide. The important thing to know is that for logical entailment analysis, the tool attempts to prove the statements in the last section (whatever its name may be) using the constraints in all sections that precede it. Consistency and realizability look for conflicts amongst the constraints.
We will now fill in the contents of a specification for an adder (i.e., an addition operator) as an example. Note that the specification name matches the file name by default, so we do not need to modify the specification name. The first thing we need are two inputs to add. In the ‘Inputs’ section, add two input variables. We will need to pick a type for these. Let’s use integers for this example.
Note that there are two ways to declare the type. You can use the symbol ‘:’ or the phrase “is an.” (The phrase “is a” is also supported.)
Next we need to declare the output. We do that in the ‘Outputs’ section of the file. Since this is a specification for adding two integers, the output will also be an integer.
We have one requirement: that the output of ‘adder’ is equal to the sum of its inputs. Write a requirement (or derived requirement) in the ‘DerivedRequirements’ section stating that. You will need to give the requirement a name. In this case, we use r0.
Note that SpeAR’s addition is unbounded.
That’s it! Now you can state and check properties of your adder. For example, if the inputs are positive, then the output should be positive. Add a property (requirement) stating this, and then prove it by running logical entailment analysis.
Try some additional properties of your own.
In this subsection, we demonstrated how to create a new specification file using the SpeAR File Wizard. You may wish to tailor the file generated by the wizard with the section headers you want to use. From that point on, you can simply copy your template file, rename it, and modify it for each new specification you wish to create.