ГОСТ Р ИСО 18629-42—2011
34.5 Определения вариации препятствующих входных условий
Для вариации препятствующих входных условий определены нижеследующие понятия.
34.5.1 statejntorfore
Некотороедействие ?а препятствует состоянию тогда и только тогда, когда какие-либо события, согла
сованные по состоянию, имеют те же сохраненные фильтры.
(forall (?а) (iff(state„interfere ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (atomic ?a1)
(state_equiv ?s1 ?s2))
(iff(preserved_filter?a1 ?a?s1)
(preservedJtter?a1 ?a ?s2)))))
34.5.2 partialjnterfere
Некотороедействие ?a препятствует частично тогда и только тогда, когда существуютсобытия, согла
сованные по состоянию и имеющие те же сохраненные фильтры.
(forall (?а) (iff(partialjnterfere ?а)
(and (exists (?s1 ?a1)
(forall (?s2)
(implies (and (atomic ?a1)
(state_equiv?s1 ?s2))
(iff (preservedJlter?a1 ?a?s1)
(preservedJitter ?a1 ?a?s2)))))
(exists (?a2 ?s3 ?s4)
(and (atomic ?a2)
(state_equiv ?s3 ?s4)
(preserved_filter ?a2 ?a ?s3)
(not (preserved_filter ?a2 ?a ?s4)))))))
34.5.3 unconditionaljnterfore
Некотороедействие препятствует безусловно тогда и только тогда, когда для каких-либо согласован
ных по состоянию событий существуют различные сохраненные фильтры.
(forall (?а) (iff(unconditional Jnterfere ?а)
(forall (?s1)
(exists (?a1 ?s2)
(and (atomic ?a1)
(state_equiv?s1 ?s2)
(iff(preserved_filter ?a1 ?a ?s1)
(not (preservedJitter ?a1 ?a ?s2))))))))
34.5.4 tim ejnterfere
Некоторое действие ?a препятствует no времени тогда и только тогда, когда какие-либо согласован
ные по времени начала отсчета события имеют те же сохраненные фильтры.
(forall (?а) (iff(timejnterfere ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (atomic ?a1)
(begin_equiv ?s1 ?s2))
(iff(preservedJitter ?a1 ?a ?s1)
(preservedJitter ?a1 ?a?s2))))))
34.5.5 sometime_interfere
Некотороедействие ?a препятствует иногда тогда и только тогда, когда существуют согласованные по
времени начала отсчета события, имеющие те же сохраненные фильтры.
(forall (?а) (iff (sometimejnterfere ?а)
(and (exists (?s1 ?a1)
(forall (?s2)
(implies (and (atomic ?a1)
(begin_equiv ?s1 ?s2))
(iff (preservedJitter ?a1 ?a ?s1)
(preservedjlter?a1 ?a ?s2)))))
52