PRC PRC Intro 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. It has two component, one is the Graph_HA editor and the second is the Checker. File Download You can download our production from the hyperlink below 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 How To Start After download PRC, please unzip this ".rar" file; Edit your Environment variable add ".;" in the very begining of ClassPath Click "Start" button in the windows and run cmd; Enter the folder you've just unzip the file to, for example: E:/PRC/ModelChecking Edition_2 then type the command java modelchecking.ModelChecking to execute this tool.   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.     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