Описание тега alloy
Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the resulting structures.
1
ответ
Добавление элементов набора в Alloy
За установленное время: {1,2,3,4}, как мы можем вычислить сумму элементов в наборе в Alloy? Есть ли способ использовать функцию добавления Alloy для наборов? pred addTime[time: set Time]{ add[time] = 10 }
25 фев '18 в 16:43
1
ответ
Каковы операции для каждого служебного модуля Alloy?
Служебные модули, предоставляемые Alloy, перечислены на этой веб-странице: http://alloy.mit.edu/alloy/documentation/quickguide/util.html Но это не перечисляет операции, предоставляемые каждым модулем. Например, на веб-странице написано, что есть мод…
09 дек '16 в 15:09
1
ответ
Проецирование экземпляра из A4Solution
Я пытаюсь создать новый интерфейс для визуализации моих экземпляров Alloy. Я получил решение A4S и успешно извлек атомы, отношения, проверил подписи атомов, НО я не могу понять, как спроецировать экземпляр на какой-нибудь сигнал. Я заметил, что я мо…
06 дек '13 в 17:58
1
ответ
Возможна ли минимизация затрат в Alloy?
abstract sig Item { price: one Int } one sig item1 extends Item {} { price = 1 } one sig item2 extends Item {} { price = 2 } one sig item3 extends Item {} { price = 3 } one sig item4 extends Item {} { price = 4 } // .. аналогично пунктам с 4 по 10 М…
02 сен '13 в 18:24
1
ответ
Как использовать String в Alloy?
Как использовать String в Alloy? Какие функции или операторы для String поддерживаются в Alloy? Я искал вопросы здесь и нашел, что String - это ключевое слово в Alloy. Но я не могу найти ссылку на то, как использовать String в Alloy. Не могли бы вы …
14 ноя '14 в 11:21
1
ответ
Какие идиомы используются в моделировании?
На странице 195 книги "Программные абстракции" написано: Alloy не имеет фиксированной идиомы для моделей, поэтому вы можете использовать любую идиому, которая лучше всего подходит для данной модели. Книга дает прекрасный пример использования "идиомы…
27 дек '16 в 14:09
2
ответа
Ограничения кардинальности неудовлетворительные
У меня проблемы с получением кардинального оператора Alloy (#) работает как положено даже на простых примерах. Например, следующий файл Alloy... sig Y {} sig X {r : Y -> Y} { //#r = 2 } run {} for exactly 1 X, 3 Y ... дает мне решение, которое со…
25 мар '16 в 09:10
1
ответ
Используя мой собственный API в Alloy
Просто интересно, как я могу использовать свой собственный API в сплаве? Я разработал API в сплаве, но я не знаю, как его использовать? С уважением угрюмый
27 июн '12 в 16:02
1
ответ
Проблемы со спецификацией сплава
Ниже приведена так называемая спецификация сплава, которую я недавно закончил для текстовых сообщений мобильного телефона. Это просто основные требования к текстовым сообщениям, и, поскольку это практика, у меня нет строгих требований к соблюдению. …
07 янв '13 в 14:15
1
ответ
Как мы моделируем случай переключения в Alloy?
У меня есть модель сплава, которая должна иметь некоторые правила, такие как abstract sig country {} one sig US extends country {} one sig UK extends country {} one sig DE extends country {} one sig CA extends country {} abstract sig currencyCode {}…
13 сен '13 в 16:24
2
ответа
Заказ в Сплаве, используя утилиту / заказ
Я пытаюсь узнать о том, как работает заказ в Alloy. У меня есть временная подпись, которую я использовал для создания экземпляра модуля заказа. Я хочу, чтобы предикат addPage добавил страницу в книгу в момент времени t', где t' = t.next. (Как правил…
24 май '17 в 23:05
1
ответ
Как реализовать порядок в наборе наборов?
Когда воздушное судно приближается к аэропорту для приземления, процедура захода на посадку воздушного судна делится на переходы. Каждый переход состоит из набора ножек. sig Transition { legs: set Leg } sig Leg {} Набор ног в переходе упорядочен. Дл…
26 мар '17 в 20:57
1
ответ
Как узнать, когда оператор точки используется для ссылки на поле или для реляционного объединения в Alloy?
Меня смущает оператор точки в Alloy (формальный язык моделирования). Иногда кажется, что когда я выполняю реляционное соединение, я получаю ожидаемый результат, однако иногда я чувствую, что оно используется только для доступа к полю sig, и реляцион…
09 май '17 в 04:01
2
ответа
Выбор SAT Solver из командной строки
Класс edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler предоставляет пример того, как выполнять команды Alloy из командной строки. В этом примере используется бэкэнд-решатель Sat4J. Я хотел бы поменять решатель на один из более быстрых, таких к…
26 апр '16 в 17:52
1
ответ
Несвязный союз двух подписей в Alloy
Я уже спрашивал о декартовом произведении и непересекающемся союзе в Alloy здесь. Там я рассматривал множества как унарные определенные предикаты. Что если я просто хочу разделить объединение двух простых подписей в Alloy. Предположим, у меня есть с…
08 дек '14 в 19:25
2
ответа
Alloy: проверка дерева отношений с помощью предиката
Интересно, как описать древовидные отношения в виде: module tree pred isTree (r: univ −> univ) {...} run isTree for 4 если у меня есть: refines module Graph pred isConnected { some n: Node | (Graph.nodes = n) || (Graph.nodes = n.^(edges.(src + de…
07 сен '16 в 01:51
1
ответ
Оператор кардинальности (#) неверный результат в Alloy
Я использую оператор #, чтобы получить количество декартовых произведений (A->B) и Union (A+B). Но он возвращает странные отрицательные числа, и я понятия не имею, что это такое!? Посмотрите снимок ниже, показывающий содержание A-> B и A + B для мое…
29 мар '15 в 21:57
3
ответа
Почему визуализатор говорит, что каждый атом скрыт?
Ниже приведена модель лиц и их отцов. Я хочу, чтобы Alloy Analyzer показал экземпляр модели. В инструменте Alloy я выбираю "Run Show" (в меню "Выполнить"). Затем я выбираю кнопку "Показать". Вот что отображает документ-камера: Я не знаю, что это зна…
12 ноя '16 в 12:27
1
ответ
Сплав - решение парадокса Барбера все еще противоречиво
Известно, что парадокс парикмахера решается, если есть несколько парикмахеров, чтобы они могли брить друг друга. Эта спецификация соответствует: sig Man {shaves: set Man} some sig Barber extends Man {} fact { Barber.shaves = {m: Man | m not in m.sha…
17 ноя '14 в 00:27
1
ответ
Почему производительность проверки согласованности двух моделей в Alloy не имеет различий?
У меня есть две модели, как следующие. Первый описывает модель. Пол узла и связанные с ним ребра и ограничения удаляются во второй модели. //Signatures for nodes sig NPerson{} abstract sig NGender{} abstract sig NCivilStatus{} lone sig Nmale, Nfemal…
27 мар '15 в 13:35