1. Improve etcdraft spec to provide hooks for model-checking and trace validation.
2. Add new sample application based on raft and capable of injecting various faults.
3. Add new test to generate random traces (with faults) and run trace validation on them.
4. Fix some issues in etcdraft spec.

Signed-off-by: Joshua Zhang <[email protected]>

1. Remove type annotations which are not needed here.
2. Add more comments for the actions.
3. Fix simulation argument in valide-model.sh.
4. Let validate-model.sh use all cores to improve performance.

Signed-off-by: Joshua Zhang <[email protected]>

1. Decouple SpecAction and relevant definitions from the core etcd raft spec.
Put them into a middle layer spec etcdraft_control.tla
2. Fix racing issue in trace_validation_test.go.

Signed-off-by: Joshua Zhang <[email protected]>