Description

This is a demo project for SAMC model checker. The program 'LeaderElection' does
only leader election. When you start multiple processes of LeaderElection, these
processes talk with each other to elect a leader, and become idle.

We integrate SAMC to the LeaderElection. The model checker will run the cluster
of LeaderElection program and model check it.


Compiling

1. Download and install AspectJ, more detail can find here,
https://eclipse.org/aspectj/

2. Set environment variable ASPECTJ_LIB to point to the AspectJ library path, 
e.g., If you use bash, add the following line to your bashrc
export ASPECTJ_LIB="/path/aspectj/lib"

3. Set Java classpath to include the AspectJ library (all AspectJ jar files).
e.g., If you use bash, add the following lines to your bashrc
CLASSPATH="$CLASSPATH:$ASPECTJ_LIB/aspectjrt.jar"
CLASSPATH="$CLASSPATH:$ASPECTJ_LIB/aspectjtools.jar"
CLASSPATH="$CLASSPATH:$ASPECTJ_LIB/aspectjweaver.jar"
CLASSPATH="$CLASSPATH:$ASPECTJ_LIB/org.aspectj.matcher.jar"
export CLASSPATH

4. Make sure that environment variables you set has an effect on your current
shell
e.g., If you use bash, you can run 
`source /path/to/your/bashrc`

5. Run ant to compile the LeaderElection program integrating with SAMC.
i.e.,
`ant`


Running

0. To run the model checker, you need to setup environment as same as when you
are compiling it (step 2 - 4).

1. Go to mcdeploy.

2. Open mcsystem.conf with a text editor. The mcsystem.conf is a config file for
model checker.
  - Change working_dir variable to a path model checker will work on. The
    model checker will store every file here including the intermediate data,
    environment setup script, log files, result, etc. It could be any path that
    you have permission to write (e.g. ~/modelcheck)
  - Change num_node to be the number of node of LeaderElection we want to test
  - Change exploring_strategy to be exploration strategy that we want to run
    - edu.uchicago.cs.ucare.samc.server.DfsTreeTravelModelChecker for DFS
      exploration
    - edu.uchicago.cs.ucare.samc.server.DporTreeTravelModelChecker for black-box
      DPOR
    - edu.uchicago.cs.ucare.samc.server.RandomModelChecker for random
      exploration
    - edu.uchicago.cs.ucare.samc.election.LeaderElectionSemanticAwareModelChecker
      for semantic-aware exploration

3. Go to mcdeploy/resource

4. Open testrunner.sh with a text editor. This is a shell script to run the
model checker.
  - Change `leader_election` variable assignment to the path of this project.

5. Go to mcdeploy again.

6. Run setup script (i.e. `./setup`), this is a shell script that setup
environment for running model checker in the working directory you specified in
mcsystem.conf

7. Run lermi script (i.e. `./lermi`), this is a shell script that run
rmiregistry with class path specifying. You have to change the defined variable
java.rmi.server.codebase to point to SAMC location class directory (i.e.
/path_to_samc/bin)

8. Go to the working directory that you have specified in mcsystem.conf

9. Run testrunner.sh (i.e. `./testrunner.sh`), now model checker will keep
running until it explores all paths.

10. In a log file, mc.log, there should not be ERROR line, and it should keep
informing the result this means that the setup is fine


Code

The aspect for LeaderElection program can be found here,
src/edu/uchicago/cs/ucare/example/election/LeaderElectionAspect.aj 

When a LeaderElection node send a packet to other nodes, the aspect intercepts
it and informs to model checker server. High level LeaderElection logic thinks
that it have done send the packet, but actually, the aspect keeps the packet
with itself. If model checker server decides to make that packet to be really
sent, it calls callback to the sender node, the aspect, and it really sends the
packet this time. When the receiver node gets the packet, it acknowledges back
to model checker. Every communication between LeaderElection program and model
checker server is done by RMI