first results for parametric benchmarks

parametric/003SetAdd-apalache.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetAdd/SetAdd_5.tla,apalache,1h,,,,--length=5
+6,SetAdd/SetAdd_6.tla,apalache,1h,,,,--length=6
+7,SetAdd/SetAdd_7.tla,apalache,1h,,,,--length=7
+8,SetAdd/SetAdd_8.tla,apalache,1h,,,,--length=8
+9,SetAdd/SetAdd_9.tla,apalache,1h,,,,--length=9
+10,SetAdd/SetAdd_10.tla,apalache,1h,,,,--length=10
+11,SetAdd/SetAdd_11.tla,apalache,1h,,,,--length=11
+12,SetAdd/SetAdd_12.tla,apalache,1h,,,,--length=12
+13,SetAdd/SetAdd_13.tla,apalache,1h,,,,--length=13
+14,SetAdd/SetAdd_14.tla,apalache,1h,,,,--length=14
+15,SetAdd/SetAdd_15.tla,apalache,1h,,,,--length=15
+
+

parametric/003SetAdd-tlc.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetAdd/SetAdd_5.tla,tlc,1h,,,,
+6,SetAdd/SetAdd_6.tla,tlc,1h,,,,
+7,SetAdd/SetAdd_7.tla,tlc,1h,,,,
+8,SetAdd/SetAdd_8.tla,tlc,1h,,,,
+9,SetAdd/SetAdd_9.tla,tlc,1h,,,,
+10,SetAdd/SetAdd_10.tla,tlc,1h,,,,
+11,SetAdd/SetAdd_11.tla,tlc,1h,,,,
+12,SetAdd/SetAdd_12.tla,tlc,1h,,,,
+13,SetAdd/SetAdd_13.tla,tlc,1h,,,,
+14,SetAdd/SetAdd_14.tla,tlc,1h,,,,
+15,SetAdd/SetAdd_15.tla,tlc,1h,,,,
+
+

parametric/003SetAdd-z3.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetAdd/SetAdd_5.smt,z3,1h,,,,
+6,SetAdd/SetAdd_6.smt,z3,1h,,,,
+7,SetAdd/SetAdd_7.smt,z3,1h,,,,
+8,SetAdd/SetAdd_8.smt,z3,1h,,,,
+9,SetAdd/SetAdd_9.smt,z3,1h,,,,
+10,SetAdd/SetAdd_10.smt,z3,1h,,,,
+11,SetAdd/SetAdd_11.smt,z3,1h,,,,
+12,SetAdd/SetAdd_12.smt,z3,1h,,,,
+13,SetAdd/SetAdd_13.smt,z3,1h,,,,
+14,SetAdd/SetAdd_14.smt,z3,1h,,,,
+15,SetAdd/SetAdd_15.smt,z3,1h,,,,
+
+

parametric/004SetAddDel-apalache.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetAddDel/SetAddDel_5.tla,apalache,1h,,,,--length=5
+6,SetAddDel/SetAddDel_6.tla,apalache,1h,,,,--length=6
+7,SetAddDel/SetAddDel_7.tla,apalache,1h,,,,--length=7
+8,SetAddDel/SetAddDel_8.tla,apalache,1h,,,,--length=8
+9,SetAddDel/SetAddDel_9.tla,apalache,1h,,,,--length=9
+10,SetAddDel/SetAddDel_10.tla,apalache,1h,,,,--length=10
+11,SetAddDel/SetAddDel_11.tla,apalache,1h,,,,--length=11
+12,SetAddDel/SetAddDel_12.tla,apalache,1h,,,,--length=12
+13,SetAddDel/SetAddDel_13.tla,apalache,1h,,,,--length=13
+14,SetAddDel/SetAddDel_14.tla,apalache,1h,,,,--length=14
+15,SetAddDel/SetAddDel_15.tla,apalache,1h,,,,--length=15
+
+

parametric/004SetAddDel-tlc.csv

