温度逻辑表达式答案

【问题标题】：Temperature logical expressions温度逻辑表达式
【发布时间】：2013-02-18 15:47:46
【问题描述】：

我正在研究一些逻辑表达式。我想将 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，但不是全部。

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

【问题讨论】：

【解决方案1】：

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

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

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

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

【讨论】：

谢谢！你介意快速为我解释一下他的部分“inds temp & temp(i) > 400 是什么意思吗？就像你如何用英语读出来一样
您需要查看语言参考手册（在 Overture 网站上）。但简而言之，序列的“inds”是索引集，因此“inds [x,y,z]”是集合 {1,2,3}。所以在exists子句中，它的意思是“列表中存在一个索引，使得该索引的温度超过400”——这听起来像你想要的。
顺便说一下，你的 ContOverLimit 应该是一个“forall”，如“forall i in set inds temp & temp(i) > 400”。然后无论序列的长度如何，它都会起作用。所以“exists”就像一个超级或，而“forall”就像一个超级与。