Search code examples
logicboolean-logicvdm++

Temperature logical expressions

I'm working on some logical expressions. I want to merge 2 expressions into one but not right sure how. I am using the VDM Overture Tool.

I am looking at set of 5 temperatures. Some are over 400, some under, etc.

My first expression is true when at least 1 temperature is over 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;`

The second expression is true when all values in set are over 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;

The expression I am trying to make now is when at least one temperature is over 400, but not all of them.

Any ideas how to combine these two?

Solution

  • It sounds like you're looking for an existential quantifier. I'm guessing that TempRead is a sequence, so something like:

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

    If you literally mean "but not all of them" you would want an additional "and exists" to check that one existed that was < 400.

    Incidentally, be careful combining two exists expressions with an and: you need to bracket the whole exists expression, otherwise the "and" clause is considered to be part of the first exists!