PRC 2.0

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.

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