Присвоение значения в Alloy и использование Enum - PullRequest
Новая
       48

Присвоение значения в Alloy и использование Enum

0 голосов
/ 13 марта 2019

Как назначить переменную в Alloy? 

Sig ClassA{
    variable_1: String,
    variable_2: Int
}

Sig ClassB{
    variable_1: String,
    variable_2: Int
}

pred isLess[a:ClassA,b:ClassB]{
    a.variable_2 < b.variable_2
}

assert integrityTest{
    all a:ClassA,b:ClassB| isLess[a,b]

}

Теперь я хочу проверить контрпример переменных, когда я присваиваю большее значение в a.variable_2, чем b.variable_2.Но я не уверен, как назначить переменную в Alloy.Единственное, что я придумал, это следующее, но оно не работает - 

pred assignValue[a:ClassA]{
    a.variable_2 = Int[4]  
}

Однако я верю, что оно проверит равенство только с 4 и вернет false.Это не имеет ничего общего с заданием.Итак, мой вопрос: как мне создать контрпример, когда a.variable_2>b.variable_2

И как я могу использовать Enum of Int в сплаве?Как- Enum MetricValue {1,2,3,4,5} назначить переменную 1.

РЕДАКТИРОВАТЬ Мне все еще не удается найти контрпример, хотя я могу найти его, вручную проверяя, когда я переключаю значение переменной_2из ca и cb. 

 sig ClassA{ 
    variable_1: String, 
    variable_2 = Int 
 } 

 sig CA extends ClassA{}{ 
    variable_2 = 1 
 } 
 sig ClassB{ 
    variable_1: String,
    variable_2 = Int 
 } 
 sig CB extends ClassB{}{ 
    variable_2 = 4 
 }

 pred checkAllConstraint [ca: ClassA, cb: ClassB] { 
    ca.variable_2 > cb.variable_2 } 

  assert checkAll{ 
    all ca: ClassA, cb: ClassB | checkAllConstraint[ca,cb] 
  } 
  check checkAll for 15

1 Ответ

1 голос
/ 14 марта 2019

Вы можете ограничить поле одним значением через факты.В вашем случае факты подписи пригодятся.

Это будет выглядеть так: 

sig ClassA{
  variable_1: String,
  variable_2: Int
}{
    variable_1="hello world"
    variable_2=4
}

Чтобы связать поле с одним значением из набора, вы можете использовать ключевое слово "in" вместоиз "=" следующим образом: 

sig ClassA{
variable_1: String,
variable_2: Int
}{
    variable_1 in ("hello" + "world")
    variable_2 in (1+2+3+4)  
}

Обратите внимание, что в Alloy + является оператором UNION.Он не суммирует и не объединяет, как вы могли ожидать.

РЕДАКТИРОВАТЬ Он не работает по двум причинам:

  • вы написали: variable_2 = Int вместоvariable_2: Int.При этом ни один действительный экземпляр не содержит атомов, типизированных CA или CB, потому что, например, ClassA.variable2 ограничен набором всех целых чисел, а CA.variable2 ограничен значением 1
  • , атом String не определен.Это одна из странных частей Alloy.Если вы хотите использовать Strings в вашей модели, вам нужно указать где-нибудь строковые литералы, например, на самом деле.

Вот ваша модель с исправлением: 

sig ClassA{ 
    variable_1: String, 
    variable_2 : Int 
 } 

 sig CA extends ClassA{}{ 
    variable_2 = 1 
 } 
 sig ClassB{ 
    variable_1: String,
    variable_2 : Int 
 } 
 sig CB extends ClassB{}{ 
    variable_2 = 4 
 }

 pred checkAllConstraint [ca: ClassA, cb: ClassB] { 
    ca.variable_2 > cb.variable_2 } 

  assert checkAll{ 
    all ca: ClassA, cb: ClassB | checkAllConstraint[ca,cb] 
  } 
  check checkAll for 15

fact { String in ("test"+"test2"+"test3"+"test4")}

Если вывсе еще есть вопросы, пожалуйста, создайте новый.

-

...