1. Put your TicketingDS.java and other related files in the ticketingsystem directory.

2. The TrainConfig file contains the configuration of a Train Ticketing System.

3. The history.sh calls GenerateHistory to generate a finite history of size threadNum * testNum, i.e., with threadNum threads and testNum operations per thread. The parameters for GenerateHistory are threadNum, testNum, isSequential, msec and nsec. 
   * isSequential=1 for a sequential execution, and 0 for a concurrent one
   * msec and nsec are the milli- and nano-seconds of a delay, e.g., msec=1 and nsec=0 for delay 1ms 

4. The verilin.sh calls VeriLin.jar for linearizability checking. The parameters for VeriLin are threadNum, historyFile, isPosttime and outputFile.
   * historyFile is generated by GenerateHistory, possibly out of order even for a sequential execution
   * isPosttime=1 for post-time sorting, and 0 for pre-time sorting
   * outputFile is a maximal linearizable history prefix

5. The replay.sh calls Replay to check if a sequential or sequentialized history is correct.