Model errors of create with generate_name (#566)

By removing the precondition on the API error type from `drop_req`, we
generalize our fault model by including a new type of error: creation
request with `generate_name` fails to create the object when all the
creation attempts conflict with existing objects. This type of error is
non-deterministic because the API server uses a name randomly generated
when handling a creation request whose `name` is empty and
`generate_name` is in use. We treat it as a transient error and assume
that it will eventually disappear. Otherwise, there is no way for
controllers that issue creation requests with `generate_name` to finish
reconciliation.

---------

Signed-off-by: Xudong Sun <[email protected]>

src/v2/kubernetes_cluster/spec/cluster.rs

@@ -411,11 +411,17 @@ impl Cluster {
         }
     }
 
-    // The drop_req drops a request sent to the API server and results in a timeout error
-    // to the sending controller. This is used to model network failures -- in a real-world
-    // cluster, we should expect that a request sent by a controller doesn't arrive at the
-    // API server due to various reasons including network configuration faults and
-    // hardware or software faults in the networking stack.
+    // The drop_req intercepts a request sent to the API server and returns an error
+    // to the sending controller. This is used to model different types of transient
+    // failures, including:
+    // * Network failures that drop the request, where the error might be Timeout.
+    // * API server is running busy and cannot take more requests, where the error
+    //   might be ServerTimeout.
+    // * Non-deterministic requests get rejected by API server. For example, when
+    //   creating an object using a generate_name, API server will try to create
+    //   the object using a randomly generated name, and retry if it fails. If all
+    //   attempts fail, the request will fail with AlreadyExists error. For more
+    //   details, see https://github.com/kubernetes/kubernetes/blob/v1.30.0/staging/src/k8s.io/apiserver/pkg/registry/generic/registry/store.go#L435.
     pub open spec fn drop_req(self) -> Action<ClusterState, (Message, APIError), ()> {
         let result = |input: (Message, APIError), s: ClusterState| {
             let req_msg = input.0;
@@ -435,7 +441,6 @@ impl Cluster {
                 &&& s.req_drop_enabled
                 &&& req_msg.dst.is_APIServer()
                 &&& req_msg.content.is_APIRequest()
-                &&& api_err.is_Timeout() || api_err.is_ServerTimeout()
                 &&& result(input, s).is_Enabled()
             },
             transition: |input: (Message, APIError), s: ClusterState| {