logic - 温度論理式

Question

私はいくつかの論理式に取り組んでいます。2 つの式を 1 つにマージしたいのですが、方法がわかりません。VDM Overture Toolを使用しています。

私は5つの温度のセットを見ています。400を超えるものもあれば、下回るものもあります。

最初の式は、少なくとも 1 つの温度が 400 度を超える場合に true になります。

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

2 番目の式は、セット内のすべての値が 400 を超える場合に true になります。

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

私が今作成しようとしている表現は、少なくとも 1 つの温度が 400 度を超える場合ですが、すべてではありません。

これら2つを組み合わせる方法はありますか？

Answer 1

存在量指定子を探しているようです。TempRead はシーケンスであると推測しているので、次のようになります。

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

文字通り「すべてではない」という意味であれば、400 未満のものが存在することを確認するために「and exists」を追加する必要があります。

existsちなみに、2 つの式を: で結合する場合は注意してandください。exists 式全体を括弧で囲む必要があります。そうしないと、"and" 節は最初の exists の一部と見なされます。