@@ -0,0 +1,22 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetAddDel/SetAddDel_5.tla,tlc,1h,,,,
+6,SetAddDel/SetAddDel_6.tla,tlc,1h,,,,
+7,SetAddDel/SetAddDel_7.tla,tlc,1h,,,,
+8,SetAddDel/SetAddDel_8.tla,tlc,1h,,,,
+9,SetAddDel/SetAddDel_9.tla,tlc,1h,,,,
+10,SetAddDel/SetAddDel_10.tla,tlc,1h,,,,
+11,SetAddDel/SetAddDel_11.tla,tlc,1h,,,,
+12,SetAddDel/SetAddDel_12.tla,tlc,1h,,,,
+13,SetAddDel/SetAddDel_13.tla,tlc,1h,,,,
+14,SetAddDel/SetAddDel_14.tla,tlc,1h,,,,
+15,SetAddDel/SetAddDel_15.tla,tlc,1h,,,,
+16,SetAddDel/SetAddDel_16.tla,tlc,1h,,,,
+17,SetAddDel/SetAddDel_17.tla,tlc,1h,,,,
+18,SetAddDel/SetAddDel_18.tla,tlc,1h,,,,
+19,SetAddDel/SetAddDel_19.tla,tlc,1h,,,,
+20,SetAddDel/SetAddDel_20.tla,tlc,1h,,,,
+21,SetAddDel/SetAddDel_21.tla,tlc,1h,,,,
+22,SetAddDel/SetAddDel_22.tla,tlc,1h,,,,
+23,SetAddDel/SetAddDel_23.tla,tlc,1h,,,,
+
+

parametric/004SetAddDel-z3.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetAddDel/SetAddDel_5.smt,z3,1h,,,,
+6,SetAddDel/SetAddDel_6.smt,z3,1h,,,,
+7,SetAddDel/SetAddDel_7.smt,z3,1h,,,,
+8,SetAddDel/SetAddDel_8.smt,z3,1h,,,,
+9,SetAddDel/SetAddDel_9.smt,z3,1h,,,,
+10,SetAddDel/SetAddDel_10.smt,z3,1h,,,,
+11,SetAddDel/SetAddDel_11.smt,z3,1h,,,,
+12,SetAddDel/SetAddDel_12.smt,z3,1h,,,,
+13,SetAddDel/SetAddDel_13.smt,z3,1h,,,,
+14,SetAddDel/SetAddDel_14.smt,z3,1h,,,,
+15,SetAddDel/SetAddDel_15.smt,z3,1h,,,,
+
+

parametric/005SetSndRcv-apalache.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_5.tla,apalache,1h,,,,--length=10
+6,SetSndRcv/SetSndRcv_6.tla,apalache,1h,,,,--length=12
+7,SetSndRcv/SetSndRcv_7.tla,apalache,1h,,,,--length=14
+8,SetSndRcv/SetSndRcv_8.tla,apalache,1h,,,,--length=16
+9,SetSndRcv/SetSndRcv_9.tla,apalache,1h,,,,--length=18
+10,SetSndRcv/SetSndRcv_10.tla,apalache,1h,,,,--length=20
+11,SetSndRcv/SetSndRcv_11.tla,apalache,1h,,,,--length=22
+12,SetSndRcv/SetSndRcv_12.tla,apalache,1h,,,,--length=24
+13,SetSndRcv/SetSndRcv_13.tla,apalache,1h,,,,--length=26
+14,SetSndRcv/SetSndRcv_14.tla,apalache,1h,,,,--length=28
+15,SetSndRcv/SetSndRcv_15.tla,apalache,1h,,,,--length=30
+
+

parametric/005SetSndRcv-tlc.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_5.tla,tlc,1h,,,,
+6,SetSndRcv/SetSndRcv_6.tla,tlc,1h,,,,
+7,SetSndRcv/SetSndRcv_7.tla,tlc,1h,,,,
+8,SetSndRcv/SetSndRcv_8.tla,tlc,1h,,,,
+9,SetSndRcv/SetSndRcv_9.tla,tlc,1h,,,,
+10,SetSndRcv/SetSndRcv_10.tla,tlc,1h,,,,
+11,SetSndRcv/SetSndRcv_11.tla,tlc,1h,,,,
+12,SetSndRcv/SetSndRcv_12.tla,tlc,1h,,,,
+13,SetSndRcv/SetSndRcv_13.tla,tlc,1h,,,,
+14,SetSndRcv/SetSndRcv_14.tla,tlc,1h,,,,
+15,SetSndRcv/SetSndRcv_15.tla,tlc,1h,,,,
+
+

