主要观点：在模型检查器上运行看似简单的并发程序时发现了令人惊讶的方面，初始化为零的“n”在两个进程执行完语句后在模型检查器上的最低值可能为 2，通过在 SPIN 中编写程序并添加断言进行验证，展示了极端的交错情况，还尝试用 Go 程序限制为单线程来观察，对能否在实践中观察到“n”为 2 感到疑惑，想知道是否有其他方式能创建此计算或“n”值低于 10 的计算。
关键信息：模型检查器上并发程序的“n”最低值为 2 的极端交错情况，SPIN 程序及相关断言，Go 程序限制为单线程的实验，对能否在实践中实现特定情况的思考。
重要细节：在 PROMELA 程序中进程的执行顺序导致“n”最终为 2，给出了 Go 程序代码及运行结果，提到从未见过如此极端的交错，对其他可能创建特定计算的方式感到好奇。