Repliss

The replicated information system verification tool for the development of applications with strong guarantees on weakly consistent data stores.

Getting started

See User Documentation.

To use Repliss there are several options:

1. Run the web interface using Docker:

    docker run -i --rm -p 8080:8080 peterzel/repliss --server -h 0.0.0.0 -p 8080 
   

2. Run Repliss on a single file using docker. The following example assumes chatapp.rpls is the file to check in the current working directory. The model directory is mounted to have access to the outputs generated by Repliss.

    docker run -i --rm -v $(pwd):/code -v $(pwd)/model:/opt/repliss/model  peterzel/repliss /code/chatapp.rpls --quickcheck --symbolicCheck
   

3. Compile and run manually using the steps below.

Compilation

Software Requirements:

• The Scala Build Tool (SBT)
• Operation system: x86_64-linux (for other operating systems, the CVC4 library must be added manually)
• Graphviz

To run the Repliss Demo webserver run:

sbt "run --server"

Hostname and port can be configured with the --host and --port arguments.

Other useful commands, which can be used in an SBT console:

• Build an executable jar file with replissJVM/assembly

• Compile with compile

• Run tests with test

• For continuous building of the web server:

  • Run the main project with ~reStart --server
  • Run the js subproject with dev and open port 8081.

• Run a specific file with replissJVM/run <filename> By default Repliss only parses and typechecks the file. Use the --quickcheck option to enable automatic tests and the --symbolicCheck option to verify the input.

  For example:

  replissJVM/run verified/userbase.rpls --symbolicCheck --quickcheck