/usr/lib64/jvm/java/bin/java -Didea.launcher.port=7532 -Didea.launcher.bin.path=/home/ssedai/tools/idea-IC-139.224.1/bin -Dfile.encoding=UTF-8 -classpath /home/ssedai/projects/retrascope.svn/bin:/usr/lib64/jvm/java/jre/lib/rt.jar:/usr/lib64/jvm/java/jre/lib/management-agent.jar:/usr/lib64/jvm/java/jre/lib/charsets.jar:/usr/lib64/jvm/java/jre/lib/jce.jar:/usr/lib64/jvm/java/jre/lib/resources.jar:/usr/lib64/jvm/java/jre/lib/rhino.jar:/usr/lib64/jvm/java/jre/lib/jsse.jar:/usr/lib64/jvm/java/jre/lib/ext/dnsns.jar:/usr/lib64/jvm/java/jre/lib/ext/sunjce_provider.jar:/usr/lib64/jvm/java/jre/lib/ext/gnome-java-bridge.jar:/usr/lib64/jvm/java/jre/lib/ext/zipfs.jar:/usr/lib64/jvm/java/jre/lib/ext/sunpkcs11.jar:/usr/lib64/jvm/java/jre/lib/ext/localedata.jar:/usr/lib64/jvm/java/jre/lib/ext/pulse-java.jar:/home/ssedai/projects/retrascope.svn/share/jar/collections-generic-4.01.jar:/home/ssedai/projects/retrascope.svn/share/jar/commons-cli-1.2.jar:/home/ssedai/projects/retrascope.svn/share/jar/commons-io-2.4.jar:/home/ssedai/projects/retrascope.svn/share/jar/commons-logging-1.0.4.jar:/home/ssedai/projects/retrascope.svn/share/jar/commons-lang-2.4.jar:/home/ssedai/projects/retrascope.svn/share/jar/jung-api-2.0.1.jar:/home/ssedai/projects/retrascope.svn/share/jar/jung-graph-impl-2.0.1.jar:/home/ssedai/projects/retrascope.svn/share/jar/junit-4.7.jar:/home/ssedai/projects/retrascope.svn/share/jar/jython.jar:/home/ssedai/projects/retrascope.svn/share/jar/log4j-1.2.14.jar:/home/ssedai/projects/retrascope.svn/share/jar/log5j-1.2.jar:/home/ssedai/projects/retrascope.svn/share/jar/antlrworks-1.4.3.jar:/home/ssedai/projects/retrascope.svn/share/jar/zamiacad.jar:/home/ssedai/projects/retrascope.svn/share/jar:/home/ssedai/projects/retrascope.svn/share/jar/veritrans.jar:/home/ssedai/projects/retrascope.svn/share/jar/fortress-0.3.3-beta-141226.jar:/home/ssedai/tools/idea-IC-139.224.1/lib/idea_rt.jar com.intellij.rt.execution.application.AppMain ru.ispras.retrascope.Retrascope /home/ssedai/projects/retrascope.svn/src/test/vhdl/itc99-poli2/b10/b10.vhd --engine efsm-fate-test-generator --toplevel b10
2015.01.23 18:50:26.991. INFO: Retrascope is starting
Running: vhdl-parser
Options: {args=/home/ssedai/projects/retrascope.svn/src/test/vhdl/itc99-poli2/b10/b10.vhd --engine efsm-fate-test-generator --toplevel b10, vhd=[/home/ssedai/projects/retrascope.svn/src/test/vhdl/itc99-poli2/b10/b10.vhd]}
Storing: cfg

Running: cfg-cgaa-transformer
Options: {args=/home/ssedai/projects/retrascope.svn/src/test/vhdl/itc99-poli2/b10/b10.vhd --engine efsm-fate-test-generator --toplevel b10, cfg=<cfg>}
Storing: cgaa

Running: cgaa-efsm-transformer
Options: {cgaa=<cgaa>, args=/home/ssedai/projects/retrascope.svn/src/test/vhdl/itc99-poli2/b10/b10.vhd --engine efsm-fate-test-generator --toplevel b10}
2015.01.23 18:50:30.225. INFO: Number of GADD paths: 33
2015.01.23 18:50:30.226. INFO: ======================================
2015.01.23 18:50:30.226. INFO: Clock-like variables: [RESET, CLOCK]
2015.01.23 18:50:30.226. INFO: Transforming the process of module: WORK.B10(BEHAV)
2015.01.23 18:50:30.478. INFO: 11 states are extracted.
2015.01.23 18:50:30.478. INFO: The state-like variables are: [STATO]
2015.01.23 18:50:45.334. INFO: 66 transitions are extracted.
Storing: efsm
2015.01.23 18:50:45.334. INFO: 1 EFSM(s) are extracted.

