Описание тега tlc
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
ответ
Можно ли использовать tlc при проектировании потоков состояний в MATLAB Simulink?
TLC может быть сохранен в виде текстового файла и имеет tracebilty. Возможно ли использовать tlc в дизайне потока состояний? Или любое другое предложение сохранить функцию tracebilty в проекте sateflow?
26 янв '19 в 11:18
2
ответа
Как я могу назначить последовательности константам в разделе CONSTANTS файла конфигурации TLA+?
Я пробовал CONSTANTS seq = <<5,6,7>> но TLC дает мне синтаксическую ошибку: Ошибка: TLC обнаружил ошибку в файле конфигурации в строке 1. Он ожидал = или <- и не нашел ее. Я также попытался включить Sequences Модуль в файле конфигурации,…
21 май '10 в 06:59
0
ответов
Что здесь означает четвертая позиция?
Я делаю файл .tlc, и у меня такая ситуация в гипотетической модели: Цикл: CompiledModel.DWorks Я получаю this_dwork за каждое взаимодействие: %foreach i = CompiledModel.DWorks.NumDWorks %assign this_dwork = CompiledModel.DWorks.DWork[i] Я в DWork по…
01 янв '19 в 21:07
0
ответов
TLA+ Как визуализировать граф состояний
Я новый TLA+ пользователь. Я читал, что TLA Панель инструментов позволяет нам визуализировать график состояния после завершения проверки модели. Для этого нужно установить точку, что я и сделал. Но я не понял, как запустить визуализацию. Могу ли я к…
28 авг '18 в 10:29
0
ответов
Ошибка: неопределенные параметры в файле TLC при попытке развернуть модель Simulink в Arduino
В то время как я пытаюсь развернуть модель Simulink в Arduino Mega 2560, эти ошибки возникают. Я использую версию Matlab 2017B Educationla, и модель содержит функцию Matlab M s. В последние несколько месяцев я смог сгенерировать tlc-файл из этой s-ф…
25 фев '18 в 07:51
0
ответов
Как я могу устранить ошибку TLC, которую я получаю при построении моей модели для ControlDesk в Simulink 2015b?
Я получаю следующую ошибку во время генерации кода при попытке построить мою модель: No implementation for 'Scope' has been defined in 'C:\Program Files\MATLAB\R2015b\rtw\c\tlc\mw\genmap.tlc'. --------------------------------------------------------…
09 авг '18 в 07:37
1
ответ
Модель запуска ошибки TLA+ на панели инструментов: переопределенное значение Nat
В течение нескольких дней я сталкивался со следующей ошибкой в наборе инструментов TLA+ в различных контекстах: "Attempted to compute the number of elements in the overridden value Nat.". Ниже приведен простейший модуль, который я придумаю и котор…
15 окт '17 в 22:24
1
ответ
Python IDLE не открывается из-за ошибки Tcl/tk
Я только что установил последнюю версию Python 3.6.5 с python.org. Я использую 64-битную Windows 8.1 . Раньше он показывал все виды ошибок.DLL, я пытался установить все обновления и C++ Redistributable, но ничего не произошло, потом я вручную загруз…
19 апр '18 в 13:37
0
ответов
TLC не может справиться с этим соединением спецификации
У меня есть модуль TLA+, который в итоге выглядит следующим образом: --- MODULE Group --- CONSTANTS People VARIABLES members Join(person) == ... Leave(person) == ... Init == members \subseteq People Next == \E p \in People : \/ Join(p) \/ Leave(p) =…
22 ноя '18 в 02:25
1
ответ
Как использовать самозаверяющий сертификат для перехвата зашифрованного трафика с клиента на какой-либо веб-сайт?
Для моего курса Internet Security мне был предложен проект, в котором я должен в конечном итоге воспользоваться "запомни свой пароль" на сайте, создав сертификат, вручную поместив его в свой "клиентский" браузер, чтобы получить доверие, а затем имет…
16 апр '19 в 02:33
0
ответов
Библиотека C TLC5971
Есть ли у кого-нибудь библиотека C для TLC5971? Или знал, как преобразоватьArduino library использовать это в Mbed compiler? Я нашелArduino library но я использую STM32 Nucleo доска и Arduino library не работайте в mbed combiler.
04 мар '20 в 15:32
0
ответов
Как получить параметр S-функции в качестве вывода блока в файле .tlc
Я отхожу от S-функции ver_file_data.c, где я получаю определение параметра в диалоговом окне блока. #define DVC_TYPE(S) ssGetSFcnParam(S, 0) А потом внутри mdlRTW (SimStruct *S) unsigned char dvc_tp = *mxArrayToString(DVC_TYPE(S)); if (!ssWriteRTWSc…
21 окт '19 в 15:50
1
ответ
Как исправить эту ошибку __init__ self.init_window()
Я начал настраивать свой графический интерфейс с помощью pyCharm, но столкнулся с некоторыми ошибками при компиляции после добавления строки меню. Я удалил весь код, относящийся к строке меню, и он работает, но не помогает, поскольку я хотел бы доба…
18 окт '19 в 21:42
1
ответ
Как прервать работу файла порта macports при возникновении ошибки?
Я работал над повышением версии на cc65 и столкнулся с проблемой с linuxdoc-tools. Поскольку я не могу исправить linuxdoc-tools и есть простой способ обхода, я решил добавить оператор if, чтобы проинформировать пользователя вместе с обходным путем: …
03 окт '20 в 12:10
1
ответ
Почему TLC сообщает об ошибках в действительных состояниях?
У меня есть следующая спецификация очереди: ------------------------------- MODULE queue ------------------------------- EXTENDS Naturals CONSTANT L (* The fixed max length of the queue *) VARIABLE q (* Represents the queue as the number of items in…
22 ноя '20 в 12:40
0
ответов
Tcl/Tk отправка электронной почты с smtp и mime с вложениями, не отображающими прикрепленное имя файла
Я могу отправлять электронные письма с помощью smtp и mime с вложением, но когда я читаю письмо, у прикрепленного файла нет имени. Мой код выглядит следующим образом: set messageT [mime::initialize -canonical text/plain -string $TEXT] set pdfT [mime…
25 апр '21 в 23:33
0
ответов
Сигнальный конверт
Я хотел понять, как я могу рассчитать огибающую сигнала, если у меня есть следующие данные, доступные в моем файле Excel Далее я хотел бы изобразить это графически. Спасибо вам всем.
05 янв '22 в 14:43
0
ответов
Ошибка выполнения при отправке в Hacker Earth Проблема: циклические смены
Постановка задачи в HackerEarth: Большое двоичное число представлено строкой A размера N, состоящей из нулей и единиц. Вы должны выполнить циклический сдвиг этой строки. Операция циклического сдвига определяется следующим образом: Если строка A равн…
26 янв '22 в 14:38
1
ответ
Ошибка TLA+: инвариантные инварианты не являются предикатом состояния
В моей спецификации я пытаюсь проверить, является ли изменение в последовательности -1, 0 или 1. Я описал этот инвариант следующим образом: PVariance == Len(waitingRoomP') - Len(waitingRoomP) \in {-1,0,1} CVariance == Len(waitingRoomC') - Len(waitin…
03 мар '21 в 20:01