Configuration of SpeAR Preferences - lgwagner/SpeAR GitHub Wiki
This section describes the SpeAR settings that can be changed via the SpeAR Preferences window. To access the SpeAR preferences, go to Window -> Preferences in the menu. On the left-hand side of the pop-up window, select SpeAR -> Analysis to view the SpeAR preferences. You should see a settings window similar to that shown below.
Most users will only need to modify the solver selection, the number of PDR instances, and the timeout. In this section, we walk through all the settings from top to bottom.
The SMT Solver drop down allows the user to select a solver. The options are SMTInterpol, Z3, Yices 2, and CVC4. Recall that Z3 is needed to run realizability analysis. For entailment analysis, you may wish to experiment with the other solvers to compare their performance on your model.
The three checkboxes that follow are for the different techniques that are used during analysis: bounded model checking, k-induction, and invariant generation. It is recommended to leave all three boxes checked.
Next is a text box where the user can specify the number of PDR instances to use. Setting this to 1 is a good place to start. In our experience, PDR = 0 is not sufficient to prove some properties. If your computer has six or more cores, you can set the number of PDR instances to four less than the number of cores on your machine. Using more than one PDR instance can speed up analysis but typically not if they are sharing a core. The reason we recommend four less than the number of cores on the machine is that it is ideal for the the main thread and the three other engines to each get a core.
By default, Generate inductive counterexamples is checked. This is the setting that controls whether or not an inductive counterexample is generated and made available for a property with an unknown result. They can help the user identify states which the model checker thinks may be reachable, and the user can in turn refine the property or state a supporting property/lemma. However, generating and storing these inductive counterexamples uses memory and as a result may slow down analysis; so this can be turned off when the inductive counterexamples are not being used by the user. It is recommended to turn this setting off until the user needs to investigate some properties with unknown results (in which case analysis can be run again with this setting turned on).
Generate smooth counterexamples (minimal number of input value changes) is available with Yices 2 and Z3. It attempts to minimize the changes in the values in a counterexample. This can help to avoid distracting value changes.
Generalize counterexamples using interval analysis works for all solvers. It attempts to provide an interval of values that will generate the same type of counterexample.
The maximum depth for k-induction is the max size of k that the tool will consider. Reducing the size of k may save some analysis time. Increasing the size of k may enable a property to be validated. Our experience to date is that k=100 or even k=20 is sufficient.
The next box is the timeout in seconds. This is the time at which the model checker gives up on properties it has not get proven and reports "unknown." We have seen top-level files that require 15-20 minutes to prove all the properties.
Debug mode (record log files) will store log files for debugging purposes. This is useful for SpeAR developers. Generate Lustre File will store the intermediate Lustre representation to a file. This feature is also more for SpeAR developers. Make graphical display recursive selection controls whether "Generate Graphical View" recursively includes imported specifications as well. Enabling IVC is required for traceability analysis. Disable unused variable validations turns off validation warnings indicating when a variable is defined by never referenced. These are annoying to some users.
Finally, there is a text box to set the depth for consistency checking. The consistency checker will look for a single trace of length greater than this depth such that the requirements are all satisfied. If it finds one, it declares the specification "consistent." (Recall that this is not a proof of consistency for all inputs and for unbounded traces. Realizability provides that stronger kind of consistency analysis.)