я недавно работаю с Alloy. Могу ли я сказать что-то вроде:
fact{
all i: Int | i >= 0
}
Я хочу сказать: все Integer, которые использует Alloy, должны быть положительными. Alloy не подводит, но и экземпляров мне не дают.
Привет
Alloy: факты и т. д. о Int
comment
У меня был аналогичный вопрос, ответ может быть полезен title="сплав определяет отношение только к положительным целым числам"> stackoverflow.com/questions/52690845/
- person Anentropic schedule 09.10.2018
Ответы (1)
Вы не можете в настоящее время сказать, что. Единственная область, которую вы можете указать для целых чисел (которая сообщает Alloy, какие целые числа «использовать»), — это разрядность (например, 4 Int); Затем Alloy всегда использует все целые числа в пределах этой битовой ширины (например, для битовой ширины 4 используются целые числа -8, ..., 7).
Если в вашей модели есть поле типа Int, вы можете использовать факт (как вы сказали выше), чтобы ограничить его значения:
sig S { i: Int }
fact { all s: S | s.i >= 0 }
person
Aleksandar Milicevic
schedule
29.03.2014
но у меня есть небольшая проблема с этим: я хочу сказать: что int находится между 0 и несколько. например, у меня есть этот сигнал: сигнал A{id: int}, и я использую эти факты: факт{все a:A | a.id › 0 } факт{ все a:A | a.id ‹ 20 } Я не получаю экземпляров. Что я делаю не так?
- person Lao Tse; 11.04.2014
Я понял, что один факт неверен. в следующей моей модели и факте, который я считаю неправильным: `sig State extends StateOrJunction{ actionID:one Int, superState:lone State, subStates:set State} sig Transition{ conditionID:one Int, destination:one StateOrJunction, source:lone StateOrJunction} abstract sig StateOrJunction{transitions:set Transition}` Факт, который, я полагаю, неверен, заключается в следующем: fact{ all s:State | нет s':(State-s) | s.actionID = s'.actionID } Я хочу сказать, что все состояния имеют непересекающиеся идентификаторы действий.
- person Lao Tse; 28.04.2014
