PetriStructureReducer.cpp

#include <chrono>
#include <omp.h>
#include "PetriStructureReducer.h"
#include "Petri_Net.h"
#include <algorithm>  // 为std::find
#include <atomic>
#include <numeric>  // 为std::gcd
#include <functional>
#include <limits>   // 为numeric_limits
#include "DebugConfig.h"
// PetriStructureReducer.cpp

bool PetriStructureReducer::importFromFile(const string& filename) {
    ifstream fin(filename);
    if (!fin) {
        cerr << "无法打开文件: " << filename << endl;
        return false;
    }

    // 清空现有数据
    places.clear();
    transitions.clear();
    units.clear();
    significantPlaces.clear();  // 清空重要库所集合

    // 读取库所、变迁和重要库所的总数
    int totalPlaces, totalTransitions, totalSignificant;
    fin >> totalPlaces >> totalTransitions >> totalSignificant;

    // 读取重要库所列表
    for (int i = 0; i < totalSignificant; i++) {
        string placeId;
        fin >> placeId;
        significantPlaces.insert(placeId);
    }

    // 读取库所信息
    for (int i = 0; i < totalPlaces; i++) {
        string id, unitId;
        unsigned int tokens;
        fin >> id >> tokens >> unitId;

        PetriPlace place;
        place.id = id;
        place.tokens = tokens;
        place.unitId = unitId;
        places[id] = place;

        // 同时更新或创建unit
        if (units.find(unitId) == units.end()) {
            units[unitId] = PetriUnit{unitId, {}};
        }
        units[unitId].places.insert(id);
    }

    // 读取变迁信息
    for (int i = 0; i < totalTransitions; i++) {
        string id;
        int inCount, outCount;
        fin >> id >> inCount >> outCount;

        PetriTransition trans;
        trans.id = id;

        // 读取输入库所
        for (int j = 0; j < inCount; j++) {
            string placeId;
            weight_t weight;
            fin >> placeId >> weight;
            trans.inPlaces[placeId] = weight;
            places[placeId].outTransitions[id] = weight;
        }

        // 读取输出库所
        for (int j = 0; j < outCount; j++) {
            string placeId;
            weight_t weight;
            fin >> placeId >> weight;
            trans.outPlaces[placeId] = weight;
            places[placeId].inTransitions[id] = weight;
        }

        transitions[id] = trans;
    }

    fin.close();
    return true;
}

void PetriStructureReducer::exportToFile(const string& filename) const {
    // 打开输出文件
    ofstream fout(filename);
    if (!fout) {
        cerr << "无法创建文件: " << filename << endl;
        return;
    }

    // ===== 1. 写入网络基本信息 =====
    // 格式: [库所数量] [变迁数量] [重要库所数量]
    fout << places.size() << " " 
         << transitions.size() << " " 
         << significantPlaces.size() << endl;

    // ===== 2. 写入重要库所列表 =====
    // 格式: 每行一个库所ID
    for (const string& placeId : significantPlaces) {
        fout << placeId << endl;
    }

    // ===== 3. 写入所有库所信息 =====
    // 格式: [库所ID] [标识数] [单元ID]
    for (const auto& [id, place] : places) {
        fout << place.id << " " 
             << place.tokens << " " 
             << place.unitId << endl;
    }

    // ===== 4. 写入所有变迁信息 =====
    for (const auto& [id, trans] : transitions) {
        // 变迁头部信息: [变迁ID] [输入库所数量] [输出库所数量]
        fout << trans.id << " " 
             << trans.inPlaces.size() << " " 
             << trans.outPlaces.size() << endl;
        
        // 写入输入库所及其权重
        // 格式: [库所ID] [权重]
        for (const auto& [placeId, weight] : trans.inPlaces) {
            fout << placeId << " " << weight << endl;
        }
        
        // 写入输出库所及其权重
        // 格式: [库所ID] [权重]
        for (const auto& [placeId, weight] : trans.outPlaces) {
            fout << placeId << " " << weight << endl;
        }
    }

    fout.close();
}

void PetriStructureReducer::importFromPetri(const Petri& petri, const set<index_t>& vis, bool cardinality) {
    // 导入库所
    for(index_t i = 0; i < petri.placecount; i++) {
        PetriPlace place;
        const Place& originalPlace = petri.place[i];
        
        place.id = originalPlace.id;
        place.tokens = originalPlace.initialMarking;
        if(petri.NUPN) {
            place.unitId = petri.unittable[petri.nupnExtra[i].myunit].uid;
        } else {
            place.unitId = "";
        }
        place.atomicLinks = originalPlace.atomicLinks;
        
        // 导入弧
        for(const auto& arc : originalPlace.producer) {
            place.inTransitions[petri.transition[arc.idx].id] = arc.weight;
        }
        for(const auto& arc : originalPlace.consumer) {
            place.outTransitions[petri.transition[arc.idx].id] = arc.weight;
        }
        
        places[place.id] = place;
        if(petri.NUPN) {
            units[place.unitId].places.insert(place.id);
        }
    }

    // 导入变迁
    for(index_t i = 0; i < petri.transitioncount; i++) {
        PetriTransition trans;
        const Transition& originalTrans = petri.transition[i];
        
        trans.id = originalTrans.id;
        
        for(const auto& arc : originalTrans.producer) {
            trans.inPlaces[petri.place[arc.idx].id] = arc.weight;
        }
        for(const auto& arc : originalTrans.consumer) {
            trans.outPlaces[petri.place[arc.idx].id] = arc.weight;
        }
        
        transitions[trans.id] = trans;
    }

    // 设置重要元素（库所或变迁）
    // cout<<"vis: "<<endl;
    // for (auto i :vis){
    //     cout<<i <<" ";
    // }cout<<endl;
    if(cardinality) {
        // 对于Cardinality: 重要元素是查询中引用的库所
        for(auto idx : vis) {
            significantPlaces.insert(petri.place[idx].id);
        }
    } else {
        // 对于Fireability: 重要元素是查询中引用的变迁
        // 首先收集变迁的ID
        for(auto idx : vis) {
            significantTransitions.insert(petri.transition[idx].id);
        }
        
        // 对于Fireability约简，我们需要识别出变迁的输入库所
        // 因为变迁能否激活取决于其所有输入库所是否有足够的标记
        for(const auto& transId : significantTransitions) {
            const auto& trans = transitions[transId];
            // 将变迁的所有输入库所标记为重要库所
            for(const auto& [placeId, _] : trans.inPlaces) {
                significantPlaces.insert(placeId);
            }
        }
    }
    for(auto i:significantPlaces){
        DEBUG_INFO("significantPlaces: "<<i);
    } 
    // for(auto i)
    // cout<<endl;
}

void PetriStructureReducer::exportToPetri(Petri& petri) {
    // 清理原有数据
    delete[] petri.place;
    delete[] petri.transition;
    delete[] petri.unittable;
    delete[] petri.nupnExtra;    
    // map<string,index_t> mapPlace;
    // map<string,index_t> mapTransition;
    bool& LONGBITPLACE = petri.LONGBITPLACE;
    petri.mapPlace.clear();
    petri.mapTransition.clear();

    // 设置新的大小
    petri.placecount = places.size();
    petri.transitioncount = transitions.size();
    petri.unitcount = units.size();

    // 创建映射表
    unordered_map<string, index_t> placeIndex;
    unordered_map<string, index_t> transitionIndex;
    unordered_map<string, index_t> unitIndex;

    // 分配内存
    petri.place = new Place[petri.placecount];
    petri.transition = new Transition[petri.transitioncount];
    if(petri.NUPN) {
        petri.nupnExtra = new NUPN_extra[petri.placecount];
        petri.unittable = new Unit[petri.unitcount];
        // 导出unit
        index_t unitIdx = 0;
        for(const auto& unit : units) {
            petri.unittable[unitIdx].uid = unit.first;
            petri.unittable[unitIdx].size = unit.second.places.size();
            unitIndex[unit.first] = unitIdx++;
        }
    } else {
        petri.nupnExtra = nullptr;
        petri.unittable = nullptr;
    }

    // 导出place
    index_t placeIdx = 0;
    for(const auto& p : places) {
        const PetriPlace& place = p.second;
        placeIndex[place.id] = placeIdx;
        petri.mapPlace[place.id] = placeIdx;
        
        petri.place[placeIdx].id = place.id;
        petri.place[placeIdx].initialMarking = place.tokens;
        petri.place[placeIdx].atomicLinks = place.atomicLinks;
        
        // 临时存储，等所有索引建立后再填充
        if(petri.NUPN) {
            petri.nupnExtra[placeIdx].myunit = unitIndex[place.unitId];
        } else {
            // petri.nupnExtra[placeIdx].myunit = -1;
        }
        
        placeIdx++;
    }

    // 导出transition
    index_t transIdx = 0;
    for(const auto& t : transitions) {
        const PetriTransition& trans = t.second;
        transitionIndex[trans.id] = transIdx;
        petri.mapTransition[trans.id] = transIdx;
        
        petri.transition[transIdx].id = trans.id;
        petri.transition[transIdx].significant = true;
        
        transIdx++;
    }

    // 填充弧信息
    for(const auto& p : places) {
        const PetriPlace& place = p.second;
        index_t pIdx = placeIndex[place.id];
        
        // 处理入弧
        for(const auto& arc : place.inTransitions) {
            SArc sarc;
            sarc.weight = arc.second;
            sarc.idx = transitionIndex[arc.first];
            petri.place[pIdx].producer.push_back(sarc);
        }
        
        // 处理出弧
        for(const auto& arc : place.outTransitions) {
            SArc sarc;
            sarc.weight = arc.second;
            sarc.idx = transitionIndex[arc.first];
            petri.place[pIdx].consumer.push_back(sarc);
        }
    }

    // 填充变迁的弧信息
    for(const auto& t : transitions) {
        const PetriTransition& trans = t.second;
        index_t tIdx = transitionIndex[trans.id];
        
        // 处理入弧
        for(const auto& arc : trans.inPlaces) {
            SArc sarc;
            sarc.weight = arc.second;
            sarc.idx = placeIndex[arc.first];
            petri.transition[tIdx].producer.push_back(sarc);
        }
        
        // 处理出弧
        for(const auto& arc : trans.outPlaces) {
            SArc sarc;
            sarc.weight = arc.second;
            sarc.idx = placeIndex[arc.first];
            petri.transition[tIdx].consumer.push_back(sarc);
        }
    }

    // 计算unit相关的编码信息
    if(petri.NUPN) {
        index_t temp_len = 0;
        index_t startpos = 0;
        for(index_t i = 0; i < petri.unitcount; i++) {
            petri.unittable[i].startpos = startpos;
            petri.unittable[i].mark_sp = temp_len;
            petri.unittable[i].mark_length = ceil(log2(petri.unittable[i].size + 1));
            temp_len = temp_len + petri.unittable[i].mark_length;
        }

        // 计算place的编码信息
        for(const auto& p : places) {
            index_t pIdx = placeIndex[p.first];
            const PetriUnit& unit = units[p.second.unitId];
            auto it = unit.places.find(p.first);
            index_t offset = distance(unit.places.begin(), it);
            
        NUPN_extra& pe = petri.nupnExtra[pIdx];
        const Unit& uu = petri.unittable[pe.myunit];
        
        pe.myoffset = offset;
        pe.intnum = uu.mark_sp / 32;
        pe.intoffset = uu.mark_sp % 32;
        pe.read_mask = (((mask_t)1 << uu.mark_length) - 1) << pe.intoffset;
        pe.zero_mask = ~(pe.read_mask);
        pe.write_mask = ((mask_t)pe.myoffset + 1) << pe.intoffset;
        }
    }
}

void PetriStructureReducer::printNetworkStatistics(const string& prefix) const {
    DEBUG_INFO(prefix << "网络统计信息：");
    DEBUG_INFO(prefix << "- 库所数量: " << places.size());
    DEBUG_INFO(prefix << "- 变迁数量: " << transitions.size());
    DEBUG_INFO(prefix << "- 单元数量: " << units.size());
    DEBUG_INFO(prefix << "- 重要库所数量: " << significantPlaces.size());
    
    // 计算弧的总数
    size_t totalArcs = 0;
    for(const auto& [_, trans] : transitions) {
        totalArcs += trans.inPlaces.size() + trans.outPlaces.size();
    }
    DEBUG_INFO(prefix << "- 弧数量: " << totalArcs);
}

string PetriStructureReducer::getTransitionSignature(const PetriTransition& trans) const {
    // Step 1: Collect and sort input arcs (place ID and weight)
    // Use vector of pairs and sort by place ID string
    vector<pair<string, int>> sortedInArcs(trans.inPlaces.begin(), trans.inPlaces.end());
    sort(sortedInArcs.begin(), sortedInArcs.end(), [](const auto& a, const auto& b){
        return a.first < b.first; // Sort pairs based on the place ID (string comparison)
    });

    // Step 2: Collect and sort output arcs (place ID and weight)
    vector<pair<string, int>> sortedOutArcs(trans.outPlaces.begin(), trans.outPlaces.end());
    sort(sortedOutArcs.begin(), sortedOutArcs.end(), [](const auto& a, const auto& b){
        return a.first < b.first; // Sort pairs based on the place ID (string comparison)
    });

    // Step 3: Build the signature string
    // Format: "in:pID1:w1,pID2:w2|out:pID3:w3,pID4:w4"
    string signature = "in:";
    for (const auto& p_w : sortedInArcs) {
        signature += p_w.first + ":" + to_string(p_w.second) + ",";
    }
    // Remove the trailing comma if there were input places
    if (!sortedInArcs.empty()) {
        signature.pop_back();
    }

    signature += "|out:";
    for (const auto& p_w : sortedOutArcs) {
        signature += p_w.first + ":" + to_string(p_w.second) + ",";
    }
    // Remove the trailing comma if there were output places
    if (!sortedOutArcs.empty()) {
        signature.pop_back();
    }

    return signature;
}


