状态空间简介.doc

CPN TOOLS状态空间手册 翻译：中国石油大学（华东） 2007．10目录 第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章 建立自定义的查询 16 节点和弧 16 强连通部件 17 查找节点SearchNodes 17 PredNodes 与 EvalNodes 20 SearchNodes调用举例 20 查找弧SearchArcs 21 SearchArcs调用举例 22 查找强连通部件SearchSccs 22 SearchSccs调用举例 23 第6章 改变选项 23 字符串表示选项String Representation Options 23 节点和弧描述符选项 24 计算状态空间的选项 25 停止选项 25 分支选项 SS tool 26 保存报告选项 26 参考文献 27 第1章 状态空间简介 状态空间工具的历史 本手册给出了计算和分析状态空间工具的描述 (也称作出现图，可达图或可达树)。 状态空间工具是集成在CPN Tools里的。这意味着你可以很容易地在编辑器、模拟器和状态空间工具之间切换。当一个状态空间节点发现后，它就可以在模拟器中观察到。这意味着在CPN模型里你可以以图形方式看到这个标志。你可以看到触发的转移实例，研究其绑定以及模拟它。与此类似地是，当在模拟器中发现一个标志，它可以加到状态空间里，或者作为一个新的状态空间的初始标记。 状态空间工具里有大量内置查询。可以用来调查一个CPN网的所有标准属性，例如可达性、有界性、家性、活性、公平性。除此之外，还提供了大量有哪些信誉好的足球投注网站工具允许你定制自己的非标准查询。标准查询不需要任何编程，而非标准查询则需要你写2-5行简单的ML 代码。 例子: Dining Philosophers问题 状态空间最基本的想法就是对于每个可达的标记建立一个节点，对于每个发生的绑定元素建立一个弧而构成一个有向图。关于状态空间的介绍可以参看教材Sect. 5.1 of [CPN 1] 和 Sect. 1.1 of [CPN 2]。 本手册里我们用哲学家系统作为我们的主要的例子。5个中国哲学家围一个圆桌而坐，在桌子的中央有一盘美味的米饭，在每2个哲学家之间有1只筷子，每个哲学家都交替进行思考和吃饭，为了吃饭，哲学家需要2只筷子，而他只允许使用2只靠近他的筷子（即紧靠自己左右两边的）。而对筷子的共享使得近邻的两个哲学家不能同时吃饭。 哲学家系统的CPN模型见下图。PH 颜色集代表哲学家，CS 颜色集代表筷子。函数Chopsticks 将每位哲学家映射为靠近他的2只筷子。 dining philosophers问题的状态空间如下图。每个节点代表一个可达的标记，而每个弧代表从源节点到目的节点的一个绑定元素的发生。为了增加可读性，我们只显示了部分标记和绑定元素的细节。需要说明的是所有的弧都是双弧，代表两个单独的弧。 dining philosophers问题的状态空间是通过CPN Tools中的状态空间工具产生的。需要说明的是这里的状态空间是非典型的。很多状态空间是非常大的。目前的版本可以处理20,000-200,000个节点和50,000-2,000,000 条弧，当然前提是你的机器有足够的内存空间。将来的版本可以处理大的多的状态空间。  第2章 状态空间工具的使用 计算状态空间产生状态空间报告，在仿真器和状态空间工具之间传递状态矢量等http://wiki.daimi.au.dk/cpntools-help/use_state_space_tool.wiki 状态空间代码的产生 在状态空间计算之前，要产生状态空间代码，就是说用来计算和分析状态空间的ML 代码。为了产生状态空间代码，必须按顺序完成下面的步骤： a) 确保所有的转移、库所和网中的页都有名字。名字必须是唯一的和满足ML-标识符要求文字数字：任意顺序的字母、数字及 (’) 、(_)，而且字母打头。 b) 对网使用状态空间工具，即选择状态空间工具板的“Enter SS”命令，将它应用到网中的1页上。 新节点的产生过程是以“广度优先”原则完成的。这意味着处理的节点的顺序是它们产生的顺序。在一个特定范围内，“深度优先” 的