这篇文章主要探讨了在基于模型的测试中如何处理不确定性（nondeterminism），包含了以下主要内容：

• 模型与实现的差异及挑战：在基于模型的测试中，模型是系统的简化描述，与实际实现存在差异，不确定性使模型状态与实现状态的映射变得复杂，如在认证系统模型中，除了业务相关的错误，还需考虑与实现相关的超时错误。
• 处理实现级错误的方法：对于实现中的超时错误，在模型中有两种主要解释，即对应模型中的空操作或单独的错误值，可通过设置统计正确性声明或预测未来来避免测试通过过于轻易，在基于模型的测试中，可利用测试替身（如存根）来控制超时等不确定性，通过引入预言变量（prophecy variable）来动态配置存根，以确保测试的可靠性。
• 预言变量的理论基础：预言变量比示例测试中的简单存根更强大，其理论基础是解决具有不确定性的规范之间的细化证明问题，通过添加历史和预言变量可以找到合适的细化映射，文章还提到了相关的论文和博客，介绍了预言变量的应用和理论。
• 与预言意识相关的依赖和模态确定性：依赖关系是一把双刃剑，大多数依赖关系并非预言意识的，因此需要创建包装假对象来建模依赖关系，使其具有不确定性和预言意识，以实现对测试的控制，通过创建数据库模型来准确模拟非重复读取等不确定性行为，并利用预言变量在应用测试中选择正确的值。
• 总结与展望：不确定性是基于模型测试的一个难题，预言变量提供了一种处理它的模式，虽然要构建完整的生产级数据库模型还有很多工作要做，但这种方法在原则上是可行的，并且可以应用于各种测试场景。