D.4.1 Introduction
The BMC/DCValidator expects an ASCII file as its input. This file contains a straightforward textual representation of the DC formula(s) to be verified, along with a selection of the settings as explained in Section D.3 on page 108.
Macros may be defined to abbreviate complex formulas. Before parsing the input files, a preprocessor will inline the macro definitions.
First, we shall give an example of an input file, and then we will give a detailed explanation of the abstract syntax of the input format. For a formal specification of the input format, please refer to the BNF in Appendix E on page 115.
APPENDIX D. USER’S GUIDE
D.4.2 Example
The following is an input file for checking the validity of 2 l≤30⇒R
(gas∧ ¬flame)≤5 by performing bounded model checking withk= 31.
:- set k = 31.
:- set outputFormat = zolcs.
:- state gas.
:- state flame.
:- leak =^= (gas /\ ~flame).
:- m =^= 30.
:- gbsafe(n) =^= all(l <= m -> dur leak <= n).
:- goal gbsafeout gbsafe(5).
The choice of output format is described in Section D.3.7 on the preceding page. The goalis the formula to be verified, preceded by the name (without extension) of the output file for the SAT problem.
In this example, we have defined a macrogbsafethat would make it easy to check the validity of additional formulas by adding goals with different values forn.
D.4.3 Writing Lines of Input
The input file consists of a number of lines. Each line must start with a ’:-’
token and end with a ’.’ (dot) token. The following example shows a line containing start and end tokens and some line content.
:- some line content.
The input format allows line breaks, spaces and tabs within a line and the following input is thus semantically equivalent to the previous example.
:- some line content.
D.4.4 Declaration of States
All states that will be referred to in the state assertions of the duration formulas must be declared before they are referenced.
As an example, we use thestatekeyword to declare the stateflame:
:- state flame.
D.4.5 Declaration of Goals
A goal represents a DC formula to be verified. The first word after the goal keyword is the name (without extension) of the file to which the SAT problem will be written. Multiple goals are allowed in the same file. One SAT problem will be generated for each goal, and written to separate files as specified.
Example:
APPENDIX D. USER’S GUIDE :- goal firstGoal dur flame >= 2.
This input file makes the BMC/DCValidator check validity of the DC for-mulaR
flame ≥2. The SAT problem corresponding to ¬R
flame ≥2 is written to file firstGoal.zolcs(given that the selected output format is ZOLCS, see Section D.3.7 on page 110).
D.4.6 Translation Settings
In order to change the behaviour of the translation algorithm, one case use a number of settings. Setting values may be of type boolean, keyword, quoted string, and integer. See Appendix E on page 115 for further details on possible settings and types.
The following example shows a line that disables polarity optimisation:
:- set polarityOpt = false.
:- goal goalWithoutPolOpt dur x /\ y /\ z >= 2.
When a setting has been set, its value is preserved throughout the following lines until it is set again. In the above case, polarity optimisation is enabled in the translation process of goalgoalWithPolOptand any goal that may follow.
If, instead, one wants to perform a translation process both with and without polarity optimisation on a formula, one could write the following input lines to the BMC/DCValidator:
:- set polarityOpt = true.
:- goal goalWithPolOpt dur x /\ y /\ z >= 2.
:- set polarityOpt = false.
:- goal goalWithoutPolOpt dur x /\ y /\ z >= 2.
Actually, one can even leave out the first line since polarity optimisation is enabled by default. Find more information about settings and their default values in Section D.3 on page 108.
Example: Setting the Model Length Bound
In most cases, one wants to specify a bound on the number of steps used in the translation process. Thekvalue is a setting just like any other setting and can therefore be set one or more times as needed.
Example:
:- set k = 3.
:- goal goal3 dur x /\ y /\ z >= 2.
:- set k = 5.
:- goal goal5 dur x /\ y /\ z >= 2.
D.4.7 Shell Commands
Between the validation of goals, you may wish to have a shell command executed, e.g. to update yourPATHsystem variable to point to the SAT solver. This can be achieved using the shellkeyword, as illustrated in the following example:
:- shell("export PATH=$PATH:~/hysat/hysat-1.7/bin").
APPENDIX D. USER’S GUIDE
D.4.8 Taking Advantage of Pre-Processing
The pre-processing macro expansion makes it possible to avoid repeated use of the same text in an input file.
Simple Macros
The pre-processor works in such a way that it looks for definitions (characterised by ’=^=’) and for references to those definitions in the input file. Each time a definition is referenced in a piece of text, that reference is substituted with the original definition. Redefinition is not allowed, and neither are recursive definitions.
The main idea is shown in the following example that could have been part of an input file for the BMC/DCValidator:
:- a =^= x /\ y
:- goal goalWithPolOpt dur a /\ z >= 2.
:- set polarityOpt = false.
:- goal goalWithoutPolOpt dur a /\ u >= 2.
The point is that the macro pre-processing substitutes all occurences of awith x/\y and leaves out the definition of a.
:- goal goalWithPolOpt dur x /\ y /\ z >= 2.
:- set polarityOpt = false.
:- goal goalWithoutPolOpt dur x /\ y /\ u >= 2.
Parameterised Macros
It is also possible to create parameterised references with zero or more parame-ters. Again, one needs to be aware that redefining or overloading of a reference is not allowed.
:- a(n) =^= dur x /\ y /\ z >= n.
:- b() =^= a(1).
:- goal goalWithPolOpt2 a(2).
:- goal goalWithPolOpt4 a(4).
:- set polarityOpt = false.
:- goal goalWithoutOptPol2 a(2).
:- goal goalWithoutOptPol4 a(4).
:- goal goalWithoutOptPol1 b().
:- goal goalWithoutOptPol1Again b.
After pre-processing, the input looks like this:
:- goal goalWithPolOpt2 dur x /\ y /\ z >= 2.
:- goal goalWithPolOpt4 dur x /\ y /\ z >= 4.
:- set polarityOpt = false.
:- goal goalWithoutOptPol2 dur x /\ y /\ z >= 2.
:- goal goalWithoutOptPol4 dur x /\ y /\ z >= 4.
:- goal goalWithoutOptPol1 dur x /\ y /\ z >= 1.
:- goal goalWithoutOptPol1Again dur x /\ y /\ z >= 1.
APPENDIX D. USER’S GUIDE