Running: efsm-fate-test-generator
2015.01.23 18:50:45.334. INFO: FATE: sequence length isn't specified. Setting it to the default value: 11
Options: {efsm=<efsm>, args=/home/ssedai/projects/retrascope.svn/src/test/vhdl/itc99-poli2/b10/b10.vhd --engine efsm-fate-test-generator --toplevel b10}
2015.01.23 18:50:45.335. INFO: FATE: sequences number isn't specified. Setting it to the default value: 6
2015.01.23 18:50:45.346. INFO: EFSM simulator.WORK.B10(BEHAV)_0: resetting EFSM
2015.01.23 18:50:45.346. INFO: FATE.WORK.B10(BEHAV)_0: detecting control dependencies
2015.01.23 18:50:45.588. INFO: FATE.WORK.B10(BEHAV)_0: control dependencies have been processed successfully
2015.01.23 18:50:45.588. INFO: FATE.WORK.B10(BEHAV)_0: detecting data dependencies
2015.01.23 18:50:45.934. INFO: FATE.WORK.B10(BEHAV)_0: data dependencies have been processed successfully
2015.01.23 18:50:45.934. INFO: FATE.WORK.B10(BEHAV)_0: detecting counters
2015.01.23 18:50:45.982. INFO: FATE.WORK.B10(BEHAV)_0: the counter VOTO2 is defined by the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1) (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[VOTO2] := (BVNOT VOTO2)}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.086. INFO: FATE.WORK.B10(BEHAV)_0: the counter VOTO2 is defined by the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1) (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[VOTO2] := (BVNOT VOTO2)}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.095. INFO: FATE.WORK.B10(BEHAV)_0: the counter VOTO2 is defined by the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (NOT (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1)) (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[VOTO2] := (BVNOT VOTO2)}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.147. INFO: FATE.WORK.B10(BEHAV)_0: the counter VOTO2 is defined by the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (NOT (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1)) (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[VOTO2] := (BVNOT VOTO2)}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.174. INFO: FATE.WORK.B10(BEHAV)_0: counters have been processed successfully
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ TEST 0)) (AND (OR (EQ TEST 1) (EQ TEST 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[SIGN] := 0000}; assignment: {[STATO] := 9}}}}}
2015.01.23 18:50:46.175. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ TEST 0))) (AND (OR (EQ TEST 1) (EQ TEST 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[VOTO0__retrascope_29] := 0}; assignment: {[VOTO1__retrascope_30] := 0}; assignment: {[VOTO2__retrascope_31] := 0}; assignment: {[VOTO3__retrascope_32] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[STATO] := 1}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ START 1) (NOT (EQ RTR 1)) (EQ RTR 0)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[CTS] := BLOCK_CTS_0}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 1)) (NOT (EQ RTR 1)) (EQ RTR 0)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[CTS] := BLOCK_CTS_0}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ START 0)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[STATO] := 3}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1) (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[VOTO2] := (BVNOT VOTO2)}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1) (NOT (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1))) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (NOT (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1)) (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1)) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[VOTO2] := (BVNOT VOTO2)}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (EQ KEY 1) (NOT (EQ (BVAND (BVXOR G_BUTTON LAST_G) G_BUTTON) 1)) (NOT (EQ (BVAND (BVXOR R_BUTTON LAST_R) R_BUTTON) 1))) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ LAST_G 1) (EQ LAST_G 0)) (OR (EQ LAST_R 1) (EQ LAST_R 0)) (OR (EQ G_BUTTON 1) (EQ G_BUTTON 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0)) (OR (EQ R_BUTTON 1) (EQ R_BUTTON 0))))}->{{assignment: {[VOTO0] := KEY}; assignment: {[LAST_G] := G_BUTTON}; assignment: {[LAST_R] := R_BUTTON}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ START 0)) (NOT (EQ KEY 1))) (AND (OR (EQ START 1) (EQ START 0)) (OR (EQ KEY 1) (EQ KEY 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{}: {predicate: (AND (NOT (EQ RESET 1)) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO3] := (BVXOR VOTO0 (BVXOR VOTO1 VOTO2))}; assignment: {[STATO] := 4}; assignment: {[VOTO0] := 0}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ RTR 1) (AND (AND (AND (EQ VOTO0 0) (EQ VOTO1 1)) (EQ VOTO2 1)) (EQ VOTO3 0))) (AND (OR (EQ VOTO2 1) (EQ VOTO2 0)) (OR (EQ VOTO3 1) (EQ VOTO3 0)) (OR (EQ VOTO0 1) (EQ VOTO0 0)) (OR (EQ VOTO1 1) (EQ VOTO1 0)) (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[BLOCK_V_OUT_0] := VOTO0}; assignment: {[BLOCK_V_OUT_1] := VOTO1}; assignment: {[BLOCK_V_OUT_2] := VOTO2}; assignment: {[BLOCK_V_OUT_3] := VOTO3}; assignment: {[BLOCK_CTS_4] := 1}; assignment: {[V_OUT] := BLOCK_V_OUT_0}; assignment: {[V_OUT] := BLOCK_V_OUT_1}; assignment: {[V_OUT] := BLOCK_V_OUT_2}; assignment: {[V_OUT] := BLOCK_V_OUT_3}; assignment: {[CTS] := BLOCK_CTS_4}; assignment: {[STATO] := 8}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ RTR 1) (NOT (AND (AND (AND (EQ VOTO0 0) (EQ VOTO1 1)) (EQ VOTO2 1)) (EQ VOTO3 0)))) (AND (OR (EQ VOTO2 1) (EQ VOTO2 0)) (OR (EQ VOTO3 1) (EQ VOTO3 0)) (OR (EQ VOTO0 1) (EQ VOTO0 0)) (OR (EQ VOTO1 1) (EQ VOTO1 0)) (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[BLOCK_V_OUT_0] := VOTO0}; assignment: {[BLOCK_V_OUT_1] := VOTO1}; assignment: {[BLOCK_V_OUT_2] := VOTO2}; assignment: {[BLOCK_V_OUT_3] := VOTO3}; assignment: {[BLOCK_CTS_4] := 1}; assignment: {[V_OUT] := BLOCK_V_OUT_0}; assignment: {[V_OUT] := BLOCK_V_OUT_1}; assignment: {[V_OUT] := BLOCK_V_OUT_2}; assignment: {[V_OUT] := BLOCK_V_OUT_3}; assignment: {[CTS] := BLOCK_CTS_4}; assignment: {[STATO] := 5}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ RTR 1))) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (EQ BLOCK_STATO_1 0)))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (NOT (EQ BLOCK_STATO_1 0)) (EQ BLOCK_STATO_1 1))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (EQ BLOCK_STATO_1 2))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (EQ BLOCK_STATO_1 3))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (EQ BLOCK_STATO_1 4))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.176. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (EQ BLOCK_STATO_1 5))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (EQ BLOCK_STATO_1 6))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (EQ BLOCK_STATO_1 7))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (EQ BLOCK_STATO_1 8))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (NOT (EQ BLOCK_STATO_1 8))) (EQ BLOCK_STATO_1 9))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTS 0)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (NOT (EQ BLOCK_STATO_1 8))) (NOT (EQ BLOCK_STATO_1 9))) (EQ BLOCK_STATO_1 10))))}->{{assignment: {[BLOCK_CTR_0] := 1}; assignment: {[BLOCK_STATO_1] := 6}; assignment: {[CTR] := BLOCK_CTR_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ RTS 0))) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ RTS 1)) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[VOTO0] := (BVEXTRACT 0 0 V_IN)}; assignment: {[VOTO1] := (BVEXTRACT 1 1 V_IN)}; assignment: {[VOTO2] := (BVEXTRACT 2 2 V_IN)}; assignment: {[VOTO3] := (BVEXTRACT 3 3 V_IN)}; assignment: {[CTR] := 0}; assignment: {[STATO] := 7}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ RTS 1))) (AND (OR (EQ RTS 1) (EQ RTS 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (EQ BLOCK_STATO_1 0)))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (NOT (EQ BLOCK_STATO_1 0)) (EQ BLOCK_STATO_1 1))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (EQ BLOCK_STATO_1 2))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (EQ BLOCK_STATO_1 3))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (EQ BLOCK_STATO_1 4))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (EQ BLOCK_STATO_1 5))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (EQ BLOCK_STATO_1 6))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (EQ BLOCK_STATO_1 7))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.177. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (EQ BLOCK_STATO_1 8))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (NOT (EQ BLOCK_STATO_1 8))) (EQ BLOCK_STATO_1 9))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (NOT (EQ BLOCK_STATO_1 8))) (NOT (EQ BLOCK_STATO_1 9))) (EQ BLOCK_STATO_1 10))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 4}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ RTR 0))) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (EQ BLOCK_STATO_1 0)))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (NOT (EQ BLOCK_STATO_1 0)) (EQ BLOCK_STATO_1 1))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (EQ BLOCK_STATO_1 2))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (EQ BLOCK_STATO_1 3))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (EQ BLOCK_STATO_1 4))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (EQ BLOCK_STATO_1 5))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (EQ BLOCK_STATO_1 6))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (EQ BLOCK_STATO_1 7))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (EQ BLOCK_STATO_1 8))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (NOT (EQ BLOCK_STATO_1 8))) (EQ BLOCK_STATO_1 9))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); guarded action: {{posedge of CLOCK}: {predicate: (AND (AND (AND (NOT (EQ RESET 1)) (EQ RTR 0)) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0)))) (AND (AND (NOT (LESS BLOCK_STATO_1 0)) (OR (LESS BLOCK_STATO_1 10) (EQ BLOCK_STATO_1 10))) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ BLOCK_STATO_1 0)) (NOT (EQ BLOCK_STATO_1 1))) (NOT (EQ BLOCK_STATO_1 2))) (NOT (EQ BLOCK_STATO_1 3))) (NOT (EQ BLOCK_STATO_1 4))) (NOT (EQ BLOCK_STATO_1 5))) (NOT (EQ BLOCK_STATO_1 6))) (NOT (EQ BLOCK_STATO_1 7))) (NOT (EQ BLOCK_STATO_1 8))) (NOT (EQ BLOCK_STATO_1 9))) (EQ BLOCK_STATO_1 10))))}->{{assignment: {[BLOCK_CTS_0] := 0}; assignment: {[BLOCK_STATO_1] := 1}; assignment: {[CTS] := BLOCK_CTS_0}; assignment: {[STATO] := BLOCK_STATO_1}}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (EQ RTR 0))) (AND (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{}}}}
2015.01.23 18:50:46.178. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (AND (AND (AND (EQ (BVEXTRACT 0 0 V_IN) 1) (EQ (BVEXTRACT 1 1 V_IN) 1)) (EQ (BVEXTRACT 2 2 V_IN) 1)) (EQ (BVEXTRACT 3 3 V_IN) 1))) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0] := (BVEXTRACT 0 0 V_IN)}; assignment: {[VOTO1] := (BVEXTRACT 1 1 V_IN)}; assignment: {[VOTO2] := (BVEXTRACT 2 2 V_IN)}; assignment: {[VOTO3] := (BVEXTRACT 3 3 V_IN)}; assignment: {[SIGN] := 1000}; assignment: {[STATO] := 10}}}}}
2015.01.23 18:50:46.179. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (NOT (AND (AND (AND (EQ (BVEXTRACT 0 0 V_IN) 1) (EQ (BVEXTRACT 1 1 V_IN) 1)) (EQ (BVEXTRACT 2 2 V_IN) 1)) (EQ (BVEXTRACT 3 3 V_IN) 1)))) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0] := (BVEXTRACT 0 0 V_IN)}; assignment: {[VOTO1] := (BVEXTRACT 1 1 V_IN)}; assignment: {[VOTO2] := (BVEXTRACT 2 2 V_IN)}; assignment: {[VOTO3] := (BVEXTRACT 3 3 V_IN)}; assignment: {[SIGN] := 1000}}}}}
2015.01.23 18:50:46.179. INFO: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{}: {predicate: (AND (NOT (EQ RESET 1)) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0__retrascope_33] := (BVXOR 1 (BVEXTRACT 0 0 SIGN))}; assignment: {[VOTO0__retrascope_34] := (BVXOR 0 (BVEXTRACT 1 1 SIGN))}; assignment: {[VOTO0__retrascope_35] := (BVXOR 0 (BVEXTRACT 2 2 SIGN))}; assignment: {[VOTO0] := (BVXOR 1 (BVEXTRACT 3 3 SIGN))}; assignment: {[STATO] := 4}}}}}
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (EQ STATO 2)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (EQ STATO 3)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (EQ STATO 6)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (EQ STATO 7)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (EQ STATO 8)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9)))
2015.01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10)))
2015.01.23 18:50:46.181. INFO: FATE: starting a new sequence (01 of 6)
2015.01.23 18:50:46.181. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:46.181. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random sequence
2015.01.23 18:50:46.182. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 0% (0 of 66 transitions)
2015.01.23 18:50:46.207. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.207. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 1; START = 0; V_IN = 0001; G_BUTTON = 0; RTS = 0; KEY = 1; RTR = 0; R_BUTTON = 0}}
2015.01.23 18:50:46.207. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 0% (0 of 66 transitions)
2015.01.23 18:50:46.208. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:46.208. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 0001; G_BUTTON = 0; RTS = 0; KEY = 1; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:46.259. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.464. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:46.464. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:46.465. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 0; V_IN = 0001; RTS = 0; RESET = 1; RTR = 0; KEY = 1; R_BUTTON = 0}}
2015.01.23 18:50:46.466. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:46.466. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:46.466. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:46.486. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.486. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 1; START = 1; V_IN = 1111; G_BUTTON = 0; RTS = 1; KEY = 1; RTR = 1; R_BUTTON = 0}}
2015.01.23 18:50:46.486. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:46.486. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:46.486. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 1; V_IN = 1111; G_BUTTON = 0; RTS = 1; KEY = 1; RTR = 1; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:46.544. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.749. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:46.750. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:46.750. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 1; G_BUTTON = 0; V_IN = 1111; RTS = 1; RESET = 1; RTR = 1; KEY = 1; R_BUTTON = 0}}
2015.01.23 18:50:46.750. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:46.750. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:46.750. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:46.773. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:46.773. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 1; START = 0; V_IN = 0101; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 1; R_BUTTON = 1}}
2015.01.23 18:50:46.773. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:46.773. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:46.773. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 0101; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 1; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:46.830. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:47.046. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:47.046. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:47.046. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 1; V_IN = 0101; RTS = 0; RESET = 1; RTR = 1; KEY = 1; R_BUTTON = 1}}
2015.01.23 18:50:47.046. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.046. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:47.047. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.064. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:47.064. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 1010; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; R_BUTTON = 1}}
2015.01.23 18:50:47.064. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.064. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:47.065. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 1010; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:47.124. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:47.636. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:47.636. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:47.637. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 1010; RTS = 0; RESET = 1; RTR = 1; KEY = 0; R_BUTTON = 1}}
2015.01.23 18:50:47.637. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.638. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:47.638. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.656. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:47.656. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 1; START = 0; V_IN = 0110; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; R_BUTTON = 0}}
2015.01.23 18:50:47.656. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.657. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:47.657. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 0110; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:47.788. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:47.991. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:47.992. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:47.992. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 1; V_IN = 0110; RTS = 0; RESET = 1; RTR = 1; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:47.992. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:47.992. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:47.992. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.009. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.009. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 1; V_IN = 1100; G_BUTTON = 0; RTS = 0; KEY = 0; RTR = 0; R_BUTTON = 0}; transaction: {RESET = 1}}
2015.01.23 18:50:48.010. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.010. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:48.010. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 1; V_IN = 1100; G_BUTTON = 0; RTS = 0; KEY = 0; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:48.059. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.272. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:48.272. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:48.273. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 1; G_BUTTON = 0; V_IN = 1100; RTS = 0; RTR = 0; KEY = 0; RESET = 1; R_BUTTON = 0}}
2015.01.23 18:50:48.273. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.273. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:48.274. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.291. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.292. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 1; V_IN = 0111; G_BUTTON = 0; RTS = 0; KEY = 1; RTR = 1; R_BUTTON = 0}}
2015.01.23 18:50:48.292. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.292. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:48.292. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 1; V_IN = 0111; G_BUTTON = 0; RTS = 0; KEY = 1; RTR = 1; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:48.350. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.548. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:48.548. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:48.549. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 1; G_BUTTON = 0; V_IN = 0111; RTS = 0; RESET = 1; RTR = 1; KEY = 1; R_BUTTON = 0}}
2015.01.23 18:50:48.549. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.549. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:48.550. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.568. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.568. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 0; V_IN = 1011; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 1; R_BUTTON = 0}; transaction: {RESET = 1}}
2015.01.23 18:50:48.568. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.569. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:48.569. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 1011; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:48.624. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.829. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:48.829. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:48.830. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 0; V_IN = 1011; RTS = 1; RESET = 1; RTR = 1; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:48.830. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.830. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:48.831. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.853. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:48.854. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 1011; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 0; R_BUTTON = 1}}
2015.01.23 18:50:48.854. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:48.854. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:48.854. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 1011; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 0; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:48.906. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.097. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:49.097. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:49.098. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 0; V_IN = 1011; RTS = 1; RESET = 1; RTR = 0; KEY = 0; R_BUTTON = 1}}
2015.01.23 18:50:49.098. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.098. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:49.099. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.118. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.118. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 0101; G_BUTTON = 1; RTS = 1; KEY = 0; RTR = 0; R_BUTTON = 0}}
2015.01.23 18:50:49.118. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.119. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:49.119. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 0101; G_BUTTON = 1; RTS = 1; KEY = 0; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:49.174. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.386. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:49.386. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:49.387. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 0101; RTS = 1; RESET = 1; RTR = 0; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:49.387. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.387. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:49.388. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.406. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.406. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 1; V_IN = 0000; G_BUTTON = 0; RTS = 1; KEY = 1; RTR = 0; R_BUTTON = 0}; transaction: {RESET = 1}}
2015.01.23 18:50:49.407. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.407. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:49.407. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 1; V_IN = 0000; G_BUTTON = 0; RTS = 1; KEY = 1; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:49.457. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.643. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:49.643. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:49.644. INFO: EFSM simulator.WORK.B10(BEHAV)_0: resetting EFSM
2015.01.23 18:50:49.645. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 1; G_BUTTON = 0; V_IN = 0000; RTS = 1; RTR = 0; KEY = 1; RESET = 1; R_BUTTON = 0}}
2015.01.23 18:50:49.645. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.645. INFO: FATE: starting a new sequence (11 of 6)
2015.01.23 18:50:49.646. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:49.646. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random sequence
2015.01.23 18:50:49.646. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.664. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.664. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 0; START = 1; V_IN = 0000; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 1; R_BUTTON = 1}; transaction: {RESET = 1}}
2015.01.23 18:50:49.664. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.665. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:49.665. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 1; V_IN = 0000; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:49.720. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.923. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:49.923. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:49.924. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 1; G_BUTTON = 0; V_IN = 0000; RTS = 1; RTR = 1; KEY = 0; RESET = 1; R_BUTTON = 1}}
2015.01.23 18:50:49.924. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.925. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:49.925. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.943. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:49.943. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 0; V_IN = 1011; G_BUTTON = 1; RTS = 1; KEY = 0; RTR = 0; R_BUTTON = 0}; transaction: {RESET = 1}}
2015.01.23 18:50:49.943. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:49.944. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:49.944. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 1011; G_BUTTON = 1; RTS = 1; KEY = 0; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:49.995. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:50.197. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:50.197. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:50.198. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 1; V_IN = 1011; RTS = 1; RESET = 1; RTR = 0; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:50.198. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.199. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:50.199. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.218. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:50.218. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 0011; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 0; R_BUTTON = 0}}
2015.01.23 18:50:50.218. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.218. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:50.218. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 0011; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:50.270. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:50.482. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:50.483. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:50.484. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 0011; RTS = 0; RESET = 1; RTR = 0; KEY = 1; R_BUTTON = 0}}
2015.01.23 18:50:50.484. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.484. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:50.485. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.504. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:50.504. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 1000; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; R_BUTTON = 0}}
2015.01.23 18:50:50.504. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.504. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:50.505. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 1000; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:50.555. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:50.749. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:50.750. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:50.751. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 1000; RTS = 0; RESET = 1; RTR = 1; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:50.751. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.751. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:50.751. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.769. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:50.769. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 0; V_IN = 1001; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 0; R_BUTTON = 1}; transaction: {RESET = 1}}
2015.01.23 18:50:50.769. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:50.770. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:50.770. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 1001; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 0; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:50.825. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.029. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:51.029. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:51.030. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 1; V_IN = 1001; RTS = 0; RTR = 0; KEY = 1; RESET = 1; R_BUTTON = 1}}
2015.01.23 18:50:51.030. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.030. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:51.031. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.049. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.049. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 0100; G_BUTTON = 1; RTS = 1; KEY = 1; RTR = 1; R_BUTTON = 1}}
2015.01.23 18:50:51.049. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.049. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:51.049. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 0100; G_BUTTON = 1; RTS = 1; KEY = 1; RTR = 1; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:51.103. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.318. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:51.318. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:51.319. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 0100; RTS = 1; RESET = 1; RTR = 1; KEY = 1; R_BUTTON = 1}}
2015.01.23 18:50:51.319. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.319. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:51.320. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.343. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.343. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 0; V_IN = 0000; G_BUTTON = 0; RTS = 0; KEY = 0; RTR = 1; R_BUTTON = 1}; transaction: {RESET = 1}}
2015.01.23 18:50:51.343. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.343. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:51.343. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 0000; G_BUTTON = 0; RTS = 0; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:51.404. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.603. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:51.603. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:51.603. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 0; V_IN = 0000; RTS = 0; RESET = 1; RTR = 1; KEY = 0; R_BUTTON = 1}}
2015.01.23 18:50:51.604. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.604. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:51.604. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.622. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.622. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 1; V_IN = 0000; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; R_BUTTON = 0}}
2015.01.23 18:50:51.622. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.622. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:51.622. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 1; V_IN = 0000; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:51.673. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.875. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:51.875. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:51.876. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 1; G_BUTTON = 1; V_IN = 0000; RTS = 0; RESET = 1; RTR = 1; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:51.877. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.877. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:51.877. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.895. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:51.895. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 0; START = 0; V_IN = 0000; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 0; R_BUTTON = 0}; transaction: {RESET = 1}}
2015.01.23 18:50:51.895. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:51.896. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:51.896. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 0000; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:51.948. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:52.145. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:52.145. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:52.146. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 0000; RTS = 0; RTR = 0; KEY = 1; RESET = 1; R_BUTTON = 0}}
2015.01.23 18:50:52.146. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.146. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:52.146. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.165. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:52.166. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 1; START = 0; V_IN = 1010; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 0; R_BUTTON = 1}; transaction: {RESET = 1}}
2015.01.23 18:50:52.166. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.166. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:52.166. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 0; V_IN = 1010; G_BUTTON = 0; RTS = 1; KEY = 0; RTR = 0; RESET = 1; R_BUTTON = 1}
2015.01.23 18:50:52.224. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:52.422. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:52.422. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:52.423. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 0; G_BUTTON = 0; V_IN = 1010; RTS = 1; RTR = 0; KEY = 0; RESET = 1; R_BUTTON = 1}}
2015.01.23 18:50:52.423. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.423. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:52.424. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.446. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:52.446. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 1}; transaction: {TEST = 0; START = 0; V_IN = 0111; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 0; R_BUTTON = 0}}
2015.01.23 18:50:52.446. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.447. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:52.447. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 0111; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 0; RESET = 1; R_BUTTON = 0}
2015.01.23 18:50:52.497. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); guarded action: {{}: {predicate: (AND (EQ RESET 1) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[STATO] := 0}; assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[SIGN] := 0000}; assignment: {[LAST_G] := 0}; assignment: {[LAST_R] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[V_OUT] := 0000}}}}}
2015.01.23 18:50:52.692. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
2015.01.23 18:50:52.692. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:52.693. INFO: EFSM simulator.WORK.B10(BEHAV)_0: resetting EFSM
2015.01.23 18:50:52.695. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 0111; RTS = 0; RESET = 1; RTR = 0; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:52.695. INFO: FATE: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.695. INFO: FATE: starting a new sequence (21 of 6)
2015.01.23 18:50:52.696. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:52.696. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random sequence
2015.01.23 18:50:52.696. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.716. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ TEST 0)) (AND (OR (EQ TEST 1) (EQ TEST 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[SIGN] := 0000}; assignment: {[STATO] := 9}}}}}
2015.01.23 18:50:52.716. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 0; RESET = 0}; transaction: {START = 0; V_IN = 1001; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; R_BUTTON = 0}}
2015.01.23 18:50:52.716. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
2015.01.23 18:50:52.717. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:52.717. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 0; V_IN = 1001; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; RESET = 0; R_BUTTON = 0}
2015.01.23 18:50:52.772. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0)); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ TEST 0)) (AND (OR (EQ TEST 1) (EQ TEST 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[VOTO0] := 0}; assignment: {[VOTO1] := 0}; assignment: {[VOTO2] := 0}; assignment: {[VOTO3] := 0}; assignment: {[CTS] := 0}; assignment: {[CTR] := 0}; assignment: {[SIGN] := 0000}; assignment: {[STATO] := 9}}}}}
2015.01.23 18:50:52.916. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9)))
2015.01.23 18:50:52.916. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:52.917. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 0; G_BUTTON = 1; V_IN = 1001; RTS = 0; RESET = 0; RTR = 1; KEY = 0; R_BUTTON = 0}}
2015.01.23 18:50:52.917. INFO: FATE: current coverage: 3% (2 of 66 transitions)
2015.01.23 18:50:52.917. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:52.918. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 3% (2 of 66 transitions)
2015.01.23 18:50:52.937. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (AND (AND (AND (EQ (BVEXTRACT 0 0 V_IN) 1) (EQ (BVEXTRACT 1 1 V_IN) 1)) (EQ (BVEXTRACT 2 2 V_IN) 1)) (EQ (BVEXTRACT 3 3 V_IN) 1))) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0] := (BVEXTRACT 0 0 V_IN)}; assignment: {[VOTO1] := (BVEXTRACT 1 1 V_IN)}; assignment: {[VOTO2] := (BVEXTRACT 2 2 V_IN)}; assignment: {[VOTO3] := (BVEXTRACT 3 3 V_IN)}; assignment: {[SIGN] := 1000}; assignment: {[STATO] := 10}}}}}
2015.01.23 18:50:52.937. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {V_IN = 1111; RESET = 0}; transaction: {TEST = 0; START = 1; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 1; R_BUTTON = 1}}
2015.01.23 18:50:52.937. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 3% (2 of 66 transitions)
2015.01.23 18:50:52.937. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:52.937. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 1; V_IN = 1111; G_BUTTON = 1; RTS = 0; KEY = 1; RTR = 1; RESET = 0; R_BUTTON = 1}
2015.01.23 18:50:52.997. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (EQ STATO 9))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (AND (AND (AND (EQ (BVEXTRACT 0 0 V_IN) 1) (EQ (BVEXTRACT 1 1 V_IN) 1)) (EQ (BVEXTRACT 2 2 V_IN) 1)) (EQ (BVEXTRACT 3 3 V_IN) 1))) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0] := (BVEXTRACT 0 0 V_IN)}; assignment: {[VOTO1] := (BVEXTRACT 1 1 V_IN)}; assignment: {[VOTO2] := (BVEXTRACT 2 2 V_IN)}; assignment: {[VOTO3] := (BVEXTRACT 3 3 V_IN)}; assignment: {[SIGN] := 1000}; assignment: {[STATO] := 10}}}}}
2015.01.23 18:50:53.110. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10)))
2015.01.23 18:50:53.110. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:53.111. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 0; START = 1; V_IN = 1111; G_BUTTON = 1; RTS = 0; RESET = 0; RTR = 1; KEY = 1; R_BUTTON = 1}}
2015.01.23 18:50:53.111. INFO: FATE: current coverage: 5% (3 of 66 transitions)
2015.01.23 18:50:53.111. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:53.111. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 5% (3 of 66 transitions)
2015.01.23 18:50:53.129. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{}: {predicate: (AND (NOT (EQ RESET 1)) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0__retrascope_33] := (BVXOR 1 (BVEXTRACT 0 0 SIGN))}; assignment: {[VOTO0__retrascope_34] := (BVXOR 0 (BVEXTRACT 1 1 SIGN))}; assignment: {[VOTO0__retrascope_35] := (BVXOR 0 (BVEXTRACT 2 2 SIGN))}; assignment: {[VOTO0] := (BVXOR 1 (BVEXTRACT 3 3 SIGN))}; assignment: {[STATO] := 4}}}}}
2015.01.23 18:50:53.129. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {RESET = 0}; transaction: {TEST = 1; START = 1; V_IN = 0100; G_BUTTON = 1; RTS = 1; KEY = 0; RTR = 0; R_BUTTON = 1}}
2015.01.23 18:50:53.129. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 5% (3 of 66 transitions)
2015.01.23 18:50:53.129. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:53.130. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 1; START = 1; V_IN = 0100; G_BUTTON = 1; RTS = 1; KEY = 0; RTR = 0; RESET = 0; R_BUTTON = 1}
2015.01.23 18:50:53.166. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (NOT (EQ STATO 5))) (NOT (EQ STATO 6))) (NOT (EQ STATO 7))) (NOT (EQ STATO 8))) (NOT (EQ STATO 9))) (EQ STATO 10))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); guarded action: {{}: {predicate: (AND (NOT (EQ RESET 1)) (OR (EQ RESET 1) (EQ RESET 0)))}->{{assignment: {[VOTO0__retrascope_33] := (BVXOR 1 (BVEXTRACT 0 0 SIGN))}; assignment: {[VOTO0__retrascope_34] := (BVXOR 0 (BVEXTRACT 1 1 SIGN))}; assignment: {[VOTO0__retrascope_35] := (BVXOR 0 (BVEXTRACT 2 2 SIGN))}; assignment: {[VOTO0] := (BVXOR 1 (BVEXTRACT 3 3 SIGN))}; assignment: {[STATO] := 4}}}}}
2015.01.23 18:50:53.265. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing has been finished successfully. New state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4)))
2015.01.23 18:50:53.265. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
2015.01.23 18:50:53.266. INFO: FATE: the vector has been generated successfully: {events: {}; transaction: {TEST = 1; START = 1; G_BUTTON = 1; V_IN = 0100; RTS = 1; RESET = 0; RTR = 0; KEY = 0; R_BUTTON = 1}}
2015.01.23 18:50:53.266. INFO: FATE: current coverage: 6% (4 of 66 transitions)
2015.01.23 18:50:53.266. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
2015.01.23 18:50:53.267. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random input vector. Current coverage: 6% (4 of 66 transitions)
2015.01.23 18:50:53.285. INFO: FATE.WORK.B10(BEHAV)_0: the transition has been traversed successfully: {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ RTR 1) (NOT (AND (AND (AND (EQ VOTO0 0) (EQ VOTO1 1)) (EQ VOTO2 1)) (EQ VOTO3 0)))) (AND (OR (EQ VOTO2 1) (EQ VOTO2 0)) (OR (EQ VOTO3 1) (EQ VOTO3 0)) (OR (EQ VOTO0 1) (EQ VOTO0 0)) (OR (EQ VOTO1 1) (EQ VOTO1 0)) (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[BLOCK_V_OUT_0] := VOTO0}; assignment: {[BLOCK_V_OUT_1] := VOTO1}; assignment: {[BLOCK_V_OUT_2] := VOTO2}; assignment: {[BLOCK_V_OUT_3] := VOTO3}; assignment: {[BLOCK_CTS_4] := 1}; assignment: {[V_OUT] := BLOCK_V_OUT_0}; assignment: {[V_OUT] := BLOCK_V_OUT_1}; assignment: {[V_OUT] := BLOCK_V_OUT_2}; assignment: {[V_OUT] := BLOCK_V_OUT_3}; assignment: {[CTS] := BLOCK_CTS_4}; assignment: {[STATO] := 5}}}}}
2015.01.23 18:50:53.285. INFO: FATE.WORK.B10(BEHAV)_0: input vector: {events: {}; transaction: {TEST = 0; START = 1; V_IN = 1110; G_BUTTON = 1; RTS = 0; KEY = 0; R_BUTTON = 0}; transaction: {RESET = 0; RTR = 1}}
2015.01.23 18:50:53.285. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 6% (4 of 66 transitions)
2015.01.23 18:50:53.286. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
2015.01.23 18:50:53.286. INFO: EFSM simulator.WORK.B10(BEHAV)_0: input dump: {TEST = 0; START = 1; V_IN = 1110; G_BUTTON = 1; RTS = 0; KEY = 0; RTR = 1; RESET = 0; R_BUTTON = 0}
2015.01.23 18:50:53.361. INFO: EFSM simulator.WORK.B10(BEHAV)_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{}: {predicate: (AND (AND (NOT (EQ RESET 1)) (EQ RTR 1) (NOT (AND (AND (AND (EQ VOTO0 0) (EQ VOTO1 1)) (EQ VOTO2 1)) (EQ VOTO3 0)))) (AND (OR (EQ VOTO2 1) (EQ VOTO2 0)) (OR (EQ VOTO3 1) (EQ VOTO3 0)) (OR (EQ VOTO0 1) (EQ VOTO0 0)) (OR (EQ VOTO1 1) (EQ VOTO1 0)) (OR (EQ RTR 1) (EQ RTR 0)) (OR (EQ RESET 1) (EQ RESET 0))))}->{{assignment: {[BLOCK_V_OUT_0] := VOTO0}; assignment: {[BLOCK_V_OUT_1] := VOTO1}; assignment: {[BLOCK_V_OUT_2] := VOTO2}; assignment: {[BLOCK_V_OUT_3] := VOTO3}; assignment: {[BLOCK_CTS_4] := 1}; assignment: {[V_OUT] := BLOCK_V_OUT_0}; assignment: {[V_OUT] := BLOCK_V_OUT_1}; assignment: {[V_OUT] := BLOCK_V_OUT_2}; assignment: {[V_OUT] := BLOCK_V_OUT_3}; assignment: {[CTS] := BLOCK_CTS_4}; assignment: {[STATO] := 5}}}}}
2015.01.23 18:50:53.487. ERROR: The exception has been encountered: java.lang.RuntimeException: Failed to resolve the assignment constraint: [line 2 column 32: invalid function application, sort mismatch on argument at position 2, (declare-const assignmentResult (_ BitVec 4))
(assert  (= assignmentResult #b0))
(check-sat)
(get-value ( assignmentResult))
(get-model)
(exit)
]
	at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.executeAssignment(EfsmSimulator.java:567)
	at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.executeAction(EfsmSimulator.java:477)
	at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.processEvents(EfsmSimulator.java:330)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmAtomicFateTestGenerator.tryToTraverseTransition(EfsmAtomicFateTestGenerator.java:559)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmAtomicFateTestGenerator.generateInputVectorRandomly(EfsmAtomicFateTestGenerator.java:239)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.RandomFateSequenceIterator.next(RandomFateSequenceIterator.java:47)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.RandomFateSequenceIterator.next(RandomFateSequenceIterator.java:27)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGenerator.start(EfsmFateTestGenerator.java:246)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGenerator.start(EfsmFateTestGenerator.java:55)
	at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
	at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
	at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
	at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:114)
	at ru.ispras.retrascope.Retrascope.main(Retrascope.java:329)
	at ru.ispras.retrascope.Retrascope.main(Retrascope.java:350)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:606)
	at com.intellij.rt.execution.application.AppMain.main(AppMain.java:134)

