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 four-nodes deadlock
scenario. There are two changes:
1. We consider the node to be "Committed" if it has the Commit message
   sent at _any_ view.
2. We should count lost nodes as far. We consider the node to be "Lost"
   if it hasn't sent any messages in the current round.

Based on this adjustment, the first liveness lock scenario mentioned in
neo-project/neo-modules#792 (comment)
("Liveness lock with four non-faulty nodes") is unreachable. However,
there's stil a liveness lock 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,12 +103,16 @@ 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).
-MoreThanFNodesCommitted(r) == CountCommitted(r) > F
+\* CountLost returns the number of nodes that considered to be lost. These are the nodes
+\* that didn't send any messages in the current or larger view (as the node r sees it).
+CountLost(r) == Cardinality({rm \in RM : \neg (\E msg \in msgs : msg.view >= rmState[r].view)})
+
+\* MoreThanFNodesCommittedOrLost returns whether more than F nodes have been committed
+\* in the current round (as the node r sees it) or haven't been seen at all at the current view.
+MoreThanFNodesCommittedOrLost(r) == (CountCommitted(r) + CountLost(r)) > F
 
 \* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest
 \* message received from the current round's speaker (as the node r sees it).
@@ -143,13 +147,12 @@ RMSendPrepareResponse(r) ==
      \* and
      \* https://github.com/neo-project/neo-modules/blob/d00d90b9c27b3d0c3c57e9ca1f560a09975df241/src/DBFTPlugin/Consensus/ConsensusService.OnMessage.cs#L79).
      \* However, we can't easily count the number of "lost" nodes in this specification to match precisely
-     \* the implementation. Moreover, we don't need it to be counted as the RMSendPrepareResponse enabling
-     \* 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.
+     \* the implementation. We consider the "lost" nodes to be those who didn't send any message in the current
+     \* view from the r's point of view. 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.
      \/ /\ rmState[r].type = "cv"
-        /\ MoreThanFNodesCommitted(r)
+        /\ MoreThanFNodesCommittedOrLost(r)
   /\ \neg IsPrimary(r)
   /\ PrepareRequestSentOrReceived(r)
   /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
@@ -163,7 +166,7 @@ RMSendCommit(r) ==
      \* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage,
      \* see the related comment inside the RMSendPrepareResponse definition.
      \/ /\ rmState[r].type = "cv"
-        /\ MoreThanFNodesCommitted(r)
+        /\ MoreThanFNodesCommittedOrLost(r)
   /\ Cardinality({
                    msg \in msgs : /\ (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest")
                                   /\ msg.view = rmState[r].view
@@ -374,7 +377,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 13:06:40 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