Skip to content

Latest commit

 

History

History
89 lines (50 loc) · 3.88 KB

how_to_start.md

File metadata and controls

89 lines (50 loc) · 3.88 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:

Action Type Description of Action Type
Input Represent a node receiving an input message, from a network endpoint or a terminal, for example
Output Represent a node sending an output message, to a network endpoint or a terminal, for example
Internal Represent an internal event in a node

Use the 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 traces.

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.

The figure below illustrates how the deterministic player reorders the actions based on predefined orders.

reorder_action

The physical system will align with the logical model, ensuring consistency. Our framework incorporates various macros to facilitate the implementation of anchor actions that verify the coherence between our source-level implementation and abstract-level design.

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

When running deterministic testing, the message channel would be taken over by the deterministic player.

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 this repo.