• 2019年3月10日 10:10

    Petri nets是一个并行系统的模型,用来描述系统状态的变化。 Petri nets由德国的 Carl Adam Petri在1962年的论文中提出。

    Petri nets有什么优势?它是用来描述并行系统的一个low-level的模型,可以快捷地表示并发、冲突和因果关系等。Petri nets可以表示有限状态和无限状态。
    听说过Statebox吗?statebox.org/ 是一个很有实力的团队,方向是形式化验证。他们有计划直接用Petri nets生成Rholang程序。好期待他们的成果。
    Petrinets1.png

    图中的圆圈表示位置(place), 方块表示变迁(transition),它们由有向的弧(arc)连接。
    位置(place)代表状态(state)、条件(condition)或资源(resource)
    变迁(transition)代表行动(action)

    Petrinets2.png

    标记有黑点(token)的位置表示具备了成熟的条件或资源,可以移动其它位置。这个行动称为fire。
    上图表示位置s1和s3条件具备,t可以fire,然后s2和s4将会被标记为黑点(token)。
    Dining philosophers是一个并行计算中很著名的例子,未来几天我们会专门讲解Rholang如何优雅地解决这个问题。

    Petrinets3.png

    哲学家们围坐在桌子边,每两个人中间放着一把叉子,他们的食物是意大利面。哲学家只有两个行为:eating和thinking。只有左右两手都握有一把叉子时,哲学家才能eating。因为叉子数量有限,所以他们不可能同时进餐。
    现在我们可以方便地用Petri nets图描述一下这个问题:
    Petrinets4.png

    Petri nets的详细讲解请见:www.cs.tau.ac.il/~nachumd/models/Nets.pdf

    Petrinets4.png

    PNG, 68.8 KB, 被 Dimworm上传于2019年3月10日

    Petrinets3.png

    PNG, 23.8 KB, 被 Dimworm上传于2019年3月10日

    Petrinets2.png

    PNG, 10.1 KB, 被 Dimworm上传于2019年3月10日

    Petrinets1.png

    PNG, 9.5 KB, 被 Dimworm上传于2019年3月10日