models: adjust MoreThanFNodesCommitted check

Based on the neo-project/neo-modules#792 (comment),
the definition of MoreThanFNodesCommitted should be adjusted to match
the core algorithm as it's the key factor of the four-good-nodes liveness lock
scenario. There following change is made:

* We consider the node to be "Committed" if it has the Commit message
  sent at _any_ view. If the good node has committed, then we know for sure
  that it won't go further to the next consensus round and can rely on
  this information.

The thing that remains the same is that we do not conu "lost" nodes, because
this information can't be reliably trusted. See the comment inside the commit.

Based on this adjustment, the first liveness lock scenario mentioned in
neo-project/neo-modules#792 (comment)
("Liveness lock with four non-faulty nodes") needs to include one more step
to enter a deadlock: one of the replicas that in the "cv" state must die.

Moreover, there's another liveness lock scenario when one of the nodes is in
the RMDead list, i.e. can "die" at any moment. Consider running the base model
specification with the following configuration:
```
RM      	RMFault 	RMDead 	MaxView
{0, 1, 2, 3} 	{}      	{0} 	2
```

Author: AnnaShaleva

formal-models/dbft/dbft.tla

@@ -103,11 +103,19 @@ GetPrimary(view) == CHOOSE r \in RM : view % N = r
 GetNewView(oldView) == oldView + 1
 
 \* CountCommitted returns the number of nodes that have sent the Commit message
-\* in the current round (as the node r sees it).
-CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit" /\ msg.view = rmState[r].view}) /= 0})
+\* in the current round or in some other round.
+CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit"}) /= 0})
 
 \* MoreThanFNodesCommitted returns whether more than F nodes have been committed
 \* in the current round (as the node r sees it).
+\*
+\* IMPORTANT NOTE: we intentionally do not add the "lost" nodes calculation to the specification, and here's
+\* the reason: from the node's point of view we can't reliably check that some neighbour is completely
+\* out of the network. It is possible that the node doesn't receive consensus messages from some other member
+\* due to network delays. On the other hand, real nodes can go down at any time. The absence of the
+\* member's message doesn't mean that the member is out of the network, we never can be sure about
+\* that, thus, this information is unreliable and can't be trusted during the consensus process.
+\* What can be trusted is whether there's a Commit message from some member was received by the node.
 MoreThanFNodesCommitted(r) == CountCommitted(r) > F
 
 \* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest
@@ -147,7 +155,7 @@ RMSendPrepareResponse(r) ==
      \* condition specifies only the thing that may happen given some particular set of enabling conditions.
      \* Thus, we've extended the NotAcceptingPayloadsDueToViewChanging condition to consider only MoreThanFNodesCommitted.
      \* It should be noted that the logic of MoreThanFNodesCommittedOrLost can't be reliable in detecting lost nodes
-     \* (even with neo-project/neo#2057), because real nodes can go down at any time.
+     \* (even with neo-project/neo#2057), because real nodes can go down at any time. See the comment abothe the MoreThanFNodesCommitted.
      \/ /\ rmState[r].type = "cv"
         /\ MoreThanFNodesCommitted(r)
   /\ \neg IsPrimary(r)
@@ -374,7 +382,7 @@ THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount)
 
 =============================================================================
 \* Modification History
-\* Last modified Mon Feb 27 16:46:19 MSK 2023 by root
+\* Last modified Mon Mar 06 15:28:34 MSK 2023 by root
 \* Last modified Fri Feb 17 15:47:41 MSK 2023 by anna
 \* Last modified Sat Jan 21 01:26:16 MSK 2023 by rik
 \* Created Thu Dec 15 16:06:17 MSK 2022 by anna