// -----------------------------------------------------------------------------
// Rule Lpre: Remove strictly identical duplicate transitions.
// This rule groups transitions by their arc signatures and removes all but one
// transition from each group of duplicates, unless any transition in the group
// is marked as significant. This should be applied before other reduction rules
// like Rule L to handle duplicates cleanly.
// -----------------------------------------------------------------------------
int PetriStructureReducer::removeDuplicateTransitionsRuleLpre() {
    int count = 0; // Counter for removed transitions
    // Map to group transition IDs by their unique signature
    // Key: signature string, Value: vector of transition IDs with that signature
    unordered_map<string, vector<string>> signatureToTransitionIds;
    // List of transition IDs that are marked for removal
    vector<string> toRemove;

    // Step 1: Group transitions by their signature
    // Iterate through all transitions in the net
    for (const auto& [transId, trans] : transitions) {
        // Get the unique signature for the current transition
        string signature = getTransitionSignature(trans);
        // Add the transition's ID to the vector associated with this signature
        signatureToTransitionIds[signature].push_back(transId);
    }

    // Step 2: Identify duplicate groups and mark transitions for removal
    // Iterate through the map of signatures to transition lists
    for (const auto& [signature, transIds] : signatureToTransitionIds) {
        // If a signature maps to more than one transition ID, these are duplicates
        if (transIds.size() > 1) {
            bool hasSignificant = false;
            // Check if *any* transition within this group of duplicates is marked as significant
            for (const string& transId : transIds) {
                if (significantTransitions.count(transId)) {
                    hasSignificant = true;
                    break; // Found a significant transition, we should keep all duplicates in this group
                }
            }

            // If the group does NOT contain any significant transition, mark duplicates for removal
            if (!hasSignificant) {
                // We keep the first transition in the list (arbitrary choice as the representative)
                // Mark all subsequent transitions in the list for removal
                for (size_t i = 1; i < transIds.size(); ++i) {
                    // Add the ID to the toRemove list
                    toRemove.push_back(transIds[i]);
                }
            }
            // If hasSignificant is true, the entire group of duplicates is kept. Do nothing here.
        }
    }

    // Step 3: Perform the actual removal of marked transitions
    // Iterate through the list of transitions to remove
    for (const string& transId : toRemove) {
         // Safety check: Double-check that the transition is not significant before removing.
         // Based on the logic in Step 2 (hasSignificant), this check should theoretically
         // always pass for transitions in the 'toRemove' list, but it adds robustness.
         if (significantTransitions.find(transId) == significantTransitions.end()) {
            // Call the function to remove the transition from the net structure
            eraseTransition(transId); // Assumes eraseTransition correctly updates transitions map, arcs, and place connections
            count++; // Increment the counter for successfully removed transitions
         }
    }

    // Return the total number of duplicate transitions removed
    return count;
}

void PetriStructureReducer::reduce(string &applyrules, int time_limit_reduce, bool contains_next, bool all_ltl) {
    // 在约简开始前打印统计信息
    DEBUG_INFO("约简前:");
    printNetworkStatistics("  ");
    
    int total = 0;
    double allTime = 0;
    
    // 执行各种约简操作
    int count;
    auto start = chrono::high_resolution_clock::now();
    
    // 根据LTL属性的特性确定约简策略
    bool changed = true;
    bool RQ = false;
    
    //限时
    auto periodicEnd = chrono::high_resolution_clock::now();
    auto periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
    
    int duplicatesRemoved = removeDuplicateTransitionsRuleLpre();
    DEBUG_INFO("Removed " << duplicatesRemoved << " duplicate transitions.");
    // cout << "Removed " << duplicatesRemoved << " duplicate transitions." << endl;
    do {
restart:
        // 如果LTL公式不包含NEXT操作符，可以应用更多规则
        if (!contains_next) {
            // 应用规则I AutoFlight-PT-06b-LTLFireability-08
            if(applyrules.find("i") != string::npos) {
                // count = removeIrrelevantElements();
                changed = (count > 0);
                // cout << "irrelevant_elements countsum:" << count << endl;

                periodicEnd = chrono::high_resolution_clock::now();
                periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                if (periodicDuration.count() > time_limit_reduce * 1000) {
                    // cout << "时间限制到达，停止约简" << endl;
                    return;
                }
            }
        }
        
        // 应用规则J（GCD约简）- 这个规则对所有类型的公式都适用
        if(applyrules.find("j") != string::npos) {
            // count = reducePlaceWeightsByGCD();
            changed |= (count > 0);
            // DEBUG_INFO("reducePlaceWeightsByGCD countsum:" << count);
            // cout << "reduce_weights_by_gcd countsum:" << count << endl;

            periodicEnd = chrono::high_resolution_clock::now();
            periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
            if (periodicDuration.count() > time_limit_reduce * 1000) {
                // cout << "时间限制到达，停止约简" << endl;
                return;
            }
        }
        
        do {
            do { 
                // 首先应用不移动标记的规则
                changed = false;
                
                // 规则E和规则N都不会改变网络的行为
                // E对于识别和移除死变迁是不完全的
                if(applyrules.find("e") != string::npos) {
                    count = applyRuleE();
                    changed |= (count > 0);
                    DEBUG_INFO("rule_e countsum:" << count);
                    // cout << "rule_e countsum:" << count << endl;

                    periodicEnd = chrono::high_resolution_clock::now();
                    periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                    if (periodicDuration.count() > time_limit_reduce * 1000) {
                        // cout << "时间限制到达，停止约简" << endl;
                        return;
                    }
                }
                
                // 规则N 疑似有bug， CSRepetitions-PT-02-LTLCardinality 验证
                if(applyrules.find("n") != string::npos) {
                    // count = removeNonDisablingArcs();
                    changed |= (count > 0);
                    // cout << "non_disabling_arcs countsum:" << count << endl;

                    periodicEnd = chrono::high_resolution_clock::now();
                    periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                    if (periodicDuration.count() > time_limit_reduce * 1000) {
                        // cout << "时间限制到达，停止约简" << endl;
                        return;
                    }
                }
                
                // 应用规则C
                if(applyrules.find("c") != string::npos) {
                    count = applyRuleFusionParallelPlaces();
                    changed |= (count > 0);
                    DEBUG_INFO("rule_c countsum:" << count);
                    // cout << "rule_c countsum:" << count << endl;

                    periodicEnd = chrono::high_resolution_clock::now();
                    periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                    if (periodicDuration.count() > time_limit_reduce * 1000) {
                        // cout << "时间限制到达，停止约简" << endl;
                        return;
                    }
                }

                // 基于公式特性应用规则
                if (!contains_next) {
                    // 规则F（冗余库所）可能会影响循环结构
                    if(applyrules.find("f") != string::npos) {
                        count = removeRedundantPlacesRuleF();
                        changed |= (count > 0);
                        DEBUG_INFO("redundant_places_rule_f countsum:" << count);
                        // cout << "redundant_places_rule_f countsum:" << count << endl;

                        periodicEnd = chrono::high_resolution_clock::now();
                        periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                        if (periodicDuration.count() > time_limit_reduce * 1000) {
                            // cout << "时间限制到达，停止约简" << endl;
                            return;
                        }
                    }
                    
                    // 规则G（冗余变迁） AutonomousCar-PT-02b-LTLFireability-09 
                    if(applyrules.find("g") != string::npos) {
                        // count = removeRedundantTransitionsRuleG();
                        changed |= (count > 0);
                        // cout << "redundant_transitions_rule_g countsum:" << count << endl;

                        periodicEnd = chrono::high_resolution_clock::now();
                        periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                        if (periodicDuration.count() > time_limit_reduce * 1000) {
                            // cout << "时间限制到达，停止约简" << endl;
                            return;
                        }
                    }

                    // 规则D（变迁融合）
                    if(applyrules.find("d") != string::npos) {
                        count = applyRuleD();
                        changed |= (count > 0);
                        DEBUG_INFO("rule_d countsum:" << count);
                        // cout << "rule_d countsum:" << count << endl;

                        periodicEnd = chrono::high_resolution_clock::now();
                        periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                        if (periodicDuration.count() > time_limit_reduce * 1000) {
                            // cout << "时间限制到达，停止约简" << endl;
                            return;
                        }
                    }
                }
            } while (changed);
            
            // 应用可能移动标记的规则
            if (!contains_next) {
                // 规则B（串行变迁合并）疑似有bug，BridgeAndVehicles-PT-V04P05N02-LTLCardinality 验证
                if(applyrules.find("b") != string::npos) {
                    // count = applyRuleB();
                    changed |= (count > 0);
                    // cout << "rule_b countsum:" << count << endl;

                    periodicEnd = chrono::high_resolution_clock::now();
                    periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                    if (periodicDuration.count() > time_limit_reduce * 1000) {
                        // cout << "时间限制到达，停止约简" << endl;
                        return;
                    }
                }

                // 规则A（变迁扩展）
                if(applyrules.find("a") != string::npos) {
                    count = applyRuleA();
                    changed |= (count > 0);
                    DEBUG_INFO("rule_a countsum:" << count);
                    // cout << "rule_a countsum:" << count << endl;

                    periodicEnd = chrono::high_resolution_clock::now();
                    periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                    if (periodicDuration.count() > time_limit_reduce * 1000) {
                        // cout << "时间限制到达，停止约简" << endl;
                        return;
                    }
                }
            }
        } while (changed);
        // 应用规则L（结构等价变迁合并）DES-PT-00a-LTLCardinality-03 验证 AutonomousCar-PT-02b-LTLFireability-09 

        if(applyrules.find("l") != string::npos) {
            // count = removeRedundantTransitionsRuleL();
            changed |= (count > 0);
            // cout << "redundant_transitions_rule_l countsum:" << count << endl;

            periodicEnd = chrono::high_resolution_clock::now();
            periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
            if (periodicDuration.count() > time_limit_reduce * 1000) {
                // cout << "时间限制到达，停止约简" << endl;
                return;
            }
        }
        
        // 对于不包含NEXT的LTL公式，可以应用更多高级规则
        if (!contains_next && !changed) {
            // 规则H（处理自循环）
            if(applyrules.find("h") != string::npos) {
                // bool ruleHApplied = applyRuleH();
                // changed |= ruleHApplied;
                
                // if (ruleHApplied) {
                    // cout << "rule_h applied" << endl;
                // }
                periodicEnd = chrono::high_resolution_clock::now();
                periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                if (periodicDuration.count() > time_limit_reduce * 1000) {
                    // cout << "时间限制到达，停止约简" << endl;
                    return;
                }
            }

            
            // 规则S（复杂结构替换）
            if(applyrules.find("s") != string::npos) {
                // count = applyRuleS();
                changed |= (count > 0);
                // cout << "rule_s countsum:" << count << endl;

                periodicEnd = chrono::high_resolution_clock::now();
                periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                if (periodicDuration.count() > time_limit_reduce * 1000) {
                    // cout << "时间限制到达，停止约简" << endl;
                    return;
                }
            }
            
            // 规则R（后置聚合）- 作为最后的手段
            if(applyrules.find("r") != string::npos) {
                // count = applyRuleR();
                changed |= (count > 0);
                DEBUG_INFO("rule_r countsum:" << count);
                // cout << "rule_r countsum:" << count << endl;

                periodicEnd = chrono::high_resolution_clock::now();
                periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
                if (periodicDuration.count() > time_limit_reduce * 1000) {
                    // cout << "时间限制到达，停止约简" << endl;
                    return;
                }
            }
        }
        
        // 规则Q可能会让之前应用不了的规则变得可以应用
        if(applyrules.find("q") != string::npos) {
            if (!changed && !RQ && !contains_next) {
                RQ = (applyRuleQ() > 0);
                if (RQ) {
                    DEBUG_INFO("rule_q applied, restarting...");
                    // cout << "rule_q applied, restarting..." << endl;
                    goto restart;
                }
            }
            RQ = false;

            periodicEnd = chrono::high_resolution_clock::now();
            periodicDuration = chrono::duration_cast<chrono::milliseconds>(periodicEnd - start);
            if (periodicDuration.count() > time_limit_reduce * 1000) {
                // cout << "时间限制到达，停止约简" << endl;
                return;
            }
        }
        
        total += count;
    } while (changed);

    auto end = chrono::high_resolution_clock::now();
    allTime = chrono::duration_cast<chrono::nanoseconds>(end - start).count() / 1000000.0;
    
    // 在约简结束后打印统计信息
    DEBUG_INFO("约简后：");
    printNetworkStatistics("  ");
    
    // 计算减少的百分比
    // cout << "\n约简效果：" << endl;
    // cout << "- 总约简次数: " << total << endl;
    // cout << "- 总约简时间: " << allTime << " ms" << endl;
}

struct ReductionUnit {
    string transId;                    // 要删除的变迁
    string inputPlaceId;              // 输入库所
    weight_t inputPlaceTokens;        // 输入库所的标识数
    unordered_map<string, weight_t> inTransToWeight;    // 输入变迁及其权重
    unordered_map<string, weight_t> outPlaceToWeight;   // 输出库所及其权重
};

// 检查是否可以应用规则 A
bool PetriStructureReducer::canApplyRuleA(const string& transId, string& prePlace) {
    // 检查变迁是否存在
    if (transitions.find(transId) == transitions.end()) return false;
    const PetriTransition& trans = transitions.at(transId);
    
    // A1: 检查是否只有一个输入库所
    if (trans.inPlaces.size() != 1) return false;
    
    // 获取唯一的输入库所
    prePlace = trans.inPlaces.begin()->first;
    
    // 检查输入库所是否存在
    if (places.find(prePlace) == places.end()) return false;
    const PetriPlace& pre = places.at(prePlace);
    
    // A5: 检查 pre 是否不是重要库所 (提前检查以避免不必要的后续检查)
    if (significantPlaces.find(prePlace) != significantPlaces.end()) return false;
    
    // A2: 检查输入库所是否只连接到这个变迁
    if (pre.outTransitions.size() != 1 || pre.outTransitions.begin()->first != transId) return false;
    
    // 获取弧 pre -> trans 的权重
    weight_t w = trans.inPlaces.at(prePlace);
    
    // A3: 检查输入弧权重条件 (所有到 pre 的生产者变迁的权重是否是 w 的倍数)
    for (const auto& inTrans : pre.inTransitions) {
        if (inTrans.second % w != 0) return false;
    }
    
    // A3 (cont.): 检查 pre 的初始标记是否可以被 w 整除
    if (pre.tokens % w != 0) return false;
    
    // A4: 检查 pre 是否不在 trans 的输出库所中 (非自循环)
    if (trans.outPlaces.find(prePlace) != trans.outPlaces.end()) return false;
    
    // A6: 检查 trans 的输出库所是否都不是重要库所
    for (const auto& outPlace : trans.outPlaces) {
        if (significantPlaces.find(outPlace.first) != significantPlaces.end()) return false;
    }
    
    return true;
}

