TLA+ generator and generated example for verification
Generate specification for module which uses GenServer with:
mix gen_spec <filename>
in gen_spec folder.
Already generated example (together with manually written specification for sequential code) is available in gen_spec/tla/bracha.tla. It was generated from bracha/lib/bracha.ex file.