Status with in-flight HTLC seems incorrect to me

[TKone7]

Hi there
I am eager to learn more about the Lightning Network protocol and remembered you, @guggero, to mention this HTLC-demo in your talk at the Lightning Conference in Berlin. Eventually, I found time to look into it.
I am a little confused when I compare your illustrations with other explanations, in particular, the transaction format in BOLT #3. I completely agree with the to_local output and to_remote output before the HTLC's are introduced. Let me explain my confusion after the HTLC-checkbox is checked.

Initial channel balance

Before any payments are made the channel balances are 4 BTC to Alice and 6 BTC to Bob. Now Alice offers an HTLC to Bob over 1 BTC. I will explain each output in both, Alice's and Bob's, new commitment transaction.

Alice's commitment transaction including HTLC

I don't agree that the 6 BTC output, claimable by Bob immediately, is reduced by 1 BTC. It should stay the same. If it were reduced the whole commitment transaction does no longer add up to the total channel balance.

I agree that the 4 BTC output (either claimable by Bob with revocation private key or by Alice with a timelock) is reduced to 3 BTC.

I agree with the HTLC output.

Bob's commitment transaction including HTLC

I agree with the reduction of 4 BTC (immediately claimable by Alice) to 3 BTC.
I agree with the 6 BTC output remaining the same.
I don't agree with the conditions of the HTLC output. Let me state how I think would be correct:

IF
   <revocation-pubkey> 1 (to Alice)
ELSE
   IF HASH(<preimage>) 
      <receiver-pubkey> 1 (to Bob)
   ELSE
      CLTV
      <sender-pubkey> 1 (to Alice)

Not 100% sure if the exact locking script. I guess in reality it's a little bit more complex. But from the idea, Bob must be able to claim the HTLC output with the preimage and at the same time, it should default back to Alice after the CLTV timeout expires.

Ok, I hope my explanation makes sense. As stated, I am still learning this stuff, so please correct me if I am wrong. Maybe I find time to propose a change to the demo.

[guggero]

Thank you for your feedback!
I added the HTLC view in a hurry before the conference so it's quite possible it's not yet correct.
The HTLC script will probably never look 100% like the script in the spec. Because that would require a second-stage transaction which is probably too complicated to show visually.
My plan was to come up with a reasonable compromise between realism and ease of understanding.

I'll invest some more time in this during the upcoming holidays. There are quite a few features I'd like to add too.