Описание тега event-b
Формальный метод моделирования и анализа на системном уровне. Его ключевыми особенностями являются использование теории множеств в качестве нотации моделирования, использование уточнения для представления систем на различных уровнях абстракции и использование математического доказательства для проверки согласованности между уровнями уточнения.
2
ответа
event-b: возможно ли сгенерировать последовательность из... в... простых чисел через лямбду в одном выражении?
Интересно, возможно ли сгенерировать последовательность простых чисел с одним лямбда- выражением в событии b? Это то, что я до сих пор: @axm1 primeSet = {x∣ x ∈ 1‥100 ∧ ¬(∃y·y < x ∧ y > 1 ∧ x mod y = 0)} ∧ finite(primeSet) @axm2 primeSeq ∈ 1‥c…
07 фев '14 в 10:31
1
ответ
Событие B, формальное моделирование: как повлиять на все элементы набора в отношении
У меня довольно много проблем с Event-B.. Я хотел бы установить связь между группой клиентов и номером клиента каждый У меня есть отношение этого типа: cli(PERSON) = NAT1 (Персона - это конечное множество) и в случае, если у меня есть подмножество ч…
26 апр '15 в 10:16
1
ответ
Event-B Доказательства Обязательства
У меня в Event-B проблема с выполнением доказательств. В своей работе я хочу формализовать спецификацию требований защиты памяти, чтобы проверить их соответствие. Чтобы сделать это, я использовал Event-B Context для формализации структуры системы и …
18 июл '17 в 07:32
1
ответ
Моделирование отношений в Event-B
У меня есть вопрос следующим образом: Класс начальной школы содержит множество детей и множество книг. Напишите модель, которая отслеживает книги, которые прочитали дети. Следует поддерживать связь между детьми и книгами. Итак, у меня есть свой конт…
18 мар '14 в 13:58
0
ответов
Как визуализировать большое количество кода в Pro-B
У меня проблема с визуализацией большого количества кода в ProB. На этом графике показан раздел входа в систему сервера с (используя dotv от Graphviz) ProB, но не существует решения для большого количества кода для получения графика. Пожалуйста, дай…
10 авг '16 в 05:40
1
ответ
Платформа Родена Event-B, отношение Подмножества моделирования
Я новичок в Event-B, и я пытаюсь смоделировать машину, где набор PERSONNE включает в себя набор CLIENT, который включает в себя набор RESIDENT... Я искал документацию Родена, но ничего не нашел.. Вот контекст context contexteHumain sets PERSONNE CLI…
04 апр '15 в 13:30
1
ответ
Событие B Общая функция
У меня есть вопрос следующим образом: Класс начальной школы содержит множество детей и множество книг. Напишите модель, которая отслеживает книги, которые прочитали дети. Следует поддерживать связь между детьми и книгами. Он также должен обрабатыват…
19 мар '14 в 00:07
2
ответа
Получение простого / следующего состояния переменной
Учитывая некоторое условие, я хочу проверить, что переменное следующее состояние выполняется для некоторого предложения. Я не смог создать то, что Роден принял. Мой точный случай - следующий инвариант. Я хочу убедиться, что переменная door никогда н…
11 дек '15 в 11:20
1
ответ
Как исправить неизвестную конфигурацию org.animb.valuation.valBase в моем проекте Rodin Platform Event-B?
Я импортировал полностью уточненную модель в мою последнюю версию Платформы Родена, и я пытаюсь использовать IUMLB с аниматором ProB в этом проекте. Но так как в проекте уже был предварительно настроенный аниматор AnimB, который не поддерживается по…
29 мар '19 в 15:35
1
ответ
Обязательство по подтверждению полной функции Event-B
У меня вопрос следующий: Набор A определена и общая функция X с инвариантным типом X ∈ A --> BOOL и событие A_setSate: A_setSate = WHEN X(A) = TRUE THEN X(A) := FALSE проблема в том, что доказательство сохранения события обязательства (INV) A_set…
25 сен '19 в 10:58
1
ответ
Как заполнить отношение аксиомой в событии b
Итак, у меня есть проект Rodin event-b, и я хотел бы определить известную статическую связь. В качестве примера, допустим, у меня есть набор {a,b,c}, и я хотел бы указать константу отношения, которая равна {(a,1),(a,2),(b,3)} в аксиома контекста. (М…
29 май '20 в 12:55
0
ответов
Как смоделировать OIL_TANK
У меня есть эта проблема ниже: Что я пытаюсь смоделировать детерминистический нефтяной резервуар, и я использую Rodin для моделирования этого. Дело в том, что у нас есть масляный бак, уровень которого будет между 20 и 40 единицами. И у нас есть клап…
08 апр '22 в 14:20
0
ответов
Платформа Event-B Rodin, Моделирование отношений для гостиничной системы
Я новичок в Event-B и пытаюсь смоделировать гостиничную систему. В контексте у меня есть набор комнат для бронирования Клиент, который может сделать бронирование, регистрацию, выезд и отмену. У меня также есть Разрешение, когда комната пуста или зан…
22 мар '22 в 19:50
1
ответ
Доказательство инструмента Родена - транзитивность
Итак, я знакомлюсь с языком спецификации event-b и инструментом Rodin. При этом я столкнулся с каким-то странным поведением инструмента Rodin, и я хотел бы получить здесь помощь. Я занимаюсь доказыванием, и у меня есть две гипотезы: 1 <= v v <…
19 июл '22 в 15:24
0
ответов
как получить набор двух концов отношения в теории множеств
Вот у меня есть отношениеr ∈ A ↔ B, и если бы я только знал оrкак мне получить наборAиB? Является ли это возможным? На самом деле я сомневаюсь, что это можно сделать в соответствии с тем, что я знаю, а если это невозможно, мне нужно найти какие-то н…
18 ноя '23 в 12:25
0
ответов
как обрабатывать несколько упорядоченных пар в Event-B
Я хочу получить два последних сопоставленных элемента детерминированной троичной упорядоченной пары в виде двоично упорядоченных пар, вот пример:set A = { 1 ↦ 2 ↦ 3,1 ↦ 5 ↦ 6} ,Я хочу получитьset B = {2 ↦ 3, 5 ↦ 6} ,Что я должен делать? Кстати: это …
27 окт '23 в 01:51