Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

cex @ 106

Last change on this file since 106 was 105, checked in by cecile, 12 years ago
Hufmann case study
File size: 31.4 KB

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

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format