// 应用规则 A 进行约简
int PetriStructureReducer::applyRuleA() {
    int count = 0;
    vector<string> toRemove;
    
    // 预先收集所有变迁ID
    vector<string> allTransIds;
    allTransIds.reserve(transitions.size());
    for (const auto& pair : transitions) {
        allTransIds.push_back(pair.first);
    }
    
    // 查找可约简的变迁
    for (const string& transId : allTransIds) {
        string prePlace;
        if (canApplyRuleA(transId, prePlace)) {
            // 执行约简
            // if (prePlace != "start") continue;
            const PetriTransition& trans = transitions[transId];
            PetriPlace& pre = places[prePlace];
            weight_t w = trans.inPlaces.at(prePlace);
            
            // UA1: 更新所有输出库所的初始标识
            for (const auto& outPlace : trans.outPlaces) {
                places[outPlace.first].tokens += (pre.tokens / w) * outPlace.second;
            }
            
            // UA2: 为每个输入变迁建立到输出库所的新连接
            for (const auto& inTrans : pre.inTransitions) {
                PetriTransition& inTransition = transitions[inTrans.first];
                weight_t sourceWeight = inTrans.second;
                
                // 对于每个输出库所
                for (const auto& outPlace : trans.outPlaces) {
                    weight_t newWeight = (sourceWeight / w) * outPlace.second;
                    
                    // 更新或创建连接
                    if (inTransition.outPlaces.find(outPlace.first) != inTransition.outPlaces.end()) {
                        inTransition.outPlaces[outPlace.first] += newWeight;
                    } else {
                        inTransition.outPlaces[outPlace.first] = newWeight;
                    }
                    
                    // 更新输出库所的输入变迁
                    if (places[outPlace.first].inTransitions.find(inTrans.first) != places[outPlace.first].inTransitions.end()) {
                        places[outPlace.first].inTransitions[inTrans.first] += newWeight; // 累加，不要覆盖
                    } else {
                        places[outPlace.first].inTransitions[inTrans.first] = newWeight;
                    }
                    // places[outPlace.first].inTransitions[inTrans.first] = inTransition.outPlaces[outPlace.first];
                }
                
                // 删除输入变迁到 pre 的连接
                inTransition.outPlaces.erase(prePlace);
            }
            
            // 删除所有输出库所到变迁的连接
            for (const auto& outPlace : trans.outPlaces) {
                places[outPlace.first].inTransitions.erase(transId);
            }
            
            // 删除 pre 和变迁
            erasePlace(prePlace);
            toRemove.push_back(transId);
            
            count++;
            break;
        }
    }
    
    // 删除所有标记的变迁
    for (const string& transId : toRemove) {
        eraseTransition(transId);
    }
    
    return count;
}

// 检查是否可以应用规则 B
bool PetriStructureReducer::canApplyRuleB(const string& placeId, string& inTransId, string& outTransId) {
    const PetriPlace& place = places[placeId];
    
    // B2: 检查是否只有一个消费者变迁和至少一个生产者变迁
    if (place.outTransitions.size() != 1 || place.inTransitions.empty()) {
        return false;
    }
    
    // 获取唯一的消费者变迁
    inTransId = place.outTransitions.begin()->first;
    
    // 检查消费者变迁是否是重要变迁
    if (significantTransitions.find(inTransId) != significantTransitions.end()) {
        return false;
    }
    
    // 检查每个生产者变迁
    for (const auto& inTrans : place.inTransitions) {
        outTransId = inTrans.first;
        
        // B1: 检查生产者不是消费者
        if (outTransId == inTransId) {
            continue;
        }
        
        // 检查生产者变迁是否是重要变迁
        if (significantTransitions.find(outTransId) != significantTransitions.end()) {
            continue;
        }
        
        const PetriTransition& in = transitions[inTransId];
        const PetriTransition& out = transitions[outTransId];
        
        // 检查至少一个变迁是单一的
        if (out.outPlaces.size() != 1 && in.inPlaces.size() != 1) {
            continue;
        }
        
        // 如果库所有初始标记且输入变迁不是单一的，则跳过
        if (place.tokens > 0 && in.inPlaces.size() != 1) {
            continue;
        }
        
        // B3: 检查输出权重是输入权重的倍数且非零
        weight_t inWeight = place.outTransitions.at(inTransId);
        weight_t outWeight = inTrans.second;
        
        if (outWeight < inWeight || (outWeight % inWeight) != 0) {
            continue;
        }
        
        // B5: 检查库所是否不是重要库所
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            continue;
        }
        
        // B6: 检查消费变迁的后置集中的库所是否不是重要库所
        bool postOk = true;
        for (const auto& outPlace : in.outPlaces) {
            if (significantPlaces.find(outPlace.first) != significantPlaces.end()) {
                postOk = false;
                break;
            }
        }
        if (!postOk) continue;
        
        // B7: 检查消费变迁的前置集中的库所是否不是重要库所
        bool preOk = true;
        for (const auto& inPlace : in.inPlaces) {
            if (significantPlaces.find(inPlace.first) != significantPlaces.end()) {
                preOk = false;
                break;
            }
        }
        if (!preOk) continue;
        
        // B2.a: 检查除了p之外没有其他库所给到消费变迁tIn
        const auto& arcs = in.inPlaces.size() < out.outPlaces.size() ? in.inPlaces : out.outPlaces;
        for (const auto& arc : arcs) {
            if (arc.first != placeId && arc.second > 0) {
                return false;
            }
        }
        
        return true;
    }
    
    return false;
}

// 应用规则 B 进行约简
int PetriStructureReducer::applyRuleB() {
    int count = 0;
    vector<string> placesToRemove;
    
    // 预先收集所有库所ID
    vector<string> allPlaceIds;
    allPlaceIds.reserve(places.size());
    for (const auto& pair : places) {
        allPlaceIds.push_back(pair.first);
    }
    
    // 查找可约简的库所
    for (const string& placeId : allPlaceIds) {
        if (find(placesToRemove.begin(), placesToRemove.end(), placeId) != placesToRemove.end()) {
            continue;  // 已经标记为删除
        }
        
        string inTransId, outTransId;
        if (canApplyRuleB(placeId, inTransId, outTransId)) {
            // 执行约简
            const PetriPlace& place = places[placeId];
            PetriTransition& in = transitions[inTransId];
            PetriTransition& out = transitions[outTransId];
            
            weight_t inWeight = place.outTransitions.at(inTransId);
            weight_t outWeight = place.inTransitions.at(outTransId);
            size_t multiplier = outWeight / inWeight;
            
            // UB2: 记住初始标记
            weight_t initMarking = place.tokens;
            initMarking /= inWeight;  // 整数除法默认向下取整
            
            // UB3: 将弧从消费变迁移动到生产变迁
            // 处理后置弧 - 消费变迁的输出弧
            for (const auto& arc : in.outPlaces) {
                weight_t newWeight = arc.second * multiplier;
                
                // 更新或创建连接
                if (out.outPlaces.find(arc.first) != out.outPlaces.end()) {
                    out.outPlaces[arc.first] += newWeight;
                } else {
                    out.outPlaces[arc.first] = newWeight;
                }
                
                // 更新库所的输入变迁
                places[arc.first].inTransitions[outTransId] = out.outPlaces[arc.first];
                
                // 更新初始标记
                places[arc.first].tokens += initMarking * arc.second;
            }
            
            // 处理前置弧 - 消费变迁的输入弧
            for (const auto& arc : in.inPlaces) {
                if (arc.first == placeId) continue;
                
                weight_t newWeight = arc.second * multiplier;
                
                // 更新或创建连接
                if (out.inPlaces.find(arc.first) != out.inPlaces.end()) {
                    out.inPlaces[arc.first] += newWeight;
                } else {
                    out.inPlaces[arc.first] = newWeight;
                }
                
                // 更新库所的输出变迁
                places[arc.first].outTransitions[outTransId] = out.inPlaces[arc.first];
                
                // 更新初始标记
                places[arc.first].tokens += initMarking * arc.second;
            }
            
            // 删除生产变迁到该库所的连接
            out.outPlaces.erase(placeId);
            
            // 标记要删除的库所
            placesToRemove.push_back(placeId);
            
            // 如果库所没有生产者了，则删除消费变迁
            if (place.inTransitions.size() <= 1) {
                eraseTransition(inTransId);
            }
            
            count++;
        }
    }
    
    // 删除所有标记的库所
    for (const string& placeId : placesToRemove) {
        erasePlace(placeId);
    }
    
    return count;
}

// Helper functions to check if input/output bags are equal
// A "bag" is a multiset representation using a map {Element -> Count/Weight}
bool PetriStructureReducer::areInputBagsEqual(const std::string& p1Id, const std::string& p2Id) {
    if (!places.count(p1Id) || !places.count(p2Id)) return false;
    const auto& in1 = places.at(p1Id).inTransitions;
    const auto& in2 = places.at(p2Id).inTransitions;

    // Check size first for efficiency
    if (in1.size() != in2.size()) return false;

    // Check if all entries in in1 exist in in2 with the same weight
    for (const auto& [transId, weight] : in1) {
        auto it = in2.find(transId);
        if (it == in2.end() || it->second != weight) {
            return false;
        }
    }
    // No need to check in2 -> in1 because sizes are equal
    return true;
}

bool PetriStructureReducer::areOutputBagsEqual(const std::string& p1Id, const std::string& p2Id) {
    if (!places.count(p1Id) || !places.count(p2Id)) return false;
    const auto& out1 = places.at(p1Id).outTransitions;
    const auto& out2 = places.at(p2Id).outTransitions;

    // Check size first for efficiency
    if (out1.size() != out2.size()) return false;

    // Check if all entries in out1 exist in out2 with the same weight
    for (const auto& [transId, weight] : out1) {
        auto it = out2.find(transId);
        if (it == out2.end() || it->second != weight) {
            return false;
        }
    }
    // No need to check out2 -> out1 because sizes are equal
    return true;
}


// 实现融合并行库所的规则 (替代原规则C)
int PetriStructureReducer::applyRuleFusionParallelPlaces() {
    int count = 0;
    // Keep track of places removed in this pass to skip them
    std::unordered_set<std::string> removedThisPass;

    // Get a list of place IDs to iterate over, as the map will be modified
    std::vector<std::string> placeIds;
    for(const auto& pair : places) {
        placeIds.push_back(pair.first);
    }

    // Iterate through all unique pairs of places
    for (size_t i = 0; i < placeIds.size(); ++i) {
        std::string p1Id = placeIds[i];

        // If p1 was already removed in this pass, skip it
        if (removedThisPass.count(p1Id) || places.find(p1Id) == places.end()) {
            continue;
        }

        for (size_t j = i + 1; j < placeIds.size(); ++j) {
            std::string p2Id = placeIds[j];

            // If p2 was already removed in this pass, skip it
             if (removedThisPass.count(p2Id) || places.find(p2Id) == places.end()) {
                continue;
            }

            // Ensure p1 and p2 are distinct (already guaranteed by j = i + 1, but defensive)
            if (p1Id == p2Id) continue;

            // --- Rule Conditions Check ---

            // Condition 3: Neither p1 nor p2 is significant
            if (significantPlaces.count(p1Id) || significantPlaces.count(p2Id)) {
                continue;
            }

            // Condition 1 & 2: p1 and p2 have the same input and output bags
            if (areInputBagsEqual(p1Id, p2Id) && areOutputBagsEqual(p1Id, p2Id)) {
                // --- Fusion is Applicable ---

                const PetriPlace& p1 = places.at(p1Id);
                const PetriPlace& p2 = places.at(p2Id);

                // 1. Create the new fused place
                std::string newPlaceId = "fused_p_" + p1.id + "_" + p2.id;
                PetriPlace newPlace;
                newPlace.id = newPlaceId;
                // Initial marking is the sum
                newPlace.tokens = p1.tokens + p2.tokens;
                
                // Connections of the new place are the same as p1 (or p2)
                newPlace.inTransitions = p1.inTransitions;
                newPlace.outTransitions = p1.outTransitions;

                // 2. Add the new place to the map
                places[newPlaceId] = newPlace;
                // The new place is not significant by default (fusing non-significant places)

                // 3. Update connected transitions to point to the new place
                // For each transition that was an input to p1/p2:
                for (const auto& [transId, weight] : newPlace.inTransitions) {
                    if (transitions.count(transId)) {
                         // Update transition's output connection to the new place
                         transitions.at(transId).outPlaces[newPlaceId] = weight;
                         // The old connections to p1Id and p2Id will be removed when erasing p1 and p2
                    }
                }
                 // For each transition that was an output from p1/p2:
                for (const auto& [transId, weight] : newPlace.outTransitions) {
                     if (transitions.count(transId)) {
                         // Update transition's input connection from the new place
                         transitions.at(transId).inPlaces[newPlaceId] = weight;
                         // The old connections from p1Id and p2Id will be removed when erasing p1 and p2
                     }
                 }


                // 4. Remove the old places (p1 and p2)
                // erasePlace handles removing the place from the map and its connections from transitions
                erasePlace(p1Id);
                erasePlace(p2Id);

                // Mark these places as removed in this pass
                removedThisPass.insert(p1Id);
                removedThisPass.insert(p2Id);

                count++; // One fusion operation performed

                // Since p1 and p2 are removed, we can break the inner loop (finding p2)
                // and continue the outer loop (finding the next p1 candidate)
                break;
            }
        }
    }

    return count;
}

