This download contains the source file and make file for a new version 
of timed automata model-checker RED based on REDLIB.  
This program supports the following verification tasks. 

1. for timed automata 

   a. safety/risk analysis, 
   b. TCTL model-checking, 
   c. simulation checking, and 
   d. bisimulation checking.  

2. for linear-hybrid automata 

   a. parametric risk analysis 

Note that we have not restored all the functionalities for address 
enforcers in the synchronizers. 

Ths file also serves to show how to use REDLIB.  
The contents are: 

1. READ.red.7.080504.txt
2. red.c
   The source file for the model-checker that calls REDLIB. 
3. vmake
   The make file for making the mode-checker. 
4. red
   The executable of red 7. 

You execute the model-checker with the following command in Linux. 

  % red [options] model-file-name spec-file-name 
     
You can check the source code in red.c to understand the options 
in executing the model-checker. 
The model-file-name is the name of the file for the input model file. 
The model file contains the process count specifications, 
the variable declarations, the transition rule declarations, and 
the initial condition declaration.  

The spec-file-name is the name of the file for the input specification. 
Depending on the verification task, 
the specification can be a safety predicate, a risk predicate, 
a TCTL formulus, or a role specification (for simulation/bisimulation 
checking).  
You may check how to write the various specifications with some of the 
benchmarks downloadable in the webpage. 

The options are as follows. 

-A    over-approximation of state space. 
-C    counter example generation for risk analysis
-Dn   Here 'n' is an integer constant in [0,255]. 
      This option tells the model-checker to stop reachability analysis 
      after n iterations. 
-F    For full reachability anslysis.  
      This option is in conflict with option '-D.'  
-Pn   Here 'n' is a non-negative integer constant for the process 
      count. 
      This option overrides the process count specified in the 
      input model file.  
-T    Option for task
      -Ts  safety checking 
      -Tr  risk checking (default)
      -Tg  goal checking 
      -Td  deadlock checking 
      -Tz  Zeno state checking 
      -Tm  TCTL model checking 
      -Tb  branching bisimulation checking 
      -Ti  branching simulation checking 
-Z    Option for quantification on non-Zeno runs only. 
      This option may affect the result of model-checking and 
      simulation/bisimulation checking. 
      Due to its cost, the default is to turn this option off. 
