- NAME
- kronos - symbolic verification of real-time systems
- SYNOPSIS
- kronos options f1 [.tg] [ f2 [.tctl] ]
- DESCRIPTION
- kronos checks whether a timed automaton satisfies a TCTL-formula.
- OPTIONS
- -c
- kronos creates the file f1.cpt obtained from the input
file f1.tg by computing the canonical forms of all constraints on clocks.
- -f formula
- kronos creates the file aux.tctl containing formula
and takes it as the formula.
- -g
- kronos generates the symbolic reachability graph starting at the
initial state. By default, the size of the graph is limited to sim-size.
The output is written in the file f1.sim.
- -G size
- Instead of -g. Changes sim-size to size.
- -h
- Makes kronos to write the evaluation of every subformula to a file
.log. By default, kronos only creates the output file .eval
with the result of the overall evaluation. Only for backward reachability.
- -r
- kronos evaluates the formula using forward reachability.
The algorithm generates upto sim-size reachable symbolic states.
By default, backward reachability is used.
- -R size
- Instead of -r. Changes sim-size to size.
- -v
- Sets to verbose. This option causes information about the progress of the
evaluation to be reported to the standard output. By default, kronos runs
quietly.
- -s step
- Sets the time step used to evaluate unbounded au formulas to step.
Only for backward reachabilty. By default, kronos uses 1.
- INPUT FILES
- A timed automaton (.tg file)
- A TCTL-formula (.tctl file)
- DIAGNOSTIC FILES
- Characteristic set of the formula (.eval file)
- Characteristic set of every subformula (.log file) [option -h]
- Reachability graph (.sim file) [options -g and -G]
- Counter-example (path.reach and trace.reach files)
[options -r and -R]
- OUTPUT FILES
- kronos generates the following files for internal use:
.kro, .prop, .reg, .lab, .reg.
- RELATED COMMANDS
- ptg
- SEE ALSO
-
KRONOS home page.
- BUGS, QUESTIONS and COMMENTS
- Please contact Sergio Yovine.
-
Last modified: Aug 29, 1996.