Вращение светофора - PullRequest
Новая
       31

Вращение светофора

0 голосов
/ 11 мая 2018

Во-первых, я должен сказать, что я очень новичок в этом, и я должен сделать семафор с некоторыми условиями.

Мы будем моделировать только один светофор для каждого направления (второй просто повторяет то же самое поведение),Например, на картинке выше вертикальный свет - зеленый, а горизонтальный - красный.Первоначально оба направления красные.Когда автомобиль прибывает, он обнаруживается датчиком, и соответствующий ему свет становится зеленым.Однако это происходит только в том случае, если другое направление все еще выделено красным;в противном случае он будет ожидать закрытия другого направления.Как только любое направление станет зеленым, оно станет оранжевым (есть таймер, но мы не будем моделировать задержку), а затем снова станет красным.

На самом деле это мой код прямо сейчас:

mtype = { red, yellow, green };
mtype light0 = red;
mtype light1 = red;

active proctype TL0() {
    do
        :: if
        :: light0 == red -> Ered: atomic {
            light1 == red; /* wait*/
            light0 = green;
        }
        :: light0 == green -> EY: light0 = yellow
        :: light0 == yellow -> EG: light0 =red
        fi;
        printf("The light0 is now %e\n", light0)
    od
}

active proctype TL1() {
    do
        :: if
        :: light1 == red -> Ered: atomic {
            light0 == red; /* wait*/
            light1 = green;
        }
        :: light1 == green -> EY: light1 = yellow
        :: light1 == yellow -> EG: light1 =red
        fi;
        printf("The light1 is now %e\n", light1)
    od
}

Проблема в том, что когда я использую

spin -a -f '<> (! TL0 @ Ered &&! TL1 @ Ered)' sem3.pml

для проверки безопасности я получаю один erorr.

предупреждение: никогда не требовать + принимать ярлыки требует флаг -a для полной проверки предупреждения: для сокращения po действительны утверждения никогдадолжен быть инвариантным к заиканию (утверждения, сгенерированные из формул LTL, никогда не зацикливаются) pan: 1: утверждение нарушено! ((! ((TL0._p == Ered)) &&! ((TL1._p == Ered)))) (на глубине 0) pan: wrote sem3.pml.trail

(версия Spin 6.4.8 - 2 марта 2018) Предупреждение: поиск не завершен + сокращение частичного заказа

полный поиск в пространстве состоянийдля: никогда не требовать + (никогда_0) нарушений утверждений + (если в рамках объема требований) принятие
циклов - (не выбрано) недопустимых конечных состояний - (disподдерживается флагом -E)

Вектор состояния 36 байт, глубина достигнута 0, ошибки: 1 1 состояния, сохранено 0 состояний, сопоставлено 1 переходов (= сохранено + сопоставлено) 0 конфликтов хэша атомных шагов: 0 (разрешено)

Но на самом деле я понятия не имею, в чем проблема: (

Надеюсь, кто-то может мне помочь

Thx!

1 Ответ

0 голосов
/ 11 мая 2018

Модель в порядке, но я бы посоветовал вам вручную создать верификатор.

Сначала добавьте следующие строки внизу вашего файла: 

ltl p1 { <>(!TL0@Ered && !TL1@Ered) };
ltl p2 { [] !(TL0@EY && TL1@EY) };     // perhaps you wanted (something like) this?

Затем сгенерируйте верификатор: 

~$ spin -a file_name.pml
~$ gcc -o run pan.c
~$ ./run -a -N p1
...
~$ ./run -a -N p2
...
...