ГОСТ Р ИСО 18629-42—2011
(forall (?а) (iff (state_dobber ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (atomic ?a1)
(state_equiv?s1 ?s2))
(iff(preserved_effects ?a1 ?a ?s1)
(preserved_effects ?a1 ?a ?s2))))))
35.5.2 partial_state_clobbor
Некоторое действие ?a частично затирает данные о состоянии тогда и только тогда, когда существуют
согласованные по состоянию события, сохраняющие те же эффекты.
(forall (?а) (iff (partial_ck>bber?а)
(and (exists (?s1 ?a1)
(forall (?s2)
(implies (and (atomic ?a1)
(state_equiv ?s1 ?s2))
(iff(preserved_effects ?a1 ?a ?s1)
(preserved_effects ?a1 ?a ?s2)))))
(exists (?a2 ?s3 ?s4)
(and (atomic ?a2)
(state_equiv ?s3 ?s4)
(preserved_effects ?a2 ?a ?s3)
(not (preserved_effects ?a2 ?a ?s4)))))))
35.5.3 unconditional_clobbor
Некоторое действие ?a затираетданные безусловно тогда и только тогда, когда существуют согласо
ванные по состоянию события, не сохраняющие те же эффекты.
(forall (?а) (iff(unconditional_clobber ?а)
(forall (?s1)
(exists (?a1 ?s2)
(and (atomic ?a1)
(state_equiv ?s1 ?s2)
(iff(preserved_effects?a1 ?a?s1)
(not(preserved_effects?a1 ?a ?s2))))))))
35.5.4 time_clobbor
Некотороедействие ?a затирает данные о времени тогда и только тогда, когда какие-либо согласован
ные по времени начала отсчета события сохраняют теже эффекты.
(forall (?а) (iff (time_clobber ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (atomic ?a1)
(begin_equiv ?s1 ?s2))
(iff(preserved_effects ?a1 ?a ?s1)
(preserved_effects ?a1 ?a ?s2))))))
35.5.5 sometime_cIobbcr
Некоторое действие ?a иногда затирает данные о времени тогда и только тогда, когда существуют
согласованные по времени начала отсчета события, сохраняющие теже эффекты.
(forall (?а) (iff (sometime_clobber ?а)
(and (exists (?s1 ?a1)
(forall (?s2)
(implies (and (atomic ?a1)
(begin_equiv ?s1 ?s2))
(iff (preserved_effects ?a1 ?a ?s1)
(preserved_effects ?a1 ?a ?s2)))))
(exists (?a2 ?s3 ?s4)
(and (atomic ?a2)
(begin_equiv ?s3 ?s4)
(preserved_effects ?a2 ?a ?s3)
(not (preserved_effects ?a2 ?a ?s4)))))))
54