Дорогие студенты,
Обратите внимание, что изменение оператором значения переменной
(например, в случае присваивания) происходит _после_ выполнения данного
оператора.
Т.е. в тот момент, когда изменился счётчик программы, эффект от
выполнения оператора ещё не наблюдается. Учитывайте это при построении
множества достижимых состояний.
Для удобства лучше всегда добавлять в последовательную программу
"терминальный" оператор, в который переходит управление после выполнения
последнего оператора программы, и в котором наблюдается эффект от
последнего оператора.
С уважением,
Константин Савенков.