Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Normal
Revision Log

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

Rev	Line
[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
	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