parametric/005SetSndRcv-z3.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_5.smt,z3,1h,,,,
+6,SetSndRcv/SetSndRcv_6.smt,z3,1h,,,,
+7,SetSndRcv/SetSndRcv_7.smt,z3,1h,,,,
+8,SetSndRcv/SetSndRcv_8.smt,z3,1h,,,,
+9,SetSndRcv/SetSndRcv_9.smt,z3,1h,,,,
+10,SetSndRcv/SetSndRcv_10.smt,z3,1h,,,,
+11,SetSndRcv/SetSndRcv_11.smt,z3,1h,,,,
+12,SetSndRcv/SetSndRcv_12.smt,z3,1h,,,,
+13,SetSndRcv/SetSndRcv_13.smt,z3,1h,,,,
+14,SetSndRcv/SetSndRcv_14.smt,z3,1h,,,,
+15,SetSndRcv/SetSndRcv_15.smt,z3,1h,,,,
+
+

parametric/006SetSndRcv_NoFullDrop-apalache.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_NoFullDrop_5.tla,apalache,1h,,,,--length=10
+6,SetSndRcv/SetSndRcv_NoFullDrop_6.tla,apalache,1h,,,,--length=12
+7,SetSndRcv/SetSndRcv_NoFullDrop_7.tla,apalache,1h,,,,--length=14
+8,SetSndRcv/SetSndRcv_NoFullDrop_8.tla,apalache,1h,,,,--length=16
+9,SetSndRcv/SetSndRcv_NoFullDrop_9.tla,apalache,1h,,,,--length=18
+10,SetSndRcv/SetSndRcv_NoFullDrop_10.tla,apalache,1h,,,,--length=20
+11,SetSndRcv/SetSndRcv_NoFullDrop_11.tla,apalache,1h,,,,--length=22
+12,SetSndRcv/SetSndRcv_NoFullDrop_12.tla,apalache,1h,,,,--length=24
+13,SetSndRcv/SetSndRcv_NoFullDrop_13.tla,apalache,1h,,,,--length=26
+14,SetSndRcv/SetSndRcv_NoFullDrop_14.tla,apalache,1h,,,,--length=28
+15,SetSndRcv/SetSndRcv_NoFullDrop_15.tla,apalache,1h,,,,--length=30
+
+

parametric/006SetSndRcv_NoFullDrop-tlc.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_NoFullDrop_5.tla,tlc,1h,,,,
+6,SetSndRcv/SetSndRcv_NoFullDrop_6.tla,tlc,1h,,,,
+7,SetSndRcv/SetSndRcv_NoFullDrop_7.tla,tlc,1h,,,,
+8,SetSndRcv/SetSndRcv_NoFullDrop_8.tla,tlc,1h,,,,
+9,SetSndRcv/SetSndRcv_NoFullDrop_9.tla,tlc,1h,,,,
+10,SetSndRcv/SetSndRcv_NoFullDrop_10.tla,tlc,1h,,,,
+11,SetSndRcv/SetSndRcv_NoFullDrop_11.tla,tlc,1h,,,,
+12,SetSndRcv/SetSndRcv_NoFullDrop_12.tla,tlc,1h,,,,
+13,SetSndRcv/SetSndRcv_NoFullDrop_13.tla,tlc,1h,,,,
+14,SetSndRcv/SetSndRcv_NoFullDrop_14.tla,tlc,1h,,,,
+15,SetSndRcv/SetSndRcv_NoFullDrop_15.tla,tlc,1h,,,,
+
+

parametric/006SetSndRcv_NoFullDrop-z3.csv

@@ -0,0 +1,13 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_NoFullDrop_5.smt,z3,1h,,,,
+6,SetSndRcv/SetSndRcv_NoFullDrop_6.smt,z3,1h,,,,
+7,SetSndRcv/SetSndRcv_NoFullDrop_7.smt,z3,1h,,,,
+8,SetSndRcv/SetSndRcv_NoFullDrop_8.smt,z3,1h,,,,
+9,SetSndRcv/SetSndRcv_NoFullDrop_9.smt,z3,1h,,,,
+10,SetSndRcv/SetSndRcv_NoFullDrop_10.smt,z3,1h,,,,
+11,SetSndRcv/SetSndRcv_NoFullDrop_11.smt,z3,1h,,,,
+12,SetSndRcv/SetSndRcv_NoFullDrop_12.smt,z3,1h,,,,
+13,SetSndRcv/SetSndRcv_NoFullDrop_13.smt,z3,1h,,,,
+14,SetSndRcv/SetSndRcv_NoFullDrop_14.smt,z3,1h,,,,
+15,SetSndRcv/SetSndRcv_NoFullDrop_15.smt,z3,1h,,,,
+

