Описание тега tla+

Описание тега Вопросы с тегом
TLA+ is a language and toolchain for specifications based on TLA, the Temporal Logic of Actions. The TLA Toolbox includes a translator from PlusCal to TLA+, the TLC model checker, and an IDE.
1 ответ

\in работает, в то время как \subseteq выдает ошибку "идентификатор не определен"

У меня есть следующие спецификации: ------------------------------ MODULE Group ------------------------------ CONSTANTS People VARIABLES members Init == members \subseteq People Next == members' = members Group == Init /\ [][Next]_members =========…
22 ноя '18 в 07:42
1 ответ

Сравнение элементов последовательности и набора в TLA+

Дана последовательность S = <<1,2,3,4>> и множество S' = {1,2,3,4,5,6}. Как мы можем проверить, содержат ли они оба одинаковые значения в TLA+?
23 мар '18 в 22:46
1 ответ

Выражая временную логику действий в эрланге. любой естественный способ?

Я хотел бы перевести некоторые действия, указанные в TLA на Erlang. Можете ли вы придумать какой-нибудь естественный способ сделать это непосредственно в Erlang или какую-либо инфраструктуру, доступную для этого? В двух словах (очень маленький), дей…
16 фев '11 в 18:42
1 ответ

Последовательность TLA+ не обновляется вызовами Append или Tail

Эта проблема Я играю с TLA+ и думал, что напишу следующую явно ложную спецификацию в PlusCal: ---- MODULE transfer ---- EXTENDS Naturals, TLC, Sequences (* --algorithm transfer \* Simple algorithm: \* 1. Start with a shared-memory list with one elem…
07 янв '19 в 00:26
1 ответ

Вопросы о постоянном операторе в TLA+

Я недавно читаю книгу "Уточняющие системы". В главе 5 Лесли определяет постоянный оператор Send (,,,). Я не понимаю, как присвоить значение (True/False) этому константному выражению? Нужно ли присваивать True / False каждому (p, v, m, m') в программ…
11 фев '19 в 05:48
1 ответ

Задание нескольких шагов с использованием TLA+ (временная логика действий)

Просмотр здесь в основном показывает простые примеры спецификаций действий, где вы ссылаетесь на следующее состояние, используя ', как в: UponV1(self) == /\ pc[self] = "V1" /\ pc' = [pc EXCEPT ![self] = "AC"] /\ sent' = sent \cup { &lt;&lt;self, "EC…
01 мар '19 в 13:48
1 ответ

Выбор одного элемента из симметричного набора

У меня есть спецификация TLA+ сродни следующему: CONSTANT Items VARIABLE item И я бы хотел Items быть симметричным, и выбрать один элемент из Items и сохранить его в item, Я использую item = CHOOSE x \in Items: TRUE, но я узнал, что это нарушает сим…
15 фев '19 в 22:55
1 ответ

Как я могу утверждать, что число идет или список растет в TLA+?

У меня есть спецификация TLA+, в которой я хотел бы заявить, что список только увеличивается в длину (хорошо, если он остается неизменным при заикании). Прямо сейчас у меня что-то вроде этого, но я уверен, что это не правильно NoWorkIsLost == Len(sa…
03 янв '19 в 20:54
1 ответ

Идеи для проекта TLA+

Пожалуйста, дайте мне несколько советов по теме проекта на языке TLA+. Я прохожу курс по языку, это первый год, когда я изучаю спецификацию и проверку, и я понятия не имею, что выбрать для внедрения через две недели. Есть идеи?
20 май '10 в 06:30
1 ответ

Есть ли в TLA+ инфиксный оператор xor (исключительный или)?

Есть ли в TLA+ оператор xor, определенный как часть самого языка, или я должен определить свой собственный?
11 окт '17 в 22:23
1 ответ

Как утверждать, что данное состояние приводит к другому состоянию с переменными в TLA+?

Извините, заголовок немного загадочный. У меня есть спецификация TLA+, которая определяет два набора: variables Requests = {}, Outcomes = {}; У меня есть один набор работников, добавляющих запросы, и другой набор или работников, выполняющих их и пиш…
11 окт '17 в 15:23
2 ответа

Как я могу назначить последовательности константам в разделе CONSTANTS файла конфигурации TLA+?

Я пробовал CONSTANTS seq = &lt;&lt;5,6,7&gt;&gt; но TLC дает мне синтаксическую ошибку: Ошибка: TLC обнаружил ошибку в файле конфигурации в строке 1. Он ожидал = или <- и не нашел ее. Я также попытался включить Sequences Модуль в файле конфигурации,…
21 май '10 в 06:59
2 ответа

Что такое индуктивный инвариант простой параллельной программы?

Вот простая параллельная программа из статьи Лесли Лампорта " Обучение параллелизму ". Рассмотрим $N$ процессы, пронумерованные от 0 до $N-1$, в которых каждый процесс $ i $ выполняется x[i] := 1 y[i] := x[(i - 1) % N] и останавливается, где каждый …
28 июл '14 в 06:44
1 ответ

Как проверить модель модуля, который зависит от несвязанной переменной?

Я сейчас прохожу через Specifying Systems и немного озадачен тем, как я проверю модель следующего модуля: ---------------------------- MODULE BoundedFIFO ---------------------------- EXTENDS Naturals, Sequences VARIABLES in, out CONSTANT Message, N …
01 фев '18 в 21:07
1 ответ

Как перевести формулу в код TLA+

Я написал спецификацию TLA+ Ханойской башни: TEX ASCII ------------------------------- MODULE Hanoi ------------------------------- EXTENDS Sequences, Integers VARIABLE A, B, C CanMove(x,y) == /\ Len(x) &gt; 0 /\ IF Len(y) &gt; 0 THEN Head(y) &gt; H…
03 апр '16 в 23:08
1 ответ

TLA+ Spec с предположениями о внешних системах

Я пробую TLA+ для проекта на работе. Я хочу доказать, что выборка данных с одним и тем же ключом вернет те же данные, несмотря на некоторые изменения внутренних данных. Для этого я хотел бы смоделировать внешнюю систему как черный ящик, ответы котор…
24 окт '17 в 02:12
0 ответов

TLA+ Как визуализировать граф состояний

Я новый TLA+ пользователь. Я читал, что TLA Панель инструментов позволяет нам визуализировать график состояния после завершения проверки модели. Для этого нужно установить точку, что я и сделал. Но я не понял, как запустить визуализацию. Могу ли я к…
28 авг '18 в 10:29
3 ответа

Разница между => и <=>

Я изучаю TLA+ с этой замечательной страницы "Learn TLA+". Я не могу получить практическую разницу между =&gt; а также &lt;=&gt;, Я понимаю это с точки зрения "таблицы правды", но я не могу этого понять. Можно ли привести практический пример TLA+, по…
11 ноя '17 в 22:10
1 ответ

Проверьте, что ветви выполнены

Программа может переходить из START в левую или правую ветку. Как я могу проверить, что есть путь выполнения для ЛЕВОЙ ветви и другой путь выполнения для ПРАВОЙ ветви? ------------------------------ MODULE WFBranch ------------------------------ VAR…
10 дек '17 в 21:56
2 ответа

LTL, CTL или TLA для моделирования для моей модели (подробное описание внутри)?

В настоящее время я пишу магистерскую диссертацию и сталкиваюсь с определением и проверкой моего подхода во временной логике. Какую временную логику лучше всего использовать в моих обстоятельствах? Мне бы очень хотелось получить отзыв о моем подходе…
03 мар '14 в 12:40