Условия дела не являются исчерпывающими?

Я пишу два модуля в NuSMV, но получаю сообщение об ошибке «Условия случая не являются исчерпывающими». Эта ошибка указывает на последний оператор случая, который у меня есть в коде. Я не уверен, как это исправить, потому что те случаи, которые у меня есть в настоящее время, - это единственные случаи, которые требуются для переменной. Первый модуль «поезд» создается дважды, так что два поезда могут находиться на одном пути. Модуль «контроллер» действует как контроллер, который получает входные данные от двух поездов и не позволяет им обоим находиться на мосту одновременно.

Вот код:

MODULE main
VAR
  trainE : Train(controller1.signalE);
  trainW : Train(controller1.signalW);
  controller1 : controller(trainE.out, trainW.out);

  INVARSPEC(!(trainE.mode = bridge & trainW.mode = bridge))
MODULE Train(signal)
    VAR 
    mode: {away, wait, bridge};
    out: {None, arrive, leave};
    ASSIGN
        init(mode) := away;
        init(out) := None;

        --Task A1
        next(out)  := case
                    mode = away: arrive;
                    mode = bridge: leave;
                    TRUE: None;
        esac;

        --Task A2
        next(mode) := case
                    mode = away & next(out) = arrive: wait;
                    mode = bridge & next(out) = leave: away;
                    mode = wait & signal = green: bridge;
                    TRUE: mode;

        esac;

MODULE controller(outE, outW)
    VAR
        signalE: {green, red};
        signalW: {green, red};
        west: {green, red};
        east: {green, red};
        nearE: boolean;
        nearW: boolean;
    ASSIGN
        init(west):= red;
        init(east):= red;
        init(nearW):= FALSE;
        init(nearE):= FALSE;

        --Task A1
        next(signalW):= west;

        --Task A2
        next(signalE):= east;

        --Task A3
        next(nearE):= case
                        outE = arrive: TRUE;
                        outE = leave: FALSE;
                        esac;
        next(nearW):= case
                        outW = arrive: TRUE;
                        outW = leave: FALSE;
                        esac;
        next(east):= case
                        next(nearE) = FALSE: red;
                        west = red: green;
                        esac;
        next(west):= case
                        next(nearW) = FALSE: red;
                        east = red: green;
                        esac;

model-checking nusmv
person Flower    schedule 11.03.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

На самом деле у вас одна и та же ошибка во всех case условиях:

file test.smv: line 68: case conditions are not exhaustive
file test.smv: line 64: case conditions are not exhaustive
file test.smv: line 60: case conditions are not exhaustive
file test.smv: line 56: case conditions are not exhaustive

Рассмотрим ошибку в строке 56. Вы написали следующие случаи:

next(nearE) := case
    outE = arrive : TRUE;
    outE = leave  : FALSE;
esac;

Теперь outE является входом, подключенным к trainE.out. Внутри модуля Train out объявляется как переменная, которая может иметь 3 возможных значения: {None, arrive, leave}. Однако в коде вы указываете будущее значение nearE только для двух возможных текущих значений outE. Поэтому NuSMV справедливо жалуется, потому что не знает, какое значение должно быть присвоено nearE в следующем состоянии, когда в текущем состоянии outE равно None.

Таким образом, чтобы исправить эту ошибку, вы должны подумать, что бы вы хотели, чтобы произошло, когда outE = None, и добавить эту спецификацию в свою модель.

В случае, когда вы не хотите, чтобы значение nearE менялось, обычной практикой проектирования является добавление условия охвата всех случаев следующим образом:

next(nearE) := case
    outE = arrive : TRUE;
    outE = leave  : FALSE;
    TRUE          : nearE;
esac;
person Patrick Trentin    schedule 12.03.2017