salt

"S-expressions for Actions with Logic Temporal"

An experimental tool to convert a subset of Clojure into TLA+. Although it is experimental it has been used to produce real, useful TLA+ specifications.

You might want to use this if you know Clojure and are writing TLA+ specifications. Specifically it provides:

• an interactive REPL based authoring experience
• facilities for automated unit tests of invariants and actions
• automatic formatting of resulting TLA+ code
• a mapping from TLA+ to Clojure concepts that may facilitate learning TLA+

To use it:

1. Write a specification using salt.
2. Evaluate the salt specification in the REPL as part of the development process.
3. Once it is ready to be run in the TLA+ Toolbox, invoke the salt transpiler to emit TLA+ code.
4. Run the resulting TLA+ specification in the TLA+ Toolbox to assess the temporal properties of the specification.

The library is available on Clojars: [org.clojars.david-mcneil/salt "0.0.4"]

In your salt specification file require the salt language as:

(:require [salt.lang :refer :all])

From the Clojure REPL, transpile a salt source file into a TLA+ file using an incantation like this:

(spit <tla+-filename> (salt.transpiler/transpile-text (slurp <salt-filename>)))

Alternatively, the salt transpiler can be invoked from the command line:

lein uberjar

java -cp target/salt-0.0.1-standalone.jar clojure.main -m salt.main <salt-filename>

Table of Contents

• Language Identifiers
• Clojure to TLA+ Concepts
• Standard Modules
• Docs
  • Primitives
  • Code Structure
  • Arithmetic
  • Specs
  • Logic
  • Temporal Logic
  • Sets
  • Vectors
  • Maps
  • Maps As Records
  • Maps As Tuples
  • Functions
• Example Salt
• Example TLA+
• Change Log

Language Identifiers

The following identifiers are reserved for the salt language.

Identifiers from the Clojure language:

and comment cond conj contains? count def defn difference expt first fn if intersection into let ns not or require select str subset? superset? union

Identifiers from the Clojure language, whose semantics were modified to match TLA+:

every?* get* map* mod* range* rest*

Identifiers that were added specifically to support transpiling, they are neither part of Clojure nor TLA+:

always- CHANGED- defm- eventually- fm- leads-to- line- maps- subset-proper? superset-proper? VARS-

Identifiers from the TLA+ language:

== => <=> = > < >= <= + - * A ASSUME Cardinality CHOOSE CONSTANT div DOMAIN E EXCEPT Nat not= UNCHANGED UNION SelectSeq Seq SF SubSeq SUBSET VARIABLE WF X

Clojure to TLA Concepts

Technically a TLA+ operator is better understood as a Clojure macro rather than a Clojure function. However, since Clojure functions are easier to write and higher order functions are very natural to write, the decision was taken to model TLA+ operators as Clojure functions. This does not cause issues because the functions are never applied without having all of the variables bound. Whether they are applied or structurally substituted at that point does not matter.

In a way TLA+ functions might be usefully considered as Clojure functions. But, of course Clojure maps can be used as Clojure functions.

Standard Modules

Portions of some of the TLA+ standard modules have been implemented. They can be referenced from a salt file as follows:

  (:require [salt.lang :refer :all]
            [tlaplus.FiniteSets :refer :all]
            [tlaplus.Integers :refer :all]
            [tlaplus.Naturals :refer :all]
            [tlaplus.Sequences :refer :all])

The salt transpiler will detect these values in the salt source file and produce the corresponding EXTENDS statement in the TLA+ output.

Docs

Primitives

Integers are represented the same in salt and TLA+:

Strings are sequences of characters

Symbols are identifiers. For example "x" is a symbol in the following:

Boolean literals:

Code Structure

Let statements are used to establish bindings between symbols and values:

Conditional statements are expressed as:

To perform many checks on a value use 'cond'. NOTE: cond only allows one condition to be applied, whereas with TLA+ all matching conditions are possible results.

Arithmetic

Arithmetic on integers:

Subtraction

Multiplication

Integer division

Integer division results are truncated

Compute the modulus of two numbers.

Compute exponentiation

Refer to the set of natural numbers. The clojure version of this uses a very small set of natural numbers by default. NOTE: Nat is invoked as a function in clojure so that the upper limit can be dynamically bound, if necessary for testing.

Logic

Use standard logic operators

The 'or' operator

Specify that if x is true then y must be true as well

Use the TLA+ <=> operator

Check for equality

Equality works on complex types

Check for two items not being equal to each other

Use the standard inequality operators:

Specify something is true for some item in a set.

Specify something is true for all items in a set

Specs

Start a spec with a standard namespace declaration.

Define the CONSTANTS, which serve as a sort of 'input' to the specification and define the scope of the model.

Make assertions about constants

Define the variables that make up the state:

Reference the variables via the convenience identifier VARS-