2015.01.23 18:50:53.488. INFO: Retrascope is shutting down
Exception in thread "main" java.lang.RuntimeException: Failed to resolve the assignment constraint: [line 2 column 32: invalid function application, sort mismatch on argument at position 2, (declare-const assignmentResult (_ BitVec 4))
(assert  (= assignmentResult #b0))
(check-sat)
(get-value ( assignmentResult))
(get-model)
(exit)
]
	at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.executeAssignment(EfsmSimulator.java:567)
	at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.executeAction(EfsmSimulator.java:477)
	at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.processEvents(EfsmSimulator.java:330)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmAtomicFateTestGenerator.tryToTraverseTransition(EfsmAtomicFateTestGenerator.java:559)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmAtomicFateTestGenerator.generateInputVectorRandomly(EfsmAtomicFateTestGenerator.java:239)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.RandomFateSequenceIterator.next(RandomFateSequenceIterator.java:47)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.RandomFateSequenceIterator.next(RandomFateSequenceIterator.java:27)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGenerator.start(EfsmFateTestGenerator.java:246)
	at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGenerator.start(EfsmFateTestGenerator.java:55)
	at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
	at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
	at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
	at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:114)
	at ru.ispras.retrascope.Retrascope.main(Retrascope.java:329)
	at ru.ispras.retrascope.Retrascope.main(Retrascope.java:350)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:606)
	at com.intellij.rt.execution.application.AppMain.main(AppMain.java:134)