我在 uppaal 中建立了具有传播延迟的简单非门模型。但我无法证明一个属性。附上自动机的截图。Xinp 是输入，xout 是输出。3在这里用作传播延迟。
P1: A[] (xinp && t>3 imply (xout==!xinp))
此属性工作正常，经过 3 个时间单位后，输出变为输入的否定。
P2: A[] (xinp && t<3 imply (xout==!xinp))
这个属性应该是不可满足的，以便我可以验证非门在传播延迟之后和 3 个时间单位输出之前不是根据非门工作。但是这个属性并不是不能满足的。
谢谢
