346 lines
12 KiB
Plaintext
346 lines
12 KiB
Plaintext
|
// Petri Net Reachability - Full Type-Theoretic Encoding
|
||
|
|
//
|
||
|
|
// This showcase demonstrates geolog's core capabilities through a
|
||
|
|
// non-trivial domain: encoding Petri net reachability as dependent types.
|
||
|
|
//
|
||
|
|
// A solution to a reachability problem is NOT a yes/no boolean but a
|
||
|
|
// CONSTRUCTIVE WITNESS: a diagrammatic proof that tokens can flow from
|
||
|
|
// initial to target markings via a sequence of transition firings.
|
||
|
|
//
|
||
|
|
// Key concepts demonstrated:
|
||
|
|
// - Parameterized theories (Marking depends on PetriNet instance)
|
||
|
|
// - Nested instance types (ReachabilityProblem contains Marking instances)
|
||
|
|
// - Sort-parameterized theories (Iso takes two sorts as parameters)
|
||
|
|
// - Cross-instance references (solution's trace elements reference problem's tokens)
|
||
|
|
//
|
||
|
|
// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY: PetriNet
|
||
|
|
// Places, transitions, and arcs with proper arc semantics
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
theory PetriNet {
|
||
|
|
P : Sort; // Places
|
||
|
|
T : Sort; // Transitions
|
||
|
|
in : Sort; // Input arcs (place -> transition)
|
||
|
|
out : Sort; // Output arcs (transition -> place)
|
||
|
|
|
||
|
|
in/src : in -> P; // Input arc source place
|
||
|
|
in/tgt : in -> T; // Input arc target transition
|
||
|
|
out/src : out -> T; // Output arc source transition
|
||
|
|
out/tgt : out -> P; // Output arc target place
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY: Marking (parameterized by N : PetriNet)
|
||
|
|
// A marking assigns tokens to places
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
theory (N : PetriNet instance) Marking {
|
||
|
|
token : Sort;
|
||
|
|
token/of : token -> N/P;
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY: ReachabilityProblem (parameterized by N : PetriNet)
|
||
|
|
// Initial and target markings as nested instances
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
theory (N : PetriNet instance) ReachabilityProblem {
|
||
|
|
initial_marking : N Marking instance;
|
||
|
|
target_marking : N Marking instance;
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY: Trace (parameterized by N : PetriNet)
|
||
|
|
// A trace records transition firings and token flow via wires
|
||
|
|
// ============================================================
|
||
|
|
//
|
||
|
|
// A trace is a diagrammatic proof of reachability:
|
||
|
|
// - Firings represent transition occurrences
|
||
|
|
// - Wires connect output arcs of firings to input arcs of other firings
|
||
|
|
// - Terminals connect to the initial/target markings
|
||
|
|
//
|
||
|
|
// The completeness axiom (ax/must_be_fed) ensures every input arc
|
||
|
|
// of every firing is accounted for - either wired from another firing
|
||
|
|
// or fed by an input terminal.
|
||
|
|
|
||
|
|
theory (N : PetriNet instance) Trace {
|
||
|
|
// Firings
|
||
|
|
F : Sort;
|
||
|
|
F/of : F -> N/T;
|
||
|
|
|
||
|
|
// Wires connect output arcs of firings to input arcs of other firings
|
||
|
|
W : Sort;
|
||
|
|
W/src_firing : W -> F;
|
||
|
|
W/src_arc : W -> N/out;
|
||
|
|
W/tgt_firing : W -> F;
|
||
|
|
W/tgt_arc : W -> N/in;
|
||
|
|
|
||
|
|
// Wire coherence: source arc must belong to source firing's transition
|
||
|
|
ax/wire_src_coherent : forall w : W.
|
||
|
|
|- w W/src_arc N/out/src = w W/src_firing F/of;
|
||
|
|
|
||
|
|
// Wire coherence: target arc must belong to target firing's transition
|
||
|
|
ax/wire_tgt_coherent : forall w : W.
|
||
|
|
|- w W/tgt_arc N/in/tgt = w W/tgt_firing F/of;
|
||
|
|
|
||
|
|
// Wire place coherence: wire connects matching places
|
||
|
|
ax/wire_place_coherent : forall w : W.
|
||
|
|
|- w W/src_arc N/out/tgt = w W/tgt_arc N/in/src;
|
||
|
|
|
||
|
|
// Terminals
|
||
|
|
input_terminal : Sort;
|
||
|
|
output_terminal : Sort;
|
||
|
|
input_terminal/of : input_terminal -> N/P;
|
||
|
|
output_terminal/of : output_terminal -> N/P;
|
||
|
|
|
||
|
|
// Terminals connect to specific firings and arcs
|
||
|
|
input_terminal/tgt_firing : input_terminal -> F;
|
||
|
|
input_terminal/tgt_arc : input_terminal -> N/in;
|
||
|
|
output_terminal/src_firing : output_terminal -> F;
|
||
|
|
output_terminal/src_arc : output_terminal -> N/out;
|
||
|
|
|
||
|
|
// Terminal coherence axioms
|
||
|
|
ax/input_terminal_coherent : forall i : input_terminal.
|
||
|
|
|- i input_terminal/tgt_arc N/in/tgt = i input_terminal/tgt_firing F/of;
|
||
|
|
|
||
|
|
ax/output_terminal_coherent : forall o : output_terminal.
|
||
|
|
|- o output_terminal/src_arc N/out/src = o output_terminal/src_firing F/of;
|
||
|
|
|
||
|
|
// Terminal place coherence
|
||
|
|
ax/input_terminal_place : forall i : input_terminal.
|
||
|
|
|- i input_terminal/of = i input_terminal/tgt_arc N/in/src;
|
||
|
|
|
||
|
|
ax/output_terminal_place : forall o : output_terminal.
|
||
|
|
|- o output_terminal/of = o output_terminal/src_arc N/out/tgt;
|
||
|
|
|
||
|
|
// COMPLETENESS: Every arc of every firing must be accounted for.
|
||
|
|
|
||
|
|
// Input completeness: every input arc must be fed by a wire or input terminal
|
||
|
|
ax/input_complete : forall f : F, arc : N/in.
|
||
|
|
arc N/in/tgt = f F/of |-
|
||
|
|
(exists w : W. w W/tgt_firing = f, w W/tgt_arc = arc) \/
|
||
|
|
(exists i : input_terminal. i input_terminal/tgt_firing = f, i input_terminal/tgt_arc = arc);
|
||
|
|
|
||
|
|
// Output completeness: every output arc must be captured by a wire or output terminal
|
||
|
|
ax/output_complete : forall f : F, arc : N/out.
|
||
|
|
arc N/out/src = f F/of |-
|
||
|
|
(exists w : W. w W/src_firing = f, w W/src_arc = arc) \/
|
||
|
|
(exists o : output_terminal. o output_terminal/src_firing = f, o output_terminal/src_arc = arc);
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY: Iso (parameterized by two sorts)
|
||
|
|
// Isomorphism (bijection) between two sorts
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
theory (X : Sort) (Y : Sort) Iso {
|
||
|
|
fwd : X -> Y;
|
||
|
|
bwd : Y -> X;
|
||
|
|
|
||
|
|
// Roundtrip axioms ensure this is a true bijection
|
||
|
|
fb : forall x : X. |- x fwd bwd = x;
|
||
|
|
bf : forall y : Y. |- y bwd fwd = y;
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// THEORY: Solution (parameterized by N and RP)
|
||
|
|
// A constructive witness that target is reachable from initial
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution {
|
||
|
|
trace : N Trace instance;
|
||
|
|
|
||
|
|
// Bijection: input terminals <-> initial marking tokens
|
||
|
|
initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance;
|
||
|
|
|
||
|
|
// Bijection: output terminals <-> target marking tokens
|
||
|
|
target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance;
|
||
|
|
|
||
|
|
// Commutativity axioms (currently unchecked):
|
||
|
|
// ax/init_comm : forall i : trace/input_terminal.
|
||
|
|
// |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of;
|
||
|
|
// ax/target_comm : forall o : trace/output_terminal.
|
||
|
|
// |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of;
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// INSTANCE: ExampleNet
|
||
|
|
//
|
||
|
|
// A Petri net with places A, B, C and transitions:
|
||
|
|
// ab: consumes 1 token from A, produces 1 token in B
|
||
|
|
// ba: consumes 1 token from B, produces 1 token in A
|
||
|
|
// abc: consumes 1 token from A AND 1 from B, produces 1 token in C
|
||
|
|
//
|
||
|
|
// +---[ba]----+
|
||
|
|
// v |
|
||
|
|
// (A) --[ab]->(B) --+
|
||
|
|
// | |
|
||
|
|
// +----[abc]-------+--> (C)
|
||
|
|
//
|
||
|
|
// The abc transition is interesting: it requires BOTH an A-token
|
||
|
|
// and a B-token to fire, producing a C-token.
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
instance ExampleNet : PetriNet = {
|
||
|
|
A : P; B : P; C : P;
|
||
|
|
ab : T; ba : T; abc : T;
|
||
|
|
|
||
|
|
// A -> B (via ab)
|
||
|
|
ab_in : in; ab_in in/src = A; ab_in in/tgt = ab;
|
||
|
|
ab_out : out; ab_out out/src = ab; ab_out out/tgt = B;
|
||
|
|
|
||
|
|
// B -> A (via ba)
|
||
|
|
ba_in : in; ba_in in/src = B; ba_in in/tgt = ba;
|
||
|
|
ba_out : out; ba_out out/src = ba; ba_out out/tgt = A;
|
||
|
|
|
||
|
|
// A + B -> C (via abc) - note: two input arcs!
|
||
|
|
abc_in1 : in; abc_in1 in/src = A; abc_in1 in/tgt = abc;
|
||
|
|
abc_in2 : in; abc_in2 in/src = B; abc_in2 in/tgt = abc;
|
||
|
|
abc_out : out; abc_out out/src = abc; abc_out out/tgt = C;
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// PROBLEM 0: Can we reach B from A with one token?
|
||
|
|
// Initial: 1 token in A
|
||
|
|
// Target: 1 token in B
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
instance problem0 : ExampleNet ReachabilityProblem = {
|
||
|
|
initial_marking = {
|
||
|
|
tok : token;
|
||
|
|
tok token/of = ExampleNet/A;
|
||
|
|
};
|
||
|
|
target_marking = {
|
||
|
|
tok : token;
|
||
|
|
tok token/of = ExampleNet/B;
|
||
|
|
};
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// SOLUTION 0: Yes! Fire transition 'ab' once.
|
||
|
|
//
|
||
|
|
// This Solution instance is a CONSTRUCTIVE PROOF:
|
||
|
|
// - The trace contains one firing (f1) of transition 'ab'
|
||
|
|
// - The input terminal feeds the A-token into f1's input arc
|
||
|
|
// - The output terminal captures f1's B-token output
|
||
|
|
// - The isomorphisms prove the token counts match exactly
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
instance solution0 : ExampleNet problem0 Solution = {
|
||
|
|
trace = {
|
||
|
|
// One firing of transition 'ab'
|
||
|
|
f1 : F;
|
||
|
|
f1 F/of = ExampleNet/ab;
|
||
|
|
|
||
|
|
// Input terminal: feeds the initial A-token into f1
|
||
|
|
it : input_terminal;
|
||
|
|
it input_terminal/of = ExampleNet/A;
|
||
|
|
it input_terminal/tgt_firing = f1;
|
||
|
|
it input_terminal/tgt_arc = ExampleNet/ab_in;
|
||
|
|
|
||
|
|
// Output terminal: captures f1's B-token output
|
||
|
|
ot : output_terminal;
|
||
|
|
ot output_terminal/of = ExampleNet/B;
|
||
|
|
ot output_terminal/src_firing = f1;
|
||
|
|
ot output_terminal/src_arc = ExampleNet/ab_out;
|
||
|
|
};
|
||
|
|
|
||
|
|
initial_iso = {
|
||
|
|
trace/it fwd = problem0/initial_marking/tok;
|
||
|
|
problem0/initial_marking/tok bwd = trace/it;
|
||
|
|
};
|
||
|
|
|
||
|
|
target_iso = {
|
||
|
|
trace/ot fwd = problem0/target_marking/tok;
|
||
|
|
problem0/target_marking/tok bwd = trace/ot;
|
||
|
|
};
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// PROBLEM 2: Can we reach C from two A-tokens?
|
||
|
|
// Initial: 2 tokens in A
|
||
|
|
// Target: 1 token in C
|
||
|
|
//
|
||
|
|
// This is interesting because the only path to C is via 'abc',
|
||
|
|
// which requires tokens in BOTH A and B simultaneously.
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
instance problem2 : ExampleNet ReachabilityProblem = {
|
||
|
|
initial_marking = {
|
||
|
|
t1 : token; t1 token/of = ExampleNet/A;
|
||
|
|
t2 : token; t2 token/of = ExampleNet/A;
|
||
|
|
};
|
||
|
|
target_marking = {
|
||
|
|
t : token;
|
||
|
|
t token/of = ExampleNet/C;
|
||
|
|
};
|
||
|
|
}
|
||
|
|
|
||
|
|
// ============================================================
|
||
|
|
// SOLUTION 2: Yes! Fire 'ab' then 'abc'.
|
||
|
|
//
|
||
|
|
// Token flow diagram:
|
||
|
|
//
|
||
|
|
// [it1]--A-->[f1: ab]--B--wire-->[f2: abc]--C-->[ot]
|
||
|
|
// [it2]--A-----------------^
|
||
|
|
//
|
||
|
|
// Step 1: Fire 'ab' to move one token A -> B
|
||
|
|
// - it1 feeds A-token into f1 via ab_in
|
||
|
|
// - f1 produces B-token via ab_out
|
||
|
|
// Step 2: Fire 'abc' consuming one A-token and one B-token
|
||
|
|
// - it2 feeds A-token into f2 via abc_in1
|
||
|
|
// - Wire connects f1's ab_out to f2's abc_in2 (the B-input)
|
||
|
|
// - f2 produces C-token via abc_out
|
||
|
|
// ============================================================
|
||
|
|
|
||
|
|
instance solution2 : ExampleNet problem2 Solution = {
|
||
|
|
trace = {
|
||
|
|
// Two firings
|
||
|
|
f1 : F; f1 F/of = ExampleNet/ab; // First: A -> B
|
||
|
|
f2 : F; f2 F/of = ExampleNet/abc; // Second: A + B -> C
|
||
|
|
|
||
|
|
// Wire connecting f1's B-output to f2's B-input
|
||
|
|
// This is the crucial connection that makes the trace valid!
|
||
|
|
w1 : W;
|
||
|
|
w1 W/src_firing = f1;
|
||
|
|
w1 W/src_arc = ExampleNet/ab_out;
|
||
|
|
w1 W/tgt_firing = f2;
|
||
|
|
w1 W/tgt_arc = ExampleNet/abc_in2;
|
||
|
|
|
||
|
|
// Input terminal 1: feeds first A-token into f1
|
||
|
|
it1 : input_terminal;
|
||
|
|
it1 input_terminal/of = ExampleNet/A;
|
||
|
|
it1 input_terminal/tgt_firing = f1;
|
||
|
|
it1 input_terminal/tgt_arc = ExampleNet/ab_in;
|
||
|
|
|
||
|
|
// Input terminal 2: feeds second A-token into f2
|
||
|
|
it2 : input_terminal;
|
||
|
|
it2 input_terminal/of = ExampleNet/A;
|
||
|
|
it2 input_terminal/tgt_firing = f2;
|
||
|
|
it2 input_terminal/tgt_arc = ExampleNet/abc_in1;
|
||
|
|
|
||
|
|
// Output terminal: captures f2's C-token output
|
||
|
|
ot : output_terminal;
|
||
|
|
ot output_terminal/of = ExampleNet/C;
|
||
|
|
ot output_terminal/src_firing = f2;
|
||
|
|
ot output_terminal/src_arc = ExampleNet/abc_out;
|
||
|
|
};
|
||
|
|
|
||
|
|
// Bijection: 2 input terminals <-> 2 initial tokens
|
||
|
|
initial_iso = {
|
||
|
|
trace/it1 fwd = problem2/initial_marking/t1;
|
||
|
|
trace/it2 fwd = problem2/initial_marking/t2;
|
||
|
|
problem2/initial_marking/t1 bwd = trace/it1;
|
||
|
|
problem2/initial_marking/t2 bwd = trace/it2;
|
||
|
|
};
|
||
|
|
|
||
|
|
// Bijection: 1 output terminal <-> 1 target token
|
||
|
|
target_iso = {
|
||
|
|
trace/ot fwd = problem2/target_marking/t;
|
||
|
|
problem2/target_marking/t bwd = trace/ot;
|
||
|
|
};
|
||
|
|
}
|