main.cpp

#include "product.h"
#include "Petri_Net.h"  // 确保这个先包含
#include "BA/Simplifier.h"  // 然后才是Simplifier.h
#include <iostream>
#include <sys/time.h>
#include "thread_pool.h"
#include "bitree/table2.h"
#include <sys/resource.h>
#include <errno.h>
#include <vector>
#include <future>
#include <array>
#include <signal.h>
#include <getopt.h>

using namespace std;
using namespace EnPAC;  // 添加EnPAC命名空间的引用
mutex _lock; 
#define TOTALTOOLTIME 180

// const int CORES = 4; // 处理器核心数
const int CORES = 4; // 处理器核心数
// const int CORES = 1; // 处理器核心数

size_t  heap_malloc_total, heap_free_total,mmap_total, mmap_count;
void print_info() {
    malloc_stats();
}

// 使用RAII方式确保线程在函数退出时被正确终止
struct ThreadGuard {
    std::thread& t;
    std::atomic<bool>& exit_flag;
    ThreadGuard(std::thread& thread, std::atomic<bool>& flag) : t(thread), exit_flag(flag) {}
    ~ThreadGuard() {
        exit_flag.store(true);
        if (t.joinable()) t.join();
    }
};
// NUM_t FIELDCOUNT;
// NUM_t placecount;
// NUM_t transitioncount;
// NUM_t MARKLEN;
// bool NUPN = false;            //whether the checking process uses NUPN encoding
// bool SAFE = false;            //whether the checking process uses SAFE encoding
// bool PINVAR = false;          //whether the checking process uses P-invariant encoding
// bool LONGBITPLACE = false;    //whether the checking process externs marking storage from short to int
// bool SLICEPLACE = true;       //whether using Petri-nets slice (cut off places)
// bool SLICETRANSITION = true;  //whether using Petri-nets slice (cut off transitions)
// atomic_bool ready2exit(false);
jmp_buf petrienv;

//以MB为单位
short int total_mem;          //memory limit
pid_t mypid;
// Petri *petri = NULL;

template <typename T, size_t state_cnt, size_t threads_cnt>
class GlobalVariables {
public:
    DataStructure<T>* htable;
    stateColor* state_color;
    vector<bitset<state_cnt>> state_color_cyan;

    GlobalVariables(size_t hash_size) {
        if (hash_size == 0) {
            hash_size = state_cnt;
        }
        htable = DataStructureFactory<T>::create(state_cnt, hash_size);
        state_color = new stateColor(state_cnt);
        state_color_cyan.resize(threads_cnt);
    }
    void clear() {
        if (htable) htable->clear();
    }
    void init(PetriNetConfig& petri_net_config) {
        htable->init(petri_net_config.FIELDCOUNT*2);
        state_color->reset();
        for (auto & i : state_color_cyan){
            i.reset();
        }
    }
    ~GlobalVariables() {
        delete htable;
        delete state_color;
    }
};

int debug_test = -1;

double get_time() {
    struct timeval t;
    gettimeofday(&t, NULL);
    return t.tv_sec + t.tv_usec / 1000000.0;
}

void CHECKMEM() {
    mypid = getpid();
        
    // 设置资源限制，防止OOM Killer终止进程
    struct rlimit rlim;
    // 设置为总内存的90%，单位是字节
    rlim.rlim_cur = total_mem * 1024 * 1024 * 0.9;
    rlim.rlim_max = total_mem * 1024 * 1024;
    
    // 设置虚拟内存限制
    // if (setrlimit(RLIMIT_AS, &rlim) != 0) {
    //     std::cerr << "设置内存限制失败: " << strerror(errno) << std::endl;
    // } else {
    //     std::cout << "已设置内存限制为: " << (total_mem * 0.9) << "MB" << std::endl;
    // }
}

