function petriDeadlockFixGui
% petriDeadlockFixGui Visualize how a Petri net 
% can expose and fix deadlocks.
%
% Mode 1 (deadlock-prone):
%   P0 --T1--> P1 --T2--> Pdead
%
% Mode 2 (fixed with recovery):
%   P0 --T1--> P1 --T2--> Pdead --T3--> P0
%
% The GUI computes the reachability graph and 
% highlights deadlock markings.

modeNames = ["Deadlock-prone", "Fixed with recovery"];

fig = uifigure('Name', 'Petri Net Deadlock Fix', 'Position', [100 100 1180 680]);

mainGrid = uigridlayout(fig, [1 2]);
mainGrid.ColumnWidth = {380, '1x'};
mainGrid.RowHeight = {'1x'};

leftPanel = uipanel(mainGrid, 'Title', 'Controls');
rightPanel = uipanel(mainGrid, 'Title', 'Reachability Graph');

leftGrid = uigridlayout(leftPanel, [10 2]);
leftGrid.RowHeight = {22, 22, 22, 28, 28, 28, 34, '1x', 24, 24};
leftGrid.ColumnWidth = {150, '1x'};

lbl = uilabel(leftGrid, 'Text', 'Petri Net Deadlock Fix', 'FontWeight', 'bold');
lbl.Layout.Row = 1;
lbl.Layout.Column = [1 2];

lbl = uilabel(leftGrid, 'Text', 'Deadlock-prone: P0 -> P1 -> Pdead');
lbl.Layout.Row = 2;
lbl.Layout.Column = [1 2];

lbl = uilabel(leftGrid, 'Text', 'Fixed: add Pdead -> P0 recovery');
lbl.Layout.Row = 3;
lbl.Layout.Column = [1 2];

lbl = uilabel(leftGrid, 'Text', 'Mode');
lbl.Layout.Row = 4;
lbl.Layout.Column = 1;

modeDropDown = uidropdown(leftGrid, ...
    'Items', cellstr(modeNames), ...
    'Value', char(modeNames(1)), ...
    'ValueChangedFcn', @computeAndPlot);
modeDropDown.Layout.Row = 4;
modeDropDown.Layout.Column = 2;

lbl = uilabel(leftGrid, 'Text', 'Initial P0');
lbl.Layout.Row = 5;
lbl.Layout.Column = 1;

p0Field = uieditfield(leftGrid, 'numeric', ...
    'Value', 1, ...
    'RoundFractionalValues', 'on', ...
    'Limits', [0 Inf], ...
    'ValueChangedFcn', @computeAndPlot);
p0Field.Layout.Row = 5;
p0Field.Layout.Column = 2;

lbl = uilabel(leftGrid, 'Text', 'Initial P1');
lbl.Layout.Row = 6;
lbl.Layout.Column = 1;

p1Field = uieditfield(leftGrid, 'numeric', ...
    'Value', 0, ...
    'RoundFractionalValues', 'on', ...
    'Limits', [0 Inf], ...
    'ValueChangedFcn', @computeAndPlot);
p1Field.Layout.Row = 6;
p1Field.Layout.Column = 2;

lbl = uilabel(leftGrid, 'Text', 'Initial Pdead');
lbl.Layout.Row = 7;
lbl.Layout.Column = 1;

pdeadField = uieditfield(leftGrid, 'numeric', ...
    'Value', 0, ...
    'RoundFractionalValues', 'on', ...
    'Limits', [0 Inf], ...
    'ValueChangedFcn', @computeAndPlot);
pdeadField.Layout.Row = 7;
pdeadField.Layout.Column = 2;

stateTable = uitable(leftGrid);
stateTable.Layout.Row = 8;
stateTable.Layout.Column = [1 2];

statusLabel = uilabel(leftGrid, 'Text', 'Ready.', 'FontAngle', 'italic');
statusLabel.Layout.Row = 9;
statusLabel.Layout.Column = [1 2];

computeButton = uibutton(leftGrid, 'Text', 'Recompute', ...
    'ButtonPushedFcn', @computeAndPlot);
computeButton.Layout.Row = 10;
computeButton.Layout.Column = [1 2];

ax = uiaxes(rightPanel);
ax.Position = [20 20 760 620];
axis(ax, 'off');

