Ошибка типа в Alloy с использованием оператора Double In

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

declarative language-specifications declarative-programming alloy
person M5RKED    schedule 05.03.2020    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Другой путь:

все бананы представлены набором Banana все свежие яблоки представлены набором Fresh & Apple x дорого представлен набором x in Expensive

So

Banana in Expensive
(Fresh & Apple) in Expensive

или просто

Banana + (Fresh & Apple) in Expensive
person Daniel Jackson    schedule 05.03.2020

arrow_upward
0
arrow_downward

Если я правильно понимаю, что вы пытаетесь сделать, код не дает сбоя, потому что у вас есть 2 оператора "in", это потому, что вы используете оператор объединения ("+") вместо логического И ("и" или "&&").

Возврат предиката должен оцениваться как 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

Однако, если вы пытаетесь сказать:

  • Экземпляры Apple, которые являются свежими, стоят дорого И
  • Экземпляры банана дорогие

... следующий код - один из способов сделать это:

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 быть дорогими.

person JustAnotherSystemsEngineer    schedule 05.03.2020