《状态空间简介》由会员分享，可在线阅读，更多相关《状态空间简介（30页珍藏版）》请在金锄头文库上搜索。
1、CPN TOOLS 状态空间手册翻译：中国石油大学（华东）200710目录第1 章 状态空间简介 1状态空间工具的历史 1例子: Dining Philosophers 问题 1第2 章 状态空间工具的使用 3状态空间代码的产生 4细节与限制（第1次阅读可以跳过） 4状态空间的产生与强连通图 4标准报告 5统计函数 6状态空间传送到仿真器 6状态矢量从仿真器传递到状态空间 7第3 章 如何引用状态空间的条目 7节点、弧及强连通图 7库所实例 7变迁实例 8标记 8绑定元素 8字符串表达 9时间值 10第4 章 标准查询 10可达性 11有界性 11家性 12活性 13公平性 15第5 章 建立
2、自定义的查询 16节点和弧 16强连通部件 17查找节点 SearchNodes 17PredNodes 与 EvalNodes 20SearchNodes 调用举例 20查找弧 SearchArcs 21SearchArcs 调用举例 22查找强连通部件 SearchSccs 22SearchSccs 调用举例 23第6 章 改变选项 23字符串表示选项 String Representation Options 23节点和弧描述符选项 24计算状态空间的选项 25停止选项 25分支选项 SS tool 26保存报告选项 26参考文献 27第 1 章 状态空间简介状态空间工具的历史本手册给出
3、了计算和分析状态空间工具的描述 （也称作出现图，可达图或可达树）。状态空间工具是集成在CPN Tools里的。这意味着你可以很容易地在编辑器、模拟器和状态 空间工具之间切换。当一个状态空间节点发现后，它就可以在模拟器中观察到。这意味着在CPN 模型里你可以以图形方式看到这个标志。你可以看到触发的转移实例，研究其绑定以及模拟它。 与此类似地是，当在模拟器中发现一个标志，它可以加到状态空间里，或者作为一个新的状态 空间的初始标记。状态空间工具里有大量内置查询。可以用来调查一个CPN网的所有标准属性，例如可达性、 有界性、家性、活性、公平性。除此之外，还提供了大量搜索工具允许你定制自己的非标准查 询
4、。标准查询不需要任何编程，而非标准查询则需要你写2-5行简单的ML代码。例子: Dining Philosophers 问题状态空间最基本的想法就是对于每个可达的标记建立一个节点，对于每个发生的绑定元素建立一个弧而构成一个有向图。关于状态空间的介绍可以参看教材Sect. 5.1 of CPN 1和Sect.1.1 of CPN 2。本手册里我们用哲学家系统作为我们的主要的例子。 5 个中国哲学家围一个圆桌而坐，在桌子 的中央有一盘美味的米饭，在每2个哲学家之间有1只筷子，每个哲学家都交替进行思考和吃 饭，为了吃饭，哲学家需要 2 只筷子，而他只允许使用 2 只靠近他的筷子（即紧靠自己左右两 边
5、的）。而对筷子的共享使得近邻的两个哲学家不能同时吃饭。哲学家系统的CPN模型见下图。PH颜色集代表哲学家，CS颜色集代表筷子。函数phiph?ph 3C54Chopsticks 将每位哲学家映射为靠近他的2只筷子。vc.1 n = 5;iz-clc t 亍三 = inci.SK ph -vith L 二l；iz.cl = t C3 = index cs :fith 1. .n;VaL 匚；Pr.rfur ?hG3tLCk,5j =1 c： i i 十+ 1 Y ii.5 i z i_=i: then 1 els 3 l+lj ;dining philosophers问题的状态空间如下图。每个节
6、点代表一个可达的标记，而每个弧代表 从源节点到目的节点的一个绑定元素的发生。为了增加可读性，我们只显示了部分标记和绑定 元素的细节。需要说明的是所有的弧都是双弧，代表两个单独的弧。dining philosophers问题的状态空间是通过CPN Tools中的状态空间工具产生的。需要说明的 是这里的状态空间是非典型的。很多状态空间是非常大的。目前的版本可以处理20,000-200,000 个节点和50,000-2,000,000 条弧，当然前提是你的机器有足够的内存空间。将来的版本可以处理 大的多的状态空间。nu s-ed 1L cs ( 3)Eat: l-ph(l)+l ph(4)Tmki
7、psphflj Take : p-ph (4) J*第2 章 状态空间工具的使用计算状态空间、产生状态空间报告，在仿真器和状态空间工具之间传递状态矢量等可在状 态空间工具板完成。关于使用状态空间工具板的更多信息可以通过网页查找。状态空间代码的产生在状态空间计算之前，要产生状态空间代码，就是说用来计算和分析状态空间的ML代码。 为了产生状态空间代码，必须按顺序完成下面的步骤：a）确保所有的转移、库所和网中的页都有名字。名字必须是唯一的和满足ML-标识符要求 文字数字：任意顺序的字母、数字及 （） 、 （_），而且字母打头。b）对网使用状态空间工具，即选择状态空间工具板的卫nter SS”命令，将
8、它应用到网中的1 页上。新节点的产生过程是以“广度优先”原则完成的。这意味着处理的节点的顺序是它们产生 的顺序。在一个特定范围内，“深度优先”的产生可以通过使用选项Branching Options 的”narrow”（在第6章）获得。对于时控的状态空间，处理的顺序由建立时间确定。 （就是说，模型时间是单个标记开始存 在的时间）。我们建议你现在就试着建立dining philosophers问题的状态空间代码。模型叫做 DiningPhilosophers,位于CPN Tools工具下的Sample Nets目录下。细节与限制（第 1次阅读可以跳过）当你修改CPN图之后，你必须从图的草稿中重新
9、产生状态空间代码。这意味着状态空间已 经失效（如果有的话）。当模拟器中的修改发生时，再次应用“Enter SS命令就可以了。状态空间的计算是对网中那些可以参与模拟的部分而计算出来的。请记住，在状态空间里， 只是在非常有限的方式里使用代码有意义的，譬如，在CPN模型初始化时。在输出弧上使用自由变量是不允许的，除非他们是一个小颜色集的变量。状态空间的产生与强连通图当你产生了状态空间代码后（用前面介绍的步骤），你就准备好了状态空间的计算。如果状 态空间不大（譬如，几百个节点和弧），你简单在网的页上应用Calculate State Space计算状态 空间工具（从状态空间工具板上选）。此外，你可能需
10、要改变Stop Options或者Branching Options （第6章有述）。在第4章有许多查询函数使用强连通图。要计算强连通图，必须在网的页上使用状态空间工 具板上选的Calculate Scc Graph计算强连通图工具状态空间和强连通图也可以通过使用下面的ML函数然后使用Evaluate ML工具计算，这和 使用状态空间工具板是等价的。这在譬如由CPN模型或Stop options （见第6章）引起的异常情况下 是很有用的：fun CalculateOccGraph unit - unitfun CalculateSccGraph unit - unit 关于Calculate
11、State Space计算状态空间工具的选项在第6章中有介绍。标准报告当你为一个CPN网产生了状态空间后，你可以使用Save Report保存报告工具产生一个文 本文件，具体包含下面的信息： Statistics （状态空间大小和See图）. Boundedness Properties （库所实例的整数和多态集范围）. Home Properties （家标记）. Liveness Properties （死标记, 死/活变迁实例）. Fairness Properties （impartial/fair/just 变迁实例）.使用Save Report保存报告工具的选项（见第6章），我们可
12、以指定多少信息可以放到报告 中。这可以通过指定上面提及的1个或多个可能性实现。只有计算了强连通图家性和公平性才可 以包含进来。下面给出的是dining philosophers问题的全部标准报告：StatisticsState Space Nodes: 11 Arcs: 30Secs: 1 Status: Full Scc Graph Nodes: 1Arcs: 0Secs: 0Boundedness PropertiesBest Integer BoundsUpperLowerSystemEat 120SystemThink 153SystemUnused_Chopsticks 151Bes
13、t Upper Multi-set BoundsSys temEat 1 lph(1)+ lph(2)+lph(3)+1、ph(4)+ 1、ph(5)Sys temThink 1 lph(1)+ 1、ph(2)+ 1、ph(3)+ lph(4)+ lph(5)Sys temUnused_Chops ti cks 1 1、cs(1)+ 1、cs(2)+ 1、cs(3)+1、cs(4)+ 1、cs(5)Best Lower Multi-set Bounds SystemEat 1 emptySystemThink 1 empty SystemUnused_Chopsticks 1 empty Ho
14、me PropertiesHome Markings: All Liveness PropertiesDead Markings: NoneDead Transitions Instances: NoneLive Transitions Instances: AllFairness PropertiesSystemPut_Down_Chopsticks 1 Impartial SystemTake_Chopsticks 1 Impartial还可以定制库所实例和变迁实例的显示（譬如将SystemEat 1替换成Eat），这可以 通过第6章中介绍的St ring Represen tat ion
15、 Opt ion选项实现。统计函数为了获取状态空间大小和See图的规模，大量函数可以使用。状态空间至少有1个节点（即使Calculate State Space 计算状态空间工具没有使用）。按照惯例，数字1表示初始标记。如果状 态空间是不完整的，你可以再次使用Calculate State Space计算状态空间工具而扩展它（可能更 改了一些类似与Stop Op tions或Branching Opt ion选项）。关于状态空间和See图的计算统 计可以通过下面的ML函数访问：fun NoOfNodes unit - intfun NoOfArcs unit - intfun NoOfSecs unit - intfun EntireGraphCalculated unit - boolfun SccNoOfNodes unit -
