1、ICS 25.040.40 L 67 远望国家标准和国11: /、中华人民第41GB/T 20719. 41-201 O/ISO 18629-41 : 2006 工业自动化系统与集成过程规范语言部分:定义性扩展:活动扩展Industrial automation system and integration Process specification language一Part 41 : Definitional extension: Activity extensions CISO 18629-41: 2006 , IDT) 2011-01-14发布2011-06-01实施数码防伪中华人民共
2、和国国家质量监督检验检菇总局中国国家标准化管理委员会发布GB/T 20719.4 1-2010/ISO 18629-41 :2006 目次前言.1 引言.m I 范围.2 规范性引用文件3 术语、定义和缩略语4 GB/T 20719的第41部分第49部分的常规组织 4 5 GB/T 20719本部分的组织 5 6 非确定性活动:置换分支结构.6 7 非确定性活动:折叠分支结构.88 非确定性活动:分支结构和排序109 非确定性活动:重复的分支结构MM 活动谱:置换活动树11 活动谱:压实分支结构1812 活动谱:活动树和重新排序.20 13 谱和子树遏制nu 活动的嵌入约束.24 日梗概活动树
3、.26 16 原子活动:向上并发.29 17 原子活动:向下并发30M 原子活动谱19 活动的前提.34 附录A(规范性附录)GBjT 20719.41的ASN.1标识符附录B(资料性附录)使用GBjT20719.41描述过程的实例附录NA(资料性附录)本部分英文黑体词的含义45参考文献.48 索引.49GB/T 20719.4 1-201 O/ISO 18629-41 : 2006 目lJ1=1 GB/T 20719(工业自动化系统与集成过程规范语言目前拟分为以下部分:一一第1部分z概述与基本原理;一一第11部分:PSL核心;一一第12部分:外核;一一第13部分:时序理论;一一第14部分:资
4、源理论;一一第15部分:活动性能理论:一一第21部分:EXPRESS; 一一第22部分:XML;一一第23部分:UML;第41部分:定义性扩展z活动扩展;一一第42部分:时间和状态;一一第43部分:定义性扩展:活动次序和持续时间扩展;一一第44部分:定义性扩展z资源扩展;一一第45部分:资源集的种类;第46部分:加工活动;一一第47部分z过程目的。本部分为GB/T20719的第41部分。本部分等同采用ISO18629-41: 2006(工业自动化系统与集成过程规范语言第41部分z定义性扩展活动扩展)(英文版)。本部分的技术内容和组成结构与ISO18629-41: 2006相一致，在编写格式上符
5、合GB/T1. 1-2000 标准化工作导则第1部分:标准的结构和编写规则上只根据我国国家标准的制定要求和为方便使用，做了如下编辑性的改动:一一将ISO18629改为GB/T20719 ，把ISO18629-41改成GB/T20719.41或GB/T20719 本部分; ISO 18629-1改成GB/T20719. l;ISO 18629-11改成GB/T20719.11; ISO 18629-12改成GB/T20719.12。一将6.6的注:GB/T20719.1-2004，3.3.8，4.2.4和5.1中阐明了GB/T20719中的语法句子的功能和重要性。改成注:GB/T20719. 1
6、-2004, 4. 3. 4中阐明了GB/T20719中的语法句子的功能和重要性。一一删除了ISO18629-41 :2006的前言，并按照我国国家标准编制要求重新起草了前言。二一将ISO18629-41: 2006第2章规范性引用文件中的引导语改为GB/T1. 1-2000中规定的引导语。将本部分中出现的已转化为国家标准的国际标准编号改为国家标准编号，便于使用和查阅。未转化的国际标准保留。一一为了使读者便于理解本部分黑体词的含义，增加了附录队。一-删去了原文中不符合我国标准编写的字句。I GB/T 20719.4 1-2010/ISO 18629-41 :2006 E 本部分的附录A为规范性
7、附录，附录B、附录NA为资料性附录。本部分由中国机械工业联合会提出。本部分由全国自动化系统与集成标准化技术委员会CSAC/TC159)归口。本部分主要起草单位:北京机械工业自动化研究所，清华大学。主要起草人z王思斯、黄双喜。GB/T 20719.4 1-20 10/ISO 18629-41 :2006 引GB/T 20719是为了进行与制造过程相关的计算机可解释的信息交换所使用的国家标准。GB/T 20719包含的所有部分结合在一起，为描述贯穿整个生产过程的制造过程提供了一类语言(该生产过程可能位于一个工业公司，也可能跨越几个工业部门或公司)，并独立于任何特定的表示模型。语言的本质使得它适用于
8、在生产过程的各个阶段共享与制造相关的过程规范和性质。本部分提供了与在GB/T20719中定义的活动扩展相关的语言的定义性扩展的描述。GB/T 20719中的所有部分与给定的应用软件中使用的任何特定过程的表述模型无关。它们一同为改善这些应用软件的协同性提供了一个结构框架。皿GB/T 20719.41-2010/ISO 18629-41 :2006 1 范围工业自动化系统与集成过程规范语言第41部分:定义性扩展:活动扩展本部分通过使用GB/T20719语言中编写的一组定义来提供这种语言的非基本概念的规范。这些定义为本部分中的术语提供了语义的公理化。以下包括在本部分的范围中:使用GB/T20719.
9、 11一2010和GB/T20719. 12-2010的概念详细描述的、与状态和时间关系无关的、但与例如第5章中列出的那些活动类别相关的概念的定义。以下不包括在本部分的范围中:一一使用GB/T20719. 11-2010和GB/T20719. 12-2010的概念详细描述的、与状态和时间相关的概念的定义。2 规范性引用文件下列文件中的条款通过GB/T20719的本部分的引用而成为本部分的条款。凡是注日期的引用文件，其随后所有的修改单(不包括勘误的内容)或修订版均不适用于本部分，然而，鼓励根据本部分达成协议的各方研究是否可使用这些文件的最新版本。凡是不注日期的引用文件，其最新版本适用于本部分。G
10、B/T 16262. 1信息技术抽象语法记法一(ASN.l)第1部分:基本记法规范(GB/T16262.1-2006 ,ISO/IEC 8824-1: 2002 , IDT) GB/T 16656.1 工业自动化系统与集成产品数据表示与交换第1部分z概述与基本原理(GB/T 16656.1-2008,ISO 10303-1:1994,MOD) GB/T 19114.1 工业自动化系统与集成工业制造管理数据第1部分:综述(GB/T19114.1-2003 ,ISO 15531-1: 2002 , IDT) GB/T 20719.1-2006 工业自动化系统与集成过程规范语言第l部分:概述与基本原
11、理(lSO 18629.1: 2004 , IDT) GB/T 20719. 11-2010 工业自动化系统与集成过程规范语言第11部分:PSL核心(lSO 18629-11:2005 ,IDT) GB/T 20719. 12-2010工业自动化系统与集成过程规范语言第12部分z外核(lSO18629-12: 2005 , IDT) 3 术语、定义和缩略语3. 1 术语和定义下列术语和定义适用于GB/T20719的本部分。3. 1. 1 公理axiom 形式语言中的合式公式，用以对一门语言的词汇中的符号解释加以约束。1 GB/T 20719.4 1-2010/ISO 18629-41 :200
12、6 GB/T 20719. 1-2006J 3. 1. 2 数据data 一种形式化的信息表达，它适合于人或计算机进行通信、解释或处理。GB/T 16656. 1-2008J 3. 1.3 定义的词汇defined lexicon 非逻辑词汇的一系列符号，表示所定义概念。注:定义词汇划分为常数符号、函数符号和关系符号。例:具有保守定义的术语。GB/T 20719. 1-2006J 3.1.4 定义性扩展definitional extension 指PSL核心的扩展，它引入了完全由PSL核心定义的新的语言术语。注:定义性扩展没有为PSL核心增加新的表达能力，但它常常定义领域应用中的语义及术语。
13、GB/T 20719. 1-2006，定义3.1. 6J 3. 1. 5 离散制造discrete manufacturing 离散项目的生产。例:汽车，装置或计算机。GB/T 19114.1-2003J 3. 1.6 扩展extension 包含附加公理的PSL核心的扩充。注1:PSL核心是一组相对简单的公理，足以表达较广范围内的基本过程。然而，更复杂的过程所需的表达性资源超出了PSL核心的范围。相对于将每一个可能的概念(其对于描述一个或另一个过程可能有用)杂乱地添加到PSL核心中去唱更好的方式是开发各种独立的、模块化的扩展，并把它们添加进P$L核心。采用这种方式，用户可以根据自己的表达省求
14、精确地裁剪语言，注2:所有的扩展均为核心理论或定义性扩展。GB/T 20719. 1-2006J 3. 1. 7 语法grammar 说明如何将逻辑符号和词汇术语组合为合式公式的规范。GB/T 20719. 1-2006J 3. 1.8 信息information 事实、概念或指令。GB/T 16656. 1-2008J 3. 1.9 语言language 词汇和语法的结合。GB/T 20719.1-2006J 3. 1. 10 制造manufacturing 将原材料或半成品转换成成品的功能或行为。2 注:定义采自APICS字典，第八版。GB/T 19114. 1-2003J 3. 1. 1
15、1 制造过程manufacturing process GB/T 20719.4 1-2010/ISO 18629-41 :2006 一套结构化的行为或操作，它完成了将原材料或半成品向成品的转化。注:制造过程可被安排在程序规划、产品规划、单元规划或装配位置规划里。根据战略性应用和物质的分配，制造过程可被用于支持按库存生产，按订单生产，按订单装配。GB/T 19114. 1-2003J 3. 1. 12 模型model 满足一种理论中所有合式公式的一组元素和事实任务的组合。注1:模型这个词在逻辑中的用法不同于它在大多数科学及日常读物中的用法:如果一个命题在某种解释中为真，那么就可以说这种解释是该
16、命题的模型。这里所说的语义常被称作模型理论语义。注2:模型一般表示为包含附加结构的集合(半定序，点阵，或向量空间)。模型定义了术语的含义以及本模型中所采用语言的命题的事实概念。给定一个模型，在公理集中使用的数学结构基本公理集就通过语言及它们的逻辑关系成为概念论证的基础，因此模型的集合构成了本体的形式语义。GB/T 20719. 1-2006J 3. 1. 13 本体ontology 按照词汇中术语的含义的某些规范而定的专门术语的词汇。注1:与形式语言中术语含义的规范一同给出的相关术语的结构化集合。术语含义的规范说明了术语为什么相关、如何相关，以及集合划分和构造的条件。注2:PSL(比如GB/T
17、20719)的主要部分就是一个本体。基本概念就是本体论。通过GB/T20719，可以描述基本的制造过程及业务过程。注3:本体的核心不只是术语，也包括它们的含义。术语的任意集合包含在本体中，但只有在含义一致时这些术语才能被共享。共享的是术语的指定语义，而不是简单的术语共享。注4:没有显式定义的任何术语都可能成为含糊及混乱的来源。本体论的难点是:需要建立一个框架以使框架中术语的含义更为清晰明确。对于GB/T20719这个本体，有必要提供一个过程信息的严格的数学特性描述以及GB/T 20719语言中信息的基本逻辑特性的精确表达。注5:实际上，扩展合并了外核的公理。GB/T 20719. 1-2006
18、J 3. 1. 14 基本概念primitive concept 没有保守定义的词汇术语。GB/T 20719.1-2006J 3.1. 15 基本词汇primitive lexicon 表示基本概念的非逻辑词汇的符号集合。注:基本词汇分为常量、函数符号和关系符号。GB/T 20719. 1-2006J 3. 1. 16 过程process 涉及各种企业实体的一套结构化的活动，是为特定的目的设计和组织的。注z这里提供的定义和GB/T16656.49的定义非常接近。然而GB/T19114需要一套结构化活动的概念，对于时间和步骤没有任何预先确定。另外，从流程管理的观点来看，为同一目的需要一些空过程
19、，尽管实际上它们不GB/T 20719.4 1-2010/ISO 18629-41 :2006 起任何作用。GB/T 19114. 1-2003J 3. 1. 17 产晶product 由天然或人造而成的事物。GB/T 16656. 1-2008J 3. 1. 18 资源resource 在企业生产产品或服务中装置的任何设备、工具和手段。注1:这里所定义的资源包括人力资源，作为一种具有给定才能和能力的特定的手段。这些工具通过指派任务而被认为涉及制造过程。除了它们在制造过程中完成给定的任务(即原材料或组件的变换，后勤服务保证的能力外，不包括人力资源的个体或通用人类行为建模。作为包括人力手段的其他
20、资源，仅从他们的功能、能力、状态(即空闲的、忙)，它不包括任何方面的个体或共同的社会行为建模或表述。注2:此定义包括GB/T16656. 49的定义。而适用于GB/T20719. 14和GB/T20719.44的原材料和消耗品的定义包括GB/T16656.49定义。GB/T 19114. 1-2003J 3. 1. 19 理论theory 关于某个指定概念或概念集的公理和定义的集合。注:该定义反映了人工智能方法，在该方法中，理论是一组假设，以这些假设为基础得到相关概念的含义。GB/T 20719. 1-2006J 3.2 缩略语本部分使用了以下缩略语。KIF Knowledge Interch
21、ange Format 知识交换格式4 GB/T 20719的第41部分第49部分的常规组织1)GB/T 20719的第41部分第49部分详细描述了给出GB/T20719的非基本概念的精确定义和一组公理所需的定义性扩展。定义性扩展是引入了有关词汇的新项目的GB/T20719. 11-2010和GB/T 20719. 12-2010的扩展。在定义性扩展中存在的这些项目可以用GB/T20719. 11二2010和GB/T 20719. 12-2010的理论完全定义。此定义性扩展为个体应用软件或以协同性为目的的应用软件类型的规范中所使用的元素提供精确的语义定义。定义性扩展存在于以下范畴中:一一活动扩
22、展;时间和状态扩展;活动次序和周期扩展;一一一资源角色;一一资源集合;一一处理器活动扩展。GB/T 20719的单个用户或用户团体可能需要扩展GB/T20719来详细描述目前在GB/T20719 的第41部分第49部分中缺少的概念。它们应该采用GB/T20719中存在的元素来这样做。自定义扩展及其定义组成定义性扩展，但不应成为GB/T20719的第41部分第49部分中的一部分。注z自定义扩展应像在GB/T20719.1-2006的5.1和5.2中所定义的那样符合GB/T20719. 以下包括在GB/T20719的第41部分第49部分的范围内:1) 某些部分正在开发中。4 GB/T 20719.
23、4 1-2010/ISO 18629-41 :2006 一一使用GB/T20719. 11一2010和GB/T20719. 12一2010中的概念，特别针对上面概述的6个概念的元素的语义定义;一一约束定义性扩展中元素的使用的一组公理。以下不包括在GB/T20719的第41部分第49部分的范围内:一一作为GB/T20719. 11-2010和GB/T20719. 12-2010中一部分的概念的定义和公理;-一没有使用GB/T20719.11-2010和GB/T20719.12-2010中的元素来定义的元素;一一自定义扩展。5 GB/T 20719本部分的组织组成本部分的基本理论是:-一一非确定性
24、活动:置换分支结构;一一非确定性活动:折叠分支结构;非确定性活动:分支结构和排序;一一非确定性活动:重复的分支结构;一一活动谱:置换活动树;一一活动谱:压实分支结构;一一活动谱:活动树和重新排序;一一谱和子树遏制;活动的嵌入约束;一一梗概活动树;原子活动:向上并发;一一原子活动:向下并发;一一原子活动谱;一一活动的前提。图1显示这些扩展与GB/T20719. 12-2010的核心理论之间的关系，以用于详细说明GB/T 20719本部分中的定义性扩展。箭头显示本部分中的扩展和GB/T20719. 12-2010之间的相关性。本部分中的全部理论均为GB/T207192. 12-2010的扩展，GB
25、/T 20719. 12-2010本身是GB/T 20719. 11-2010的扩展。注:GB/T 20719. 12-2010中的扩展之间相关性的完整图表存在于GB/T20719.12-2010的5.1中。置换活动树重复的分支结构原子活动:向下活动活动的前提GBrr 20719. 12 原子活动谱图1GB/T 20719的定义性扩展活动树和重新排序谱和子树逼制5 GB/T 20719.4 1-2010/ISO 18629-41 :2006 6 非确定性活动:置换分支结构本条款表征了关于非确定性活动z置换分支结构的全部定义。6. 1 置换分支结构的基本词汇置换分支结构的词典不需要基本关系。6.
26、2 置换分支结构的概念的定义词汇本条款中定义了以下关系:(branch_monomorphic ?a ? occl ? occ2); (branch_automorphic ?a ? occl ? occ2); (permuted ?a) ; (nondet_permuted ?a); (partial_permuted ?的;(s扛nple?a)。每一个概念由非正式语义和一个KIF公理来描述。6.3 置换分支结构所需的核心理论此扩展需要:一一-act_occ.th; 一-complex.th; 一一-atomic.th; subactivity. th; 一一一occtree.th; -一-
27、psLcore.th。6.4 置换分支结构所需的定义性扩展置换分支结构不需要定义性扩展。6.5 置换分支结构的概念的定义对于置换分支结构定义以下概念。6. 5. 1 Branch_monomorphic 当且仅当最小活动树的一个分支中的原子活动发生的集合能被嵌入到另一分支上的原子活动发生的集合中时，此一个分支对于另一分支是branch_monomorpl山。(forall(?occl ?occ2) (iff(branch_monomorphic ?occl ?occ2) (forall(?sl ?a) (implies (and(occurrence_of ?occl ?a) (subacti
28、vity_occurrence ?sl ?occl) (exists(?s2) (and (subactivity_occurrence ?s2 ?occ2) (mono ?sl ?s2 ?a) 6. 5. 2 Branch_automorphic 当且仅当最小活动树的一个分支上的原子活动发生的集合是该最小活动树的另一分支上的原子活动发生的集合的置换时，这两个分支是branch_automorphic。(forall(?occl ?occ2) (iff(branch_automorphic ?occl ?occ2) (and(branch_monomorphic ?occl ?occ2) (b
29、ranch_monomorphic ?occ2 ?occl) 6 GB/T 20719.4 1-2010/ISO 18629-41 :2006 6. 5. 3 Permuted 当且仅当最小活动树的每一个分支上的原子子活动发生的集合都是每一个其他分支上的原子子活动发生的置换时，一个活动发生是permutedo(forall(?occ) (iff(permuted ?occ) (forall(?occl ?occ2) (implies (and(same_grove ?occl ?occ) (same_grove ?occ2 ?occ) (branch_automorphic ?occl ?oc
30、c2) 6.5.4 Nondet_permuted 当且仅当最小活动树的每一个分支上的原子子活动发生的集合是其他一些分支上的原子子活动发生的置换时，一个活动发生是nondet_permuted。(forall(?occ) (iff(nondet_permuted ?occ) (forall(?occl) (implies(same_grove ?occl ?occ) (exists(?occ2) (and (same_grove ?occl ?occ2) 6. 5. 5 Partial_permuted (not( = ?occl ?occ2) (branch_automorphic ?occ
31、l ?occ2) 当且仅当存在一个分支使得原子子活动发生的集合是在其他一些分支上的原子子活动发生的置换，且存在不是任何其他分支的置换的一个分支时，一个活动发生是partial_permu ted 0 (forall(?occ) (iff(partial_permuted ?occ) (exist(?occl ?occ2 ?occ3) (and (s四e_grove?occl ?occ) (same_grove ?occ2 ?occ) 6. 5. 6 Simple (not( = ?occl ?occ2) (branch_automorphic ?occl ?occ2) (same_grove
32、?occ3 ?occ) (forall(?occ4) (implies (and(same_grove ?occ3 ?occ4 ?的(branch_automorphic ?occ3 ?occ4) (= ?occ3 ?occ4) 当且仅当一个活动树的所有分支都不是分支自同构时，一个活动发生是simpleo(forall(?occ) (iff(simple ?occ) (forall(?occl ?occ2) (implies (and(same_grove ?occl ?occ) (same_grove ?occ2 ?occ) (branch_automorphic ?occl ?occ2)
33、(= ?occl ?occ2) 6.6 置换分支结构关系的语法下列语法句子描述了用于置换分支结构的KIF中详细说明的过程描述和辅助规则。注:在GB/T20719.1-2006的4.3.4中阎明了GB/T20719中的语法句子的功能和重要性。7 GB/T 20719.4 1-2010/ISO 18629-41 :2006 (permuted_spec): : = (forall( (variable) (implies(same_tree(variable)?occ) (occurrence_sentence) (nondet_permuted_spec): = (forall(variable
34、)祷)(implies(same_tree(variable)?occ) (or(occurrence_sentence)祷)(partial_permuted _spec): : = (or(nondet_permuted_spec) (simple_spec) (simple_spec ): = (exists( (variable)祷)(and(occurrce_formula (br缸lch_spec) ) (occurrence_literal): = (occurrence(variable) (term) (subactivity_occurrence(variable) (va
35、riable) (occurrence_formula): = (occurrence_literal)I (and(occurrence_literal)兴)(occurrence_sentence): = (existsC(variable)长)(occurrence_formula) (branch spec : = (and(same_tree(variable)?occ) + (not( = (variable)?occ) +) 7 非确定性活动t折叠分支结构本条款表征了有关非确定性活动:折叠分支结构的全部定义。7. 1 折叠分支结构的基本词汇折叠分支结构的词典不需要基本关系。7.2
36、 折叠分支结构概念的定义词汇本条款中定义了以下关系:一一(branch_homomorphic?occl ?occ2); 一一一(folded?a); 一(nondet_folded?a); 一一一(partial_folded? a) ; 一一一(rigid?a)。每一个概念由非正式语义和一个KIF公理来描述。7.3 折叠分支结构所需的理论本理论需要:一一-act_occ.th; 一一-complex.th; 一一-atomic.th; subactivity. th; 一一occtree.th; 一一-psl_core.th。7.4 折叠分支结构所需的定义性扩展折叠分支结构不需要定义性扩展
37、。8 GB/T 20719.4 1-2010/ISO 18629-41 :2006 7.5 折叠分支结构的定义对于折叠分支结构定义以下概念。7. 5. 1 Branch_homomorphic 当且仅当存在从一个最小活动树的一个分支的原子活动发生的集合到此最小活动树的另一个分支的原子活动发生的集合的映射时，此一个分支对于另一个分支是branch_homomorphic。(forall(?occ1 ?occ2) (iff branch_homomorphic ?occ1 ?occ2) (皿d(s皿e_grove?occ1 ?occ2) 7. 5. 2 Folded (forall(?s1 ?a)
38、 (implies(and(occurrence_of ?occ1 ?a) (subactivity_occurrence ?s1 ?occ1) (exists (?s2) (subactivity_occurrence ?s2 ?occ2) (hom ?s1 ?s2 ?a) 当且仅当存在一个单独的分支，使得最小活动树的每一个分支上的原子子活动发生的集合是这个单独的分支上的原子子活动发生的置换时，一个活动是folded。(forall(?occ) (iff(folded ?occ) (exists(?occ1) (and(same_grove ?occ1 ?occ) (forall(?occ2
39、) (implies(same_grove ?occ2 ?occ) (branch_homomorphic ?occ1 ?occ2) 7.5.3 Nondet_folded 当且仅当存在一个分支，使得最小活动树的每一个分支上的原子子活动发生的集合是第一个分支上的原子子活动发生的置换时，一个活动是nondet_folded。(forall(?occ) (iff(nondet_folded ?occ) (forall(?occ1) (implies(same_grove ?occ1 ?occ) (exists(?occ2) (and (same_grove ?occ2 ?occ) 7. 5. 4
40、Partial folded (not( = ?occ1 ?occ2) (branch_homomorphic ?occ1 ?occ2) 当且仅当存在一个分支，使得最小活动树的每一个分支上的原子子活动发生的集合是第一个分支上的原子子活动发生的置换时，一个活动是partiaLfolded0 (forall(?occ) (iff(partial_folded ?occ) (exists(?occ1 ?occ2 ?occ3) (and (same_grove ?occ1 ?occ) (same_grove ?occ2 ?occ) (not( = ?occ1 ?occ2) (branch_homomo
41、rphic ?occ1 ?occ2) (same_grove ?occ3 ?occ) (forall(?occ4) 9 GB/T 20719.4 1-2010/ISO 18629-41 :2006 (implies (and(same_grove ?occ4 ?occ) (not( = ?occ3 ?occ4) (not(branch_homomorphic ?occ3 ?occ4) 7.5.5 Rigid 当且仅当一个活动树中所有分支都不是分支同态，则称一个活动是rigido(forall(?occ) (iff(rigid ?occ) (forall(?occl ?occ2) (implie
42、s (and(same_grove ?occl ?occ) (s四e_grove?occ2 ?occ) (not( = ?occl ?occ2) (not(branch_homomorphic ?。但1?c2) 7.6 折叠分支结构的过程描述语法下列语法句子描述了用于折叠分支结构的KIF中详细说明的过程描述和辅助规则。(folded_spec ): : (exists( (variable) (and (same_tree(variable) ?occ) (occurrence_axiom) (nondet_folded_spec): = (exists(variable) (and(same
43、_tree(variable)?occ) (or(occurrence_axiom)祷)(partial_folded_spec): : = (or(丑。ndetfolded_spec)(rigid_spec) (rigid_spec): = (existsC (variable)祷(皿d(occurrence_formula)(branch_spec) (occurrenc_disjunct): = (occurrence_literal)I Cor(occurrence_literal)善)(occurrence_axiom ) : : = (exists ( variable川)(occ
44、urrence_disjunct) 8 非确定性活动:分支结构和排序本条款表征了有关非确定性活动:分支结构和排序的全部定义。8. 1 分支结构和排序的基本词汇分支结构和排序的词典不需要基本关系。8.2 分支结构和排序的定义词汇本条款中定义了以下关系:10 一一-(mono_tree?sl ?s2 ?a); 一一一(order_tree?sl ?s2 ?a); 一一一(root_automorphic?occl ?occ2); (ordered ?occ) ; -一一(nondet_ordered?occ); 一一一(broken_ordered?occ) ; (unordered ?occ)。
45、每一个概念由非正式语义和一个KIF公理来描述。GB/T 20719.4 1-2010/ISO 18629-41 :2006 8.3 分支结构和排序所需的理论本理论需要:一一-act_occ.th; 一一-cornplex.th; atornic. th; 二一-subactivity.th; 一一一occtree.th; 一一-psl_core.th。8.4 分支结构和排序所需的定义性扩展分支结构和排序不需要定义性扩展。8.5 分支结构和排序的定义对于为分支结构和排序定义以下概念。8. 5. 1 Mono_tree 生根于?sl的子树能被单一同态地嵌入到生根于?s2的子树中。(forall(?
46、sl ?s2 ?a)(iff(mono_tree ?sl ?s2 ?a) (forall(?s3 ?s4 ?s5) (implies (and(min_precedes ?sl ?s3 ?a) (min_precedes ?s2 ?s4 ?a) (mono ?s3 ?s4 ?a) (min_precedes ?s3 ?s5 ?a) 8. 5. 2 Order_tree (exists(?s6) (and(mono ?s5 ?s6 ?a) (min_precedes ?s4 ?s6 ?a) 当且仅当存在一个将生根于?sl的子树映射到生根于?s2的子树的序自同构时，此关系保持。(forall(?sl ?s2 ?a)(iff(order_tree ?sl ?s2 ?a) (and(mono_tree ?sl ?s2 ?a) (forall(?s3 ?s4 ?s5 ?s6) (implies (and(min_precedes ?sl ?s3 ?a) (min_precedes ?s2 ?s4 ?a) (cousin ?s3 ?s4 ?a) (min_precedes ?s3 ?s5 ?a) (cousin ?s5 ?s6 ?a) (iff
