ГОСТ Р ИСО 18629-42—2011
(forall (?а) (iff(partial_time_filter ?а)
(and (exists (?s1)
(forall (?s2)
(implies (and (subactivity ?a1 ?a)
(poss ?a ?s1)
(poss ?a ?s2)
(begin_equiv ?s1 ?s2))
(poss_equiv?a1 ?s1 ?s2))))
(exists (?a2 ?s3 ?s4)
(and (subactivity ?a2 ?a)
(poss ?a ?s3)
(poss ?a ?s4)
(begin_equiv ?s3 ?s4)
(not (poss_equiv ?a2 ?s3 ?s4)))))))
30.5.6 rigid_time_filter
Некоторое неделимое комплексноедействие ?а является жестким фильтром по времени при условии;
если и только если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала
отсчета, то существуют составляющиедействия для ?а, которые не могут происходить (случаться).
(forall (?а) (iff(ngid_time_filter ?а)
(forall (?s1)
(exists (?a1 ?s2)
(and (begin_equiv ?s1 ?s2)
(poss ?a ?s1)
(poss ?a ?s2)
(not(poss_equiv?a1 ?s1 ?s2)))))))
30.5.7 state_nonfiltor
Некоторое неделимое комплексноедействие ?а не является фильтром состояния при условии; если и
только если какие-либо и когда-либодопустимые события для ?а согласованы по состоянию, то все собы
тия для составляющих действий ?а согласованы по допустимости.
(forall (?а) (iff(state_nonfilter ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (subactivity ?a1 ?a)
(not (poss ?a ?s1))
(not (poss ?a ?s2))
(state_equiv ?s1 ?s2))
(poss_equiv?a1 ?s1 ?s2)))))
30.5.8 partial_state_nonfilter
Некоторое неделимое комплексноедействие ?а не является частичным фильтром по состоянию тогда
и только тогда, когда существуют допустимые события для ?а, согласованные по состоянию, вкоторых все
составляющиедействиядля ?а согласованы подопустимости.
(forall (?а) (iff(partial_state_nonfilter ?а)
(and (exists (?s1)
(forall (?s2)
(implies (and (subactivity ?a1 ?a)
(not (poss ?a ?s1))
(not (poss ?a ?s2))
(state_equiv?s1 ?s2))
(poss_equiv ?a1 ?s1 ?s2))))
(exists (?a2 ?s3 ?s4)
(and (subactivity ?a2 ?a)
(not (poss ?a ?s3))
(not (poss ?a ?s4))
(state_equiv ?s3 ?s4)
(not (poss_equiv ?a2 ?s3 ?s4)))))))
43