- Additional batch and query files

CMD Verifier/Sanity-1-log.txt

+Options for the verification:
+  Generating no trace
+  Search order is breadth first
+  Using conservative space optimisation
+  Seed is 1466156939
+  State space representation uses minimal constraint systems
+
+Verifying property 1 at line 6
+ -- Throughput: 2199 states/sec, Load: 41 states
 -- Throughput: 62850 states/sec, Load: 470 states
 -- Throughput: 74640 states/sec, Load: 5498 states
 -- Throughput: 77120 states/sec, Load: 8978 states
 -- Throughput: 82513 states/sec, Load: 11025 states
 -- Throughput: 78580 states/sec, Load: 17456 states
 -- Throughput: 79807 states/sec, Load: 19855 states
 -- Throughput: 77315 states/sec, Load: 20628 states
 -- Throughput: 82581 states/sec, Load: 21057 states
 -- Throughput: 85361 states/sec, Load: 18871 states
 -- Throughput: 80163 states/sec, Load: 18726 states
 -- Property is satisfied.
+Exit code      : 0
+Elapsed time   : 9.64
+Kernel time    : 0.09 (1.0%)
+User time      : 9.45 (98.1%)
+page fault #   : 9509
+Working set    : 37312 KB
+Paged pool     : 42 KB
+Non-paged pool : 7 KB
+Page file size : 60792 KB
+Options for the verification:
+  Generating no trace
+  Search order is depth first
+  Using conservative space optimisation
+  Seed is 1466156960
+  State space representation uses minimal constraint systems
+
+Verifying property 1 at line 6
+ -- Property is satisfied.
+Exit code      : 0
+Elapsed time   : 0.12
+Kernel time    : 0.06 (52.6%)
+User time      : 0.02 (13.2%)
+page fault #   : 2107
+Working set    : 8228 KB
+Paged pool     : 42 KB
+Non-paged pool : 7 KB
+Page file size : 36656 KB
+Options for the verification:
+  Generating no trace
+  Search order is depth first
+  Using conservative space optimisation
+  Seed is 1466158212
+  State space representation uses minimal constraint systems
+
+Verifying property 1 at line 6
+ -- Throughput: 2200 states/sec, Load: 36 states
 -- Property is satisfied.
+Exit code      : 0
+Elapsed time   : 0.16
+Kernel time    : 0.03 (19.4%)
+User time      : 0.06 (38.8%)
+page fault #   : 2106
+Working set    : 8224 KB
+Paged pool     : 42 KB
+Non-paged pool : 7 KB
+Page file size : 36656 KB

CMD Verifier/Sanity-1.bat

+color 0a
+TimeMem-1.0 verifyta -d ../Clocks-Test-4.xml Sanity-1.q >> Sanity-ALL-log.txt
\ No newline at end of file

CMD Verifier/Sanity-2-log.txt

+Options for the verification:
+  Generating no trace
+  Search order is breadth first
+  Using conservative space optimisation
+  Seed is 1466158213
+  State space representation uses minimal constraint systems
+
+Verifying property 1 at line 6
+ -- Throughput: 1833 states/sec, Load: 41 states
 -- Throughput: 35960 states/sec, Load: 397 states
 -- Throughput: 48334 states/sec, Load: 3627 states
 -- Throughput: 59746 states/sec, Load: 6507 states
 -- Throughput: 52317 states/sec, Load: 8939 states
 -- Throughput: 54441 states/sec, Load: 9641 states
 -- Throughput: 58729 states/sec, Load: 14910 states
 -- Throughput: 56579 states/sec, Load: 17929 states
 -- Throughput: 52243 states/sec, Load: 20357 states
 -- Throughput: 54138 states/sec, Load: 19103 states
 -- Throughput: 52358 states/sec, Load: 18699 states
 -- Throughput: 54145 states/sec, Load: 22845 states
 -- Throughput: 50556 states/sec, Load: 20384 states
 -- Throughput: 52228 states/sec, Load: 17412 states
 -- Throughput: 52386 states/sec, Load: 21013 states
 -- Throughput: 49987 states/sec, Load: 24148 states
 -- Throughput: 43810 states/sec, Load: 23094 states
 -- Throughput: 45119 states/sec, Load: 28709 states
 -- Throughput: 48360 states/sec, Load: 27183 states
 -- Throughput: 50115 states/sec, Load: 30943 states
 -- Throughput: 51138 states/sec, Load: 30915 states
 -- Throughput: 43858 states/sec, Load: 31526 states
 -- Throughput: 56738 states/sec, Load: 33499 states
 -- Throughput: 55790 states/sec, Load: 30191 states
 -- Throughput: 50262 states/sec, Load: 31751 states
 -- Throughput: 58787 states/sec, Load: 28492 states
 -- Throughput: 52163 states/sec, Load: 27896 states
 -- Throughput: 52744 states/sec, Load: 25217 states
 -- Throughput: 57393 states/sec, Load: 24964 states
 -- Throughput: 53589 states/sec, Load: 24269 states
 -- Throughput: 53590 states/sec, Load: 24733 states
 -- Throughput: 47806 states/sec, Load: 25721 states
 -- Throughput: 49540 states/sec, Load: 25829 states
 -- Throughput: 56683 states/sec, Load: 25503 states
 -- Throughput: 51066 states/sec, Load: 22612 states
 -- Throughput: 52864 states/sec, Load: 21405 states
 -- Throughput: 54669 states/sec, Load: 18456 states
 -- Throughput: 52365 states/sec, Load: 14277 states
 -- Throughput: 55531 states/sec, Load: 13171 states
 -- Throughput: 50300 states/sec, Load: 13985 states
 -- Throughput: 56202 states/sec, Load: 13613 states
 -- Throughput: 58120 states/sec, Load: 10672 states
 -- Throughput: 58589 states/sec, Load: 4747 states
 -- Throughput: 61608 states/sec, Load: 2629 states
 -- Property is satisfied.