// 应用规则 D - 移除具有相同前置集和后置集的变迁
int PetriStructureReducer::applyRuleD() {
    int count = 0;
    unordered_set<string> transToRemove;
    
    // 用于比较变迁签名的结构
    struct TransitionSignature {
        vector<pair<string, weight_t>> inPlaces;
        vector<pair<string, weight_t>> outPlaces;
        weight_t minInWeight = numeric_limits<weight_t>::max();
    };
    
    unordered_map<string, TransitionSignature> transSignatures;
    
    // 预计算所有变迁的签名
    for (const auto& transPair : transitions) {
        const string& transId = transPair.first;
        const PetriTransition& trans = transPair.second;
        
        TransitionSignature sig;
        
        // 收集并排序前置集
        for (const auto& p : trans.inPlaces) {
            sig.inPlaces.push_back(p);
            sig.minInWeight = min(sig.minInWeight, p.second);
        }
        sort(sig.inPlaces.begin(), sig.inPlaces.end());
        
        // 收集并排序后置集
        for (const auto& p : trans.outPlaces) {
            sig.outPlaces.push_back(p);
        }
        sort(sig.outPlaces.begin(), sig.outPlaces.end());
        
        transSignatures[transId] = sig;
    }
    
    // 按库所分组变迁，只比较共享同一输入库所的变迁
    unordered_map<string, vector<string>> placeToTrans;
    for (const auto& transPair : transitions) {
        const string& transId = transPair.first;
        const PetriTransition& trans = transPair.second;
        
        for (const auto& inPlace : trans.inPlaces) {
            placeToTrans[inPlace.first].push_back(transId);
        }
    }
    
    // 对每个库所的消费者变迁进行比较
    for (const auto& placeTrans : placeToTrans) {
        const vector<string>& consumers = placeTrans.second;
        
        // 跳过没有多个消费者的库所
        if (consumers.size() < 2) continue;
        
        // 比较每对消费者变迁
        for (size_t i = 0; i < consumers.size(); i++) {
            const string& t1Id = consumers[i];
            
            // 如果变迁已经被标记为删除，则跳过
            if (transToRemove.find(t1Id) != transToRemove.end()) {
                continue;
            }
            
            // 检查重要变迁，不能被删除
            if (significantTransitions.find(t1Id) != significantTransitions.end()) {
                continue;
            }
            
            const TransitionSignature& sig1 = transSignatures[t1Id];
            
            for (size_t j = i + 1; j < consumers.size(); j++) {
                const string& t2Id = consumers[j];
                
                // 如果变迁已经被标记为删除，则跳过
                if (transToRemove.find(t2Id) != transToRemove.end()) {
                    continue;
                }
                
                // 检查重要变迁，不能被删除
                if (significantTransitions.find(t2Id) != significantTransitions.end()) {
                    continue;
                }
                
                const TransitionSignature& sig2 = transSignatures[t2Id];
                
                // 快速过滤：检查前置集和后置集大小
                if (sig1.inPlaces.size() != sig2.inPlaces.size() || 
                    sig1.outPlaces.size() != sig2.outPlaces.size()) {
                    continue;
                }
                
                // 检查哪个变迁应该被保留（权重较小的）
                bool t1ShouldBeRemoved = false;
                bool t2ShouldBeRemoved = false;
                
                // 比较前置集
                if (sig1.minInWeight > sig2.minInWeight) {
                    t1ShouldBeRemoved = true;
                } else if (sig1.minInWeight < sig2.minInWeight) {
                    t2ShouldBeRemoved = true;
                } else {
                    // 最小权重相同，需要详细比较
                    
                    // 检查前置集是否匹配
                    bool preMatch = true;
                    weight_t multiplier = 0;
                    
                    // 前置集已排序，可以线性比较
                    for (size_t p = 0; p < sig1.inPlaces.size(); p++) {
                        if (sig1.inPlaces[p].first != sig2.inPlaces[p].first) {
                            preMatch = false;
                            break;
                        }
                        
                        weight_t w1 = sig1.inPlaces[p].second;
                        weight_t w2 = sig2.inPlaces[p].second;
                        
                        if (p == 0) {
                            // 确定乘数
                            if (w1 <= w2 && w2 % w1 == 0) {
                                multiplier = w2 / w1;
                                t2ShouldBeRemoved = true;
                            } else if (w2 <= w1 && w1 % w2 == 0) {
                                multiplier = w1 / w2;
                                t1ShouldBeRemoved = true;
                            } else {
                                preMatch = false;
                                break;
                            }
                        } else {
                            // 验证乘数一致性
                            if (t2ShouldBeRemoved && w2 != w1 * multiplier) {
                                preMatch = false;
                                break;
                            } else if (t1ShouldBeRemoved && w1 != w2 * multiplier) {
                                preMatch = false;
                                break;
                            }
                        }
                    }
                    
                    if (!preMatch) continue;
                    
                    // 检查后置集是否匹配
                    bool postMatch = true;
                    
                    // 后置集已排序，可以线性比较
                    for (size_t p = 0; p < sig1.outPlaces.size(); p++) {
                        if (sig1.outPlaces[p].first != sig2.outPlaces[p].first) {
                            postMatch = false;
                            break;
                        }
                        
                        weight_t w1 = sig1.outPlaces[p].second;
                        weight_t w2 = sig2.outPlaces[p].second;
                        
                        if (t2ShouldBeRemoved && w2 != w1 * multiplier) {
                            postMatch = false;
                            break;
                        } else if (t1ShouldBeRemoved && w1 != w2 * multiplier) {
                            postMatch = false;
                            break;
                        }
                    }
                    
                    if (!postMatch) continue;
                }
                
                // 确定要移除的变迁
                if (t2ShouldBeRemoved) {
                    transToRemove.insert(t2Id);
                    count++;
                } else if (t1ShouldBeRemoved) {
                    transToRemove.insert(t1Id);
                    count++;
                    break;  // t1被移除，不需要继续比较
                }
            }
        }
    }
    
    // 删除所有标记的变迁
    for (const string& transId : transToRemove) {
        // 删除变迁
        eraseTransition(transId);
    }
    
    return count;
}

// 应用规则 E 进行约简 - 移除初始禁用的变迁
int PetriStructureReducer::applyRuleE() {
    int count = 0;
    vector<string> transToRemove;
    
    // 检查每个变迁
    for (const auto& transPair : transitions) {
        const string& transId = transPair.first;
        const PetriTransition& trans = transPair.second;
        
        // 检查重要变迁，不能被删除
        if (significantTransitions.find(transId) != significantTransitions.end()) {
            continue;
        }
        
        // 检查变迁是否初始禁用
        bool initiallyDisabled = false;
        
        for (const auto& inPlace : trans.inPlaces) {
            const string& placeId = inPlace.first;
            const PetriPlace& place = places[placeId];
            
            // 如果输入库所的标记不足以启用变迁，则变迁初始禁用
            if (place.tokens < inPlace.second) {
                initiallyDisabled = true;
                break;
            }
        }
        
        // 如果变迁初始禁用，检查是否可以移除
        if (initiallyDisabled) {
            bool canRemove = true;
            
            // 检查变迁的输入库所是否有可能获得足够的标记
            for (const auto& inPlace : trans.inPlaces) {
                const string& placeId = inPlace.first;
                const PetriPlace& place = places[placeId];
                
                // 如果库所没有输入变迁，且初始标记不足，则变迁永远禁用
                if (place.inTransitions.empty() && place.tokens < inPlace.second) {
                    continue;  // 这个条件确认了变迁永远禁用
                }
                
                // 检查是否有输入变迁可以增加库所的标记
                bool canIncrease = false;
                for (const auto& inTrans : place.inTransitions) {
                    // 如果有输入变迁可以增加库所的标记，则变迁可能会被启用
                    if (inTrans.first != transId) {  // 避免自循环
                        canIncrease = true;
                        break;
                    }
                }
                
                if (!canIncrease && place.tokens < inPlace.second) {
                    continue;  // 这个条件确认了变迁永远禁用
                } else if (canIncrease) {
                    // 如果有输入变迁可以增加库所的标记，则变迁可能会被启用
                    canRemove = false;
                    break;
                }
            }
            
            if (canRemove) {
                transToRemove.push_back(transId);
                count++;
            }
        }
    }
    
    // 删除所有标记的变迁
    for (const string& transId : transToRemove) {
        eraseTransition(transId);
    }
    
    return count;
}

// 新增：完整实现规则 F 的冗余库所检查
bool PetriStructureReducer::canRemoveRedundantPlaceRuleF(const string& p0Id) {
    const PetriPlace& p0 = places.at(p0Id);
    
    // 检查是否是重要库所
    if (significantPlaces.find(p0Id) != significantPlaces.end()) {
        return false;
    }
    
    // 检查所有消费变迁
    for (const auto& [tId, weight] : p0.outTransitions) {
        // 条件1：如果弧权重大于初始标记，则不能移除
        if (weight > p0.tokens) {
            return false;
        }
        
        // 条件2：检查是否存在从变迁到该库所的回弧，且权重不小于输入弧权重
        auto outTransIt = p0.inTransitions.find(tId);
        if (outTransIt == p0.inTransitions.end() || outTransIt->second < weight) {
            return false;
        }
    }
    
    return true;
}

int PetriStructureReducer::removeRedundantPlacesRuleF() {
    int count = 0;
    vector<string> toRemove;
    
    for (const auto& [p0Id, p0] : places) {
        if (canRemoveRedundantPlaceRuleF(p0Id)) {
            toRemove.push_back(p0Id);
            // cout << "removeRedundantPlacesRuleF: " << p0Id << endl;
        }
    }
    for (const auto& p0Id : toRemove) {
        erasePlace(p0Id);
        count++;
    }
    
    return count;
}

// 新增：检查是否满足规则G的条件
bool PetriStructureReducer::canRemoveRedundantTransitionRuleG(const string& transId) {
    // 重要变迁不能被移除
    if (significantTransitions.find(transId) != significantTransitions.end()) {
        return false;
    }
    
    const PetriTransition& trans = transitions[transId];
    
    // 条件1：变迁的输入库所数量不小于输出库所数量
    if (trans.inPlaces.size() < trans.outPlaces.size()) return false;
    
    // 创建输入库所和输出库所的映射，以便于比较
    unordered_map<string, weight_t> inPlacesMap = trans.inPlaces;
    
    // 条件2：检查每个输出库所
    for (const auto& [placeId, outWeight] : trans.outPlaces) {
        // 如果输出库所也是输入库所
        auto inIt = inPlacesMap.find(placeId);
        if (inIt != inPlacesMap.end()) {
            weight_t inWeight = inIt->second;
            
            // 如果是重要库所，输入权重必须等于输出权重
            if (significantPlaces.find(placeId) != significantPlaces.end()) {
                if (inWeight != outWeight) return false;
            } 
            // 如果不是重要库所，输入权重必须大于等于输出权重
            else if (inWeight < outWeight) {
                return false;
            }
            
            // 从输入库所映射中移除已处理的库所
            inPlacesMap.erase(placeId);
        } else {
            // 输出库所不是输入库所，不满足条件
            return false;
        }
    }
    
    // 条件3：检查剩余的仅作为输入的库所，它们不能是重要库所
    for (const auto& [placeId, _] : inPlacesMap) {
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            return false;
        }
    }
    
    return true;
}

// 新增：使用规则G移除冗余变迁
int PetriStructureReducer::removeRedundantTransitionsRuleG() {
    int count = 0;
    vector<string> toRemove;
    
    for (const auto& [transId, _] : transitions) {
        if (canRemoveRedundantTransitionRuleG(transId)) {
            toRemove.push_back(transId);
        }
    }
    
    for (const string& transId : toRemove) {
        eraseTransition(transId);
        count++;
    }
    
    return count;
}

// 计算前向可达的库所和变迁
pair<unordered_set<string>, unordered_set<string>> PetriStructureReducer::computeForwardReachable() {
    unordered_set<string> reachablePlaces;
    unordered_set<string> reachableTransitions;
    
    // 从重要库所开始
    queue<string> workQueue;
    for (const string& transId : significantTransitions) {
        workQueue.push(transId);
        reachableTransitions.insert(transId);
    }
    for (const string& placeId : significantPlaces) {
        workQueue.push(placeId);
        reachablePlaces.insert(placeId);
    }
    
    // 广度优先搜索
    while (!workQueue.empty()) {
        string currentId = workQueue.front();
        workQueue.pop();
        
        // 如果是库所，找出所有后继变迁
        if (places.find(currentId) != places.end()) {
            const PetriPlace& place = places[currentId];
            for (const auto& [transId, _] : place.outTransitions) {
                if (reachableTransitions.find(transId) == reachableTransitions.end()) {
                    reachableTransitions.insert(transId);
                    workQueue.push(transId);
                }
            }
        }
        // 如果是变迁，找出所有后继库所
        else if (transitions.find(currentId) != transitions.end()) {
            const PetriTransition& trans = transitions[currentId];
            for (const auto& [placeId, _] : trans.outPlaces) {
                if (reachablePlaces.find(placeId) == reachablePlaces.end()) {
                    reachablePlaces.insert(placeId);
                    workQueue.push(placeId);
                }
            }
        }
    }
    
    return {reachableTransitions, reachablePlaces};
}

// 计算后向可达的库所和变迁
pair<unordered_set<string>, unordered_set<string>> PetriStructureReducer::computeBackwardReachable() {
    unordered_set<string> reachablePlaces;
    unordered_set<string> reachableTransitions;
    
    // 从重要库所开始
    queue<string> workQueue;
    for (const string& transId : significantTransitions) {
        workQueue.push(transId);
        reachableTransitions.insert(transId);
    }
    for (const string& placeId : significantPlaces) {
        workQueue.push(placeId);
        reachablePlaces.insert(placeId);
    }
    
    // 广度优先搜索
    while (!workQueue.empty()) {
        string currentId = workQueue.front();
        workQueue.pop();
        
        // 如果是库所，找出所有前驱变迁
        if (places.find(currentId) != places.end()) {
            const PetriPlace& place = places[currentId];
            for (const auto& [transId, _] : place.inTransitions) {
                if (reachableTransitions.find(transId) == reachableTransitions.end()) {
                    reachableTransitions.insert(transId);
                    workQueue.push(transId);
                }
            }
        }
        // 如果是变迁，找出所有前驱库所
        else if (transitions.find(currentId) != transitions.end()) {
            const PetriTransition& trans = transitions[currentId];
            for (const auto& [placeId, _] : trans.inPlaces) {
                if (reachablePlaces.find(placeId) == reachablePlaces.end()) {
                    reachablePlaces.insert(placeId);
                    workQueue.push(placeId);
                }
            }
        }
    }
    
    return {reachableTransitions, reachablePlaces};
}

// 检查库所是否可以被移除（规则I）
bool PetriStructureReducer::canRemoveIrrelevantPlace(const string& placeId) {
    // 重要库所不能移除
    if (significantPlaces.find(placeId) != significantPlaces.end()) {
        return false;
    }
    
    return true;
}

// 检查变迁是否可以被移除（规则I）
bool PetriStructureReducer::canRemoveIrrelevantTransition(const string& transId) {
    // 重要变迁不能移除
    if (significantTransitions.find(transId) != significantTransitions.end()) {
        return false;
    }
    
    return true;
}