parametric/007SetSndRcv_NoFullDropCard-apalache.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_NoFullDropCard_5.tla,apalache,1h,,,,--length=10
+6,SetSndRcv/SetSndRcv_NoFullDropCard_6.tla,apalache,1h,,,,--length=12
+7,SetSndRcv/SetSndRcv_NoFullDropCard_7.tla,apalache,1h,,,,--length=14
+8,SetSndRcv/SetSndRcv_NoFullDropCard_8.tla,apalache,1h,,,,--length=16
+9,SetSndRcv/SetSndRcv_NoFullDropCard_9.tla,apalache,1h,,,,--length=18
+10,SetSndRcv/SetSndRcv_NoFullDropCard_10.tla,apalache,1h,,,,--length=20
+11,SetSndRcv/SetSndRcv_NoFullDropCard_11.tla,apalache,1h,,,,--length=22
+12,SetSndRcv/SetSndRcv_NoFullDropCard_12.tla,apalache,1h,,,,--length=24
+13,SetSndRcv/SetSndRcv_NoFullDropCard_13.tla,apalache,1h,,,,--length=26
+14,SetSndRcv/SetSndRcv_NoFullDropCard_14.tla,apalache,1h,,,,--length=28
+15,SetSndRcv/SetSndRcv_NoFullDropCard_15.tla,apalache,1h,,,,--length=30
+
+

parametric/007SetSndRcv_NoFullDropCard-tlc.csv

@@ -0,0 +1,14 @@
+no,filename,tool,timeout,init,inv,next,args
+5,SetSndRcv/SetSndRcv_NoFullDropCard_5.tla,tlc,1h,,,,
+6,SetSndRcv/SetSndRcv_NoFullDropCard_6.tla,tlc,1h,,,,
+7,SetSndRcv/SetSndRcv_NoFullDropCard_7.tla,tlc,1h,,,,
+8,SetSndRcv/SetSndRcv_NoFullDropCard_8.tla,tlc,1h,,,,
+9,SetSndRcv/SetSndRcv_NoFullDropCard_9.tla,tlc,1h,,,,
+10,SetSndRcv/SetSndRcv_NoFullDropCard_10.tla,tlc,1h,,,,
+11,SetSndRcv/SetSndRcv_NoFullDropCard_11.tla,tlc,1h,,,,
+12,SetSndRcv/SetSndRcv_NoFullDropCard_12.tla,tlc,1h,,,,
+13,SetSndRcv/SetSndRcv_NoFullDropCard_13.tla,tlc,1h,,,,
+14,SetSndRcv/SetSndRcv_NoFullDropCard_14.tla,tlc,1h,,,,
+15,SetSndRcv/SetSndRcv_NoFullDropCard_15.tla,tlc,1h,,,,
+
+

parametric/008IntClocks-apalache.csv

@@ -0,0 +1,13 @@
+no,filename,tool,timeout,init,inv,next,args
+1,IntClocks/IntClocks_1.tla,apalache,1h,,,,--length=10
+2,IntClocks/IntClocks_2.tla,apalache,1h,,,,--length=20
+3,IntClocks/IntClocks_3.tla,apalache,1h,,,,--length=30
+4,IntClocks/IntClocks_4.tla,apalache,1h,,,,--length=40
+5,IntClocks/IntClocks_5.tla,apalache,1h,,,,--length=50
+6,IntClocks/IntClocks_6.tla,apalache,1h,,,,--length=60
+7,IntClocks/IntClocks_7.tla,apalache,1h,,,,--length=70
+8,IntClocks/IntClocks_8.tla,apalache,1h,,,,--length=80
+9,IntClocks/IntClocks_9.tla,apalache,1h,,,,--length=90
+10,IntClocks/IntClocks_10.tla,apalache,1h,,,,--length=100
+
+

