How to Run the Verification Examples using the HyTech System
Run the command
hytech <filename>.hy
from the directory where the file <filename>.hy is stored.
More details on the HyTech system can be found on the HyTech page.
%-------------- Example ---------------------
[maurizio@proietti ~]$ cd HyTech/examples/
[maurizio@proietti examples]$ hytech Bakery2_HyTech.hy
Command: /usr/local/bin/hytech Bakery2_HyTech.hy
=================================================================
HyTech: symbolic model checker for embedded systems
Version 1.04f (last modified 1/24/02) from v1.04a of 12/6/96
For more info:
email: hytech@eecs.berkeley.edu
http://www.eecs.berkeley.edu/~tah/HyTech
Warning: Input has changed from version 1.00(a). Use -i for more info
=================================================================
Checking automaton p2
Checking automaton p1
Composing automata *
......Number of iterations required for reachability: 6
mutual exclusion holds!
Location: s_use.s_use
a >= 0 & b >= 0
Location: s_use.s_wait
b < a & b >= 0
|
a = 0 & b >= 0
|
b = 0 & a >= 0
Location: s_use.s_think
a = 0 & b >= 0
Location: s_wait.s_use
a < b & a >= 0
|
b = 0 & a >= 0
|
a = 0 & b >= 0
Location: s_wait.s_wait
a = 0 & 0 < b
|
b = 0 & 0 < a
|
a = 0 & b = 0
|
a = 0 & b >= 0
|
b = 0 & a >= 0
Location: s_wait.s_think
a = 0 & b >= 0
Location: s_think.s_use
b = 0 & a >= 0
Location: s_think.s_wait
b = 0 & 0 < a
|
a = 0 & b = 0
|
b = 0 & a >= 0
=================================================================
Max memory used = 0 pages = 0 bytes = 0.00 MB
Time spent = 0.02u + 0.00s = 0.02 sec total
=================================================================