Plot histogram for variable counter

[lemmy]

diff --git a/MCEWD998.cfg b/MCEWD998.cfg
index d998f17..75f0f3d 100644
--- a/MCEWD998.cfg
+++ b/MCEWD998.cfg
@@ -1,6 +1,9 @@
 CONSTANT N = 3
+CONSTANT Init <- StatsInit
 SPECIFICATION Spec
+CONSTRAINT Stats
 CONSTRAINT StateConstraint
\ No newline at end of file
+CONSTRAINT Plot
\ No newline at end of file
diff --git a/MCEWD998.tla b/MCEWD998.tla
index 4ce9ddd..8540b60 100644
--- a/MCEWD998.tla
+++ b/MCEWD998.tla
@@ -1,5 +1,38 @@
 ------------------------------- MODULE MCEWD998 -------------------------------
-EXTENDS EWD998
+EXTENDS EWD998, CSV, TLC, FiniteSets, Sequences, IOUtils
+
+-----------------------------------------------------------------------------
+
+StatsInit ==
+    (* Just a single initial state. *)
+    /\ active \in [Node -> {TRUE}]
+    /\ pending = [i \in Node |-> 0]
+    (* Rule 0 *)
+    /\ color \in [Node -> {"black"}]
+    /\ counter = [i \in Node |-> 0]
+    /\ pending = [i \in Node |-> 0]
+    /\ token = [pos |-> 0, q |-> 0, color |-> "black"]
+
+
+CSVFile ==
+    "MCEWD998.csv"
+
+ASSUME
+    (* Write CSV header at startup *)
+    CSVRecords(CSVFile) = 0 => CSVWrite("n#counter", <<>>, CSVFile)
+
+Stats ==
+    \* Cfg: CONSTRAINT Stats
+    \A n \in Node: CSVWrite("%1$s#%2$s", <<n, counter[n]>>, CSVFile)
+
+Plot ==
+    \* Cfg: CONSTRAINT Plot
+    \* level 2 and not 1 because all initial states are generated at startup.
+    TLCGet("level") = 2 =>
+        IOExec(<<
+            "/usr/bin/env", "Rscript",
+            "MCEWD998.R", CSVFile>>).exitValue = 0
+-----------------------------------------------------------------------------
 
 (***************************************************************************)
 (* Bound the otherwise infinite state space that TLC has to check.         *)

MCEWD998.R

#!/usr/bin/env Rscript
args = commandArgs(trailingOnly=TRUE)

svg("MCEWD998.svg")

d <-
  read.csv(
    header = TRUE, sep = '#', 
       file = args[1])

hist(d$counter, 
     main='EWD840!counter', 
     xlab ='Number of Messages', 
     xlim = c(min(d$counter), max(d$counter)))

dev.off()