CTX_sysTb : CONTEXT =
BEGIN
  
  STATE : TYPE =
    [# inst_gcd : CTX_sysMethods!STATE
     , inst_c1 : CTX_RegN{51}!STATE
     , inst_c2 : CTX_RegN{51}!STATE
     , inst_rg : CTX_RegN{51}!STATE
     , inst_state : CTX_RegN{2}!STATE
     #] ;
  
  ctor : STATE =
    (# inst_gcd := CTX_sysMethods!ctor
     , inst_c1 := CTX_RegN{51}!ctor(Bit{51}!mkConst(19))
     , inst_c2 := CTX_RegN{51}!ctor(Bit{51}!mkConst(5))
     , inst_rg := CTX_RegN{51}!ctor(Bit{51}!mkConst(0))
     , inst_state := CTX_RegN{2}!ctor(Bit{2}!mkConst(0))
     #) ;
  
  rule_RL_r0 (state0 : STATE) : [ BOOLEAN, STATE ] =
    LET def_b__h284 : Bit{51}!T = CTX_RegN{51}!meth_read(state0.inst_c1)
    IN LET def_b__h285 : Bit{51}!T = CTX_RegN{51}!meth_read(state0.inst_c2)
    IN LET def_state__h244 : Bit{2}!T = CTX_RegN{2}!meth_read(state0.inst_state)
    IN LET def_b__h322 : Bit{51}!T = CTX_module_add!fn(def_b__h284, Bit{51}!mkConst(3))
    IN LET def_b__h345 : Bit{51}!T = CTX_module_add!fn(def_b__h285, Bit{51}!mkConst(2))
    IN LET def_gcd_RDY_start____d1 : BOOLEAN = CTX_sysMethods!meth_RDY_start(state0.inst_gcd)
    IN LET def_state_EQ_0___d3 : BOOLEAN = Prim1{2}!primEQ(def_state__h244, Bit{2}!mkConst(0))
    IN LET def_gcd_RDY_start_AND_state_EQ_0___d4 : BOOLEAN =
	     def_gcd_RDY_start____d1 AND def_state_EQ_0___d3
    IN LET act1 : [ CTX_sysMethods!STATE, Unit!T ] =
	     CTX_sysMethods!meth_start(def_b__h284, def_b__h285, state0.inst_gcd)
    IN LET state1 : STATE = state0 WITH .inst_gcd := act1.1
    IN LET act2 : [ CTX_RegN{51}!STATE, Unit!T ] = CTX_RegN{51}!meth_write(def_b__h322, state1.inst_c1)
    IN LET state2 : STATE = state1 WITH .inst_c1 := act2.1
    IN LET act3 : [ CTX_RegN{51}!STATE, Unit!T ] = CTX_RegN{51}!meth_write(def_b__h345, state2.inst_c2)
    IN LET state3 : STATE = state2 WITH .inst_c2 := act3.1
    IN LET act4 : [ CTX_RegN{2}!STATE, Unit!T ] =
	     CTX_RegN{2}!meth_write(Bit{2}!mkConst(1), state3.inst_state)
    IN LET state4 : STATE = state3 WITH .inst_state := act4.1
    IN ( def_gcd_RDY_start_AND_state_EQ_0___d4, state4 ) ;
  
  rule_RL_r1 (state0 : STATE) : [ BOOLEAN, STATE ] =
    LET def_b__h284 : Bit{51}!T = CTX_RegN{51}!meth_read(state0.inst_c1)
    IN LET def_b__h285 : Bit{51}!T = CTX_RegN{51}!meth_read(state0.inst_c2)
    IN LET def_state__h244 : Bit{2}!T = CTX_RegN{2}!meth_read(state0.inst_state)
    IN LET def_b__h322 : Bit{51}!T = CTX_module_add!fn(def_b__h284, Bit{51}!mkConst(3))
    IN LET def_b__h345 : Bit{51}!T = CTX_module_add!fn(def_b__h285, Bit{51}!mkConst(2))
    IN LET def_state_EQ_1___d9 : BOOLEAN = Prim1{2}!primEQ(def_state__h244, Bit{2}!mkConst(1))
    IN LET act1 : [ CTX_sysMethods!STATE, Bit{51}!T ] =
	     CTX_sysMethods!meth_start_and_result(def_b__h284, def_b__h285, state0.inst_gcd)
    IN LET state1 : STATE = state0 WITH .inst_gcd := act1.1
    IN LET def_b__h381 : Bit{51}!T = act1.2
    IN LET def_gcd_start_and_result_0_PLUS_1___d11 : Bit{51}!T =
	     Prim1{51}!primAdd(def_b__h381, Bit{51}!mkConst(1))
    IN LET act2 : [ CTX_RegN{51}!STATE, Unit!T ] =
	     CTX_RegN{51}!meth_write(Prim2{50,1}!primConcat(Prim2{51,50}!primExtract(def_gcd_start_and_result_0_PLUS_1___d11),
							    Bit{1}!mkConst(0)),
				     state1.inst_rg)
    IN LET state2 : STATE = state1 WITH .inst_rg := act2.1
    IN LET act3 : [ CTX_RegN{51}!STATE, Unit!T ] = CTX_RegN{51}!meth_write(def_b__h322, state2.inst_c1)
    IN LET state3 : STATE = state2 WITH .inst_c1 := act3.1
    IN LET act4 : [ CTX_RegN{51}!STATE, Unit!T ] = CTX_RegN{51}!meth_write(def_b__h345, state3.inst_c2)
    IN LET state4 : STATE = state3 WITH .inst_c2 := act4.1
    IN LET act5 : [ CTX_RegN{2}!STATE, Unit!T ] =
	     CTX_RegN{2}!meth_write(Bit{2}!mkConst(2), state4.inst_state)
    IN LET state5 : STATE = state4 WITH .inst_state := act5.1
    IN ( def_state_EQ_1___d9, state5 ) ;
  
  rule_RL_r2 (state0 : STATE) : [ BOOLEAN, STATE ] =
    LET def_state__h244 : Bit{2}!T = CTX_RegN{2}!meth_read(state0.inst_state)
    IN LET def_gcd_RDY_result____d14 : BOOLEAN = CTX_sysMethods!meth_RDY_result(state0.inst_gcd)
    IN LET def_gcd_result____d17 : Bit{51}!T = CTX_sysMethods!meth_result(state0.inst_gcd)
    IN LET def_gcd_result__7_PLUS_1___d18 : Bit{51}!T =
	     Prim1{51}!primAdd(def_gcd_result____d17, Bit{51}!mkConst(1))
    IN LET def_state_EQ_2___d15 : BOOLEAN = Prim1{2}!primEQ(def_state__h244, Bit{2}!mkConst(2))
    IN LET def_gcd_RDY_result__4_AND_state_EQ_2_5___d16 : BOOLEAN =
	     def_gcd_RDY_result____d14 AND def_state_EQ_2___d15
    IN LET act1 : [ CTX_RegN{51}!STATE, Unit!T ] =
	     CTX_RegN{51}!meth_write(Prim2{50,1}!primConcat(Prim2{51,50}!primExtract(def_gcd_result__7_PLUS_1___d18),
							    Bit{1}!mkConst(0)),
				     state0.inst_rg)
    IN LET state1 : STATE = state0 WITH .inst_rg := act1.1
    IN LET act2 : [ CTX_RegN{2}!STATE, Unit!T ] =
	     CTX_RegN{2}!meth_write(Bit{2}!mkConst(0), state1.inst_state)
    IN LET state2 : STATE = state1 WITH .inst_state := act2.1
    IN ( def_gcd_RDY_result__4_AND_state_EQ_2_5___d16, state2 ) ;
  
  rule_RL_exit (state0 : STATE) : [ BOOLEAN, STATE ] =
    LET def_b__h284 : Bit{51}!T = CTX_RegN{51}!meth_read(state0.inst_c1)
    IN LET def_c1_ULE_100___d21 : BOOLEAN = Prim1{51}!primULE(def_b__h284, Bit{51}!mkConst(100))
    IN LET def_v__h538 : Bit{64}!T = Bit{64}!undef
    IN ( NOT def_c1_ULE_100___d21, state0 ) ;
  
END