Публикации по теме 'spin'
Напишите SPIN-код для TM1637 и TM1638 (Часть II)
мощные семисегментные микросхемы драйверов
В патенте I этой серии мы сосредоточились на TM1637, его цифровых сигналах и синхронизации. Для сравнения, сигналы TM1638 намного проще. Поскольку у него есть дополнительный STB (так же, как линия CS SPI), нет необходимости в условиях START, END.
Несколько недорогих семисегментных модулей используют TM1638, например QTF-TM1638, модули LED&KEY. Основные функции включают в себя:
8 семисегментных цифр кнопочная клавиатура
Вот схема..
Вопросы по теме 'spin'
Доступ к локальной переменной одного процесса из другого в Promela
Можно ли получить доступ к значению локальной переменной одного процесса из другого процесса. Например, в программе ниже я хочу прочитать значение my_id из менеджера.
proctype user (byte id){
byte my_id = id;
}
proctype manager (){...
797 просмотров
schedule
06.04.2024
Тайм-аут при использовании Spin/Promela
Если бы кто-нибудь мог объяснить мне, почему я получаю тайм-аут со следующим кодом, это было бы здорово. Я понимаю, или, по крайней мере, я думаю, что понимаю идею тайм-аута, но с циклами do я думал, что это остановит это. Любые советы...
1801 просмотров
schedule
04.08.2022
Можно ли распечатать пространство состояний с помощью SPIN?
Я хотел бы, чтобы SPIN распечатывал вычисленное пространство состояний, чтобы я мог сделать его визуализацию, а затем вручную исследовать его. Это возможно?
Я уже проверил такие флаги, как -DCHECK и -DVERBOSE, но думаю, что это не то, что я ищу...
296 просмотров
schedule
24.05.2023
Каковы шаги для проверки LTL с помощью инструмента SPIN?
Я написал модель в Spin. Я хочу проверить некоторые LTL на модель. Например:
ltl L1 {<>[]Working}
в окне проверки я выбираю опцию «использовать претензию» и нажимаю «Выполнить»:
ltl L1: <> ([] (Working))
gcc -DMEMLIM=1024...
3674 просмотров
schedule
15.07.2023
Недостигнутая ошибка в Promela
Для следующего кода
proctype A()
{
byte cond1;
time = time + 1;
time = time + 2;
t[0] = 3;
a[0] = 2;
do
:: (a[0] == 0)->break;
:: else -> a[0] = a[0] - 1;
do
:: (t[0] <= t[1])->break;
od;
if
:: (cond1 != 0)...
536 просмотров
schedule
11.12.2023
представлен в виде утверждения LTl, спин
Извините за мой английский, я из Украины) Только начал изучать проверку спиновой системы. Мы задали следующую задачу: «Представить в форме ниже ЛТЛ выражение: Если я люблю Машу, я не могу любить Дашу». Я не могу понять, как это сделать. Вот что у...
163 просмотров
schedule
16.10.2022
Spin unreachable in proctype -end-
Я новичок в проверке модели вращения и хотел знать, что означает эта ошибка:
unreached in proctype P1
ex2.pml:16, state 11, "-end-"
(1 of 11 states)
unreached in proctype P2
ex2.pml:29, state 11, "-end-"
(1 of 11 states)
вот...
1599 просмотров
schedule
28.02.2024
Promela (ispin) застревает в конце цикла
ну, у меня есть это (это часть кода):
20 proctype Main(byte myID) {
21 do
22 ::int J=0;
23 int K=0;
24
25 atomic{
26 requestCS[myID]=true;
27 myNum[myID]=highestNum[myID]+1;
28 }
29
30 do
31 :: J...
265 просмотров
schedule
12.02.2023
Прохождение по ссылке в Promela
В моем дизайне у меня есть N глобальных переменных и метод, который принимает в качестве параметра некоторые из упомянутых параметров, в зависимости от состояния.
Могу ли я передавать глобальные переменные в качестве параметров по ссылке?
В...
524 просмотров
schedule
05.07.2022
Атомарные предложения Promela для нескольких экземпляров proctype
Мне было интересно, как написать никогда утверждения, которые обозначают все экземпляры proctype. Например, если у меня есть следующее предложение:
#define c (camera_node[SomePid]:start_publishing == 0)
Теперь, если я создам 5 экземпляров...
97 просмотров
schedule
11.07.2023
Как сравнить два LTL?
Как я могу сравнить два LTL, чтобы увидеть, могут ли они противоречить друг другу? Я спрашиваю об этом, потому что у меня есть иерархический конечный автомат и LTL, описывающие поведение в каждом состоянии. Мне нужно знать, может ли локальный LTL...
173 просмотров
schedule
19.07.2022
Синтаксическая ошибка Промелы
Я получаю синтаксическую ошибку, когда пытаюсь запустить свой код promela, ошибка говорит об ошибке: синтаксическая ошибка увидела «токен: ::»
который относится к этой строке кода (строки 10-13):
#define IniRunning(x,y) if...
801 просмотров
schedule
21.10.2022
Результаты вывода SPIN
Я написал код Promela для проверки протокола Needham-Schroeder с использованием SPIN. После запуска случайного моделирования кода я получаю этот вывод:
0: proc - (:root:) creates proc 0 (:init:)
Starting PIni with pid 1
1: proc 0...
264 просмотров
schedule
18.03.2023
Промела - недетерминизм не недетерминирован?
Рассмотрим этот фрагмент:
chan sel = [0] of {int};
active proctype Selector(){
int not_me;
endselector:
do
:: sel ? not_me;
if
:: 0 != not_me -> sel ! 0;
:: 1 != not_me -> sel ! 1;
:: 2 !=...
530 просмотров
schedule
15.07.2023
преобразовать программу fifo systemC на язык PROMELA со свойствами безопасности и живучести
пожалуйста, я большой специалист в области tihs, как я могу преобразовать классический пример FIFO, написанный в коде systemC, в язык PROMELA со свойствами в LTL, удовлетворяющими следующим трем свойствам:
Взаимное исключение: процессы...
288 просмотров
schedule
22.06.2022
Ошибка в операторе select() с встраиванием?
Я бы разместил это в отчетах об ошибках spinroot , но форум spinroot в настоящее время не принимает новых пользователей... Если кто-то, отвечающий за это, читает это, пожалуйста, дайте мне войти :)
Что-то очень странное происходит, когда я...
78 просмотров
schedule
16.05.2023
что такое безусловный цикл в промеле?
Я работаю над проектом, в котором используется SPIN Model checker. SPIN версии 6.4.7 и ispin версии 1.1.4. Я получаю эту ошибку при ispin, говоря:
состояние 76: безусловный цикл
proctype TDMAProtocol(byte id; chan P1, P2, PR)
54 {...
320 просмотров
schedule
06.06.2023
Модель Promela со спином — повторяющееся сообщение и поврежденное сообщение
У меня есть этот код promela, и мне нужно смоделировать дублирование и повреждение сообщений, а также мне нужно добавить механизмы для обнаружения и обработки поврежденных сообщений и дубликатов сообщений.
из моего чтения я обнаружил, что мне нужно...
134 просмотров
schedule
17.09.2022
Проверка модели: почему логика LTL ‹› не дает правильного контрпримера в Spin
Обновлять
В моей предыдущей попытке есть две проблемы. Исправив их, я успешно получаю ожидаемый ответ.
LTL, указанный с помощью параметра -f из командной строки, будет инвертирован. Вместо этого я использую встроенный LTL, добавляя ltl {...
82 просмотров
schedule
11.02.2023
Как я могу определить такой макрос в спине?
Я написал следующую модель:
#define inc(sn)if :: sn < 255 -> sn = sn + 1; ::else -> sn = 1; fi;
#define inc_twice(sn) if :: sn+2 >255 -> sn= sn-253; ::else -> sn=sn+2; fi;
active proctype monitor()
{
byte sn = 255;
assert...
90 просмотров
schedule
05.08.2022
