Сомнительное использование 'else' в сочетании с i/o, увидел ';' рядом с «если»

Ниже приведен код, вызывающий это.

        if 
            :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> 
              proc2clk[0] ? fromProc[0]; // Woke up
            :: (!(fromProc[0] == MSG_SLEEP) && !(fromProc[0] == MSG_FIN)) ->
              clk2proc[0] ! 0;  
            ::else -> 
              time = time + 1; // just for debugging
        fi;

Если я уберу вызов nempty в первом условии, ошибка исчезнет. Из того, что я прочитал, вы не можете использовать оператор else, если вы используете оператор получения или отправки в условии, но из того, что я знаю, пустой - это не оператор отправки или получения, а просто чтобы проверить, не пустой ли канал. Итак, какую ошибку я делаю, и как я могу решить эту проблему.


multithreading promela spin model-checking
person MetallicPriest    schedule 22.02.2014    source источник
comment
Этот код не является ни C, ни C++. Почему вы пометили это как таковое?   -  person David Hammen    schedule 22.02.2014
comment
Потому что Promela генерирует код на C. Хотя я удалил тег C++.   -  person MetallicPriest    schedule 22.02.2014

Ответы (1)


arrow_upward
11
arrow_downward

Это происходит потому, что компилятор Spin переводит else в отрицание всех опций if, а затем, поскольку одна из ваших опций имеет nempty(), переведенная if заканчивается !nempty(), что недопустимо. Например:

if
:: (p1) -> …
:: (p2) -> … 
:: else -> … 
if

переводится на

if
:: (p1) -> … 
:: (p2) -> … 
:: (!p1 && !p2) -> … 
if

Когда p1 или p2 содержит любой из full(), nfull(), empty() или nempty(), выражение !p1 или !p1 будет отрицать один из этих предикатов заполнения/пустоты очереди. Такое отрицание незаконно. См. www.spinroot.com для документации этих предикатов.

Решение состоит в том, чтобы сделать перевод else самостоятельно, а затем, когда вы увидите отрицание, заменить его соответствующим предикатом. Например, если вы хотите:

if
:: a == b && nempty(q) -> …
:: else
fi

затем замените else на (разработку):

!(a==b &&  nempty(q))   => DeMorgan's Laws
 (a!=b || !nempty(q))   
 (a!=b ||  empty(q))

и, таким образом, !nempty() больше не существует в окончательном переводе «от руки»:

if
:: a == b && nempty(q) -> …
:: a != b ||  empty(q))-> …
fi

Если в вашем случае с несколькими сложными вариантами, выполнение «ручного» перевода else будет подвержено ошибкам. Но это то, что вам нужно сделать.

person GoZoner    schedule 23.02.2014