parametric/008IntClocks-tlc.csv

@@ -0,0 +1,12 @@
+no,filename,tool,timeout,init,inv,next,args
+1,IntClocks/IntClocks_1.tla,tlc,1h,,,,
+2,IntClocks/IntClocks_2.tla,tlc,1h,,,,
+3,IntClocks/IntClocks_3.tla,tlc,1h,,,,
+4,IntClocks/IntClocks_4.tla,tlc,1h,,,,
+5,IntClocks/IntClocks_5.tla,tlc,1h,,,,
+6,IntClocks/IntClocks_6.tla,tlc,1h,,,,
+7,IntClocks/IntClocks_7.tla,tlc,1h,,,,
+8,IntClocks/IntClocks_8.tla,tlc,1h,,,,
+9,IntClocks/IntClocks_9.tla,tlc,1h,,,,
+10,IntClocks/IntClocks_10.tla,tlc,1h,,,,
+

parametric/008IntClocks-z3.csv

@@ -0,0 +1,12 @@
+no,filename,tool,timeout,init,inv,next,args
+1,IntClocks/IntClocks_1.smt,z3,1h,,,,
+2,IntClocks/IntClocks_2.smt,z3,1h,,,,
+3,IntClocks/IntClocks_3.smt,z3,1h,,,,
+4,IntClocks/IntClocks_4.smt,z3,1h,,,,
+5,IntClocks/IntClocks_5.smt,z3,1h,,,,
+6,IntClocks/IntClocks_6.smt,z3,1h,,,,
+7,IntClocks/IntClocks_7.smt,z3,1h,,,,
+8,IntClocks/IntClocks_8.smt,z3,1h,,,,
+9,IntClocks/IntClocks_9.smt,z3,1h,,,,
+10,IntClocks/IntClocks_10.smt,z3,1h,,,,
+

parametric/009IntClocks_Bounded-apalache.csv

@@ -0,0 +1,13 @@
+no,filename,tool,timeout,init,inv,next,args
+1,IntClocks/IntClocks_Bounded_1.tla,apalache,1h,,,,--length=10
+2,IntClocks/IntClocks_Bounded_2.tla,apalache,1h,,,,--length=20
+3,IntClocks/IntClocks_Bounded_3.tla,apalache,1h,,,,--length=30
+4,IntClocks/IntClocks_Bounded_4.tla,apalache,1h,,,,--length=40
+5,IntClocks/IntClocks_Bounded_5.tla,apalache,1h,,,,--length=50
+6,IntClocks/IntClocks_Bounded_6.tla,apalache,1h,,,,--length=60
+7,IntClocks/IntClocks_Bounded_7.tla,apalache,1h,,,,--length=70
+8,IntClocks/IntClocks_Bounded_8.tla,apalache,1h,,,,--length=80
+9,IntClocks/IntClocks_Bounded_9.tla,apalache,1h,,,,--length=90
+10,IntClocks/IntClocks_Bounded_10.tla,apalache,1h,,,,--length=100
+
+

parametric/009IntClocks_Bounded-tlc.csv

@@ -0,0 +1,12 @@
+no,filename,tool,timeout,init,inv,next,args
+1,IntClocks/IntClocks_Bounded_1.tla,tlc,1h,,,,
+2,IntClocks/IntClocks_Bounded_2.tla,tlc,1h,,,,
+3,IntClocks/IntClocks_Bounded_3.tla,tlc,1h,,,,
+4,IntClocks/IntClocks_Bounded_4.tla,tlc,1h,,,,
+5,IntClocks/IntClocks_Bounded_5.tla,tlc,1h,,,,
+6,IntClocks/IntClocks_Bounded_6.tla,tlc,1h,,,,
+7,IntClocks/IntClocks_Bounded_7.tla,tlc,1h,,,,
+8,IntClocks/IntClocks_Bounded_8.tla,tlc,1h,,,,
+9,IntClocks/IntClocks_Bounded_9.tla,tlc,1h,,,,
+10,IntClocks/IntClocks_Bounded_10.tla,tlc,1h,,,,
+

parametric/009IntClocks_Bounded-z3.csv

