fix(validators): scope bound_vars per-transition in arc_validator (audit #3) (#78)

Author: fahchen

lib/coloured_flow/validators/definition/arc_validator.ex

@@ -13,17 +13,19 @@ defmodule ColouredFlow.Validators.Definition.ArcValidator do
   alias ColouredFlow.Definition.Arc
   alias ColouredFlow.Definition.ColouredPetriNet
   alias ColouredFlow.Definition.Transition
+  alias ColouredFlow.Definition.Variable
   alias ColouredFlow.Validators.Exceptions.InvalidArcError
 
   @spec validate(ColouredPetriNet.t()) ::
           {:ok, ColouredPetriNet.t()} | {:error, InvalidArcError.t()}
   def validate(%ColouredPetriNet{} = cpnet) do
     vars_and_consts = build_vars_and_consts(cpnet)
     outputs = build_outputs(cpnet)
+    bound_vars_by_transition = build_bound_vars_by_transition(cpnet)
 
     cpnet.arcs
     |> Enum.find_value(fn %Arc{} = arc ->
-      case validate_arc(arc, vars_and_consts, outputs, cpnet) do
+      case validate_arc(arc, vars_and_consts, outputs, bound_vars_by_transition) do
         :ok -> nil
         {:error, reason} -> reason
       end
@@ -38,7 +40,7 @@ defmodule ColouredFlow.Validators.Definition.ArcValidator do
          %Arc{orientation: :p_to_t} = arc,
          {vars, consts},
          _outputs,
-         %ColouredPetriNet{}
+         _bound_vars_by_transition
        ) do
     arc.expression.vars
     |> MapSet.new()
@@ -71,20 +73,14 @@ defmodule ColouredFlow.Validators.Definition.ArcValidator do
          %Arc{orientation: :t_to_p} = arc,
          {_vars, consts},
          outputs,
-         %ColouredPetriNet{} = cpnet
+         bound_vars_by_transition
        ) do
-    bound_vars =
-      cpnet.arcs
-      |> Enum.flat_map(fn
-        %Arc{orientation: :p_to_t} = arc -> arc.expression.vars
-        %Arc{} -> []
-      end)
-      |> MapSet.new()
+    bound_vars = Map.get(bound_vars_by_transition, arc.transition, MapSet.new())
 
     vars_and_consts =
       bound_vars
       |> MapSet.union(consts)
-      |> MapSet.union(Map.get(outputs, arc.transition, []))
+      |> MapSet.union(Map.get(outputs, arc.transition, MapSet.new()))
 
     arc.expression.vars
     |> MapSet.new()
@@ -124,4 +120,15 @@ defmodule ColouredFlow.Validators.Definition.ArcValidator do
       {transition.name, MapSet.new(transition.action.outputs)}
     end)
   end
+
+  @spec build_bound_vars_by_transition(ColouredPetriNet.t()) ::
+          %{Transition.name() => MapSet.t(Variable.name())}
+  defp build_bound_vars_by_transition(%ColouredPetriNet{arcs: arcs}) do
+    arcs
+    |> Stream.filter(&(&1.orientation == :p_to_t))
+    |> Enum.group_by(& &1.transition, & &1.expression.vars)
+    |> Map.new(fn {transition, vars_lists} ->
+      {transition, vars_lists |> List.flatten() |> MapSet.new()}
+    end)
+  end
 end

test/coloured_flow/validators/definition/arc_validator_test.exs

@@ -119,6 +119,72 @@ defmodule ColouredFlow.Validators.Definition.ArcValidatorTest do
              ArcValidator.validate(cpnet)
   end
 
+  test "outgoing_unbound_vars error when var is bound on a different transition" do
+    # Two transitions T1 and T2, each with their own input/output places.
+    # T1 has an incoming arc binding `x`.
+    # T2 has an outgoing arc referencing `x`, but T2's incoming arc only binds `y`.
+    # In CPN semantics, variables bind only within a single transition's firing,
+    # so T2's outgoing arc must NOT see `x` from T1.
+    cpnet = %ColouredPetriNet{
+      colour_sets: [
+        colset(int() :: integer())
+      ],
+      places: [
+        %Place{name: "p1_in", colour_set: :int},
+        %Place{name: "p1_out", colour_set: :int},
+        %Place{name: "p2_in", colour_set: :int},
+        %Place{name: "p2_out", colour_set: :int}
+      ],
+      transitions: [
+        build_transition!(name: "t1", guard: "true"),
+        build_transition!(name: "t2", guard: "true")
+      ],
+      arcs: [
+        # T1 binds `x` on its incoming arc.
+        build_arc!(
+          label: "t1-in",
+          place: "p1_in",
+          transition: "t1",
+          orientation: :p_to_t,
+          expression: "bind {1, x}"
+        ),
+        build_arc!(
+          label: "t1-out",
+          place: "p1_out",
+          transition: "t1",
+          orientation: :t_to_p,
+          expression: "{1, x}"
+        ),
+        # T2 binds only `y` — no `x` is in scope here.
+        build_arc!(
+          label: "t2-in",
+          place: "p2_in",
+          transition: "t2",
+          orientation: :p_to_t,
+          expression: "bind {1, y}"
+        ),
+        # This outgoing arc references `x`, which was bound on a *different*
+        # transition. Pre-fix, the validator pooled bound vars across all
+        # transitions and silently accepted this; post-fix, it must reject.
+        build_arc!(
+          label: "t2-out",
+          place: "p2_out",
+          transition: "t2",
+          orientation: :t_to_p,
+          expression: "{1, x}"
+        )
+      ],
+      variables: [
+        %Variable{name: :x, colour_set: :int},
+        %Variable{name: :y, colour_set: :int}
+      ],
+      constants: []
+    }
+
+    assert {:error, %InvalidArcError{reason: :outgoing_unbound_vars}} =
+             ArcValidator.validate(cpnet)
+  end
+
   defp update_action(%ColouredPetriNet{} = cpnet, %Action{} = action) do
     put_in(
       cpnet,