File size: 1,497 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 | % prolog_backend.pl — Topology checker
% Preservation, reachability, floating ports, conduction soundness
:- module(topology_checker, [
check_preservation/1,
check_reachability/3,
check_floating/1,
check_conduction/1
]).
% Preservation: state before → state after (invariant holds)
check_preservation(Kernel) :-
atom(Kernel),
\+ \+ (
state_before(S1),
execute_kernel(Kernel, S1, S2),
state_after(S2),
invariant_holds(S2)
).
% Reachability: can reach goal from start?
check_reachability(Graph, Start, Goal) :-
reachable(Graph, Start, Goal, []).
reachable(_, Goal, Goal, _) :- !.
reachable(Graph, Current, Goal, Visited) :-
edge(Graph, Current, Next),
\+ member(Next, Visited),
reachable(Graph, Next, Goal, [Current|Visited]).
% Floating ports: all ports connected or grounded
check_floating(Circuit) :-
forall(
port(Circuit, Port),
(connected(Port) ; grounded(Port))
).
% Conduction soundness: voltage transitions valid
check_conduction(Levels) :-
forall(
transition(Levels, From, To),
valid_transition(From, To)
).
valid_transition(low, high).
valid_transition(high, low).
valid_transition(X, X).
% Dynamic facts
:- dynamic state_before/1.
:- dynamic state_after/1.
:- dynamic invariant_holds/1.
:- dynamic edge/3.
:- dynamic port/2.
:- dynamic connected/1.
:- dynamic grounded/1.
:- dynamic transition/4.
% Stub implementations
execute_kernel(_, State, State).
|