================================================================= HyTech: symbolic model checker for embedded systems Version 1.04 10/15/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 ================================================================= Number of iterations required for reachability: 68 ====== Generating trace to specified target region ======== Time: 0.00 Location: c1.start.start x1 + 30 = 0 & y1 + 30 = 0 & x2 = 0 & y2 = 0 & x3 = 0 & y3 = 0 & timer2 = 0 & timer3 = 0 --------------- VIA 1.00 time units --------------- Time: 1.00 Location: c1.start.start x1 + 30 = 0 & y1 + 20 = 0 & x2 = 0 & y2 = 0 & x3 = 0 & y3 = 0 & timer2 = 1 & timer3 = 1 ------------------------------- VIA: ------------------------------- Time: 1.00 Location: c1.c11.start x1 + 30 = 0 & y1 + 20 = 0 & x2 + 30 = 0 & y2 + 30 = 0 & x3 = 0 & y3 = 0 & timer2 = 1 & timer3 = 1 --------------- VIA 0.50 time units --------------- Time: 1.50 Location: c1.c11.start x1 + 30 = 0 & y1 + 15 = 0 & x2 + 30 = 0 & y2 + 20 = 0 & x3 = 0 & y3 = 0 & timer2 = 1 & 2timer3 = 3 ------------------------------- VIA: ------------------------------- Time: 1.50 Location: c1.p1.start x1 + 30 = 0 & y1 + 15 = 0 & x2 + 35 = 0 & y2 + 20 = 0 & x3 = 0 & y3 = 0 & timer2 = 1 & 2timer3 = 3 --------------- VIA 0.50 time units --------------- Time: 2.00 Location: c1.p1.start x1 + 30 = 0 & y1 + 10 = 0 & x2 + 35 = 0 & y2 + 10 = 0 & x3 = 0 & y3 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 2.00 Location: c1.p1.c11 x1 + 30 = 0 & y1 + 10 = 0 & x2 + 35 = 0 & y2 + 10 = 0 & x3 + 30 = 0 & y3 + 30 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 0.50 time units --------------- Time: 2.50 Location: c1.p1.c11 x1 + 30 = 0 & y1 + 5 = 0 & x2 + 35 = 0 & y2 = 0 & x3 + 30 = 0 & 2y3 + 35 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 2.50 Location: c1.c1n.c11 x1 + 30 = 0 & y1 + 5 = 0 & x2 + 30 = 0 & y2 = 0 & x3 + 30 = 0 & 2y3 + 35 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 0.50 time units --------------- Time: 3.00 Location: c1.c1n.c11 x1 + 30 = 0 & y1 = 0 & x2 + 30 = 0 & y2 = 10 & x3 + 30 = 0 & y3 + 5 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 3.00 Location: c1.c1n.p11 x1 + 30 = 0 & y1 = 0 & x2 + 30 = 0 & y2 = 10 & x3 + 35 = 0 & y3 + 5 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 0.67 time units --------------- Time: 3.67 Location: c1.c1n.p11 x1 + 30 = 0 & 3y1 = 20 & x2 + 30 = 0 & 3y2 = 70 & x3 + 35 = 0 & 3y3 = 35 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 3.67 Location: c1.c1n.c12 x1 + 30 = 0 & 3y1 = 20 & x2 + 30 = 0 & 3y2 = 70 & x3 + 30 = 0 & 3y3 = 35 & timer2 = 1 & timer3 = 2 --------------- VIA 0.33 time units --------------- Time: 4.00 Location: c1.c1n.c12 x1 + 30 = 0 & y1 = 10 & x2 + 30 = 0 & y2 = 30 & x3 + 30 = 0 & y3 = 20 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 4.00 Location: c1.c2n.c12 x1 + 30 = 0 & y1 = 10 & x2 + 30 = 0 & y2 = 30 & x3 + 30 = 0 & y3 = 20 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 4.20 Location: c1.c2n.c12 x1 + 30 = 0 & y1 = 12 & x2 + 26 = 0 & y2 = 30 & x3 + 30 = 0 & y3 = 25 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 4.20 Location: c1.c2n.p12 x1 + 30 = 0 & y1 = 12 & x2 + 26 = 0 & y2 = 30 & x3 + 35 = 0 & y3 = 25 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 4.40 Location: c1.c2n.p12 x1 + 30 = 0 & y1 = 14 & x2 + 22 = 0 & y2 = 30 & x3 + 35 = 0 & y3 = 30 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 4.40 Location: c1.c2n.p12i x1 + 30 = 0 & y1 = 14 & x2 + 22 = 0 & y2 = 30 & x3 + 35 = 0 & y3 = 30 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 4.60 Location: c1.c2n.p12i x1 + 30 = 0 & y1 = 16 & x2 + 18 = 0 & y2 = 30 & x3 + 35 = 0 & y3 = 35 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 4.60 Location: c1.c2n.p22 x1 + 30 = 0 & y1 = 16 & x2 + 18 = 0 & y2 = 30 & x3 + 35 = 0 & y3 = 35 & timer2 = 1 & timer3 = 2 --------------- VIA 1.40 time units --------------- Time: 5.1e+02 Location: c1.c2n.p22 x1 + 30 = 0 & y1 = 30 & x2 = 10 & y2 = 30 & x3 = 0 & y3 = 35 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 5.1e+02 Location: c2.c2n.p22 x1 + 30 = 0 & y1 = 30 & x2 = 10 & y2 = 30 & x3 = 0 & y3 = 35 & timer2 = 1 & timer3 = 2 --------------- VIA 1.00 time units --------------- Time: 6.1e+02 Location: c2.c2n.p22 x1 + 20 = 0 & y1 = 30 & x2 = 30 & y2 = 30 & x3 = 25 & y3 = 35 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 6.1e+02 Location: c2.c3n.p22 x1 + 20 = 0 & y1 = 30 & x2 = 30 & y2 = 30 & x3 = 25 & y3 = 35 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 7.20 Location: c2.c3n.p22 x1 + 18 = 0 & y1 = 30 & x2 = 30 & y2 = 26 & x3 = 30 & y3 = 35 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 7.20 Location: c2.c3n.p22i x1 + 18 = 0 & y1 = 30 & x2 = 30 & y2 = 26 & x3 = 30 & y3 = 35 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 7.40 Location: c2.c3n.p22i x1 + 16 = 0 & y1 = 30 & x2 = 30 & y2 = 22 & x3 = 35 & y3 = 35 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 7.40 Location: c2.c3n.p32 x1 + 16 = 0 & y1 = 30 & x2 = 30 & y2 = 22 & x3 = 35 & y3 = 35 & timer2 = 1 & timer3 = 2 --------------- VIA 2.60 time units --------------- Time: 9.1e+02 Location: c2.c3n.p32 x1 = 10 & y1 = 30 & x2 = 30 & y2 + 30 = 0 & x3 = 35 & y3 + 30 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 9.1e+02 Location: c2.c3n.p32i x1 = 10 & y1 = 30 & x2 = 30 & y2 + 30 = 0 & x3 = 35 & y3 + 30 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 9.1e+02 Location: c2.c4n.p32i x1 = 10 & y1 = 30 & x2 = 30 & y2 + 30 = 0 & x3 = 35 & y3 + 30 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 10.20 Location: c2.c4n.p32i x1 = 12 & y1 = 30 & x2 = 26 & y2 + 30 = 0 & x3 = 35 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 10.20 Location: c2.c4n.p42 x1 = 12 & y1 = 30 & x2 = 26 & y2 + 30 = 0 & x3 = 35 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 1.80 time units --------------- Time: 11.1e+02 Location: c2.c4n.p42 x1 = 30 & y1 = 30 & x2 + 10 = 0 & y2 + 30 = 0 & x3 + 10 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 11.1e+02 Location: c3.c4n.p42 x1 = 30 & y1 = 30 & x2 + 10 = 0 & y2 + 30 = 0 & x3 + 10 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 0.80 time units --------------- Time: 12.80 Location: c3.c4n.p42 x1 = 30 & y1 = 22 & x2 + 26 = 0 & y2 + 30 = 0 & x3 + 30 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 12.80 Location: c3.c4n.p42i x1 = 30 & y1 = 22 & x2 + 26 = 0 & y2 + 30 = 0 & x3 + 30 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 0.20 time units --------------- Time: 12.1e+02 Location: c3.c4n.p42i x1 = 30 & y1 = 20 & x2 + 30 = 0 & y2 + 30 = 0 & x3 + 35 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 12.1e+02 Location: c3.c1n.p42i x1 = 30 & y1 = 20 & x2 + 30 = 0 & y2 + 30 = 0 & x3 + 35 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 12.1e+02 Location: c3.c1n.p12 x1 = 30 & y1 = 20 & x2 + 30 = 0 & y2 + 30 = 0 & x3 + 35 = 0 & y3 + 35 = 0 & timer2 = 1 & timer3 = 2 --------------- VIA 2.00 time units --------------- Time: 14.1e+02 Location: c3.c1n.p12 x1 = 30 & y1 = 0 & x2 + 30 = 0 & y2 = 10 & x3 + 35 = 0 & y3 = 15 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 14.1e+02 Location: c3.c1n.c1n x1 = 30 & y1 = 0 & x2 + 30 = 0 & y2 = 10 & x3 + 30 = 0 & y3 = 15 & timer2 = 1 & timer3 = 2 --------------- VIA 0.60 time units --------------- Time: 15.60 Location: c3.c1n.c1n x1 = 30 & y1 + 6 = 0 & x2 + 30 = 0 & y2 = 22 & x3 + 30 = 0 & y3 = 30 & timer2 = 1 & timer3 = 2 ------------------------------- VIA: ------------------------------- Time: 15.60 Location: c3.c1n.c2n x1 = 30 & y1 + 6 = 0 & x2 + 30 = 0 & y2 = 22 & x3 + 30 = 0 & y3 = 30 & timer2 = 1 & timer3 = 2 --------------- VIA 0.18 time units --------------- Time: 15.78 Location: c3.c1n.c2n x1 = 30 & 9y1 + 70 = 0 & x2 + 30 = 0 & 9y2 = 230 & 9x3 + 230 = 0 & y3 = 30 & timer2 = 1 & timer3 = 2 ============ End of trace generation ============ ================================================================= Max memory used = 0 pages = 0 bytes = 0.00 MB Time spent = 139.81u + 2.43s = 142.24 sec total =================================================================