Specify the initial state predicate.

In action predicates reference primed variable symbols.

Indicate variables that are not changed

As a departure from TLA+, just the changed variables can be indicated instead. This implies that other variables are unchanged.

Include horizontal separator lines in the spec to delimit sections.

Include comments in the spec.

Comments can be multi-line

Temporal Logic

Say something is always true

Say something is eventually true

Say that something being true leads to something else being true

Specify weak fairness

Specify strong fairness

Sets

Set literals are defined as:

A sequence of values is defined with range* Note that range* produces a set and is inclusive of the final value to match TLA+ semantics.

Standard set operations come from the clojure.set namespace

Collapse many sets into one with UNION

The cartesian product of two sets is computed by the 'X' operator

Check if a set is a subset of another

Define all of the sets that can be made from a set of values.

Check if a item is contained in a set.

Filter the values in a set to be those matching a predicate

Apply a function to all elements of a set

Compute the size of a set

Use the TLA+ CHOOSE operator.

Vectors

Clojure vector literals are TLA+ tuples:

Extract the first item from a vector:

Extract a value by index. NOTE: the index starts with 1.

Produce a new vector containing all but the first item:

Produce a new vector with one element changed:

Combine the contents of two vectors into a new vector

Combine two strings, which TLA+ treats as tuples:

Compute the length of a vector or string

Extract a subsequence by index from a vector

Filter out the values in a vector

Add an item to the end of a vector

Generate all possible vectors from a set of values.

The idiom of calling 'every?*' with a set as a predicate translates into a corresponding TLA+ idiom for checking a TLA+ tuple.

Compute all of the indexes present in a vector

Convert a vector to a set

Maps

Use 'maps-' to generate all possible maps for a set of possible keys and a set of possible values.

Define a map via 'fm-'.

Use 'defm-' to define a map like with 'fm-', but assign the result a name.

Extract a value by key.

Maps As Records

Map literals whose keys are keywords become TLA+ records, which are a special type of a TLA+ function

Access the values in a TLA+ record.

Use 'DOMAIN' on maps to obtain the keys.

Produce a new TLA+ record with modified values, like assoc-in

Produce a new nested TLA+ record with modified values, like assoc-in

Produce a new TLA+ record with new values computed by lambda function, like update-in

Produce a new TLA+ record with new values and with lambdas, like combining assoc-in and update-in

Use 'maps-' to generate all possible TLA+ records for pairs of keys and value sets

Define a map via 'fm-', will auto-convert to a TLA+ record.

Maps As Tuples

Maps whose keys start with 1 and proceed in increments of 1 are treated as TLA+ tuples.

Use 'DOMAIN' on maps that correspond to TLA+ tuples.

Extract a value from a TLA+ tuple by index. NOTE: the index starts with 1.

Define a map via 'fm-', will auto-convert to a TLA+ tuple

Functions

Define a function using fn. Depending on the context it will be transpiled to different forms.

Define a new TLA+ operator with defn:

Use a docstring with defn

Invoke a function as normal:

Define a recursive function:

Define a higher-order function:

Define functions that take no arguments as usual:

Define functions that take no arguments as usual (with docstring):

Invoke a function with no arguments.

Define TLA+ operators that only rely on constants with def:

Reference a TLA+ operator that only relies on constants

Example Salt

The following is a full sample salt file:

