BACH: Bounded reAchablity CHecker | ||||||
|
Case Studies For BACH-DFS and BACH-SAT
Case Studies For BACH-DFS and BACH-SAT We give six benchmarks for BACH-DFS and BACH-SAT. You can download them and their corresponding SMT2.0 input files (The 'ha' file is for BACH while the 'smt2' files are for the SMT solvers). Tips:
We give four benchmarks for BACH4.0. You can download them and their corresponding input files for MathSAT. automated highway system composed liner hybrid automata instantiationpath_oriented reachability check of composed liner hybrid automatas path_oriented reachability check of linear hybrid automata bounded reachability check of linear hybrid automata We briefly describe the performance of BACH 2.0 with two well-known examples: the fischer protocol and the nuclear reactor system.The Fischer Protocol system consists of several competing processes which all attempt to enter the critical section. The automaton we use to model a single process is shown as follows. As this is a classical shared variable problem, in order to handle it in BACH's context (synchronize with share labels), we build a LHA: Shared Variable (denoted as SV) to represent all the evaluation and reset actions on the shared variable. The Nuclear Reactor System controls a nuclear reactor with n rods whose model is shown in Fig.4. The system use these rods to absorb neutrons one by one. Each rod that has just been moved out of the heavy water must stay out of the heavy water and cool for several time units.
The size of these two examples can easily scale up by increasing the number of processes (rods) in the system, thus they are particularly appropriate to show the ability of BACH 2.0. You can click here to download the samples, while the file with postfix "ser" can be open by the Creat_HA and the file with postfix "ha" can be check by the Checker. We strongly recommend that when you use BACH2 to make your own HA files please name the ser file and ha file with same prefix. This will help you a lot when you want to manage your own hybrid automata. As we had compared the performance of our tool with several SMT solvers, MathSAT, Yices, CVC, Barcelogic, and a SAT-based solver for HA HySAT, we put our encoding of the same models for these solvers online as well: Input file for MathSAT, Input file for other SMT solver, Input file for HySAT Furthermore, as we also compared the performance of our path-oriented part with HySAT, the files we encoded for HySAT are available too.
Since we have made some changes of the format of HA files, there are some difference in the samples of BACH2.1.
Sample Cases(For PRC2)TrainGateController Fischer Protocol
|
©2009 SEG CS NJU |