computeAndPlot();

    function computeAndPlot(~, ~)
        m0 = [round(p0Field.Value); round(p1Field.Value); round(pdeadField.Value)];

        if any(~isfinite(m0)) || any(m0 < 0)
            statusLabel.Text = 'Initial marking must be finite and nonnegative.';
            return;
        end

        mode = string(modeDropDown.Value);
        [pre, post, transitionNames, netDescription] = getNet(mode);

        [states, sourceIdx, targetIdx, edgeLabels] = computeReachability(pre, post, m0, transitionNames);

        enabledText = strings(size(states, 1), 1);
        deadlockText = strings(size(states, 1), 1);

        for k = 1:size(states, 1)
            enabledMask = getEnabledTransitions(states(k, :).', pre);
            if any(enabledMask)
                enabledText(k) = strjoin(transitionNames(enabledMask), ', ');
                deadlockText(k) = "No";
            else
                enabledText(k) = "none";
                deadlockText(k) = "Yes";
            end
        end

        stateNames = "M" + string((1:size(states, 1)).');
        stateTable.Data = table(stateNames, states(:,1), states(:,2), states(:,3), enabledText, deadlockText, ...
            'VariableNames', {'State', 'P0', 'P1', 'Pdead', 'EnabledTransitions', 'Deadlock'});

        cla(ax);

        G = digraph(sourceIdx, targetIdx, [], size(states, 1));

        nodeLabels = arrayfun(@(k) sprintf('[%d %d %d]', states(k,1), states(k,2), states(k,3)), ...
            1:size(states, 1), 'UniformOutput', false);

        h = plot(ax, G, 'Layout', 'layered', 'NodeLabel', nodeLabels);
        h.MarkerSize = 8;
        h.NodeColor = [0.2 0.5 0.8];
        h.LineWidth = 1.5;

        if ~isempty(edgeLabels)
            h.EdgeLabel = cellstr(edgeLabels);
        end

        initialNode = 1;
        deadlockNodes = find(strcmp(deadlockText, "Yes"));

        highlight(h, initialNode, 'NodeColor', [0.85 0.3 0.3], 'MarkerSize', 9);
        if ~isempty(deadlockNodes)
            highlight(h, deadlockNodes, 'NodeColor', [0.9 0.2 0.2], 'MarkerSize', 9);
        end

        title(ax, "Reachability Graph: " + mode);
        statusLabel.Text = sprintf('%s | Reachable markings: %d | Deadlocks: %d', ...
            netDescription, size(states, 1), numel(deadlockNodes));
    end
end

function [pre, post, transitionNames, netDescription] = getNet(mode)
switch mode
    case "Deadlock-prone"
        pre = [1 0;
               0 1;
               0 0];
        post = [0 0;
                1 0;
                0 1];
        transitionNames = ["T1", "T2"];
        netDescription = "Deadlock-prone net";
    otherwise
        pre = [1 0 0;
               0 1 0;
               0 0 1];
        post = [0 0 1;
                1 0 0;
                0 1 0];
        transitionNames = ["T1", "T2", "T3"];
        netDescription = "Fixed net with recovery";
end
end

function [states, sourceIdx, targetIdx, edgeLabels] = computeReachability(pre, post, m0, transitionNames)
states = m0(:).';
sourceIdx = [];
targetIdx = [];
edgeLabels = strings(0, 1);

visited = containers.Map('KeyType', 'char', 'ValueType', 'double');
queue = {m0(:)};
head = 1;

visited(markingKey(m0(:))) = 1;

while head <= numel(queue)
    m = queue{head};
    head = head + 1;

    i = visited(markingKey(m));

    enabledMask = getEnabledTransitions(m, pre);

    for t = 1:size(pre, 2)
        if enabledMask(t)
            mNext = m - pre(:, t) + post(:, t);
            keyNext = markingKey(mNext);

            if isKey(visited, keyNext)
                j = visited(keyNext);
            else
                states(end+1, :) = mNext.'; %#ok<AGROW>
                j = size(states, 1);
                visited(keyNext) = j;
                queue{end+1} = mNext; %#ok<AGROW>
            end

            sourceIdx(end+1, 1) = i; %#ok<AGROW>
            targetIdx(end+1, 1) = j; %#ok<AGROW>
            edgeLabels(end+1, 1) = transitionNames(t); %#ok<AGROW>
        end
    end
end
end

function enabledMask = getEnabledTransitions(m, pre)
enabledMask = false(1, size(pre, 2));
for t = 1:size(pre, 2)
    enabledMask(t) = all(m >= pre(:, t));
end
end

function key = markingKey(m)
key = sprintf('%d_', m(:));
end