使用Double In语句的合金类型错误

Question

我正在尝试写一个谓词，使所有香蕉和新鲜苹果都变得昂贵。我能够达到其中一个条件，但不能同时达到两个条件。我对使用Alloy非常陌生，我们将不胜感激。

下面是我的代码，由于我使用的是双重In语句，所以发生了错误，但是我不确定如何不必使用两个in语句就可以编写此代码。我收到的错误是“类型错误，这必须是集合或关系”

sig Fruit{}
sig Banana, Apple, Pear extends Fruit {}
sig Fresh, Expensive in Fruit{}

pred BananasAndFreshApplesAreExpensive {
Apple in (Expensive & Fresh) + Banana in Expensive
} 
run BananasAndFreshApplesAreExpensive

Answer 1

如果我正确理解了您要执行的操作，则代码不会失败，因为您有2条“ in”语句，这是因为您使用的是联合运算符（“ +”）而不是逻辑AND（“ and ”或“ &&”）。

谓词的返回值必须计算为TRUE或FALSE。

如果您要说以下内容：

• Apple的所有实例都是昂贵且新鲜的AND
• 香蕉的所有实例都很昂贵

...下面的代码可以做到：

sig Fruit{}
sig Banana, Apple, Pear extends Fruit {}
sig Fresh, Expensive in Fruit{}

pred BananasAndFreshApplesAreExpensive {
Apple in (Expensive & Fresh) and Banana in Expensive
} 

run BananasAndFreshApplesAreExpensive

但是，如果您想说：

• 新鲜的苹果实例很贵并且
• 香蕉实例很贵

...以下代码是实现此目的的一种方法：

sig Fruit{}
sig Banana, Apple, Pear extends Fruit {}
sig Fresh, Expensive in Fruit{}

pred BananasAndFreshApplesAreExpensive {
    (all a: Apple | a in Fresh => a in Expensive) and
    Banana in Expensive
} 

run BananasAndFreshApplesAreExpensive

不过请记住，这并未说明不新鲜的Apple实例。换句话说，它将使不新鲜的Apple实例变得昂贵。

Answer 2

另一种方式：

所有香蕉都由集合Banana表示所有新鲜苹果都由集合Fresh & Apple表示x表示为x in Expensive

所以

Banana in Expensive
(Fresh & Apple) in Expensive

或只是

Banana + (Fresh & Apple) in Expensive