TLX.Spec (TLX v0.5.2)

Copy Markdown

Use this module to define a TLA+ specification.

defmodule MySpec do
  use TLX.Spec

  variable :x, 0

  action :increment do
    guard(e(x < 5))
    next :x, e(x + 1)
  end

  invariant :bounded, e(x >= 0 and x <= 5)
end

Or use the shorthand defspec:

import TLX

defspec MySpec do
  variable :x, 0

  action :increment do
    guard(e(x < 5))
    next :x, e(x + 1)
  end

  invariant :bounded, e(x >= 0 and x <= 5)
end

Options

  • :extensions (list of module that adopts Spark.Dsl.Extension) - A list of DSL extensions to add to the Spark.Dsl

  • :otp_app (atom/0) - The otp_app to use for any application configurable options

  • :fragments (list of module/0) - Fragments to include in the Spark.Dsl. See the fragments guide for more.