Index: /cegar_dev/cegar/abstract_model/Concret_Main.v =================================================================== --- /cegar_dev/cegar/abstract_model/Concret_Main.v (revision 4) +++ /cegar_dev/cegar/abstract_model/Concret_Main.v (revision 4) @@ -0,0 +1,14 @@ + +module main(clk); + +input clk; +input i1; +output o1; +output o2; +output r_i1; + +machine_concret machine_concret1(clk, i1, o1, o2, r_i1); + +endmodule + +`include machine_concret.v Index: /cegar_dev/cegar/abstract_model/Phi_1_and_Phi_2 =================================================================== --- /cegar_dev/cegar/abstract_model/Phi_1_and_Phi_2 (revision 4) +++ /cegar_dev/cegar/abstract_model/Phi_1_and_Phi_2 (revision 4) @@ -0,0 +1,3 @@ +(r_i1 = 0) + AF (o1 = 1); +(r_i1 = 0) + AF (o2 = 1); +(o1=0)*(o2=0); Index: /cegar_dev/cegar/abstract_model/SATcnf_a1.cnf =================================================================== --- /cegar_dev/cegar/abstract_model/SATcnf_a1.cnf (revision 4) +++ /cegar_dev/cegar/abstract_model/SATcnf_a1.cnf (revision 4) @@ -0,0 +1,346 @@ +c Nd85_1296_0 68 +c Nd156_564_-1 5 +c machine_concret1_a1.state_2_0 58 +c Nd180_193_-1 16 +c o1_0_0 1 +c Nd733_2976_-1 12 +c Nd72_805_-1 47 +c Nd85_1260_0 63 +c Nd145_624_-1 27 +c Nd61_829_-1 32 +c Nd145_672_-1 44 +c Nd145_768_-1 19 +c Nd168_745_-1 98 +c Nd120_133_0 71 +c Nd733_1728_-1 31 +c Nd97_1248_0 64 +c machine_concret1_a1.state$raw_na$initial$_nb_3_-1 10 +c Nd709_3576_-1 2 +c machine_concret1_a1.state$raw_na$initial$_nb_2_-1 8 +c Nd49_781_-1 17 +c Nd685_4320_-1 43 +c Nd96_1320_0 80 +c Nd156_756_-1 20 +c Nd168_600_-1 29 +c Nd168_744_-1 21 +c machine_concret1_a1.state_1_0 56 +c Nd805_985_-1 92 +c Nd85_1500_0 76 +c Nd180_192_-1 22 +c Nd709_2664_-1 46 +c machine_concret1_a1.nd_r_i1_0_-1 48 +c r_i1_0_0 38 +c Nd120_132_0 82 +c Nd121_132_0 66 +c Nd697_901_-1 96 +c Nd108_1116_0 70 +c Nd145_696_-1 3 +c Nd157_564_-1 41 +c machine_concret1_a1.state$raw_na$initial$_nb_4_-1 11 +c machine_concret1_a1.state$raw_na$initial$_nb_1_-1 6 +c Nd157_888_-1 97 +c machine_concret1_a1.state_0_0 54 +c Nd169_600_-1 50 +c Nd157_612_-1 28 +c Nd84_1080_0 84 +c Nd85_1452_0 73 +c Nd121_133_0 59 +c Nd168_552_-1 7 +c Nd169_744_-1 35 +c Nd108_1164_0 81 +c Nd96_1212_0 74 +c Nd168_648_-1 15 +c machine_concret1_a1.state_4_0 61 +c Nd145_973_-1 93 +c Nd85_1524_0 79 +c Nd108_1068_0 65 +c Nd637_3600_-1 26 +c Nd145_576_-1 40 +c Nd181_193_-1 9 +c Nd589_5616_-1 39 +c Nd85_1224_0 53 +c Nd637_4956_-1 42 +c Nd145_720_-1 13 +c Nd721_924_-1 95 +c Nd108_1020_0 57 +c Nd829_996_-1 91 +c Nd97_1284_0 69 +c machine_concret1_a1.nd_o1_0_-1 18 +c machine_concret1_a1.state_3_0 60 +c Nd769_948_-1 94 +c machine_concret1_a1.state$raw_na$initial$_nb_0_-1 4 +c Nd144_816_-1 34 +c Nd84_108_0 90 +c Nd109_1164_0 88 +c Nd96_1284_0 77 +c Nd181_192_-1 30 +c o2_0_0 25 +c machine_concret1_a1.nd_o2_0_-1 33 +c Nd144_792_-1 49 +c Nd97_1212_0 55 +c Nd156_660_-1 14 +c Nd84_1176_0 87 +c Nd109_1068_0 85 +c Nd157_660_-1 45 +p cnf 99 261 +10 11 9 0 +-10 -9 0 +-11 -9 0 +-8 -9 7 0 +8 -7 0 +9 -7 0 +-6 -7 5 0 +6 -5 0 +7 -5 0 +4 -5 3 0 +-4 -3 0 +5 -3 0 +-10 11 16 0 +10 -16 0 +-11 -16 0 +-8 -16 15 0 +8 -15 0 +16 -15 0 +-6 -15 14 0 +6 -14 0 +15 -14 0 +4 -14 13 0 +-4 -13 0 +14 -13 0 +-10 -11 22 0 +10 -22 0 +11 -22 0 +-8 -22 21 0 +8 -21 0 +22 -21 0 +-6 -21 20 0 +6 -20 0 +21 -20 0 +4 -20 19 0 +-4 -19 0 +20 -19 0 +18 19 17 0 +-18 -17 0 +-19 -17 0 +13 -17 12 0 +-13 -12 0 +17 -12 0 +3 -12 2 0 +-3 -2 0 +12 -2 0 +1 -2 23 0 +-1 -23 0 +2 -23 0 +-1 2 24 0 +1 -24 0 +-2 -24 0 +23 24 0 +10 -11 30 0 +-10 -30 0 +11 -30 0 +-8 -30 29 0 +8 -29 0 +30 -29 0 +6 -29 28 0 +-6 -28 0 +29 -28 0 +4 -28 27 0 +-4 -27 0 +28 -27 0 +8 -22 35 0 +-8 -35 0 +22 -35 0 +-4 -35 34 0 +4 -34 0 +35 -34 0 +33 34 32 0 +-33 -32 0 +-34 -32 0 +13 -32 31 0 +-13 -31 0 +32 -31 0 +27 -31 26 0 +-27 -26 0 +31 -26 0 +25 -26 36 0 +-25 -36 0 +26 -36 0 +-25 26 37 0 +25 -37 0 +-26 -37 0 +36 37 0 +6 -7 41 0 +-6 -41 0 +7 -41 0 +4 -41 40 0 +-4 -40 0 +41 -40 0 +6 -15 45 0 +-6 -45 0 +15 -45 0 +4 -45 44 0 +-4 -44 0 +45 -44 0 +8 -30 50 0 +-8 -50 0 +30 -50 0 +-4 -50 49 0 +4 -49 0 +50 -49 0 +-48 49 47 0 +48 -47 0 +-49 -47 0 +3 -47 46 0 +-3 -46 0 +47 -46 0 +44 -46 43 0 +-44 -43 0 +46 -43 0 +27 -43 42 0 +-27 -42 0 +43 -42 0 +40 -42 39 0 +-40 -39 0 +42 -39 0 +38 39 51 0 +-38 -51 0 +-39 -51 0 +-38 -39 52 0 +38 -52 0 +39 -52 0 +51 52 0 +60 61 59 0 +-60 -59 0 +-61 -59 0 +-58 -59 57 0 +58 -57 0 +59 -57 0 +56 -57 55 0 +-56 -55 0 +57 -55 0 +54 -55 53 0 +-54 -53 0 +55 -53 0 +-53 -40 62 0 +53 -62 0 +40 -62 0 +60 -61 66 0 +-60 -66 0 +61 -66 0 +-58 -66 65 0 +58 -65 0 +66 -65 0 +56 -65 64 0 +-56 -64 0 +65 -64 0 +54 -64 63 0 +-54 -63 0 +64 -63 0 +-63 -27 67 0 +63 -67 0 +27 -67 0 +-60 61 71 0 +60 -71 0 +-61 -71 0 +-58 -71 70 0 +58 -70 0 +71 -70 0 +56 -70 69 0 +-56 -69 0 +70 -69 0 +54 -69 68 0 +-54 -68 0 +69 -68 0 +-68 -44 72 0 +68 -72 0 +44 -72 0 +-56 -57 74 0 +56 -74 0 +57 -74 0 +54 -74 73 0 +-54 -73 0 +74 -73 0 +-73 -3 75 0 +73 -75 0 +3 -75 0 +-56 -70 77 0 +56 -77 0 +70 -77 0 +54 -77 76 0 +-54 -76 0 +77 -76 0 +-76 -13 78 0 +76 -78 0 +13 -78 0 +-60 -61 82 0 +60 -82 0 +61 -82 0 +-58 -82 81 0 +58 -81 0 +82 -81 0 +-56 -81 80 0 +56 -80 0 +81 -80 0 +54 -80 79 0 +-54 -79 0 +80 -79 0 +-79 -19 83 0 +79 -83 0 +19 -83 0 +58 -66 85 0 +-58 -85 0 +66 -85 0 +-54 -85 84 0 +54 -84 0 +85 -84 0 +-84 -49 86 0 +84 -86 0 +49 -86 0 +58 -82 88 0 +-58 -88 0 +82 -88 0 +-54 -88 87 0 +54 -87 0 +88 -87 0 +-87 -34 89 0 +87 -89 0 +34 -89 0 +-54 -58 90 0 +54 -90 0 +58 -90 0 +-8 22 98 0 +8 -98 0 +-22 -98 0 +6 -98 97 0 +-6 -97 0 +98 -97 0 +5 97 96 0 +-5 -96 0 +-97 -96 0 +14 -96 95 0 +-14 -95 0 +96 -95 0 +20 -95 94 0 +-20 -94 0 +95 -94 0 +4 94 93 0 +-4 -93 0 +-94 -93 0 +49 93 92 0 +-49 -92 0 +-93 -92 0 +34 -92 91 0 +-34 -91 0 +92 -91 0 +-90 -91 99 0 +90 -99 0 +91 -99 0 +62 67 72 75 78 83 86 89 99 0 +54 0 +-56 0 +58 0 +-60 0 +-61 0 +-1 0 +25 0 +38 0 Index: /cegar_dev/cegar/abstract_model/debug_trace_abs =================================================================== --- /cegar_dev/cegar/abstract_model/debug_trace_abs (revision 4) +++ /cegar_dev/cegar/abstract_model/debug_trace_abs (revision 4) @@ -0,0 +1,107 @@ +# MC: formula failed --- (o1=0 + AF(o2=1)) +# MC: Calling debugger for trace 1 +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_19 +o1:1 +o2:0 +r_i1:0 +fails (o1=0 + AF(o2=1)). + +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_19 +o1:1 +o2:0 +r_i1:0 +fails o1=0. + +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_19 +o1:1 +o2:0 +r_i1:0 +fails AF(o2=1) + +--A fair path on which o2=1 is always false: + --Counter example begins +--Fair path stem: +--State 0: +machine_concret1_a1.state:machine_concret1_Abs1_STATE_19 +o1:1 +o2:0 +r_i1:0 + +--Goes to state 1: +machine_concret1_a1.state:machine_concret1_Abs1_STATE_20 +--On input: +machine_concret1_a1.nd_aff0:1 +machine_concret1_a1.nd_aff1:0 +machine_concret1_a1.nd_o1:1 +machine_concret1_a1.nd_o2:0 +machine_concret1_a1.nd_r_i1:0 +machine_concret1_a1.state$raw_na$initial$_nb:machine_concret1_Abs1_STATE_25 + +--Goes to state 2: +machine_concret1_a1.state:machine_concret1_Abs1_STATE_13 +--On input: + + +--Fair path cycle: +--State 0: +machine_concret1_a1.state:machine_concret1_Abs1_STATE_13 +o1:1 +o2:0 +r_i1:0 + +--Goes to state 1: + +--On input: +machine_concret1_a1.nd_aff0:1 +machine_concret1_a1.nd_aff1:0 +machine_concret1_a1.nd_o1:1 +machine_concret1_a1.nd_o2:0 +machine_concret1_a1.nd_r_i1:0 +machine_concret1_a1.state$raw_na$initial$_nb:machine_concret1_Abs1_STATE_25 + + + --Counter example ends + +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_19 +o1:1 +o2:0 +r_i1:0 +fails o2=1. + +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_20 +o1:1 +o2:0 +r_i1:0 +fails o2=1. + +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_13 +o1:1 +o2:0 +r_i1:0 +fails o2=1. + + +# MC: formula failed --- AG(o2=0) +# MC: Calling debugger for trace 1 +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_25 +o1:0 +o2:1 +r_i1:0 +fails AG(o2=0) + +since o2=0 is false at this state +--State +machine_concret1_a1.state:machine_concret1_Abs1_STATE_25 +o1:0 +o2:1 +r_i1:0 +fails o2=0. + + Index: /cegar_dev/cegar/abstract_model/machine_concret.ctl =================================================================== --- /cegar_dev/cegar/abstract_model/machine_concret.ctl (revision 4) +++ /cegar_dev/cegar/abstract_model/machine_concret.ctl (revision 4) @@ -0,0 +1,27 @@ +# Phi_1 : +(r_i1 = 0) + AF (o1 = 1); +# Expected result : formula passed +#--------------------------------------------------------- +# Phi_2 : +(r_i1 = 0) + AF (o2 = 1); +# Expected result : formula passed +#--------------------------------------------------------- +# Propriéte globale : +(o1 = 0) + AF (o2 = 1); +# Expected result : formula passed +#--------------------------------------------------------- +A((o1 = 0) U((o1 = 1) * AF(o2 = 1))); +# Expected result : formula passed +#--------------------------------------------------------- +#A((o1 = 0) U((o1 = 1) * AG(o2 = 1))); +# Expected result : formula passed +#--------------------------------------------------------- +#(r_i1 = 0) + AF (((o1=1) *( o2 = 1))); +# Expected result : formula passed +#--------------------------------------------------------- +#(r_i1 = 0) + (AF(o1 = 1) * AF (o2 = 1)); +# Expected result : formula passed +#--------------------------------------------------------- +#AG (o2 = 0); +# Expected result : formula passed (Counter-example test) +#--------------------------------------------------------- Index: /cegar_dev/cegar/abstract_model/machine_concret.fair =================================================================== --- /cegar_dev/cegar/abstract_model/machine_concret.fair (revision 4) +++ /cegar_dev/cegar/abstract_model/machine_concret.fair (revision 4) @@ -0,0 +1,1 @@ +machine_concret1.m_state = S3; Index: /cegar_dev/cegar/abstract_model/machine_concret.v =================================================================== --- /cegar_dev/cegar/abstract_model/machine_concret.v (revision 4) +++ /cegar_dev/cegar/abstract_model/machine_concret.v (revision 4) @@ -0,0 +1,67 @@ +typedef enum {S0, S1, S2, S3} MState; + +module machine_concret (clk, i1, o1, o2, r_i1); + +input clk; +input i1; +output o1; +output o2; +output r_i1; + +MState reg m_state; +reg o1; +reg o2; +reg r_i1; + +initial + begin + m_state = S0; + o1 = 0; + o2 = 0; + r_i1 = i1; + end + +always @ (posedge clk) begin + + r_i1 = i1; + case (m_state) + S0: + if (i1==1) + begin + m_state = S1; + o1 = 1; + o2 = 0; + end + else + begin + o1 = 0; + o2 = 0; + m_state = S0; + end + + S1: + begin + m_state = S2; + o1 = 0; + o2 = 1; + end + + S2: + begin + m_state = S3; + o1 = 1; + o2 = 1; + end + + S3: + begin + o1 = 1; + o2 = 1; + m_state = S3; + end + + endcase + +end + +endmodule Index: /cegar_dev/cegar/abstract_model/machine_concret1_Abs1.v =================================================================== --- /cegar_dev/cegar/abstract_model/machine_concret1_Abs1.v (revision 4) +++ /cegar_dev/cegar/abstract_model/machine_concret1_Abs1.v (revision 4) @@ -0,0 +1,358 @@ +typedef enum{machine_concret1_Abs1_STATE_28,machine_concret1_Abs1_STATE_31,machine_concret1_Abs1_STATE_30,machine_concret1_Abs1_STATE_32,machine_concret1_Abs1_STATE_27,machine_concret1_Abs1_STATE_29,machine_concret1_Abs1_STATE_35,machine_concret1_Abs1_STATE_39,machine_concret1_Abs1_STATE_41,machine_concret1_Abs1_STATE_42,machine_concret1_Abs1_STATE_34,machine_concret1_Abs1_STATE_44,machine_concret1_Abs1_STATE_38,machine_concret1_Abs1_STATE_40,machine_concret1_Abs1_STATE_36,machine_concret1_Abs1_STATE_33,machine_concret1_Abs1_STATE_45,machine_concret1_Abs1_STATE_43,machine_concret1_Abs1_STATE_46,machine_concret1_Abs1_STATE_37} machine_concret1_Abs1_STATE; + +module machine_concret1_Abs1(clk,i1,o1,o2,r_i1); + +input clk; + +input i1; + + + +output r_i1; +output o1; +output o2; + + +reg r_i1; +reg o1; +reg o2; +machine_concret1_Abs1_STATE reg state; + + +wire nd_r_i1; +wire nd_o1; +wire nd_o2; +wire nd_aff0; +wire nd_aff1; + + +assign nd_r_i1 = $ND(0,1); +assign nd_o1 = $ND(0,1); +assign nd_o2 = $ND(0,1); +assign nd_aff0 = $ND(0,1); +assign nd_aff1 = $ND(0,1); + +initial +begin + + state = $ND(machine_concret1_Abs1_STATE_27,machine_concret1_Abs1_STATE_29,machine_concret1_Abs1_STATE_33,machine_concret1_Abs1_STATE_37); + if(state == machine_concret1_Abs1_STATE_27) + begin + r_i1 = 0; + o1 = 0; + o2 = 0; + end + else + begin + if(state == machine_concret1_Abs1_STATE_29) + begin + r_i1 = 0; + o1 = 0; + o2 = 0; + end + else + begin + if(state == machine_concret1_Abs1_STATE_33) + begin + r_i1 = 0; + o1 = 0; + o2 = 0; + end + else + begin + o1 = 0; + o2 = 0; + r_i1 = nd_r_i1; + end + end + end +end + +always @(posedge clk) +begin + + case(state) + machine_concret1_Abs1_STATE_28: + begin + state = machine_concret1_Abs1_STATE_28; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_31: + begin + state = machine_concret1_Abs1_STATE_31; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_30: + begin + state = machine_concret1_Abs1_STATE_31; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_32: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_30; + o2 = 1; + r_i1 = nd_r_i1; + o1 = nd_o1; + end + else + begin + state = machine_concret1_Abs1_STATE_32; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_27: + begin + state = machine_concret1_Abs1_STATE_28; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_29: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_30; + o2 = 1; + r_i1 = nd_r_i1; + o1 = nd_o1; + end + else + begin + state = machine_concret1_Abs1_STATE_32; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_35: + begin + state = machine_concret1_Abs1_STATE_35; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_39: + begin + state = machine_concret1_Abs1_STATE_39; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_41: + begin + state = machine_concret1_Abs1_STATE_39; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_42: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_41; + o2 = 1; + r_i1 = nd_r_i1; + o1 = nd_o1; + end + else + begin + state = machine_concret1_Abs1_STATE_42; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_34: + begin + state = machine_concret1_Abs1_STATE_35; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_44: + begin + state = machine_concret1_Abs1_STATE_39; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_38: + begin + state = machine_concret1_Abs1_STATE_39; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + machine_concret1_Abs1_STATE_40: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_41; + o2 = 1; + r_i1 = nd_r_i1; + o1 = nd_o1; + end + else + begin + state = machine_concret1_Abs1_STATE_42; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_36: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_34; + o1 = 1; + r_i1 = nd_r_i1; + o2 = nd_o2; + end + else + begin + state = machine_concret1_Abs1_STATE_36; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_33: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_34; + o1 = 1; + r_i1 = nd_r_i1; + o2 = nd_o2; + end + else + begin + state = machine_concret1_Abs1_STATE_36; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_45: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_44; + o1 = 1; + r_i1 = nd_r_i1; + o2 = nd_o2; + end + else + begin + state = machine_concret1_Abs1_STATE_45; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_43: + begin + if(nd_aff0 == 1) + begin + state = machine_concret1_Abs1_STATE_44; + o1 = 1; + r_i1 = nd_r_i1; + o2 = nd_o2; + end + else + begin + state = machine_concret1_Abs1_STATE_45; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + machine_concret1_Abs1_STATE_46: + begin + if(nd_aff0 == 1) + begin + if(nd_aff1 == 1) + begin + state = machine_concret1_Abs1_STATE_38; + o1 = 1; + o2 = 1; + r_i1 = nd_r_i1; + end + else + begin + state = machine_concret1_Abs1_STATE_40; + o1 = 1; + r_i1 = nd_r_i1; + o2 = nd_o2; + end + end + else + begin + if(nd_aff1 == 1) + begin + state = machine_concret1_Abs1_STATE_43; + o2 = 1; + r_i1 = nd_r_i1; + o1 = nd_o1; + end + else + begin + state = machine_concret1_Abs1_STATE_46; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + end + machine_concret1_Abs1_STATE_37: + begin + if(nd_aff0 == 1) + begin + if(nd_aff1 == 1) + begin + state = machine_concret1_Abs1_STATE_38; + o1 = 1; + o2 = 1; + r_i1 = nd_r_i1; + end + else + begin + state = machine_concret1_Abs1_STATE_40; + o1 = 1; + r_i1 = nd_r_i1; + o2 = nd_o2; + end + end + else + begin + if(nd_aff1 == 1) + begin + state = machine_concret1_Abs1_STATE_43; + o2 = 1; + r_i1 = nd_r_i1; + o1 = nd_o1; + end + else + begin + state = machine_concret1_Abs1_STATE_46; + r_i1 = nd_r_i1; + o1 = nd_o1; + o2 = nd_o2; + end + end + end + endcase +end + +endmodule Index: /cegar_dev/cegar/abstract_model/main_abstract.fair =================================================================== --- /cegar_dev/cegar/abstract_model/main_abstract.fair (revision 4) +++ /cegar_dev/cegar/abstract_model/main_abstract.fair (revision 4) @@ -0,0 +1,5 @@ +#machine_concret1.m_state = S3; +machine_concret1_a1.state = machine_concret1_Abs1_STATE_28 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_31 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_30 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_32 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_35 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_39 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_41 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_42; +machine_concret1_a1.state = machine_concret1_Abs1_STATE_28 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_35 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_34 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_36 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_31 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_39 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_44 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_45; +machine_concret1_a1.state = machine_concret1_Abs1_STATE_28 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_31 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_30 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_32 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_35 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_39 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_41 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_42 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_34 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_44 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_38 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_40 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_36 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_45 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_43 + machine_concret1_a1.state = machine_concret1_Abs1_STATE_46; + Index: /cegar_dev/cegar/abstract_model/main_abstract.mv =================================================================== --- /cegar_dev/cegar/abstract_model/main_abstract.mv (revision 4) +++ /cegar_dev/cegar/abstract_model/main_abstract.mv (revision 4) @@ -0,0 +1,1802 @@ +# vl2mv main_abstract.v +# version: 1.4 +# date: 18:29:55 09/16/2010 (CEST) +.model main_Abs +# I/O ports +.outputs o1 +.outputs o2 +.inputs i1 +.outputs r_i1 +.subckt machine_concret1_Abs1 machine_concret1_a1 i1=i1 o1=o1 o2=o2 r_i1=r_i1 +# conflict arbitrators +# non-blocking assignments +# latches +# quasi-continuous assignment +.end + + +.model machine_concret1_Abs1 +# I/O ports +.outputs o1 +.outputs o2 +.inputs i1 +.outputs r_i1 +.mv state 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +# assign nd_r_i1 = $ND ( 0,1 ) +.names nd_r_i1 +0 +1 +# assign nd_o1 = $ND ( 0,1 ) +.names nd_o1 +0 +1 +# assign nd_o2 = $ND ( 0,1 ) +.names nd_o2 +0 +1 +# assign nd_aff0 = $ND ( 0,1 ) +.names nd_aff0 +0 +1 +# assign nd_aff1 = $ND ( 0,1 ) +.names nd_aff1 +0 +1 +# state = $ND ( 4,5,15,19 ) +.mv state$raw_na 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.mv state$raw_na$initial$_nb 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$raw_na$initial$_nb +machine_concret1_Abs1_STATE_27 +machine_concret1_Abs1_STATE_29 +machine_concret1_Abs1_STATE_33 +machine_concret1_Abs1_STATE_37 +.names state$raw_na$initial$_nb state$raw_na +- =state$raw_na$initial$_nb +.mv _nd 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _nd +machine_concret1_Abs1_STATE_27 +# state == 4 +.names state$raw_na _nd _nc +.def 0 +- =state$raw_na 1 +.names _nc _ne +- =_nc +# r_i1 = 0 +.names r_i1$_nc_nf$true +0 +# o1 = 0 +.names o1$_nc_n10$true +0 +# o2 = 0 +.names o2$_nc_n11$true +0 +.mv _n13 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n13 +machine_concret1_Abs1_STATE_29 +# state == 5 +.names state$raw_na _n13 _n12 +.def 0 +- =state$raw_na 1 +.names _n12 _n14 +- =_n12 +# r_i1 = 0 +.names r_i1$_n12_n15$true +0 +# o1 = 0 +.names o1$_n12_n16$true +0 +# o2 = 0 +.names o2$_n12_n17$true +0 +.mv _n19 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n19 +machine_concret1_Abs1_STATE_33 +# state == 15 +.names state$raw_na _n19 _n18 +.def 0 +- =state$raw_na 1 +.names _n18 _n1a +- =_n18 +# r_i1 = 0 +.names r_i1$_n18_n1b$true +0 +# o1 = 0 +.names o1$_n18_n1c$true +0 +# o2 = 0 +.names o2$_n18_n1d$true +0 +# o1 = 0 +.names o1$_n18_n1e$false +0 +# o2 = 0 +.names o2$_n18_n1f$false +0 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n18_n20$false +- =nd_r_i1 +# if/else (state == 15) +.names o1$_n18_n1c$true o1$_n18_n1e$false _n18 o1$_n18$raw_n25 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n18_n1d$true o2$_n18_n1f$false _n18 o2$_n18$raw_n27 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n18_n1b$true r_i1$_n18_n20$false _n18 r_i1$_n18$raw_n29 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +# if/else (state == 5) +.names o1$_n12_n16$true o1$_n18$raw_n25 _n12 o1$_n12$raw_n38 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n12_n17$true o2$_n18$raw_n27 _n12 o2$_n12$raw_n3a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n12_n15$true r_i1$_n18$raw_n29 _n12 r_i1$_n12$raw_n3c +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +# if/else (state == 4) +.names o1$_nc_n10$true o1$_n12$raw_n38 _nc o1$_nc$raw_n4b +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nc_n11$true o2$_n12$raw_n3a _nc o2$_nc$raw_n4d +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nc_nf$true r_i1$_n12$raw_n3c _nc r_i1$_nc$raw_n4f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +# non-blocking assignments for initial +.mv _n5c 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n5c +machine_concret1_Abs1_STATE_28 +.names state _n5c _n5b +.def 0 +- =state 1 +.names _n5b _n5a +1 1 +0 0 +# state = 0 +.mv state$_n5a_n5d$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n5a_n5d$true +machine_concret1_Abs1_STATE_28 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n5a_n5e$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n5a_n5f$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n5a_n60$true +- =nd_o2 +.mv _n63 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n63 +machine_concret1_Abs1_STATE_31 +.names state _n63 _n62 +.def 0 +- =state 1 +.names _n62 _n61 +1 1 +0 0 +# state = 1 +.mv state$_n61_n64$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n61_n64$true +machine_concret1_Abs1_STATE_31 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n61_n65$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n61_n66$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n61_n67$true +- =nd_o2 +.mv _n6a 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n6a +machine_concret1_Abs1_STATE_30 +.names state _n6a _n69 +.def 0 +- =state 1 +.names _n69 _n68 +1 1 +0 0 +# state = 1 +.mv state$_n68_n6b$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n68_n6b$true +machine_concret1_Abs1_STATE_31 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n68_n6c$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n68_n6d$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n68_n6e$true +- =nd_o2 +.mv _n71 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n71 +machine_concret1_Abs1_STATE_32 +.names state _n71 _n70 +.def 0 +- =state 1 +.names _n70 _n6f +1 1 +0 0 +.names _n73 +1 +# nd_aff0 == 1 +.names nd_aff0 _n73 _n74 +.def 0 +0 1 1 +1 0 1 +.names _n74 _n72 +0 1 +1 0 +.names _n72 _n76 +- =_n72 +# state = 2 +.mv state$_n72_n77$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n72_n77$true +machine_concret1_Abs1_STATE_30 +# o2 = 1 +.names o2$_n72_n78$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n72_n79$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n72_n7a$true +- =nd_o1 +# state = 3 +.mv state$_n72_n7b$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n72_n7b$false +machine_concret1_Abs1_STATE_32 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n72_n7c$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n72_n7d$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n72_n7e$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n72_n7a$true o1$_n72_n7d$false _n72 o1$_n72$raw_n83 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n72_n78$true o2$_n72_n7e$false _n72 o2$_n72$raw_n85 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n72_n79$true r_i1$_n72_n7c$false _n72 r_i1$_n72$raw_n87 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n72$raw_n89 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n72_n77$true state$_n72_n7b$false _n72 state$_n72$raw_n89 +- - 0 =state$_n72_n7b$false +- - 1 =state$_n72_n77$true +.mv _n94 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n94 +machine_concret1_Abs1_STATE_27 +.names state _n94 _n93 +.def 0 +- =state 1 +.names _n93 _n92 +1 1 +0 0 +# state = 0 +.mv state$_n92_n95$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n92_n95$true +machine_concret1_Abs1_STATE_28 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n92_n96$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n92_n97$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n92_n98$true +- =nd_o2 +.mv _n9b 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n9b +machine_concret1_Abs1_STATE_29 +.names state _n9b _n9a +.def 0 +- =state 1 +.names _n9a _n99 +1 1 +0 0 +.names _n9d +1 +# nd_aff0 == 1 +.names nd_aff0 _n9d _n9e +.def 0 +0 1 1 +1 0 1 +.names _n9e _n9c +0 1 +1 0 +.names _n9c _na0 +- =_n9c +# state = 2 +.mv state$_n9c_na1$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n9c_na1$true +machine_concret1_Abs1_STATE_30 +# o2 = 1 +.names o2$_n9c_na2$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n9c_na3$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n9c_na4$true +- =nd_o1 +# state = 3 +.mv state$_n9c_na5$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n9c_na5$false +machine_concret1_Abs1_STATE_32 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n9c_na6$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n9c_na7$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n9c_na8$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n9c_na4$true o1$_n9c_na7$false _n9c o1$_n9c$raw_nad +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n9c_na2$true o2$_n9c_na8$false _n9c o2$_n9c$raw_naf +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n9c_na3$true r_i1$_n9c_na6$false _n9c r_i1$_n9c$raw_nb1 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n9c$raw_nb3 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n9c_na1$true state$_n9c_na5$false _n9c state$_n9c$raw_nb3 +- - 0 =state$_n9c_na5$false +- - 1 =state$_n9c_na1$true +.mv _nbe 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _nbe +machine_concret1_Abs1_STATE_35 +.names state _nbe _nbd +.def 0 +- =state 1 +.names _nbd _nbc +1 1 +0 0 +# state = 6 +.mv state$_nbc_nbf$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nbc_nbf$true +machine_concret1_Abs1_STATE_35 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nbc_nc0$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nbc_nc1$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_nbc_nc2$true +- =nd_o2 +.mv _nc5 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _nc5 +machine_concret1_Abs1_STATE_39 +.names state _nc5 _nc4 +.def 0 +- =state 1 +.names _nc4 _nc3 +1 1 +0 0 +# state = 7 +.mv state$_nc3_nc6$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nc3_nc6$true +machine_concret1_Abs1_STATE_39 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nc3_nc7$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nc3_nc8$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_nc3_nc9$true +- =nd_o2 +.mv _ncc 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _ncc +machine_concret1_Abs1_STATE_41 +.names state _ncc _ncb +.def 0 +- =state 1 +.names _ncb _nca +1 1 +0 0 +# state = 7 +.mv state$_nca_ncd$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nca_ncd$true +machine_concret1_Abs1_STATE_39 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nca_nce$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nca_ncf$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_nca_nd0$true +- =nd_o2 +.mv _nd3 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _nd3 +machine_concret1_Abs1_STATE_42 +.names state _nd3 _nd2 +.def 0 +- =state 1 +.names _nd2 _nd1 +1 1 +0 0 +.names _nd5 +1 +# nd_aff0 == 1 +.names nd_aff0 _nd5 _nd6 +.def 0 +0 1 1 +1 0 1 +.names _nd6 _nd4 +0 1 +1 0 +.names _nd4 _nd8 +- =_nd4 +# state = 8 +.mv state$_nd4_nd9$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nd4_nd9$true +machine_concret1_Abs1_STATE_41 +# o2 = 1 +.names o2$_nd4_nda$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nd4_ndb$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nd4_ndc$true +- =nd_o1 +# state = 9 +.mv state$_nd4_ndd$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nd4_ndd$false +machine_concret1_Abs1_STATE_42 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nd4_nde$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nd4_ndf$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_nd4_ne0$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_nd4_ndc$true o1$_nd4_ndf$false _nd4 o1$_nd4$raw_ne5 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nd4_nda$true o2$_nd4_ne0$false _nd4 o2$_nd4$raw_ne7 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nd4_ndb$true r_i1$_nd4_nde$false _nd4 r_i1$_nd4$raw_ne9 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nd4$raw_neb 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nd4_nd9$true state$_nd4_ndd$false _nd4 state$_nd4$raw_neb +- - 0 =state$_nd4_ndd$false +- - 1 =state$_nd4_nd9$true +.mv _nf6 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _nf6 +machine_concret1_Abs1_STATE_34 +.names state _nf6 _nf5 +.def 0 +- =state 1 +.names _nf5 _nf4 +1 1 +0 0 +# state = 6 +.mv state$_nf4_nf7$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nf4_nf7$true +machine_concret1_Abs1_STATE_35 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nf4_nf8$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nf4_nf9$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_nf4_nfa$true +- =nd_o2 +.mv _nfd 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _nfd +machine_concret1_Abs1_STATE_44 +.names state _nfd _nfc +.def 0 +- =state 1 +.names _nfc _nfb +1 1 +0 0 +# state = 7 +.mv state$_nfb_nfe$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nfb_nfe$true +machine_concret1_Abs1_STATE_39 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_nfb_nff$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_nfb_n100$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_nfb_n101$true +- =nd_o2 +.mv _n104 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n104 +machine_concret1_Abs1_STATE_38 +.names state _n104 _n103 +.def 0 +- =state 1 +.names _n103 _n102 +1 1 +0 0 +# state = 7 +.mv state$_n102_n105$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n102_n105$true +machine_concret1_Abs1_STATE_39 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n102_n106$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n102_n107$true +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n102_n108$true +- =nd_o2 +.mv _n10b 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n10b +machine_concret1_Abs1_STATE_40 +.names state _n10b _n10a +.def 0 +- =state 1 +.names _n10a _n109 +1 1 +0 0 +.names _n10d +1 +# nd_aff0 == 1 +.names nd_aff0 _n10d _n10e +.def 0 +0 1 1 +1 0 1 +.names _n10e _n10c +0 1 +1 0 +.names _n10c _n110 +- =_n10c +# state = 8 +.mv state$_n10c_n111$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n10c_n111$true +machine_concret1_Abs1_STATE_41 +# o2 = 1 +.names o2$_n10c_n112$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n10c_n113$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n10c_n114$true +- =nd_o1 +# state = 9 +.mv state$_n10c_n115$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n10c_n115$false +machine_concret1_Abs1_STATE_42 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n10c_n116$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n10c_n117$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n10c_n118$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n10c_n114$true o1$_n10c_n117$false _n10c o1$_n10c$raw_n11d +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n10c_n112$true o2$_n10c_n118$false _n10c o2$_n10c$raw_n11f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n10c_n113$true r_i1$_n10c_n116$false _n10c r_i1$_n10c$raw_n121 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n10c$raw_n123 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n10c_n111$true state$_n10c_n115$false _n10c state$_n10c$raw_n123 +- - 0 =state$_n10c_n115$false +- - 1 =state$_n10c_n111$true +.mv _n12e 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n12e +machine_concret1_Abs1_STATE_36 +.names state _n12e _n12d +.def 0 +- =state 1 +.names _n12d _n12c +1 1 +0 0 +.names _n130 +1 +# nd_aff0 == 1 +.names nd_aff0 _n130 _n131 +.def 0 +0 1 1 +1 0 1 +.names _n131 _n12f +0 1 +1 0 +.names _n12f _n133 +- =_n12f +# state = 10 +.mv state$_n12f_n134$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n12f_n134$true +machine_concret1_Abs1_STATE_34 +# o1 = 1 +.names o1$_n12f_n135$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n12f_n136$true +- =nd_r_i1 +# o2 = nd_o2 +.names nd_o2 o2$_n12f_n137$true +- =nd_o2 +# state = 14 +.mv state$_n12f_n138$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n12f_n138$false +machine_concret1_Abs1_STATE_36 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n12f_n139$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n12f_n13a$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n12f_n13b$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n12f_n135$true o1$_n12f_n13a$false _n12f o1$_n12f$raw_n140 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n12f_n137$true o2$_n12f_n13b$false _n12f o2$_n12f$raw_n142 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n12f_n136$true r_i1$_n12f_n139$false _n12f r_i1$_n12f$raw_n144 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n12f$raw_n146 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n12f_n134$true state$_n12f_n138$false _n12f state$_n12f$raw_n146 +- - 0 =state$_n12f_n138$false +- - 1 =state$_n12f_n134$true +.mv _n151 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n151 +machine_concret1_Abs1_STATE_33 +.names state _n151 _n150 +.def 0 +- =state 1 +.names _n150 _n14f +1 1 +0 0 +.names _n153 +1 +# nd_aff0 == 1 +.names nd_aff0 _n153 _n154 +.def 0 +0 1 1 +1 0 1 +.names _n154 _n152 +0 1 +1 0 +.names _n152 _n156 +- =_n152 +# state = 10 +.mv state$_n152_n157$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n152_n157$true +machine_concret1_Abs1_STATE_34 +# o1 = 1 +.names o1$_n152_n158$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n152_n159$true +- =nd_r_i1 +# o2 = nd_o2 +.names nd_o2 o2$_n152_n15a$true +- =nd_o2 +# state = 14 +.mv state$_n152_n15b$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n152_n15b$false +machine_concret1_Abs1_STATE_36 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n152_n15c$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n152_n15d$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n152_n15e$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n152_n158$true o1$_n152_n15d$false _n152 o1$_n152$raw_n163 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n152_n15a$true o2$_n152_n15e$false _n152 o2$_n152$raw_n165 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n152_n159$true r_i1$_n152_n15c$false _n152 r_i1$_n152$raw_n167 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n152$raw_n169 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n152_n157$true state$_n152_n15b$false _n152 state$_n152$raw_n169 +- - 0 =state$_n152_n15b$false +- - 1 =state$_n152_n157$true +.mv _n174 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n174 +machine_concret1_Abs1_STATE_45 +.names state _n174 _n173 +.def 0 +- =state 1 +.names _n173 _n172 +1 1 +0 0 +.names _n176 +1 +# nd_aff0 == 1 +.names nd_aff0 _n176 _n177 +.def 0 +0 1 1 +1 0 1 +.names _n177 _n175 +0 1 +1 0 +.names _n175 _n179 +- =_n175 +# state = 11 +.mv state$_n175_n17a$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n175_n17a$true +machine_concret1_Abs1_STATE_44 +# o1 = 1 +.names o1$_n175_n17b$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n175_n17c$true +- =nd_r_i1 +# o2 = nd_o2 +.names nd_o2 o2$_n175_n17d$true +- =nd_o2 +# state = 16 +.mv state$_n175_n17e$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n175_n17e$false +machine_concret1_Abs1_STATE_45 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n175_n17f$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n175_n180$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n175_n181$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n175_n17b$true o1$_n175_n180$false _n175 o1$_n175$raw_n186 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n175_n17d$true o2$_n175_n181$false _n175 o2$_n175$raw_n188 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n175_n17c$true r_i1$_n175_n17f$false _n175 r_i1$_n175$raw_n18a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n175$raw_n18c 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n175_n17a$true state$_n175_n17e$false _n175 state$_n175$raw_n18c +- - 0 =state$_n175_n17e$false +- - 1 =state$_n175_n17a$true +.mv _n197 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n197 +machine_concret1_Abs1_STATE_43 +.names state _n197 _n196 +.def 0 +- =state 1 +.names _n196 _n195 +1 1 +0 0 +.names _n199 +1 +# nd_aff0 == 1 +.names nd_aff0 _n199 _n19a +.def 0 +0 1 1 +1 0 1 +.names _n19a _n198 +0 1 +1 0 +.names _n198 _n19c +- =_n198 +# state = 11 +.mv state$_n198_n19d$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n198_n19d$true +machine_concret1_Abs1_STATE_44 +# o1 = 1 +.names o1$_n198_n19e$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n198_n19f$true +- =nd_r_i1 +# o2 = nd_o2 +.names nd_o2 o2$_n198_n1a0$true +- =nd_o2 +# state = 16 +.mv state$_n198_n1a1$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n198_n1a1$false +machine_concret1_Abs1_STATE_45 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n198_n1a2$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n198_n1a3$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n198_n1a4$false +- =nd_o2 +# if/else (nd_aff0 == 1) +.names o1$_n198_n19e$true o1$_n198_n1a3$false _n198 o1$_n198$raw_n1a9 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n198_n1a0$true o2$_n198_n1a4$false _n198 o2$_n198$raw_n1ab +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n198_n19f$true r_i1$_n198_n1a2$false _n198 r_i1$_n198$raw_n1ad +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n198$raw_n1af 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n198_n19d$true state$_n198_n1a1$false _n198 state$_n198$raw_n1af +- - 0 =state$_n198_n1a1$false +- - 1 =state$_n198_n19d$true +.mv _n1ba 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n1ba +machine_concret1_Abs1_STATE_46 +.names state _n1ba _n1b9 +.def 0 +- =state 1 +.names _n1b9 _n1b8 +1 1 +0 0 +.names _n1bc +1 +# nd_aff0 == 1 +.names nd_aff0 _n1bc _n1bd +.def 0 +0 1 1 +1 0 1 +.names _n1bd _n1bb +0 1 +1 0 +.names _n1bb _n1bf +- =_n1bb +.names _n1c1 +1 +# nd_aff1 == 1 +.names nd_aff1 _n1c1 _n1c2 +.def 0 +0 1 1 +1 0 1 +.names _n1c2 _n1c0 +0 1 +1 0 +.names _n1c0 _n1c4 +- =_n1c0 +# state = 12 +.mv state$_n1c0_n1c5$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1c0_n1c5$true +machine_concret1_Abs1_STATE_38 +# o1 = 1 +.names o1$_n1c0_n1c6$true +1 +# o2 = 1 +.names o2$_n1c0_n1c7$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n1c0_n1c8$true +- =nd_r_i1 +# state = 13 +.mv state$_n1c0_n1c9$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1c0_n1c9$false +machine_concret1_Abs1_STATE_40 +# o1 = 1 +.names o1$_n1c0_n1ca$false +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n1c0_n1cb$false +- =nd_r_i1 +# o2 = nd_o2 +.names nd_o2 o2$_n1c0_n1cc$false +- =nd_o2 +# if/else (nd_aff1 == 1) +.names o1$_n1c0_n1c6$true o1$_n1c0_n1ca$false _n1c0 o1$_n1c0$raw_n1d1 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n1c0_n1c7$true o2$_n1c0_n1cc$false _n1c0 o2$_n1c0$raw_n1d3 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n1c0_n1c8$true r_i1$_n1c0_n1cb$false _n1c0 r_i1$_n1c0$raw_n1d5 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n1c0$raw_n1d7 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1c0_n1c5$true state$_n1c0_n1c9$false _n1c0 state$_n1c0$raw_n1d7 +- - 0 =state$_n1c0_n1c9$false +- - 1 =state$_n1c0_n1c5$true +.names _n1e1 +1 +# nd_aff1 == 1 +.names nd_aff1 _n1e1 _n1e2 +.def 0 +0 1 1 +1 0 1 +.names _n1e2 _n1e0 +0 1 +1 0 +.names _n1e0 _n1e4 +- =_n1e0 +# state = 17 +.mv state$_n1e0_n1e5$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1e0_n1e5$true +machine_concret1_Abs1_STATE_43 +# o2 = 1 +.names o2$_n1e0_n1e6$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n1e0_n1e7$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n1e0_n1e8$true +- =nd_o1 +# state = 18 +.mv state$_n1e0_n1e9$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1e0_n1e9$false +machine_concret1_Abs1_STATE_46 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n1e0_n1ea$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n1e0_n1eb$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n1e0_n1ec$false +- =nd_o2 +# if/else (nd_aff1 == 1) +.names o1$_n1e0_n1e8$true o1$_n1e0_n1eb$false _n1e0 o1$_n1e0$raw_n1f1 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n1e0_n1e6$true o2$_n1e0_n1ec$false _n1e0 o2$_n1e0$raw_n1f3 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n1e0_n1e7$true r_i1$_n1e0_n1ea$false _n1e0 r_i1$_n1e0$raw_n1f5 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n1e0$raw_n1f7 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1e0_n1e5$true state$_n1e0_n1e9$false _n1e0 state$_n1e0$raw_n1f7 +- - 0 =state$_n1e0_n1e9$false +- - 1 =state$_n1e0_n1e5$true +# if/else (nd_aff0 == 1) +.names o1$_n1c0$raw_n1d1 o1$_n1e0$raw_n1f1 _n1bb o1$_n1bb$raw_n204 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n1c0$raw_n1d3 o2$_n1e0$raw_n1f3 _n1bb o2$_n1bb$raw_n206 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n1bb$raw_n208 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1c0$raw_n1d7 state$_n1e0$raw_n1f7 _n1bb state$_n1bb$raw_n208 +- - 0 =state$_n1e0$raw_n1f7 +- - 1 =state$_n1c0$raw_n1d7 +.names r_i1$_n1c0$raw_n1d5 r_i1$_n1e0$raw_n1f5 _n1bb r_i1$_n1bb$raw_n209 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv _n215 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n215 +machine_concret1_Abs1_STATE_37 +.names state _n215 _n214 +.def 0 +- =state 1 +.names _n214 _n213 +1 1 +0 0 +.names _n217 +1 +# nd_aff0 == 1 +.names nd_aff0 _n217 _n218 +.def 0 +0 1 1 +1 0 1 +.names _n218 _n216 +0 1 +1 0 +.names _n216 _n21a +- =_n216 +.names _n21c +1 +# nd_aff1 == 1 +.names nd_aff1 _n21c _n21d +.def 0 +0 1 1 +1 0 1 +.names _n21d _n21b +0 1 +1 0 +.names _n21b _n21f +- =_n21b +# state = 12 +.mv state$_n21b_n220$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n21b_n220$true +machine_concret1_Abs1_STATE_38 +# o1 = 1 +.names o1$_n21b_n221$true +1 +# o2 = 1 +.names o2$_n21b_n222$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n21b_n223$true +- =nd_r_i1 +# state = 13 +.mv state$_n21b_n224$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n21b_n224$false +machine_concret1_Abs1_STATE_40 +# o1 = 1 +.names o1$_n21b_n225$false +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n21b_n226$false +- =nd_r_i1 +# o2 = nd_o2 +.names nd_o2 o2$_n21b_n227$false +- =nd_o2 +# if/else (nd_aff1 == 1) +.names o1$_n21b_n221$true o1$_n21b_n225$false _n21b o1$_n21b$raw_n22c +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n21b_n222$true o2$_n21b_n227$false _n21b o2$_n21b$raw_n22e +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n21b_n223$true r_i1$_n21b_n226$false _n21b r_i1$_n21b$raw_n230 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n21b$raw_n232 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n21b_n220$true state$_n21b_n224$false _n21b state$_n21b$raw_n232 +- - 0 =state$_n21b_n224$false +- - 1 =state$_n21b_n220$true +.names _n23c +1 +# nd_aff1 == 1 +.names nd_aff1 _n23c _n23d +.def 0 +0 1 1 +1 0 1 +.names _n23d _n23b +0 1 +1 0 +.names _n23b _n23f +- =_n23b +# state = 17 +.mv state$_n23b_n240$true 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n23b_n240$true +machine_concret1_Abs1_STATE_43 +# o2 = 1 +.names o2$_n23b_n241$true +1 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n23b_n242$true +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n23b_n243$true +- =nd_o1 +# state = 18 +.mv state$_n23b_n244$false 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n23b_n244$false +machine_concret1_Abs1_STATE_46 +# r_i1 = nd_r_i1 +.names nd_r_i1 r_i1$_n23b_n245$false +- =nd_r_i1 +# o1 = nd_o1 +.names nd_o1 o1$_n23b_n246$false +- =nd_o1 +# o2 = nd_o2 +.names nd_o2 o2$_n23b_n247$false +- =nd_o2 +# if/else (nd_aff1 == 1) +.names o1$_n23b_n243$true o1$_n23b_n246$false _n23b o1$_n23b$raw_n24c +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n23b_n241$true o2$_n23b_n247$false _n23b o2$_n23b$raw_n24e +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n23b_n242$true r_i1$_n23b_n245$false _n23b r_i1$_n23b$raw_n250 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n23b$raw_n252 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n23b_n240$true state$_n23b_n244$false _n23b state$_n23b$raw_n252 +- - 0 =state$_n23b_n244$false +- - 1 =state$_n23b_n240$true +# if/else (nd_aff0 == 1) +.names o1$_n21b$raw_n22c o1$_n23b$raw_n24c _n216 o1$_n216$raw_n25f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n21b$raw_n22e o2$_n23b$raw_n24e _n216 o2$_n216$raw_n261 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n216$raw_n263 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n21b$raw_n232 state$_n23b$raw_n252 _n216 state$_n216$raw_n263 +- - 0 =state$_n23b$raw_n252 +- - 1 =state$_n21b$raw_n232 +.names r_i1$_n21b$raw_n230 r_i1$_n23b$raw_n250 _n216 r_i1$_n216$raw_n264 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +# case (state ) +.names o1$_n216$raw_n25f o1 _n213 o1$_n213$raw_n276 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n216$raw_n261 o2 _n213 o2$_n213$raw_n278 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n216$raw_n264 r_i1 _n213 r_i1$_n213$raw_n27a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n213$raw_n27c 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n216$raw_n263 state _n213 state$_n213$raw_n27c +- - 0 =state +- - 1 =state$_n216$raw_n263 +.names o1$_n1bb$raw_n204 o1$_n213$raw_n276 _n1b8 o1$_n1b8$raw_n27d +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n1bb$raw_n206 o2$_n213$raw_n278 _n1b8 o2$_n1b8$raw_n27f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n1bb$raw_n209 r_i1$_n213$raw_n27a _n1b8 r_i1$_n1b8$raw_n281 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n1b8$raw_n283 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n1bb$raw_n208 state$_n213$raw_n27c _n1b8 state$_n1b8$raw_n283 +- - 0 =state$_n213$raw_n27c +- - 1 =state$_n1bb$raw_n208 +.names o1$_n198$raw_n1a9 o1$_n1b8$raw_n27d _n195 o1$_n195$raw_n290 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n198$raw_n1ab o2$_n1b8$raw_n27f _n195 o2$_n195$raw_n292 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n195$raw_n294 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n198$raw_n1af state$_n1b8$raw_n283 _n195 state$_n195$raw_n294 +- - 0 =state$_n1b8$raw_n283 +- - 1 =state$_n198$raw_n1af +.names r_i1$_n198$raw_n1ad r_i1$_n1b8$raw_n281 _n195 r_i1$_n195$raw_n295 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n175$raw_n186 o1$_n195$raw_n290 _n172 o1$_n172$raw_n2a3 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n175$raw_n188 o2$_n195$raw_n292 _n172 o2$_n172$raw_n2a5 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n172$raw_n2a7 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n175$raw_n18c state$_n195$raw_n294 _n172 state$_n172$raw_n2a7 +- - 0 =state$_n195$raw_n294 +- - 1 =state$_n175$raw_n18c +.names r_i1$_n175$raw_n18a r_i1$_n195$raw_n295 _n172 r_i1$_n172$raw_n2a8 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n152$raw_n163 o1$_n172$raw_n2a3 _n14f o1$_n14f$raw_n2b6 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n152$raw_n165 o2$_n172$raw_n2a5 _n14f o2$_n14f$raw_n2b8 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n14f$raw_n2ba 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n152$raw_n169 state$_n172$raw_n2a7 _n14f state$_n14f$raw_n2ba +- - 0 =state$_n172$raw_n2a7 +- - 1 =state$_n152$raw_n169 +.names r_i1$_n152$raw_n167 r_i1$_n172$raw_n2a8 _n14f r_i1$_n14f$raw_n2bb +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n12f$raw_n140 o1$_n14f$raw_n2b6 _n12c o1$_n12c$raw_n2c9 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n12f$raw_n142 o2$_n14f$raw_n2b8 _n12c o2$_n12c$raw_n2cb +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n12c$raw_n2cd 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n12f$raw_n146 state$_n14f$raw_n2ba _n12c state$_n12c$raw_n2cd +- - 0 =state$_n14f$raw_n2ba +- - 1 =state$_n12f$raw_n146 +.names r_i1$_n12f$raw_n144 r_i1$_n14f$raw_n2bb _n12c r_i1$_n12c$raw_n2ce +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n10c$raw_n11d o1$_n12c$raw_n2c9 _n109 o1$_n109$raw_n2dc +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n10c$raw_n11f o2$_n12c$raw_n2cb _n109 o2$_n109$raw_n2de +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n109$raw_n2e0 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n10c$raw_n123 state$_n12c$raw_n2cd _n109 state$_n109$raw_n2e0 +- - 0 =state$_n12c$raw_n2cd +- - 1 =state$_n10c$raw_n123 +.names r_i1$_n10c$raw_n121 r_i1$_n12c$raw_n2ce _n109 r_i1$_n109$raw_n2e1 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n102_n107$true o1$_n109$raw_n2dc _n102 o1$_n102$raw_n2ef +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n102_n108$true o2$_n109$raw_n2de _n102 o2$_n102$raw_n2f1 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n102_n106$true r_i1$_n109$raw_n2e1 _n102 r_i1$_n102$raw_n2f3 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n102$raw_n2f5 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n102_n105$true state$_n109$raw_n2e0 _n102 state$_n102$raw_n2f5 +- - 0 =state$_n109$raw_n2e0 +- - 1 =state$_n102_n105$true +.names o1$_nfb_n100$true o1$_n102$raw_n2ef _nfb o1$_nfb$raw_n302 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nfb_n101$true o2$_n102$raw_n2f1 _nfb o2$_nfb$raw_n304 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nfb_nff$true r_i1$_n102$raw_n2f3 _nfb r_i1$_nfb$raw_n306 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nfb$raw_n308 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nfb_nfe$true state$_n102$raw_n2f5 _nfb state$_nfb$raw_n308 +- - 0 =state$_n102$raw_n2f5 +- - 1 =state$_nfb_nfe$true +.names o1$_nf4_nf9$true o1$_nfb$raw_n302 _nf4 o1$_nf4$raw_n315 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nf4_nfa$true o2$_nfb$raw_n304 _nf4 o2$_nf4$raw_n317 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nf4_nf8$true r_i1$_nfb$raw_n306 _nf4 r_i1$_nf4$raw_n319 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nf4$raw_n31b 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nf4_nf7$true state$_nfb$raw_n308 _nf4 state$_nf4$raw_n31b +- - 0 =state$_nfb$raw_n308 +- - 1 =state$_nf4_nf7$true +.names o1$_nd4$raw_ne5 o1$_nf4$raw_n315 _nd1 o1$_nd1$raw_n328 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nd4$raw_ne7 o2$_nf4$raw_n317 _nd1 o2$_nd1$raw_n32a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nd1$raw_n32c 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nd4$raw_neb state$_nf4$raw_n31b _nd1 state$_nd1$raw_n32c +- - 0 =state$_nf4$raw_n31b +- - 1 =state$_nd4$raw_neb +.names r_i1$_nd4$raw_ne9 r_i1$_nf4$raw_n319 _nd1 r_i1$_nd1$raw_n32d +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_nca_ncf$true o1$_nd1$raw_n328 _nca o1$_nca$raw_n33b +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nca_nd0$true o2$_nd1$raw_n32a _nca o2$_nca$raw_n33d +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nca_nce$true r_i1$_nd1$raw_n32d _nca r_i1$_nca$raw_n33f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nca$raw_n341 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nca_ncd$true state$_nd1$raw_n32c _nca state$_nca$raw_n341 +- - 0 =state$_nd1$raw_n32c +- - 1 =state$_nca_ncd$true +.names o1$_nc3_nc8$true o1$_nca$raw_n33b _nc3 o1$_nc3$raw_n34e +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nc3_nc9$true o2$_nca$raw_n33d _nc3 o2$_nc3$raw_n350 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nc3_nc7$true r_i1$_nca$raw_n33f _nc3 r_i1$_nc3$raw_n352 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nc3$raw_n354 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nc3_nc6$true state$_nca$raw_n341 _nc3 state$_nc3$raw_n354 +- - 0 =state$_nca$raw_n341 +- - 1 =state$_nc3_nc6$true +.names o1$_nbc_nc1$true o1$_nc3$raw_n34e _nbc o1$_nbc$raw_n361 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_nbc_nc2$true o2$_nc3$raw_n350 _nbc o2$_nbc$raw_n363 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_nbc_nc0$true r_i1$_nc3$raw_n352 _nbc r_i1$_nbc$raw_n365 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_nbc$raw_n367 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_nbc_nbf$true state$_nc3$raw_n354 _nbc state$_nbc$raw_n367 +- - 0 =state$_nc3$raw_n354 +- - 1 =state$_nbc_nbf$true +.names o1$_n9c$raw_nad o1$_nbc$raw_n361 _n99 o1$_n99$raw_n374 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n9c$raw_naf o2$_nbc$raw_n363 _n99 o2$_n99$raw_n376 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n99$raw_n378 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n9c$raw_nb3 state$_nbc$raw_n367 _n99 state$_n99$raw_n378 +- - 0 =state$_nbc$raw_n367 +- - 1 =state$_n9c$raw_nb3 +.names r_i1$_n9c$raw_nb1 r_i1$_nbc$raw_n365 _n99 r_i1$_n99$raw_n379 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n92_n97$true o1$_n99$raw_n374 _n92 o1$_n92$raw_n387 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n92_n98$true o2$_n99$raw_n376 _n92 o2$_n92$raw_n389 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n92_n96$true r_i1$_n99$raw_n379 _n92 r_i1$_n92$raw_n38b +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n92$raw_n38d 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n92_n95$true state$_n99$raw_n378 _n92 state$_n92$raw_n38d +- - 0 =state$_n99$raw_n378 +- - 1 =state$_n92_n95$true +.names o1$_n72$raw_n83 o1$_n92$raw_n387 _n6f o1$_n6f$raw_n39a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n72$raw_n85 o2$_n92$raw_n389 _n6f o2$_n6f$raw_n39c +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n6f$raw_n39e 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n72$raw_n89 state$_n92$raw_n38d _n6f state$_n6f$raw_n39e +- - 0 =state$_n92$raw_n38d +- - 1 =state$_n72$raw_n89 +.names r_i1$_n72$raw_n87 r_i1$_n92$raw_n38b _n6f r_i1$_n6f$raw_n39f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o1$_n68_n6d$true o1$_n6f$raw_n39a _n68 o1$_n68$raw_n3ad +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n68_n6e$true o2$_n6f$raw_n39c _n68 o2$_n68$raw_n3af +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n68_n6c$true r_i1$_n6f$raw_n39f _n68 r_i1$_n68$raw_n3b1 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n68$raw_n3b3 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n68_n6b$true state$_n6f$raw_n39e _n68 state$_n68$raw_n3b3 +- - 0 =state$_n6f$raw_n39e +- - 1 =state$_n68_n6b$true +.names o1$_n61_n66$true o1$_n68$raw_n3ad _n61 o1$_n61$raw_n3c0 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n61_n67$true o2$_n68$raw_n3af _n61 o2$_n61$raw_n3c2 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n61_n65$true r_i1$_n68$raw_n3b1 _n61 r_i1$_n61$raw_n3c4 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n61$raw_n3c6 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n61_n64$true state$_n68$raw_n3b3 _n61 state$_n61$raw_n3c6 +- - 0 =state$_n68$raw_n3b3 +- - 1 =state$_n61_n64$true +.names o1$_n5a_n5f$true o1$_n61$raw_n3c0 _n5a o1$_n5a$raw_n3d3 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n5a_n60$true o2$_n61$raw_n3c2 _n5a o2$_n5a$raw_n3d5 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names r_i1$_n5a_n5e$true r_i1$_n61$raw_n3c4 _n5a r_i1$_n5a$raw_n3d7 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv state$_n5a$raw_n3d9 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names state$_n5a_n5d$true state$_n61$raw_n3c6 _n5a state$_n5a$raw_n3d9 +- - 0 =state$_n61$raw_n3c6 +- - 1 =state$_n5a_n5d$true +# conflict arbitrators +.names _n5a _n61 _n68 _n6f _n76 _n92 _n99 _na0 _nbc _nc3 _nca _nd1 _nd8 _nf4 _nfb _n102 _n109 _n110 _n12c _n133 _n14f _n156 _n172 _n179 _n195 _n19c _n1b8 _n1bf _n1c4 _n1e4 _n213 _n21a _n21f _n23f _n3e6 +.def 0 + 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 1 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 0 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 1 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 0 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 1 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 0 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 1 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 0 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 1 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 0 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 1 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 0 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 1 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 0 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 1 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 0 1 +.names _n3e6 o1$_n5a$raw_n3d3 o1 _n3e7 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n5a _n61 _n68 _n6f _n76 _n92 _n99 _na0 _nbc _nc3 _nca _nd1 _nd8 _nf4 _nfb _n102 _n109 _n110 _n12c _n133 _n14f _n156 _n172 _n179 _n195 _n19c _n1b8 _n1bf _n1c4 _n1e4 _n213 _n21a _n21f _n23f _n3e8 +.def 0 + 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 1 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 0 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 1 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 0 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 1 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 0 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 1 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 0 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 1 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 0 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 1 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 0 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 1 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 0 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 1 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 0 1 +.names _n3e8 o2$_n5a$raw_n3d5 o2 _n3e9 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n5a _n61 _n68 _n6f _n76 _n92 _n99 _na0 _nbc _nc3 _nca _nd1 _nd8 _nf4 _nfb _n102 _n109 _n110 _n12c _n133 _n14f _n156 _n172 _n179 _n195 _n19c _n1b8 _n1bf _n1c4 _n1e4 _n213 _n21a _n21f _n23f _n3ea +.def 0 + 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 1 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 0 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 1 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 0 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 1 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 0 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 1 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 0 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 1 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 0 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 1 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 0 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 1 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 0 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 1 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 0 1 +.mv _n3eb 20 machine_concret1_Abs1_STATE_28 machine_concret1_Abs1_STATE_31 machine_concret1_Abs1_STATE_30 machine_concret1_Abs1_STATE_32 machine_concret1_Abs1_STATE_27 machine_concret1_Abs1_STATE_29 machine_concret1_Abs1_STATE_35 machine_concret1_Abs1_STATE_39 machine_concret1_Abs1_STATE_41 machine_concret1_Abs1_STATE_42 machine_concret1_Abs1_STATE_34 machine_concret1_Abs1_STATE_44 machine_concret1_Abs1_STATE_38 machine_concret1_Abs1_STATE_40 machine_concret1_Abs1_STATE_36 machine_concret1_Abs1_STATE_33 machine_concret1_Abs1_STATE_45 machine_concret1_Abs1_STATE_43 machine_concret1_Abs1_STATE_46 machine_concret1_Abs1_STATE_37 +.names _n3ea state$_n5a$raw_n3d9 state _n3eb +1 - - =state$_n5a$raw_n3d9 +0 - - =state +.names _n5a _n61 _n68 _n6f _n76 _n92 _n99 _na0 _nbc _nc3 _nca _nd1 _nd8 _nf4 _nfb _n102 _n109 _n110 _n12c _n133 _n14f _n156 _n172 _n179 _n195 _n19c _n1b8 _n1bf _n1c4 _n1e4 _n213 _n21a _n21f _n23f _n3f6 +.def 0 + 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 1 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 1 0 - - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 1 - - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 1 - - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 1 - - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 1 - - - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 1 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 1 0 - - - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 1 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 1 0 - - - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 1 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 1 0 - - - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 1 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 1 0 - - - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 1 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 1 0 - - - - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 1 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 1 0 - - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 1 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 1 0 - 0 - - - - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 1 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 1 0 - 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 1 1 + 0 0 0 0 - 0 0 - 0 0 0 0 - 0 0 0 0 - 0 - 0 - 0 - 0 - 0 - - - 1 0 - 0 1 +.names _n3f6 r_i1$_n5a$raw_n3d7 r_i1 _n3f7 +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +# non-blocking assignments +# latches +.r o1$_nc$raw_n4b o1 +0 0 +1 1 +.latch _n3e7 o1 +.r o2$_nc$raw_n4d o2 +0 0 +1 1 +.latch _n3e9 o2 +.r r_i1$_nc$raw_n4f r_i1 +0 0 +1 1 +.latch _n3f7 r_i1 +.r state$raw_na state +- =state$raw_na +.latch _n3eb state +# quasi-continuous assignment +.end + + Index: /cegar_dev/cegar/abstract_model/main_abstract.v =================================================================== --- /cegar_dev/cegar/abstract_model/main_abstract.v (revision 4) +++ /cegar_dev/cegar/abstract_model/main_abstract.v (revision 4) @@ -0,0 +1,14 @@ + +module main_Abs(clk); + +input clk; +input i1; +output o1; +output o2; +output r_i1; + +machine_concret1_Abs1 machine_concret1_a1(clk,i1,o1,o2,r_i1); + + +endmodule +`include machine_concret1_Abs1.v Index: /cegar_dev/cegar/abstract_model/param_abs_cegar_1 =================================================================== --- /cegar_dev/cegar/abstract_model/param_abs_cegar_1 (revision 4) +++ /cegar_dev/cegar/abstract_model/param_abs_cegar_1 (revision 4) @@ -0,0 +1,2 @@ +machine_concret1 Phi_1_and_Phi_2 + Index: /cegar_dev/cegar/concrete_model/SATcnf_c1.cnf =================================================================== --- /cegar_dev/cegar/concrete_model/SATcnf_c1.cnf (revision 4) +++ /cegar_dev/cegar/concrete_model/SATcnf_c1.cnf (revision 4) @@ -0,0 +1,318 @@ +c o1_0_0 58 +c Nd25_36_3 38 +c Nd25_36_2 25 +c Nd24_36_4 56 +c Nd25_36_1 11 +c Nd24_36_3 43 +c Nd25_36_0 15 +c Nd24_36_2 30 +c Nd25_37_4 45 +c Nd24_36_1 17 +c Nd25_37_3 32 +c Nd25_37_2 19 +c r_i1_0_0 76 +c Nd25_37_1 5 +c Nd24_37_4 54 +c r_i1_0_1 80 +c Nd25_37_0 1 +c Nd24_37_3 41 +c r_i1_0_2 83 +c Nd24_37_2 28 +c r_i1_0_3 86 +c Nd13_84_3 48 +c Nd24_37_1 14 +c r_i1_0_4 89 +c Nd13_84_2 35 +c machine_concret1.m_state_1_0 3 +c i1_0_-1 77 +c Nd13_84_1 22 +c Nd277_301_3 73 +c machine_concret1.m_state_1_1 7 +c Nd13_84_0 8 +c Nd277_301_2 69 +c Nd12_84_3 52 +c Nd277_301_1 65 +c Nd12_84_2 39 +c machine_concret1.m_state_1_2 21 +c Nd277_301_0 61 +c Nd12_84_1 26 +c machine_concret1.m_state_1_3 34 +c Nd12_84_0 12 +c machine_concret1.m_state_1_4 47 +c o2_0_4 103 +c machine_concret1.m_state_0_0 2 +c i1_0_0 9 +c o2_0_3 100 +c machine_concret1.m_state_0_1 6 +c i1_0_1 23 +c o2_0_2 97 +c o1_0_4 72 +c machine_concret1.m_state_0_2 20 +c i1_0_2 36 +c o2_0_1 94 +c machine_concret1.m_state_0_3 33 +c i1_0_3 49 +c o1_0_3 68 +c o2_0_0 92 +c machine_concret1.m_state_0_4 46 +c o1_0_2 64 +c Nd25_36_4 51 +c o1_0_1 60 +p cnf 105 257 +2 3 1 0 +-2 -1 0 +-3 -1 0 +-1 4 0 +1 -4 0 +4 0 +6 7 5 0 +-6 -5 0 +-7 -5 0 +9 -1 8 0 +-9 -8 0 +1 -8 0 +-5 -8 10 0 +5 -10 0 +8 -10 0 +6 -7 11 0 +-6 -11 0 +7 -11 0 +-9 -1 12 0 +9 -12 0 +1 -12 0 +-11 -12 13 0 +11 -13 0 +12 -13 0 +-6 7 14 0 +6 -14 0 +-7 -14 0 +2 -3 15 0 +-2 -15 0 +3 -15 0 +-14 -15 16 0 +14 -16 0 +15 -16 0 +-6 -7 17 0 +6 -17 0 +7 -17 0 +-17 -2 18 0 +17 -18 0 +2 -18 0 +10 13 16 18 0 +20 21 19 0 +-20 -19 0 +-21 -19 0 +23 -5 22 0 +-23 -22 0 +5 -22 0 +-19 -22 24 0 +19 -24 0 +22 -24 0 +20 -21 25 0 +-20 -25 0 +21 -25 0 +-23 -5 26 0 +23 -26 0 +5 -26 0 +-25 -26 27 0 +25 -27 0 +26 -27 0 +-20 21 28 0 +20 -28 0 +-21 -28 0 +-28 -11 29 0 +28 -29 0 +11 -29 0 +-20 -21 30 0 +20 -30 0 +21 -30 0 +-30 -6 31 0 +30 -31 0 +6 -31 0 +24 27 29 31 0 +33 34 32 0 +-33 -32 0 +-34 -32 0 +36 -19 35 0 +-36 -35 0 +19 -35 0 +-32 -35 37 0 +32 -37 0 +35 -37 0 +33 -34 38 0 +-33 -38 0 +34 -38 0 +-36 -19 39 0 +36 -39 0 +19 -39 0 +-38 -39 40 0 +38 -40 0 +39 -40 0 +-33 34 41 0 +33 -41 0 +-34 -41 0 +-41 -25 42 0 +41 -42 0 +25 -42 0 +-33 -34 43 0 +33 -43 0 +34 -43 0 +-43 -20 44 0 +43 -44 0 +20 -44 0 +37 40 42 44 0 +46 47 45 0 +-46 -45 0 +-47 -45 0 +49 -32 48 0 +-49 -48 0 +32 -48 0 +-45 -48 50 0 +45 -50 0 +48 -50 0 +46 -47 51 0 +-46 -51 0 +47 -51 0 +-49 -32 52 0 +49 -52 0 +32 -52 0 +-51 -52 53 0 +51 -53 0 +52 -53 0 +-46 47 54 0 +46 -54 0 +-47 -54 0 +-54 -38 55 0 +54 -55 0 +38 -55 0 +-46 -47 56 0 +46 -56 0 +47 -56 0 +-56 -33 57 0 +56 -57 0 +33 -57 0 +50 53 55 57 0 +58 59 0 +-58 -59 0 +59 0 +8 15 61 0 +-8 -61 0 +-15 -61 0 +60 61 62 0 +-60 -62 0 +-61 -62 0 +-60 -61 63 0 +60 -63 0 +61 -63 0 +62 63 0 +22 11 65 0 +-22 -65 0 +-11 -65 0 +64 65 66 0 +-64 -66 0 +-65 -66 0 +-64 -65 67 0 +64 -67 0 +65 -67 0 +66 67 0 +35 25 69 0 +-35 -69 0 +-25 -69 0 +68 69 70 0 +-68 -70 0 +-69 -70 0 +-68 -69 71 0 +68 -71 0 +69 -71 0 +70 71 0 +48 38 73 0 +-48 -73 0 +-38 -73 0 +72 73 74 0 +-72 -74 0 +-73 -74 0 +-72 -73 75 0 +72 -75 0 +73 -75 0 +74 75 0 +76 77 78 0 +-76 -78 0 +-77 -78 0 +-76 -77 79 0 +76 -79 0 +77 -79 0 +78 79 0 +80 9 81 0 +-80 -81 0 +-9 -81 0 +-80 -9 82 0 +80 -82 0 +9 -82 0 +81 82 0 +83 23 84 0 +-83 -84 0 +-23 -84 0 +-83 -23 85 0 +83 -85 0 +23 -85 0 +84 85 0 +86 36 87 0 +-86 -87 0 +-36 -87 0 +-86 -36 88 0 +86 -88 0 +36 -88 0 +87 88 0 +89 49 90 0 +-89 -90 0 +-49 -90 0 +-89 -49 91 0 +89 -91 0 +49 -91 0 +90 91 0 +92 93 0 +-92 -93 0 +93 0 +94 -1 95 0 +-94 -95 0 +1 -95 0 +-94 1 96 0 +94 -96 0 +-1 -96 0 +95 96 0 +97 -5 98 0 +-97 -98 0 +5 -98 0 +-97 5 99 0 +97 -99 0 +-5 -99 0 +98 99 0 +100 -19 101 0 +-100 -101 0 +19 -101 0 +-100 19 102 0 +100 -102 0 +-19 -102 0 +101 102 0 +103 -32 104 0 +-103 -104 0 +32 -104 0 +-103 32 105 0 +103 -105 0 +-32 -105 0 +104 105 0 +-58 0 +-92 0 +-76 0 +60 0 +-94 0 +-80 0 +64 0 +-97 0 +-83 0 +68 0 +-100 0 +-86 0 +72 0 +-103 0 +-89 0 Index: /cegar_dev/cegar/concrete_model/concret_main.mv =================================================================== --- /cegar_dev/cegar/concrete_model/concret_main.mv (revision 4) +++ /cegar_dev/cegar/concrete_model/concret_main.mv (revision 4) @@ -0,0 +1,275 @@ +# vl2mv Concret_Main.v +# version: 1.4 +# date: 13:18:30 09/06/2010 (CEST) +.model main +# I/O ports +.outputs o1 +.outputs o2 +.inputs i1 +.outputs r_i1 +.subckt machine_concret machine_concret1 i1=i1 o1=o1 o2=o2 r_i1=r_i1 +# conflict arbitrators +# non-blocking assignments +# latches +# quasi-continuous assignment +.end + + +.model machine_concret +# I/O ports +.outputs o1 +.outputs o2 +.inputs i1 +.outputs r_i1 +.mv m_state 4 S0 S1 S2 S3 +# m_state = 0 +.mv m_state$raw_n0 4 S0 S1 S2 S3 +.names m_state$raw_n0 +S0 +# o1 = 0 +.names o1$raw_n1 +0 +# o2 = 0 +.names o2$raw_n2 +0 +# r_i1 = i1 +.names i1 r_i1$raw_n3 +- =i1 +# non-blocking assignments for initial +# r_i1 = i1 +.names i1 r_i1$raw_n4 +- =i1 +.mv _n7 4 S0 S1 S2 S3 +.names _n7 +S0 +.names m_state _n7 _n6 +.def 0 +- =m_state 1 +.names _n6 _n5 +1 1 +0 0 +.names _n9 +1 +# i1 == 1 +.names i1 _n9 _na +.def 0 +0 1 1 +1 0 1 +.names _na _n8 +0 1 +1 0 +.names _n8 _nc +- =_n8 +# m_state = 1 +.mv m_state$_n8_nd$true 4 S0 S1 S2 S3 +.names m_state$_n8_nd$true +S1 +# o1 = 1 +.names o1$_n8_ne$true +1 +# o2 = 0 +.names o2$_n8_nf$true +0 +# o1 = 0 +.names o1$_n8_n10$false +0 +# o2 = 0 +.names o2$_n8_n11$false +0 +# m_state = 0 +.mv m_state$_n8_n12$false 4 S0 S1 S2 S3 +.names m_state$_n8_n12$false +S0 +# if/else (i1 == 1) +.names o1$_n8_ne$true o1$_n8_n10$false _n8 o1$_n8$raw_n17 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n8_nf$true o2$_n8_n11$false _n8 o2$_n8$raw_n19 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv m_state$_n8$raw_n1b 4 S0 S1 S2 S3 +.names m_state$_n8_nd$true m_state$_n8_n12$false _n8 m_state$_n8$raw_n1b +- - 0 =m_state$_n8_n12$false +- - 1 =m_state$_n8_nd$true +.mv _n27 4 S0 S1 S2 S3 +.names _n27 +S1 +.names m_state _n27 _n26 +.def 0 +- =m_state 1 +.names _n26 _n25 +1 1 +0 0 +# m_state = 2 +.mv m_state$_n25_n28$true 4 S0 S1 S2 S3 +.names m_state$_n25_n28$true +S2 +# o1 = 0 +.names o1$_n25_n29$true +0 +# o2 = 1 +.names o2$_n25_n2a$true +1 +.mv _n2d 4 S0 S1 S2 S3 +.names _n2d +S2 +.names m_state _n2d _n2c +.def 0 +- =m_state 1 +.names _n2c _n2b +1 1 +0 0 +# m_state = 3 +.mv m_state$_n2b_n2e$true 4 S0 S1 S2 S3 +.names m_state$_n2b_n2e$true +S3 +# o1 = 1 +.names o1$_n2b_n2f$true +1 +# o2 = 1 +.names o2$_n2b_n30$true +1 +.mv _n33 4 S0 S1 S2 S3 +.names _n33 +S3 +.names m_state _n33 _n32 +.def 0 +- =m_state 1 +.names _n32 _n31 +1 1 +0 0 +# o1 = 1 +.names o1$_n31_n34$true +1 +# o2 = 1 +.names o2$_n31_n35$true +1 +# m_state = 3 +.mv m_state$_n31_n36$true 4 S0 S1 S2 S3 +.names m_state$_n31_n36$true +S3 +# case (m_state ) +.names o1$_n31_n34$true o1 _n31 o1$_n31$raw_n3f +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n31_n35$true o2 _n31 o2$_n31$raw_n41 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv m_state$_n31$raw_n43 4 S0 S1 S2 S3 +.names m_state$_n31_n36$true m_state _n31 m_state$_n31$raw_n43 +- - 0 =m_state +- - 1 =m_state$_n31_n36$true +.names o1$_n2b_n2f$true o1$_n31$raw_n3f _n2b o1$_n2b$raw_n46 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n2b_n30$true o2$_n31$raw_n41 _n2b o2$_n2b$raw_n48 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv m_state$_n2b$raw_n4a 4 S0 S1 S2 S3 +.names m_state$_n2b_n2e$true m_state$_n31$raw_n43 _n2b m_state$_n2b$raw_n4a +- - 0 =m_state$_n31$raw_n43 +- - 1 =m_state$_n2b_n2e$true +.names o1$_n25_n29$true o1$_n2b$raw_n46 _n25 o1$_n25$raw_n58 +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n25_n2a$true o2$_n2b$raw_n48 _n25 o2$_n25$raw_n5a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv m_state$_n25$raw_n5c 4 S0 S1 S2 S3 +.names m_state$_n25_n28$true m_state$_n2b$raw_n4a _n25 m_state$_n25$raw_n5c +- - 0 =m_state$_n2b$raw_n4a +- - 1 =m_state$_n25_n28$true +.names o1$_n8$raw_n17 o1$_n25$raw_n58 _n5 o1$_n5$raw_n6a +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.names o2$_n8$raw_n19 o2$_n25$raw_n5a _n5 o2$_n5$raw_n6c +0 - 1 0 +1 - 1 1 +- 0 0 0 +- 1 0 1 +.mv m_state$_n5$raw_n6e 4 S0 S1 S2 S3 +.names m_state$_n8$raw_n1b m_state$_n25$raw_n5c _n5 m_state$_n5$raw_n6e +- - 0 =m_state$_n25$raw_n5c +- - 1 =m_state$_n8$raw_n1b +# conflict arbitrators +.names _n5 _nc _n25 _n2b _n31 _n7c +.def 0 + 1 1 - - - 1 + 1 0 - - - 1 + 0 - 1 - - 1 + 0 - 0 1 - 1 + 0 - 0 0 1 1 +.names _n7c o1$_n5$raw_n6a o1 _n7d +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n5 _nc _n25 _n2b _n31 _n7e +.def 0 + 1 1 - - - 1 + 1 0 - - - 1 + 0 - 1 - - 1 + 0 - 0 1 - 1 + 0 - 0 0 1 1 +.names _n7e o2$_n5$raw_n6c o2 _n7f +1 0 - 0 +1 1 - 1 +0 - 0 0 +0 - 1 1 +.names _n5 _nc _n25 _n2b _n31 _n80 +.def 0 + 1 1 - - - 1 + 1 0 - - - 1 + 0 - 1 - - 1 + 0 - 0 1 - 1 + 0 - 0 0 1 1 +.mv _n81 4 S0 S1 S2 S3 +.names _n80 m_state$_n5$raw_n6e m_state _n81 +1 - - =m_state$_n5$raw_n6e +0 - - =m_state +.names _n82 +.def 0 + 1 +.names _n82 r_i1$raw_n4 _n83 +.def 0 +1 0 0 +1 1 1 +# non-blocking assignments +# latches +.r o1$raw_n1 o1 +0 0 +1 1 +.latch _n7d o1 +.r o2$raw_n2 o2 +0 0 +1 1 +.latch _n7f o2 +.r m_state$raw_n0 m_state +- =m_state$raw_n0 +.latch _n81 m_state +.r r_i1$raw_n3 r_i1 +0 0 +1 1 +.latch _n83 r_i1 +# quasi-continuous assignment +.end + + Index: /cegar_dev/cegar/concrete_model/concret_main.v =================================================================== --- /cegar_dev/cegar/concrete_model/concret_main.v (revision 4) +++ /cegar_dev/cegar/concrete_model/concret_main.v (revision 4) @@ -0,0 +1,17 @@ +/* ----- Symbolic variables ----- */ +//typedef enum {S0, S1, S2, S3} MState; + +/* ----- Main Module ----- */ + +module main(clk); + +input clk; +input i1; +output o1, o2; +output r_i1; + +machine_concret machine_concret1(clk, i1, o1, o2, r_i1); + +endmodule + +`include machine_concret.v Index: /cegar_dev/cegar/concrete_model/debug_trace_crt =================================================================== --- /cegar_dev/cegar/concrete_model/debug_trace_crt (revision 4) +++ /cegar_dev/cegar/concrete_model/debug_trace_crt (revision 4) @@ -0,0 +1,41 @@ +# MC: formula failed --- AG(o2=0) +# MC: Calling debugger for trace 1 +--State +machine_concret1.m_state:S0 +o1:0 +o2:0 +r_i1:0 +fails AG(o2=0) + +--Counter example is a path to a state where o2=0 is false + --Counter example begins +--State 0: +machine_concret1.m_state:S0 +o1:0 +o2:0 +r_i1:0 + +--Goes to state 1: +machine_concret1.m_state:S1 +o1:1 +r_i1:1 +--On input: +i1:1 + +--Goes to state 2: +machine_concret1.m_state:S2 +o1:0 +o2:1 +--On input: + + + --Counter example ends + +--State +machine_concret1.m_state:S2 +o1:0 +o2:1 +r_i1:1 +fails o2=0. + + Index: /cegar_dev/cegar/concrete_model/machine_concret.ctl =================================================================== --- /cegar_dev/cegar/concrete_model/machine_concret.ctl (revision 4) +++ /cegar_dev/cegar/concrete_model/machine_concret.ctl (revision 4) @@ -0,0 +1,24 @@ +# Phi_1 : +(r_i1 = 0) + AF (o1 = 1); +# Expected result : formula passed +#--------------------------------------------------------- +# Phi_2 : +(r_i1 = 0) + AF (o2 = 1); +# Expected result : formula passed +#--------------------------------------------------------- +# Propriéte globale : +(o1 = 0) + AF (o2 = 1); +# Expected result : formula passed +#--------------------------------------------------------- +A((o1 = 0) U((o1 = 1) * AF(o2 = 1))); +# Expected result : formula passed +#--------------------------------------------------------- +(r_i1 = 0) + AF (((o1=1) *( o2 = 1))); +# Expected result : formula passed +#--------------------------------------------------------- +(r_i1 = 0) + (AF(o1 = 1) * AF (o2 = 1)); +# Expected result : formula passed +#--------------------------------------------------------- +AG (o2 = 0); +# Expected result : formula failed (Counter-example test) +#--------------------------------------------------------- Index: /cegar_dev/cegar/concrete_model/machine_concret.fair =================================================================== --- /cegar_dev/cegar/concrete_model/machine_concret.fair (revision 4) +++ /cegar_dev/cegar/concrete_model/machine_concret.fair (revision 4) @@ -0,0 +1,1 @@ +machine_concret1.m_state = S3; Index: /cegar_dev/cegar/concrete_model/machine_concret.v =================================================================== --- /cegar_dev/cegar/concrete_model/machine_concret.v (revision 4) +++ /cegar_dev/cegar/concrete_model/machine_concret.v (revision 4) @@ -0,0 +1,69 @@ +/* ----- Symbolic variables ----- */ +typedef enum {S0, S1, S2, S3} MState; + +/* ----- Main Module ----- */ +module machine_concret (clk, i1, o1, o2, r_i1); + +input clk; +input i1; +output o1; +output o2; +output r_i1; + +MState reg m_state; +reg o1, o2; +reg r_i1; + +initial + begin + m_state = S0; + o1 = 0; + o2 = 0; + r_i1 = i1; + end //initial + +always @ (posedge clk) begin + + r_i1 = i1; + case (m_state) + S0: + if (i1==1) + begin + m_state = S1; + o1 = 1; + o2 = 0; + end + else + begin + o1 = 0; + o2 = 0; + m_state = S0; + end + + S1: + begin + m_state = S2; + o1 = 0; + o2 = 1; + end + + S2: + begin + m_state = S3; + o1 = 1; + o2 = 1; + end + + S3: + begin + o1 = 1; + o2 = 1; + m_state = S3; + end + + endcase +// r_i1 = i1; + +end //always + +endmodule Index: /cegar_dev/cegar/main.c =================================================================== --- /cegar_dev/cegar/main.c (revision 3) +++ /cegar_dev/cegar/main.c (revision 4) @@ -41,17 +41,16 @@ /*********************************************************/ -#define BLIF_MV_FILE_C1 "EX_C1/Concret_Main.mv" -#define FAIRNESS_FILE_C1 "EX_C1/machine_concret.fair" -#define CTL_FILE_C1 "EX_C1/machine_concret.ctl" -#define CNF_FILE_C1 "EX_C1/SATcnf_c1.cnf" -#define CNF_FILE_C1_BIS "EX_C1/SATcnf_c1_bis.cnf" -#define DEBUG_FILE_C1 "EX_C1/TEST_debug_trace" - - -#define BLIF_MV_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/main_abstract.mv" -#define FAIRNESS_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/main_abstract.fair" -#define CTL_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/machine_concret.ctl" -#define CNF_FILE_A1 "EX_A1/Abs_Phi1_and_Phi2_REFINED/SATcnf_a1.cnf" -#define DEBUG_FILE_A1 "TEST_debug_trace" +#define BLIF_MV_FILE_C1 "concrete_model/concret_main.mv" +#define FAIRNESS_FILE_C1 "concrete_model/machine_concret.fair" +#define CTL_FILE_C1 "concrete_model/machine_concret.ctl" +#define CNF_FILE_C1 "concrete_model/SATcnf_c1.cnf" +#define DEBUG_FILE_C1 "concrete_model/debug_trace_crt" + + +#define BLIF_MV_FILE_A1 "abstract_model/main_abstract.mv" +#define FAIRNESS_FILE_A1 "abstract_model/main_abstract.fair" +#define CTL_FILE_A1 "abstract_model/machine_concret.ctl" +#define CNF_FILE_A1 "abstract_model/SATcnf_a1.cnf" +#define DEBUG_FILE_A1 "abstract_model/debug_trace_abs" /*****************************************************/