Логические выражения температуры

Я работаю над некоторыми логическими выражениями. Я хочу объединить 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;`

Второе выражение верно, когда все значения в наборе больше 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, но не все.

Любые идеи, как объединить эти два?


logic boolean-logic vdm++
person Tom    schedule 18.02.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Похоже, вы ищете квантификатор существования. Я предполагаю, что TempRead - это последовательность, поэтому что-то вроде:

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

Если вы буквально имеете в виду «но не все из них», вам понадобится дополнительный «и существует», чтобы проверить, существует ли тот, который стоит ‹ 400.

Кстати, будьте осторожны при объединении двух выражений exists с and: вам нужно заключить в скобки все выражение exists, иначе предложение "и" считается частью первого выражения exists!

person Nick Battle    schedule 18.02.2013
comment
Спасибо! Не могли бы вы быстро объяснить мне, что означает temp & temp(i) › 400? как бы вы прочитали это на английском языке - person Tom; 18.02.2013
comment
Вам нужно посмотреть Справочное руководство по языку (оно есть на сайте Overture). Но вкратце, индексы последовательности — это набор индексов, поэтому индексы [x, y, z] — это набор {1,2,3}. Таким образом, в предложении exists это означает, что в списке существует такой индекс, что временный индекс этого индекса превышает 400, что звучит как то, что вы хотите. - person Nick Battle; 18.02.2013
comment
Между прочим, ваш ContOverLimit действительно должен быть forall, как forall i в set inds temp & temp(i) > 400. Тогда он будет работать независимо от длины последовательности. Итак, существует как супер-или, а forall подобен супер-и. - person Nick Battle; 18.02.2013