logic - 温度逻辑表达式

Question

我正在研究一些逻辑表达式。我想将 2 个表达式合并为一个，但不确定如何。我正在使用VDM Overture Tool。

我正在查看一组 5 个温度。有些超过400，有些低于，等等。

当至少 1 个温度超过 400 时，我的第一个表达式为真：

OverLimit: TempRead -> bool
OverLimit(temp) == temp(1) > 400 or temp(2) > 400 or 
temp(3) > 400 or temp(4) > 400 or 
temp(5) > 400;`

当 set 中的所有值都超过 400 时，第二个表达式为真：

ContOverLimit: TempRead -> bool 
ContOverLimit(temp) ==
temp(1) > 400 and temp(2) > 400 and 
temp(3) > 400 and temp(4) > 400 and 
temp(5) > 400;

我现在要表达的意思是至少有一个温度超过 400，但不是全部。

任何想法如何将这两者结合起来？

Answer 1

听起来您正在寻找一个存在量词。我猜 TempRead 是一个序列，所以类似于：

exists i in set inds temp & temp(i) > 400

如果您的字面意思是“但不是全部”，您将需要一个额外的“并且存在”来检查是否存在 < 400。

顺便说一句，将两个exists表达式与and: 结合使用时要小心，您需要将整个存在表达式括起来，否则“and”子句被认为是第一个存在的一部分！