Illegal vs Unwanted States

April 28, 2026

Keep Unwanted States Representable 保持“非预期状态”的可表示性

An illegal state is a state we never want our system to be in. An unwanted state is a state we don’t want to stay in. Many states that we wish were illegal are actually unwanted. “非法状态”是指我们绝不希望系统进入的状态；而“非预期状态”则是指我们不希望长期停留的状态。许多我们希望定义为“非法”的状态，实际上只是“非预期”的。

Considering a calendaring software which stores calendar events as {user: {events: [event]}}, where each event has a start and end time. This allows one person to attend two events at the same time. We might consider this illegal and replace the data type with {user: {time: optional event}} which makes this impossible. 以日历软件为例，其数据结构为 {user: {events: [event]}}，每个事件都有开始和结束时间。这允许一个人同时参加两个事件。我们可能会认为这是非法的，并将数据类型替换为 {user: {time: optional event}}，从而在逻辑上杜绝这种情况。

However, a scheduling conflict isn’t illegal, only unwanted! It is possible for a person to sign up for two overlapping events. Maybe they’re supposed to choose one event, maybe they’ll decide which event to go to later, maybe one of the events doesn’t actually represent an in-person meeting. In that case it’s acceptable, if not ideal, to remain in the unwanted state. 然而，日程冲突并非非法，只是“非预期”的！一个人完全可能报名参加两个重叠的活动。也许他们需要二选一，也许他们稍后才会决定去哪个，又或者其中一个活动并非线下会议。在这种情况下，停留在这种非预期状态虽然不理想，但却是可以接受的。

Other unwanted states lead to invalid states if not exited quickly. An airline flight is in an unwanted state if there are more passengers booked to fly than seats available. This must be resolved before passengers actually board, as “more passengers physically on the plane than seats available” is an illegal state. 其他一些非预期状态如果不能迅速退出，就会导致无效状态。例如，如果航班预订人数超过了座位数，这就是一种非预期状态。这种情况必须在乘客登机前解决，因为“飞机上实际人数超过座位数”属于非法状态。

In some cases, an unwanted state does not lead to illegal states, but permanently remaining in the unwanted state is still a problem. We might guarantee that a network partition does not ever lead to inconsistent data. Even though the unwanted state of a network partition cannot cause the illegal state of corrupt data, we still have a big problem if we don’t ever fix the partition. 在某些情况下，非预期状态并不会导致非法状态，但长期停留在该状态依然是个问题。我们可以保证网络分区不会导致数据不一致。尽管网络分区这种非预期状态不会直接导致数据损坏这种非法状态，但如果我们永远不修复分区，依然会面临严重问题。

Why systems must represent unwanted states 为什么系统必须能够表示非预期状态

Generally, unwanted states can happen if we don’t have complete control over our system’s behavior. We can’t guarantee our network is perfectly reliable, our servers are always up, our users all put in correct data. If our system gets input from the external world then the world can push us into an unwanted state. We need to be able to detect these states so we can resolve them. 通常，如果我们无法完全控制系统的行为，非预期状态就会发生。我们无法保证网络绝对可靠、服务器永不宕机，也无法保证用户输入的数据永远正确。如果系统接收来自外部世界的输入，外部世界就可能将我们推入非预期状态。我们需要能够检测到这些状态，以便及时解决。

Even when we have complete control over the system, we still may want to be able to temporarily dip into unwanted states. If they wanted, airlines could make overbooking flights impossible. But airlines want to be able to overbook because they expect some number of no-shows. We need to allow them their unwanted state and then put systems in place to prevent it evolving into an illegal state. 即使我们对系统拥有完全控制权，有时也需要暂时进入非预期状态。如果航空公司愿意，他们完全可以禁止超售。但航空公司希望保留超售能力，因为他们预期会有一定比例的乘客缺席。我们需要允许这种非预期状态存在，并建立相应的机制，防止其演变为非法状态。

Sometimes we need unwanted states to make certain workflows possible. It may be the case that 95% never, ever want to accept conflicting events, and preventing that unwanted state would make their lives better. But without that unwanted state, intentionally double booking yourself is impossible. Some people might need that! In these cases we want to make it very clear to users that they’re entering an unwanted state, and then let them decide for themselves how to leave it. (The airlines and users want the unwanted state! It’s us engineers who consider it “unwanted” because it can lead to problems down the road.) 有时，我们需要非预期状态来实现特定的工作流。也许 95% 的用户永远不想接受冲突的日程，禁止这种非预期状态会让他们的生活更美好。但如果没有这种状态，用户就无法主动进行双重预订。有些人可能确实需要这个功能！在这种情况下，我们应该明确告知用户他们正在进入非预期状态，然后让他们自己决定如何处理。（航空公司和用户其实想要这种非预期状态！是我们工程师将其视为“非预期”，因为它可能会在未来引发问题。）

Formal models of unwanted states 非预期状态的形式化模型

Illegal states correspond to violated invariants. Conventionally speaking we write this as []!Illegal: it should be true at all times that Illegal is not true. If a single state ever satisfies Illegal then our system has a bug. 非法状态对应于被破坏的不变量。按照惯例，我们将其写为 []!Illegal：即在任何时候，“非法”都不应为真。如果系统进入了任何一个满足“非法”的状态，就说明系统存在 Bug。

Unwanted states are trickier, since they can be both safety and liveness properties. If modeling an airline system, we don’t necessarily want to check properties of overbooking, we only need to check that no overflights happen. We may discover in the process of verifying that overbooking is the main cause of overflights and/or that if overbooking is not resolved, then we will eventually have an overflight. Further, if “we never overbook” guarantees “we never overflight”, we’d say that “no overbooks” is a stronger property than “no overflights”. 非预期状态则更为复杂，因为它们既涉及安全性（Safety）也涉及活性（Liveness）属性。在建模航空系统时，我们不一定非要检查“超售”属性，只需检查“超载飞行”是否发生。在验证过程中，我们可能会发现超售是导致超载飞行的主要原因，或者如果超售问题不解决，最终会导致超载飞行。此外，如果“从不超售”能保证“从不超载飞行”，那么我们称“无超售”是一个比“无超载飞行”更强的属性。

“We never remain in a network partition” is formalized as []<>!Partition: we can enter a partition and stay partitioned a long time but must eventually heal the partition. The P specification language calls these hot states. “我们从不长期处于网络分区状态”可以形式化为 []<>!Partition：我们可以进入分区状态并停留一段时间，但最终必须修复分区。P 规范语言将此类状态称为“热状态”（hot states）。