function petriDeadlockGui
% petriDeadlockGui GUI for illustrating deadlock 
% in a simple Petri net.
%
% Net:
%   P0 --T1--> P1 --T2--> Pdead
%
% The marking [0 0 1] is a deadlock state 
% because no transitions are enabled.

% Places: P0, P1, Pdead
% Transitions: T1, T2
pre = [1 0;
       0 1;
       0 0];

post = [0 0;
        1 0;
        0 1];

transitionNames = ["T1", "T2"];

fig = uifigure('Name', 'Petri Net Deadlock', 'Position', [100 100 1120 660]);

mainGrid = uigridlayout(fig, [1 2]);
mainGrid.ColumnWidth = {360, '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, 28, 34, '1x', 24};
leftGrid.ColumnWidth = {140, '1x'};

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

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

lbl = uilabel(leftGrid, 'Text', 'P1 --T2--> Pdead');
lbl.Layout.Row = 3;
lbl.Layout.Column = [1 2];

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

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

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

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

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

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

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

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

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

ax = uiaxes(rightPanel);
ax.Position = [20 20 720 600];
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

        [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');
        statusLabel.Text = sprintf('Found %d reachable markings. Deadlock markings are shown in red.', ...
            size(states, 1));
    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