PRC 2.0
Based on linear programming we develop the techniques towards an efficient
path-oriented tool for the bounded reachability analysis of linear hybrid
automata. We call this tool PRC stands for Path-Oriented Reachability
Checker.
This edition of PRC 2.0 is based on its older edition with the expanding on the ability of processing compositional reachablity analysis of a group linear hybrid automatas.

This edition of PRC is composed of three main part.
1.Graph_HA: It is the component for graphical representation of the automata, and it can generate the textual edition of the object hybrid system automaticallly, with some pre syntax checking.
 2.HA_Check: The component of Checking part which can only process one automata. Graph_HA+HA_Check=Edition 1.
3.HAN_Check: The new part of this eidition. It can make a bounded compositional reachability analysis of a group of Linear Hybrid System.
(Hint: While you only input one HA file, the process procedure is just the same with the component 2: HA_Check)

File Download
You can download our production from the hyperlink below, and just double click this jar file to run our program.
link: PRC
 
User manual
This manual is a detailed description of this tool.Especially in how
do this tool's two main component work and we have listed several points
that should pay attention to in every topic
link:UserManual.pdf


Sample Cases
TRAIN_GATE CONTROLLER
Fischer Protocol


Hint
At the first time you use PRC you can find some samples in the folder
"sample_ha" while the file with postfix "ser" can
be open by the Graph_HA and the file with postfix "ha" can
be check by the Checker. And the two files with the same prefix means
the same hybrid automata. We strongly recommend that when you use PRC
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.
If still have any question about the usage of our tool, please refer to the Edition 1 of PRC.

End
Thank you vey much for trying our production!
If you have any question or find some errors please contact us.
We are glad to see your reply:)
Email:lxd@nju.edu.cn or bl@seg.nju.edu.cn
|