b10-fate.txt - Retrascope - Open-Source Projects

Bug #5572 » b10-fate.txt

Sergey Smolov, 01/23/2015 06:55 PM

       /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
 .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}
 .01.23 18:50:30.225. INFO: Number of GADD paths: 33
 .01.23 18:50:30.226. INFO: ======================================
 .01.23 18:50:30.226. INFO: Clock-like variables: [RESET, CLOCK]
 .01.23 18:50:30.226. INFO: Transforming the process of module: WORK.B10(BEHAV)
 .01.23 18:50:30.478. INFO: 11 states are extracted.
 .01.23 18:50:30.478. INFO: The state-like variables are: [STATO]
 .01.23 18:50:45.334. INFO: 66 transitions are extracted.
       Storing: efsm
 .01.23 18:50:45.334. INFO: 1 EFSM(s) are extracted.
       Running: efsm-fate-test-generator
 .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}
 .01.23 18:50:45.335. INFO: FATE: sequences number isn't specified. Setting it to the default value: 6
 .01.23 18:50:45.346. INFO: EFSM simulator.WORK.B10(BEHAV)_0: resetting EFSM
 .01.23 18:50:45.346. INFO: FATE.WORK.B10(BEHAV)_0: detecting control dependencies
 .01.23 18:50:45.588. INFO: FATE.WORK.B10(BEHAV)_0: control dependencies have been processed successfully
 .01.23 18:50:45.588. INFO: FATE.WORK.B10(BEHAV)_0: detecting data dependencies
 .01.23 18:50:45.934. INFO: FATE.WORK.B10(BEHAV)_0: data dependencies have been processed successfully
 .01.23 18:50:45.934. INFO: FATE.WORK.B10(BEHAV)_0: detecting counters
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .01.23 18:50:46.174. INFO: FATE.WORK.B10(BEHAV)_0: counters have been processed successfully
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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))))}->{{}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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))))}->{{}}}}
 .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}}}}}
 .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))))}->{{}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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))))}->{{}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .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))))}->{{}}}}
 .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}}}}}
 .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}}}}}
 .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}}}}}
 .01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (EQ STATO 0))
 .01.23 18:50:46.180. INFO: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (NOT (EQ STATO 0)) (EQ STATO 1)))
 .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)))
 .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)))
 .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)))
 .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)))
 .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)))
 .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)))
 .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)))
 .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)))
 .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)))
 .01.23 18:50:46.181. INFO: FATE: starting a new sequence (01 of 6)
 .01.23 18:50:46.181. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .01.23 18:50:46.181. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random sequence
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:46.207. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 0% (0 of 66 transitions)
 .01.23 18:50:46.208. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:46.464. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:46.466. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:46.466. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:46.486. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:46.486. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:46.750. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:46.750. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:46.750. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:46.773. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:46.773. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:47.046. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:47.046. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:47.046. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:47.064. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:47.064. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:47.636. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:47.637. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:47.638. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:47.656. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:47.657. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:47.992. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:47.992. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:47.992. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:48.010. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.010. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:48.272. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:48.273. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.273. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:48.292. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.292. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:48.548. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:48.549. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.549. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:48.568. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.569. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:48.829. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:48.830. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.830. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:48.854. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:48.854. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:49.097. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:49.098. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.098. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:49.118. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.119. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:49.386. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:49.387. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.387. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:49.407. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.407. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:49.643. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .01.23 18:50:49.644. INFO: EFSM simulator.WORK.B10(BEHAV)_0: resetting EFSM
 .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}}
 .01.23 18:50:49.645. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.645. INFO: FATE: starting a new sequence (11 of 6)
 .01.23 18:50:49.646. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .01.23 18:50:49.646. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random sequence
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:49.664. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.665. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:49.923. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:49.924. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.925. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:49.943. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:49.944. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:50.197. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:50.198. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:50.199. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:50.218. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:50.218. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:50.483. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:50.484. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:50.484. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:50.504. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:50.504. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:50.750. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:50.751. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:50.751. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:50.769. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:50.770. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:51.029. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:51.030. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.030. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:51.049. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.049. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:51.318. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:51.319. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.319. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:51.343. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.343. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:51.603. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:51.604. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.604. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:51.622. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.622. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:51.875. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:51.877. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.877. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:51.895. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:51.896. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:52.145. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:52.146. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:52.146. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:52.166. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:52.166. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:52.422. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:52.423. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:52.423. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:52.446. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:52.447. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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))
 .01.23 18:50:52.692. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .01.23 18:50:52.693. INFO: EFSM simulator.WORK.B10(BEHAV)_0: resetting EFSM
 .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}}
 .01.23 18:50:52.695. INFO: FATE: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:52.695. INFO: FATE: starting a new sequence (21 of 6)
 .01.23 18:50:52.696. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .01.23 18:50:52.696. INFO: FATE.WORK.B10(BEHAV)_0: generating a new random sequence
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:52.716. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 2% (1 of 66 transitions)
 .01.23 18:50:52.717. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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)))
 .01.23 18:50:52.916. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:52.917. INFO: FATE: current coverage: 3% (2 of 66 transitions)
 .01.23 18:50:52.917. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:52.937. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 3% (2 of 66 transitions)
 .01.23 18:50:52.937. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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)))
 .01.23 18:50:53.110. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:53.111. INFO: FATE: current coverage: 5% (3 of 66 transitions)
 .01.23 18:50:53.111. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:53.129. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 5% (3 of 66 transitions)
 .01.23 18:50:53.129. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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)))
 .01.23 18:50:53.265. INFO: EFSM simulator.WORK.B10(BEHAV)_0: output dump: {CTR = 0; V_OUT = 0000; CTS = 0}
 .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}}
 .01.23 18:50:53.266. INFO: FATE: current coverage: 6% (4 of 66 transitions)
 .01.23 18:50:53.266. INFO: FATE: processing the EFSM WORK.B10(BEHAV)_0
 .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)
 .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}}}}}
 .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}}
 .01.23 18:50:53.285. INFO: FATE.WORK.B10(BEHAV)_0: current coverage: 6% (4 of 66 transitions)
 .01.23 18:50:53.286. INFO: EFSM simulator.WORK.B10(BEHAV)_0: processing the events: {}
 .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}
 .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}}}}}
 .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)
 .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)

(1-1/1)

Project

General

Profile

Retrascope

Bug #5572 » b10-fate.txt