Skip to content

Latest commit

 

History

History
70 lines (40 loc) · 2.87 KB

how_to_start.md

File metadata and controls

70 lines (40 loc) · 2.87 KB
Raw

How To Start

Configure TLA+ toolbox

Configure TLA+ toolbox

Write TLA+ specification

In the TLA+ specification, we use InitAction and SetAction to specify the action of I/O automata and output the state to sqlite database.

Run TLA+ model checker and generate state database(a sqlite file).

  1. Filling Model checker setting:

    Specify constant value and Temporal formula

  2. In Model -> TLC Options Page -> Parameters -> JVM arguments: box:

    Specify Java property parameter "tlc2.overrides.TLCOverrides" by filling the text,

-Dtlc2.overrides.TLCOverrides=tlc2.overrides.TLCOverrides:tlc2.overrides.SedeveTLCOverrides

The "tlc2.overrides.TLCOverrides" is used by thethe ComunityModeules; and "the tlc2.overrides.SedeveTLCOverrides" is used by SedeveModules.

More about overrides, see SpecProcessor.java, TLCOverrides.java

  1. Click then Runs TLC on the model Button

Development by specification

Generate a trace from the sqlite state database that was output by the TLA+ toolbox.

A trace is a finite sequence of actions. An action is a step of state transition. We define several action types based on their functionalities. The action types include:

Use the sedeve_trace-gen to traversal state space and dump all trace into a database(e.g., sqlite DB file) The trace format is represented in JSON, similar to this JSON file The action incoming interface can be used to read action steps of trace.

Insert anchor actions to the testing source code

We define certain anchor actions that allow us to send a message to the deterministic player for reordering the actions.

Implement the Rust code

Add assert invariants to the testing source code

During testing, we add invariants to assert the correctness of our assumptions.

Running deterministic testing

Example

Two-Phase Commit Protocol(2PC) is a atomic commit protocol. The example of using this kit to develop 2PC could be found at example-2pc.

Raft consensus algorithm. We implement scupt-raft