// 实现规则I：移除与查询无关的库所和变迁
int PetriStructureReducer::removeIrrelevantElements() {
    int count = 0;
    
    // 计算前向和后向可达的库所和变迁
    auto [forwardTransitions, forwardPlaces] = computeForwardReachable();
    auto [backwardTransitions, backwardPlaces] = computeBackwardReachable();
    
    // 合并前向和后向可达集合
    unordered_set<string> relevantPlaces;
    unordered_set<string> relevantTransitions;
    
    for (const string& placeId : forwardPlaces) {
        relevantPlaces.insert(placeId);
    }
    for (const string& placeId : backwardPlaces) {
        relevantPlaces.insert(placeId);
    }
    for (const string& transId : forwardTransitions) {
        relevantTransitions.insert(transId);
    }
    for (const string& transId : backwardTransitions) {
        relevantTransitions.insert(transId);
    }
    
    // 找出不相关的库所
    vector<string> irrelevantPlaces;
    for (const auto& [placeId, _] : places) {
        if (relevantPlaces.find(placeId) == relevantPlaces.end() && 
            canRemoveIrrelevantPlace(placeId)) {
            irrelevantPlaces.push_back(placeId);
        }
    }
    
    // 找出不相关的变迁
    vector<string> irrelevantTransitions;
    for (const auto& [transId, _] : transitions) {
        if (relevantTransitions.find(transId) == relevantTransitions.end() && 
            canRemoveIrrelevantTransition(transId)) {
            irrelevantTransitions.push_back(transId);
        }
    }
    
    // 移除不相关的库所
    for (const string& placeId : irrelevantPlaces) {
        erasePlace(placeId);
        count++;
    }
    
    // 移除不相关的变迁
    for (const string& transId : irrelevantTransitions) {
        eraseTransition(transId);
        count++;
    }
    
    return count;
}
// 规则H：循环简化规则
bool PetriStructureReducer::canApplyRuleH(const string& transId) {
    // 检查重要变迁，不能被处理
    if (significantTransitions.find(transId) != significantTransitions.end()) {
        return false;
    }

    // 检查变迁是否满足规则H的条件
    const PetriTransition& trans = transitions[transId];
    
    // 变迁必须只有一个输入库所和一个输出库所
    if (trans.inPlaces.size() != 1 || trans.outPlaces.size() != 1) {
        return false;
    }
    
    // 获取输入和输出库所ID
    string inPlaceId = trans.inPlaces.begin()->first;
    string outPlaceId = trans.outPlaces.begin()->first;
    
    // 输入和输出库所必须不同
    if (inPlaceId == outPlaceId) {
        return false;
    }
    
    // 输入和输出的权重应为1（可以根据需要调整）
    if (trans.inPlaces.at(inPlaceId) != 1 || trans.outPlaces.at(outPlaceId) != 1) {
        return false;
    }
    
    return true;
}

// 查找循环
vector<string> PetriStructureReducer::findCycle(const string& startTransId) {
    unordered_map<string, int> transStatus; // 0: 未访问, 1: 在当前路径上, 2: 已完成
    vector<string> path;
    vector<string> cycle;
    
    function<bool(const string&)> dfs = [&](const string& transId) -> bool {
        // 检查是否是重要变迁
        if (significantTransitions.find(transId) != significantTransitions.end()) {
            return false; // 不处理重要变迁
        }

        // 如果变迁已经在当前路径上，找到了循环
        if (transStatus[transId] == 1) {
            // 找到循环的起点
            auto it = find(path.begin(), path.end(), transId);
            if (it != path.end()) {
                cycle.assign(it, path.end());
                cycle.push_back(transId); // 添加闭合点
                return true;
            }
            return false;
        }
        
        // 如果变迁已经被完全处理过
        if (transStatus[transId] == 2) {
            return false;
        }
        
        // 标记变迁为当前路径上的
        transStatus[transId] = 1;
        path.push_back(transId);
        
        // 检查这个变迁是否满足规则H的条件
        if (!canApplyRuleH(transId)) {
            transStatus[transId] = 2;
            path.pop_back();
            return false;
        }
        
        // 获取输出库所
        const PetriTransition& trans = transitions[transId];
        string outPlaceId = trans.outPlaces.begin()->first;
        const PetriPlace& outPlace = places[outPlaceId];
        
        // 遍历输出库所的所有消费者变迁
        for (const auto& [nextTransId, _] : outPlace.outTransitions) {
            if (dfs(nextTransId)) {
                return true;
            }
        }
        
        // 标记变迁为已完成
        transStatus[transId] = 2;
        path.pop_back();
        return false;
    };
    
    dfs(startTransId);
    return cycle;
}

// 应用规则H
bool PetriStructureReducer::applyRuleH() {
    bool reduced = false;
    
    // 创建变迁ID的副本，因为我们可能会在迭代过程中修改transitions
    vector<string> allTransIds;
    for (const auto& [transId, _] : transitions) {
        allTransIds.push_back(transId);
    }
    
    for (const string& transId : allTransIds) {
        // 如果变迁已被删除，跳过
        if (transitions.find(transId) == transitions.end()) {
            continue;
        }
        
        // 尝试找到从这个变迁开始的循环
        vector<string> cycle = findCycle(transId);
        if (cycle.size() <= 1) {
            continue; // 没有找到循环或循环太小
        }
        
        // 找到循环中的库所
        vector<string> cyclePlaces;
        for (size_t i = 0; i < cycle.size() - 1; ++i) {
            const PetriTransition& trans = transitions[cycle[i]];
            string outPlaceId = trans.outPlaces.begin()->first;
            cyclePlaces.push_back(outPlaceId);
        }
        
        // 检查是否有重要库所在循环中
        bool hasSignificantPlace = false;
        for (const string& placeId : cyclePlaces) {
            if (significantPlaces.find(placeId) != significantPlaces.end()) {
                hasSignificantPlace = true;
                break;
            }
        }
        
        if (hasSignificantPlace) {
            continue; // 不能简化包含重要库所的循环
        }
        
        // 合并循环中的库所
        for (size_t i = 1; i < cyclePlaces.size(); ++i) {
            string p1Id = cyclePlaces[0];
            string p2Id = cyclePlaces[i];
            
            PetriPlace& p1 = places[p1Id];
            PetriPlace& p2 = places[p2Id];
            
            // 将p2的所有消费者变迁重定向到p1
            for (const auto& [transId, weight] : p2.outTransitions) {
                PetriTransition& trans = transitions[transId];
                
                // 如果p1已经是这个变迁的输入，更新权重
                if (trans.inPlaces.find(p1Id) != trans.inPlaces.end()) {
                    trans.inPlaces[p1Id] += weight;
                } else {
                    trans.inPlaces[p1Id] = weight;
                }
                
                // 更新p1的输出变迁
                p1.outTransitions[transId] = trans.inPlaces[p1Id];
            }
            
            // 将p2的所有生产者变迁重定向到p1
            for (const auto& [transId, weight] : p2.inTransitions) {
                PetriTransition& trans = transitions[transId];
                
                // 如果p1已经是这个变迁的输出，更新权重
                if (trans.outPlaces.find(p1Id) != trans.outPlaces.end()) {
                    trans.outPlaces[p1Id] += weight;
                } else {
                    trans.outPlaces[p1Id] = weight;
                }
                
                // 更新p1的输入变迁
                p1.inTransitions[transId] = trans.outPlaces[p1Id];
            }
            
            // 将p2的初始标记加到p1上
            p1.tokens += p2.tokens;
            
            // 删除p2
            erasePlace(p2Id);
            
            reduced = true;
        }
        
        // 删除循环中的一个变迁（可选）
        if (cycle.size() > 2) {
            string transToRemove = cycle[cycle.size() - 2];
            const PetriTransition& trans = transitions[transToRemove];
            
            // 从相关库所中移除连接
            eraseTransition(transToRemove);
            reduced = true;
        }
        
        if (reduced) {
            break; // 一次只应用一个简化
        }
    }
    
    return reduced;
}

// 新增：规则J - 约简库所弧权重
weight_t PetriStructureReducer::canReducePlaceWeightsByGCD(const string& placeId) {
    const PetriPlace& place = places[placeId];
    
    // 检查是否是重要库所
    if (significantPlaces.find(placeId) != significantPlaces.end()) {
        return false;
    }
    
    // 如果没有输入或输出变迁，则不适用
    if (place.inTransitions.empty() || place.outTransitions.empty()) {
        return false;
    }
    
    // 计算所有输入弧权重的最大公约数
    weight_t gcdIn = 0;
    for (const auto& [_, weight] : place.inTransitions) {
        if (gcdIn == 0) {
            gcdIn = weight;
        } else {
            gcdIn = std::gcd(gcdIn, weight);
        }
        if (gcdIn == 1) break;  // 如果GCD已经是1，无需继续计算
    }
    
    // 如果GCD为1，则无法约简
    if (gcdIn == 1) return false;
    
    // 计算所有输出弧权重的最大公约数
    weight_t gcdOut = 0;
    for (const auto& [_, weight] : place.outTransitions) {
        if (gcdOut == 0) {
            gcdOut = weight;
        } else {
            gcdOut = std::gcd(gcdOut, weight);
        }
        if (gcdOut == 1) break;  // 如果GCD已经是1，无需继续计算
    }
    
    // 如果GCD为1，则无法约简
    if (gcdOut == 1) return false;
    
    // 计算输入和输出弧权重的公共GCD
    weight_t commonGcd = std::gcd(gcdIn, gcdOut);
    
    // 如果初始标记不能被GCD整除，则不能约简
    if (place.tokens % commonGcd != 0) return false;
    
    // 如果GCD大于1，则可以约简
    return commonGcd;
}

int PetriStructureReducer::reducePlaceWeightsByGCD() {
    int count = 0;
    
    for (auto& [placeId, place] : places) {
        auto commonGcd = canReducePlaceWeightsByGCD(placeId);
        if (commonGcd <= 1) continue;
        
        if (place.tokens % commonGcd) continue;
        // 约简输入弧权重
        for (auto& [transId, weight] : place.inTransitions) {
            weight_t newWeight = weight / commonGcd;
            weight = newWeight;
            transitions[transId].outPlaces[placeId] = newWeight;
        }
        
        // 约简输出弧权重
        for (auto& [transId, weight] : place.outTransitions) {
            weight_t newWeight = weight / commonGcd;
            weight = newWeight;
            transitions[transId].inPlaces[placeId] = newWeight;
        }
        
        // 约简初始标记
        place.tokens /= commonGcd;
        
        count++;
    }
    
    return count;
}


// 新增：检查是否可以应用规则K（自循环处理）
bool PetriStructureReducer::canApplyRuleK(const string& transId) {
    const PetriTransition& trans = transitions[transId];
    
    // 检查是否是自循环（只有一个输入库所和一个输出库所，且是同一个库所）
    if (trans.inPlaces.size() != 1 || trans.outPlaces.size() != 1) {
        return false;
    }
    
    // 获取输入和输出库所ID
    const string& inPlaceId = trans.inPlaces.begin()->first;
    const string& outPlaceId = trans.outPlaces.begin()->first;
    
    // 检查是否是同一个库所（自循环）
    if (inPlaceId != outPlaceId) {
        return false;
    }
    
    // 获取库所
    const PetriPlace& place = places[inPlaceId];
    
    // 检查库所是否是重要库所
    if (significantPlaces.find(inPlaceId) != significantPlaces.end()) {
        return false;
    }
    
    // 检查库所的初始标记是否足够触发自循环
    weight_t inWeight = trans.inPlaces.at(inPlaceId);
    if (place.tokens >= inWeight) {
        // 如果初始标记足够，则该自循环是相关的，不应该被移除
        return false;
    }
    
    // 如果自循环的权重为1，则该库所的其他消费变迁对活性是不相关的
    if (inWeight == 1) {
        // 检查是否有其他消费变迁
        return place.outTransitions.size() > 1;
    }
    
    return false;
}

// 新增：实现规则K，移除与自循环相关的不相关变迁
int PetriStructureReducer::removeIrrelevantByRuleK() {
    int count = 0;
    unordered_map<string, vector<string>> placeToSelfLoops;
    unordered_map<string, vector<string>> placeToConsumers;
    
    // 第一步：找出所有自循环和消费变迁
    for (const auto& [transId, trans] : transitions) {
        // 检查是否是自循环
        if (trans.inPlaces.size() == 1 && trans.outPlaces.size() == 1) {
            const string& inPlaceId = trans.inPlaces.begin()->first;
            const string& outPlaceId = trans.outPlaces.begin()->first;
            
            if (inPlaceId == outPlaceId) {
                // 是自循环
                placeToSelfLoops[inPlaceId].push_back(transId);
            }
        }
        
        // 记录所有消费变迁
        for (const auto& [placeId, _] : trans.inPlaces) {
            placeToConsumers[placeId].push_back(transId);
        }
    }
    
    // 第二步：处理每个有自循环的库所
    vector<string> toRemove;
    
    for (const auto& [placeId, selfLoops] : placeToSelfLoops) {
        const PetriPlace& place = places[placeId];
        
        // 跳过重要库所
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            continue;
        }
        
        // 检查是否有权重为1的自循环
        bool hasWeightOneSelfLoop = false;
        for (const string& loopId : selfLoops) {
            if (transitions[loopId].inPlaces.at(placeId) == 1) {
                hasWeightOneSelfLoop = true;
                break;
            }
        }
        
        // 如果有权重为1的自循环，且初始标记不足以触发，则其他消费变迁是不相关的
        if (hasWeightOneSelfLoop) {
            bool initiallyEnabled = false;
            for (const string& loopId : selfLoops) {
                if (place.tokens >= transitions[loopId].inPlaces.at(placeId)) {
                    initiallyEnabled = true;
                    break;
                }
            }
            
            if (!initiallyEnabled) {
                // 移除该库所的其他消费变迁（非自循环）
                for (const string& consumerId : placeToConsumers[placeId]) {
                    bool isSelfLoop = false;
                    for (const string& loopId : selfLoops) {
                        if (consumerId == loopId) {
                            isSelfLoop = true;
                            break;
                        }
                    }
                    
                    if (!isSelfLoop) {
                        toRemove.push_back(consumerId);
                    }
                }
            }
        }
    }
    
    // 移除不相关的变迁
    for (const string& transId : toRemove) {
        eraseTransition(transId);
        count++;
    }
    
    return count;
}


