Вопросы по теме 'alloy'
Моделирование торгового бокса с использованием сплава Alloy
Я пытаюсь смоделировать программу торгового автомата, используя сплав. Я хочу создать модель, в которую я мог бы вставить немного денег и предоставить машине возможность выбора для элемента, и она предоставила бы мне то же самое, и в случае, если...
205 просмотров
schedule
08.09.2021
Спецификация ограничений сплава
Я написал следующий блок кода в Alloy:
one h: Human | h in s.start => {
s'.currentCall = h.from
}
Я хочу выбрать одного «человека» из набора людей (s.start) и установить переменную (s'.currentCall) равной h.from. Однако я думаю, что...
152 просмотров
schedule
29.11.2021
Использование моделей из сплава
Я работаю над проектом об обновлении приложений высокой доступности в промежуточном программном обеспечении SA Forum. В рамках моего исследования мне нужно создать профиль UML для входного файла кампании обновления и проверить этот файл на предмет...
84 просмотров
schedule
09.09.2021
Ограничение диапазона n-арного отношения в сплаве
У меня есть подпись
abstract sig B{}
sig B1 extends B{}
sig B2 extends B{}
sig A{
rel: B->C
}
Как ограничить B объекта rel типом B1? Я попробовал установить факт rel :> (B1 -> C) , но получаю ошибку типа.
Спасибо.
709 просмотров
schedule
16.09.2021
Как определить взаимно однозначное отношение в сплаве
У меня есть три подписи из сплава, как показано ниже:
sig A{}
sig B{}
sig C{}
Как я могу определить биективное отношение (или изоморфизм) между C и A + B.
549 просмотров
schedule
25.09.2021
Почему Визуализатор говорит, что каждый атом скрыт?
Ниже представлены модели людей и их отцов. Я хочу, чтобы анализатор сплава показал экземпляр модели. В инструменте Alloy я выбираю «Run Show» (в меню «Execute»). Затем выбираю кнопку «Показать». Вот что отображает визуализатор:
Я не...
335 просмотров
schedule
03.10.2021
Построение отношения в Alloy
В задаче обедающих философов у нас есть стол с философами и вилками.
sig P {}
sig F {}
Для этой проблемы мне нужно следующее отношение, представляющее таблицу:
P1 -> F1
F1 -> P2
P2 -> F2
F2 -> P3
P3 -> F3
F3 -> P1...
184 просмотров
schedule
24.11.2021
количественная оценка более высокого порядка, которая не может быть сколемизирована
Я изучаю Alloy и экспериментирую с созданием предикатов для отношений injective и surjective . Я пробовал это в Alloy, используя следующую модель:
sig A {}
sig B {}
pred injective(r: A -> B) {
all disj a, a': r.B | no (a.r & a'.r)
}...
256 просмотров
schedule
29.09.2021
Сплавная модель головоломки Эйнштейна
[ Обновление ] Благодаря отличным советам @Daniel Jackson и @Peter Kriens я исправил свою модель Alloy. Теперь анализатор сплавов создает один экземпляр. Я написал эту проблему и показываю решение. Я показываю для каждого из 5 домов цвет,...
228 просмотров
schedule
05.04.2022
Разница между функцией и предикатом в сплаве 4?
Мне трудно понять разницу между предикатами и функциями в Alloy 4. Я прочитал раздел 4.5.2 в «Абстракциях программного обеспечения», но мне все еще не ясно. Может ли кто-нибудь помочь мне понять?
754 просмотров
schedule
18.04.2022
Ошибка типа в спецификации сплава
В статье «Разработка требований» (2007 г.) «Развитие требований в фреймах задач» есть проработанный пример задачи о светофорах, который я транскрибировал в редакторе Alloy. К сожалению, при тестировании кода я получаю следующую ошибку.
Запускаем...
272 просмотров
schedule
20.04.2022
Сплав - рефлекторно-переходное закрытие включает посторонние элементы
Итак, у меня есть это mwe:
abstract sig S { r: set S }
one sig A, B extends S {}
one sig C { }
run { r = A->B and A->A + B->B + A->B = *r }
Где я ожидал бы, что рефлексивно-транзитивное замыкание будет A->A + B->B +...
209 просмотров
schedule
25.04.2022
Сравнение элементов Alloy Analyzer из набора
Немного предыстории: мой проект состоит в том, чтобы сделать компилятор, который компилирует C-подобный язык в Alloy. Язык ввода, имеющий синтаксис, подобный Си, должен поддерживать контракты . На данный момент я пытаюсь реализовать операторы if,...
119 просмотров
schedule
29.04.2022
Как получить ограничение множественности «один» с помощью языка Alloy Kernel?
Я читал Приложение C: Семантика ядра книги Software Abstraction (автор Дэниел Джексон, второе издание, очень приятно читать, кстати!) и обнаружил, что немного застрял в понимании того, как получить ограничение множественности one , используя другие...
63 просмотров
schedule
10.05.2022
Как перебирать решения с помощью Alloy API?
Я использую Alloy, используя его API, как описано в Alloy — создание экземпляра .xml из .als .
Я хочу перебрать все решения.
Как это сделать?
219 просмотров
schedule
22.05.2022
Экземпляр не найден при использовании seq
Меня озадачивает тот факт, что Alloy сообщает No instance found для этой модели, используя seq :
one sig Const {
T: seq (seq Int)
}
fact const_facts {
Const.T = {
0 -> {0->1 + 1->9} +
1 -> {0->3 + 1->15}
}
}...
43 просмотров
schedule
22.05.2022
прохождение A4Solution
В настоящее время я использую API Alloy в своем проекте, и мне нужно отобразить A4Solutions. Я могу легко сделать это с помощью визуализатора, который предоставляет Alloy (vizGUI), но он слишком ограничен для моей цели. Поэтому я хочу генерировать...
284 просмотров
schedule
05.06.2022
От CompModule к Alloy
Используя Alloy API, можно получить из файла сплава CompModule, который содержит все, что вам нужно, чтобы поиграть с данным модулем сплава.
Это легко достигается с помощью: CompUtil.parseEverything_fromFile(...)
Мой вопрос сейчас следующий....
94 просмотров
schedule
13.06.2022
Моделирование полностью связного графа в Alloy
Я пытаюсь намочить ноги с помощью Alloy (также относительно нового для формальной логики), и я пытаюсь начать с полностью связанного графа узлов.
sig Node {
adj : set Node
}
fact {
adj = ~adj -- symmetrical
no iden & adj -- no...
690 просмотров
schedule
29.06.2022
Почему производительность проверки согласованности двух моделей в Alloy не отличается?
У меня есть две модели, как показано ниже. Первый описывает модель. Пол узла и связанные с ним ребра и ограничения удалены во второй модели.
//Signatures for nodes
sig NPerson{}
abstract sig NGender{}
abstract sig NCivilStatus{}
lone sig...
76 просмотров
schedule
01.07.2022