+Exit code      : 0
+Elapsed time   : 42.33
+Kernel time    : 0.09 (0.2%)
+User time      : 38.95 (92.0%)
+page fault #   : 21558
+Working set    : 81920 KB
+Paged pool     : 42 KB
+Non-paged pool : 8 KB
+Page file size : 99544 KB

CMD Verifier/Sanity-2.bat

+color 0b
+TimeMem-1.0 verifyta ../Clocks-Test-4.xml Sanity-2.q >> Sanity-ALL-log.txt
\ No newline at end of file

CMD Verifier/Sanity-2.q

+// This file was generated by hand (c) Kristof Teichel June 16 2016
+
+/*
+
+*/
+A[] deadlock imply P_ClientBehavior.FINISH_PROCEDURE
\ No newline at end of file

CMD Verifier/Sanity-3-log.txt

+Options for the verification:
+  Generating no trace
+  Search order is breadth first
+  Using conservative space optimisation
+  Seed is 1466158213
+  State space representation uses difference bound matrices
+
+Verifying property 1 at line 6
+ -- Property is satisfied.
+Exit code      : 0
+Elapsed time   : 52.56
+Kernel time    : 0.22 (0.4%)
+User time      : 48.59 (92.5%)
+page fault #   : 34876
+Working set    : 135180 KB
+Paged pool     : 42 KB
+Non-paged pool : 9 KB
+Page file size : 144548 KB

CMD Verifier/Sanity-3.bat

+color 0e
+TimeMem-1.0 verifyta -C ../Clocks-Test-4.xml Sanity-3.q >> Sanity-ALL-log.txt
\ No newline at end of file

CMD Verifier/Sanity-3.q

+// This file was generated by hand (c) Kristof Teichel June 16 2016
+
+/*
+
+*/
+A<> P_ClientBehavior.FINISH_PROCEDURE
\ No newline at end of file

CMD Verifier/Sanity-ALL-log.txt

+Options for the verification:
+  Generating no trace
+  Search order is depth first
+  Using conservative space optimisation
+  Seed is 1466162828
+  State space representation uses minimal constraint systems
+
+Verifying property 1 at line 6
+ -- Throughput: 1833 states/sec, Load: 36 states
 -- Property is satisfied.
+Exit code      : 0
+Elapsed time   : 0.08
+Kernel time    : 0.05 (59.4%)
+User time      : 0.03 (39.6%)
+page fault #   : 2104
+Working set    : 8216 KB
+Paged pool     : 42 KB
+Non-paged pool : 7 KB
+Page file size : 36664 KB
+Options for the verification:
+  Generating no trace
+  Search order is breadth first
+  Using conservative space optimisation
+  Seed is 1466162841
+  State space representation uses minimal constraint systems
+
+Verifying property 1 at line 6
+ -- Throughput: 640935 states/sec, Load: 221 states
 -- Throughput: 76709 states/sec, Load: 17476 states
 -- Throughput: 81118 states/sec, Load: 21366 states
 -- Throughput: 78662 states/sec, Load: 24339 states
 -- Throughput: 70862 states/sec, Load: 27317 states
Exit code      : 3221225786
+Elapsed time   : 12.17
+Kernel time    : 0.06 (0.5%)
+User time      : 12.00 (98.5%)
+page fault #   : 11687
+Working set    : 44500 KB
+Paged pool     : 42 KB
+Non-paged pool : 7 KB
+Page file size : 67196 KB

CMD Verifier/Shell-MAIN.bat

+start cmd /k Sanity-1.bat 
+start cmd /k Sanity-2.bat 
+start cmd /k Sanity-3.bat 
\ No newline at end of file

Clocks-Test-4.xml

@@ -26,10 +26,10 @@ chan			server_interval_step;
 
 // PREFERENCES (Fixed constants, chosen by user via this source code) //
 
-const int 				unicast_repetitions_max 	= 	2;
+const int 				unicast_repetitions_max 	= 	1;
 int [0, unicast_repetitions_max]	unicast_repetitions_counter 	=	0;
 
-const int 				broadcast_repetitions_max 	= 	3;
+const int 				broadcast_repetitions_max 	= 	6;
 int[0, broadcast_repetitions_max] 	broadcast_repetitions_counter 	= 	0;
 
 const int