# Independent structural reference for the Gimmer open-net essai.
# Run with Julia and AlgebraicPetri.jl + Catlab.jl. The browser does not run Julia.
using Test
using AlgebraicPetri
using Catlab
using Catlab.CategoricalAlgebra
using Catlab.Programs.RelationalPrograms

# Each reusable method fragment takes one lift token, returns it, and produces
# one distinct installed-work token. Open exposes both places as ports.
frame = Open(PetriNet(2, 1 => (1, 2)))
roof  = Open(PetriNet(2, 1 => (1, 2)))
methods = Dict(:frame => frame, :roof => roof)

# One junction identifies the two lift ports. Distinct completion places remain.
shared_pattern = @relation () begin
  frame(lift, frame_done)
  roof(lift, roof_done)
end
shared = apex(oapply(shared_pattern, methods))

# Separate lift junctions retain separately owned resources.
separate_pattern = @relation () begin
  frame(frame_lift, frame_done)
  roof(roof_lift, roof_done)
end
separate = apex(oapply(separate_pattern, methods))

@testset "AlgebraicPetri open-net structural reference" begin
  @test ns(shared) == 3       # one lift plus frame/roof completion
  @test ns(separate) == 4     # two lifts plus frame/roof completion
  @test nt(shared) == nt(separate) == 2
  @test ni(shared) == ni(separate) == 2
  @test no(shared) == no(separate) == 4
end

# Read the incidence of the package-assembled net. This is an ordinary
# multiset-firing check written here, not a claim that AlgebraicPetri chooses a
# project's marking or once-only selected occurrence semantics.
function fire_once(net, marking, transition)
  required = zeros(Int, ns(net))
  produced = zeros(Int, ns(net))
  for arc in 1:ni(net)
    if net[arc, :it] == transition
      required[net[arc, :is]] += 1
    end
  end
  for arc in 1:no(net)
    if net[arc, :ot] == transition
      produced[net[arc, :os]] += 1
    end
  end
  all(marking .>= required) || return nothing
  marking .- required .+ produced
end

# The shared lift is the only place consumed by both transitions. With one
# token there, the same package transition can fire twice, accumulating two
# frame-completion tokens. Our selected-work contract disallows the second use
# because Frame identifies one chosen occurrence. Open-net gluing alone does
# not carry that policy.
lift_species = only([s for s in 1:ns(shared)
  if count(==(s), shared[:is]) == 2 && count(==(s), shared[:os]) == 2])
initial = zeros(Int, ns(shared))
initial[lift_species] = 1
after_one = fire_once(shared, initial, 1)
after_two = fire_once(shared, after_one, 1)
@testset "repeated firing is an extra planning-semantics boundary" begin
  @test after_one !== nothing
  @test after_two !== nothing
  @test after_two[lift_species] == 1
  @test sum(after_two) == 3
end

println("OPEN_NET_REFERENCE shared=(places=$(ns(shared)), events=$(nt(shared)), inputs=$(ni(shared)), outputs=$(no(shared))) separate=(places=$(ns(separate)), events=$(nt(separate)), inputs=$(ni(separate)), outputs=$(no(separate)))")
println("Structural gluing only: no initial marking, once-only occurrence policy, joint-step or schedule claim is established by these checks.")
println("Ordinary incidence admits a repeated Frame firing under the chosen marking; the once-only project-work contract rejects that second use.")