Transpiling to TLC bug with IF ELSE expressions

[kakysha]

After I transpiled my Quint model to TLA+, TLC complained about not all states being set after transition:

Successor state is not completely specified by action reRecheckSequentially of the next-state relation. The following variables are not defined: checkStateSequences, committedSequences, finalizeBlockProcess, mempool,
sharedVar, txsQueue.

here is the Quint code:

action reRecheckSequentially = all {
		size(processes) == 0, // all recheck processes are done
		
		val failedTxns = mempool.select(tx => checkStateSequences.get(tx.sender) < tx.seq) // failed txns are those that are not applied to checkState (their seq is > than in checkState)
		if (length(failedTxns) == 0) all {// done sequential re-recheck
			unlock(mempoolMuxKey),
			processes' = processes,
		} else all {
			mutexes' = mutexes,
			startCheckTxProcesses([head(failedTxns)]),
		},

		mempool' = mempool,
		txsQueue' = txsQueue,
		finalizeBlockProcess' = finalizeBlockProcess,
		sharedVar' = sharedVar,
		committedSequences' = committedSequences,
		checkStateSequences' = checkStateSequences,
	}

and transpiled TLA+ code:

(*
  @type: (() => Bool);
*)
reRecheckSequentially ==
  Cardinality(processes) = 0
    /\ LET (*
      @type: (() => Seq({ sender: Str, seq: Int }));
    *)
    failedTxns ==
      LET (*
        @type: ((Seq({ sender: Str, seq: Int }), { sender: Str, seq: Int }) => Seq({ sender: Str, seq: Int }));
      *)
      __QUINT_LAMBDA25(__quint_var5, __QUINT_LAMBDA24) ==
        IF LET (*
          @type: (({ sender: Str, seq: Int }) => Bool);
        *)
        __QUINT_LAMBDA23(tx_612) ==
          checkStateSequences[tx_612["sender"]] < tx_612["seq"]
        IN
        __QUINT_LAMBDA23(__QUINT_LAMBDA24)
        THEN Append(__quint_var5, __QUINT_LAMBDA24)
        ELSE __quint_var5
      IN
      ApaFoldSeqLeft(__QUINT_LAMBDA25, <<>>, mempool)
    IN
    IF Len((failedTxns)) = 0
    THEN unlock((mempoolMuxKey)) /\ processes' := processes
    ELSE mutexes' := mutexes /\ startCheckTxProcesses(<<(Head((failedTxns)))>>
    /\ mempool' := mempool
    /\ txsQueue' := txsQueue
    /\ finalizeBlockProcess' := finalizeBlockProcess
    /\ sharedVar' := sharedVar
    /\ committedSequences' := committedSequences
    /\ checkStateSequences' := checkStateSequences

as @bugarela suggested, enclosing

IF Len((failedTxns)) = 0
    THEN unlock((mempoolMuxKey)) /\ processes' := processes
    ELSE mutexes' := mutexes /\ startCheckTxProcesses(<<(Head((failedTxns)))>>

in parenthesis fixes the problem.

Attached my full quint spec below

parallel_checktx.txt