// 新增：规则 L - 移除冗余变迁（当一个变迁与另一个变迁具有相同的效果但有更多前置条件时）
bool PetriStructureReducer::canRemoveRedundantTransitionRuleL(const string& t1Id, const string& t2Id) {
    // 重要变迁不能被移除
    
    if (significantTransitions.find(t1Id) != significantTransitions.end() ||
        significantTransitions.find(t2Id) != significantTransitions.end()) {
        return false;
    }

    const PetriTransition& t1 = transitions[t1Id];
    const PetriTransition& t2 = transitions[t2Id];
    
    // 新增检查：t1 是否连接到重要库所
    for (const auto& [placeId, _] : t1.inPlaces) {
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            // cout << "  t1 连接到重要输入库所 " << placeId << "，不能移除" << endl;
            return false; // t1 的输入库所是重要库所，不能移除
        }
    }
    for (const auto& [placeId, _] : t1.outPlaces) {
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            // cout << "  t1 连接到重要输出库所 " << placeId << "，不能移除" << endl;
            return false; // t1 的输出库所是重要库所，不能移除
        }
    }

    // 新增检查：t2 是否连接到重要库所 (如果 t2 被认为"覆盖"了 t1 的行为，
    // 且 t1 被移除，那么 t2 必须是安全的替代品，其连接的重要库所也需要保护)
     for (const auto& [placeId, _] : t2.inPlaces) {
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            // cout << "  t2 连接到重要输入库所 " << placeId << "，不能移除与t2相关的t1" << endl;
            return false; // t2 的输入库所是重要库所，不能移除 t1 (基于 t2)
        }
    }
    for (const auto& [placeId, _] : t2.outPlaces) {
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            // cout << "  t2 连接到重要输出库所 " << placeId << "，不能移除与t2相关的t1" << endl;
            return false; // t2 的输出库所是重要库所，不能移除 t1 (基于 t2)
        }
    }

    // 条件1：t1的前置条件集合大小必须大于等于t2的前置条件集合大小
    if (t1.inPlaces.size() < t2.inPlaces.size()) return false;
    
    // 条件2：t1的后置条件集合大小必须大于等于t2的后置条件集合大小
    // if (t1.outPlaces.size() < t2.outPlaces.size()) return false;
    
    // 检查t2的所有前置条件是否都在t1中，且权重要求满足
    for (const auto& [placeId, weight] : t2.inPlaces) {
        auto it = t1.inPlaces.find(placeId);
        if (it == t1.inPlaces.end() || it->second < weight) {
            return false;
        }
    }
    
    // 检查t2的所有后置条件是否都在t1中
    for (const auto& [placeId, weight] : t2.outPlaces) {
        auto it = t1.outPlaces.find(placeId);
        if (it == t1.outPlaces.end()) {
            return false;
        }
    }
    
    // 检查每个库所的净效果是否相同
    // 创建一个映射来存储每个库所的净效果
    unordered_map<string, int> t1Effect;
    unordered_map<string, int> t2Effect;
    
    // 计算t1的净效果
    for (const auto& [placeId, weight] : t1.inPlaces) {
        t1Effect[placeId] -= weight;
    }
    for (const auto& [placeId, weight] : t1.outPlaces) {
        t1Effect[placeId] += weight;
    }
    
    // 计算t2的净效果
    for (const auto& [placeId, weight] : t2.inPlaces) {
        t2Effect[placeId] -= weight;
    }
    for (const auto& [placeId, weight] : t2.outPlaces) {
        t2Effect[placeId] += weight;
    }
    
    // 比较所有库所的净效果
    for (const auto& [placeId, effect] : t1Effect) {
        auto it = t2Effect.find(placeId);
        if (it == t2Effect.end()) {
            // 如果t2没有这个库所的效果，那么t1的效果必须为0
            if (effect != 0) return false;
        } else if (effect != it->second) {
            // 如果t2有这个库所的效果，那么效果必须相同
            return false;
        }
    }
    
    // 检查t2中有但t1中没有的库所
    for (const auto& [placeId, effect] : t2Effect) {
        if (t1Effect.find(placeId) == t1Effect.end() && effect != 0) {
            return false;
        }
    }
    
    return true;
}

int PetriStructureReducer::removeRedundantTransitionsRuleL() {
    int count = 0;
    vector<string> toRemove;
    
    // 为每个库所创建一个消费者变迁列表，以优化查找
    unordered_map<string, vector<string>> placeConsumers;
    for (const auto& [transId, trans] : transitions) {
        for (const auto& [placeId, _] : trans.inPlaces) {
            placeConsumers[placeId].push_back(transId);
        }
    }
    
    // 遍历所有变迁
    for (const auto& [t1Id, t1] : transitions) {
        // 如果t1没有输入库所，跳过
        if (t1.inPlaces.empty()) continue;
        
        // 获取t1的一个输入库所的所有消费者变迁
        const string& someInputPlace = t1.inPlaces.begin()->first;
        const vector<string>& potentialT2s = placeConsumers[someInputPlace];
        
        // 检查每个潜在的t2
        for (const string& t2Id : potentialT2s) {
            if (t1Id == t2Id) continue; // 跳过自身
            
            if (canRemoveRedundantTransitionRuleL(t1Id, t2Id)) {
                toRemove.push_back(t1Id);
                break; // 一旦找到可以移除t1的理由，就不需要继续检查
            }
        }
    }
    
    // 移除冗余变迁
    for (const string& transId : toRemove) {
        eraseTransition(transId);
        count++;
    }
    
    return count;
}

// 新增：实现规则 M，移除不可达的库所和变迁
int PetriStructureReducer::removeUnreachableElements() {
    int count = 0;
    
    // 用于标记库所是否可以增加或减少标记
    unordered_map<string, bool> canIncrease;
    unordered_map<string, bool> canDecrease;
    
    // 用于标记变迁是否可能被激活
    unordered_map<string, bool> canFire;
    
    // 初始化所有库所的状态
    for(const auto& [placeId, _] : places) {
        canIncrease[placeId] = false;
        canDecrease[placeId] = false;
    }
    
    // 初始化所有变迁的状态
    for(const auto& [transId, _] : transitions) {
        canFire[transId] = false;
    }
    
    // 处理初始可激活的变迁
    for(const auto& [transId, trans] : transitions) {
        bool enabled = true;
        for(const auto& [placeId, weight] : trans.inPlaces) {
            if(places[placeId].tokens < weight) {
                enabled = false;
                break;
            }
        }
        
        if(enabled) {
            canFire[transId] = true;
            
            // 处理变迁的效果
            for(const auto& [placeId, weight] : trans.outPlaces) {
                canIncrease[placeId] = true;
            }
            
            for(const auto& [placeId, weight] : trans.inPlaces) {
                canDecrease[placeId] = true;
            }
        }
    }
    
    // 迭代直到达到不动点
    bool changed;
    do {
        changed = false;
        
        // 检查每个变迁
        for(const auto& [transId, trans] : transitions) {
            if(canFire[transId]) continue; // 已经标记为可激活
            
            bool canBeEnabled = true;
            for(const auto& [placeId, weight] : trans.inPlaces) {
                // 如果库所当前标记不足且不能增加标记，则变迁不能激活
                if(places[placeId].tokens < weight && !canIncrease[placeId]) {
                    canBeEnabled = false;
                    break;
                }
            }
            
            if(canBeEnabled) {
                canFire[transId] = true;
                changed = true;
                
                // 处理变迁的效果
                for(const auto& [placeId, weight] : trans.outPlaces) {
                    if(!canIncrease[placeId]) {
                        canIncrease[placeId] = true;
                        changed = true;
                    }
                }
                
                for(const auto& [placeId, weight] : trans.inPlaces) {
                    if(!canDecrease[placeId]) {
                        canDecrease[placeId] = true;
                        changed = true;
                    }
                }
            }
        }
    } while(changed);
    
    // 移除不可达的库所（既不能增加也不能减少标记的库所）
    vector<string> placesToRemove;
    for(const auto& [placeId, place] : places) {
        // 如果库所是重要库所，则不移除
        if(significantPlaces.find(placeId) != significantPlaces.end()) {
            continue;
        }
        
        // 如果库所既不能增加也不能减少标记，则移除
        if(!canIncrease[placeId] && !canDecrease[placeId]) {
            placesToRemove.push_back(placeId);
        }
    }
    
    // 移除不可激活的变迁
    vector<string> transToRemove;
    for(const auto& [transId, trans] : transitions) {
        if(!canFire[transId]) {
            transToRemove.push_back(transId);
        }
    }
    
    // 执行移除操作
    for(const string& placeId : placesToRemove) {
        erasePlace(placeId);
        count++;
    }
    
    for(const string& transId : transToRemove) {
        eraseTransition(transId);
        count++;
    }
    
    return count;
}


// 修改：实现规则N - 移除永远不会禁用变迁的弧好的，要提供一个"正确"版本的规则 N 是一个挑战，因为其核心的静态分析（计算可靠的库所标记下界）本身就是一个复杂的问题，原代码中的实现是不健全的（unsound）。一个完全健全的下界计算通常需要更高级的技术（如 P-invariant 分析或声音的抽象解释），这超出了直接修改代码片段的范围。

// 修改：实现规则N - 移除永远不会禁用变迁的弧
int PetriStructureReducer::removeNonDisablingArcs() {
    int count = 0;

    // ====================================================================
    // *** 警告：以下静态分析部分存在根本性问题，其计算出的 lowerBounds
    // *** 和 canIncrease/canDecrease 标志是不健全的（不准确的过高估计），
    // *** 可能导致后续的约简是不健全的（错误移除可以禁用变迁的弧）。
    // *** 一个健全的下界计算需要更高级的可达性或结构分析技术。
    // ====================================================================

    // 用于标记库所是否可以增加或减少标记
    std::unordered_map<std::string, bool> canIncrease;
    std::unordered_map<std::string, bool> canDecrease;
    std::unordered_map<std::string, weight_t> lowerBounds;

    // 初始化所有库所的状态
    for(const auto& [placeId, place] : places) {
        canIncrease[placeId] = false;
        canDecrease[placeId] = false;
        lowerBounds[placeId] = place.tokens; // Initial marking is a lower bound
    }

    // 处理初始可激活的变迁 (第一步传播)
    for(const auto& [transId, trans] : transitions) {
        bool enabled = true;
        for(const auto& [placeId, weight] : trans.inPlaces) {
            if(places.at(placeId).tokens < weight) { // Use .at() for safety if placeId is guaranteed to exist
                enabled = false;
                break;
            }
        }

        if(enabled) {
            // 处理变迁的效果，更新 canIncrease/canDecrease 并基于初始标记更新 lowerBounds
            for(const auto& [placeId, weight] : trans.outPlaces) {
                canIncrease[placeId] = true;
            }

            for(const auto& [placeId, weight] : trans.inPlaces) {
                canDecrease[placeId] = true;

                // 计算净效果对下界的影响 (基于初始标记)
                weight_t outWeight = 0;
                auto outIt = trans.outPlaces.find(placeId);
                if(outIt != trans.outPlaces.end()) {
                    outWeight = outIt->second;
                }

                if(outWeight < weight) { // Net consumption
                    // Potential new lower bound after one firing from initial marking
                    // Still uses initial tokens, flawed for subsequent steps in loop below
                    weight_t netConsumption = weight - outWeight;
                    weight_t newLower = std::max(0u, places.at(placeId).tokens - netConsumption); // Use .at()
                    lowerBounds[placeId] = std::min(lowerBounds[placeId], newLower);
                }
            }
        }
    }

    // 迭代直到达到不动点
    bool changed;
    do {
        changed = false;

        // 检查每个变迁是否可能在某个可达状态下被激活
        // *** 警告：以下 canBeEnabled 判断逻辑不健全！***
        // *** 它过高估计了变迁的可使能性。应替换为健全的静态分析。***
        for(const auto& [transId, trans] : transitions) {
            bool canBeEnabled = true;
            for(const auto& [placeId, weight] : trans.inPlaces) {
                // Original flawed logic: Is initial tokens >= weight OR can the place increase?
                // Correct check requires checking if a state exists where ALL inputs satisfy weight condition.
                if(places.at(placeId).tokens < weight && !canIncrease.at(placeId)) { // Use .at()
                    canBeEnabled = false;
                    break;
                }
            }

            if(canBeEnabled) { // 如果这个变迁"可能"被激活 (基于不健全的判断)
                // 传播库所的可增加/可减少状态
                for(const auto& [placeId, weight] : trans.outPlaces) {
                    if(!canIncrease.at(placeId)) { // Use .at()
                        canIncrease[placeId] = true;
                        changed = true;
                    }
                }

                for(const auto& [placeId, weight] : trans.inPlaces) {
                    if(!canDecrease.at(placeId)) { // Use .at()
                        canDecrease[placeId] = true;
                        changed = true;
                    }

                    // 更新下界 (*** 警告：这里的下界更新逻辑可能也不健全 ***)
                    // 它基于一个不健全的 canBeEnabled 判断，并且仍然引用初始标记进行计算。
                    // 健全的下界传播需要考虑抽象状态的最小值传播。
                    weight_t outWeight = 0;
                    auto outIt = trans.outPlaces.find(placeId);
                    if(outIt != trans.outPlaces.end()) {
                        outWeight = outIt->second;
                    }

                    if(outWeight < weight) { // Net consumption
                         weight_t netConsumption = weight - outWeight;
                        // Flawed update: still using initial tokens.
                        // weight_t newLower = std::max(0, places.at(placeId).tokens - netConsumption);
                        // A sound update would be more complex, e.g., lowerBounds[placeId] = std::max(0, lowerBounds[placeId] - netConsumption)
                        // but this is only valid if trans is *guaranteed* fireable from a state reaching lowerBounds[placeId]
                        // Keeping the original update logic for demonstration of code structure, but it's flawed.
                        weight_t newLower = std::max(0u, places.at(placeId).tokens - netConsumption); // Use .at()
                        if(newLower < lowerBounds.at(placeId)) { // Use .at()
                            lowerBounds[placeId] = newLower;
                            changed = true;
                        }
                    }
                }
            }
        }
    } while(changed);
    // ====================================================================
    // *** 静态分析部分结束 ***
    // ====================================================================


    // ====================================================================
    // 应用规则N部分：移除基于 (可能不健全的) 下界的非禁用弧
    // ====================================================================

    // 不能在遍历时修改集合，先收集要修改/移除的信息
    struct ArcModification {
        std::string transId;
        std::string placeId;
        bool removeInputArc;
        bool removeOutputArc; // For self-loops where net effect is zero or negative
        weight_t outputWeightReduction; // For self-loops with net production
    };
    std::vector<ArcModification> modifications;


    for(const auto& [transId, trans] : transitions) {
        for(const auto& [placeId, inWeight] : trans.inPlaces) {
            // 规则判断：如果库所的 (可能不健全的) 下界大于等于输入弧权重，则该弧被视为"非禁用弧"
            if(lowerBounds.at(placeId) >= inWeight) { // Use .at()

                // *** 警告：检查重要库所！不能修改连接到重要库所的弧！***
                if (significantPlaces.find(placeId) != significantPlaces.end()) {
                    // cout << "Skipping arc modification for significant place: " << placeId << " on transition " << transId << endl;
                    continue; // 跳过重要库所
                }

                // 这个输入弧 (trans -> placeId, inWeight) 是"非禁用弧"

                // 查找对应的输出弧 (placeId -> transId) (自循环情况)
                auto outIt = trans.outPlaces.find(placeId);

                if(outIt != trans.outPlaces.end()) { // 存在从变迁到同一库所的输出弧 (自循环)
                    weight_t outWeight = outIt->second;

                    // 根据原代码逻辑，对自循环进行特殊处理
                    if(outWeight > inWeight) { // 净生产
                        // 原代码逻辑：移除输入弧，并减少输出弧权重
                         modifications.push_back({transId, placeId, true, false, inWeight});
                         // count++; // Increment count during modification application
                    } else if(outWeight == inWeight) { // 净零变化
                        // 原代码逻辑：移除输入弧和输出弧
                         modifications.push_back({transId, placeId, true, true, 0});
                         // count++; // Increment count during modification application
                    } else { // outWeight < inWeight (净消耗或零) - 原代码这里没有显式修改输出弧
                        // 移除输入弧，输出弧保持不变 (根据原代码分支行为推断)
                         modifications.push_back({transId, placeId, true, false, 0}); // Output weight reduction is 0
                         // count++; // Increment count during modification application
                    }
                } else { // 不存在从变迁到同一库所的输出弧 (不是自循环，或只有输入弧的自循环表示)
                    // 原代码逻辑：只有输入弧 (或自循环输入弧部分)，移除输入弧
                     modifications.push_back({transId, placeId, true, false, 0});
                     // count++; // Increment count during modification application
                }
            }
        }
    } // End collecting modifications

    // 应用收集到的修改
    for(const auto& mod : modifications) {
         // Check again if the transition still exists (might have been removed by another rule in an iterative process)
         if (transitions.find(mod.transId) == transitions.end()) continue;

         PetriTransition& trans = transitions.at(mod.transId); // Use .at()
         // Check if the input arc still exists before trying to remove/process
         if (trans.inPlaces.find(mod.placeId) == trans.inPlaces.end()) continue;

         // *** 移除输入弧 (主规则 N 的作用) ***
         trans.inPlaces.erase(mod.placeId);
         if (places.find(mod.placeId) != places.end()) { // Ensure place still exists
              places.at(mod.placeId).outTransitions.erase(mod.transId); // Use .at()
         }
         count++; // Increment count for the input arc removal

         // *** 应用自循环相关的修改 (根据原代码逻辑) ***
         if (trans.outPlaces.find(mod.placeId) != trans.outPlaces.end()) { // 检查输出弧是否存在（可能是自循环）
             if (mod.removeOutputArc) { // 需要移除输出弧 (净零或净负消耗)
                 trans.outPlaces.erase(mod.placeId);
                 if (places.find(mod.placeId) != places.end()) { // Ensure place still exists
                     places.at(mod.placeId).inTransitions.erase(mod.transId); // Use .at()
                 }
             } else if (mod.outputWeightReduction > 0) { // 需要减少输出弧权重 (净生产)
                 trans.outPlaces[mod.placeId] -= mod.outputWeightReduction;
                 if (places.find(mod.placeId) != places.end()) { // Ensure place still exists
                      places.at(mod.placeId).inTransitions[mod.transId] -= mod.outputWeightReduction; // Use .at()
                 }
             }
             // else: output arc exists but is <= input weight, input removed, output untouched (as per original logic)
         }
         // else: no output arc, only input arc removed.
    }


    return count;
}

