Финальные модели спецификации . Финальные модели спецификации Игорь Бурдонов <*****@***ru>,. Александр Косачев <*****@***ru> (стр. 11 )

μ⋅λ∈SafeγΔ(Σ).

Тогда по доказанному в п.7.1 μ⋅λ∈SafeγΔ(ptr(Σ)). Пусть κ∈fs(ptr(Σ),μ⋅бPс⋅λ). Тогда 1) κ=т, или 2) κ=бΔс, или 3) κ=бz,γс, 4) κ=бzс и μ⋅бPс⋅λ⋅бz,γс∈ptr(Σ), или 5) μ⋅λ=μ⋅λ1⋅бQс, где Q∈Q. Случая 5 быть не может, так как R-модель Σ не содержит Q-отказов. Поскольку ptr(Σ)⊆Σ, Σ d-замкнуто, имеем κ∈fs(Σ,μ⋅λ). Поскольку μ⋅λ∈SafeγΔ(Σ), имеем κ∈fs(ptr(Σ),μ⋅λ). Следовательно, fs(ptr(Σ),μ⋅бPс⋅λ)⊆fs(ptr(Σ),μ⋅λ).

μ⋅λ∉SafeγΔ(Σ).

Тогда, поскольку μ⋅бPс⋅λ∈SafeγΔ(ptr(Σ)), имеем μ∈SafeγΔ(ptr(Σ)). Поэтому у трассы λ найдется такой префикс λ1⋅бuс, что μ⋅λ1∈SafeγΔ(ptr(Σ)), но μ⋅λ1⋅бuс∉SafeγΔ(ptr(Σ)).

Следовательно, u=Δ или u∈L∪R и u safeγΔ Σ after μ⋅λ1. Поскольку, μ⋅бPс⋅λ1⋅бuс≤μ⋅бPс⋅λ∈SafeγΔ(ftr(Σ)), трасса μ⋅λ1⋅бuс является L∪R-трассой, следовательно, случая u=Δ быть не может. Поэтому u∈L∪R и u safeγΔ Σ after μ⋅λ1. Тогда либо μ⋅λ1⋅бΔс∈Σ, либо для каждой кнопки R∈but(u) имеется трасса μ⋅λ1⋅бz,γс∈Σ для некоторого z∈R. А тогда по определению предфинальных трасс либо μ⋅λ1⋅бΔс∈ptr(Σ), либо для каждой кнопки R∈but(u) имеется трасса μ⋅λ1⋅бz,γс∈ptr(Σ) для некоторого z∈R. Следовательно, в обоих случаях трасса μ⋅λ∈UnSafeγΔ(ptr(Σ)).

Доказательство Теорема 6:

Сначала докажем, что D(Ψ) является R-моделью.

По определению p-модели Ψ она является незамкнутой R-моделью. Поэтому по теореме 4 D(Ψ) является R-моделью.

Теперь покажем, что ptr(D(Ψ))=Ψ. Пусть бγс∈Ψ. Тогда по определению предфинальных трасс ptr(Ψ)={т, бγс}. По определению p-модели, Ψ=ptr(Ψ)={т, бγс}. По определению d-замыкания D(Ψ)=Ψ={т, бγс}. По определению предфинальных трасс ptr(D(Ψ))={т, бγс}. Следовательно, ptr(D(Ψ))={т, бγс}=Ψ. Пусть бγс∉Ψ. Тогда по согласованности p-модели бγс∉D(Ψ). А тогда т∈SafeγΔ(Ψ) и т∈SafeγΔ(D(Ψ)). Сначала покажем, что ptr(D(Ψ))⊆Ψ. Покажем, что SafeγΔ(D(Ψ))⊆SafeγΔ(Ψ).

Пусть трасса σ∈SafeγΔ(D(Ψ)).

Допустим противное: σ∉SafeγΔ(Ψ). Поскольку т∈SafeγΔ(Ψ), у трассы σ найдется префикс μ⋅бuс такой, что μ∈SafeγΔ(Ψ), а μ⋅бuс∉SafeγΔ(Ψ). Поскольку σ∈SafeγΔ(D(Ψ)), а μ⋅бuс≤σ, имеем u≠Δ и u≠γ, то есть u∈L∪R и u safeγΔ Ψ after μ.

