ГОСТ Р ИСО 18629-42—2011
30.5.1 state_filter
Некоторое неделимое комплексноедействие ?а является фильтром состояния при условии: если и
только если какие-либо и когда-либо допустимые события для действия ?а согласованы по состоянию, то
все составляющие действия ?а могутдействительно иметь место.
(forall (?а) (iff (state_filter ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (subactivity ?a1 ?a)
(poss ?a ?s1)
(poss ?a ?s2)
(state_equiv?s1 ?s2))
(poss_equiv ?a1 ?s1 ?s2)))))
30.5.2 partial_state_filtor
Некоторое неделимое комплексное действие ?а является частичным фильтром состояния тогда и
только тогда, когда существуют допустимые события для действия ?а, согласованные по состоянию, в
которых все составляющиедействиядля ?а могут действительно иметь место.
(forall (?а) (iff(partial_state_fitter ?а)
(and (exists (?s1)
(forall (?s2)
(implies (and (subactivity ?a1 ?a)
(poss ?a ?s1)
(poss ?a ?s2)
(state_equiv?s1 ?s2))
(poss_equiv ?a1 ?s1 ?s2))))
(exists (?a2 ?s3 ?s4)
(and (subactivity ?a2 ?a)
(poss ?a ?s3)
(poss ?a ?s4)
(state_equiv ?s3 ?s4)
(not (poss_equiv ?a2 ?s3 ?s4)))))))
30.5.3 rigid_state_filtor
Некоторое неделимое комплексноедействие ?а является жестким фильтром состояния при условии,
если и только если какие-либо и когда-либодопустимые события для действия ?а согласованы по состоя
нию. то существуют составляющие действия для ?а. которые не могут происходить (случаться).
(forall (?а) (iff(rigid_state_filter?a)
(forall (?s1)
(exists (?a1 ?s2)
(and (state_equiv ?s1 ?s2)
(poss ?a ?s1)
(poss ?a ?s2)
(not(poss_equiv?a1 ?s1 ?s2)))))))
30.5.4 time_filter
Некоторое неделимое комплексное действие ?а является фильтром по времени при условии: если и
только если какие-либо и когда-либодопустимые события для ?а согласуются по времени начала отсчета,
то все составляющие действия для ?а могутдействительно происходить (случаться).
(forall (?а) (iff (time_filter ?а)
(forall (?а1 ?s1 ?s2)
(implies (and (subactivity ?a1 ?a)
(poss ?a ?s1)
(poss ?a ?s2)
(begin_equiv ?s1 ?s2))
(poss_equiv ?a1 ?s1 ?s2)))))
30.5.5 partial_timo_filter
Некоторое неделимое комплексное действие ?а является частичным фильтром по времени тогда и
только тогда, когда существуютдопустимые события для ?а. согласованные по времени начала отсчета, в
которых все составляющиедействия для ?а могутдействительно происходить (случаться).
42