Вопросы по теме 'alloy'
Alloy API приводит к ошибке java.lang.UnsatisfiedLinkError
В настоящее время я использую Alloy Analyzer API для создания программы и получаю какое-то странное поведение. В частности, если я открою файл и проанализирую его (используя CompUtil.parseEverything), затем создам новую команду и вызову...
663 просмотров
schedule
15.10.2022
Значение ключевого слова «частное» в Alloy? Значение объявления enum?
грамматика Alloy 4 позволяет объявлениям подписи (и некоторым другим вещам) нести ключевое слово private . Это также позволяет разрешать спецификации содержать объявления перечисления в форме
enum nephews { hughie, louis, dewey }
enum ducks {...
778 просмотров
schedule
07.02.2024
Встроенные целочисленные математические функции Alloy не работают в импортированных файлах.
У меня есть модель сплава в avlTree.als. В этой модели используется целочисленная арифметика, в частности, функции плюс и минус. В этой модели есть несколько утверждений, и я могу легко запустить их с помощью графического интерфейса Alloy Analyzer....
488 просмотров
schedule
03.06.2023
факты отношения сплава
Ниже часть моей работы на данный момент. По какой-то причине я получаю циклы и двусторонние соединения между моими линиями и одиночные соединения из сообщений в строки. Я не понимаю, почему никогда не бывает более одного сообщения для линейных...
266 просмотров
schedule
18.06.2023
модель сплава для углеводородов
мне нужно смоделировать структуру углеводорода, используя сплав, в основном мне нужно спроектировать алкановые, алкеновые и алкиновые группы, которые я создал следующие сигнатуры (пример алкена)
sig Hydrogen{}
sig Carbon{}
sig alkenegrp{
c:one...
197 просмотров
schedule
30.04.2023
Возможна ли минимизация затрат в 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
}
//...
187 просмотров
schedule
15.02.2023
Подсчет количества Total CounterExamples в Alloy
Вызов
Kodkod.execute()
метод возвращает объект A4Soluiton , который мы можем повторять с помощью метода next() , пока он не достигнет контрпримера, который является неудовлетворительным() . Таким образом, мы можем подсчитать общее...
208 просмотров
schedule
18.01.2023
полезно/естественное неожиданное поведение в сплаве
Я попробовал следующий фрагмент Alloy4 и обнаружил, что меня смущает поведение модуля util/Natural. Комментарии объясняют более подробно, что было неожиданным. Я надеялся, что кто-то может объяснить, почему это происходит.
module weirdNatural...
275 просмотров
schedule
20.04.2023
Генерация явно несовместимых экземпляров сплава
Я делаю метамодель в сплаве для подмножества Java.
Ниже у нас есть несколько подписей:
abstract sig Id {}
sig Package{}
sig ClassId, MethodId,FieldId extends Id {}
abstract sig Accessibility {}
one sig public, private_, protected extends...
131 просмотров
schedule
19.02.2023
Как смоделировать оператор по модулю в сплаве?
Как смоделировать оператор по модулю в сплаве?
Я хочу попробовать сплав, чтобы доказать, что любое число, кратное 4, делится на 2....
Вот мой код..
//proof that 4n is divisible by 2
module I4nDivisibleby2
sig num {}
fact...
130 просмотров
schedule
06.11.2022
Это имя неоднозначно из-за нескольких совпадений:
У меня есть модель Alloy, у которой есть 2 подписи, у которых есть отношение с одинаковым именем.
sig Model {
components : set Component
}
sig Port extends Element {
belongsTo : Component
}
sig Component extends Element{
belongsTo :...
369 просмотров
schedule
14.11.2023
Как добавить ограничения на поля подписи, когда в модели два экземпляра
У меня есть следующая модель Alloy, которая описывает группу людей. упростить задачу. Вот пример фрагмента кода.
sig groupofpeople {
member: set person,
country: Country
}{
#person=2
}
sig people {
teamleader: Bool,
position: String
}...
86 просмотров
schedule
23.05.2023
Как проверить эквивалентность двух предикатов?
У меня есть две разные реализации для определенного предиката, и я хочу проверить, возвращают ли они оба один и тот же экземпляр, как я могу этого добиться?
Спасибо.
407 просмотров
schedule
04.01.2023
Почему возможен сплав отрицательной кардинальности
Я описываю некоторые модели на языке Alloy. Чтобы описать конечный автомат, я предоставил несколько строк кода:
sig FSA_state {
transitions: some FSA_state,
initial: lone InitialState
}
sig InitialState {}
fact i {
all f: FSA_state...
328 просмотров
schedule
21.10.2022
Решатель сплавов не имеет плавающего типа
Я пытаюсь написать задачу Alloy, в которой у меня есть набор состояний и переходов между ними. Моя цель — найти переходы между состояниями. Кроме того, каждое состояние s имеет значение, называемое X(s), которое можно вычислить, используя значение X...
421 просмотров
schedule
12.06.2024
Alloy: факты и т. д. о Int
я недавно работаю с Alloy. Могу ли я сказать что-то вроде:
fact{
all i: Int | i >= 0
}
Я хочу сказать: все Integer, которые использует Alloy, должны быть положительными. Alloy не подводит, но и экземпляров мне не дают.
Привет
1340 просмотров
schedule
26.01.2023
Значение квадратных скобок в спецификации грамматики Alloy
В спецификации грамматики Alloy на веб-сайте Alloy я запутался. с помощью квадратных скобок.
В постановке, подобной следующей, все кажется ясным.
specification ::= [module] open* paragraph*
Я предполагаю, что квадратные скобки указывают...
172 просмотров
schedule
27.07.2022
Кодирование семантики абстрактных ключевых слов в Alloy с помощью ограничений
Я хотел бы закодировать семантику ключевого слова abstract как ограничение в Alloy (проявите терпение, мне нужно сделать это не просто так! :) ). если у меня есть следующий код:
abstract sig A {}
sig a1 extends A{}
sig a2 extends A{}
Я...
116 просмотров
schedule
08.03.2023
Простой конечный автомат в сплаве
Я новичок в сплаве и его функциях. Недавно у меня было задание о простой машине состояний: begin_state->normal_state->end_state. Есть только одно begin_state, но несколько normal_state и несколько end_state. Тогда я не могу заставить представление...
391 просмотров
schedule
23.01.2023
операция xor в Alloy
Есть ли в сплаве операция xor, если нет, то как ее определить:
Я хотел бы иметь предикат с именем xor, который получает два предиката в качестве аргумента и остается истинным, когда их xor остается истинным.
более подробно, если у меня есть P1 и...
869 просмотров
schedule
05.12.2022
