6.3.1 Main
In Figure 6.2, we have illustrated the associations and dependencies between some of the key classes of the BMC/DCValidator. Prominently, the class bmc.Maingoverns the flow of control and instantiates a number of objects that are responsible for subtasks of the validation. The classes corresponding to those objects are:
bmc.parser.BMCPreprocessor Parses the input file and performs inlining of macro definitions.
bmc.parser.BMCParser Parses the result of the preprocessor and creates an internal representation of the formulas to be validated and the settings.
bmc.simp.DCSimplifier Performs simplification of DC formulas.
bmc.util.KValFinder Checks that the DC formula belongs to a class of for-mulas that have models of elementary length in the formula size, and determines that length.
bmc.trans.DCTranslator Translates the DC formula to an equisatisfiable SAT problem. The design of this class is described further in Section 6.3.3 on the next page.
bmc.constraint.ConstraintWriter Writes individual constraints to a file.
CHAPTER 6. DESIGN bmc.util.ShellExecutor Spawns a new process, e.g. for invoking the SAT
solver.
bmc.trace.HySatSolutionParser Parses the textual output from the SAT solver.
bmc.trace.StateTraceFrame Displays state traces when a counter example has been found, using a graphical user interface.
6.3.2 Formulas
The DC formulas and state assertions (or SA formulas, as we shall refer to them in the context of design and implementation) are represented by an abstract superclass Formula with appropriate subclasses Chop, Disjunction etc. as illustrated in the diagram in Figure 6.2 on the preceding page.
No distinction is made between the DC and SA formulas, since this enables us to reuse code in e.g. the DCSimplifierwhere the DC formulas and SA formulas have common simplification rules for disjunctions and conjunctions.
Where appropriate, type checking can be enforced by throwing exceptions when for example a duration formula is encountered where only SA formulas are expected. It is the responsibility of the BMCParserto ensure that the formulas to be validated specified by the user are in fact proper DC formulas.
AFormulaobject can save a reference to an ROBDD representing itself. It uses the ROBDDUtilclass for constructing such anROBDDobject.
6.3.3 DC → SAT Translation
TheDCTranslatoris an abstract class whose subclasses areDCToDIMACSTranslator andDCToZOLCSTranslator. It is the values of theSettingsobject that is car-ried around with the formula to be validated (based on the user’s specification in the input file), that determines which of the two is chosen. They implement the algorithms described in Appendix C on page 101 and produce constraints that are handed to theConstraintWriter.
TheLiteralHandlergenerates the literals needed to represent each subfor-mula in different time instants, as described in Section 3.2 on page 16.
It is also responsible for controlling when regeneration of constraints may be avoided in the case of subformula recurrence. Directly corresponding to the three levels of formula recurrence recognition (with different time and space complexities) that were described in Section 3.7, we have three different sub-classes of theLiteralHandler:
• IDLookupLiteralHandler
• SyntacticLookupLiteralHandler
• SemanticLookupLiteralHandler
As with the output format, it is the user’s specification that determines which is selected.
CHAPTER 6. DESIGN
Figure 6.3: Class Diagram for DC→SAT Translation
Chapter 7
Implementation
This chapter shall describe the implementation of the individual classes of the BMC/DCValidator. The segregation of duties among the classes was done in Chapter 6 on Design.
We have chosen not to tire the reader with samples of the source code, but shall merely mention that the entire source code of the program may be found in Appendix I on page 275. The implementation has been written using the Java language.
7.1 Package bmc
7.1.1 Class Main
TheMainclass has a class-scope methodmain(String[] args)that enables it to act as a standalone Java application where the argsare the command line arguments.
As mandatory arguments, one must specify an input file containing an ASCII representation of the formula(s) to be validated and various settings, and a command specifying where the SAT solver may be found. Optionally, one may specify a command for executing shell(...) commands in the input file in between the validations, e.g. for moving or renaming files. Also, one may specify whether counter example traces should be displayed or not. For more details on how to run the program, please refer to the User’s Guide in Appendix D on page 107.
If there was an error in one of the command line arguments, the program usage is printed on screen. Otherwise, an instance ofMainis created after some initial setup and therun(...) method is invoked on that instance.
Therun(...)method will parse the input file using first theBMCPreprocessor and then theBMCParserwith the scannerBMCLex. See Section 7.6 on page 68 for details.
In our terminology, the input file consists of various tasks. Each task is either
• aGoal, consisting of a Formula to be validated, the set of States that may occur in the formula and someSettingsor,
• aCommandto be executed
CHAPTER 7. IMPLEMENTATION For Commands, we simply invoke the ShellExecutorof Section 7.10.5 on page 75.
For Goals, we must take a number of steps to determine validity of the formula:
1. A clock is started so we can time the work done by the frontend.
2. The formula is negated, since we are checking whether ¬φ is satisfiable when validatingφ.
3. If specified in the Settings, the formula is rewritten to NNF.
4. A DCSimplifieris instantiated.
5. The DC formula is simplified by the DCSimplifier, see Section 7.7.1 on page 70.
6. If specified in the Settings, the k value is calculated from the formula using theKValFinderas described in Section 7.10.3 on page 74.
7. Ajava.io.RandomAccessFileis instantiated where the SAT solver input file can be written.
8. Based on the Settings, aLiteralHandleris chosen and instantiated.
9. A ConstraintWriteris instantiated.
10. Based on theSettings, aDCTranslatoris chosen and instantiated.
11. The DCTranslator(or, to be exact, an instance of one of its subclasses) translates the DC formula to a SAT problem. See Section 7.9 on page 72 for details.
12. The clock value is saved (giving the frontend time).
13. The SAT solver is executed using theShellExecutor.
14. AHySatSolutionParseris instantiated and parses the output of the SAT solver as described in Section 7.8.1 on page 71.
15. The validity of the formula is printed on the screen, along with frontend and backend times, the latter being retrieved from the SAT solver’s output by theHySatSolutionParser.
16. Depending on the command line parameters given, the state traces may be displayed using aStateTraceFrame(see Section 7.8.4 on page 72) if the formula turned out to be invalid.