// 新增：规则Q - 预先执行初始可激活的变迁
bool PetriStructureReducer::canApplyRuleQ(const string& transId) {
    // 检查是否是重要变迁
    if (significantTransitions.find(transId) != significantTransitions.end()) {
        return false;
    }

    const PetriTransition& trans = transitions[transId];
    
    // 如果变迁没有输入库所，不适用此规则
    if (trans.inPlaces.empty()) return false;
    
    // 检查前置集和后置集是否有交集
    for (const auto& [inPlaceId, _] : trans.inPlaces) {
        if (trans.outPlaces.find(inPlaceId) != trans.outPlaces.end()) {
            return false; // 前置集和后置集有交集，可能导致无限执行
        }
    }
    
    // 检查变迁是否初始可激活，以及前置库所是否只有这一个消费者
    weight_t k = 0; // 可以执行的次数
    for (const auto& [placeId, weight] : trans.inPlaces) {
        const PetriPlace& place = places[placeId];
        
        // 检查库所是否是重要库所
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            return false;
        }
        
        // 检查库所是否只有这一个消费者变迁
        if (place.outTransitions.size() != 1) {
            return false;
        }
        
        // 计算可以执行的次数
        weight_t n = place.tokens / weight;
        if (n == 0) {
            return false; // 不能执行
        }
        
        if (k == 0) {
            k = n;
        } else {
            k = min(k, n);
        }
    }
    
    // 检查后置库所是否有重要库所
    for (const auto& [placeId, _] : trans.outPlaces) {
        if (significantPlaces.find(placeId) != significantPlaces.end()) {
            return false;
        }
    }
    
    return k > 0;
}

int PetriStructureReducer::applyRuleQ() {
    int count = 0;
    bool continueReductions = true;
    
    while (continueReductions) {
        continueReductions = false;
        
        // 创建变迁ID的副本，因为我们可能会在迭代过程中修改transitions
        vector<string> allTransIds;
        for (const auto& [transId, _] : transitions) {
            allTransIds.push_back(transId);
        }
        
        for (const string& transId : allTransIds) {
            // 如果变迁已被删除，跳过
            if (transitions.find(transId) == transitions.end()) {
                continue;
            }
            
            if (!canApplyRuleQ(transId)) {
                continue;
            }
            
            const PetriTransition& trans = transitions[transId];
            
            // 计算可以执行的次数
            weight_t k = numeric_limits<weight_t>::max();
            for (const auto& [placeId, weight] : trans.inPlaces) {
                weight_t n = places[placeId].tokens / weight;
                k = min(k, n);
            }
            
            // 更新初始标记
            for (const auto& [placeId, weight] : trans.inPlaces) {
                places[placeId].tokens -= weight * k;
            }
            
            for (const auto& [placeId, weight] : trans.outPlaces) {
                places[placeId].tokens += weight * k;
            }
            
            count++;
            continueReductions = true;
        }
    }
    
    return count;
}

int PetriStructureReducer::applyRuleR() {
    int count = 0;
    std::vector<std::string> placesToProcess;
    
    // 遍历所有库所，筛选可约简的
    for (const auto& [placeId, _] : places) {
        if (canApplyRuleR(placeId)) {
            placesToProcess.push_back(placeId);
        }
    }
    
    // 限制单次处理的库所数量，防止内存爆炸
    const size_t MAX_PLACES_TO_PROCESS = 100;
    if (placesToProcess.size() > MAX_PLACES_TO_PROCESS) {
        std::sort(placesToProcess.begin(), placesToProcess.end(), [this](const std::string& a, const std::string& b) {
            // 优先处理爆炸系数较小的库所
            const PetriPlace& placeA = places[a];
            const PetriPlace& placeB = places[b];
            return (placeA.inTransitions.size() * placeA.outTransitions.size()) < 
                   (placeB.inTransitions.size() * placeB.outTransitions.size());
        });
        placesToProcess.resize(MAX_PLACES_TO_PROCESS);
    }

    // 预估内存使用量指标
    size_t totalNewTransitions = 0;
    size_t currentTransCount = transitions.size();
    size_t maxNewTransitions = std::max(size_t(10000), currentTransCount * 2); // 限制新变迁总数

    // 处理满足条件的库所
    for (const std::string& placeId : placesToProcess) {
        // 估算当前库所将产生的新变迁数
        const PetriPlace& place = places[placeId];
        size_t estimatedNewTrans = place.inTransitions.size() * place.outTransitions.size();
        
        // 如果添加这个库所的变迁会超过阈值，跳过
        if (totalNewTransitions + estimatedNewTrans > maxNewTransitions) {
            continue;
        }

        // 进行约简并更新计数
        int added = applyRuleRToPlace(placeId);
        count += added;
        totalNewTransitions += estimatedNewTrans;
        
        // 动态调整 explosion_limiter，避免过度增长
        explosion_limiter = std::max(explosion_limiter, transitions.size() / 2);
        
        // 如果变迁数量已经很大，及时中止
        if (transitions.size() > maxNewTransitions) {
            break;
        }
    }

    return count;
}

bool PetriStructureReducer::canApplyRuleR(const std::string& placeId) {
    auto placeIt = places.find(placeId);
    if (placeIt == places.end() || significantPlaces.count(placeId)) {
        return false;
    }

    const PetriPlace& place = placeIt->second;

    // 检查是否有生产者和消费者
    if (place.inTransitions.empty() || place.outTransitions.empty()) {
        return false;
    }

    // 更严格的限制：如果生产者或消费者数量过多，直接跳过
    if (place.inTransitions.size() > 5 || place.outTransitions.size() > 5) {
        return false;
    }

    // 检查生产者和消费者是否包含重要变迁
    for (const auto& [prodId, _] : place.inTransitions) {
        if (significantTransitions.find(prodId) != significantTransitions.end()) {
            return false;
        }
    }
    
    for (const auto& [consId, _] : place.outTransitions) {
        if (significantTransitions.find(consId) != significantTransitions.end()) {
            return false;
        }
    }

    // 检查生产者和消费者不相交（使用 unordered_set 优化）
    std::unordered_set<std::string> producers;
    producers.reserve(place.inTransitions.size()); // 预分配提升效率
    for (const auto& [prodId, _] : place.inTransitions) {
        producers.insert(prodId);
    }
    for (const auto& [consId, _] : place.outTransitions) {
        if (producers.count(consId)) {
            return false;
        }
    }

    // 检查所有消费者只从该库所消费
    for (const auto& [consId, _] : place.outTransitions) {
        auto consIt = transitions.find(consId);
        if (consIt == transitions.end() || consIt->second.inPlaces.size() != 1) {
            return false;
        }
    }

    // 更保守的爆炸限制: 新变迁数不超过当前变迁数的10%
    size_t newTransCount = place.inTransitions.size() * place.outTransitions.size();
    size_t currentSize = transitions.size();
    if (newTransCount > explosion_limiter || newTransCount > currentSize / 10) {
        return false;
    }

    return true;
}

int PetriStructureReducer::applyRuleRToPlace(const std::string& placeId) {
    PetriPlace& place = places[placeId];
    int count = 0;

    // 找出消费者的最大权重
    weight_t maxConsWeight = 0;
    for (const auto& [_, weight] : place.outTransitions) {
        maxConsWeight = std::max(maxConsWeight, weight);
    }

    // 收集可处理的生产者
    std::vector<std::string> producersToProcess;
    producersToProcess.reserve(place.inTransitions.size());
    for (const auto& [prodId, weight] : place.inTransitions) {
        if (weight >= maxConsWeight) {
            producersToProcess.push_back(prodId);
        }
    }

    // 处理每个生产者
    bool removedAllProducers = !producersToProcess.empty();
    for (const std::string& prodId : producersToProcess) {
        auto prodIt = transitions.find(prodId);
        if (prodIt == transitions.end()) {
            removedAllProducers = false;
            continue;
        }

        const PetriTransition& prod = prodIt->second;

        // 为每个消费者创建新变迁
        for (const auto& [consId, consWeight] : place.outTransitions) {
            auto consIt = transitions.find(consId);
            if (consIt == transitions.end()) {
                continue;
            }

            const PetriTransition& cons = consIt->second;

            // 创建新变迁
            std::string newTransId = prodId + "_" + consId;
            PetriTransition newTrans;
            newTrans.id = newTransId;

            // 添加生产者的输入弧
            for (const auto& [inPlaceId, inWeight] : prod.inPlaces) {
                if (places.count(inPlaceId)) {
                    newTrans.inPlaces[inPlaceId] = inWeight;
                    places[inPlaceId].outTransitions[newTransId] = inWeight;
                }
            }

            // 添加消费者的输出弧
            for (const auto& [outPlaceId, outWeight] : cons.outPlaces) {
                if (places.count(outPlaceId)) {
                    newTrans.outPlaces[outPlaceId] = outWeight;
                    places[outPlaceId].inTransitions[newTransId] = outWeight;
                }
            }

            // 处理生产者到 placeId 的输出弧
            auto prodOutIt = prod.outPlaces.find(placeId);
            if (prodOutIt != prod.outPlaces.end()) {
                weight_t prodWeight = prodOutIt->second;
                weight_t leftoverWeight = prodWeight - consWeight;
                if (leftoverWeight > 0) {
                    newTrans.outPlaces[placeId] = leftoverWeight;
                }
            }

            // 添加生产者的其他输出弧
            for (const auto& [outPlaceId, outWeight] : prod.outPlaces) {
                if (outPlaceId != placeId && places.count(outPlaceId)) {
                    newTrans.outPlaces[outPlaceId] = outWeight;
                    places[outPlaceId].inTransitions[newTransId] = outWeight;
                }
            }

            transitions[newTransId] = std::move(newTrans);
            count++;
        }

        // 移除原生产者
        eraseTransition(prodId);
        count++;
    }

    // 如果所有生产者被移除且初始标记为 0，则移除库所和消费者
    if (removedAllProducers && place.tokens == 0) {
        // std::vector<std::string> consumersToRemove(place.outTransitions.begin(), place.outTransitions.end());
        std::vector<std::string> consumersToRemove;
        consumersToRemove.reserve(place.outTransitions.size()); // 预分配提升效率
        for (const auto& [consId, _] : place.outTransitions) {
            consumersToRemove.push_back(consId);
        }
        for (const std::string& consId : consumersToRemove) {
            eraseTransition(consId);
        }
        erasePlace(placeId);
        count++;
    }

    return count;
}
// 规则S：聚合规则
// 检查库所是否满足规则S的条件
bool PetriStructureReducer::canApplyRuleS(const string& placeId) {
    // 首先检查库所是否存在
    auto placeIt = places.find(placeId);
    if (placeIt == places.end()) {
        return false;
    }
    
    const PetriPlace& place = placeIt->second;
    
    // S1: 库所不是重要库所
    if (significantPlaces.find(placeId) != significantPlaces.end()) {
        return false;
    }
    
    // S2: 库所有输入变迁和输出变迁
    if (place.inTransitions.empty() || place.outTransitions.empty()) {
        return false;
    }
    
    // 检查输入和输出变迁是否有重要变迁
    for (const auto& [transId, _] : place.inTransitions) {
        if (significantTransitions.find(transId) != significantTransitions.end()) {
            return false;
        }
    }
    
    for (const auto& [transId, _] : place.outTransitions) {
        if (significantTransitions.find(transId) != significantTransitions.end()) {
            return false;
        }
    }
    
    // S3: 库所的初始标识小于所有输出弧的权重
    for (const auto& [transId, weight] : place.outTransitions) {
        if (place.tokens >= weight) {
            return false;
        }
    }
    
    // S4: 输入变迁集合和输出变迁集合不相交
    for (const auto& [inTransId, _] : place.inTransitions) {
        if (place.outTransitions.find(inTransId) != place.outTransitions.end()) {
            return false;
        }
    }
    
    // S5: 检查所有输入变迁
    for (const auto& [prodId, prodWeight] : place.inTransitions) {
        // 检查变迁是否存在
        auto prodIt = transitions.find(prodId);
        if (prodIt == transitions.end()) {
            return false;
        }
        
        const PetriTransition& producer = prodIt->second;
        
        // S6: 输入变迁只有一个输出库所
        if (producer.outPlaces.size() != 1) {
            return false;
        }
        
        // S7: 输入变迁的输入库所不包含重要库所
        for (const auto& [inPlaceId, _] : producer.inPlaces) {
            if (significantPlaces.find(inPlaceId) != significantPlaces.end()) {
                return false;
            }
        }
        
        // S8: 检查输入变迁的输入库所的后继变迁集合是否只包含place的输入变迁
        for (const auto& [inPlaceId, _] : producer.inPlaces) {
            // 检查输入库所是否存在
            auto inPlaceIt = places.find(inPlaceId);
            if (inPlaceIt == places.end()) {
                return false;
            }
            
            const PetriPlace& inPlace = inPlaceIt->second;
            for (const auto& [outTransId, _] : inPlace.outTransitions) {
                if (place.inTransitions.find(outTransId) == place.inTransitions.end()) {
                    return false;
                }
            }
        }
        
        // S9: 对于所有输出变迁，检查输入弧权重是否整除输入变迁的输出弧权重
        for (const auto& [consId, consWeight] : place.outTransitions) {
            if (prodWeight % consWeight != 0) {
                return false;
            }
        }
    }
    const int MAX_NEW_TRANSITIONS = 1e4;
    // 检查是否会导致变迁数量过度增加
    int newTransCount = 0;
    for (const auto& [prodId, prodWeight] : place.inTransitions) {
        for (const auto& [consId, consWeight] : place.outTransitions) {
            newTransCount += prodWeight / consWeight;
        }
    }
    
    // 如果新增变迁数量过多，不应用规则
    if (newTransCount > MAX_NEW_TRANSITIONS) {
        return false;
    }
    
    return true;
}

