NuSMV stucked for none reason

Question

I'm writing a model in NuSMV. However, there is a problem. When I try to simulate the model in using the interactive mode using ./NuSMV -int, it stucks on a state saying that there is not any further reachable states. But, this should not be true according the way I write the model and the transition from that state. For more information I put here the entire model, the execution trace and the entire last state of the trace.

For the model I put the link of pastebin Model. The intereseted part of the model is the MODULE PI and the transition from the pc = 53 to the pc = 54 in the TRANS section.

This is the trace of the simulation

Trace Type: Simulation 
  -> State: 13.1 <-
    ca.x1 = None
    ca.x2 = None
    ca.PK = None
    ca.x3 = None
    ca.len = 0
    cb.x1 = None
    cb.PK = None
    cb.x2 = None
    cb.len = 0
    IniCommitAB = FALSE
    IniRunningAB = FALSE
    ResRunningAB = FALSE
    ResCommitAB = FALSE
    p_initial.PIni_process1.slef = None
    p_initial.PIni_process1.party = None
    p_initial.PIni_process1.nonce = None
    p_initial.PIni_process1.runable = FALSE
    p_initial.PIni_process1.g1 = None
    p_initial.PIni_process1.pc = 1
    p_initial.PIni_process2.slef = None
    p_initial.PIni_process2.party = None
    p_initial.PIni_process2.nonce = None
    p_initial.PIni_process2.runable = FALSE
    p_initial.PIni_process2.g1 = None
    p_initial.PIni_process2.pc = 1
    p_initial.PRes_process.slef = None
    p_initial.PRes_process.nonce = None
    p_initial.PRes_process.g2 = None
    p_initial.PRes_process.g3 = None
    p_initial.PRes_process.runable = FALSE
    p_initial.PRes_process.pc = 1
    p_initial.PI_process.kNa = FALSE
    p_initial.PI_process.kNb = FALSE
    p_initial.PI_process.k_Na_Nb__A = FALSE
    p_initial.PI_process.k_Na_A__B = FALSE
    p_initial.PI_process.k_Nb__B = FALSE
    p_initial.PI_process.x1 = None
    p_initial.PI_process.x2 = None
    p_initial.PI_process.x3 = None
    p_initial.PI_process.pc = 1
    p_initial.PI_process.runable = FALSE
    p_initial.pc = 1
    cb_is_empty = TRUE
    ca_is_empty = TRUE
    p_initial.PI_process.x3_I = FALSE
    p_initial.PI_process.check = TRUE
  -> Input: 13.2 <-
    _process_selector_ = p_initial
    running = FALSE
    p_initial.running = TRUE
    p_initial.PI_process.running = FALSE
    p_initial.PRes_process.running = FALSE
    p_initial.PIni_process2.running = FALSE
    p_initial.PIni_process1.running = FALSE
    cb.running = FALSE
    ca.running = FALSE
  -> State: 13.2 <-
    p_initial.pc = 2
  -> Input: 13.3 <-
  -> State: 13.3 <-
    p_initial.PIni_process1.slef = A1
    p_initial.PIni_process1.party = I
    p_initial.PIni_process1.nonce = Na
    p_initial.PIni_process1.runable = TRUE
    p_initial.pc = 4
  -> Input: 13.4 <-
  -> State: 13.4 <-
    p_initial.PRes_process.slef = B
    p_initial.PRes_process.nonce = Nb
    p_initial.PRes_process.runable = TRUE
    p_initial.pc = 5
  -> Input: 13.5 <-
  -> State: 13.5 <-
    p_initial.PI_process.runable = TRUE
    p_initial.pc = 6
  -> Input: 13.6 <-
    _process_selector_ = p_initial.PIni_process1
    p_initial.running = FALSE
    p_initial.PIni_process1.running = TRUE
  -> State: 13.6 <-
    p_initial.PIni_process1.pc = 4
  -> Input: 13.7 <-
  -> State: 13.7 <-
    p_initial.PIni_process1.pc = 5
  -> Input: 13.8 <-
  -> State: 13.8 <-
    p_initial.PIni_process1.pc = 6
  -> Input: 13.9 <-
  -> State: 13.9 <-
    ca.x1 = A1
    ca.x2 = Na
    ca.PK = A1
    ca.x3 = I
    ca.len = 1
    p_initial.PIni_process1.pc = 7
    ca_is_empty = FALSE
  -> Input: 13.10 <-
    _process_selector_ = p_initial.PI_process
    p_initial.PI_process.running = TRUE
    p_initial.PIni_process1.running = FALSE
  -> State: 13.10 <-
    p_initial.PI_process.pc = 52
  -> Input: 13.11 <-
  -> State: 13.11 <-
    ca.x1 = None
    ca.x2 = None
    ca.PK = None
    ca.x3 = None
    ca.len = 0
    p_initial.PI_process.x1 = Na
    p_initial.PI_process.x2 = A1
    p_initial.PI_process.x3 = I
    p_initial.PI_process.pc = 53
    ca_is_empty = TRUE
    p_initial.PI_process.x3_I = TRUE

While this is the entire last state of the execution

ca.x1 = None
    ca.x2 = None
    ca.PK = None
    ca.x3 = None
    ca.len = 0
    cb.x1 = None
    cb.PK = None
    cb.x2 = None
    cb.len = 0
    IniCommitAB = FALSE
    IniRunningAB = FALSE
    ResRunningAB = FALSE
    ResCommitAB = FALSE
    p_initial.PIni_process1.slef = A1
    p_initial.PIni_process1.party = I
    p_initial.PIni_process1.nonce = Na
    p_initial.PIni_process1.runable = TRUE
    p_initial.PIni_process1.g1 = None
    p_initial.PIni_process1.pc = 7
    p_initial.PIni_process2.slef = None
    p_initial.PIni_process2.party = None
    p_initial.PIni_process2.nonce = None
    p_initial.PIni_process2.runable = FALSE
    p_initial.PIni_process2.g1 = None
    p_initial.PIni_process2.pc = 1
    p_initial.PRes_process.slef = B
    p_initial.PRes_process.nonce = Nb
    p_initial.PRes_process.g2 = None
    p_initial.PRes_process.g3 = None
    p_initial.PRes_process.runable = TRUE
    p_initial.PRes_process.pc = 1
    p_initial.PI_process.kNa = FALSE
    p_initial.PI_process.kNb = FALSE
    p_initial.PI_process.k_Na_Nb__A = FALSE
    p_initial.PI_process.k_Na_A__B = FALSE
    p_initial.PI_process.k_Nb__B = FALSE
    p_initial.PI_process.x1 = Na
    p_initial.PI_process.x2 = A1
    p_initial.PI_process.x3 = I
    p_initial.PI_process.pc = 53
    p_initial.PI_process.runable = TRUE
    p_initial.pc = 6
    cb_is_empty = TRUE
    ca_is_empty = TRUE
p_initial.PI_process.x3_I = TRUE

The problem is that NuSMV stucks on this state. I don't know why, since the condition to step in the next state is that (x3 = I) that is true, in fact p_initial.PI_process.x3_I = TRUE. Moreover, for every simulation it stops at most at the 11th state. These are the command that I give to execute

read_model -i <model>
flatten_hierarchy
encode_variables
build_model
pick_state -r
simulate -r -p -k 12

I know that it is not a simple problem. But I need help, I'm stucked on this problem since weeks.