А тогда либо трасса μ⋅бΔс∈Ψ, либо для каждой кнопки R∈but(u) имеется трасса μ⋅бz,γс∈Ψ для некоторого z∈R. А тогда μ⋅бΔс∈D(Ψ), либо для каждой кнопки R∈but(u) имеется трасса μ⋅бz,γс∈D(Ψ) для некоторого z∈R. Следовательно, u safeγΔ D(Ψ) after μ. Но это противоречит тому, что μ⋅бuс≤σ и σ∈SafeγΔ(D(Ψ)). Мы пришли к противоречию, следовательно, σ∈SafeγΔ(Ψ), что и требовалось доказать.

Покажем, что ptr(D(Ψ))\SafeγΔ(D(Ψ))⊆Ψ\SafeγΔ(Ψ).

Пусть трасса σ∈ptr(D(Ψ))\SafeγΔ(D(Ψ)). Тогда трасса σ является финальным продолжением в D(Ψ) некоторой трассы μ∈SafeγΔ(D(Ψ)) и σ≠μ. Тогда по доказанному μ∈SafeγΔ(Ψ). Нам надо показать, что σ является финальным продолжением μ в Ψ и σ∉SafeγΔ(Ψ).

Поскольку σ≠μ, по определению финального продолжения и отсутствию в p-модели Q-отказов возможны три варианта: 1) σ=μ⋅бΔс∈D(Ψ), 2) σ=μ⋅бz,γс∈D(Ψ), 3) σ=μ⋅бzс∈D(Ψ) и μ⋅бz,γс∈D(Ψ).

По определению d-замыкания найдется такая трасса μ`∈Ψ, что μ∈d(μ`) и 1) μ`⋅бΔс∈Ψ, 2) μ`⋅бz,γс∈Ψ, 3) μ`⋅бzс∈Ψ и μ`⋅бz,γс∈Ψ. Отсюда по свойству предфинальности Ψ трасса μ`∈SafeγΔ(Ψ).

А тогда по финально-замкнутости Ψ либо 1) μ∈UnSafeγΔ(Ψ), либо 2) μ∈SafeγΔ(Ψ) и fs(Ψ,μ`)⊆fs(Ψ,μ).

Случай 1 противоречит μ∈SafeγΔ(Ψ). Следовательно, 1) σ=μ⋅бΔс∈Ψ, 2) σ=μ⋅бz,γс∈Ψ, 3) σ=μ⋅бzс∈Ψ и μ⋅бz,γс∈Ψ.

Следовательно, σ является финальным продолжением μ в Ψ.

Во всех этих случаях также σ∉SafeγΔ(Ψ).

Теперь покажем, что ptr(D(Ψ))⊇Ψ. Покажем, что SafeγΔ(D(Ψ))⊇SafeγΔ(Ψ).

Пусть трасса σ∈SafeγΔ(Ψ). Тогда σ∈Ψ и, следовательно, σ∈D(Ψ). Допустим, утверждение не верно: σ∈D(Ψ)\SafeγΔ(D(Ψ)).

Поскольку т∈SafeγΔ(Ψ), у трассы σ найдется префикс μ⋅бuс такой, что μ∈SafeγΔ(D(Ψ)), а μ⋅бuс∉SafeγΔ(D(Ψ)).

Поскольку σ∈SafeγΔ(Ψ), а μ⋅бuс≤σ, имеем u≠Δ и u≠γ, то есть u∈L∪R и тогда u safeγΔ D(Ψ) after μ.

Следовательно, либо 1) μ⋅бΔс∈D(Ψ), либо 2) для каждой кнопки R∈but(u) имеется трасса μ⋅бzR,γс∈D(Ψ) для некоторого zR∈R.

Тогда по определению d-замыкания либо 1) найдется такая трасса μ`∈Ψ, что μ∈d(μ`) и μ`⋅бΔс∈Ψ, либо 2) для каждой кнопки R∈but(u) найдется такая трасса μR`∈Ψ, что μ∈d(μR`) и μR`⋅бzR,γс∈Ψ.

По свойству предфинальности Ψ 1) трасса μ`∈SafeγΔ(Ψ) или 2) все трассы μR`∈SafeγΔ(Ψ).

