Skip to content
No description, website, or topics provided.
Clojure
Branch: master
Clone or download

README.md

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.

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

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

Clojure Clojure example TLA+ TLA+ example
set #{1 2} set {1, 2}
vector [1 2] tuple <<1, 2>>
map {1 10 2 20} function (1 :> 10 @@ 2 :> 20)
map {:a 10 :b 20} record [a |-> 100, b |-> 200]
function (defn Add [x y] (+ 1 2)) operator Add( x, y ) == x + y
lambda (fn [x] (> x 2)) lambda in SelectSeq LAMBDA x: (x > 2)
lambda #(* 2 %) lambda in Except @ * 2

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+:

salt tla+
code 1 1
result 1 1

Strings are sequences of characters

salt tla+
code "hello" "hello"
result "hello" "hello

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

salt tla+
code (let [x 1] x) LET x == 1
IN x
result 1 1

Boolean literals:

salt tla+
code true TRUE
result true TRUE
salt tla+
code false FALSE
result false FALSE

Code Structure

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

salt tla+
code (let [x 1 y 2] (+ x y)) LET x == 1
y == 2
IN x + y
result 3 3

Conditional statements are expressed as:

salt tla+
code (if true 100 0) IF TRUE
THEN 100
ELSE 0
result 100 100

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.

salt tla+
code (let
[x 3]
(cond (= x 1) true (= x 2) true (= x 3) 7 :default false))
LET x == 3
IN CASE
(x = 1) -> TRUE
[] (x = 2) -> TRUE
[] (x = 3) -> 7
[] OTHER -> FALSE
result 7 7

Arithmetic

Arithmetic on integers:

salt tla+
code (+ 1 2) 1 + 2
result 3 3

Subtraction

salt tla+
code (- 3 2) 3 - 2
result 1 1

Multiplication

salt tla+
code (* 3 2) 3 * 2
result 6 6

Integer division

salt tla+
code (div 10 2) 10 \\div 2
result 5 5

Integer division results are truncated

salt tla+
code (div 9 2) 9 \\div 2
result 4 4

Compute the modulus of two numbers.

salt tla+
code (mod* 10 3) 10 % 3
result 1 1

Compute exponentiation

salt tla+
code (expt 2 3) 2^3
result 8 8

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.

salt tla+
code (contains? (Nat) 2) 2 \\in Nat
result true TRUE

Logic

Use standard logic operators

salt tla+
code (and true false) /\ TRUE
/\ FALSE
result false FALSE

The 'or' operator

salt tla+
code (or true false) \/ TRUE
\/ FALSE
result true TRUE

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

salt tla+
code (=> true false) TRUE => FALSE
result false FALSE

Use the TLA+ <=> operator

salt tla+
code (<=> true false) TRUE <=> FALSE
result false FALSE

Check for equality

salt tla+
code (= 5 5) 5 = 5
result true TRUE

Equality works on complex types

