task3.cpp

#include "main.h"

BDD runTask3(Cudd& mgr, vector<Place>& places, vector<Transition>& transitions) {
    cout << "\n==========================================" << endl;
    cout << "   TASK 3: SYMBOLIC REACHABILITY (BDD)    " << endl;
    cout << "==========================================" << endl;
    auto start_time = chrono::high_resolution_clock::now();

    int numPlaces = places.size();
    
    map<Place*, int> placeToIndex;
    for (int i = 0; i < numPlaces; ++i) {
        placeToIndex[&places[i]] = i;
    }

    vector<BDD> x(numPlaces);
    vector<BDD> y(numPlaces);

    for (int i = 0; i < numPlaces; ++i) {
        x[i] = mgr.bddVar(2 * i);
        y[i] = mgr.bddVar(2 * i + 1);
    }

    BDD M0 = mgr.bddOne();
    for (int i = 0; i < numPlaces; ++i) {
        if (places[i].token > 0) {
            M0 *= x[i];
        } else {
            M0 *= !x[i];
        }
    }

    BDD T = mgr.bddZero();

    for (const auto& t : transitions) {
        BDD t_rel = mgr.bddOne();
        vector<bool> isAffected(numPlaces, false);

        for (Place* p : t.inputs) {
            int idx = placeToIndex[p];
            t_rel *= x[idx]; 
        }

        for (Place* p : t.inputs) {
            int idx = placeToIndex[p];
            bool isSelfLoop = false;
            for (Place* out : t.outputs) {
                if (out == p) { isSelfLoop = true; break; }
            }
            if (!isSelfLoop) {
                t_rel *= !y[idx];
                isAffected[idx] = true;
            }
        }
        for (Place* p : t.outputs) {
            int idx = placeToIndex[p];
            t_rel *= y[idx]; 
            isAffected[idx] = true;
        }

        for (int i = 0; i < numPlaces; ++i) {
            if (!isAffected[i]) {
                t_rel *= (x[i].Xnor(y[i])); 
            }
        }
        T += t_rel;
    }

    BDD R_current = M0;
    BDD R_prev = mgr.bddZero();
    
    BDD x_cube = mgr.bddOne();
    for (int i = 0; i < numPlaces; ++i) x_cube *= x[i];

    int steps = 0;
    while (R_current != R_prev) {
        R_prev = R_current;
        steps++;
        BDD next_y = R_current.AndAbstract(T, x_cube);
        BDD next_x = next_y.SwapVariables(y, x);
        R_current += next_x;
    }

    auto end_time = chrono::high_resolution_clock::now();
    chrono::duration<double> diff = end_time - start_time;

    cout << "Iterations: " << steps << endl;
    cout << "Total Reachable Markings: " << (long long)R_current.CountMinterm(numPlaces) << endl;
    cout << "BDD Nodes (Reachable Set): " << R_current.nodeCount() << endl;
    cout << "Runtime: " << diff.count() << " s" << endl;

    // Print
   cout << "\n[Reachable States - Sorted by Sequence Logic]" << endl;
    
    cout << "Place(s) ID / Marking:" << endl;
    for (int i = 0; i < numPlaces; ++i) cout << places[i].id << " ";
    cout << "\n------------------------" << endl;

    vector<string> discovered_states;
    
    DdGen *gen;
    int *cube;
    CUDD_VALUE_TYPE val;

    Cudd_ForeachCube(mgr.getManager(), R_current.getNode(), gen, cube, val) {
        string state_str = "";
        for (int i = 0; i < numPlaces; i++) {
            int index = 2 * i;
            if (cube[index] == 0) state_str += "0";
            else if (cube[index] == 1) state_str += "1";
            else state_str += "- ";
            for (size_t j = 0; j < places[i].id.length(); ++j) {
                state_str += " ";
            }
        }
        discovered_states.push_back(state_str);
    }

    sort(discovered_states.begin(), discovered_states.end(), greater<string>());

    for (const auto& s : discovered_states) {
        cout << s << endl;
    }

    cout << "==========================================" << endl;

    return R_current;
}