template<size_t state_cnt, size_t threads_cnt, typename GlobalVType>
char CHECKLTL(size_t property_id, PetriNetConfig &petri_net_config, bool cardinality, GlobalVType &globals, int time_limit_model_check, int time_limit_reduce, bool reduce = true, string applyrules = "abcdefghijklmnopqrstuvwxyz",BuchiOptimization optimization = BuchiOptimization::High, APCompression compression = APCompression::None, int query_reduction_timeout = 0, int lp_timeout = 10, bool print_query_stats = true) {
    // 添加内存检查
    // struct rusage usage;
    // getrusage(RUSAGE_SELF, &usage);
    // long current_memory = usage.ru_maxrss / 1024; // 转换为MB
    
    // 如果当前内存使用已经超过总内存的70%，直接返回未知结果
    // if (current_memory > total_mem * 0.7) {
    //     std::cerr << "内存使用已达到: " << current_memory << "MB，跳过属性 " << property_id << std::endl;
    //     return '?';
    // }
    
    // BitRG *bitgraph;
    General *GBA = nullptr;
    Buchi *BA = nullptr;
    StateBuchi *SBA = nullptr;
    Syntax_Tree *syntaxTree = nullptr;
    double starttime, endtime;
    char result = '?';
    string propertyid;
    auto petri = petri_net_config.petri;
    
    NUM_t& FIELDCOUNT = petri_net_config.FIELDCOUNT;
    NUM_t& placecount = petri_net_config.placecount;
    NUM_t& transitioncount = petri_net_config.transitioncount;
    NUM_t& MARKLEN = petri_net_config.MARKLEN;
    bool& NUPN = petri_net_config.NUPN;
    bool& SAFE = petri_net_config.SAFE;
    bool& PINVAR = petri_net_config.PINVAR;
    bool& LONGBITPLACE = petri_net_config.LONGBITPLACE;
    bool& SLICEPLACE = petri_net_config.SLICEPLACE;
    bool& SLICETRANSITION = petri_net_config.SLICETRANSITION;    
    char ff[] = "LTLFireability.xml";
    char cc[] = "LTLCardinality.xml";
    
    std::atomic<bool> should_abort(false);
    // 使用future来控制前半部分的超时
    auto preprocessing_future = std::async(std::launch::async, [&]() -> char {
        // 创建一个原子变量来指示是否应该中断
        
        try {
            // 添加内存监控线程
            std::thread memory_monitor([&]() {
                while (!should_abort.load()) {
                    // 获取当前进程内存使用情况
                    struct rusage usage;
                    getrusage(RUSAGE_SELF, &usage);
                    // 转换为MB
                    long used_memory = usage.ru_maxrss / 1024;
                    
                    // 如果内存使用超过阈值(设为总内存的75%)，设置中断标志
                    if (used_memory > total_mem * 0.9) {
                        globals.clear();
                        // std::cerr << "预处理阶段内存使用达到阈值: " << used_memory << "MB，中断处理" << std::endl;
                        should_abort.store(true);
                        break;
                    }
                    
                    // 每秒检查一次
                    std::this_thread::sleep_for(std::chrono::seconds(1));
                }
            });
            ThreadGuard guard(memory_monitor, should_abort);
            // memory_monitor.detach();
            
            // 在预处理的关键点检查是否应该中断
            syntaxTree = new Syntax_Tree(petri_net_config);
            if (should_abort.load()) throw std::runtime_error("预处理阶段内存不足");
            
            // 解析XML文件中的特定属性
            if (cardinality) {
                if (syntaxTree->ParseXML(cc, propertyid, property_id) == CONSISTENCY_ERROR) {
                    cout << "FORMULA " << propertyid << " CANNOT_COMPUTE" << endl;
                    delete syntaxTree;
                    return '?';
                }
            } else {
                if (syntaxTree->ParseXML(ff, propertyid, property_id) == CONSISTENCY_ERROR) {
                    cout << "FORMULA " << propertyid << " CANNOT_COMPUTE" << endl;
                    delete syntaxTree;
                    return '?';
                }
            }

            // 在每个主要操作后检查是否应该中断
            if (should_abort.load()) throw std::runtime_error("预处理阶段内存不足");
            MallocExtension::instance()->ReleaseFreeMemory();
            // syntaxTree->PrintTree();
            syntaxTree->Push_Negation(syntaxTree->root);
            
            // cout<<"old AT:"<<endl;
            // syntaxTree->PrintAT();
            // 添加查询约简调用
            bool slice = syntaxTree->isNextFree();
            // bool slice = syntaxTree->isNextFree();
            slice = false;
            // cout<<"syntaxTree->isNextFree(); "<< syntaxTree->isNextFree() <<endl;
            // syntaxTree->PrintTree();
            petri->syntaxTree_contains_next = syntaxTree->hasNextOperator || !syntaxTree->isNextFree();
            syntaxTree->SimplifyLTL(true, optimization, compression);
            // syntaxTree->PrintTree();
            simplify_queries(syntaxTree, petri_net_config, query_reduction_timeout, lp_timeout, print_query_stats);
            // syntaxTree->PrintTree();
            // cout<<"syntaxTree->isNextFree(); "<< syntaxTree->isNextFree() <<endl;
            
            // syntaxTree->Evaluate(syntaxTree->root);
            if (syntaxTree->root->groundtruth != UNKNOW) {
                cout << "FORMULA " << propertyid << " " << ((syntaxTree->root->groundtruth == TRUE) ? "FALSE" : "TRUE") << endl;
                return ((syntaxTree->root->groundtruth == TRUE) ? 'F' : 'T');
            }
            // syntaxTree->Universe(syntaxTree->root);
            // syntaxTree->Get_DNF(syntaxTree->root);
            // syntaxTree->Build_VWAA();
            // syntaxTree->VWAA_Simplify();
            syntaxTree->getVisibleIterms(cardinality, petri);
            // slice = false;
            // reduce = false;
            if (reduce) {
                // 获取LTL公式的属性，并设置到petri对象
                petri->syntaxTree_is_ltl = true; // 默认为LTL公式
                
                petri->structureReduce(syntaxTree->visibleIterms,cardinality,applyrules,time_limit_reduce);
                syntaxTree->RebuildAT();
                // delete syntaxTree;
                // syntaxTree = new Syntax_Tree(petri_net_config);
                // if (cardinality) {
                //     syntaxTree->ParseXML(cc, propertyid, property_id);
                // } else {
                //     syntaxTree->ParseXML(ff, propertyid, property_id);
                // }
                // syntaxTree->Push_Negation(syntaxTree->root);
                
                // // 在结构约简后再次进行查询约简
                // syntaxTree->SimplifyLTL(true, optimization, compression);
                // simplify_queries(syntaxTree, petri_net_config, query_reduction_timeout, lp_timeout, print_query_stats);
                
                // syntaxTree->Evaluate(syntaxTree->root);
                // if (syntaxTree->root->groundtruth != UNKNOW) {
                //     cout << "FORMULA " << propertyid << " " << ((syntaxTree->root->groundtruth == TRUE) ? "FALSE" : "TRUE") << endl;
                //     return ((syntaxTree->root->groundtruth == TRUE) ? 'F' : 'T');
                // }
                syntaxTree->getVisibleIterms(cardinality, petri);

                // slice = syntaxTree->isNextFree();
                // slice = false;
            }
            
            syntaxTree->Universe(syntaxTree->root);
            syntaxTree->Get_DNF(syntaxTree->root);
            syntaxTree->Build_VWAA();
            syntaxTree->VWAA_Simplify();
            // 在每个主要操作后检查是否应该中断
            if (should_abort.load()) throw std::runtime_error("预处理阶段内存不足");
            MallocExtension::instance()->ReleaseFreeMemory();
            petri->constructMatrix();
            petri->judgeSAFE();
            petri->judgePINVAR();
            petri->destroyMatrix();
            petri->setGlobalPetriAttribute();

            if (slice) {
                SLICEPLACE = SLICETRANSITION = true;
                petri->implementSlice(syntaxTree->visibleIterms,cardinality);
            } else {
                SLICEPLACE = SLICETRANSITION = false;
                petri->computeOrder(syntaxTree->visibleIterms,cardinality);
                petri->undoSlicePlace();
                petri->undoSliceTrans();
            }
            
            petri->setGlobalPetriAttribute();
            setGlobalValue(petri_net_config);
            globals.init(petri_net_config);

            // 在每个主要操作后检查是否应该中断
            if (should_abort.load()) throw std::runtime_error("预处理阶段内存不足");
            MallocExtension::instance()->ReleaseFreeMemory();
            GBA = new General;
            GBA->Build_GBA(*syntaxTree);
            GBA->Simplify();
            GBA->self_check();

            BA = new Buchi;
            BA->Build_BA(*GBA);
            BA->Simplify();
            BA->self_check();
            BA->Backward_chaining();

            SBA = new StateBuchi;
            SBA->Build_SBA(*BA);
            SBA->Simplify();
            SBA->Tarjan();
            SBA->Complete1();
            SBA->Add_heuristic();
            SBA->Complete2();
            SBA->self_check();
            SBA->linkAtomics(syntaxTree->AT,cardinality);
            
            should_abort.store(true);
            return 0; // 成功完成预处理
        }
        catch (const std::exception& e) {
            should_abort.store(true);
            // std::cerr << "预处理阶段异常: " << e.what() << std::endl;
            return '?';
        }
        catch (...) {
            should_abort.store(true);
            // std::cerr << "预处理阶段未知异常" << std::endl;
            return '?';
        }
    });

    starttime = get_time();
    
    // 等待预处理完成，设置超时
    auto preprocess_status = preprocessing_future.wait_for(std::chrono::seconds(time_limit_model_check));
    
    if (preprocess_status == std::future_status::timeout) {
        should_abort.store(true);
        // std::cerr << "属性 " << property_id-1 << " 预处理阶段超时" << std::endl;
        // 清理资源
        if (syntaxTree) delete syntaxTree;
        if (GBA) delete GBA;
        if (BA) delete BA;
        if (SBA) delete SBA;
        return '?';
    }
    
    char preprocess_result = preprocessing_future.get();
    if (preprocess_result != 0) {
        // 预处理阶段返回了结果或出错
        return preprocess_result;
    }

    // 预处理成功完成，继续执行后半部分
    string Techniques;
    Product_Automata<BitRGNode, threads_cnt, GlobalVType> *product;
    product = new Product_Automata<BitRGNode, threads_cnt, GlobalVType>(petri_net_config, SBA, globals);
    std::atomic<bool> monitor_should_exit(false);
    auto future = std::async(std::launch::async, [&]() {
        // 创建一个原子变量来控制内存监控线程
        try {
            // 添加内存监控逻辑
            // std::thread memory_monitor([&]() {
            //     while (!monitor_should_exit.load() && !product->ready2exit.load()) {
            //         // 获取当前进程内存使用情况
            //         struct rusage usage;
            //         getrusage(RUSAGE_SELF, &usage);
            //         // 转换为MB
            //         long used_memory = usage.ru_maxrss / 1024;
                    
            //         // 如果内存使用超过阈值(设为总内存的80%)，主动中断
            //         if (used_memory > total_mem * 0.9) {
            //             // std::cerr << "内存使用达到阈值: " << used_memory << "MB，主动中断" << std::endl;
            //             product->timeflag.store(false);
            //             product->ready2exit.store(true);
            //             monitor_should_exit.store(true);
            //             break;
            //         }
                    
            //         // 每秒检查一次
            //         std::this_thread::sleep_for(std::chrono::seconds(1));
            //     }
            // });
            
            // ThreadGuard guard(memory_monitor, monitor_should_exit);
            // 设置内存监控线程为分离状态
            // memory_monitor.detach();
            
            product->ModelChecker(propertyid, time_limit_model_check, Techniques);
        } 
        catch (const std::exception& e) {
            // 处理异常，可能是由于超时导致的
            result = '?';
            cout << "Exception caught: " << e.what() << endl;
        }
    });

    auto status = future.wait_for(std::chrono::seconds(time_limit_model_check));

    if (status == std::future_status::timeout) {
        product->timeflag.store(false);
        product->ready2exit.store(true);
        monitor_should_exit.store(true);
        // 可能需要额外的机制来确保ModelChecker能及时响应终止信号
    }
    
    while(1){
        auto final_status = future.wait_for(std::chrono::seconds(2));
        if (final_status == std::future_status::ready) {
            // cout << " ModelChecker已正常结束" << endl;
            break;
        } else {
            // cout << " ModelChecker可能仍在运行" << endl;
        }
    }
    endtime = get_time();

    // cout << " NODECOUNT " << globals.htable->get_count() << " TIME " << (endtime - starttime)
    //         << " MEM " << product->get_current_mem() << Techniques << endl;
    if(Techniques!=""){
        cout << " TECHNIQUES" << Techniques;
    }
    cout << endl;

    int ret = product->getresult();
                
    if (ret == -1) {
        result = '?';
    } else {
        result = (ret == 0) ? 'F' : 'T';
    }
    delete product;

    // 清理资源
    // if (SLICEPLACE && PINVAR) {
    //     petri->undoPinvarSlicePlace();
    // } else if (SLICEPLACE)
    //     petri->undoSlicePlace();
    // if (SLICETRANSITION)
    //     petri->undoSliceTrans();

    
    endtime = get_time();
    // cout << "PROPERTY " << property_id << " TIME " << (endtime - starttime) << " RESULT " << result << endl;

    delete syntaxTree;
    delete GBA;
    delete BA;
    delete SBA;

    if (status == std::future_status::timeout) {
        return '?';  // 超时
    } else {
        return result;
    }
}

