function petriBoundednessGui
% petriBoundednessGui GUI for illustrating boundedness in a simple Petri net.
%
% Net:
%   Source --Tmove--> Buffer
%   Buffer --Treturn--> Source
%
% Buffer is bounded by a user-defined capacity. When Buffer = capacity,
% the input transition is disabled, preventing overflow.

pre = [1 0;
       0 1];

post = [0 1;
        1 0];

transitionNames = ["Move to buffer", "Return to source"];

fig = uifigure('Name', 'Petri Net Boundedness', 'Position', [100 100 1100 650]);

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, [9 2]);
leftGrid.RowHeight = {22, 22, 22, 28, 28, 28, 34, '1x', 24};
leftGrid.ColumnWidth = {150, '1x'};

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

lbl = uilabel(leftGrid, 'Text', 'Source --Tmove--> Buffer');
lbl.Layout.Row = 2;
lbl.Layout.Column = [1 2];

lbl = uilabel(leftGrid, 'Text', 'Buffer --Treturn--> Source');
lbl.Layout.Row = 3;
lbl.Layout.Column = [1 2];

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

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

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

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

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

capacityField = uieditfield(leftGrid, 'numeric', ...
    'Value', 3, ...
    'RoundFractionalValues', 'on', ...
    'Limits', [0 Inf]);
capacityField.Layout.Row = 6;
capacityField.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 = 9;
statusLabel.Layout.Column = [1 2];

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

computeAndPlot();

    function computeAndPlot(~, ~)
        m0 = [round(sourceField.Value); round(bufferField.Value)];
        capacity = round(capacityField.Value);

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

        if m0(2) > capacity
            statusLabel.Text = 'Initial Buffer cannot exceed capacity.';
            stateTable.Data = table;
            cla(ax);
            axis(ax, 'off');
            return;
        end

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

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

        stateNames = "M" + string((1:size(states, 1)).');
        stateTable.Data = table(stateNames, states(:, 1), states(:, 2), enabledText, ...
            'VariableNames', {'State', 'Source', 'Buffer', 'EnabledTransitions'});

        cla(ax);

        if isempty(sourceIdx)
            G = digraph([], [], [], size(states, 1));
        else
            G = digraph(sourceIdx, targetIdx, [], size(states, 1));
        end

        nodeLabels = arrayfun(@(k) sprintf('[%d %d]', states(k, 1), states(k, 2)), ...
            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

        if numnodes(G) >= 1
            highlight(h, 1, 'NodeColor', [0.85 0.3 0.3], 'MarkerSize', 9);
        end

        title(ax, 'Reachability Graph');
        statusLabel.Text = sprintf('Found %d reachable markings. Overflow is blocked at Buffer = %d.', ...
            size(states, 1), capacity);
    end
end

function [states, sourceIdx, targetIdx, edgeLabels] = computeReachability(pre, post, m0, capacity, 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, capacity);

    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, capacity)
enabledMask = false(1, size(pre, 2));

for t = 1:size(pre, 2)
    if all(m >= pre(:, t))
        if t == 1
            % Tmove adds one token to Buffer, so block it at capacity.
            enabledMask(t) = m(2) < capacity;
        else
            enabledMask(t) = true;
        end
    end
end
end

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