Petri网可达性图计算问题排查及更优简化计算方法咨询

我正尝试为任意Petri网计算可达性图，但负责计算的函数无法触发已使能的变迁，生成的图里只有带初始标识的初始节点。想知道问题出在哪、怎么修正，同时求更优/简便的可达性计算方法。

相关代码如下：

def calculate_reachability_tree(num_places, num_transitions, markings_vector, incidence_matrix):
    # Initialize the reachability tree and markings list
    reachability_tree = nx.DiGraph()
    markings_list = [tuple(markings_vector.flatten())]
    reachability_tree.add_node(0)

    # Initialize the queue with the initial markings
    queue = deque([(0, markings_vector)])

    while queue:
        parent_index, parent_markings = queue.popleft()
        print(parent_markings)

        for t in range(num_transitions):
            print(num_transitions)
            # Check if the transition is enabled
            if np.all(parent_markings + incidence_matrix[:, t] >= 0):
                print('in if')
                # Fire the transition
                new_markings = parent_markings + incidence_matrix[:, t]

                # Check if the new markings are already in the markings list
                try:
                    child_index = markings_list.index(tuple(new_markings.flatten()))
                except ValueError:
                    # Add the new markings to the markings list and reachability tree
                    child_index = len(markings_list)
                    new_markings_clipped = new_markings[:num_places]
                    markings_list.append(tuple(new_markings_clipped.flatten()))
                    reachability_tree.add_node(child_index)
                    queue.append((child_index, new_markings_clipped))

                # Add an edge between the parent and child markings
                reachability_tree.add_edge(parent_index, child_index, transition=t)

    return reachability_tree, markings_list

问题排查与修正 #

1. 核心错误：使能判断逻辑颠倒 #

Petri网变迁使能的正确条件是所有输入库所的标识数 ≥ 该变迁对对应库所的消耗数。关联矩阵中，输入弧对应负数（表示消耗），输出弧对应正数（表示生成）。你当前用parent_markings + incidence_matrix[:, t] >= 0，这是判断触发后的标识是否非负，而非判断变迁是否满足触发前提。

正确的使能判断应该是：

# 验证所有输入库所的标识足够覆盖变迁消耗
if np.all(parent_markings >= -incidence_matrix[:, t]):

2. 次要问题：标识查找效率低下 #

用markings_list.index()查找已存在标识的时间复杂度是O(n)，当可达标识数量较多时会严重拖慢速度。建议改用字典映射标识元组到节点索引，将查找时间降为O(1)。

3. 潜在问题：标识裁剪冗余 #

代码中new_markings_clipped = new_markings[:num_places]属于冗余操作，只要incidence_matrix的行数等于num_places，new_markings本身就是对应所有库所的标识向量，无需裁剪。

修正后代码示例 #

import networkx as nx
from collections import deque
import numpy as np

def calculate_reachability_tree(num_places, num_transitions, markings_vector, incidence_matrix):
    # 初始化可达图与标识-索引映射（优化查找效率）
    reachability_tree = nx.DiGraph()
    initial_marking = tuple(markings_vector.flatten())
    marking_to_idx = {initial_marking: 0}
    reachability_tree.add_node(0, marking=initial_marking)

    queue = deque([(0, markings_vector.copy())])

    while queue:
        parent_idx, parent_markings = queue.popleft()

        for t in range(num_transitions):
            # 正确判断变迁使能
            if np.all(parent_markings >= -incidence_matrix[:, t]):
                new_markings = parent_markings + incidence_matrix[:, t]
                new_markings_tuple = tuple(new_markings.flatten())

                # 处理新标识
                if new_markings_tuple not in marking_to_idx:
                    child_idx = len(marking_to_idx)
                    marking_to_idx[new_markings_tuple] = child_idx
                    reachability_tree.add_node(child_idx, marking=new_markings_tuple)
                    queue.append((child_idx, new_markings.copy()))
                else:
                    child_idx = marking_to_idx[new_markings_tuple]

                # 添加变迁触发边
                reachability_tree.add_edge(parent_idx, child_idx, transition=t)

    # 转换为原接口要求的列表格式
    markings_list = [None] * len(marking_to_idx)
    for marking, idx in marking_to_idx.items():
        markings_list[idx] = marking

    return reachability_tree, markings_list

更优的可达性计算思路 #

1. 使用成熟Petri网库：直接用pm4py或pypetri等专业库，这些工具已经实现了高效的可达性分析、覆盖树生成等功能，无需手动实现底层逻辑。
2. 无界网处理：如果Petri网是无界的，可达性树会无限增长，此时应改用**覆盖树（Coverability Tree）**算法，通过标记ω符号避免无限循环。
3. 并行化优化：对于大型Petri网，可以将使能变迁的触发和标识检查逻辑并行化，提升计算速度。

内容的提问来源于stack exchange，提问作者samm bodie