// 辅助函数：运行一组任务
void runBatch(const std::vector<std::function<char()>>& batch, int startIndex) {
    std::vector<std::future<char>> futures;
    for (const auto& task : batch) {
        futures.emplace_back(std::async(std::launch::async, task));
    }
    
    bool allFinished = false;
    while (!allFinished) {
        allFinished = true;
        for (size_t i = 0; i < futures.size(); ++i) {
            auto status = futures[i].wait_for(std::chrono::seconds(0));
            if (status != std::future_status::ready) {
                allFinished = false;
                break;
            }
        }
        if (!allFinished) {
            std::this_thread::sleep_for(std::chrono::milliseconds(100));
        }
    }
    // cout<<"end"<<endl;
    // 在批处理结束后释放内存
    MallocExtension::instance()->ReleaseFreeMemory();
    
    // 输出当前内存使用情况
    struct rusage usage;
    getrusage(RUSAGE_SELF, &usage);
    // std::cout << "当前内存使用: " << (usage.ru_maxrss / 1024) << "MB" << std::endl;
    
    // for (size_t i = 0; i < futures.size(); ++i) {
    //     futures[i].get();
    // }
}

void test(int argc, char *argv[]){
    // 添加命令行参数处理
    int query_reduction_timeout = 0;  // 默认不进行查询约简
    int lp_timeout = 10;  // 默认线性规划超时10秒
    bool print_statistics = true;  // 默认打印统计信息
    
    if (argc >= 2) {
        debug_test = stoi(argv[1]);
    }
    CHECKMEM();
    
    constexpr size_t NUM_PROPERTIES = 16;
    const int SHORT_TIMEOUT = 30; // 短限时
    // const int LONG_TIMEOUT = 30; // 长限时，例如300秒
    // vector<future<char>> results;
    std::array<std::atomic<char>, NUM_PROPERTIES> result_chars;

    // 初始化结果数组
    for (auto& result : result_chars) {
        result.store('?');
    }

    std::vector<std::shared_ptr<PetriNetConfig>> configs;
    // std::vector<std::shared_ptr<GlobalVariables<vector<int>, tshort_size, 1>>> globals_vec;

    // 预先创建所需数量的 PetriNetConfig
    for (int i = 0; i < 1; ++i) {
        // configs.push_back(std::make_shared<PetriNetConfig>());
    //     globals_vec.push_back(std::make_shared<GlobalVariables<vector<int>, tshort_size, 1>>(0));
    }

    // auto globals = GlobalVariables<vector<int>, t2_size, 8>(hash_size);
    auto globals = GlobalVariables<vector<int>, tshort_size, 1>(0);
    for (int i = 0; i < NUM_PROPERTIES; ++i) {
        if (debug_test != -1 && debug_test != i) {
            continue;
        }
        if (result_chars[i].load() == '?') {
            configs.clear();
            configs.push_back(std::make_shared<PetriNetConfig>());
            // char result = CHECKLTL<t2_size, 8>(i+1, *(configs[0]), true, globals, LONG_TIMEOUT);
            char result = CHECKLTL<tshort_size, 1>(i+1, *(configs[0]), true, globals, SHORT_TIMEOUT, true);
            result_chars[i].store(result);
        }
        // break;
    }

    
    // 将结果写入文件
    ofstream outresult("boolresult.txt", ios::app);
    for (const auto& result : result_chars) {
        outresult << result.load();
    }
    outresult << endl;
    // for (int batchIndex = 0; batchIndex < (NUM_PROPERTIES + CORES - 1) / CORES; ++batchIndex) {
    //     std::vector<std::function<char()>> batchTasks;
    //     for (int i = 0; i < CORES && batchIndex * CORES + i < NUM_PROPERTIES; ++i) {
    //         int taskIndex = batchIndex * CORES + i;
    //         if (debug_test != -1 && debug_test != taskIndex) {
    //             continue;
    //         }
            
    //         configs.clear(); 
    //         configs.push_back(std::make_shared<PetriNetConfig>());
    //         batchTasks.push_back([taskIndex, SHORT_TIMEOUT, &result_chars, config = configs[i], globals_vec = globals_vec[i]]() {
    //             // cout<<"taskIndex: "<<taskIndex<<endl;
    //             char result = CHECKLTL<tshort_size, 1>(taskIndex+1, *config, true, *globals_vec, SHORT_TIMEOUT);
    //             result_chars[taskIndex].store(result);
    //             return result;
    //         });
    //     }
    //     // 运行这个批次的任务
    //     runBatch(batchTasks, batchIndex * CORES);
    // }
}

