Trouble in processing some Elle list-append histories

[temeo]

Hi,

While playing with elle-cli, I hit the following error with some histories:

java.lang.IllegalStateException: Explainer
...
was unable to explain the relationship between {:process 1, :type :ok, :f nil, :value [[:append 3 1] [:append 2 4] [:r 4 []]], :index 6} and #knossos.op.Op{:process 0, :type :ok, :f nil, :value [[:r 2 []] [:r 3 []] [:append 4 0]], :index 8}
	at elle.core$explain_cycle_pair_data.invokeStatic(core.clj:402)
	at elle.core$explain_cycle_pair_data.invoke(core.clj:396)
...

One example of such a history is:

{:index 1, :type :invoke, :process 2, :value [[ :append 4 2] [ :append 5 5] ]}
{:index 2, :type :invoke, :process 0, :value [[ :r 2 nil] [ :r 3 nil] [ :append 4 0] ]}
{:index 3, :type :invoke, :process 1, :value [[ :append 3 1] [ :append 2 4] [ :r 4 nil] ]}
{:index 4, :type :ok, :process 2, :value [[ :append 4 2] [ :append 5 5] ]}
{:index 5, :type :invoke, :process 2, :value [[ :append 2 8] ]}
{:index 6, :type :ok, :process 1, :value [[ :append 3 1] [ :append 2 4] [ :r 4 [ ]] ]}
{:index 7, :type :invoke, :process 1, :value [[ :append 3 7] [ :append 4 10] ]}
{:index 8, :type :ok, :process 0, :value [[ :r 2 [ ]] [ :r 3 [ ]] [ :append 4 0] ]}
{:index 9, :type :ok, :process 2, :value [[ :append 2 8] ]}
{:index 10, :type :ok, :process 1, :value [[ :append 3 7] [ :append 4 10] ]}

I tried the same directly with Elle and the processing went fine, so I believe that this is something to do how elle-cli imports history files.

After copy pasting the code to read history from Elle tests https://github.com/jepsen-io/elle/blob/main/test/elle/core_test.clj#L14, the problem went away.

diff --git a/src/elle_cli/cli.clj b/src/elle_cli/cli.clj
index d43cdb2..dc479b4 100644
--- a/src/elle_cli/cli.clj
+++ b/src/elle_cli/cli.clj
@@ -27,17 +27,10 @@
   expecting it to be a collection of op maps. If the initial character is {,
   loads it piecewise as op maps."
   [filepath]
-  (let [h (with-open [r (PushbackReader. (io/reader filepath))]
-            (->> (repeatedly #(edn/read {:eof nil} r))
-                 (take-while identity)
-                 vec))
-        ; Handle the presence or absence of an enclosing vector.
-        h (if (and (= 1 (count h))
-                   (sequential? (first h)))
-            (vec (first h))
-            h)]
-    ; Normalize ops.
-    (history/parse-ops h)))
+    (with-open [r (PushbackReader. (io/reader filepath))]
+    (->> (repeatedly #(edn/read {:eof nil} r))
+         (take-while identity)
+         vec)))
 
 (defn vl
   [v]

Being new to both Elle and Clojure I can't say for sure if the above change is correct for all models, but it seems to work
for elle-list-append.

To reproduce:

• Paste the above history in test.edn
• Run lein run --model elle-list-append --format edn --consistency-models repeatable-read test.edn

[ligurio]

@temeo thanks for reporting the issue. I'll take a look on it.

[ligurio]

Updated Markdown markup in description for better readability.

[ligurio]

elle-cli uses the same code as in Knossos checker for reading a file with history:
https://github.com/jepsen-io/knossos/blob/21a5c2b111fd90c51a519aea160f9d20bf2a6412/src/knossos/cli.clj#L16-L32