// 应用规则S进行约简
int PetriStructureReducer::applyRuleS() {
    int count = 0;
    vector<string> placesToCheck;
    
    // 收集所有可能的库所
    for (const auto& [placeId, _] : places) {
        placesToCheck.push_back(placeId);
    }
    
    for (const string& placeId : placesToCheck) {
        // 检查库所是否仍然存在（可能在之前的迭代中被删除）
        auto placeIt = places.find(placeId);
        if (placeIt == places.end()) {
            continue;
        }
        
        if (canApplyRuleS(placeId)) {
            const PetriPlace& place = placeIt->second;
            
            // 为每对输入变迁和输出变迁创建新的聚合变迁
            vector<pair<string, weight_t>> inTransitions;
            for (const auto& inTrans : place.inTransitions) {
                inTransitions.push_back(inTrans);
            }
            
            vector<pair<string, weight_t>> outTransitions;
            for (const auto& outTrans : place.outTransitions) {
                outTransitions.push_back(outTrans);
            }
            
            for (const auto& [prodId, prodWeight] : inTransitions) {
                // 检查生产者是否存在
                auto prodIt = transitions.find(prodId);
                if (prodIt == transitions.end()) {
                    continue;
                }
                
                const PetriTransition& producer = prodIt->second;
                
                for (const auto& [consId, consWeight] : outTransitions) {
                    // 检查消费者是否存在
                    auto consIt = transitions.find(consId);
                    if (consIt == transitions.end()) {
                        continue;
                    }
                    
                    const PetriTransition& consumer = consIt->second;
                    
                    // 计算可以执行多少次consumer
                    weight_t k = prodWeight / consWeight;
                    
                    // 创建新的聚合变迁
                    for (weight_t k_i = 1; k_i <= k; k_i++) {
                        string newTransId = "agg_" + prodId + "_" + consId + "_" + to_string(k_i);
                        PetriTransition newTrans;
                        newTrans.id = newTransId;
                        
                        // 添加producer的输入弧
                        for (const auto& [inPlaceId, inWeight] : producer.inPlaces) {
                            // 检查输入库所是否存在
                            if (places.find(inPlaceId) == places.end()) {
                                continue;
                            }
                            
                            newTrans.inPlaces[inPlaceId] = inWeight;
                            places[inPlaceId].outTransitions[newTransId] = inWeight;
                        }
                        
                        // 添加consumer的输出弧，权重乘以k_i
                        for (const auto& [outPlaceId, outWeight] : consumer.outPlaces) {
                            // 检查输出库所是否存在
                            if (places.find(outPlaceId) == places.end()) {
                                continue;
                            }
                            
                            newTrans.outPlaces[outPlaceId] = outWeight * k_i;
                            places[outPlaceId].inTransitions[newTransId] = outWeight * k_i;
                        }
                        
                        // 添加consumer的输入弧（除了当前处理的库所）
                        for (const auto& [inPlaceId, inWeight] : consumer.inPlaces) {
                            if (inPlaceId != placeId) {
                                // 检查输入库所是否存在
                                if (places.find(inPlaceId) == places.end()) {
                                    continue;
                                }
                                
                                newTrans.inPlaces[inPlaceId] = inWeight * k_i;
                                places[inPlaceId].outTransitions[newTransId] = inWeight * k_i;
                            }
                        }
                        
                        // 如果k_i < k，需要添加到place的输出弧
                        if (k_i < k) {
                            weight_t remainingTokens = (k - k_i) * consWeight;
                            newTrans.outPlaces[placeId] = remainingTokens;
                            
                            // 确保库所仍然存在
                            if (places.find(placeId) != places.end()) {
                                places[placeId].inTransitions[newTransId] = remainingTokens;
                            }
                        }
                        
                        // 添加新变迁
                        transitions[newTransId] = newTrans;
                        count++;
                    }
                }
            }
            
            // 删除原始的输出变迁
            vector<string> transToRemove;
            for (const auto& [consId, _] : place.outTransitions) {
                transToRemove.push_back(consId);
            }
            
            for (const string& transId : transToRemove) {
                if (transitions.find(transId) != transitions.end()) {
                    eraseTransition(transId);
                    count++;
                }
            }
            
            // 如果库所没有输出变迁了，也删除输入变迁和库所本身
            if (place.outTransitions.size() == transToRemove.size()) {
                vector<string> inTransToRemove;
                for (const auto& [prodId, _] : place.inTransitions) {
                    inTransToRemove.push_back(prodId);
                }
                
                for (const string& prodId : inTransToRemove) {
                    if (transitions.find(prodId) != transitions.end()) {
                        eraseTransition(prodId);
                        count++;
                    }
                }
                
                // 从unit中移除库所
                erasePlace(placeId);
                count++;
            }
        }
    }
    
    return count;
}

void PetriStructureReducer::exportToHumanReadableFile(const string& filename) const {
    // 打开输出文件
    ofstream fout(filename);
    if (!fout) {
        cerr << "无法创建文件: " << filename << endl;
        return;
    }
    
    // 使用固定宽度以美化输出
    fout << fixed;
    
    // 写入标题和基本统计信息
    fout << "===========================================" << endl;
    fout << "        Petri网结构 - 人类可读格式        " << endl;
    fout << "===========================================" << endl << endl;
    
    fout << "网络统计:" << endl;
    fout << "  库所数量: " << places.size() << endl;
    fout << "  变迁数量: " << transitions.size() << endl;
    fout << "  单元数量: " << units.size() << endl;
    fout << "  重要库所: " << significantPlaces.size() << endl;
    fout << endl;
    
    // 打印重要库所列表
    if (!significantPlaces.empty()) {
        fout << "重要库所列表:" << endl;
        fout << "-------------------------------------------" << endl;
        for (const string& placeId : significantPlaces) {
            fout << "  " << placeId;
            // 添加库所的当前标识
            auto it = places.find(placeId);
            if (it != places.end()) {
                fout << " (标识数: " << it->second.tokens << ")";
            }
            fout << endl;
        }
        fout << endl;
    }
    
    // 按单元组织库所
    fout << "单元与库所:" << endl;
    fout << "-------------------------------------------" << endl;
    
    // 先处理有单元的库所
    for (const auto& [unitId, unit] : units) {
        if (unit.places.empty()) continue;
        
        fout << "单元: " << unitId << endl;
        for (const string& placeId : unit.places) {
            const auto& place = places.at(placeId);
            fout << "  库所: " << placeId
                 << " (标识数: " << place.tokens << ")" << endl;
                 
            // 显示输入变迁
            if (!place.inTransitions.empty()) {
                fout << "    输入变迁:" << endl;
                for (const auto& [transId, weight] : place.inTransitions) {
                    fout << "      " << transId << " (权重: " << weight << ")" << endl;
                }
            }
            
            // 显示输出变迁
            if (!place.outTransitions.empty()) {
                fout << "    输出变迁:" << endl;
                for (const auto& [transId, weight] : place.outTransitions) {
                    fout << "      " << transId << " (权重: " << weight << ")" << endl;
                }
            }
            fout << endl;
        }
    }
    
    // 处理没有单元的库所
    bool hasPlacesWithoutUnit = false;
    for (const auto& [placeId, place] : places) {
        if (place.unitId.empty()) {
            if (!hasPlacesWithoutUnit) {
                fout << "无单元库所:" << endl;
                hasPlacesWithoutUnit = true;
            }
            
            fout << "  库所: " << placeId
                 << " (标识数: " << place.tokens << ")" << endl;
                 
            // 显示输入变迁
            if (!place.inTransitions.empty()) {
                fout << "    输入变迁:" << endl;
                for (const auto& [transId, weight] : place.inTransitions) {
                    fout << "      " << transId << " (权重: " << weight << ")" << endl;
                }
            }
            
            // 显示输出变迁
            if (!place.outTransitions.empty()) {
                fout << "    输出变迁:" << endl;
                for (const auto& [transId, weight] : place.outTransitions) {
                    fout << "      " << transId << " (权重: " << weight << ")" << endl;
                }
            }
            fout << endl;
        }
    }
    
    // 变迁列表及其连接
    fout << "变迁详细信息:" << endl;
    fout << "-------------------------------------------" << endl;
    for (const auto& [transId, trans] : transitions) {
        fout << "变迁: " << transId << endl;
        
        // 显示输入库所
        if (!trans.inPlaces.empty()) {
            fout << "  输入库所:" << endl;
            for (const auto& [placeId, weight] : trans.inPlaces) {
                fout << "    " << placeId << " (权重: " << weight << ")";
                
                // 添加当前库所标识信息
                auto it = places.find(placeId);
                if (it != places.end()) {
                    fout << " [当前标识: " << it->second.tokens << "]";
                }
                fout << endl;
            }
        }
        
        // 显示输出库所
        if (!trans.outPlaces.empty()) {
            fout << "  输出库所:" << endl;
            for (const auto& [placeId, weight] : trans.outPlaces) {
                fout << "    " << placeId << " (权重: " << weight << ")" << endl;
            }
        }
        
        // 判断变迁是否已激活
        bool enabled = true;
        for (const auto& [placeId, weight] : trans.inPlaces) {
            auto it = places.find(placeId);
            if (it == places.end() || it->second.tokens < weight) {
                enabled = false;
                break;
            }
        }
        
        fout << "  状态: " << (enabled ? "已激活" : "未激活") << endl;
        fout << endl;
    }
    
    fout << "===========================================" << endl;
    fout << "           导出完成                       " << endl;
    fout << "===========================================" << endl;
    
    fout.close();
}

// 规范化删除变迁的函数
void PetriStructureReducer::eraseTransition(const string& transId) {
    // 检查变迁是否存在
    if (transitions.find(transId) == transitions.end()) {
        return;
    }
    
    // 检查是否是重要变迁，如果是则不删除
    if (significantTransitions.find(transId) != significantTransitions.end()) {
        return;
    }
    
    const PetriTransition& trans = transitions[transId];
    
    // 从所有相关库所中移除对该变迁的引用
    for(auto & [_, place] : places){
        if (place.outTransitions.find(transId) != place.outTransitions.end()) {
            place.outTransitions.erase(transId);
        }
        if (place.inTransitions.find(transId) != place.inTransitions.end()) {
            place.inTransitions.erase(transId);
        }
    }
    // for (const auto& [placeId, _] : trans.inPlaces) {
    //     if (places.find(placeId) != places.end()) {
    //         places[placeId].outTransitions.erase(transId);
    //     }
    // }
    
    // for (const auto& [placeId, _] : trans.outPlaces) {
    //     if (places.find(placeId) != places.end()) {
    //         places[placeId].inTransitions.erase(transId);
    //     }
    // }
    
    // 删除变迁
    transitions.erase(transId);
}

// 规范化删除库所的函数
void PetriStructureReducer::erasePlace(const string& placeId) {
    // 检查库所是否存在
    if (places.find(placeId) == places.end()) {
        return;
    }
    
    const PetriPlace& place = places[placeId];
    
    // 从所有相关变迁中移除对该库所的引用
    for(auto & [_, transition] : transitions){
        if (transition.outPlaces.find(placeId) != transition.outPlaces.end()) {
            transition.outPlaces.erase(placeId);
        }
        if (transition.inPlaces.find(placeId) != transition.inPlaces.end()) {
            transition.inPlaces.erase(placeId);
        }
    }
    // for (const auto& [transId, _] : place.inTransitions) {
    //     if (transitions.find(transId) != transitions.end()) {
    //         transitions[transId].outPlaces.erase(placeId);
    //     }
    // }
    
    // for (const auto& [transId, _] : place.outTransitions) {
    //     if (transitions.find(transId) != transitions.end()) {
    //         transitions[transId].inPlaces.erase(placeId);
    //     }
    // }
    
    // 从unit中移除
    if (units.find(place.unitId) != units.end()) {
        units[place.unitId].places.erase(placeId);
    }
    
    // 从重要库所集合中移除（如果存在）
    significantPlaces.erase(placeId);
    
    // 删除库所
    places.erase(placeId);
}