|
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).
Tips:
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)
TrainGateController
Fischer
Protocol
|