source: caseStudy_Huffmann/huffmann/huff_synchro/cex @ 105

Last change on this file since 105 was 105, checked in by cecile, 12 years ago

Hufmann case study

File size: 31.4 KB
RevLine 
[105]1# MC: formula failed --- AG((((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))))
2# MC: Calling debugger for trace 1
3--State
4ch<0>:0
5ch<1>:0
6ch<2>:0
7ch<3>:0
8ch<4>:0
9ch<5>:0
10ch<6>:0
11ch<7>:0
12character<0>:0
13character<1>:0
14character<2>:0
15character<3>:0
16character<4>:0
17character<5>:0
18character<6>:0
19character<7>:0
20ci:0
21decoder.state<0>:0
22decoder.state<1>:0
23decoder.state<2>:0
24decoder.state<3>:0
25decoder.state<4>:0
26decoder.state<5>:0
27decoder.state<6>:0
28decoder.state<7>:0
29decoder.state<8>:0
30decoder.state<9>:0
31encoder.shiftreg<0>:0
32encoder.shiftreg<1>:0
33encoder.shiftreg<2>:0
34encoder.shiftreg<3>:0
35encoder.shiftreg<4>:0
36encoder.shiftreg<5>:0
37encoder.shiftreg<6>:0
38encoder.shiftreg<7>:0
39encoder.shiftreg<8>:0
40encoder.shiftreg<9>:0
41start:0
42fails AG((((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))))
43
44since (((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))) is false at this state
45--State
46ch<0>:0
47ch<1>:0
48ch<2>:0
49ch<3>:0
50ch<4>:0
51ch<5>:0
52ch<6>:0
53ch<7>:0
54character<0>:0
55character<1>:0
56character<2>:0
57character<3>:0
58character<4>:0
59character<5>:0
60character<6>:0
61character<7>:0
62ci:0
63decoder.state<0>:0
64decoder.state<1>:0
65decoder.state<2>:0
66decoder.state<3>:0
67decoder.state<4>:0
68decoder.state<5>:0
69decoder.state<6>:0
70decoder.state<7>:0
71decoder.state<8>:0
72decoder.state<9>:0
73encoder.shiftreg<0>:0
74encoder.shiftreg<1>:0
75encoder.shiftreg<2>:0
76encoder.shiftreg<3>:0
77encoder.shiftreg<4>:0
78encoder.shiftreg<5>:0
79encoder.shiftreg<6>:0
80encoder.shiftreg<7>:0
81encoder.shiftreg<8>:0
82encoder.shiftreg<9>:0
83start:0
84fails (((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1) -> AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))).
85
86--State
87ch<0>:0
88ch<1>:0
89ch<2>:0
90ch<3>:0
91ch<4>:0
92ch<5>:0
93ch<6>:0
94ch<7>:0
95character<0>:0
96character<1>:0
97character<2>:0
98character<3>:0
99character<4>:0
100character<5>:0
101character<6>:0
102character<7>:0
103ci:0
104decoder.state<0>:0
105decoder.state<1>:0
106decoder.state<2>:0
107decoder.state<3>:0
108decoder.state<4>:0
109decoder.state<5>:0
110decoder.state<6>:0
111decoder.state<7>:0
112decoder.state<8>:0
113decoder.state<9>:0
114encoder.shiftreg<0>:0
115encoder.shiftreg<1>:0
116encoder.shiftreg<2>:0
117encoder.shiftreg<3>:0
118encoder.shiftreg<4>:0
119encoder.shiftreg<5>:0
120encoder.shiftreg<6>:0
121encoder.shiftreg<7>:0
122encoder.shiftreg<8>:0
123encoder.shiftreg<9>:0
124start:0
125passes ((((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0) + decoder.leaf=1).
126
127--State
128ch<0>:0
129ch<1>:0
130ch<2>:0
131ch<3>:0
132ch<4>:0
133ch<5>:0
134ch<6>:0
135ch<7>:0
136character<0>:0
137character<1>:0
138character<2>:0
139character<3>:0
140character<4>:0
141character<5>:0
142character<6>:0
143character<7>:0
144ci:0
145decoder.state<0>:0
146decoder.state<1>:0
147decoder.state<2>:0
148decoder.state<3>:0
149decoder.state<4>:0
150decoder.state<5>:0
151decoder.state<6>:0
152decoder.state<7>:0
153decoder.state<8>:0
154decoder.state<9>:0
155encoder.shiftreg<0>:0
156encoder.shiftreg<1>:0
157encoder.shiftreg<2>:0
158encoder.shiftreg<3>:0
159encoder.shiftreg<4>:0
160encoder.shiftreg<5>:0
161encoder.shiftreg<6>:0
162encoder.shiftreg<7>:0
163encoder.shiftreg<8>:0
164encoder.shiftreg<9>:0
165start:0
166passes (((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0) * decoder.state<0>=0).
167
168--State
169ch<0>:0
170ch<1>:0
171ch<2>:0
172ch<3>:0
173ch<4>:0
174ch<5>:0
175ch<6>:0
176ch<7>:0
177character<0>:0
178character<1>:0
179character<2>:0
180character<3>:0
181character<4>:0
182character<5>:0
183character<6>:0
184character<7>:0
185ci:0
186decoder.state<0>:0
187decoder.state<1>:0
188decoder.state<2>:0
189decoder.state<3>:0
190decoder.state<4>:0
191decoder.state<5>:0
192decoder.state<6>:0
193decoder.state<7>:0
194decoder.state<8>:0
195decoder.state<9>:0
196encoder.shiftreg<0>:0
197encoder.shiftreg<1>:0
198encoder.shiftreg<2>:0
199encoder.shiftreg<3>:0
200encoder.shiftreg<4>:0
201encoder.shiftreg<5>:0
202encoder.shiftreg<6>:0
203encoder.shiftreg<7>:0
204encoder.shiftreg<8>:0
205encoder.shiftreg<9>:0
206start:0
207passes ((((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0) * decoder.state<1>=0).
208
209--State
210ch<0>:0
211ch<1>:0
212ch<2>:0
213ch<3>:0
214ch<4>:0
215ch<5>:0
216ch<6>:0
217ch<7>:0
218character<0>:0
219character<1>:0
220character<2>:0
221character<3>:0
222character<4>:0
223character<5>:0
224character<6>:0
225character<7>:0
226ci:0
227decoder.state<0>:0
228decoder.state<1>:0
229decoder.state<2>:0
230decoder.state<3>:0
231decoder.state<4>:0
232decoder.state<5>:0
233decoder.state<6>:0
234decoder.state<7>:0
235decoder.state<8>:0
236decoder.state<9>:0
237encoder.shiftreg<0>:0
238encoder.shiftreg<1>:0
239encoder.shiftreg<2>:0
240encoder.shiftreg<3>:0
241encoder.shiftreg<4>:0
242encoder.shiftreg<5>:0
243encoder.shiftreg<6>:0
244encoder.shiftreg<7>:0
245encoder.shiftreg<8>:0
246encoder.shiftreg<9>:0
247start:0
248passes (((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0) * decoder.state<2>=0).
249
250--State
251ch<0>:0
252ch<1>:0
253ch<2>:0
254ch<3>:0
255ch<4>:0
256ch<5>:0
257ch<6>:0
258ch<7>:0
259character<0>:0
260character<1>:0
261character<2>:0
262character<3>:0
263character<4>:0
264character<5>:0
265character<6>:0
266character<7>:0
267ci:0
268decoder.state<0>:0
269decoder.state<1>:0
270decoder.state<2>:0
271decoder.state<3>:0
272decoder.state<4>:0
273decoder.state<5>:0
274decoder.state<6>:0
275decoder.state<7>:0
276decoder.state<8>:0
277decoder.state<9>:0
278encoder.shiftreg<0>:0
279encoder.shiftreg<1>:0
280encoder.shiftreg<2>:0
281encoder.shiftreg<3>:0
282encoder.shiftreg<4>:0
283encoder.shiftreg<5>:0
284encoder.shiftreg<6>:0
285encoder.shiftreg<7>:0
286encoder.shiftreg<8>:0
287encoder.shiftreg<9>:0
288start:0
289passes ((((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0) * decoder.state<3>=0).
290
291--State
292ch<0>:0
293ch<1>:0
294ch<2>:0
295ch<3>:0
296ch<4>:0
297ch<5>:0
298ch<6>:0
299ch<7>:0
300character<0>:0
301character<1>:0
302character<2>:0
303character<3>:0
304character<4>:0
305character<5>:0
306character<6>:0
307character<7>:0
308ci:0
309decoder.state<0>:0
310decoder.state<1>:0
311decoder.state<2>:0
312decoder.state<3>:0
313decoder.state<4>:0
314decoder.state<5>:0
315decoder.state<6>:0
316decoder.state<7>:0
317decoder.state<8>:0
318decoder.state<9>:0
319encoder.shiftreg<0>:0
320encoder.shiftreg<1>:0
321encoder.shiftreg<2>:0
322encoder.shiftreg<3>:0
323encoder.shiftreg<4>:0
324encoder.shiftreg<5>:0
325encoder.shiftreg<6>:0
326encoder.shiftreg<7>:0
327encoder.shiftreg<8>:0
328encoder.shiftreg<9>:0
329start:0
330passes (((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0) * decoder.state<4>=0).
331
332--State
333ch<0>:0
334ch<1>:0
335ch<2>:0
336ch<3>:0
337ch<4>:0
338ch<5>:0
339ch<6>:0
340ch<7>:0
341character<0>:0
342character<1>:0
343character<2>:0
344character<3>:0
345character<4>:0
346character<5>:0
347character<6>:0
348character<7>:0
349ci:0
350decoder.state<0>:0
351decoder.state<1>:0
352decoder.state<2>:0
353decoder.state<3>:0
354decoder.state<4>:0
355decoder.state<5>:0
356decoder.state<6>:0
357decoder.state<7>:0
358decoder.state<8>:0
359decoder.state<9>:0
360encoder.shiftreg<0>:0
361encoder.shiftreg<1>:0
362encoder.shiftreg<2>:0
363encoder.shiftreg<3>:0
364encoder.shiftreg<4>:0
365encoder.shiftreg<5>:0
366encoder.shiftreg<6>:0
367encoder.shiftreg<7>:0
368encoder.shiftreg<8>:0
369encoder.shiftreg<9>:0
370start:0
371passes ((((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0) * decoder.state<5>=0).
372
373--State
374ch<0>:0
375ch<1>:0
376ch<2>:0
377ch<3>:0
378ch<4>:0
379ch<5>:0
380ch<6>:0
381ch<7>:0
382character<0>:0
383character<1>:0
384character<2>:0
385character<3>:0
386character<4>:0
387character<5>:0
388character<6>:0
389character<7>:0
390ci:0
391decoder.state<0>:0
392decoder.state<1>:0
393decoder.state<2>:0
394decoder.state<3>:0
395decoder.state<4>:0
396decoder.state<5>:0
397decoder.state<6>:0
398decoder.state<7>:0
399decoder.state<8>:0
400decoder.state<9>:0
401encoder.shiftreg<0>:0
402encoder.shiftreg<1>:0
403encoder.shiftreg<2>:0
404encoder.shiftreg<3>:0
405encoder.shiftreg<4>:0
406encoder.shiftreg<5>:0
407encoder.shiftreg<6>:0
408encoder.shiftreg<7>:0
409encoder.shiftreg<8>:0
410encoder.shiftreg<9>:0
411start:0
412passes (((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0) * decoder.state<6>=0).
413
414--State
415ch<0>:0
416ch<1>:0
417ch<2>:0
418ch<3>:0
419ch<4>:0
420ch<5>:0
421ch<6>:0
422ch<7>:0
423character<0>:0
424character<1>:0
425character<2>:0
426character<3>:0
427character<4>:0
428character<5>:0
429character<6>:0
430character<7>:0
431ci:0
432decoder.state<0>:0
433decoder.state<1>:0
434decoder.state<2>:0
435decoder.state<3>:0
436decoder.state<4>:0
437decoder.state<5>:0
438decoder.state<6>:0
439decoder.state<7>:0
440decoder.state<8>:0
441decoder.state<9>:0
442encoder.shiftreg<0>:0
443encoder.shiftreg<1>:0
444encoder.shiftreg<2>:0
445encoder.shiftreg<3>:0
446encoder.shiftreg<4>:0
447encoder.shiftreg<5>:0
448encoder.shiftreg<6>:0
449encoder.shiftreg<7>:0
450encoder.shiftreg<8>:0
451encoder.shiftreg<9>:0
452start:0
453passes ((decoder.state<9>=0 * decoder.state<8>=0) * decoder.state<7>=0).
454
455--State
456ch<0>:0
457ch<1>:0
458ch<2>:0
459ch<3>:0
460ch<4>:0
461ch<5>:0
462ch<6>:0
463ch<7>:0
464character<0>:0
465character<1>:0
466character<2>:0
467character<3>:0
468character<4>:0
469character<5>:0
470character<6>:0
471character<7>:0
472ci:0
473decoder.state<0>:0
474decoder.state<1>:0
475decoder.state<2>:0
476decoder.state<3>:0
477decoder.state<4>:0
478decoder.state<5>:0
479decoder.state<6>:0
480decoder.state<7>:0
481decoder.state<8>:0
482decoder.state<9>:0
483encoder.shiftreg<0>:0
484encoder.shiftreg<1>:0
485encoder.shiftreg<2>:0
486encoder.shiftreg<3>:0
487encoder.shiftreg<4>:0
488encoder.shiftreg<5>:0
489encoder.shiftreg<6>:0
490encoder.shiftreg<7>:0
491encoder.shiftreg<8>:0
492encoder.shiftreg<9>:0
493start:0
494passes (decoder.state<9>=0 * decoder.state<8>=0).
495
496--State
497ch<0>:0
498ch<1>:0
499ch<2>:0
500ch<3>:0
501ch<4>:0
502ch<5>:0
503ch<6>:0
504ch<7>:0
505character<0>:0
506character<1>:0
507character<2>:0
508character<3>:0
509character<4>:0
510character<5>:0
511character<6>:0
512character<7>:0
513ci:0
514decoder.state<0>:0
515decoder.state<1>:0
516decoder.state<2>:0
517decoder.state<3>:0
518decoder.state<4>:0
519decoder.state<5>:0
520decoder.state<6>:0
521decoder.state<7>:0
522decoder.state<8>:0
523decoder.state<9>:0
524encoder.shiftreg<0>:0
525encoder.shiftreg<1>:0
526encoder.shiftreg<2>:0
527encoder.shiftreg<3>:0
528encoder.shiftreg<4>:0
529encoder.shiftreg<5>:0
530encoder.shiftreg<6>:0
531encoder.shiftreg<7>:0
532encoder.shiftreg<8>:0
533encoder.shiftreg<9>:0
534start:0
535passes decoder.state<9>=0.
536
537--State
538ch<0>:0
539ch<1>:0
540ch<2>:0
541ch<3>:0
542ch<4>:0
543ch<5>:0
544ch<6>:0
545ch<7>:0
546character<0>:0
547character<1>:0
548character<2>:0
549character<3>:0
550character<4>:0
551character<5>:0
552character<6>:0
553character<7>:0
554ci:0
555decoder.state<0>:0
556decoder.state<1>:0
557decoder.state<2>:0
558decoder.state<3>:0
559decoder.state<4>:0
560decoder.state<5>:0
561decoder.state<6>:0
562decoder.state<7>:0
563decoder.state<8>:0
564decoder.state<9>:0
565encoder.shiftreg<0>:0
566encoder.shiftreg<1>:0
567encoder.shiftreg<2>:0
568encoder.shiftreg<3>:0
569encoder.shiftreg<4>:0
570encoder.shiftreg<5>:0
571encoder.shiftreg<6>:0
572encoder.shiftreg<7>:0
573encoder.shiftreg<8>:0
574encoder.shiftreg<9>:0
575start:0
576passes decoder.state<8>=0.
577
578--State
579ch<0>:0
580ch<1>:0
581ch<2>:0
582ch<3>:0
583ch<4>:0
584ch<5>:0
585ch<6>:0
586ch<7>:0
587character<0>:0
588character<1>:0
589character<2>:0
590character<3>:0
591character<4>:0
592character<5>:0
593character<6>:0
594character<7>:0
595ci:0
596decoder.state<0>:0
597decoder.state<1>:0
598decoder.state<2>:0
599decoder.state<3>:0
600decoder.state<4>:0
601decoder.state<5>:0
602decoder.state<6>:0
603decoder.state<7>:0
604decoder.state<8>:0
605decoder.state<9>:0
606encoder.shiftreg<0>:0
607encoder.shiftreg<1>:0
608encoder.shiftreg<2>:0
609encoder.shiftreg<3>:0
610encoder.shiftreg<4>:0
611encoder.shiftreg<5>:0
612encoder.shiftreg<6>:0
613encoder.shiftreg<7>:0
614encoder.shiftreg<8>:0
615encoder.shiftreg<9>:0
616start:0
617passes decoder.state<7>=0.
618
619--State
620ch<0>:0
621ch<1>:0
622ch<2>:0
623ch<3>:0
624ch<4>:0
625ch<5>:0
626ch<6>:0
627ch<7>:0
628character<0>:0
629character<1>:0
630character<2>:0
631character<3>:0
632character<4>:0
633character<5>:0
634character<6>:0
635character<7>:0
636ci:0
637decoder.state<0>:0
638decoder.state<1>:0
639decoder.state<2>:0
640decoder.state<3>:0
641decoder.state<4>:0
642decoder.state<5>:0
643decoder.state<6>:0
644decoder.state<7>:0
645decoder.state<8>:0
646decoder.state<9>:0
647encoder.shiftreg<0>:0
648encoder.shiftreg<1>:0
649encoder.shiftreg<2>:0
650encoder.shiftreg<3>:0
651encoder.shiftreg<4>:0
652encoder.shiftreg<5>:0
653encoder.shiftreg<6>:0
654encoder.shiftreg<7>:0
655encoder.shiftreg<8>:0
656encoder.shiftreg<9>:0
657start:0
658passes decoder.state<6>=0.
659
660--State
661ch<0>:0
662ch<1>:0
663ch<2>:0
664ch<3>:0
665ch<4>:0
666ch<5>:0
667ch<6>:0
668ch<7>:0
669character<0>:0
670character<1>:0
671character<2>:0
672character<3>:0
673character<4>:0
674character<5>:0
675character<6>:0
676character<7>:0
677ci:0
678decoder.state<0>:0
679decoder.state<1>:0
680decoder.state<2>:0
681decoder.state<3>:0
682decoder.state<4>:0
683decoder.state<5>:0
684decoder.state<6>:0
685decoder.state<7>:0
686decoder.state<8>:0
687decoder.state<9>:0
688encoder.shiftreg<0>:0
689encoder.shiftreg<1>:0
690encoder.shiftreg<2>:0
691encoder.shiftreg<3>:0
692encoder.shiftreg<4>:0
693encoder.shiftreg<5>:0
694encoder.shiftreg<6>:0
695encoder.shiftreg<7>:0
696encoder.shiftreg<8>:0
697encoder.shiftreg<9>:0
698start:0
699passes decoder.state<5>=0.
700
701--State
702ch<0>:0
703ch<1>:0
704ch<2>:0
705ch<3>:0
706ch<4>:0
707ch<5>:0
708ch<6>:0
709ch<7>:0
710character<0>:0
711character<1>:0
712character<2>:0
713character<3>:0
714character<4>:0
715character<5>:0
716character<6>:0
717character<7>:0
718ci:0
719decoder.state<0>:0
720decoder.state<1>:0
721decoder.state<2>:0
722decoder.state<3>:0
723decoder.state<4>:0
724decoder.state<5>:0
725decoder.state<6>:0
726decoder.state<7>:0
727decoder.state<8>:0
728decoder.state<9>:0
729encoder.shiftreg<0>:0
730encoder.shiftreg<1>:0
731encoder.shiftreg<2>:0
732encoder.shiftreg<3>:0
733encoder.shiftreg<4>:0
734encoder.shiftreg<5>:0
735encoder.shiftreg<6>:0
736encoder.shiftreg<7>:0
737encoder.shiftreg<8>:0
738encoder.shiftreg<9>:0
739start:0
740passes decoder.state<4>=0.
741
742--State
743ch<0>:0
744ch<1>:0
745ch<2>:0
746ch<3>:0
747ch<4>:0
748ch<5>:0
749ch<6>:0
750ch<7>:0
751character<0>:0
752character<1>:0
753character<2>:0
754character<3>:0
755character<4>:0
756character<5>:0
757character<6>:0
758character<7>:0
759ci:0
760decoder.state<0>:0
761decoder.state<1>:0
762decoder.state<2>:0
763decoder.state<3>:0
764decoder.state<4>:0
765decoder.state<5>:0
766decoder.state<6>:0
767decoder.state<7>:0
768decoder.state<8>:0
769decoder.state<9>:0
770encoder.shiftreg<0>:0
771encoder.shiftreg<1>:0
772encoder.shiftreg<2>:0
773encoder.shiftreg<3>:0
774encoder.shiftreg<4>:0
775encoder.shiftreg<5>:0
776encoder.shiftreg<6>:0
777encoder.shiftreg<7>:0
778encoder.shiftreg<8>:0
779encoder.shiftreg<9>:0
780start:0
781passes decoder.state<3>=0.
782
783--State
784ch<0>:0
785ch<1>:0
786ch<2>:0
787ch<3>:0
788ch<4>:0
789ch<5>:0
790ch<6>:0
791ch<7>:0
792character<0>:0
793character<1>:0
794character<2>:0
795character<3>:0
796character<4>:0
797character<5>:0
798character<6>:0
799character<7>:0
800ci:0
801decoder.state<0>:0
802decoder.state<1>:0
803decoder.state<2>:0
804decoder.state<3>:0
805decoder.state<4>:0
806decoder.state<5>:0
807decoder.state<6>:0
808decoder.state<7>:0
809decoder.state<8>:0
810decoder.state<9>:0
811encoder.shiftreg<0>:0
812encoder.shiftreg<1>:0
813encoder.shiftreg<2>:0
814encoder.shiftreg<3>:0
815encoder.shiftreg<4>:0
816encoder.shiftreg<5>:0
817encoder.shiftreg<6>:0
818encoder.shiftreg<7>:0
819encoder.shiftreg<8>:0
820encoder.shiftreg<9>:0
821start:0
822passes decoder.state<2>=0.
823
824--State
825ch<0>:0
826ch<1>:0
827ch<2>:0
828ch<3>:0
829ch<4>:0
830ch<5>:0
831ch<6>:0
832ch<7>:0
833character<0>:0
834character<1>:0
835character<2>:0
836character<3>:0
837character<4>:0
838character<5>:0
839character<6>:0
840character<7>:0
841ci:0
842decoder.state<0>:0
843decoder.state<1>:0
844decoder.state<2>:0
845decoder.state<3>:0
846decoder.state<4>:0
847decoder.state<5>:0
848decoder.state<6>:0
849decoder.state<7>:0
850decoder.state<8>:0
851decoder.state<9>:0
852encoder.shiftreg<0>:0
853encoder.shiftreg<1>:0
854encoder.shiftreg<2>:0
855encoder.shiftreg<3>:0
856encoder.shiftreg<4>:0
857encoder.shiftreg<5>:0
858encoder.shiftreg<6>:0
859encoder.shiftreg<7>:0
860encoder.shiftreg<8>:0
861encoder.shiftreg<9>:0
862start:0
863passes decoder.state<1>=0.
864
865--State
866ch<0>:0
867ch<1>:0
868ch<2>:0
869ch<3>:0
870ch<4>:0
871ch<5>:0
872ch<6>:0
873ch<7>:0
874character<0>:0
875character<1>:0
876character<2>:0
877character<3>:0
878character<4>:0
879character<5>:0
880character<6>:0
881character<7>:0
882ci:0
883decoder.state<0>:0
884decoder.state<1>:0
885decoder.state<2>:0
886decoder.state<3>:0
887decoder.state<4>:0
888decoder.state<5>:0
889decoder.state<6>:0
890decoder.state<7>:0
891decoder.state<8>:0
892decoder.state<9>:0
893encoder.shiftreg<0>:0
894encoder.shiftreg<1>:0
895encoder.shiftreg<2>:0
896encoder.shiftreg<3>:0
897encoder.shiftreg<4>:0
898encoder.shiftreg<5>:0
899encoder.shiftreg<6>:0
900encoder.shiftreg<7>:0
901encoder.shiftreg<8>:0
902encoder.shiftreg<9>:0
903start:0
904passes decoder.state<0>=0.
905
906--State
907ch<0>:0
908ch<1>:0
909ch<2>:0
910ch<3>:0
911ch<4>:0
912ch<5>:0
913ch<6>:0
914ch<7>:0
915character<0>:0
916character<1>:0
917character<2>:0
918character<3>:0
919character<4>:0
920character<5>:0
921character<6>:0
922character<7>:0
923ci:0
924decoder.state<0>:0
925decoder.state<1>:0
926decoder.state<2>:0
927decoder.state<3>:0
928decoder.state<4>:0
929decoder.state<5>:0
930decoder.state<6>:0
931decoder.state<7>:0
932decoder.state<8>:0
933decoder.state<9>:0
934encoder.shiftreg<0>:0
935encoder.shiftreg<1>:0
936encoder.shiftreg<2>:0
937encoder.shiftreg<3>:0
938encoder.shiftreg<4>:0
939encoder.shiftreg<5>:0
940encoder.shiftreg<6>:0
941encoder.shiftreg<7>:0
942encoder.shiftreg<8>:0
943encoder.shiftreg<9>:0
944start:0
945fails AX((ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))))
946
947 --Counter example begins
948--State 0:
949ch<0>:0
950ch<1>:0
951ch<2>:0
952ch<3>:0
953ch<4>:0
954ch<5>:0
955ch<6>:0
956ch<7>:0
957character<0>:0
958character<1>:0
959character<2>:0
960character<3>:0
961character<4>:0
962character<5>:0
963character<6>:0
964character<7>:0
965ci:0
966decoder.state<0>:0
967decoder.state<1>:0
968decoder.state<2>:0
969decoder.state<3>:0
970decoder.state<4>:0
971decoder.state<5>:0
972decoder.state<6>:0
973decoder.state<7>:0
974decoder.state<8>:0
975decoder.state<9>:0
976encoder.shiftreg<0>:0
977encoder.shiftreg<1>:0
978encoder.shiftreg<2>:0
979encoder.shiftreg<3>:0
980encoder.shiftreg<4>:0
981encoder.shiftreg<5>:0
982encoder.shiftreg<6>:0
983encoder.shiftreg<7>:0
984encoder.shiftreg<8>:0
985encoder.shiftreg<9>:0
986start:0
987
988--Goes to state 1:
989character<0>:1
990character<3>:1
991character<6>:1
992decoder.state<0>:1
993encoder.shiftreg<0>:1
994encoder.shiftreg<4>:1
995start:1
996
997 --Counter example ends
998
999
1000--State
1001ch<0>:0
1002ch<1>:0
1003ch<2>:0
1004ch<3>:0
1005ch<4>:0
1006ch<5>:0
1007ch<6>:0
1008ch<7>:0
1009character<0>:1
1010character<1>:0
1011character<2>:0
1012character<3>:1
1013character<4>:0
1014character<5>:0
1015character<6>:1
1016character<7>:0
1017ci:0
1018decoder.state<0>:1
1019decoder.state<1>:0
1020decoder.state<2>:0
1021decoder.state<3>:0
1022decoder.state<4>:0
1023decoder.state<5>:0
1024decoder.state<6>:0
1025decoder.state<7>:0
1026decoder.state<8>:0
1027decoder.state<9>:0
1028encoder.shiftreg<0>:1
1029encoder.shiftreg<1>:0
1030encoder.shiftreg<2>:0
1031encoder.shiftreg<3>:0
1032encoder.shiftreg<4>:1
1033encoder.shiftreg<5>:0
1034encoder.shiftreg<6>:0
1035encoder.shiftreg<7>:0
1036encoder.shiftreg<8>:0
1037encoder.shiftreg<9>:0
1038start:1
1039fails (ci=0 -> AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))).
1040
1041--State
1042ch<0>:0
1043ch<1>:0
1044ch<2>:0
1045ch<3>:0
1046ch<4>:0
1047ch<5>:0
1048ch<6>:0
1049ch<7>:0
1050character<0>:1
1051character<1>:0
1052character<2>:0
1053character<3>:1
1054character<4>:0
1055character<5>:0
1056character<6>:1
1057character<7>:0
1058ci:0
1059decoder.state<0>:1
1060decoder.state<1>:0
1061decoder.state<2>:0
1062decoder.state<3>:0
1063decoder.state<4>:0
1064decoder.state<5>:0
1065decoder.state<6>:0
1066decoder.state<7>:0
1067decoder.state<8>:0
1068decoder.state<9>:0
1069encoder.shiftreg<0>:1
1070encoder.shiftreg<1>:0
1071encoder.shiftreg<2>:0
1072encoder.shiftreg<3>:0
1073encoder.shiftreg<4>:1
1074encoder.shiftreg<5>:0
1075encoder.shiftreg<6>:0
1076encoder.shiftreg<7>:0
1077encoder.shiftreg<8>:0
1078encoder.shiftreg<9>:0
1079start:1
1080passes ci=0.
1081
1082--State
1083ch<0>:0
1084ch<1>:0
1085ch<2>:0
1086ch<3>:0
1087ch<4>:0
1088ch<5>:0
1089ch<6>:0
1090ch<7>:0
1091character<0>:1
1092character<1>:0
1093character<2>:0
1094character<3>:1
1095character<4>:0
1096character<5>:0
1097character<6>:1
1098character<7>:0
1099ci:0
1100decoder.state<0>:1
1101decoder.state<1>:0
1102decoder.state<2>:0
1103decoder.state<3>:0
1104decoder.state<4>:0
1105decoder.state<5>:0
1106decoder.state<6>:0
1107decoder.state<7>:0
1108decoder.state<8>:0
1109decoder.state<9>:0
1110encoder.shiftreg<0>:1
1111encoder.shiftreg<1>:0
1112encoder.shiftreg<2>:0
1113encoder.shiftreg<3>:0
1114encoder.shiftreg<4>:1
1115encoder.shiftreg<5>:0
1116encoder.shiftreg<6>:0
1117encoder.shiftreg<7>:0
1118encoder.shiftreg<8>:0
1119encoder.shiftreg<9>:0
1120start:1
1121fails AX((ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))))
1122
1123 --Counter example begins
1124--State 0:
1125ch<0>:0
1126ch<1>:0
1127ch<2>:0
1128ch<3>:0
1129ch<4>:0
1130ch<5>:0
1131ch<6>:0
1132ch<7>:0
1133character<0>:1
1134character<1>:0
1135character<2>:0
1136character<3>:1
1137character<4>:0
1138character<5>:0
1139character<6>:1
1140character<7>:0
1141ci:0
1142decoder.state<0>:1
1143decoder.state<1>:0
1144decoder.state<2>:0
1145decoder.state<3>:0
1146decoder.state<4>:0
1147decoder.state<5>:0
1148decoder.state<6>:0
1149decoder.state<7>:0
1150decoder.state<8>:0
1151decoder.state<9>:0
1152encoder.shiftreg<0>:1
1153encoder.shiftreg<1>:0
1154encoder.shiftreg<2>:0
1155encoder.shiftreg<3>:0
1156encoder.shiftreg<4>:1
1157encoder.shiftreg<5>:0
1158encoder.shiftreg<6>:0
1159encoder.shiftreg<7>:0
1160encoder.shiftreg<8>:0
1161encoder.shiftreg<9>:0
1162start:1
1163
1164--Goes to state 1:
1165ch<0>:1
1166ch<3>:1
1167ch<6>:1
1168ci:1
1169decoder.state<0>:0
1170decoder.state<1>:1
1171encoder.shiftreg<0>:0
1172encoder.shiftreg<3>:1
1173encoder.shiftreg<4>:0
1174start:0
1175
1176 --Counter example ends
1177
1178
1179--State
1180ch<0>:1
1181ch<1>:0
1182ch<2>:0
1183ch<3>:1
1184ch<4>:0
1185ch<5>:0
1186ch<6>:1
1187ch<7>:0
1188character<0>:1
1189character<1>:0
1190character<2>:0
1191character<3>:1
1192character<4>:0
1193character<5>:0
1194character<6>:1
1195character<7>:0
1196ci:1
1197decoder.state<0>:0
1198decoder.state<1>:1
1199decoder.state<2>:0
1200decoder.state<3>:0
1201decoder.state<4>:0
1202decoder.state<5>:0
1203decoder.state<6>:0
1204decoder.state<7>:0
1205decoder.state<8>:0
1206decoder.state<9>:0
1207encoder.shiftreg<0>:0
1208encoder.shiftreg<1>:0
1209encoder.shiftreg<2>:0
1210encoder.shiftreg<3>:1
1211encoder.shiftreg<4>:0
1212encoder.shiftreg<5>:0
1213encoder.shiftreg<6>:0
1214encoder.shiftreg<7>:0
1215encoder.shiftreg<8>:0
1216encoder.shiftreg<9>:0
1217start:0
1218fails (ci=1 -> AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))).
1219
1220--State
1221ch<0>:1
1222ch<1>:0
1223ch<2>:0
1224ch<3>:1
1225ch<4>:0
1226ch<5>:0
1227ch<6>:1
1228ch<7>:0
1229character<0>:1
1230character<1>:0
1231character<2>:0
1232character<3>:1
1233character<4>:0
1234character<5>:0
1235character<6>:1
1236character<7>:0
1237ci:1
1238decoder.state<0>:0
1239decoder.state<1>:1
1240decoder.state<2>:0
1241decoder.state<3>:0
1242decoder.state<4>:0
1243decoder.state<5>:0
1244decoder.state<6>:0
1245decoder.state<7>:0
1246decoder.state<8>:0
1247decoder.state<9>:0
1248encoder.shiftreg<0>:0
1249encoder.shiftreg<1>:0
1250encoder.shiftreg<2>:0
1251encoder.shiftreg<3>:1
1252encoder.shiftreg<4>:0
1253encoder.shiftreg<5>:0
1254encoder.shiftreg<6>:0
1255encoder.shiftreg<7>:0
1256encoder.shiftreg<8>:0
1257encoder.shiftreg<9>:0
1258start:0
1259passes ci=1.
1260
1261--State
1262ch<0>:1
1263ch<1>:0
1264ch<2>:0
1265ch<3>:1
1266ch<4>:0
1267ch<5>:0
1268ch<6>:1
1269ch<7>:0
1270character<0>:1
1271character<1>:0
1272character<2>:0
1273character<3>:1
1274character<4>:0
1275character<5>:0
1276character<6>:1
1277character<7>:0
1278ci:1
1279decoder.state<0>:0
1280decoder.state<1>:1
1281decoder.state<2>:0
1282decoder.state<3>:0
1283decoder.state<4>:0
1284decoder.state<5>:0
1285decoder.state<6>:0
1286decoder.state<7>:0
1287decoder.state<8>:0
1288decoder.state<9>:0
1289encoder.shiftreg<0>:0
1290encoder.shiftreg<1>:0
1291encoder.shiftreg<2>:0
1292encoder.shiftreg<3>:1
1293encoder.shiftreg<4>:0
1294encoder.shiftreg<5>:0
1295encoder.shiftreg<6>:0
1296encoder.shiftreg<7>:0
1297encoder.shiftreg<8>:0
1298encoder.shiftreg<9>:0
1299start:0
1300fails AX((ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)))
1301
1302 --Counter example begins
1303--State 0:
1304ch<0>:1
1305ch<1>:0
1306ch<2>:0
1307ch<3>:1
1308ch<4>:0
1309ch<5>:0
1310ch<6>:1
1311ch<7>:0
1312character<0>:1
1313character<1>:0
1314character<2>:0
1315character<3>:1
1316character<4>:0
1317character<5>:0
1318character<6>:1
1319character<7>:0
1320ci:1
1321decoder.state<0>:0
1322decoder.state<1>:1
1323decoder.state<2>:0
1324decoder.state<3>:0
1325decoder.state<4>:0
1326decoder.state<5>:0
1327decoder.state<6>:0
1328decoder.state<7>:0
1329decoder.state<8>:0
1330decoder.state<9>:0
1331encoder.shiftreg<0>:0
1332encoder.shiftreg<1>:0
1333encoder.shiftreg<2>:0
1334encoder.shiftreg<3>:1
1335encoder.shiftreg<4>:0
1336encoder.shiftreg<5>:0
1337encoder.shiftreg<6>:0
1338encoder.shiftreg<7>:0
1339encoder.shiftreg<8>:0
1340encoder.shiftreg<9>:0
1341start:0
1342
1343--Goes to state 1:
1344ci:0
1345decoder.state<0>:1
1346decoder.state<1>:0
1347decoder.state<2>:1
1348encoder.shiftreg<2>:1
1349encoder.shiftreg<3>:0
1350
1351 --Counter example ends
1352
1353
1354--State
1355ch<0>:1
1356ch<1>:0
1357ch<2>:0
1358ch<3>:1
1359ch<4>:0
1360ch<5>:0
1361ch<6>:1
1362ch<7>:0
1363character<0>:1
1364character<1>:0
1365character<2>:0
1366character<3>:1
1367character<4>:0
1368character<5>:0
1369character<6>:1
1370character<7>:0
1371ci:0
1372decoder.state<0>:1
1373decoder.state<1>:0
1374decoder.state<2>:1
1375decoder.state<3>:0
1376decoder.state<4>:0
1377decoder.state<5>:0
1378decoder.state<6>:0
1379decoder.state<7>:0
1380decoder.state<8>:0
1381decoder.state<9>:0
1382encoder.shiftreg<0>:0
1383encoder.shiftreg<1>:0
1384encoder.shiftreg<2>:1
1385encoder.shiftreg<3>:0
1386encoder.shiftreg<4>:0
1387encoder.shiftreg<5>:0
1388encoder.shiftreg<6>:0
1389encoder.shiftreg<7>:0
1390encoder.shiftreg<8>:0
1391encoder.shiftreg<9>:0
1392start:0
1393fails (ci=0 -> (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1)).
1394
1395--State
1396ch<0>:1
1397ch<1>:0
1398ch<2>:0
1399ch<3>:1
1400ch<4>:0
1401ch<5>:0
1402ch<6>:1
1403ch<7>:0
1404character<0>:1
1405character<1>:0
1406character<2>:0
1407character<3>:1
1408character<4>:0
1409character<5>:0
1410character<6>:1
1411character<7>:0
1412ci:0
1413decoder.state<0>:1
1414decoder.state<1>:0
1415decoder.state<2>:1
1416decoder.state<3>:0
1417decoder.state<4>:0
1418decoder.state<5>:0
1419decoder.state<6>:0
1420decoder.state<7>:0
1421decoder.state<8>:0
1422decoder.state<9>:0
1423encoder.shiftreg<0>:0
1424encoder.shiftreg<1>:0
1425encoder.shiftreg<2>:1
1426encoder.shiftreg<3>:0
1427encoder.shiftreg<4>:0
1428encoder.shiftreg<5>:0
1429encoder.shiftreg<6>:0
1430encoder.shiftreg<7>:0
1431encoder.shiftreg<8>:0
1432encoder.shiftreg<9>:0
1433start:0
1434passes ci=0.
1435
1436--State
1437ch<0>:1
1438ch<1>:0
1439ch<2>:0
1440ch<3>:1
1441ch<4>:0
1442ch<5>:0
1443ch<6>:1
1444ch<7>:0
1445character<0>:1
1446character<1>:0
1447character<2>:0
1448character<3>:1
1449character<4>:0
1450character<5>:0
1451character<6>:1
1452character<7>:0
1453ci:0
1454decoder.state<0>:1
1455decoder.state<1>:0
1456decoder.state<2>:1
1457decoder.state<3>:0
1458decoder.state<4>:0
1459decoder.state<5>:0
1460decoder.state<6>:0
1461decoder.state<7>:0
1462decoder.state<8>:0
1463decoder.state<9>:0
1464encoder.shiftreg<0>:0
1465encoder.shiftreg<1>:0
1466encoder.shiftreg<2>:1
1467encoder.shiftreg<3>:0
1468encoder.shiftreg<4>:0
1469encoder.shiftreg<5>:0
1470encoder.shiftreg<6>:0
1471encoder.shiftreg<7>:0
1472encoder.shiftreg<8>:0
1473encoder.shiftreg<9>:0
1474start:0
1475fails (((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0) * plain<0>=1).
1476
1477--State
1478ch<0>:1
1479ch<1>:0
1480ch<2>:0
1481ch<3>:1
1482ch<4>:0
1483ch<5>:0
1484ch<6>:1
1485ch<7>:0
1486character<0>:1
1487character<1>:0
1488character<2>:0
1489character<3>:1
1490character<4>:0
1491character<5>:0
1492character<6>:1
1493character<7>:0
1494ci:0
1495decoder.state<0>:1
1496decoder.state<1>:0
1497decoder.state<2>:1
1498decoder.state<3>:0
1499decoder.state<4>:0
1500decoder.state<5>:0
1501decoder.state<6>:0
1502decoder.state<7>:0
1503decoder.state<8>:0
1504decoder.state<9>:0
1505encoder.shiftreg<0>:0
1506encoder.shiftreg<1>:0
1507encoder.shiftreg<2>:1
1508encoder.shiftreg<3>:0
1509encoder.shiftreg<4>:0
1510encoder.shiftreg<5>:0
1511encoder.shiftreg<6>:0
1512encoder.shiftreg<7>:0
1513encoder.shiftreg<8>:0
1514encoder.shiftreg<9>:0
1515start:0
1516fails ((((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1) * plain<1>=0).
1517
1518--State
1519ch<0>:1
1520ch<1>:0
1521ch<2>:0
1522ch<3>:1
1523ch<4>:0
1524ch<5>:0
1525ch<6>:1
1526ch<7>:0
1527character<0>:1
1528character<1>:0
1529character<2>:0
1530character<3>:1
1531character<4>:0
1532character<5>:0
1533character<6>:1
1534character<7>:0
1535ci:0
1536decoder.state<0>:1
1537decoder.state<1>:0
1538decoder.state<2>:1
1539decoder.state<3>:0
1540decoder.state<4>:0
1541decoder.state<5>:0
1542decoder.state<6>:0
1543decoder.state<7>:0
1544decoder.state<8>:0
1545decoder.state<9>:0
1546encoder.shiftreg<0>:0
1547encoder.shiftreg<1>:0
1548encoder.shiftreg<2>:1
1549encoder.shiftreg<3>:0
1550encoder.shiftreg<4>:0
1551encoder.shiftreg<5>:0
1552encoder.shiftreg<6>:0
1553encoder.shiftreg<7>:0
1554encoder.shiftreg<8>:0
1555encoder.shiftreg<9>:0
1556start:0
1557fails (((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0) * plain<2>=1).
1558
1559--State
1560ch<0>:1
1561ch<1>:0
1562ch<2>:0
1563ch<3>:1
1564ch<4>:0
1565ch<5>:0
1566ch<6>:1
1567ch<7>:0
1568character<0>:1
1569character<1>:0
1570character<2>:0
1571character<3>:1
1572character<4>:0
1573character<5>:0
1574character<6>:1
1575character<7>:0
1576ci:0
1577decoder.state<0>:1
1578decoder.state<1>:0
1579decoder.state<2>:1
1580decoder.state<3>:0
1581decoder.state<4>:0
1582decoder.state<5>:0
1583decoder.state<6>:0
1584decoder.state<7>:0
1585decoder.state<8>:0
1586decoder.state<9>:0
1587encoder.shiftreg<0>:0
1588encoder.shiftreg<1>:0
1589encoder.shiftreg<2>:1
1590encoder.shiftreg<3>:0
1591encoder.shiftreg<4>:0
1592encoder.shiftreg<5>:0
1593encoder.shiftreg<6>:0
1594encoder.shiftreg<7>:0
1595encoder.shiftreg<8>:0
1596encoder.shiftreg<9>:0
1597start:0
1598fails ((((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0) * plain<3>=0).
1599
1600--State
1601ch<0>:1
1602ch<1>:0
1603ch<2>:0
1604ch<3>:1
1605ch<4>:0
1606ch<5>:0
1607ch<6>:1
1608ch<7>:0
1609character<0>:1
1610character<1>:0
1611character<2>:0
1612character<3>:1
1613character<4>:0
1614character<5>:0
1615character<6>:1
1616character<7>:0
1617ci:0
1618decoder.state<0>:1
1619decoder.state<1>:0
1620decoder.state<2>:1
1621decoder.state<3>:0
1622decoder.state<4>:0
1623decoder.state<5>:0
1624decoder.state<6>:0
1625decoder.state<7>:0
1626decoder.state<8>:0
1627decoder.state<9>:0
1628encoder.shiftreg<0>:0
1629encoder.shiftreg<1>:0
1630encoder.shiftreg<2>:1
1631encoder.shiftreg<3>:0
1632encoder.shiftreg<4>:0
1633encoder.shiftreg<5>:0
1634encoder.shiftreg<6>:0
1635encoder.shiftreg<7>:0
1636encoder.shiftreg<8>:0
1637encoder.shiftreg<9>:0
1638start:0
1639fails (((plain<7>=0 * plain<6>=1) * plain<5>=0) * plain<4>=0).
1640
1641--State
1642ch<0>:1
1643ch<1>:0
1644ch<2>:0
1645ch<3>:1
1646ch<4>:0
1647ch<5>:0
1648ch<6>:1
1649ch<7>:0
1650character<0>:1
1651character<1>:0
1652character<2>:0
1653character<3>:1
1654character<4>:0
1655character<5>:0
1656character<6>:1
1657character<7>:0
1658ci:0
1659decoder.state<0>:1
1660decoder.state<1>:0
1661decoder.state<2>:1
1662decoder.state<3>:0
1663decoder.state<4>:0
1664decoder.state<5>:0
1665decoder.state<6>:0
1666decoder.state<7>:0
1667decoder.state<8>:0
1668decoder.state<9>:0
1669encoder.shiftreg<0>:0
1670encoder.shiftreg<1>:0
1671encoder.shiftreg<2>:1
1672encoder.shiftreg<3>:0
1673encoder.shiftreg<4>:0
1674encoder.shiftreg<5>:0
1675encoder.shiftreg<6>:0
1676encoder.shiftreg<7>:0
1677encoder.shiftreg<8>:0
1678encoder.shiftreg<9>:0
1679start:0
1680fails ((plain<7>=0 * plain<6>=1) * plain<5>=0).
1681
1682--State
1683ch<0>:1
1684ch<1>:0
1685ch<2>:0
1686ch<3>:1
1687ch<4>:0
1688ch<5>:0
1689ch<6>:1
1690ch<7>:0
1691character<0>:1
1692character<1>:0
1693character<2>:0
1694character<3>:1
1695character<4>:0
1696character<5>:0
1697character<6>:1
1698character<7>:0
1699ci:0
1700decoder.state<0>:1
1701decoder.state<1>:0
1702decoder.state<2>:1
1703decoder.state<3>:0
1704decoder.state<4>:0
1705decoder.state<5>:0
1706decoder.state<6>:0
1707decoder.state<7>:0
1708decoder.state<8>:0
1709decoder.state<9>:0
1710encoder.shiftreg<0>:0
1711encoder.shiftreg<1>:0
1712encoder.shiftreg<2>:1
1713encoder.shiftreg<3>:0
1714encoder.shiftreg<4>:0
1715encoder.shiftreg<5>:0
1716encoder.shiftreg<6>:0
1717encoder.shiftreg<7>:0
1718encoder.shiftreg<8>:0
1719encoder.shiftreg<9>:0
1720start:0
1721fails (plain<7>=0 * plain<6>=1).
1722
1723--State
1724ch<0>:1
1725ch<1>:0
1726ch<2>:0
1727ch<3>:1
1728ch<4>:0
1729ch<5>:0
1730ch<6>:1
1731ch<7>:0
1732character<0>:1
1733character<1>:0
1734character<2>:0
1735character<3>:1
1736character<4>:0
1737character<5>:0
1738character<6>:1
1739character<7>:0
1740ci:0
1741decoder.state<0>:1
1742decoder.state<1>:0
1743decoder.state<2>:1
1744decoder.state<3>:0
1745decoder.state<4>:0
1746decoder.state<5>:0
1747decoder.state<6>:0
1748decoder.state<7>:0
1749decoder.state<8>:0
1750decoder.state<9>:0
1751encoder.shiftreg<0>:0
1752encoder.shiftreg<1>:0
1753encoder.shiftreg<2>:1
1754encoder.shiftreg<3>:0
1755encoder.shiftreg<4>:0
1756encoder.shiftreg<5>:0
1757encoder.shiftreg<6>:0
1758encoder.shiftreg<7>:0
1759encoder.shiftreg<8>:0
1760encoder.shiftreg<9>:0
1761start:0
1762passes plain<7>=0.
1763
1764--State
1765ch<0>:1
1766ch<1>:0
1767ch<2>:0
1768ch<3>:1
1769ch<4>:0
1770ch<5>:0
1771ch<6>:1
1772ch<7>:0
1773character<0>:1
1774character<1>:0
1775character<2>:0
1776character<3>:1
1777character<4>:0
1778character<5>:0
1779character<6>:1
1780character<7>:0
1781ci:0
1782decoder.state<0>:1
1783decoder.state<1>:0
1784decoder.state<2>:1
1785decoder.state<3>:0
1786decoder.state<4>:0
1787decoder.state<5>:0
1788decoder.state<6>:0
1789decoder.state<7>:0
1790decoder.state<8>:0
1791decoder.state<9>:0
1792encoder.shiftreg<0>:0
1793encoder.shiftreg<1>:0
1794encoder.shiftreg<2>:1
1795encoder.shiftreg<3>:0
1796encoder.shiftreg<4>:0
1797encoder.shiftreg<5>:0
1798encoder.shiftreg<6>:0
1799encoder.shiftreg<7>:0
1800encoder.shiftreg<8>:0
1801encoder.shiftreg<9>:0
1802start:0
1803fails plain<6>=1.
1804
1805
Note: See TracBrowser for help on using the repository browser.