Elixir code and test generation from TLA specifications

For nix users, there are nix files for both a Haskell and an Elixir environment.

• GHC 8.0.2

• Elixir
• Erlang

Instructions for installation with asdf package manager

make compile

The best parsing implementation takes JSON files previously parsed from TLA with Apalache:

apalache-mc parse --output=file.json file.tla

All compliled files (CodeGenerator, WhiteboxTestGenerator and BlackboxTestGenerator) take a single argument which is a JSON-formatted configuration file similar to config-sample.json

Folders inside tla_specifications are examples containing the required files for running the three executables. You can cd into any of them and run:

../../CodeGenerator config.json && ../../BlackboxTestGenerator config.json && ../../WhiteboxTestGenerator config.json