@@ -0,0 +1,12 @@
+no,filename,tool,timeout,init,inv,next,args
+1,IntClocks/IntClocks_Bounded_1.smt,z3,1h,,,,
+2,IntClocks/IntClocks_Bounded_2.smt,z3,1h,,,,
+3,IntClocks/IntClocks_Bounded_3.smt,z3,1h,,,,
+4,IntClocks/IntClocks_Bounded_4.smt,z3,1h,,,,
+5,IntClocks/IntClocks_Bounded_5.smt,z3,1h,,,,
+6,IntClocks/IntClocks_Bounded_6.smt,z3,1h,,,,
+7,IntClocks/IntClocks_Bounded_7.smt,z3,1h,,,,
+8,IntClocks/IntClocks_Bounded_8.smt,z3,1h,,,,
+9,IntClocks/IntClocks_Bounded_9.smt,z3,1h,,,,
+10,IntClocks/IntClocks_Bounded_10.smt,z3,1h,,,,
+

parametric/SetAddDel/SetAddDel_16.cfg

@@ -0,0 +1,10 @@
+\* CONSTANT definitions
+CONSTANT
+values <- MC_values
+INIT
+MC_Init
+NEXT
+MC_Next
+INVARIANT
+MC_Inv
+\* Generated on Tue May 05 10:18:40 CEST 2020

parametric/SetAddDel/SetAddDel_16.tla

@@ -0,0 +1,15 @@
+---- MODULE SetAddDel_16 ----
+EXTENDS SetAddDel, TLC
+
+MC_values == {"v0", "v1", "v2", "v3", "v4", "v5", "v6", "v7", "v8", "v9", "v10", "v11", "v12", "v13", "v14", "v15"}
+----
+MC_Init == Init
+----
+MC_Next == Next
+----
+MC_Inv == Inv
+----
+
+=============================================================================
+\* Modification History
+\* Created Tue May 05 10:18:40 CEST 2020 by andrey

parametric/SetAddDel/SetAddDel_17.cfg

@@ -0,0 +1,10 @@
+\* CONSTANT definitions
+CONSTANT
+values <- MC_values
+INIT
+MC_Init
+NEXT
+MC_Next
+INVARIANT
+MC_Inv
+\* Generated on Tue May 05 10:18:42 CEST 2020

parametric/SetAddDel/SetAddDel_17.tla

@@ -0,0 +1,15 @@
+---- MODULE SetAddDel_17 ----
+EXTENDS SetAddDel, TLC
+
+MC_values == {"v0", "v1", "v2", "v3", "v4", "v5", "v6", "v7", "v8", "v9", "v10", "v11", "v12", "v13", "v14", "v15", "v16"}
+----
+MC_Init == Init
+----
+MC_Next == Next
+----
+MC_Inv == Inv
+----
+
+=============================================================================
+\* Modification History
+\* Created Tue May 05 10:18:42 CEST 2020 by andrey

parametric/SetAddDel/SetAddDel_18.cfg

@@ -0,0 +1,10 @@
+\* CONSTANT definitions
+CONSTANT
+values <- MC_values
+INIT
+MC_Init
+NEXT
+MC_Next
+INVARIANT
+MC_Inv
+\* Generated on Tue May 05 10:18:44 CEST 2020

parametric/SetAddDel/SetAddDel_18.tla

@@ -0,0 +1,15 @@
+---- MODULE SetAddDel_18 ----
+EXTENDS SetAddDel, TLC
+
+MC_values == {"v0", "v1", "v2", "v3", "v4", "v5", "v6", "v7", "v8", "v9", "v10", "v11", "v12", "v13", "v14", "v15", "v16", "v17"}
+----
+MC_Init == Init
+----
+MC_Next == Next
+----
+MC_Inv == Inv
+----
+
+=============================================================================
+\* Modification History
+\* Created Tue May 05 10:18:44 CEST 2020 by andrey

parametric/SetAddDel/SetAddDel_19.cfg

@@ -0,0 +1,10 @@
+\* CONSTANT definitions
+CONSTANT
+values <- MC_values
+INIT
+MC_Init
+NEXT
+MC_Next
+INVARIANT
+MC_Inv
+\* Generated on Tue May 05 10:18:47 CEST 2020