// 添加在main函数前的全局区域
void signal_handler(int sig) {
    // std::cerr << "捕获到信号: " << sig << std::endl;
    if (sig == SIGABRT) {
        // std::cerr << "程序内存不足，正在安全退出..." << std::endl;
        // 可以在这里执行一些清理工作
        exit(0); // 使用非137的退出码
    }
    exit(0);
}

int main(int argc, char *argv[]) {

    // 添加查询约简选项
    int query_reduction_timeout = 100;  // 默认不进行查询约简
    int lp_timeout = 10;  // 线性规划超时
    bool print_query_stats = false;  // 是否打印查询统计信息
    
    //4.14修改部分开始
    // 默认参数
    int time_limit_model_check = 300;         // 单位秒
    int time_limit_reduce = 300;
    int memory_limit = 16000;   // 单位MB
    std::string rules = "abcdefghijklmnopqrstuvwxyz"; // 默认规则
    int formula = -1;              // 新参数 --formula 的默认值
    std::string category = "c"; // 默认类别
    BuchiOptimization optimization = BuchiOptimization::High;
    APCompression compression = APCompression::None;

    // 定义 long options，包括新增的 --formula（非必需项）
    static struct option long_options[] = {
        {"BuchiOptimization", required_argument, 0, 'B'},
        {"APCompression", required_argument, 0, 'A'},
        {"category",                required_argument, 0, 'c'},
        {"tm",                required_argument, 0, 256},
        {"tr",                required_argument, 0, 257},
        {"time_limit_model_check",   required_argument, 0, 't'*'m'},
        {"time_limit_reduce",   required_argument, 0, 't'*'r'},
        {"memory_limit", required_argument, 0, 'm'},
        {"rules",        required_argument, 0, 'r'},
        {"formula",      required_argument, 0, 'f'},
        {"query-timeout", required_argument, 0, 'q'},   // 添加查询约简超时选项
        {"lp-timeout", required_argument, 0, 'l'},      // 添加线性规划超时选项
        {"query-stats", required_argument, 0, 's'},     // 添加查询统计信息选项
        {0, 0, 0, 0}
    };

    // 参数字符串中 f 后面使用两个冒号表示 --formula 的参数为可选参数
    // 参数字符串中，每个选项后面使用两个冒号表示参数为可选参数
    const char* short_options = "B::A::c::m::r::f::q::l::s::";
    int option_index = 0;
    int c;
    while ((c = getopt_long(argc, argv, short_options, long_options, &option_index)) != -1) {
        switch (c) {
            case 'B':
                if (optarg) {
                    if (strcmp(optarg, "High") == 0) {
                        optimization = BuchiOptimization::High;
                    } else if (strcmp(optarg, "Medium") == 0) {
                        optimization = BuchiOptimization::Medium;
                    } else if (strcmp(optarg, "Low") == 0) {
                        optimization = BuchiOptimization::Low;
                    } else {
                        // std::cerr << "无效的BuchiOptimization选项: " << optarg << std::endl;
                    }
                }
                break;
            case 'A':
                if (optarg) {
                    if (strcmp(optarg, "None") == 0) {
                        compression = APCompression::None;
                    } else if (strcmp(optarg, "Full") == 0) {
                        compression = APCompression::Full;
                    } else if (strcmp(optarg, "Choose") == 0) {
                        compression = APCompression::Choose;
                    } else {
                        // std::cerr << "无效的APCompression选项: " << optarg << std::endl;
                    }
                }
                break;
            case 'c':
                if (optarg) {
                    category = optarg;
                }
                break;
            case 256: // --tm
                if (optarg)
                    time_limit_model_check = atoi(optarg);
                // 若 optarg 为 NULL，则仍使用默认值
                break;
            case 257: // --tr
                if (optarg)
                    time_limit_reduce = atoi(optarg);
                // 若 optarg 为 NULL，则仍使用默认值
                break;
            case 't'*'m':
                if (optarg)
                    time_limit_model_check = atoi(optarg);
                // 若 optarg 为 NULL，则仍使用默认值
                break;
            case 't'*'r':
                if (optarg)
                    time_limit_reduce = atoi(optarg);
                // 若 optarg 为 NULL，则仍使用默认值
                break;
            case 'm':
                if (optarg)
                    memory_limit = atoi(optarg);
                break;
            case 'r':
                if (optarg)
                    rules = optarg;
                break;
            case 'f':
                if (optarg)
                    formula = atoi(optarg);
                break;
            case 'q':
                query_reduction_timeout = atoi(optarg);
                break;
            case 'l':
                lp_timeout = atoi(optarg);
                break;
            case 's':
                print_query_stats = atoi(optarg) != 0;
                break;
            default:
                std::cerr << "Usage: " << argv[0]
                          << " [--time_limit_model_check [seconds]] [--time_limit_reduce [seconds]] [--memory_limit [MB]] [--rules [ruleString]] [--formula [value] [--category [char]]"
                          //以./EnPAC_test --time_limit_model_check 300 --memory_limit 16 --rules abcdef --formula 1的方式，选项皆可选
                          << std::endl;
                exit(EXIT_FAILURE);
        }
    }
    
    // 根据传入的参数设置内存限制等（例如对memory_limit做转换）
    // 此处可以使用 memory_limit 参数替代原来的 total_mem
    total_mem = memory_limit; // 注意：total_mem单位应与实际一致

    // 后续程序使用 time_limit_model_check 和 rules 参数...
    // std::cout << "BuchiOptimization: " << ((optimization == BuchiOptimization::High) ? "High" : (optimization == BuchiOptimization::Medium) ? "Medium" : "Low") << std::endl;
    // std::cout << "APCompression: " << ((compression == APCompression::None) ? "None" : (compression == APCompression::Full) ? "Full" : "Choose") << std::endl;
    // std::cout << "模型检测时间限制: " << time_limit_model_check << "秒" << std::endl;
    // std::cout << "结构约简时间限制: " << time_limit_reduce << "秒" << std::endl;
    // std::cout << "内存限制: " << memory_limit << "MB" << std::endl;
    // std::cout << "使用规则: " << rules << std::endl;
    // std::cout << "公式参数: " << formula << std::endl;
    // std::cout << "类别参数: " << category << std::endl;
    //4.14修改部分结束

    // 设置信号处理
    signal(SIGABRT, signal_handler);
    signal(SIGSEGV, signal_handler);
    
    // test(argc, argv);
    // cout<<"test end"<<endl;
    // exit(0);

    //4.14修改部分开始
    // if (argc >= 2) {
    //     debug_test = stoi(argv[1]);
    // }
    if(formula != -1) {
        debug_test = formula;
    }
    //4.14修改部分结束

    CHECKMEM();

    double starttime, endtime;
    starttime = get_time();

    // CONSTRUCTPETRI();

    // const int NUM_PROPERTIES = 16;
    constexpr size_t NUM_PROPERTIES = 16;
    const int SHORT_TIMEOUT = 5; // 短限时，例如60秒
    const int LONG_TIMEOUT = 300; // 长限时，例如300秒

    // vector<future<char>> results;
    std::array<std::atomic<char>, NUM_PROPERTIES> result_chars;

    // 初始化结果数组
    for (auto& result : result_chars) {
        result.store('?');
    }

    std::vector<std::shared_ptr<PetriNetConfig>> configs;
    // std::vector<std::shared_ptr<GlobalVariables<vector<int>, tshort_size, 1>>> globals_vec;

    // 预先创建所需数量的 PetriNetConfig
    // for (int i = 0; i < CORES; ++i) {
    // // for (int i = 0; i < NUM_PROPERTIES; ++i) {
    //     configs.push_back(std::make_shared<PetriNetConfig>());
    //     globals_vec.push_back(std::make_shared<GlobalVariables<vector<int>, tshort_size, 1>>(0));
    //     // 可以在这里根据需要初始化每个 config
    // }

    // for (int batchIndex = 0; batchIndex < (NUM_PROPERTIES + CORES - 1) / CORES; ++batchIndex) {
    //     std::vector<std::function<char()>> batchTasks;
    //     configs.clear();
    //     for (int i = 0; i < CORES; ++i) {
    //         configs.push_back(std::make_shared<PetriNetConfig>());
    //     }
    //     for (int i = 0; i < CORES && batchIndex * CORES + i < NUM_PROPERTIES; ++i) {
    //         int taskIndex = batchIndex * CORES + i;
    //         batchTasks.push_back([taskIndex, SHORT_TIMEOUT, &result_chars, config = configs[i], globals_vec = globals_vec[i]]() {
    //         // batchTasks.push_back([taskIndex, SHORT_TIMEOUT, &result_chars, config = configs[taskIndex], globals_vec = globals_vec[i]]() {
    //             // cout<<"taskIndex: "<<taskIndex<<endl;
    //             char result = CHECKLTL<tshort_size, 1>(taskIndex+1, *config, true, *globals_vec, SHORT_TIMEOUT, false);
    //             result_chars[taskIndex].store(result);
    //             // cout<<"taskIndex: "<<taskIndex<<" result: "<<result<<endl;
    //             return result;
    //         });
    //     }

    //     // 运行这个批次的任务
    //     runBatch(batchTasks, batchIndex * CORES);

    //     // 可选：在这里更新 configs，如果需要的话
    //     // for (auto& config : configs) {
    //     //     // 更新 config
    //     // }
    // }
    
    //4.14修改部分开始
    // endtime = get_time();
    // cout<<"第1轮结束,时间: "<<endtime-starttime<<endl;
    // for (const auto& result : result_chars) {
    //     cout<<result.load();
    // }
    // cout<<endl;
    configs.clear();
    // configs.resize(1);
    // configs.push_back(std::make_shared<PetriNetConfig>());
    // globals_vec.clear();
    bool flag = false;
    vector<int> unSolvedProperties;
    for (int i = 0; i < NUM_PROPERTIES; ++i) {
        if (result_chars[i].load() == '?') {
            flag = true;
            unSolvedProperties.push_back(i);
        }
    }
    // if (flag) {
    // // 第二轮：高限时处理未解决的属性
    //     auto globals = GlobalVariables<vector<int>, t2_size, 4>(hash_size);
    //     for (auto i : unSolvedProperties) {
    //         // if (result_chars[i].load() == '?') {
    //             configs.clear();
    //             configs.push_back(std::make_shared<PetriNetConfig>());
    //             char result = CHECKLTL<t2_size, 4>(i+1, *(configs[0]), true, globals, LONG_TIMEOUT, true);
    //             result_chars[i].store(result);
    //         // }
    //     }
    //     cout<<endl;
    // }
    if (flag) {
    // 限时处理未解决的属性
        auto globals = GlobalVariables<vector<int>, t2_size, 4>(hash_size);
            for (auto i : unSolvedProperties) {
                if (debug_test != -1 && debug_test != i) {
                    continue;
                }
                configs.clear();
                configs.push_back(std::make_shared<PetriNetConfig>());
                // char result = CHECKLTL<t2_size, 8>(i+1, *(configs[0]), true, globals, LONG_TIMEOUT, true);
                if(category=="c") {
                    char result = CHECKLTL<t2_size, 4>(i+1, *(configs[0]), true, globals, 
                                                     time_limit_model_check, time_limit_reduce, 
                                                     true, rules, optimization, compression,
                                                     query_reduction_timeout, lp_timeout, print_query_stats);
                    result_chars[i].store(result);
                } else {
                    char result = CHECKLTL<t2_size, 4>(i+1, *(configs[0]), false, globals, 
                                                     time_limit_model_check, time_limit_reduce, 
                                                     true, rules, optimization, compression,
                                                     query_reduction_timeout, lp_timeout, print_query_stats);
                    result_chars[i].store(result);
                }
            }
        
        // cout<<endl;
    }
    //4.14修改部分结束
    
    endtime = get_time();
    // cout<<"第2轮结束,时间: "<<endtime-starttime<<endl;
    // for (const auto& result : result_chars) {
    //     cout<<result.load();
    // }
    // cout<<endl;

    // 将结果写入文件
    ofstream outresult("boolresult.txt", ios::app);
    for (const auto& result : result_chars) {
        outresult << result.load();
    }
    outresult << endl;

    endtime = get_time();
    // cout << "RUNTIME " << endtime - starttime << endl;

    return 0;
}