Вопросы по теме 'alloy'
Alloy Analyzer 4.2 (mac) по сравнению с API сплава
В настоящее время я делаю программу, которая обрабатывает некоторые аннотации в java, а затем создает модель сплава, анализирует ее с помощью API сплава, а затем запускает некоторые команды сплава. Когда я тестирую сгенерированную модель сплава в...
700 просмотров
schedule
28.02.2023
значение предиката Alloy в реляционном соединении
Рассмотрим следующий простой вариант примера с адресной книгой.
sig Name, Addr {}
sig Book { addr : Name -> Addr } // no lone on Addr
pred show(b:Book) { some n : Name | #addr[b,n] > 1 }
run show for exactly 2 Book, exactly 2 Addr, exactly 2...
389 просмотров
schedule
29.10.2022
Реализация Enqueue и Dequeue для Queue с помощью Alloy
Имея следующее:
sig Queue { root: Node }
sig Node { next: lone Node }
fact nextNotReflexive { no n:Node | n = n.next }
fact nextNotCyclic { no n:Node | n in n.^next }
Может кто помочь по реализации Enq и Deq?
pred Enq[q,q':Queue,...
364 просмотров
schedule
24.09.2022
Вставка и удаление в связанных списках в сплаве
Я создал простую версию связанного списка, используя сплав. Теперь я хочу создать связанный список, в котором я мог бы выполнять вставку и удаление. Я только начал кодировать в сплаве. на данный момент у меня возникают проблемы при выполнении...
1054 просмотров
schedule
15.06.2022
Лучшая практика использования логического значения в модели Alloy
Я создаю простой Alloy для создания простых объектов Java Pojo, и некоторые поля этого pojo являются логическими значениями. Теперь я использую следующий механизм для достижения этой функции
one sig item {
autoPay: String,
Price: Int
}...
2361 просмотров
schedule
10.12.2023
Сплав: используйте для String
Как я могу взять длину строки в сплаве?
Если я хочу сказать, что пароль должен состоять как минимум из 8 символов, как я могу выразить длину этой строки?
Моя подпись пароля:
sig Password{пароль: одна строка}
430 просмотров
schedule
25.11.2022
Программирование рекурсивных функций в сплаве
Я пытаюсь построить рекурсивную функцию в Alloy. Согласно грамматике, представленной в книге Дэниела Джексона, это возможно. Моя функция:
fun auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method]: Method{
(m.b.id = idTarget) => {...
1122 просмотров
schedule
22.09.2023
Сплав — единственный экземпляр
Я пишу простой код Alloy, но я не могу понять, как я могу сказать, что МАКСИМАЛЬНО один A связан с pD (так что МАКСИМАЛЬНО будет единица или ноль). Итак, я написал приведенный ниже код, но утверждение не представляет нет контрпримера с экземпляром...
295 просмотров
schedule
01.04.2024
Как обновить установленный размер модели сплава, чтобы он находился в определенном диапазоне?
Если у меня есть модель Alloy в следующем формате
one sig player {
name: String,
spot: set position
}
sig position {
Attack: Bool,
accuracy: int,
strength: int,
}
Если я хочу иметь определенное правило, чтобы каждый...
644 просмотров
schedule
26.03.2023
Проблема с памятью в Alloy
Я новичок в Alloy. Я пытаюсь найти решение для модели с 512 состояниями. Но у него заканчивается память. Я установил память и стек на максимальный уровень, но этого недостаточно. Есть ли другой способ увеличить объем памяти, которую использует...
94 просмотров
schedule
03.06.2024
Синтаксис ограничений в предикате и в утверждении
Я хочу знать, отличается ли синтаксис ограничений при использовании в предикате, чем в утверждении.
Ограничение все disj x1,x2:X | x1 =x2 дает разные результаты при выполнении в предикате и в утверждении.
Например, предположим следующую...
176 просмотров
schedule
11.10.2022
Синтаксис сплава для остаточных типов?
Есть ли прямой способ представить тип остатка в Alloy вместо того, чтобы явно вычитать объединение всех подтипов? Например, в:
sig Test {}
one sig A, B extends Test {}
Я хотел бы иметь возможность ссылаться на выражение Test-(A+B) с...
126 просмотров
schedule
28.04.2023
Почему оператор Plus не работает с целыми числами в Alloy?
приведенный ниже код сплава предназначен для проблемы с 8 ферзями Я не знаю, почему оператор плюс и минус не работают правильно поэтому после выполнения есть ферзи на той же диагонали Более того, я сталкиваюсь с этой ошибкой при использовании плюс и...
179 просмотров
schedule
05.03.2023
Количественное определение определенного количества элементов в наборе
Итак, у меня есть предикат, который принимает набор в качестве аргумента, и поэтому я могу сделать это:
all disj t1, t2, t3: set Thing | predicate[t1+t2+t3]
Мне было интересно, можно ли это сделать, просто указав размер набора, так что что-то...
438 просмотров
schedule
24.11.2022
Преобразование выражения высшего порядка в логику первого порядка сплава
Я хотел бы написать взаимно однозначное соответствие между набором и отношением в Alloy.
Например, в следующем коде я хотел бы определить ref как соответствие между QArrow и событием. Поэтому пишу факт bij . Но Alloy жалуется, так как я думаю,...
152 просмотров
schedule
23.02.2023
Как повторно использовать факты с помощью модулей в Alloy
У меня есть следующая спецификация в Alloy:
sig A {}
sig Q{isA: one A}
fact {
all c1,c2:Q | c1.isA=c2.isA => c1=c2 // injective mapping
all a1:A | some c1:Q | c1.isA=a1 //surjective
}
В моих моделях вышеуказанный факт...
139 просмотров
schedule
18.07.2023
связанный список, нет двух одинаковых элементов
sig List {
header: set Node
}
sig Node {
link: set Node,
elem: set Int
}
Я не хочу, чтобы два узла указывали на один и тот же элемент. Как этого добиться?
Я не очень понимаю оператор *, но я пытался
all n: Node | n.elem !=...
230 просмотров
schedule
26.12.2022
Понимание мощности сплава
Я не смог понять кардинальность сплава. Я сократил свой код до этого тривиального примера, для которого Alloy не может найти экземпляр:
sig A {}
sig B { s: set A}
fact x { one n: Int | all b: B | #(b.s) = n }
run {} for 10
А именно, что...
659 просмотров
schedule
20.11.2023
Как использовать Alloy для поиска ошибок в архитектуре программного обеспечения
Я получаю огромное удовольствие от изучения Alloy и рад возможности применить его в некоторых программных проектах, над которыми работаю.
В прошлом я неформально использовал облегченные формальные методы, чтобы записать в логике первого порядка...
224 просмотров
schedule
15.01.2023
Как построить рекурсивные предикаты/функции в Alloy
Я пытаюсь сгенерировать в Alloy два набора классов, например, классы до приложения рефакторинга и классы после приложения рефакторинга. Предположим, в первом наборе у нас есть следующие классы:
ALeft -> BLeft -> CLeft...
589 просмотров
schedule
25.11.2022
