ВПнМ, 10 лекция (от 18 апреля)

Материал из eSyr's wiki.

---

Текущая версия

Пример:

Если мы здесь уберём всё, что касается y, то мы получим корректную модель, касающуюся x. Если же мы уберём один оператор, касающийся y, и будем рассм. модель отн. перем. x и y, то получим некорректную модель. Если мы сделаем абстракцию предиката ветвления, то несмотря на то, что в сисетеме перех. добавятся и лишн. сост., и лишн. переходов, то всё равно все трассы программы будут на модели, соотв., модель будет корр. Аналогично, если уберём все операторы изм. x, то моедьл ост. крр. То есть отн. несимм., все графы поргр. включ. в во все трассы модели, но не наоборот.

[править] Неформальное определение

Это понятно опис. требования, но оно неформально.

[править] Слабая симуляция

Почему слабая симуляция --- мы акл. такое огранич., только если действ. явл. наблюдаемым. Оно не сохр. кол-во шагов между сост. Соотв., не сохраняет свойств., инв. к прореживанию (в LTL --- оператор neXt) Если же снимем усл., то получим сильную симуляцию, но тогда придётся всё заменять на скип. Также, если добавляем переменные, то надо исп. atomic.

На след неделе будут разосланы вопросы.