Вопросы по теме 'alloy'
Опыт использования Alloy в реальных проектах
Некоторое время я интересовался формальными методами. Я использовал формальные методы, чтобы рассуждать о некоторых очень специфических подобластях нескольких проектов, над которыми я работал. Мне так и не удалось убедить других членов команды...
2261 просмотров
schedule
06.04.2022
Есть объект в том или ином наборе, но не в обоих?
Это домашнее задание, и у меня много проблем с ним. Я использую Alloy для моделирования библиотеки. Вот определения объектов:
sig Library {
patrons : set Person,
on_shelves : set Book,
}
sig Book {
authors : set Person,...
608 просмотров
schedule
26.07.2022
Множественности в тернарных отношениях
Семантику нижних множеств some и one в троичных отношениях трудно понять. Согласно Software Abstractions (Rev. ed.), стр. 79–80, отношение addr: Book -> (Name -> some Addr) должно быть эквивалентно all b: Book | b.addr in Name ->...
919 просмотров
schedule
28.10.2022
Сказуемое с аргументами и сказуемое без аргументов в сплаве
Я видел следующее определение в книге:
pred show(b: Book){
some b.addr
}
куда
abstract sig Name, Addr {}
sig Book { addr: Name lone -> lone Addr }
Поиграв с анализатором Alloy, я понял, что это то же самое, что
pred show(){...
706 просмотров
schedule
17.01.2024
Заполнение набора с течением времени в Alloy в полностью подключенной сети
Дополнение от этот вопрос ...
У меня есть полностью связанный граф, и это здорово. Я также добавил понятие времени. Сейчас я борюсь с концепцией передачи данных по моему графику.
Я моделирую систему, задача которой состоит в том, чтобы каждый...
262 просмотров
schedule
15.01.2023
Как перечислить все решения?
Я хочу использовать Alloy Analyzer для перечисления всех решений из предиката в заданной области. Поддерживает ли Alloy эту функцию? Если можно, то как вызвать из командной строки?
Спасибо
453 просмотров
schedule
27.05.2023
Alloy - получить пустой набор при удалении объекта
Рассмотрим следующую спецификацию в Alloy:
sig Books {}
fun f[b:Books] : Books {
{b':Books | b' = Books -b }
}
run show {}
Предположим, у нас есть экземпляр, для которого $univ = {Books$0, Books$1, Books$2}$. Вычисление функции f с...
499 просмотров
schedule
12.11.2023
как запускать предикаты и утверждения в сплаве
Я работаю на C/C++ и пытаюсь понять, как выполняются/проверяются предикаты/утверждения в Alloy. (a) Если у меня есть более одного предиката и я хочу запустить их оба, то как при запуске первого предиката убедиться, что условия, связанные с...
1515 просмотров
schedule
20.05.2022
Alloy — создание экземпляра .xml из .als
Мне нужно создать случайные экземпляры .xml из .als в моей программе. Мне удалось это сделать, запустив сплав в фоновом режиме (невидимый JFrame) и вызвав функции doOpen, doExecuteLatest и doShowLatest. Но необходимость ждать запуска сплава каждый...
484 просмотров
schedule
15.08.2023
Перестановки экземпляров A4options.symmetry и подписи в Alloy
Я смоделировал цепочку преобразования диаграммы в Alloy. Меня интересует любая цепочка, полученная в результате решения, но некоторые цепочки абсолютно одинаковы. Они одинаковы, за исключением перестановки между экземплярами сигнатур, но отношения...
107 просмотров
schedule
12.04.2023
Как выразить структурное равенство между деревьями в Alloy?
Я определил следующую модель Alloy, которая использует один объект State для указания на корни двух деревьев State.a и State.b .
sig N {
children: set N
}
fact {
let p = ~children |
~p.p in iden
and no iden & ^p
}
one sig...
215 просмотров
schedule
18.11.2023
Как оценить предикат в исходном коде Alloy?
У меня есть предикат в моей модели Alloy с именем LS, который получает экземпляр sig с именем st. Я пытаюсь оценить этот предикат для экземпляра st с именем st$0 в исходном коде. Я могу найти решение типа A4Solution, называемое ans. Но я не знаю,...
144 просмотров
schedule
02.11.2022
Рефакторинг моделей Alloy
В модели, которую я начал рисовать в Alloy на днях, я получаю следующее сообщение, когда пытаюсь найти экземпляр определенного предиката:
Объем перевода превышен. В этом контексте Вселенная содержит 34 атома и отношения арности 12 не могут...
381 просмотров
schedule
30.12.2022
Повторение одного и того же анализа сокращает время выполнения. Как этого избежать?
Я заметил, что многократное повторение одного и того же анализа резко сокращает время, необходимое для его завершения. В моем случае генерация, которая занимает 1700 мс при первом запуске, занимает всего 200 мс после нескольких повторений.
Я...
79 просмотров
schedule
31.03.2024
Сплав - решение парадокса Барбера все еще противоречиво
Известно, что парадокс парикмахера решается, если есть несколько парикмахеров, чтобы они могли брить друг друга.
Эта спецификация соответствует:
sig Man {shaves: set Man}
some sig Barber extends Man {}
fact {
Barber.shaves = {m: Man...
279 просмотров
schedule
15.11.2023
понимание ключевого слова this в Alloy
К чему относится ключевое слово this в следующем коде из раздела 4.7.2 книги Alloy?
module library/list [t]
sig List {}
sig NonEmptyList extends List {next: List, element: t}
...
fun List.first : t {this.element}
fun List.rest : List...
321 просмотров
schedule
16.08.2022
Что не так с этим кодом Alloy?
Я получаю сообщение об ошибке синтаксиса для кода ниже. Сообщение обозначает отмеченную позицию в утверждении addLocal, утверждая: «Синтаксическая ошибка в строке 30, столбце 9: здесь может появиться 1 лексема:)» Я просто не вижу, что здесь не так....
384 просмотров
schedule
24.11.2022
наборы в средстве доказательства теорем Z3
У меня есть декларация в Alloy
sig Card{}
sig ATM {card : disj set Card}
и я преобразовал его в Z3 так:
1- (declare-sort ATM)
2- (declare-fun isATM (ATM) Bool)
3- (declare-sort Card)
4- (declare-fun isCard (Card) Bool)
5- (declare-fun...
162 просмотров
schedule
04.05.2022
Является ли использование util/ordering точно таким же, как аксиоматизация общего порядка обычным способом?
Модуль util/ordering содержит комментарий в верхней части файла о том факте, что граница параметра модуля должна иметь точно границу, разрешенную областью действия для указанной подписи.
Я несколько раз читал (например, здесь ), что это...
207 просмотров
schedule
30.08.2023
Отображение производных отношений
Рассмотрим простую графическую структуру G , которая определяет пару отношений ( r1 и r2 ) над набором X узлов. Я хочу поговорить о том, есть ли у моих графиков определенное свойство под названием wf_G . Это свойство определяется путем...
46 просмотров
schedule
11.05.2022
