BACH: Bounded reAchablity CHecker
Introduction Download Case Studies SnapShots BACH Team

Case Studies For BACH-DFS and BACH-SAT

Case Studies For BACH4.0

Case Studies For BACH_Online

Case Studies For BACH2.0

Sample Cases For BACH2.1

Sample Cases For PRC2


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).

1.To conduct the experiments on MathSAT, please add the option "-preprocessor.toplevel_propagation=false", which can decrease the memory usage and improve the performance.
2.Since BACH-SAT supports changing the LP solving algorithms, different option may affect the performance (the best option for temperature control system is Primal).

Water-Level Monitor System

Temperature Control System

Sample Automaton

Automated Highway System

Train Control System

New Sample Automaton

Case Studies For BACH4.0

We give four benchmarks for BACH4.0. You can download them and their corresponding input files for MathSAT.

automated highway system

sample case

temperature control system

water-level monitor

Case Studies For BACH_Online

composed liner hybrid automata instantiation

path_oriented reachability check of composed liner hybrid automatas

path_oriented reachability check of linear hybrid automata

bounded reachability check of linear hybrid automata

Case Studies For BACH2.0

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.


Sample Cases For BACH2.1

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)

Fischer Protocol

©2009 SEG CS NJU