Поскольку μ∈SafeγΔ(D(Ψ)), по п.2.2.1.1 μ∈SafeγΔ(Ψ).

А тогда по финально-замкнутости Ψ имеем 1) бΔс∈fs(Ψ,μ`)⊆fs(Ψ,μ) либо 2) бzR,γс∈fs(Ψ,μR`)⊆fs(Ψ,μ) для каждой кнопки R.

Следовательно, 1) трасса μ⋅бΔс∈Ψ либо 2) для каждой кнопки R∈but(u) трасса μ⋅бzR,γс∈Ψ.

Тем самым, u safeγΔ Ψ after μ, что, поскольку μ⋅бuс≤σ, противоречит σ∈SafeγΔ(Ψ).

Итак, мы пришли к противоречию, следовательно, наше допущение не верно и σ∈SafeγΔ(D(Ψ)), что и требовалось доказать.

Покажем, что ptr(D(Ψ))\SafeγΔ(D(Ψ))⊇Ψ\SafeγΔ(Ψ).

Пусть трасса σ∈Ψ\SafeγΔ(Ψ). Тогда трасса σ является финальным продолжением в Ψ некоторой трассы μ∈SafeγΔ(Ψ) и σ≠μ. Тогда по п.2.2.2.1 μ∈SafeγΔ(D(Ψ)). Нам надо показать, что σ является финальным продолжением μ в D(Ψ) и σ∉SafeγΔ(D(Ψ)).

Поскольку σ≠μ, по определению финального продолжения и отсутствию в p-модели Q-отказов возможны три варианта: 1) σ=μ⋅бΔс∈Ψ, 2) σ=μ⋅бz,γс∈Ψ, 3) σ=μ⋅бzс∈Ψ и μ⋅бz,γс∈Ψ.

Тогда по определению d-замыкания 1) σ=μ⋅бΔс∈D(Ψ), 2) σ=μ⋅бz,γс∈D(Ψ), 3) σ=μ⋅бzс∈D(Ψ) и μ⋅бz,γс∈D(Ψ).

Тогда, поскольку μ∈SafeγΔ(D(Ψ)), трасса σ является финальным продолжением μ в D(Ψ), во всех этих случаях также σ∉SafeγΔ(D(Ψ)), что и требовалось доказать.

Доказательство Теорема 7:

Пусть Ω⊆(L∪R∪Q∪{Δ,γ})* и Ψ=ΩR p-модель.

Обозначим A={σ∈Ω∩(L∪R)*|σ⋅бγс∉Ω}.

Поскольку Ψ=ΩR, имеем A={σ∈Ψ∩(L∪R)*|σ⋅бγс∉Ψ}.

Условия 4b и 4c совпадают, если SafeIn(Ω)=SafeγΔ(Ω). Поскольку Ψ=ΩR, имеем SafeγΔ(Ω)= SafeγΔ(Ψ). Поскольку Ψ p-модель, она предфинальна, поэтому по теореме 3 SafeγΔ(Ψ)=A. Следовательно, для эквивалентности условий 4b и 4c достаточно SafeIn(Ω)=A. Очевидно, SafeIn(Ω)⊆A, поэтому достаточно условия SafeIn(Ω)⊇A.

Пусть выполнены условия: ∀z∈L ∀Q∈Q ∀σ∈SafeγΔ(Ω) σ⋅бzс∈Ω & σ⋅бz,γс∉Ω

⇒ ∃P∈but(z) P safeγΔ Ω after σ & (P∈Q ⇒ σ⋅бPс∉Ω),

Q safeγΔ Ω after σ & σ⋅бQс∉Ω ⇒ ∃v∈Q σ⋅бvс∈Ω. ∀P∈Q ∀μ⋅бPс⋅λ∈Ω μ∈SafeγΔ(Ω) & P safeγΔ Ω after μ & λ=т.

Докажем, что SafeIn(Ω)⊇A и выполнены условия 2c и 3с.