salt tla+
code (= #{"a" "b"} #{"a" "b"}) { "a", "b" } = { "a", "b" }
result true TRUE

Check for two items not being equal to each other

salt tla+
code (not= 1 2) 1 # 2
result true TRUE

Use the standard inequality operators:

salt tla+
code [(< 1 2) (<= 1 1) (> 2 1) (>= 2 2)] << (1 < 2), (1 <= 1), (2 > 1), (2 >= 2) >>
result [true true true true] <<TRUE, TRUE, TRUE, TRUE>>

Specify something is true for some item in a set.

salt tla+
code (E [x #{1 3 2}] true) \\E x \\in { 1, 3, 2 } :
TRUE
result true TRUE

Specify something is true for all items in a set

salt tla+
code (A [x #{1 3 2}] (> x 2)) \\A x \\in { 1, 3, 2 } :
x > 2
result false FALSE

Specs

Start a spec with a standard namespace declaration.

salt tla+
code (ns
Buffer
(:require
[salt.lang :refer :all]
[tlaplus.Naturals :refer :all]
[tlaplus.Sequences :refer :all]))
---------------------------- MODULE Buffer ----------------------------
EXTENDS Naturals, Sequences

result

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

salt tla+
code (CONSTANT Clients Servers Data) CONSTANT Clients, Servers, Data

result

Make assertions about constants

salt tla+
code (ASSUME (and (subset? Clients Servers) (< Limit 100))) ASSUME
/\ Clients \\subseteq Servers
/\ Limit < 100

result TRUE

Define the variables that make up the state:

salt tla+
code (VARIABLE messages leaders) VARIABLE messages, leaders

result

Reference the variables via the convenience identifier VARS-

salt tla+
code VARS- << messages, leaders >>
result [messages leaders] << messages, leaders >>

Specify the initial state predicate.

salt tla+
code (and (= messages []) (= leaders #{})) /\ messages = << >>
/\ leaders = {}
result

In action predicates reference primed variable symbols.

salt tla+
code (and (= messages' []) (= leaders' #{})) /\ messages' = << >>
/\ leaders' = {}
result

Indicate variables that are not changed

salt tla+
code (UNCHANGED [messages leaders]) UNCHANGED << messages, leaders >>
result true

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

salt tla+
code (CHANGED- [leaders]) UNCHANGED << messages >>
result true

Include horizontal separator lines in the spec to delimit sections.

salt tla+
code (line-) --------------------------------------------------------------------------------
result

Include comments in the spec.

salt tla+
code (comment "this is a single line comment")
\\* this is a single line comment
result

Comments can be multi-line

salt tla+
code (comment "this is a\\nmulti line comment")
(*
this is a
multi line comment
*)
result

Temporal Logic

Say something is always true

salt tla+
code (always- (Next) vars) [][Next]_vars
result

Say something is eventually true

salt tla+
code (eventually- (Done)) <>Done
result

Say that something being true leads to something else being true

salt tla+
code (leads-to- P Q) P ~> Q
result

Specify weak fairness

salt tla+
code (WF vars (Next)) WF_vars(Next)
result

Specify strong fairness

salt tla+
code (SF vars (Next)) SF_vars(Next)
result

Sets

Set literals are defined as:

salt tla+
code #{1 3 2} { 1, 3, 2 }
result #{1 3 2} {1, 2, 3}

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.

salt tla+
code (range* 2 5) 2..5
result #{4 3 2 5} {2 3 4 5}

Standard set operations come from the clojure.set namespace

salt tla+
code [(union #{1 2} #{3 2})
(difference #{1 2} #{3 2})
(intersection #{1 2} #{3 2})]
<< ({ 1, 2 } \\union { 3, 2 }), ({ 1, 2 } \\ { 3, 2 }), ({ 1, 2 } \\intersect {
3, 2 }) >>
result [#{1 3 2} #{1} #{2}] <<{1, 2, 3}, {1}, {2}>>

Collapse many sets into one with UNION

salt tla+
code (UNION #{#{4 3} #{3 5} #{1 2}}) UNION { { 4, 3 }, { 3, 5 }, { 1, 2 } }
result #{1 4 3 2 5} {1, 2, 3, 4, 5}

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

salt tla+
code (X #{1 3 2} #{"a" "b"}) { 1, 3, 2 } \\X { "a", "b" }
result #{[2 "b"] [3 "a"] [2 "a"] [1 "a"] [1 "b"] [3 "b"]} {<<1, "a">>, <<1, "b">>, <<2, "a">>, <<2, "b">>, <<3, "a">>, <<3, "b">>}

Check if a set is a subset of another

salt tla+
code (subset? #{1 3} #{1 4 3 2}) { 1, 3 } \\subseteq { 1, 4, 3, 2 }
result true TRUE

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

salt tla+
code (SUBSET #{1 3 2}) SUBSET { 1, 3, 2 }
result #{#{} #{3} #{2} #{1} #{1 3 2} #{1 3} #{1 2} #{3 2}} {{}, {1}, {2}, {3}, {1, 2}, {1, 3}, {2, 3}, {1, 2, 3}}

Check if a item is contained in a set.

salt tla+
code (contains? #{1 3 2} 2) 2 \\in { 1, 3, 2 }
result true TRUE

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

salt tla+
code (select (fn [x] (> x 10)) #{15 5}) { x \\in { 15, 5 } :
x > 10 }
result #{15} {15}

Apply a function to all elements of a set

salt tla+
code (map* (fn [x] (+ 1 x)) #{1 2}) { 1 + x :
x \\in { 1, 2 } }
result #{3 2} {2, 3}

Compute the size of a set

salt tla+
code (Cardinality #{20 10}) Cardinality( { 20, 10 } )
result 2 2

Use the TLA+ CHOOSE operator.

salt tla+
code (CHOOSE [x #{1 3 2}] (>= x 3)) CHOOSE x \\in { 1, 3, 2 } : (x >= 3)
result 3 3

Vectors

Clojure vector literals are TLA+ tuples:

salt tla+
code [1 "a"] << 1, "a" >>
result [1 "a"] <<1, "a">>

Extract the first item from a vector:

salt tla+
code (first [1 "a"]) Head(<< 1, "a" >>)
result 1 1

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

salt tla+
code (get* [10 20 30] 2) << 10, 20, 30 >>[2]
result 20 20

Produce a new vector containing all but the first item:

salt tla+
code (rest* [1 "a"]) Tail(<< 1, "a" >>)
result ["a"] <<"a">>

Produce a new vector with one element changed:

salt tla+
code (EXCEPT [10 20 30] [2] 200) [<< 10, 20, 30 >> EXCEPT ![2] = 200]
result [10 200 30] <<10, 200, 30>>

Combine the contents of two vectors into a new vector

salt tla+
code (into [1 "a"] [2]) << 1, "a" >> \\o << 2 >>
result [1 "a" 2] <<1, "a", 2>>

Combine two strings, which TLA+ treats as tuples:

salt tla+
code (str "hel" "lo") "hel" \\o "lo"
result "hello" "hello"

Compute the length of a vector or string

salt tla+
code [(count [1 "a"]) (count "hello")] << Len( << 1, "a" >> ), Len( "hello" ) >>
result [2 5] <<2, 5>>

Extract a subsequence by index from a vector

salt tla+
code (SubSeq [10 20 30 40] 2 3) SubSeq(<< 10, 20, 30, 40 >>, 2, 3)
result [20 30] <<20, 30>>

Filter out the values in a vector

salt tla+
code (SelectSeq (fn [x] (> x 2)) [1 2 3 4]) SelectSeq(<< 1, 2, 3, 4 >>, LAMBDA x: (x > 2))
result [3 4] <<3, 4>>

Add an item to the end of a vector

salt tla+
code (conj [1 2] 3) Append(<< 1, 2 >>, 3)
result [1 2 3] <<1, 2, 3>>

Generate all possible vectors from a set of values.

salt tla+
code (Seq #{100 200}) Seq( { 100, 200 } )
result #{[100] [100 200 200] [200 100 200] [200 200] [200 100 100]
[100 200] [] [100 100] [100 200 100] [200 200 200]
[100 100 100] [200 200 100] [200] [200 100] [100 100 200]}
Seq({100, 200})

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

salt tla+
code (every?* #{1 4 3 2 5} [1 3]) << 1, 3 >> \\in (Seq( { 1, 4, 3, 2, 5 } ))
result true TRUE

Compute all of the indexes present in a vector

salt tla+
code (DOMAIN [10 20 30]) DOMAIN << 10, 20, 30 >>
result #{1 3 2} 1..3

Convert a vector to a set

salt tla+
code (map* (fn [i] (get* [10 20 30] i)) (DOMAIN [10 20 30])) { << 10, 20, 30 >>[i] :
i \\in DOMAIN << 10, 20, 30 >> }
result #{20 30 10} {10, 20, 30}

Maps

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

salt tla+
code (maps- #{20 10} #{100 200}) [{ 20, 10 } -> { 100, 200 }]
result #{{20 100, 10 200} {20 200, 10 100} {20 100, 10 100}
{20 200, 10 200}}
{ (10 :> 100 @@ 20 :> 100),
(10 :> 100 @@ 20 :> 200),
(10 :> 200 @@ 20 :> 100),
(10 :> 200 @@ 20 :> 200) }

Define a map via 'fm-'.

salt tla+
code (fm- [a #{20 10}] 30) [a \\in { 20, 10 } |-> 30]
result {20 30, 10 30} (10 :> 30 @@ 20 :> 30)

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

salt tla+
code (defm- MyMaps [a #{1 2}] (* a 10)) MyMaps == [a \\in { 1, 2 } |-> (a * 10)]

result

Extract a value by key.

salt tla+
code (get* (fm- [a #{20 10}] (* a 10)) 10) [a \\in { 20, 10 } |-> (a * 10)][10]
result 100 100

Maps As Records

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

salt tla+
code {:a 100, :b 200} [a |-> 100,
b |-> 200]
result {:a 100, :b 200} [a |-> 100, b |-> 200]

Access the values in a TLA+ record.

salt tla+
code (get* {:a 100, :b 200} :b) [a |-> 100,
b |-> 200]["b"]
result 200 200

Use 'DOMAIN' on maps to obtain the keys.

salt tla+
code (DOMAIN {:a 100, :b 200}) DOMAIN [a |-> 100,
b |-> 200]
result #{:b :a} {"a", "b"}

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

salt tla+
code (EXCEPT {:a 1, :b 2, :c 3} [:b] 20) [[a |-> 1,
b |-> 2,
c |-> 3] EXCEPT !["b"] = 20]
result {:a 1, :b 20, :c 3} [a |-> 1, b |-> 20, c |-> 3]

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

salt tla+
code (EXCEPT
{:a {:x 1, :y 10}, :b {:x 2, :y 20}, :c {:x 3, :y 30}}
[:b :x]
200)
[[a |-> [x |-> 1,
y |-> 10],
b |-> [x |-> 2,
y |-> 20],
c |-> [x |-> 3,
y |-> 30]] EXCEPT !["b"]["x"] = 200]
result {:a {:x 1, :y 10}, :b {:x 200, :y 20}, :c {:x 3, :y 30}} [ a |-> [x |-> 1, y |-> 10],
b |-> [x |-> 200, y |-> 20],
c |-> [x |-> 3, y |-> 30] ]

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

salt tla+
code (EXCEPT {:a {:x 1 :y 10}
:b {:x 2 :y 20}
:c {:x 3 :y 30}}
[:b :x]
#(* % 2))
[[a |-> [x |-> 1,
y |-> 10],
b |-> [x |-> 2,
y |-> 20],
c |-> [x |-> 3,
y |-> 30]] EXCEPT !["b"]["x"] = @ * 2]
result {:a {:x 1, :y 10}, :b {:x 4, :y 20}, :c {:x 3, :y 30}} [[
a |-> [
x |-> 1,
y |-> 10],
b |-> [
x |-> 2,
y |-> 20],
c |-> [
x |-> 3,
y |-> 30]] EXCEPT !["b"]["x"] = @ * 2]

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

salt tla+
code (EXCEPT {:a {:x 1 :y 10}
:b {:x 2 :y 20}
:c {:x 3 :y 30}}
[:b :x] #(* % 2)
[:a] "new")
[[a |-> [x |-> 1,
y |-> 10],
b |-> [x |-> 2,
y |-> 20],
c |-> [x |-> 3,
y |-> 30]] EXCEPT
!["b"]["x"] = @ * 2,
!["a"] = "new"]
result {:a "new", :b {:x 4, :y 20}, :c {:x 3, :y 30}} [a |-> "new", b |-> [x |-> 4, y |-> 20], c |-> [x |-> 3, y |-> 30]]

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

salt tla+
code (maps- [:name #{"bob" "sue"} :age #{20 10}]) [name : { "bob", "sue" },
age : { 20, 10 }]
result #{{:name "sue", :age 20} {:name "bob", :age 20}
{:name "sue", :age 10} {:name "bob", :age 10}}
{[name |-> "bob", age |-> 10], [name |-> "bob", age |-> 20], [name |-> "sue", age |-> 10], [name |-> "sue", age |-> 20]}

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

salt tla+
code (fm- [a #{"a" "b"}] 30) [a \\in { "a", "b" } |-> 30]
result {"a" 30, "b" 30} [a |-> 30, b |-> 30]

Maps As Tuples

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

salt tla+
code {1 100, 2 200} << 100, 200 >>
result {1 100, 2 200} <<100, 200>>

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

salt tla+
code (DOMAIN {1 100, 2 200}) DOMAIN << 100, 200 >>
result #{1 2} 1..2

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

salt tla+
code (get* {1 100, 2 200} 1) << 100, 200 >>[1]
result 100 100

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

salt tla+
code (fm- [a #{1 2}] (* a 10)) [a \\in { 1, 2 } |-> (a * 10)]
result {1 10, 2 20} <<10, 20>>

Functions

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

salt tla+
code [(SelectSeq (fn [x] (> x 2)) [1 2 3 4])
(map* (fn [x] (+ 1 x)) #{1 2})]
<< (SelectSeq(<< 1, 2, 3, 4 >>, LAMBDA x: (x > 2))), (
{ 1 + x :
x \\in { 1, 2 } }) >>
result [[3 4] #{3 2}] <<<<3, 4>>, {2, 3}>>

Define a new TLA+ operator with defn:

salt tla+
code (defn Add [x y] (+ x y)) Add( x, y ) ==
x + y

result

Use a docstring with defn

salt tla+
code (defn Add "docstring" [x y] (+ x y))
\\* docstring
Add( x, y ) ==
x + y

result

Invoke a function as normal:

salt tla+
code (Add 1 2) Add(1, 2)
result 3 3

Define a recursive function:

salt tla+
code (defn Add [x r] (if (> x 5) (Add (- x 1) (+ r 1)) r)) RECURSIVE Add(_, _)

Add( x, r ) ==
IF (x > 5)
THEN Add((x - 1), (r + 1))
ELSE r

result

Define a higher-order function:

salt tla+
code (defn Work [f a b] (f a b)) Work( f(_, _), a, b ) ==
f(a, b)

result

Define functions that take no arguments as usual:

salt tla+
code (defn Work [] (union a b)) Work == a \\union b

result

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

salt tla+
code (defn Work "docstring" [] (union a b))
\\* docstring
Work == a \\union b

result

Invoke a function with no arguments.

salt tla+
code (Work) Work
result

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

salt tla+
code (def Work (union A B)) Work == A \\union B

result

Reference a TLA+ operator that only relies on constants

salt tla+
code Work Work
result

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.

You can’t perform that action at this time.