search

ustcanycall / OS

0 stars 0 forks source link

调研9 #12

Open ustcanycall opened 10 years ago

ustcanycall commented 10 years ago

Petri网模型

简介

Petri网是对离散并行系统的数学表示。Petri网是1960年代由卡尔·A·佩特里发明的，适合于描述异步的、并发的计算机系统模型。 Petri网既有严格的数学表述方式，也有直观的图形表达方式，既有丰富的系统描述手段和系统行为分析技术，又为计算机科学提供坚实的概念基础。

经典模型

经典的Petri网是简单的过程模型，由两种节点：库所和变迁，有向弧，以及令牌等元素组成的。 2e2eb9389b504fc22cd202e4e5dde71191ef76c6a6ef4d7e

结构

  1. 库所（Place）圆形节点
  2. 变迁（Transition）方形节点
  3. 有向弧（Connection）是库所和变迁之间的有向弧
  4. 令牌（Token）是库所中的动态对象，可以从一个库所移动到另一个库所。

    规则

  5. 有向弧是有方向的
  6. 两个库所或变迁之间不允许有弧
  7. 库所可以拥有任意数量的令牌

    行为

  8. 如果一个变迁的每个输入库所（input place）都拥有令牌，该变迁即为被允许(enable)。一个变迁被允许时，变迁将发生(fire)，输入库所(input place)的令牌被消耗，同时为输出库所(output place)产生令牌。
  9. 变迁的发生是完整的，也就是说，没有一个变迁只发生了一半的可能性。
  10. 有两个或多个变迁都被允许的可能，但是一次只能发生一个变迁。这种情况下变迁发生的顺序没有定义。
  11. 如果出现一个变迁，其输入库所的个数与输出库所的个数不相等，令牌的个数将发生变化，也就是说，令牌数目不守恒。
  12. Petri网络是静态的，也就是说，不存在发生了一个变迁之后忽然冒出另一个变迁或者库所，从而改变Petri网结构的可能。
  13. Petri网的状态由令牌在库所的分布决定。也就是说，变迁发生完毕、下一个变迁等待发生的时候才有确定的状态，正在发生变迁的时候是没有一个确定的状态的。

    流程

一个流程的状态是由在场所中的令牌建模的，状态的变迁是由变迁建模的。令牌表示事物（人，货物，机器），信息，条件，或对象的状态； 库所代表库所，通道或地理位置；变迁代表事件，转化或传输。 一个流程有当前状态，可达状态，不可达状态。终止状态。

Petri网模拟仿真工具简介

Visual Object Net ++

Visual Object Net ++可以说是一款入门级的模拟软件了。具有非常直观的操作和非常强大的功能。支持时间以及混杂网，但是我们用得最多的还是使用它来队最普通的P/T网建模。

clip_image001

CPNTools

CPN Tools是颜色Petri网领域鼎鼎大名的建模软件，操作界面如同所示： 其操作也独具特色--添加库所、变迁以及弧的方法是使用鼠标右键点击不放，在出现的圆形弹出菜单内用左键选择相应的项目。

4

NuSMV

NuSMV-2.5.2编译 1.首先到NuSMV的主页下载NuSMV-2.5.2 http://nusmv.fbk.eu/bin/download_src2-v2.cgi

2.解压后，有四个文件夹 +NuSMV-2.5.2 +cudd-2.4.1.1 //BDD package, University of Colorado +MiniSat //open-source SAT solver +nusmv +zchaff //open-source SAT solver, non-commercial purposes only

3.编译MiniSat 进入到MiniSat目录 $ ./build.sh

会自动下载minisat2-070721.zip,自动解压、编译

4.zchaff和MiniSat类似,不过默认的是下载64bit的代码,需要修改一下zchaff-default.in

# this is for the older version
zchaff_ver=2004.11.15
zchaff_zip=zchaff.$zchaff_ver.zip
zchaff_dir=zchaff

#zchaff_ver=2007.3.12
#zchaff_zip=zchaff.64bit.$zchaff_ver.zip
zchaff_url="http://www.princeton.edu/~chaff/zchaff/${zchaff_zip}"
#zchaff_dir=zchaff64

# ----------------------------------------------------------------------
zchaff_patch=zchaff.${zchaff_ver}_nusmv.patch
#zchaff_patch=zchaff.64bit.${zchaff_ver}_nusmv.patch

5.编译cudd 在cudd-2.4.1.1目录下执行 $ make DDDEBUG= MTRDEBUG= ICFLAGS=-O2

经过上面的步骤后，依赖的bdd/sat slover都编译好了。

安装expat的头文件 sudo apt-get install libexpat1-dev 6.编译nusmv (在nusmv目录下) $> ./configure zchaff sat solver 默认不会链接到NuSMV可执行文件中, 需要的话，./configure --enable-zchaff $> make $> make install