add constraint for DFS

Author: hcirstea

conf.ndjson

@@ -1 +1 @@
-{"Key":[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20],"Val":["V1","V2","V3","V4","V5","V6","V7","V8","V9","V10","V11","V12","V13","V14","V15","V16","V17","V18","V19","V20","V21","V22","V23","V24","V25","V26","V27","V28","V29","V30","V31","V32","V33","V34","V35","V26","V37","V38","V39","V40"],"TxId":["0","1","2","3","4","5","6","7","8","9"]}
+{"Key":[1,2,3,4,5,6,7,8,9,10],"Val":["V1","V2","V3","V4","V5","V6","V7","V8","V9","V10","V11","V12","V13","V14","V15","V16","V17","V18","V19","V20"],"TxId":["0","1","2","3","4","5","6","7","8","9"]}

spec/TraceSpec.tla

@@ -72,4 +72,9 @@ TraceView ==
      \* consider  s_i  and s_j  , where  i  and  j  are the positions of  s  in the trace,
      \* to be different states.
     <<Vars, TLCGet("level")>>
+
+Termination ==
+    \* -Dtlc2.tool.queue.IStateQueue=StateDeque
+    l = Len(Trace) + 1  => TLCSet("exit", TRUE)
+
 ====