1 %%%%%%%%%%%%%%%%%
   2 % Preprocessing %
   3 %%%%%%%%%%%%%%%%%
   4 
   5 sign(m). sign(p).
   6 
   7 diff(V,V)  :- edge(V,V), obs_elabel(V,V,m), not obs_elabel(V,V, p).
   8 diff(U,V)  :- edge(U,V), obs_elabel(U,V,m), not obs_elabel(U,V, p), obs_vlabel(U,S), obs_vlabel(V,S).
   9 diff(U,V)  :- edge(U,V), obs_elabel(U,V, p), not obs_elabel(U,V,m), obs_vlabel(U,S), obs_vlabel(V,T), S != T.
  10 
  11 nontriv(V) :- vertex(V), not input(V), edge(U,V), not diff(U,V).
  12 trivial(V) :- vertex(V), not input(V), not nontriv(V).
  13 
  14 btedge(W,U,V) :- vertex(V), not input(V), not trivial(V), edge(W,V), edge(U,V), edge(Z,V), W < Z, Z < U.
  15 ntedge(W,U,V) :- vertex(V), not input(V), not trivial(V), edge(W,V), edge(U,V), W < U, not btedge(W,U,V).
  16 nfirst(U,V)   :- ntedge(W,U,V).
  17 nlast(W,V)    :- ntedge(W,U,V).
  18 first(U,V)    :- vertex(V), not input(V), not trivial(V), edge(U,V), not nfirst(U,V).
  19 last(U,V)     :- vertex(V), not input(V), not trivial(V), edge(U,V), not nlast(U,V).
  20 
  21 
  22 %%%%%%%%%%%%%
  23 % Generator %
  24 %%%%%%%%%%%%%
  25 
  26 active(V) | inactive(V) :- vertex(V), not input(V).
  27 inactive(V)             :- vertex(V), not input(V), active(W), trivial(W), V != W.
  28 singleton               :- active(V), trivial(V).
  29 
  30 reach(U,V) :- edge(U,V), active(V), not trivial(V).
  31 reach(V,U) :- edge(U,V), active(V), not trivial(V),                        not obs_vlabel(U,p), not obs_vlabel(U,m).
  32 reach(U,W) :- edge(U,V), active(V), not trivial(V), reach(V,W), vertex(W).
  33 reach(V,W) :- edge(U,V), active(V), not trivial(V), reach(U,W), vertex(W), not obs_vlabel(U,p), not obs_vlabel(U,m).
  34 
  35 aedge(V) :- vertex(V), not input(V), not trivial(V), not obs_vlabel(V,p), not obs_vlabel(V,m), active(W), edge(V,W).
  36 
  37 :- active(V), not trivial(V), active(W), not trivial(W), not reach(V,W).
  38 :- active(V), not trivial(V), not obs_vlabel(V,p), not obs_vlabel(V,m), not aedge(V).
  39 
  40 
  41 %%%%%%%%%%%%%%%%%%%%%%
  42 % Inconsistency Test %
  43 %%%%%%%%%%%%%%%%%%%%%%
  44 
  45 vlabel(V,p)   | vlabel(V,m)   :- active(V),    not trivial(V),               not obs_vlabel(V,p),   not obs_vlabel(V,m).
  46 vlabel(U,p)   | vlabel(U,m)   :- active(V),    not trivial(V), edge(U,V),    not obs_vlabel(U,p),   not obs_vlabel(U,m).
  47 llabel(U,V,p) | llabel(U,V,m) :- active(V),    not trivial(V), edge(U,V),    not obs_elabel(U,V,p), not obs_elabel(U,V,m).
  48 
  49 vlabel(V,S)   :- vertex(V), obs_vlabel(V,S),   not trivial(V), not input(V).
  50 vlabel(U,S)   :- edge(U,V), obs_vlabel(U,S),   not trivial(V), not input(V).
  51 llabel(U,V,S) :- edge(U,V), obs_elabel(U,V,S), not trivial(V), not input(V).
  52 
  53 oppo(U,V)     :- llabel(U,V,m), vlabel(U,S),   not trivial(V), not input(V), not obs_elabel(U,V,p), active(V), vlabel(V,S).
  54 oppo(U,V)     :- llabel(U,V,p), vlabel(U,S),   not trivial(V), not input(V), not obs_elabel(U,V,m), active(V), vlabel(V,T), S != T.
  55 
  56 coppo(U,V)    :- oppo(U,V), first(U,V).
  57 coppo(U,V)    :- oppo(U,V), coppo(W,V), ntedge(W,U,V).
  58 
  59 bot           :- singleton.
  60 bot           :- active(V), coppo(U,V), last(U,V).
  61 
  62 vlabel(V,S)   :- bot, vertex(V), sign(S),      not trivial(V), not input(V), not obs_vlabel(V,p),   not obs_vlabel(V,m).
  63 vlabel(U,S)   :- bot, edge(U,V), sign(S),      not trivial(V), not input(V), not obs_vlabel(U,p),   not obs_vlabel(U,m).
  64 llabel(U,V,S) :- bot, edge(U,V), sign(S),      not trivial(V), not input(V), not obs_elabel(U,V,p), not obs_elabel(U,V,m).
  65 
  66 :- not bot.
  67 
  68 
  69 %%%%%%%%%%%%%%%%%%%
  70 % Minimality Test %
  71 %%%%%%%%%%%%%%%%%%%
  72 
  73 mvlabel(W,V,p)   | mvlabel(W,V,m)   :-                active(W), not trivial(V), not trivial(W), active(V), reach(V,W), reach(W,V), W != V.
  74 mvlabel(W,U,p)   | mvlabel(W,U,m)   :- edge(U,V),     active(W), not trivial(V), not trivial(W), active(V), reach(V,W), reach(W,V), W != V.
  75 mllabel(W,U,V,p) | mllabel(W,U,V,m) :- edge(U,V),     active(W), not trivial(V), not trivial(W), active(V), reach(V,W), reach(W,V), W != V.
  76 
  77 mvlabel(W,V,S)   :- obs_vlabel(V,S),                  vertex(W), not trivial(V), not trivial(W), not input(V), not input(W),        W != V.
  78 mvlabel(W,U,S)   :- obs_vlabel(U,S),    edge(U,V),    vertex(W), not trivial(V), not trivial(W), not input(V), not input(W),        W != V.
  79 mllabel(W,U,V,S) :- obs_elabel(U,V,S),  edge(U,V),    vertex(W), not trivial(V), not trivial(W), not input(V), not input(W),        W != V.
  80 
  81 minfl(W,V,p)     :- mvlabel(W,U,S), mllabel(W,U,V,S), active(W), not trivial(V), not trivial(W), active(V), reach(V,W), reach(W,V), W != V.
  82 minfl(W,V,m)     :- mvlabel(W,U,S), mllabel(W,U,V,T), active(W), not trivial(V), not trivial(W), active(V), reach(V,W), reach(W,V), W != V, S != T.
  83 
  84 :- active(V), active(W), not trivial(V), not trivial(W), W != V, mvlabel(W,V,S), not minfl(W,V,S).
  85 
  86 
  87 %%%%%%%%%%
  88 % Output %
  89 %%%%%%%%%%
  90 
  91 % #hide.
  92 % #show active(V).