1

我正在尝试编写一个谓词，使所有香蕉和新鲜苹果都变得昂贵。我能够达到其中一个条件，但不能同时满足这两个条件。我对使用 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
4

2 回答 2

2

另一种方式：

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

所以

Banana in Expensive
(Fresh & Apple) in Expensive

要不就

Banana + (Fresh & Apple) in Expensive
于 2020-03-05T23:21:04.277 回答
0

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

谓词的返回必须评估为 TRUE 或 FALSE。

如果您要说以下内容：

  • Apple的所有实例都是昂贵且新鲜的并且
  • Banana 的所有实例都很昂贵

...以下代码将执行此操作：

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

但是，如果您想说：

  • 新鲜的苹果实例价格昂贵且
  • Banana 的实例很昂贵

...以下代码是一种方法：

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 实例。换句话说，它将让不新鲜的苹果实例变得昂贵。

于 2020-03-05T22:40:04.937 回答