(comment "example spec ported from
https://github.com/tlaplus/Examples/blob/master/specifications/transaction_commit/TwoPhase.tla")

(ns TwoPhase
  (:require [salt.lang :refer :all]))

(CONSTANT RM)

(VARIABLE
 rmState
 tmState
 tmPrepared
 msgs)

(defn Message [] (union (maps- [:type #{"Prepared"}
                                :rm RM])
                        (maps- [:type #{"Commit" "Abort"}])))

(defn TPTypeOk []
  (and (contains? (maps- RM #{"working" "prepared" "committed" "aborted"}) rmState)
       (contains? #{"init" "committed" "aborted"} tmState)
       (subset? tmPrepared RM)
       (subset? msgs Message)))

(defn TPInit []
  (and (= rmState (fm- [rm RM]
                       "working"))
       (= tmState "init")
       (= tmPrepared #{})
       (= msgs #{})))

(defn TMRcvPrepared [rm]
  (and (= tmState "init")
       (contains? msgs {:type "Prepared"
                        :rm rm})
       (= tmPrepared' (union tmPrepared #{rm}))
       (CHANGED- [tmPrepared])))

(defn TMCommit []
  (and (= tmState "init")
       (= tmPrepared RM)
       (= tmState' "committed")
       (= msgs' (union msgs #{{:type "Commit"}}))
       (CHANGED- [tmState msgs])))

(defn TMAbort []
  (and (= tmState "init")
       (= tmState' "aborted")
       (= msgs' (union msgs #{{:type "Abort"}}))
       (CHANGED- [tmState msgs])))

(defn RMPrepare [rm]
  (and (= (get* rmState rm) "working")
       (= rmState' (EXCEPT rmState [rm] "prepared"))
       (= msgs' (union msgs #{{:type "Prepared"
                               :rm rm}}))
       (CHANGED- [rmState msgs])))

(defn RMChooseToAbort [rm]
  (and (= (get* rmState rm) "working")
       (= rmState' (EXCEPT rmState [rm] "aborted"))
       (CHANGED- [rmState])))

(defn RMRcvCommitMsg [rm]
  (and (contains? msgs {:type "Commit"})
       (= rmState' (EXCEPT rmState [rm] "committed"))
       (CHANGED- [rmState])))

(defn RMRcvAbortMsg [rm]
  (and (contains? msgs {:type "Abort"})
       (= rmState' (EXCEPT rmState [rm] "aborted"))
       (CHANGED- [rmState])))

(defn TPNext []
  (or (TMCommit)
      (TMAbort)
      (E [rm RM]
         (or (TMRcvPrepared rm)
             (RMPrepare rm)
             (RMChooseToAbort rm)
             (RMRcvCommitMsg rm)
             (RMRcvAbortMsg rm)))))

(defn TPSpec []
  (and (TPInit)
       (always- (TPNext) [rmState tmState tmPrepared msgs])))

Example TLA

The following is a full sample TLA+ output produced by the salt file above:

---------------------------- MODULE TwoPhase ----------------------------

(*
example spec ported from
https://github.com/tlaplus/Examples/blob/master/specifications/transaction_commit/TwoPhase.tla
*)
CONSTANT RM

VARIABLE rmState, tmState, tmPrepared, msgs

Message == [type : {"Prepared"},
            rm : RM] \union [type : { "Commit", "Abort" }]

TPTypeOk == 
    /\  rmState \in [RM -> { "committed", "prepared", "aborted", "working" }]
    /\  tmState \in { "committed", "aborted", "init" }
    /\  tmPrepared \subseteq RM
    /\  msgs \subseteq Message

TPInit == 
    /\  rmState = [rm \in RM |-> "working"]
    /\  tmState = "init"
    /\  tmPrepared = {}
    /\  msgs = {}

TMRcvPrepared( rm ) ==
    /\  tmState = "init"
    /\  [type |-> "Prepared",
         rm |-> rm] \in msgs
    /\  tmPrepared' = tmPrepared \union {rm}
    /\  UNCHANGED << rmState, tmState, msgs >>

TMCommit == 
    /\  tmState = "init"
    /\  tmPrepared = RM
    /\  tmState' = "committed"
    /\  msgs' = msgs \union {[type |-> "Commit"]}
    /\  UNCHANGED << rmState, tmPrepared >>

TMAbort == 
    /\  tmState = "init"
    /\  tmState' = "aborted"
    /\  msgs' = msgs \union {[type |-> "Abort"]}
    /\  UNCHANGED << rmState, tmPrepared >>

RMPrepare( rm ) ==
    /\  rmState[rm] = "working"
    /\  rmState' = [rmState EXCEPT ![rm] = "prepared"]
    /\  msgs' = msgs \union {[type |-> "Prepared",
                              rm |-> rm]}
    /\  UNCHANGED << tmState, tmPrepared >>

RMChooseToAbort( rm ) ==
    /\  rmState[rm] = "working"
    /\  rmState' = [rmState EXCEPT ![rm] = "aborted"]
    /\  UNCHANGED << tmState, tmPrepared, msgs >>

RMRcvCommitMsg( rm ) ==
    /\  [type |-> "Commit"] \in msgs
    /\  rmState' = [rmState EXCEPT ![rm] = "committed"]
    /\  UNCHANGED << tmState, tmPrepared, msgs >>

RMRcvAbortMsg( rm ) ==
    /\  [type |-> "Abort"] \in msgs
    /\  rmState' = [rmState EXCEPT ![rm] = "aborted"]
    /\  UNCHANGED << tmState, tmPrepared, msgs >>

TPNext == 
    \/  TMCommit
    \/  TMAbort
    \/  \E rm \in RM :
            \/  TMRcvPrepared(rm)
            \/  RMPrepare(rm)
            \/  RMChooseToAbort(rm)
            \/  RMRcvCommitMsg(rm)
            \/  RMRcvAbortMsg(rm)

TPSpec == 
    /\  TPInit
    /\  [][TPNext]_<< rmState, tmState, tmPrepared, msgs >>


=============================================================================

Change Log

2019/08/19 version 0.0.2 Introduced symbolic evaluator that evaluates where possible and then simplifies for testing action predicates.

Copyright

Copyright (c) 2019, ViaSat Inc. All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, PUNITIVE, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.