WIP: expanding set test

src/elle/explanation.clj

@@ -4,12 +4,16 @@
   structures or text.")
 
 (defprotocol Explanation
-  (->data [ex] "Converts the explanation to a data structure.")
-  (->text [ex] "Converts the explanation to plain text."))
+  (->data [ex]
+          "Converts the explanation to a data structure.")
+  (->text [ex context]
+          "Converts the explanation to plain text. An optional context map
+          provides extra information used in rendering--for instance, short
+          names for transactions."))
 
 (def trivial
   "A trivial explanation which doesn't explain anything. Helpful for stubbing
   out methods."
   (reify Explanation
-    (->data [ex] :just-cuz)
-    (->text [ex] "just cuz")))
+    (->data [ex]      :just-cuz)
+    (->text [ex ctx]  "just cuz")))

src/elle/graph.clj

@@ -124,11 +124,18 @@
     (apply [_ a b]
       (set/union a b))))
 
-(defn ^IEdge edge
+(defn edge
   "Returns the edge between two vertices."
   [^IGraph g a b]
   (.edge g a b))
 
+(defn maybe-edge
+  "Returns the edge between two vertices, or nil if one does not exist."
+  [^IGraph g a b]
+  (let [o (out g a)]
+    (when (and o (.contains o b))
+      (.edge g a b))))
+
 (defn edges
   "A lazy seq of all edges."
   [^IGraph g]
@@ -694,3 +701,43 @@
           ; Keep exploring
           (let [v (first (c/remove seen vs))]
             (recur (conj path v) (assoc seen v (count path)))))))))
+
+(defn total-order?
+  "Returns truthy iff this graph is a total order: every vertex has at most one
+  outbound edge and one inbound edge, exactly one vertex has no inbound edge,
+  and exactly one different vertex has no outbound edge.
+
+  If this graph is a total order, returns {:min min, :max max}, where min and
+  max are the vertices with no inbound and no outbound edges, respectively."
+  [g]
+  (let [res (reduce (fn [[min max :as bounds] v]
+                      (let [in-count (.size (in g v))
+                            out-count (.size (out g v))]
+                        (cond ; Normal vertex
+                              (and (= 1 in-count) (= 1 out-count))
+                              bounds
+
+                              ; Too many edges!
+                              (or (< 1 in-count) (< 1 out-count))
+                              (reduced false)
+
+                              ; Too few edges!
+                              (and (= 0 in-count) (= 0 out-count))
+                              (reduced false)
+
+                              ; This node is a minimum
+                              (= 0 in-count)
+                              (if min
+                                (reduced false) ; Duplicate minimum!
+                                [v max])        ; We found our minimum
+
+                              (= 0 out-count)
+                              (if max
+                                (reduced false)
+                                [min v]))))
+                    [nil nil]
+                    (vertices g))]
+    (if res
+      {:min (first res)
+       :max (second res)}
+      false)))

src/elle/infer/cyclic.clj

@@ -0,0 +1,38 @@
+(ns elle.infer.cyclic
+  "This namespace infers cyclic anomalies over analyses with transaction
+  graphs--for instance, G1c, G2, G-single, etc."
+  (:require [elle [core :as elle]
+                  [explanation :as expl]
+                  [txn-graph :as tg]
+                  [txn       :as et]]))
+
+(defn anomalies
+  "Returns a map of cyclic anomalies present in an analysis."
+  [analysis]
+  (let [txn-graph       (:txn-graph analysis)
+        pair-explainer  (reify elle/DataExplainer
+                          (explain-pair-data [_ a b]
+                            ; Bit of a hack: explain-pair-data is supposed to
+                            ; return a map, so we're returning a defrecord
+                            ; Explanation, which works as *both* a map and also
+                            ; lets us do our text rendering later.
+                            (assoc (tg/explain txn-graph a b)
+                                   :a a
+                                   :b b))
+
+                          (render-explanation [_ expl a-name b-name]
+                            (expl/->text expl {:txn-names {(:a expl) a-name
+                                                           (:b expl) b-name}})))
+        graph-analyzer (fn [history]
+                         {:graph (tg/graph txn-graph)
+                          :explainer pair-explainer})
+        analyzer (apply elle/combine
+                        (cons graph-analyzer
+                              (et/additional-graphs analysis)))]
+    (et/cycles analysis analyzer (:history analysis))))
+
+(defn add-anomalies
+  "Takes an analysis, and updates its :anomalies field to include any cyclic
+  anomalies found."
+  [analysis]
+  (update analysis :anomalies merge (anomalies analysis)))

src/elle/rw_register.clj

@@ -1,5 +1,5 @@
 (ns elle.rw-register
-  "A test which looks for cycles in write/read transactionss over registers.
+  "A test which looks for cycles in write/read transactions over registers.
   Writes are assumed to be unique, but this is the only constraint.
 
   Operations are of two forms:
@@ -460,7 +460,10 @@
     (reduce (fn [cases [k version-graph]]
               (let [sccs (g/strongly-connected-components version-graph)]
                 (->> sccs
-                     (sort-by (partial reduce min))
+                     (sort-by (partial reduce (fn option-compare [a b]
+                                                (cond (nil? a) b
+                                                      (nil? b) a
+                                                      true     (min a b)))))
                      (map (fn [scc]
                             {:key k
                              :scc scc}))