Promela, Испин: модель проверки Promela моделирования со спином - PullRequest
Новая
       44

Promela, Испин: модель проверки Promela моделирования со спином

0 голосов
/ 10 февраля 2019

Я работаю над проверкой проверки модели с использованием средства проверки модели вращения при каждом запуске кода. Я получаю сообщение об ошибке:

spin: traffic_controller: 12, ошибка: необъявленная переменная: to_green saw '') '= 41'

дочерний процесс завершился ненормально, и я уже объявил это.Я использую спин версию 6.4.9 

proctype traffic_controller(int id; int red; int green; int yellow)
{
    bool event_flag = false;
    int neighbor_id , send_node_id , interval ;
    byte circular_ch[4];
    mtype  msg_signal  ;
    end_1 :
    do
    ::circular_ch[ id ]?msg_signal (send_node_id);
        if
        :: ( msg_signal == to_green ) ;
            green_state:
            if
                :: interval = GREEN_INTERVAL0 ;
                :: interval = GREEN_INTERVAL1 ;
                :: interval = GREEN_INTERVAL2 ;
            fi;
            set (clock [id] , interval) ;
            red_activated_region_end :
            red_signal [id] = false ;
            green_activated_region_start ;
            green_signal [id] = true ;
            if
                :: ( expire ( clock [id] ) ) -> clock [id] = ZERO;
                green_activated_region_end :
                green_signal [id] = false ;
                goto yellow_state ;
            fi;
            yellow_state :
            set ( clock [id] , YELLOW_INTERVAL ) ;
            yellow_activated_region_start ;
            yellow_signal [id] = false ;
            if
                :: ( expire ( clock [id] ) ) -> clock [id] = ZERO ;
                yellow_activated_region_end :
                yellow_signal [id] = false ;
                if
                    :: (id != NUM_NODES-1) -> neighbor_id = id+1 ;
                    ::else -> neighbor_id =ZERO;
                fi;
                red_signal [id] = true;
                red_activated_region_start :
                circular_ch [ neighbor_id ] ! to_green (id) ;
            fi;
        fi;
    od;
}

init
{
    run traffic_controller();
    mtype : msg_signal = { to_green, pear, banana }
}

1 Ответ

0 голосов
/ 15 марта 2019

Две проблемы с этим:

  1. Объявить msg_signal глобально, а не main.
  2. Вы оставили много неопределенным (например, GREEN_INTERVAL0, YELLOW_INTERVAL, set, clock)
...