Build type	Status
Release
Debug

Table of contents

1. Introduction
2. Installing the Tau Language Framework
   1. Linux
   2. Windows
   3. MacOS
   4. Compiling the source code
3. Quick start
   1. Run a spec with the interpreter (tau)
   2. Compile a spec to an executable (tau compile)
4. The Tau Language
   1. Tau specifications
   2. Full LTL operators
   3. CTL* fragment and semantic negation
   4. Satisfiability and execution
   5. Boolean functions
   6. Bitvectors
   7. Functions and predicates
   8. Constants
   9. Streams
   10. Variables and uninterpreted constants
   11. Type system
   12. Abstract data types
   13. Constant time constraints
   14. Pointwise revision
   15. Reserved symbols
5. Command line interface
6. The Tau REPL
   1. Basic REPL commands
   2. REPL options
   3. Functions, predicates and input/output stream variables
   4. Memory related commands
   5. Expression manipulation
   6. Logical procedures
   7. Normal forms
   8. Specification execution
7. Web IDE
8. Developer infrastructure for ω-categorical synthesis
9. The C++ API and language bindings
10. The Theory behind the Tau Language
11. Known issues
12. Future work
13. Submitting issues
14. License
15. Authors

Introduction

The Tau language is an expressive, decidable and executable formal software specification language. It allows for specifying software using requirements and constraints in a purely logical and declarative approach. Tau specifications can be checked for satisfiability, effectively deciding if there exists a program matching the specification. Furthermore, the Tau framework is able to synthesize a program adhering to a satisfiable specification.

Imagine programming by writing the tests only, while getting a working program automatically which is guaranteed to pass all the tests, thus meeting all the specified requirements.

A unique feature of the Tau language is the ability to specify programs capable of mechanized deductive reasoning over Tau specifications themselves. This allows for a controlled adaption of new requirements because the requirements for the requirements can be taken into account, which is useful for collaborative specification, maintenance, updates, safety and user control.

To go to the quick start click here.

To go to the installation guide click here.

For viewing known issues, future work and how to submit issues, click here.

For visiting the theory behind the Tau Language click here.

Please note that the Tau language is work in progress. Releases are currently in an alpha state and can contain bugs. See the submitting issues section if you want to submit a report. All features discussed below in this readme are available but can have performance issues.

Installing the Tau Language Framework

Linux

Currently, we automatically build the following binaries packages (AMD64 and ARM64 architectures):

• deb (Debian/Ubuntu): tau-0.7-Linux.deb
• rpm (Fedora): tau-0.7-Linux.rpm

• tau runs and interprets specs.
• tau-sdk compiles native specs into programs and links against Tau.
• tau-sdk-windows-x86_64-mingw is the same box for the Windows (MinGW) target. It is not a release package. Build it with ./dev preset release-w64-sdk-packages-deb (or -rpm).
• tau-sdk-wasm32-emscripten is the same box for the WebAssembly target.
• tau-sdk-linux-arm64 is the same box for the Linux arm64 target on an x86 host. It is not a release package. Build it with ./dev preset release-arm64-sdk-packages-deb (or -rpm). The ARM64 release packages carry the native tau-sdk.

Install the SDK for each platform you target: one box carries one platform's archive, headers, bundled dependencies, presets and toolchain, and nothing of another. All boxes share the prefix and install under /usr/lib/tau/sdk/<platform>/.

The executable is installed in /usr/bin/tau.

Windows

For windows, we provide a convenient installer that includes the tau executable and also a zip file:

• Installer: tau-0.7-win64.exe
• Zip file: tau-0.7-win64.zip

To build the installer (NSIS) and the zip archive yourself, on a Windows machine with the Visual Studio build tools, use ./dev preset release-msvc-packages and ./dev preset release-msvc-packages-zip; on an arm64 Windows machine, use ./dev preset release-msvc-arm64-packages and ./dev preset release-msvc-arm64-packages-zip. From Linux, the MinGW cross-build gives the same two artifacts with ./dev preset release-w64-packages and ./dev preset release-w64-packages-zip.

MacOS

The release pipeline builds a .dmg installer and a .zip archive for Apple Silicon (arm64) and Intel (x86_64) Macs; they will be published with the next release. Until then, build Tau from source (see below), or build the packages yourself with ./dev preset release-packages-macos.

Compiling the source code

To compile the source code you need a C++ compiler supporting C++23: GCC 13.3 or newer, or Clang 19 or newer (Clang 18 crashes while instantiating the tree pack in src/instantiate_pack.cpp). You also need at least cmake version 3.22.1 installed in your system. tau compile builds against the tau SDK of the running binary, with cmake's compiler and a Release build type. --cxx or TAU_CXX names another compiler, and --preset targets another platform's SDK box. The code dependencies are the Boost C++ Libraries (including Boost.Log), CVC5, libcurl, and Spot (ltlsynt, autfilt, ltlfilt) for LTL synthesis. CVC5 is used only in order to support the theory of bitvectors within the language. The core language and its algorithms are independent of CVC5.

On Ubuntu 22.04, the CI dependency set can be installed with:

./scripts/setup-ubuntu-ci-deps.sh

The CI build intentionally uses fixed tools and pinned transient dependencies: GCC/G++ 13, Ninja, Spot from the home:adl package repository, cvc5 1.3.1, and doctest v2.4.11 verified by SHA-256 during CMake configure. This avoids depending on moving upstream defaults when reproducing CI locally.

After cloning:

git clone https://github.com/IDNI/tau-lang.git

all build and test operations go through the ./dev helper, which dispatches to the scripts in scripts/. Run ./dev with no arguments to list them, and see scripts/README.md for the details of option handling, parallel jobs and build directories.

The parser is a git submodule at external/parser/; ./dev initializes it automatically on first use.

Dependencies resolve from the local store at ~/.tau/store. Configure reads a missing package from the remote store named by TAU_STORE_REMOTE (a private GHCR OCI artifact per entry) and, when that has none either, builds it with the preset's compiler. ./dev store-pull prefetches named entries and ./dev store-publish uploads the local entries the remote lacks.

To build the binaries:

./dev release          # Release build          -> build-Release/
./dev debug            # Debug build            -> build-Debug/
./dev relwithdebinfo   # Release + debug info   -> build-RelWithDebInfo/

Alternatively, use the CMake presets declared in CMakePresets.json, which build into build/<build type> (e.g. build/release; a non-default toolchain adds -gcc, -w64, -msvc or -msvc-cl, and the wasm family -wasm):

./dev preset release-tau run -- --help
./dev preset release-tests run

To build with doxygen documentation, pass -DTAU_BUILD_DOC=ON to any of the build scripts:

./dev release -DTAU_BUILD_DOC=ON

To build and run the test suites (please run both, as Debug and Release builds enable different assertions):

./dev test-release
./dev test-debug

To build the Python bindings (see The C++ API and language bindings):

./dev binding python

Once you have compiled the source code you can run the tau executable to execute Tau specifications. The tau executable is located in either build-Release or build-Debug or build-RelWithDebInfo (or in build/<build type> when building with presets).

The same binary also carries the compile verb, which turns a realizable specification into a standalone executable (see Compile a spec to an executable).

Selecting Boolean algebras (-DTAU_BAS=)

Each Boolean algebra (BA) is a plugin, and a build contains the set — the pack — chosen at configure time:

./dev preset release                              # the default pack
./dev preset release -DTAU_BAS=tau,sbf,bv         # drop qlt, qint, nlang, hsb
./dev preset release -DTAU_BAS=sbf,tau            # smallest useful pack

tau is the wrapper algebra that embeds a whole Tau spec as a value; the other ids are base algebras. A BA's dependencies are declared in its own manifest, so a pack without bv and hsb does not need CVC5, and one without nlang does not need libcurl. Referencing the type of an algebra the build does not contain is reported as an unknown type annotation, listing the ones it does contain.

Some internal machinery — the state bits of an LTL synthesis, a CTL* witness output — needs a type holding a plain 0 or 1. Which algebra provides it is the Boolean carrier, chosen from an ordered preference:

./dev preset release -DTAU_BOOL_CARRIERS=bv,sbf,bool   # the default order
./dev preset release -DTAU_BOOL_CARRIERS=sbf           # prefer sbf even when bv is present

The first listed algebra the pack actually contains wins, so one order serves every pack: with the default, a pack with bv carries bits in bv[1] and a pack without it falls to sbf.

To add an algebra — in-tree or from outside the source tree — copy src/boolean_algebras/_template/ and follow docs/adding_base_bas.md.

Quick start

Tau-lang offers two ways to execute a specification:

1. Interpret the spec directly — solve each time step on the fly. Use tau. Best for iteration and REPL use.
2. Compile the spec to a standalone executable ahead of time. Use tau compile. Best for deployment: the program makes the moves tau makes. When tau plays a finite machine, the synthesis happens once, at compile time, and the program only steps that machine.

Both use the same spec language. You can start with the interpreter while authoring a spec and switch to the compiler for production.

Run a spec with the interpreter (tau)

# Start the REPL.
tau

# Or run a spec file directly.
tau spec.tau

# Or evaluate a REPL command inline.
tau -e "sat G(o1[t]:bv = i1[t]:bv)"

Full command-line reference. The interpreter is the right choice when you want to iterate on a spec, inspect intermediate results, or run short jobs from the shell.

Generate and compile a spec (tau gen, tau codegen, tau compile)

A spec becomes a standalone program in two steps. tau gen (also spelled tau codegen) parses the spec, prepares its execution exactly as the interpreter does, and writes a small CMake project next to the spec (<spec>.build/): one main.cpp that drives the strategy through the same run loop tau <spec> uses, plus a CMakeLists.txt that links the tau SDK and a CMakePresets.json with one preset per platform. tau compile runs gen and then configures and builds that project with the SDK script, and copies the program to the requested path. The program makes the moves run makes. When run plays the finite machine of the data game's strategy, the program carries that machine; otherwise run solves as it goes, and the program executes the embedded specification the same way.

# 1. Write a spec (mirror-input example).
echo 'G(o1[t]:bv = i1[t]:bv).' > spec.tau

# 2. Emit the artifact only, or emit and build in one command.
tau gen spec.tau          # `tau codegen spec.tau` is the same command
tau compile spec.tau -o sim

# 3. Run it: it reads inputs and prints outputs like the interpreter does
#    and exits when its input closes.
./sim

The program prints its errors and warnings on stderr. Unlike tau, it prints its benchmarks (the timed report of the run) only with -b / --benchmarks.

A spec file may be -, which reads stdin. Use - once in a tau gen or tau codegen file list. A spec path that names a directory is an error ("Cannot open file").

tau gen <spec.tau>... [-o, --output-dir <dir>] (also tau codegen) takes one or more spec files. Each spec writes its own <spec>.build/. A spec from stdin has no name, so it writes a.build/. -o (--output-dir) names one output directory. It is an error with more than one spec file.

tau gen --aiger <spec.tau> writes the AIGER circuit (ASCII aag) of a controller for the spec instead, to <spec>.aag (a.aag for stdin, the -o path when given). The spec must be LTL over bv[1] streams whose atoms compare bits (=, !=, <, <=, >, >= of terms with ', &, |, +, 0 and 1), with no CTL* operator (a circuit is one linear-time controller) and no update stream u. A fixed position x[k] is taken, except an input after step 0 under a temporal operator, which the circuit would have to guess at step 0. Each atom becomes a Boolean formula over the bits of its streams, a past read x[t-k] a history latch, a fixed position x[k] a latch that keeps x's value of step k, and ltlsynt --aiger --verify synthesizes and checks the circuit; the circuit's inputs and outputs are the input and output streams by name. It is a correct controller, not necessarily the one run executes: where the strategy leaves an output free, run picks it per step and the circuit fixes it. When ltlsynt's verdict on the circuit's formula and the verdict of realizable differ, nothing is written.

tau gen --machine <spec.tau> (also tau compile --machine) builds the program from the same bit game: ltlsynt --verify synthesizes and checks a Mealy machine over the stream bits, and the program plays it as a table, with the history copies and the bookkeeping as the machine's own state. The program neither synthesizes nor solves when it runs, so it needs no Spot and no solver at start. Like the circuit, it is a controller of the spec, not necessarily the one run executes: an output the machine leaves free is 0. A spec outside the --aiger fragment, a pack whose bit type is not bv[1], or a machine with more edges than --compile-max-table-edges gets the program that follows run, with a warning that names the reason. tau gen and tau compile print the warnings of a successful build, with or without --machine. The tests run each machine program, on fixed and on seeded random inputs, and check its trace against the spec (tests/repl/check_compile_machine.cmake).

tau compile - reads the spec from stdin. With no -o, it writes the artifact to a.build/ and the program to a.out (a.exe on Windows). With -o <exe>, it writes the program to <exe> and the artifact to <exe>.build/.

tau compile option	Description
-o, --output <path>	executable path. The default is the spec file path without extension, or a.out / a.exe for stdin
-c, --cxx <compiler>	C++ compiler for the emitted project. The default is TAU_CXX, else cmake's compiler, or the compiler of the --preset platform; --cxx wins over TAU_CXX
--preset <name>	target platform or ./dev preset name. Without it the build is native and uses the SDK of the running tau
--sdk-dir <dir>	directory of the tau SDK, the directory that holds TauConfig.cmake. The default is TAU_SDK_DIR, else the SDK found beside the running tau; --sdk-dir wins over TAU_SDK_DIR
-D NAME=VALUE	cmake cache variable for the emitted project configure (repeat as needed). A value wins over the preset
-G <generator>	cmake generator for the emitted project configure
--machine	play ltlsynt's verified machine of a bv[1] LTL spec as a table (see tau gen --machine above)

The cmake build stops, and the compile fails, after --compile-build-timeout seconds (TAU_COMPILE_BUILD_TIMEOUT, 3600 by default; 0 waits without bound). This is a global option, so it comes before compile: tau --compile-build-timeout 600 compile spec.tau.

Without --preset, tau compile builds for the machine tau runs on. It uses the tau SDK of its own build folder (<build>/sdk) or the installed box beside the binary, found by the path of the binary. cmake's default compiler builds the artifact. The build type is Release, unless a -DCMAKE_BUILD_TYPE=<type> is given. -D and -G reach the configure.

With --preset <name>, tau compile targets another platform. A platform is the build folder name ./dev preset uses: release, devel, debug, and their -gcc, -w64, -arm64, -msvc, -msvc-cl, -msvc-arm64, -msvc-cl-arm64, -wasm and -wasm-nothreads twins. -msvc is the clang-cl build, the default MSVC toolchain. -msvc-cl is the cl.exe build. The *-msvc-cl presets use the default pack. -msvc-arm64 and -msvc-cl-arm64 are the same two builds for Windows arm64, and they build on an arm64 Windows host only.

Any other ./dev preset name maps to the platform of its build folder, so --preset release-msvc-all builds with the release-msvc platform, and --preset release-msvc-cl-all with the release-msvc-cl platform. An unknown name fails and lists the platforms before any SDK lookup.

Each platform has an SDK at build/<platform>/sdk/. Build that platform first with ./dev preset <platform>. An installed box lives at <prefix>/lib/tau/sdk/<platform>/; install tau-sdk, tau-sdk-windows-x86_64-mingw, tau-sdk-wasm32-emscripten or tau-sdk-linux-arm64 for the platform you target. An MSVC SDK with bv needs clang-cl as the compiler of the artifact: cl.exe cannot compile the tau headers of a pack with bv.

The build runs the SDK script cmake/tau-compile.cmake. The same script serves the CLI and ./dev compile <dir>. Without a preset both build natively: the CLI uses the SDK of the running binary and ./dev compile uses build/release/sdk, with cmake's compiler and a Release build type. For a preset build the script configures with the artifact preset, uses the SDK box of the target platform, and checks its toolchain record against the host toolchain, so a cross build names the toolchain it needs.

The emitted project's CMakePresets.json carries one preset per platform and no path of the machine that ran tau gen (tau codegen). The project finds its box at configure time: TAU_SDK_DIR names the SDK box (the directory holding TauConfig.cmake), and tau compile and ./dev compile pass a source-tree box as -DTau_DIR. A missing box fails with no SDK for <platform>; install tau-sdk-<suffix> or build it with ./dev preset <platform>.

No build, store or source path goes into tau.

The exit code is 0 when the program was built and 1 on any failure; the reason (parse error, UNREALIZABLE, no verdict from the synthesis backend, a cmake configure or build failure) is in the compile failed: … message, not in a dedicated code. A spec without a strategy is called UNREALIZABLE only when realizable would answer F; when realizability is undecided the message says UNKNOWN and names the budget or the reason that stopped it. The global options, the budgets among them, are given before the verb (tau --ltl-timeout 120 compile spec.tau). A spec run cannot execute is refused the same way. An Algorithm-B verdict over the qlt type (see the synthesis algorithms below), whose strategy is over bookkeeping bits rather than the data, is not such a spec: run and tau compile solve it again by the default path and play the strategy of its abstraction or data game.

Full worked example: examples/reactive_program/ (the Makefile runs tau compile; its main.cpp documents the shape of the emitted tau_program class, which the library API build_program_desc + emit_program in src/cpp_codegen.h produces).

Correctness: synthesis produces a program whose behaviour is consistent with the spec on every input trace. Unrealizable specs are rejected up front.

Pointwise revision (PWR) happens before code generation: a spec already produced by PWR can be compiled and stepped like any other realizable spec. A spec whose tau-typed update stream u revises it while it runs is executed by the program as run executes it, revisions included.

See the command-line reference for the tau options.

---

To start using the Tau Language, download the latest release from the GitHub page. Once you have downloaded and installed the executable (see the Section Installing the Tau Framework), you can run it from the command line by typing tau.

The programming model underlying the Tau Language is fully declarative. You specify, possibly only very implicitly, how the current and previous inputs and outputs are related, at each point of time. As a result, you do not write a program in the Tau Language, but a specification which effectively represents all programs that meet this specification. Once you run a specification, you actually run one automatically-chosen representative program from that set.

In the scope of the Tau Language, a specification is satisfiable, loosely speaking, if for all inputs, at each point in time, there exist outputs, that do not depend on future inputs while matching the specification. Implied from this definition is that all specifications run indefinitely no matter what the inputs are.

For example, the following specification:

o1[t] = 0

states that the output o1 at all time points t has to be 0. Similarly, the following specification:

o1[t] = i1[t]

states that the output o1 has to be the same as the input i1 at all time points t. In the above examples, o1 and i1 are streams. They are used to define the inputs and outputs of the specification.

An example of how to define input and output streams is the following:

i1 : tau := in console
o1 : tau := out console

In the above case we specify that i1 and o1 are of type tau, namely that they are Tau specifications, and they take values from the console (e.g. stdin/stdout). The type defines from which Boolean algebra the values come from. The tau type is a unique property of the Tau langauge because it enables Tau specifications to reason over Tau specifications themselves abstracted as Boolean algebra elements.

You can also define files as input or output streams:

i1 : tau := in file("input.in")
o1 : tau := out file("output.out")

The above two examples, o1[t] = 0 and o1[t] = i1[t], define one program each (there's a caveat in this statement, but we shall ignore it here). This is not always the case. An example of a Tau specification that specifies infinitely many programs is

o1[t] & i1[t] = 0

because many different assignments to o1[t] can be chosen as valid output. Each choice represents one program. Here & denotes conjunction in the Boolean algebra from which the inputs and outputs are taken from. This specification says that the conjunction has to be empty.

Clearly, you can consider more complicated specifications, e.g.:

o1[t] & o1[t-1] & i1[t] = 0 || o1[t] = i1[t]

which states that at each point in time, either the conjunction of the current output with the previous output and with the current input, has to be 0, or, the output has to equal the input. Note the difference between Boolean (algebraic operations) and Logical operators . The former are &, |, ', and the latter are &&, ||, !.

In order to simplify the process of writing and running Tau specifications, we allow function and predicate definitions, possibly by means of recurrence relations. The following is a simple predicate defined by a recurrence relation, which takes as argument a Tau term:

f[0](y) := T
f[n](y) := f[n - 1](y)

which you can use in your specification as follows:

o1[t] = 0 && f(i1[t])

Also, you can use the following function definition by a recurrence relation:

g[0](y):sbf := 0
g[n](y):sbf := g[n - 1](y)'

which defines a function (rather than a predicate) and alternates between 0 and 1 depending on the parity of n in the sbf Boolean algebra (see below in Type System).

In the demos folder you can find lots of examples regarding how to use the Tau Language, its semantics and workings.

The Tau Language

The core idea of the Tau Language is to specify how current and previous inputs and outputs of a program are related over time, using the first-order theory of finite and infinite atomless Boolean algebras extended with a time dimension, represented by the natural numbers starting at 0. It was carefully crafted around being purely logical, allowing efficient and decidable satisfiability checking, while being executable, yielding a framework to enable program synthesis.

For example, you can write o1[t] & o1[t-1] & i1[t] = 0 which means that the current output o1[t], the previous output o1[t-1], and the current input i1[t], have to have an empty intersection. The set-theoretic perspective of Boolean algebra is given by Stone's representation theorem for Boolean algebras. More concretely, when a Tau specification is treated as a Boolean algebra element, it can be seen as a set of all programs that admit that specification, and the Boolean operations are the set-theoretic union/intersection and complementation.

A key feature is the ability of checking satisfiability of Tau specifications within Tau specifications using the theory of Boolean equations and an abstraction of specifications to Boolean algebra elements. This enables, in particular, a novel approach to software updates. A specification which is currently executed, can take as an input an arbitrary new Tau specification, seen as an update, check if the proposed new specification is satisfiable and incorporate the update into the existing specification using an operation we call pointwise revision. Section Pointwise revision provides a more detailed introduction to this feature and how to use it.

The following is a general introduction to using the Tau language.

Tau specifications

At the top level, a Tau specification (we also say spec) is a collection of G ("globally") and F ("finally/eventually") statements applied to local specifications (expressed by local_spec, see below), combined by the logical connectives and, or and not, denoted by &&, || and ! respectively. For example a well-formed Tau specification is

(G local_spec1) && (F local_spec2)

where local_spec1 and local_spec2 are formulas as described below. We say local specification because such a formula can only talk about a fixed (though arbitrary) point in time.

In order for a specification to communicate with the outside world, so-called streams are use. Those streams come in two flavors: input and output streams. Input streams are used in a local_spec to receive input from a user, while output streams are used for presenting output to a user. Streams can be given arbitrary names; the names i1, o1, ... used throughout this document are just a convention (see section Streams). Each stream in the specification is associated with a relative or constant point in time. For example the output stream variable o1[t-2] means "the value in output stream number 1 two time-steps ago". So o1[t] would mean "the value in output stream number 1 at the current time-step". Likewise, for input stream variables like i1[t]. It means "the input in the input stream 1 at the current time-step". Input streams can also have an offset in order to speak about past inputs. For example i2[t-3] means "the input in the input stream 2 three time-steps ago". For further detail about streams, please refer to section Streams.

In all above cases, t is a free variable and refers to the current time at each point in time. The key point now is that a G (globally) statement will quantify all scoped t universally, while an F (eventually) statement will quantify them existentially. For example the specification G o1[t] = 0 says that at all time-steps the output stream number 1 will write 0. Similarly, the specification F o1[t] = 0 says that there exists a time-step at which the output stream 1 will write 0. When executing a Tau specification, the first time-step is always 0.

A Tau specification without any temporal wrapper is implicitly assumed to be a G ("globally") statement. The same holds for each top-level conjunct, also beside temporal ones: a conjunct with no always, sometimes, until, release or weak_until (a bare formula, or one whose only temporal operators are since and trigger) holds at every step. o2[t] = 1 && (sometimes o1[t] = 1) reads as (always o2[t] = 1) && (sometimes o1[t] = 1), o1[1] = 1 && (sometimes o2[t] = 1) as (always o1[1] = 1) && (sometimes o2[t] = 1), and (o1[t] = 1) since (o2[t-1] = 1) must hold at every step its clause enforces, for sat, realizable and run alike.

Formally, a specification is a (possibly empty) list of definitions followed by a single formula, its main formula:

spec        => [ definitions ] local_spec [ "." ]
             | "G" local_spec          -- globally (always)
             | "F" local_spec          -- eventually (sometimes)
             | spec "U" spec           -- until
             | spec "R" spec           -- release
             | spec "W" spec           -- weak until
             | spec "S" spec           -- since (past LTL)
             | spec "T" spec           -- trigger (past LTL)
             | (spec && spec) | (spec || spec) | !spec
definitions => ( (function_def | predicate_def | stream_def | type_def) "." )+

where type_def declares an abstract data type (see Abstract data types) where local_spec is a formula defined by the rules:

local_spec => ("(" local_spec ")")
            | (("sometimes" | "<>") local_spec)
            | (("always"    | "[]") local_spec)
            | (local_spec "?" local_spec ":" local_spec)
            | ("all" variable ("," variable)* local_spec)
            | ("ex"  variable ("," variable)* local_spec)
            | (local_spec "->"  local_spec)
            | (local_spec "<-"  local_spec)
            | (local_spec "<->" local_spec)
            | (local_spec "||"  local_spec)
            | (local_spec "^^"  local_spec)
            | (local_spec "&&"  local_spec)
            | ("!" local_spec)
            | (term "=" term) | (term "!=" term)
            | (term "<" term) | (term "!<" term) | (term "<=" term) | (term "!<=" term)
            | (term ">" term) | (term "!>" term) | (term ">=" term)| (term "!>=" term)
            | (term "<=" term "<=" term)
            | time_constraint
            | predicate
            | T | F

The naming conventions for variable are discussed in Variables and uninterpreted constants. Furthermore, term is discussed in the sections Boolean functions and Bitvectors. Note that always and sometimes are ordinary formula-level operators, and a specification with no always or sometimes at all is implicitly an always statement. The predicate non-terminal in the above grammar describes how to add predicate definitions directly into a formula. See the subsection Functions and predicates for the grammar definition of predicate, and Constant time constraints for time_constraint. In the REPL (The Tau REPL) definitions can be provided as explained in subsection Functions, predicates and input/output stream variables.

The symbols used have the following meaning, where a formula refers to either local_spec or spec:

Symbol	Meaning
!	negation of formula
&&	conjunction of formulas
^^	xor of formulas
||	disjunction of formulas
<->	equivalence of formulas
<-	left-implication of formulas
->	right-implication of formulas
ex	existential quantification of one or more variables
all	universal quantification of one or more variables
... ? ... : ...	if ... then ... else ...
=	standard equality relation in BA or bitvectors
!=	standard inequality relation in BA or bitvectors
<	standard less relation in BA or bitvectors
!<	standard not-less relation in BA or bitvectors
<=	standard less-equal relation in BA or bitvectors
!<=	standard not-less-equal relation in BA or bitvectors
>	standard greater relation in BA or bitvectors
!>	standard not-greater relation in BA or bitvectors
>=	standard greater-equal relation in BA or bitvectors
!>=	standard not-greater-equal relation in BA or bitvectors
... <= ... <= ...	interval: the middle term lies between the outer two

A quantifier can bind several variables at once, so all x, y, z ... is shorthand for all x all y all z ..., and likewise for ex.

The precedence of the logical operators/quantifiers is as follows (from higher precedence to lower): ... U ..., ... R ..., ... W ..., ... S ..., ... T ... > ! > && > ^^ > || > <-> > <- > -> > ex ... ... > all ... ... > ... ? ... : ... > F ..., G ... (see Operator precedence).

Using this notation, a slightly bigger example of a Tau spec would be

    (G o1[t] i1[t] = 0 && (i1[t] != 1 -> o1[t] != 0)) && (F o1[t] = i1[t]')

which reads: at each point of time, the output should be disjoint from the input. If the input is not 1, then the output is not zero. And, at least once during execution, the output equals the complement of the input.

Full LTL operators

Tau supports the standard LTL (Linear Temporal Logic) operators for full reactive synthesis, extending the G/F safety fragment with liveness and until-style operators.

Grammar

spec => ...
      | "F" spec               -- eventually / finally, also `sometimes`, `<>`
      | "G" spec               -- globally, also `always`, `[]`
      | spec "U" spec          -- until, also `until`
      | spec "R" spec          -- release, also `release`
      | spec "W" spec          -- weak until, also `weak_until`
      | spec "S" spec          -- since (past LTL), also `since`
      | spec "T" spec          -- trigger (past LTL), also `trigger`
      | "O" spec               -- once (past LTL), also `once`
      | "H" spec               -- historically (past LTL), also `historically`

Each letter and its word spelling parse to the same operator: F φ, sometimes φ and <> φ are one formula, as are G φ, always φ and [] φ, and φ U ψ and φ until ψ.

G (globally) and F (eventually) are the primary temporal operators. U, R, W extend the language beyond the safety fragment. S (since) and T (trigger) are the past-LTL duals of U and R respectively. O φ (once: φ held at some step up to now) and H φ (historically: φ held at every step up to now) are the past duals of F and G, read as T S φ and !(T S !φ); for example G(grant -> once request) says that every grant follows a request. A formula with past operators is decided through temporal testers (the ppLTLTT encoding) that carry each S and T to the synthesis engine as a state proposition. run executes a pure past formula with a lookback of its own as a safety formula, with each S compiled to an auxiliary output stream.

The operators X (neXt) and Y (Yesterday) are not provided as explicit keywords: they are subsumed by time-indexed stream variables. i1[t-1] refers to the previous input and o1[t+1] to the next output, so G(o1[t+1] = i1[t]) says that each next output copies the current input. A forward reference is rewritten into lookbacks when the formula is read: each top-level clause is read k steps later, k its furthest forward reference, so G(o1[t+1] = i1[t]) is G(o1[t] = i1[t-1]), and its time constraints move with it ([t >= 2] becomes [t >= 3]). The always clauses whose bodies have no temporal operator, which share one start (see Lookback initialization), move together. Because a clause starts at its deepest lookback, the rewrite keeps its meaning, also under U, R and W: (o1[t] = 0) U (o1[t+1] = 1) is (o1[t-1] = 0) U (o1[t] = 1) read from step 1. A clause that reads nothing at t or before keeps its later start too: G(o1[t+1] = 1) constrains o1 from step 1 and leaves o1[0] free. A forward reference in a clause with S or T is refused, since a past operator reads before the clause starts, and so is one in the offsets of a recurrence relation.

Past LTL via lookback indices on io_vars (i1[t-k], o1[t-k]) is the preferred way to express history constraints. The S and T operators provide an alternative surface syntax. A decision reads each S through a tester whose state at a step is ψ ∨ (φ ∧ state one step back), and T as the dual ¬(¬φ S ¬ψ). On the run path of a pure past formula, each S is an auxiliary output stream with that definition instead.

Semantics

Operator	Meaning
F φ	φ holds at some future time step (eventually)
G φ	φ holds at all future time steps (globally / always)
φ U ψ	φ holds continuously until ψ first holds (until)
φ R ψ	ψ holds until and including the first time φ holds, or forever if φ never holds (release)
φ W ψ	like U but ψ need never hold (weak until)
φ S ψ	φ has held since (some past time at which) ψ held (since — past dual of U)
φ T ψ	ψ has held since (some past time at which) φ held, or ψ has always held (trigger — past dual of R)

Standard equivalences hold: F φ ≡ T U φ, G φ ≡ ¬ F ¬ φ ≡ ⊥ R φ, φ W ψ ≡ G φ ∨ (φ U ψ). Past duals: φ S ψ is the since operator and φ T ψ is its release-like dual.

Examples

-- Output o1 must eventually be 0
F (o1[t] = 0)

-- Output o1 must stay 0 until input i1 is 1
(o1[t] = 0) U (i1[t] = 1)

-- Infinitely often the output must echo the input
G (F (o1[t] = i1[t]))

-- Release: i1[t] != 0 releases o1[t] = 0
(i1[t] != 0) R (o1[t] = 0)

Assume-guarantee specifications

A component that may rely on its environment is written as an implication, assumptions -> guarantees, with each side a conjunction of temporal clauses in parentheses. The system wins every play where an assumption fails, so it may wait for the inputs before it settles which side it keeps:

-- the environment never raises both requests; the arbiter answers each one
((G !(i1[t]:bv[1] = 1 && i2[t]:bv[1] = 1)))
  -> ((G (i1[t]:bv[1] = 1 -> o1[t]:bv[1] = 1))
      && (G (i2[t]:bv[1] = 1 -> o1[t]:bv[1] = 0)))

-- requests come infinitely often; every request is granted eventually
((G (F i1[t]:bv[1] = 1)))
  -> ((G (i1[t]:bv[1] = 1 -> F o1[t]:bv[1] = 1)))

Both are realizable. The arbiter is realizable only with its assumption: without it the environment raises both requests at once. sat, realizable and run decide such an implication by the game, never one side at a time. When the assumptions are what makes a specification unrealizable, explain names the conjuncts that conflict.

Compositional synthesis

With ltl-compositional on (--ltl-compositional, set ltl-compositional on, TAU_LTL_COMPOSITIONAL), a conjunction whose parts share no output is decided part by part, and run plays a strategy for each part. Two parts may read the same inputs. The conjunction is realizable exactly when every part is: each strategy reads the inputs and writes only its own outputs.

-- two parts: o1 answers each i1; o2 = 1 with o3 = 0 recurs on its own
(G (i1[t]:bv[1] = 1 -> F o1[t]:bv[1] = 1))
  && (G (F (o2[t]:bv[1] = 1 && o3[t]:bv[1] = 0)))

The conjuncts of an always clause are split too. Each one keeps the start of its clause, the deepest lookback the clause reads: the part gets the tautology x[t-k] = x[t-k] on one of its streams. In run, a part without a temporal game operator, or without an output, joins another part, since the data game plays only parts that have both.

An update of such a run revises only the parts that share an output with it. The other parts keep their strategies and their states. run plays every part with the data game, so a revised part that the data game does not decide is not updated, and a program from tau gen solves each step. The option is off by default, since the strategies of the parts can choose other values than the strategy of the whole.

Synthesis game semantics

Tau realizability is defined as a two-player reactive synthesis game:

• The system (synthesized program) controls all output streams (o1, o2, …).
• The environment (adversarial input) controls all input streams (i1, i2, …).
• At each time step, the environment provides inputs first; the system then produces outputs. The system may use any past inputs and outputs with lookback index [t-k].

A formula φ is:

• REALIZABLE if ∃strategy. ∀env. φ — the system has a winning strategy that satisfies φ for every possible input sequence.
• UNREALIZABLE if ∀strategy. ∃env. ¬φ — no matter what the system does, the environment can always violate φ.

-- REALIZABLE: system can always echo the input
G (o1[t] = i1[t]).

-- REALIZABLE: system can always output 0 (vacuously satisfies the antecedent)
G (i1[t] = 1 -> o1[t] = 1).

-- UNREALIZABLE: no output can satisfy both simultaneously
G (o1[t] = 0) && G (o1[t] = 1).

-- UNREALIZABLE: environment can always choose i1=1 to block the condition
G (o1[t] = 1 -> i1[t] = 0).

Naming convention: oN (N = 1, 2, …) are output stream names; iN are input stream names. The declaration of a stream decides whether it is system-controlled (output) or environment-controlled (input); a stream with no declaration takes its direction from the first letter of its name, i for an input and o for an output.

Finite traces (LTLf)

ltl-semantics finite reads a temporal specification over finite traces, as LTLf does, for sat, unsat, valid, realizable and unrealizable. The system chooses the step at which the trace ends, so a specification is realizable when the system can always reach a step where the trace read so far meets it. Spot's ltlfilt --from-ltlf gives the LTL formula ltlsynt decides: an output __alive holds up to the last step, and the temporal operators read only the steps where it holds. The constraints tau adds to the propositional skeleton (between atoms, between the steps of a stream, the testers of S and T) hold on every step.

-- infinite: T, finite: F (both values would recur up to the last step)
sat (G(F(o1[t]:bv[1] = 0))) && (G(F(o1[t]:bv[1] = 1)))

-- infinite: F, finite: T (at the last step both read o1)
valid (G(F(o1[t]:bv[1] = 1))) -> (F(G(o1[t]:bv[1] = 1)))

-- infinite: F, finite: T (the trace ends before an input must be predicted)
realizable G(o1[t]:bv[1] = i1[t+1]:bv[1])

Under finite semantics even a safety specification goes through the game, since the system may end the trace after any step. A run, a self-check of a verdict and tau gen follow a strategy over infinite traces, so run and gen refuse a specification while ltl-semantics is finite, and a realizable verdict is not self-checked. CTL* (A, E) has no LTLf reading and is refused too.

Strategy size

ltl-minimize-strategy merges the bisimilar states of each strategy ltlsynt returns: two states are one when, for every valuation of the propositions, they can move to the same states. The quotient plays exactly the runs of the strategy it came from. ltlsynt already reduces its strategies by bisimulation (ltl-simplification bisim or bwoa), so the option shrinks mainly the strategies of ltl-simplification no.

ltl-strategy-max-states n bounds the states of a strategy, after that minimisation. A larger strategy is asked again with --simplify=bwoa-sat, and one still above the bound answers UNKNOWN, since a smaller strategy may exist that ltlsynt did not find.

Realizability algorithm

LTL(ABA) realizability uses an oracle-assisted synthesis algorithm. The steps are numbered by what each builds on, not by when it runs: the data game of step 6 runs before steps 4 and 5 whenever its regions are codes of values.

1. Data atoms — maximal temporal-operator-free subformulas involving stream variables — are extracted from the formula.
2. Each data atom is replaced by a propositional variable d_i; the result is a pure-propositional LTL skeleton φ*(d₀, …, d_{K-1}). The atoms of one type over the same streams that equal or complement one another share one variable, each read as it or its negation: over bv[1], x = 0 and x != 1 are ¬d_i for the d_i of x = 1.
3. A type enumeration over the named constants in the formula (T₁ for output memory, T₂ for (memory, input) pairs) builds a propositional formula that encodes which (memory-type, data-pattern) triples are feasible. The formula also adds input propositions (P-bits) that expose the current input's T₁ type to the synthesizer, enabling type-aware strategies.
4. Spot's ltlsynt decides realizability of the propositional formula and extracts a winning Mealy strategy automaton (HOA format).
5. The ABA oracle (tau-lang's own quantifier-elimination engine) checks the strategy against the data. Each transition, and each window of consecutive transitions as deep as the deepest lookback, must have data satisfying its guards; a transition or path without such data is blocked and ltlsynt runs again. The strategy is then played against the data itself: at every step the environment picks the inputs after the history is fixed, and the system must pick outputs that satisfy the guard it takes (∀i. ∃o. guard, iterated to a fixpoint over the last values of every stream). A losing strategy that takes a path no data realizes, however long, gets that path blocked. Any other loss comes from a claim the environment or the history decides: the formula is then solved again with every claim that cannot always be kept observed by a new input proposition (whether the data lets the system keep it now), and only combinations no data satisfies forbidden. That abstraction gives the environment choices the data may not allow, so it answers REALIZABLE when its strategy wins against the data and UNKNOWN otherwise.
6. The data game decides exactly. ltlsynt --print-game-hoa prints the parity game of the skeleton of (2), without any constraint the later steps add (--algo=acd, or --algo=sd when ACD states the condition in another form), and that game is played on the data: at every step the environment picks the inputs after the history is fixed, the system then picks the outputs, and each atom of a move is read on those values. The winning regions are sets of histories (the last values of every stream) computed with Zielonka's algorithm. When every stream has a two-valued type (bv[1]), is read only through equalities with streams of its type, 0 and 1 (in a type with enough elements, such as the default type; a smaller one takes the codes below), possibly with a complement on one side (x = y', read on the pairs {v, v'} of a Boolean algebra), or has a type of at most 16 values (bv[2] .. bv[4], read in any way, with arithmetic too), has a bitvector type of at most 16 bits (bv[5] .. bv[16], each value its bits, and the comparisons, bitwise operators, +, -, shifts, min, max and, while it stays small, * circuits over them), or has a dense order (qlt) read through =, !=, <, <=, > and >= (each history then only matters up to its order type, how its values and the constants of the formula compare, of which there are finitely many; a stream of a dense order takes these codes even when only equalities read it, since the order has no element for the codes of 0 and 1 to stand for), or, whatever its type, is read alone at one step back against constants by at most four distinct comparisons (o2[t]:sbf = {X}:sbf: a code stands for one satisfiable valuation of those comparisons, its class, and an output takes any value of its class), a region is a BDD over codes of those values and the game runs before (4) and (5); otherwise, or when the nodes the regions still need outgrow its node limit (nodes no region needs any more are freed as the table fills), a region is a formula whose quantifiers the normalizer eliminates, and the game settles an UNREALIZABLE or UNKNOWN answer of (4) and (5). When a quantifier stays and every stream is of one bitvector type, the game is played once more on formulas that keep their quantifiers, each region decided whole on the bits of its values or by the solver, all of them within --ltl-closed-regions-timeout (20 seconds, each question at most a quarter of it); such a game gives a verdict but no strategy to run. The steps before step 0 are played like any other step, their inputs by the environment and their outputs by the system. The game answers UNKNOWN only when a quantifier cannot be eliminated or decided, or a fixpoint reaches the ltl-data-fixpoint-rounds cap; (4) and (5) then keep their answer.

A formula is realizable iff its data game is won; where that game is undecided, iff (4) succeeds and the strategy wins in (5).

Execution (run) plays the strategy of the procedure that decided the formula. When the data game decides it, Zielonka's algorithm also yields a winning strategy of the system there: in an attractor, each history takes a move into the part attracted before it, so the distance to the goal decreases; in the vertices of the highest odd priority it takes any move that stays in the part the system wins; elsewhere the strategies of the smaller games solved on the way apply. The strategy remembers the game vertex and reads the last values of every stream. At each step it follows the edge the inputs take, asks the solver for outputs within the move of the vertex reached (a value no stream holds when its code says so), and follows the edge those outputs take. The values before step 0 are its own: every input 0 and outputs for which the start is won. A strategy of the game on codes is also a finite Mealy machine over atoms that compare the current values with 0, 1, the elements of their type, the classes of a class code and the last values of the streams: a state is a game vertex with what the last values hold for the steps to come, and the machine is minimized. On codes of values and equalities, a state holds the pattern of equalities among the last values. On the bits of a bitvector wider than 4 bits, it holds the bits a later step reads, a step reads an input bit by bit ((i1[t] & 4) != 0), only as far as its move depends on the bits, and an output is a value of its type. On the order types of qlt values, it holds how the last values and the constants compare, a step places an input among them (i1[t] < o1[t-1], {1}:qlt < i1[t], i1[t] = {0}:qlt), and an output is the point it equals or lies strictly between its neighbours below and above. A machine is built only within 4096 states and 65536 edges; past them, or for a strategy of the game over formulas, the run plays the game's moves directly. The run plays that machine, which the Mealy introspection (the cached solution, its current state) shows, and a step reads only the inputs its move depends on. A strategy over formulas reads an input at a step only when the edge labels of its vertex or the moves it can take there name it, and at every step one that any of them names at an earlier step. A revision of the specification is made as in any run: the parts of the running specification that share an output with the update are revised pointwise by it, the other parts (the definition of the update stream among them) are kept, and the data game is solved again for the revised specification. The game starts from the values already played when it is won from them, and its clauses then hold from the revision step on: a lookback reads those values, so no clause waits for a warm-up. A stream the run never had, input or output, takes the value 0 before the revision step. A revision whose game is lost from the values already played is skipped, and the next candidate is tried. When that game does not decide the revision, the game with the warm-up of its lookbacks starts from the values already played if it is won from them. Otherwise, and when the revision reads an older step the run has no value of, it starts from values of its own, as the revised specification of any run does (see Pointwise revision). When the game shows that the running sometimes goals cannot be met along the update, they give way to it. A revised specification whose strategy another procedure gives as a safety formula (a qlt update such as always o1[t]:qlt = {5}:qlt, which the algebra's own synthesis decides), and which the game does not decide, runs as that formula from the revision step on, unless the strategy has more than one state. The revision is refused when the game shows that no strategy keeps the revised specification ("unsat"), or when nothing decides it ("could not be decided"). Otherwise run executes the strategy of (4) and (5), as a safety formula (below). A specification whose always part reads a fixed step, such as o2[0] = 0, and which the step-by-step pipeline cannot execute, runs through that strategy as well: the step counter of the realizability check carries the fixed steps. LTL formulas need the external tool ltlsynt (part of Spot ≥ 2.16). Tau looks for it on the PATH, then in the spot-bin directory, then in the Spot folder of an installed package, which ships its own copy. The first one found is used, so an older ltlsynt on the PATH hides the packaged one. A build from source refuses an ltlsynt older than 2.16 at configure; take it off the PATH and configure builds Spot 2.16 itself.

Synthesis algorithms

The algorithms below are the qlt plugin's propositional synthesis, tried first for a formula whose atoms are all qlt comparisons that its order types encode (the T₃ fragment below). A formula outside it, and a formula over any other algebra, goes to the default abstraction and the data game described above. The qlt paths are:

Algorithm	TAU_LTL_ALG	Description
Algorithm B (default for input-bearing qlt)	unset or B	Adds ⌈log₂|T₂|⌉ input propositions (P-bits) binary-encoding the T₂ type σ = (pos_m, pos_x, rel_mx). The strategy observes the current input's T₁ type, making it sound for formulas with input variables (e.g. G(o1 > i1)). Formula structure: (Φ_I ∧ Ψ_I) → (Φ_O^R ∧ Φ_δ ∧ φ*) where Φ_I/Ψ_I are env assumptions about P-bits.
Algorithm A	automatic for pure-output formulas, or A for pure-output formulas	Uses only R-bits for memory type with no input propositions. Fast for pure-output formulas. When input variables are present, Algorithm A is intentionally bypassed because it cannot observe the environment's T₁ type.
Algorithm D	D	Output-only direct parity-game construction. Builds the propositional synthesis game for φ*(D_i) via ltlsynt --print-game-hoa, then solves the data product game (synthesis game × T₁) using Zielonka's recursive attractor solver. D-patterns are decoded by AP name (d_i), not by HOA AP order. A formula it does not apply to (input variables, several outputs, an atom outside T₃) goes to the default abstraction, not to Algorithm B.

Algorithm B is the default for formulas over the qlt type that contain input variables. Pure-output qlt formulas route to Algorithm A because no P-bits are needed. Algorithm D is selected by ltl-alg set to D (TAU_LTL_ALG=D), but stays output-only. The algorithm picker follows the same soundness rule: A and D are excluded when input variables are present.

A, B and D all run on the T₃ = (memory, input, output) types, which hold one input slot, one output slot and one lookback-1 output slot. A formula they cannot represent takes the default ABA-oracle path instead: two or more input streams, a stream of unknown direction (the declaration decides the direction, not the first letter of the name), a positional atom such as o1[2], an input read with lookback, a comparison of two streams where a side is more than the bare stream ((o1 | {9}) = i1), and a constant with no long long rational in a type next to it (o1 > {9223372036854775807}).

Synthesis timeout: by default, ltlsynt gets 60 seconds to solve the propositional skeleton. The option ltl-timeout sets the limit, and 0 disables it. Give it as --ltl-timeout 120, as set ltl-timeout 120 in the REPL, or as the environment variable TAU_LTL_TIMEOUT:

TAU_LTL_TIMEOUT=120 tau "G (F (o1[t] = i1[t]))."

LTL synthesis options. Each row is an option of the options repository (see Options and the environment):

Option	Default	Description
ltl-timeout	60	Wall-clock limit in seconds for each ltlsynt call (0 = no limit).
ltl-qe-max-vars	2	Free-variable cap for the omcat (qlt) existential quantifier-elimination fast path (0 = off). Values above 2 enable a fast path that is not sound. Keep the default.
ltl-alg	auto (Algorithm B for input-bearing qlt, Algorithm A for pure-output qlt)	The synthesis algorithm: A requests Algorithm A for pure-output formulas, B is Algorithm B (P_σ binary encoding), D requests the output-only Algorithm D. Under A or D, a formula with inputs goes to the default abstraction, not to Algorithm B. Any other word is an error.
ltl-hoa-max-states	4194304 (2^22)	Largest state count accepted from an ltlsynt HOA strategy (0 = unlimited). A larger count is read as a garbled header.
ltl-guard-max-cubes	512	DNF cubes a HOA guard label may expand into in the Algorithm D product game (0 = unlimited). A guard beyond it is refused.
ltl-refinement-rounds	64	ABA-oracle refinement rounds of one realizability check (0 = unlimited). On the cap the verdict is UNKNOWN.
ltl-self-check-steps	64	Steps of the run that checks a realizable verdict of the LTL pipeline: the specification is run on generated inputs (0 or 1 of each input type, from a fixed seed), and a top-level clause the run violates turns the verdict into UNKNOWN, since the strategy found is then not one of the specification. The run plays the strategy of the verdict's data game, without solving that game again. Any other strategy is synthesized again by the interpreter of the run. 0 = no check.
ltl-compositional	off	Decide and run the parts of a conjunction that share no output each for itself (see Compositional synthesis).
ltl-data-fixpoint-rounds	64	Rounds of one data fixpoint: the check of a strategy against the data, and each fixpoint of a data game over formulas. After a losing check, at most that many longer windows are searched for a blocking clause. On the cap the verdict is UNKNOWN. At most 4096, and 0 means 4096, since a fixpoint over formulas need not converge.
ltl-window-max-paths	4096	Strategy paths the multi-step window oracle examines per check (0 = unlimited). A hit cap gives UNKNOWN.
ltl-closed-regions-timeout	20	Seconds the data game may spend on regions that keep their quantifiers, all their questions together, each question at most a quarter of it (0 = no such attempt). Past either bound that attempt is undecided.
ltl-data-game-max-nodes	8388608 (2^23)	Live nodes of the BDD a data game over codes builds (0 = unlimited). A full table leaves the game undecided. 2^23 nodes and their tables take about 1 GB.
ltl-data-game-max-memo	33554432 (2^25)	Operation memo entries of the same BDD (0 = unlimited). A memo that reaches the cap is emptied. This costs recomputation, never a verdict.
max-consistency-subsets	4096	k-ary consistency subset checks per atom group in LTL(ABA) synthesis (0 = unlimited). A fired cap is sound but can answer unrealizable.
max-cover-products	256	Literal products the ABA oracle's mixed-type coverage check may expand (0 = unlimited). Beyond it the syntactic verdict stands.
ltl-data-game-max-combinations	4096	Value combinations the data game tabulates for one comparison its circuits do not encode (0 = unlimited). Past it the comparison has no code, and the game falls back to formula regions or is undecided.
ltl-max-observations	8	Observation props whose impossible joint values the synthesis skeleton assumes away, at 3^n feasibility checks. Beyond it nothing is assumed, which leaves the environment moves no data produces. At most 30, and 0 means 30.
ltl-mealy-max-states	4096	States of the Mealy view a data-game strategy is played through. Past it the moves are played directly (0 = no view).
ltl-mealy-max-edges	65536	Edges of that Mealy view (0 = no view).
ltl-ctl-star-tableau-max-states	64	States of the tableau that decides a CTL* E asked at several steps (0 = unlimited). Past it the witness paths share one set of directions, and an unrealizable answer is UNKNOWN.
ltl-witness	off	On UNREALIZABLE, print an environment counter-strategy (HOA) to stderr. This works only when the UNREAL verdict comes from ltlsynt, not from an earlier rejection in tau. When ltlsynt does not solve the counter-strategy game, a none: line gives the reason instead, such as an ltlsynt older than Spot 2.16.
ltl-export-strategy	empty	hoa prints the winning-strategy HOA to stderr. dot prints Graphviz dot, or HOA when autfilt is not available. Any other word is an error.
ltl-export-strategy-file	empty	A path. tau also writes the HOA strategy to that file on success.
spot-bin	empty	A directory searched for ltlsynt, autfilt and ltlfilt after PATH and before the Spot folder of an installed package.
ltl-simplification	ltlsynt default	Given to ltlsynt --simplify=: no, bisim, bwoa, sat, bisim-sat or bwoa-sat (none is read as no). Any other word is an error. The SAT levels minimise the strategy ltlsynt found; they do not search for the smallest strategy. Spot 2.16 ends every SAT level with exit code 2 after a warning about unused internal options; tau then reads the verdict ltlsynt printed before it.
ltl-synth-algo	ltlsynt default	Given to ltlsynt --algo= when ltlsynt decides a verdict: sd, ds, ps, lar, lar.old or acd. The parity game of the data game is asked with it first, then with acd and sd. Any other word is an error.
ltl-decompose	ltlsynt default	Given to ltlsynt --decompose= when ltlsynt decides a verdict: yes or no (none is read as no). The parity game of the data game is never decomposed. Any other word is an error.
ltl-minimize-strategy	false	Merge the bisimilar states of each strategy ltlsynt returns (see Strategy size).
ltl-strategy-max-states	0	Most states of a strategy, after ltl-minimize-strategy. Above it ltlsynt is asked again with --simplify=bwoa-sat, and a strategy still above it answers UNKNOWN (0 = no bound).
ltl-semantics	infinite	infinite or finite: read a temporal specification over infinite traces, or over the finite traces of LTLf, whose end the system chooses (see Finite traces (LTLf)). Any other word is an error.
compile-max-table-edges	400	Edges of a Mealy view tau gen / tau compile carries as a table, and of a --machine table. A larger strategy is solved as the program runs (0 = never a table).
compile-build-timeout	3600	Seconds the cmake build of tau compile may take. Past it the build is stopped and the compile fails (0 = no timeout). On Linux and macOS the whole build is stopped. On Windows only the cmake process tau compile started is stopped, and the compilers it launched can run to their end.

Options and the environment

Every limit, flag and algebra option of tau is an option of the options repository. An option has one name on every surface:

• the command line: --max-fixpoint-steps 1000
• the REPL: set max-fixpoint-steps 1000, get max-fixpoint-steps
• the environment: TAU_MAX_FIXPOINT_STEPS=1000
• the C++ API: idni::options().set_text("max-fixpoint-steps", "1000")
• the bindings: set_option("max-fixpoint-steps", "1000") in Python and JavaScript

The variable of an option is TAU_ plus the name in upper case, with - as _. tau reads the environment once at start. A flag on the command line and a later set write over the value of the variable. A bad value in a variable is an error, and tau exits with 1. A count above the largest value it holds is an error too, never a wrapped value. Zero is a value, not an absence. For every cap here it means unlimited, and for a timeout it means no limit, unless the table says otherwise.

An algebra declares its own options, named <ba>-<option>. They exist when that algebra is in the pack. qlt declares qlt-t3-cap (data atoms its T3 encodings accept, default 20, at most 30), qlt-const-output-max (constant-output assignments the fast path in front of Algorithm B enumerates, default 100), qlt-cells-budget (formula instances one decision by cells evaluates before it is left open, default 65536) and qlt-cells-max-params (other free variables, and named endpoints, such a decision ranges over, default 2). nlang declares nlang-http-timeout (seconds per LLM request, default 15) and nlang-max-tokens (tokens per reply of an Anthropic model, default 16000). The options of bv are listed under the command line options. The tau algebra uses the prefix ba-: ba-component-factoring and ba-decision-pins. qlt-t3-cap reads TAU_QLT_T3_CAP, and bv-blastdepth reads TAU_BV_BLASTDEPTH, by the same rule.

The limits of the engine:

Option	Default
spec-size-warn	0 (off)
max-revision-alts	0 (unlimited)
block-max-splits	0 (unlimited)
block-max-rounds	0 (unlimited)
ba-decision-pins	4096 (0 = none)
cqe-max-clauses	0 (unlimited)
lgrs-max-vars	8
max-fixpoint-steps	500
max-flag-search-steps	500
block-squeeze-cap	0 (unlimited)
max-simplify-rounds	0 (unlimited)
max-def-passes	0 (unlimited)
max-enum-steps	0 (unlimited)
max-probe-steps	10000
max-rewrite-rounds	0 (unlimited)
max-constant-size	2000
cache-bound	4096 (0 = unbounded)
bf-dependence-max-nodes	65536
gc-min-size	256
gc-growth-factor	1.5 (<= 0 disables the growth-triggered sweeps)
tref-budget	0 (unlimited)
tref-budget-soft	75

A program that tau compile builds reads the same variables at start. Its command line takes only its own options (see --help of the program).

An algebra also declares options that are a flag or a text, on the same surfaces. The text options are those of the nlang oracle: --nlang-provider, --nlang-endpoint, --nlang-model, --nlang-api-key and --nlang-effort, beside the flag --nlang-fallback. In the REPL set nlang-model claude-opus-5-5 or set nlang-endpoint = http://localhost:8080/v1 writes one and get nlang-model reads it; a text takes letters, digits and . - _ : /. A text may go in double quotes, which hold any characters, and one with a . should: set nlang-endpoint "https://api.anthropic.com/v1", set nlang-model "gemini-2.0-flash". A . also separates two commands, so without the quotes the value may end at the dot. Empty quotes clear the option: set nlang-model "" goes back to the default. The table of the nlang section lists each with its environment variable and its default.

Other environment variables. TAU_BA_COMPONENT_FACTORING sets the option ba-component-factoring at start, and --ba-component-factoring / set ba-component-factoring write it later (the decision by components is taken on a formula of always clauses that read their streams at the current step and at steps back, and declined where a unit refers to absolute time, through a sometimes clause, a stream read at a fixed time point or a constraint on the time point, and where an always clause holds a temporal operator of its own, so that the whole formula decides). TAU_BV_CASE_SPLIT and TAU_BV_QUANTIFIER_FREE_DECISION set bv-case-split and bv-quantifier-free-decision at start, and the flag or set writes them later. The nlang oracle takes TAU_NLANG_PROVIDER, TAU_NLANG_API_KEY, TAU_NLANG_ENDPOINT, TAU_NLANG_MODEL, TAU_NLANG_EFFORT, TAU_NLANG_MAX_TOKENS and TAU_NLANG_FALLBACK into its nlang-* options at start, and it reads the provider's own OPENAI_API_KEY / ANTHROPIC_API_KEY when no key is given. Two diagnostic flags change logging only, never a verdict: lean-decide-crosscheck (TAU_LEAN_DECIDE_CROSSCHECK=1) re-decides the lean constant tests through the full path and reports disagreements, and phi-delta-crosscheck (TAU_PHI_DELTA_CROSSCHECK=1) shadows the ABA oracle with the closed-form Φ_Δ of the atomless algebra on matching shapes. spot-bin (TAU_SPOT_BIN) names a directory searched for ltlsynt, autfilt and ltlfilt after PATH and before the Spot folder of an installed package. TAU_CODEGEN_RUN_SDK_LINK_TEST opts the codegen test suite into a minutes-long real cmake build.

Execution: when the interpreter pipeline is given a realizable LTL formula that the data game does not decide, ltl_to_safety_formula_full converts the winning Mealy strategy to an executable G(φ) formula. Single-state strategies (common for F, G(F), R, W) use the self-loop guard directly. Multi-state strategies are encoded using one-hot auxiliary output bitvector variables (o__ltl_ms0__, o__ltl_ms1__, …) and work for any number of states.

Operator precedence

The binary temporal operators bind tighter than every propositional connective, ! included; the prefix operators F, G, O and H bind loosest:

U, R, W, S, T  >  !  >  &&  >  ^^  >  ||  >  <->  >  <-  >  ->  >  ex  >  all  >  ?:  >  F, G, O, H

So !a U b is !(a U b), a && b U c is a && (b U c), and G a && b is G (a && b). Parentheses around the operand do not change that: G(A) && F(B) is G(A && F(B)), B infinitely often, and F(A) || G(B) is F(A || G(B)). Write (G(A)) && (F(B)) for the conjunction of the two. tau warns when it reads a parenthesized operand this way. G(A) && G(B) is the one exception that needs no parentheses, since G(A && G(B)) means G(A) && G(B). Mixing binary temporal operators without parentheses is best avoided: a U b R c groups as a U (b R c) but a R b U c as (a R b) U c. The printer always parenthesises such operands.

In the CTL* fragment the prefix operators A, E and - sit at the level of F and G.

Multi-type LTL formulas

Different LTL sub-formulas may use different BA types (for example tau, sbf and bv), but each atomic formula must use exactly one type. Variables of different types must be given different stream names (e.g. o1:tau and o2:sbf).

Verified working patterns:

Pattern	Result
(F(tau)) && (F(sbf))	REALIZABLE
(F(sbf)) && (F(bv))	REALIZABLE
(G(sbf)) && (F(bv))	REALIZABLE
(G(tau)) && (F(bv))	REALIZABLE
G(tau) && G(tau)	Merged to G(tau && tau) — works
G(sbf) && G(sbf)	Merged to G(sbf && sbf) — works
G(tau) && G(sbf)	REALIZABLE ✓ (split into independent checks)
G(tau) && G(bv)	REALIZABLE ✓ (split into independent checks)

When combining two G sub-formulas of the same type, write either G(phi_A && phi_B) or G(phi_A) && G(phi_B) — the two are semantically equivalent and tau-lang automatically merges the latter form into a single G before normalization.

Lookback initialization

When a specification uses lookback stream variables (e.g. i1[t-k] or o1[t-k]), the values they read do not exist for the first k steps. The interpreter handles this per clause: the always part of a specification (every always or G statement merged into one) and each sometimes statement or other top-level conjunct of a full-LTL formula is enforced from the deepest lookback that clause reads, and asks nothing before that. During a clause's warm-up its outputs are unconstrained by it, lookback-free ones included; the interpreter picks the bottom element (0/"F" for tau, 0/"F" for sbf, etc.) unless a later step of the run needs another value, so G(o1[t-1] = 1) starts with o1[0] = 1.

A clause that reads no past starts at step 0 even beside one that does. (always o1[t] = 1) && (sometimes o1[t-2] = 0) is unsatisfiable: the always holds from step 0, so o1 never was 0 two steps earlier. Within one clause the deepest lookback counts for every literal: G(o1[t] = 1 && o2[t] = o2[t-1]) leaves o1[0] unconstrained, and G(o1[t] = i1[t-1] && o2[t] = i2[t-2]) leaves both outputs unconstrained for steps 0 and 1, whatever their individual shifts. The lookback is the one the clause is written with, also where a literal carrying it is a tautology or is absorbed by another one: o1[t-2] = o1[t-2] still gives its clause a two-step warm-up, so (always o2[t] = 1 && o1[t-2] = o1[t-2]) && (sometimes o2[t-1] = 0) is satisfiable, with o2[0] = 0, and so is (always o2[t] = 1) && (always (o2[t] = 1 || o1[t-2] = 0)) && (sometimes o2[t-1] = 0). sat, realizable, valid, run, ltl and tau compile apply the same warm-ups: (G o2[t-1] = 1) && (G o1[t] = 1) && (F o1[t] = 0) is realizable, because its always part reads o2[t-1], so o1[0] is free. A clause read under a negation keeps its warm-up too: valid φ asks whether some trace violates a clause of φ after its warm-up, so valid !φ is T exactly when no trace satisfies φ, and valid (always o2[t] = 1 && o1[t-2] = o1[t-2]) -> (always o2[t] = 1) is F. The LTL synthesis pipeline follows the same rule, so G(p U q) with q reading the past agrees with G q when p is contradictory. A past value that no clause guards belongs to a step before step 0, played like any other step: the environment picks its inputs and the system its outputs. The operands of since and trigger are guarded like those of until: a ψ reading i1[t-1] in always (φ since ψ) cannot hold before step 1, so the environment can keep it false.

A time constraint therefore has no effect before its clause starts: in always ([t = 0] -> o1[t] = i1[t]) && ([t >= 1] -> o1[t] = o1[t-1]) the clause starts at step 1, so [t = 0] never holds and o1[0] is free. sat, realizable, valid and run warn about such a constraint ("this time constraint never holds"). A fixed position constrains the warm-up steps instead: always (o1[0] = i1[0]) && ([t >= 1] -> o1[t] = o1[t-1]) copies the first input into every step.

Known LTL limitations

• Spec terminator: in specification files and in programs passed to the parser every statement ends with . (a period), e.g. G (o1[t] = 1).; the argument of a single REPL command (sat G (o1[t] = 1)) may omit it.
• Semantic negation (-): - φ under a temporal operator reads φ as started fresh at that point (see CTL* fragment and semantic negation).
• nlang needs an LLM API key: the oracle reads the nlang-api-key option, else TAU_NLANG_API_KEY, else the provider's own OPENAI_API_KEY or ANTHROPIC_API_KEY. The provider (nlang-provider: openai or anthropic), the endpoint and the model are optional, and each HTTP request is capped by the nlang-http-timeout option (15 s, or TAU_NLANG_HTTP_TIMEOUT). Without a key every emptiness, universality and equivalence question over nlang elements is answered false (not cached), a warning is printed once, and verdicts over nlang are not reliable.
• fall/fex BF quantifiers: these parse correctly but are not supported in LTL synthesis (only in safety/always formulas).
• Input-only atoms: formulas consisting entirely of input constraints (no output variables) are checked for satisfiability but cannot be synthesized (the system has no control over pure-input atoms).
• Nesting depth: deeply nested formulas may exceed stack or memory limits; there is no built-in depth cap. Use shallower formulas or increase the process stack size when needed.
• No X operator: a next-step condition is a forward index, o1[t+1] (see the X/Y note above); a forward index in a clause with S or T is refused.
• Finite traces decide only: ltl-semantics finite reads a specification over the finite traces of LTLf for sat, unsat, valid, realizable and unrealizable; run, gen, gen --aiger and CTL* refuse it, and a realizable verdict is not checked by the ltl-self-check-steps run.
• Prefix operators take everything to their right: G(A) && F(B) is G(A && F(B)) (see Operator precedence); tau warns on that spelling.
• Positional atoms in a disjunct: a disjunct of a Boolean combination of temporal clauses over inputs that mixes a fixed step (i1[0]) with relative time (o1[t]), such as (G(i1[0] = 0 && o1[t] = 0)) || (G(i1[0] != 0 && o1[t] = 1)), is not supported: realizable answers UNKNOWN. Writing the disjunction inside one G works.
• Positional atoms in a conjunct: a top-level conjunct that mixes a fixed step (o1[0]) with relative time (o1[t]), and a fixed step under a temporal operator other than a top-level G, are refused. Give each fixed-step fact its own conjunct, outside those operators.
• Data quantifiers under temporal operators: an ex or all over streams under a temporal operator that the normalizer does not eliminate has no proposition in the skeleton, so the answer is UNKNOWN (realizable F(all x:bv[8] (o1[t]:bv[8] * x = i1[t]:bv[8] * x))).
• CTL* implication and equivalence: an implication or equivalence check of formulas with A, E or - is refused.
• Bare bitvector numerals: a bitvector constant other than 0 and 1 is written braced with its type, {255}:bv[8]; a bare 255 is a syntax error (see 0 and 1 in bitvectors).

CTL* fragment and semantic negation

The default grammar fragment is LTL (linear temporal logic). To use branching-time operators, switch to the CTL* fragment:

fragment ctl_star

To switch back:

fragment ltl

CTL* operators

The CTL* fragment extends the LTL grammar with path quantifiers:

Operator	Syntax	Meaning
A (for-all paths)	A φ	φ holds on every path from the current state
E (exists path)	E φ	φ holds on at least one path from the current state

A and E quantify over the tree of possible strategy executions, one branch per input sequence, not over individual traces. Not every placement is supported by the encoding:

• E χ in positive polarity is encoded through a fresh witness output. When the specification has inputs, the witness path is pinned by one direction output per input stream, which names the value that path takes next, and the constraint is read one step later, where "the path follows the directions" is a plain always. The encoding is then exact for an E asked at one step. An E asked at several steps of a path (under always, on the left of until, ...) has a witness path from each, and two of them may have to part where they meet: in always E ((oc = 0 -> always (oc = 2 -> i1 = 1)) && (oc = 1 -> always (oc = 2 -> i1 = 0))) the paths from oc = 0 and from oc = 1 ask opposite inputs. Such an E is decided first with one set of directions, which answers a realizable spec, and when that loses, again through a tableau of χ with one set of directions per set of obligations χ leaves (GPVW), and a breakpoint over the paths for its eventualities. Past ltl-ctl-star-tableau-max-states states (64) the tableau is not built and an unrealizable result is reported as UNKNOWN. The witness state has already read its input, so its branch starts with the input the environment gave: E (F i1[t] = 1) is realizable, E (always i1[t] = 1) is not, since the first input may be 0. A past operator (S, T) inside χ has no such form: that witness keeps the all-paths encoding, which is stricter than E, so an unrealizable result is reported as UNKNOWN. Like any clause, E χ is asked from the deepest lookback χ reads: (always o1[t] = 1) && E (sometimes (o1[t] = 0 && o2[t-1] = 0)) is unrealizable, as it is without the E.
• A χ in positive polarity inside a universal context (under &&, G or another A) reduces to χ itself.
• A or E in negative polarity (under !, on the left of ->) is first rewritten through its dual (!A χ = E !χ, !E χ = A !χ).
• Anything that still has no sound encoding -- A under an existential or eventual context (||, F, U, ...), A/E on either side of <->/^^ or in the guard of ?: -- is refused with an error.

sat of a CTL* formula is sat of its encoding, so sat A φ and sat φ agree. valid does not decide formulas with A, E or - and reports UNKNOWN.

Semantic negation (-)

The CTL* fragment also introduces semantic negation (-), which is distinct from syntactic negation (!):

Negation	Syntax	Meaning
Syntactic (!)	! φ	Boolean complement of formula φ
Semantic (-)	- φ	There is no winning strategy for the system satisfying φ

- φ is a strategy-level statement: it asserts that the specification φ is unrealizable — no matter what the system does, the environment can always violate φ. This differs from ! φ, which simply flips the truth value of φ on a single trace. - φ is a closed statement about φ's own game and is decided by the realizability verdict of φ: it is true exactly when realizable φ is false, and undecided when that is. Under a temporal operator or a path quantifier it means "φ is unrealizable from this point on", read as φ started fresh there — as a specification installed by a revision reads its own lookback, what precedes its start is warm-up. That game is the same at every point, so - φ folds to the same constant wherever it sits.

Examples

-- In the CTL* fragment (REPL command, no terminator):
fragment ctl_star

-- For all paths, eventually the output is 1
A F(o1[t] = 1).

-- There exists a path where the output is always 0
E G(o1[t] = 0).

-- The environment cannot be forced to raise i1: true
-(F i1[t] = 1).

-- The same game at every step: true
G (-(F i1[t] = 1)).

-- There exists a branch where the environment raises i1
E (F i1[t] = 1).

Reduction to LTL

CTL* formulas are reduced to LTL synthesis problems with the Bloem/Schewe/Khalimov witness-output encoding (arXiv:1711.10636): each existential path choice becomes a witness output, with one direction output per input stream pinning the path it witnesses, so the existing ltlsynt-based pipeline handles the branching-time property. The witness constraint is stated one step after the witness, where "the path follows the directions" needs no next-step operator: the path formula is rewritten by its one-step expansion laws (G φ = φ ∧ X G φ, φ U ψ = ψ ∨ (φ ∧ X(φ U ψ)), …) and its present part is read back through lookback. The witness and direction streams are internal: they use the reserved w_ prefix and are never printed. The fragment ctl_star switch is a REPL setting: specification files and the API accept A, E and - without it.

Satisfiability and execution

Satisfiability

The notion of satisfiability in the Tau language is non-standard and conceptually defined in such a way that a satisfiable Tau specification can be executed indefinitely regardless of the inputs given to the specification. In particular, a specification is unsatisfiable if a particular sequence of inputs would result in a contradictory situation.

This notion of satisfiability is achieved by a certain quantification pattern of streams, which we call time-compatability. More precisely, all input streams are quantified universally and all output streams are quantified existentially in such a way that

1. the ordering of quantifiers is increasing with respect to the time step to which the quantified variable refers and
2. the outputs always depend on the inputs in a given step.

More informally, we can think of the phrase that for all input, there exists output at each point in time such that the Tau specification can be satisfied (in the standard sense).

The following example shows the explained quantification pattern for the Tau specification o1[t] = i1[t] && ( i1[t-2] = 1 -> o2[t-1] = 1 ):

all i1[t-2] ex o2[t-1] all i1[t] ex o1[t] o1[t] = i1[t] && ( i1[t-2] = 1 -> o2[t-1] = 1 )

The inputs inside a sometimes are quantified in the same way: the specification must reach the sometimes whatever the inputs do. So sometimes i1[t] = 1 is unsatisfiable, since the input can stay 0 at every step, while sometimes o1[t] = i1[t] is satisfiable, since the output can copy the input at the step it reads it.

This explanation of satisfiability neglects the fact that a contradiction can, in fact, occur only after a specification is executed for a certain number of steps. The entire procedure is, hence, (much) more involved. Further resources concerning the details can be found in the theory section.

A specification without a temporal operator is read as if it were wrapped in always, and it gets the same answers as its always spelling: a stream constraint is not decided as a single step, so o1[t]:bv[2] > o1[t-1]:bv[2] (an output that must grow forever within a finite range) is unsatisfiable.

For full LTL (U, R, W, S, T, nested temporal operators) the same notion is realizability: sat and realizable decide it through the LTL(ABA) synthesis pipeline and agree in both directions. So does a Boolean combination of always and sometimes clauses that reads an input, such as (G i1[t] = 1) -> (G o1[t] = 1): a strategy may wait for the inputs before it picks the disjunct it fulfils, so the disjuncts are not decided one by one.

Validity is not quantified over an environment but over traces: valid φ holds when no trace violates φ. It is unsat ! φ with every input stream read as an output, for always/sometimes specifications as well as for full LTL, so that valid φ implies sat φ. For example valid sometimes i1[t] = 1 is F, since the input can stay 0 at every step, and G (F i1[t] = 1) is neither valid nor satisfiable: the inputs can stay 0, and the system cannot make them 1.

A verdict that cannot be decided is reported as UNKNOWN (an error, never a T or F answer). This covers a backend failure, a resource cap that gave up, an E over inputs in the CTL* fragment, and a closed formula that normalization leaves undecided, such as a functional quantifier over arithmetic (see Boolean functions). When one disjunct of a formula is satisfiable, the answer is still decided, even if another disjunct is undecided. A problem whose decision diagrams outgrow the node table ends with the error bdd node table exhausted: a node did not fit, so the result is unknown and no answer is given. The next command runs normally.

Execution

We have talked about the execution of a Tau specification. Here we want to explain in more detail what that means. In general, the execution of Tau specification is about receiving values for the input streams from a source and to produce values for the output streams in accordance with the specification. In this fashion, a Tau specification is started at time step 0. In each consecutive step the time step is incremented by 1. As a result, we get a continues timeline starting at 0 and ending at however far the specification has been executed.

Take for a minimal example the specification G o1[t] = i1[t], saying that at each time step t, the input i1 is equal to the output o1. Executing this specification means to start at t := 0. Hence, in the first step during execution we have o1[0] = i1[0]. The value for i1[0] is then requested, let's call it v. After the value is received, i1[0] is replaced with v, yielding o1[0] = v. At this point the specification has as only stream the output o1[0] remaining and, hence, can be passed to an internal solver to get a value for o1[0], matching the specification. In this case this is easy, since it is immediate that o1[0] has to be v as well. Outputting the result for o1[0] then concludes the first step of execution. We then move to the next step being t := 1, which yields o1[1] = i1[1] for the specification. The steps above are now repeated such that at the end of the step, the value for o1[1] is outputted. In the same fashion execution can now be continued as long as desired.

For more complicated specifications the main steps stay the same:

1. Execution is started at t := 0
2. The inputs are requested (if present)
3. The outputs are produced according to the specification after the received inputs have been plugged in
4. The time step t is incremented by 1 and execution continues from point 2. above

Note that before a Tau specification is executed, it is checked for satisfiability in the sense that it can be executed indefinitely as described above. During this process the specification is also converted to what we call unbounded continuation which essentially adds all implicit assumptions from a specification ensuring that the solutions for output stream values do not make the execution contradictory in a future step.

It is not always the case that the values which can be assigned to outputs are unique. For this reason, a single specification can give rise to a multitude of different programs differing in the choices made for assignments. As a result, during execution only one of possibly many program is executed. The execution process in Tau, however, is fully deterministic, so that the same program is always chosen for the same specification.

Boolean functions

One of the key ingredients of the Tau Language are Boolean functions build from Boolean combinations of variables, streams and constants over some fixed atomless (or finite -to be developed-) Boolean algebra. In particular, each Boolean function has a unique type being this chosen Boolean algebra. They are given by the following grammar:

term => ("(" term ")") | (term "&" term) | term "'"
      | (term "^" term) | (term "|" term)
      | ("fall" variable ("," variable)* term)
      | ("fex"  variable ("," variable)* term)
      | function | constant | uninterpreted_constant
      | variable | stream_variable | "0" | "1"

where

• term stands for a well-formed subformula representing a Boolean function and the operators &, ', ^ and | respectively stand for conjunction, negation, exclusive-or and disjunction,
• fall and fex are the functional (term-level) universal and existential quantifiers. Unlike all and ex, which build a formula, these build a Boolean function: fall x f denotes the meet and fex x f the join of f over all values of x. Over a Boolean body, normalization evaluates them through Boole's expansion: fex x f becomes f[x:=0] | f[x:=1] and fall x f becomes f[x:=0] & f[x:=1], innermost first. A body with arithmetic, a cast, min/max, a function reference or a quantifier that remains keeps the functional quantifier as an atomic term, and a closed formula over it is reported as UNKNOWN,
• the conjunction operator & may be omitted between two operands, so xy is the same as x & y,
• function is the non-terminal symbol used to incorporate function definitions (see the subsection Functions and Predicates),
• constant stands for an element from an available Boolean algebra. The type of the constant determines the type of the Boolean function (see subsection Constants for details).
• uninterpreted_constant stands for an uninterpreted constant from the fixed Boolean algebra, which can be thought of as a variable being existentially quantified from the outside of the formula. Its syntax is as follows:

uninterpreted_constant => "<" [name] ":" name ">"

• variable is a variable over the fixed Boolean algebra (see subsection Variables and uninterpreted constants for details),
• stream_variable represents an input or output stream. The type of a stream also determines the type of the Boolean function (see also subsection Streams) and
• 0 and 1 stand for the bottom and top element in the fixed Boolean algebra. For a bitvector type they are the all-zeros and the all-ones vector, so 1:bv[8] is 255, not the number one (see 0 and 1 in bitvectors).

The order of the operations is the following (from higher precedence to lower): ' > & > ^ > | > fex ... ... > fall ... .... The full ordering including the bitvector operators is given in the section Bitvectors below.

If no type information is present within a Boolean function, it is assumed to be of the general type countable atomless Boolean algebra. Since all such Boolean algebras are isomorphic, no particular model is chosen.

For example, the following is a valid Boolean function of general type:

(x & y | (z ^ 0))

where x, y and z are variables.

Bitvectors

Another key ingredient of the Tau Language is bitvectors build from usual Boolean algebra operations and variables, streams and bitvector constants. They add the following to the above grammar for terms:

term => (term _ '+' _ term) | (term _ '-' _ term) | (term _ '*' _ term)
      | (term _ '/' _ term) | (term _ '%' _ term) | (term _ "!&" _ term)
      | (term _ "!|" _ term) | (term _ "!^" _ term) | (term _ "<<" _ term)
      | (term _ ">>" _ term) | ("(" "bv" "[" bit_width "]" ")" _ term)
      | ("min" _ "(" _ term _ "," _ term _ ")")
      | ("max" _ "(" _ term _ "," _ term _ ")")

where term is as above are as above and the new operators meaning is given in the following table:

Symbol	Meaning
*	modular multiplication of bitvectors
/	modular division of bitvectors
%	modular remainder of bitvectors
+	modular addition of bitvectors
-	modular subtraction of bitvectors
!&	bitwise nand of bitvectors
!|	bitwise nor of bitvectors
!^	bitwise xnor of bitvectors
<<	left shift of bitvector by a number of bits
>>	right shift of bitvector by a number of bits
(bv[n])	cast of a term to a bitvector of width n
min(x, y)	unsigned minimum of two bitvectors
max(x, y)	unsigned maximum of two bitvectors

0 and 1 in bitvectors

As in every Boolean algebra, 0 and 1 denote the bottom and the top element. For bv[n] the bottom is the all-zeros vector and the top is the all-ones vector 2^n - 1, so 1:bv[8] is 255. The number one is a constant, {1}:bv[8]. This holds everywhere a bare 1 meets a bitvector, in input and in output:

written	meaning for bv[8]
1:bv[8], x + 1	255; x + 255, i.e. x - 1 modulo 256
{1}:bv[8], x + {1}:bv[8]	the number one; the successor of x
x <= 1	always true
1 <= x	x = 255, i.e. x' = 0
x'	255 - x, the bitwise complement
(bv[8]) 1:bv[4]	{15}:bv[8]: the cast widens 1111 with zeros
n {255}:bv[8]	prints 1: an all-ones constant is shown as the top

Prefer braced constants ({ #x01 }, {1}:bv[8]) whenever a number is intended, and read a bare 1 in bitvector output as "all ones". The saturating idioms below rely on this: i1' is 2^w - 1 - i1 because the complement is taken against the all-ones top.

min and max are call-style builtins, defined only for bitvectors: using them on operands of any other Boolean algebra is a type-resolution error. Like the comparison operators they compare unsigned, so e.g. max({200}:bv[8], {100}:bv[8]) is {200}:bv[8] even though 200 is negative as a signed 8-bit value. For satisfiability they are handed to CVC5 as ite(bvule(x, y), ...); under predicate blasting (-B) they blast through a fresh result variable r constrained by ((x < y) -> r = x) && ((x >= y) -> r = y) (the dual for max), with no constant-operand precondition. Being self-delimiting they take no part in operator precedence, and the names min and max are reserved: a user function of that name can no longer be called with exactly two arguments.

The (bv[n]) entry is a cast. It converts its operand to the bitvector type of the given width, for example:

(bv[8]) x = { #x1f } : bv[8]

The cast operand must be a parenthesized term, a constant, a variable, a function call, 0, 1, a negation, a functional quantifier or another cast; wrap anything else in parentheses.

A cast converts between bitvector widths only. Its operand must itself be a bitvector term, and its result is a bitvector of the target width that takes part in the surrounding formula like any other term: casting an sbf or tau term, or mixing a cast with a non-bitvector sibling as in ((bv[8]) x:bv[4]) & y:sbf = 0, is a type error reported during type inference.

Division and remainder by zero

Division and remainder are total functions with the SMT-LIB semantics of bvudiv and bvurem (as implemented by CVC5). Neither raises an error on a zero divisor; instead, for a bitvector x of width w:

x / 0  =  2^w - 1     (all-ones, the maximum value of bv[w])
x % 0  =  x

In particular x / 0 yields the maximum of the type — the least safe default for anything metering, pricing or otherwise accumulating — so never rely on it implicitly. The same rule reaches x / x and 0 / x: both are {1} and 0 only for x != 0, and the maximum at x = 0, so the normalizer leaves them unfolded while x is symbolic; 1 / 0 and 1 % 0 are the all-ones top element again. When a divisor can be zero, guard it in the specification and pick the zero-case value explicitly:

always ( ( i2[t]:bv[24] != { #x000000 }:bv[24] && o1[t]:bv[24] = ( i1[t]:bv[24] / i2[t]:bv[24] ) )
      || ( i2[t]:bv[24] =  { #x000000 }:bv[24] && o1[t]:bv[24] = { #x000000 }:bv[24] ) ).

Here 1200 / 3 gives 400 as usual, while a zero divisor gives 0 — the spec author's own choice — instead of the inherited 16777215.

Overflow: checked and saturating arithmetic

+, -, * and << are modular, with the SMT-LIB semantics of bvadd, bvsub, bvmul and bvshl: results wrap around at the bit width silently — there is no error, no flag and no carry bit. A wrapped value looks like any other value, so a specification that must not wrap has to say so itself. Since Tau is a constraint language, the overflow condition is expressible with the ordinary operators, and a specification can branch on it. The patterns below are the recommended forms; all examples use bv[24], whose maximum is { #xffffff } (16777215), but nothing in them is width-specific.

Saturating addition. Unsigned addition overflowed iff the sum is smaller than an operand:

always ( ( ( i1[t]:bv[24] + i2[t]:bv[24] ) >= i1[t]:bv[24] && o1[t]:bv[24] = ( i1[t]:bv[24] + i2[t]:bv[24] ) )
      || ( ( i1[t]:bv[24] + i2[t]:bv[24] ) <  i1[t]:bv[24] && o1[t]:bv[24] = { #xffffff }:bv[24] ) ).

  16777115 + 100  ->  16777215   (exact sum, no clamp needed)
  16777215 + 100  ->  16777215   (clamped instead of wrapping to 99)

Checked multiplication by a constant. The largest safe operand floor((2^w - 1) / n) is itself a constant, so the guard is a plain comparison — no arithmetic at all. For n = 5 at width 24 the threshold is { #x333333 }:

always ( ( i1[t]:bv[24] <= { #x333333 }:bv[24] && o1[t]:bv[24] = ( i1[t]:bv[24] * { #x000005 }:bv[24] ) )
      || ( i1[t]:bv[24] >  { #x333333 }:bv[24] && o1[t]:bv[24] = { #xffffff }:bv[24] ) ).

  3355443  ->  16777215   (largest exact product)
  3355444  ->  16777215   (clamped instead of wrapping to 4)

Checked multiplication by a variable. When the multiplier is itself a stream there is no precomputable threshold; the round-trip test (a * b) / b = a detects the wrap (guard the divisor per Division and remainder by zero):

always ( ( i2[t]:bv[24] != { #x000000 }:bv[24] && ( ( i1[t]:bv[24] * i2[t]:bv[24] ) / i2[t]:bv[24] ) =  i1[t]:bv[24]
           && o1[t]:bv[24] = ( i1[t]:bv[24] * i2[t]:bv[24] ) )
      || ( i2[t]:bv[24] != { #x000000 }:bv[24] && ( ( i1[t]:bv[24] * i2[t]:bv[24] ) / i2[t]:bv[24] ) != i1[t]:bv[24]
           && o1[t]:bv[24] = { #xffffff }:bv[24] )
      || ( i2[t]:bv[24] =  { #x000000 }:bv[24] && o1[t]:bv[24] = { #x000000 }:bv[24] ) ).

  4000000 * 5  ->  16777215   (detected; the raw product wraps)

Saturating (monus) subtraction. Underflow is an ordering comparison:

always ( ( i1[t]:bv[24] >= i2[t]:bv[24] && o1[t]:bv[24] = ( i1[t]:bv[24] - i2[t]:bv[24] ) )
      || ( i1[t]:bv[24] <  i2[t]:bv[24] && o1[t]:bv[24] = { #x000000 }:bv[24] ) ).

  100 - 1000  ->  0   (clamped instead of 16776316)

Getting the addition predicate subtly wrong is easy, so prefer copying these forms over re-deriving them.

With the min/max builtins, the two saturating forms above collapse to single expressions — no branch at all. i1' is the bitwise complement, i.e. 2^w - 1 - i1, so the addend below can never push the sum past the maximum:

always o1[t]:bv[24] = ( i1[t]:bv[24] + min(i2[t]:bv[24], i1[t]:bv[24]') ).   # saturating +
always o1[t]:bv[24] = ( i1[t]:bv[24] - min(i1[t]:bv[24], i2[t]:bv[24]) ).    # saturating (monus) -

The checked-multiplication patterns keep their branches: the product itself wraps, so no post-hoc min can recover it. The exact (widened) arithmetic mode below lifts exactly this restriction, for callers willing to opt in.

Exact (widened) arithmetic mode

Everything above is modular: intermediate results wrap silently at the operands' declared width, so a computation that must not overflow has to be reasoned about with the guard patterns above, or, for addition and subtraction only, with the min/max idiom that closes this section. Tau also offers an opt-in exact (widened) arithmetic mode that instead computes each atomic formula's arithmetic exactly, as over the naturals, at whatever width is needed to avoid any overflow, and truncates only once, at the point where a result is actually stored. Under this mode the checked-multiplication gap admitted just above disappears: min(i1*i2, K) becomes a correct, guard-free saturating multiplication.

The mode is off by default and changes nothing when disabled. Turn it on with:

• the command line options --bv-widening (enable the mode; disabled by default) and --bv-max-width <n> (cap the width the mode is allowed to compute at; 0 leaves the current cap unchanged, 1024 unless already set). Both apply whether Tau is run as a REPL or given a specification file directly.
• the matching REPL options bv-widening (on/off, set bv-widening on) and bv-max-width (numeric, set bv-max-width <n>; 0 leaves the current cap unchanged) — like bv-case-split, a BA-declared option with no dedicated api<node> setter of its own.

Semantics. For every bitvector atomic formula (an equality, a comparison, an interval), the mode computes, bottom-up, the minimum width W at which none of the atom's arithmetic can overflow:

Node	Needed width
variable, io_var, constant	the atom's own declared or inferred width w (a leaf's own type is not consulted separately)
a + b	max(width(a), width(b)) + 1
a - b	max(width(a), width(b))
a * b	width(a) + width(b)
a / b, a % b	width(a) (a quotient or remainder never exceeds the dividend)
a << k (k a constant)	width(a) + k
a >> k, a >> v (either kind of shift right)	width(a)
a << v (v a variable)	width(a) — see caveat below
min(a, b), max(a, b)	max(width(a), width(b))
&, |, ^, ', !&, !|, !^	max of the operand widths — run at W like everything else, see caveat below

W is the largest of these over the whole atom. Every leaf is upcast once to bv[W] by zero-extension and every operator is retyped bv[W]; there is no interior truncation anywhere. The only place a result is ever cut back down is an equality with exactly one bare variable/stream side (an "assignment"): there, the other side is computed at W and then cast down, truncating, to the variable's own declared width — so o1[t] = i1[t] + i2[t] still stores the same wrapped sum as in the default mode, while o1[t] = min(i1[t] + i2[t], K) lets min see the exact, unwrapped sum before it clamps. A comparison, an interval, or an equality between two compound expressions is instead extended on both sides and compared or equated exactly, with no truncation at all — this is where the mode is most visible: i1*i2 <= c stops wrapping.

The mode changes what formulas mean. Widening is not a faster or more precise way of answering the same question: it rewrites every atom into a different formula, one over exact arithmetic, before any decision procedure sees it, so satisfiability, validity, normalization, solve, and the realizability of a specification are all decided for that rewritten formula. A formula whose truth depends on wrap-around can therefore flip its answer when the mode is switched on:

sat ex x:bv[4] (x:bv[4] << {4}:bv[4] != {0}:bv[4]).

  modular                        ->  F   (a 4-bit value shifted left by 4 is always 0)
  widened (--bv-widening)        ->  T   (the shift runs at W = 8: 1 << 4 = 16 != 0, so x = 1 works)

valid all x:bv[8] (x:bv[8] + x:bv[8] >= x:bv[8]).

  modular                        ->  F   (128 + 128 wraps to 0 < 128)
  widened (--bv-widening)        ->  T   (the sum runs at W = 9 and never wraps)

n x:bv[4] << {4}:bv[4] = {0}:bv[4]

  modular                        ->  T
  widened (--bv-widening)        ->  (bv[8]) x<<{ 4 }:bv[8] = 0

Neither answer is wrong; they answer different questions. The modular answer is the one for the formula as written over bv[4]/bv[8], and the widened answer is the one for its exact-arithmetic reading. So the mode must be chosen for a specification as a whole, not toggled around individual queries, and a wrap-around that a specification relies on (a mask computed by shifting, a counter meant to roll over) has to be pinned with an explicit cast, which the mode leaves untouched: sat ex x:bv[4] ((bv[4]) (x:bv[4] << {4}:bv[4]) != {0}:bv[4]). answers F in both modes. The only construct that keeps its modular meaning on its own is the assignment truncation described above: always o1[t]:bv[4] = i1[t]:bv[4] << {4}:bv[4] && o1[t] != {0}:bv[4] stays unsatisfiable with the mode on, because the shifted value is cut back to 4 bits when it is stored in o1[t].

Which commands see the mode. The widening pass runs at the entry of the normalizer, after definitions have been expanded, so a command decides the widened formula exactly when it normalizes its argument. Everything else handles the formula as written, in modular arithmetic, even with the mode on:

Command	Widened	Notes
normalize / n on a formula	yes	prints the elaborated atoms with their casts; the result is a fixed point (n %1 returns it unchanged)
sat, unsat, valid	yes	on formulas and on specifications alike
solve	yes	the assignment is searched for in the widened atoms
run / r, a specification file, runtime updates	yes	every execution step normalizes the current specification, see below
dnf, cnf, nnf, mnf, qelim, subst, inst	no	these transform the tree without normalizing it
a bare term, a history entry	no	there is no atom to widen; the tree is stored as parsed

qelim ex x (x:bv[8] * { 16 }:bv[8] = { 0 }:bv[8] && x != { 0 }:bv[8]).

  modular                        ->  T   (x = 16: the product wraps to 0)
  widened (--bv-widening)        ->  T   (qelim does not normalize, so the same modular answer)

sat ex x:bv[8] (x * { 16 }:bv[8] = { 0 }:bv[8] && x != { 0 }:bv[8]).

  modular                        ->  T
  widened (--bv-widening)        ->  F   (the product runs at W = 16 and is never 0 for x != 0)

solve --bv (x:bv[8] * { 16 }:bv[8] = { 0 }:bv[8] && x != { 0 }:bv[8]).

  modular                        ->  x := { 240 }:bv[8]
  widened (--bv-widening)        ->  no solution

The split matters when commands are chained through the history: whatever a non-normalizing command has already decided stays decided in modular arithmetic (qelim above returns T, and sat %1 can only confirm it), while whatever it leaves in place as a formula is widened by the next normalizing command that receives it.

Normalization. n is the command that shows what the pass did: each leaf appears under its zero-extending cast, every operator is retyped, and an assignment keeps its truncating outer cast. Two details of the printed form are worth knowing:

• A constant product that would wrap is not folded while the mode is on, so n { 16 }:bv[8] * { 16 }:bv[8] prints the product itself instead of 0. Inside an atom the same product is computed exactly: n { 16 }:bv[8] * { 16 }:bv[8] <= { 200 }:bv[8] is F with the mode on and T without it, while n x:bv[8] = { 16 }:bv[8] * { 16 }:bv[8] is x = 0 in both modes, because an assignment truncates the exact 256 back to 8 bits.
• Definitions are expanded first and widened afterwards, so a call whose body carries the arithmetic is widened like inline arithmetic: with fn(a:bv[8]) := a * a., n fn(x) <= { 200 }:bv[8] prints { 200 }:bv[16] !< (bv[16]) x*(bv[16]) x. A call that is not expanded is an opaque subterm and leaves its atom modular, see below.

Execution. The interpreter normalizes the current specification at every step — the initial specification, its expanded definitions, and any update merged at runtime — so with the mode on each step is solved over the widened atoms. Inputs are read at their declared width and outputs are stored at theirs: an output equation is an assignment, so the value that reaches the stream is always truncated to the stream's width, exactly as in the default mode. What changes is everything that sits between the arithmetic and the store — a comparison guard, a min/max, a division — which now sees the exact intermediate value. Two runs on bv[8] inputs 16, 200, 3:

always o1[t]:bv[8] = i1[t]:bv[8] * { 16 }:bv[8].

  modular                        ->  0, 128, 48    (256 and 3200 wrap on the way into o1)
  widened (--bv-widening)        ->  0, 128, 48    (same: the assignment truncates the exact product)

always (   i1[t]:bv[8] * { 16 }:bv[8] <= { 200 }:bv[8] && o1[t]:bv[8] = i1[t]:bv[8] * { 16 }:bv[8] )
    || (   i1[t]:bv[8] * { 16 }:bv[8] >  { 200 }:bv[8] && o1[t]:bv[8] = { 200 }:bv[8] ).

  modular                        ->  0, 128, 48    (the guard compares the wrapped product, so it never fires)
  widened (--bv-widening)        ->  200, 200, 48  (the guard sees 256 and 3200 and clamps)

A runtime update goes through the same normalization when it is accepted, so its widened form is what gets merged and printed. With u[t] = i1[t] running and o1[t]:bv[8] = min({ 16 }:bv[8] * { 16 }:bv[8], { 200 }:bv[8]) proposed on i1:

  modular                        ->  u[0] := always o1[t]:bv[8] = 0              then o1[1] := 0
  widened (--bv-widening)        ->  u[0] := always o1[t]:bv[8] = { 200 }:bv[8]  then o1[1] := 200

A proportional value is the everyday case of this: ( i1[t] * 5 ) / 100 wraps at the operand width in the default mode as soon as i1 * 5 exceeds the maximum, while with the mode on the product is formed at twice the width, the quotient is exact and — a quotient never needing more bits than its dividend — the final truncation into the output is lossless. At bv[24] with i1 = 3355444 the default mode stores 0 and the widened mode stores the exact 167772.

Realizability follows the same reading: whether a specification is accepted for execution or rejected (Tau specification is unsat) is decided for its widened formula. Inputs are universally quantified, so a constraint on an input that only holds without wrap-around is rejected in the default mode and accepted with the mode on:

always o1[t]:bv[8] = { 1 }:bv[8] && i1[t]:bv[8] * { 2 }:bv[8] >= i1[t]:bv[8].

  modular                        ->  Tau specification is unsat   (i1 = 128 doubles to 0 < 128)
  widened (--bv-widening)        ->  o1[0] := 1, o1[1] := 1, ...  (the product runs at W = 16, so it always holds)

Conversely a specification that is only satisfiable thanks to a wrap-around is rejected with the mode on:

always o1[t]:bv[8] * { 16 }:bv[8] = { 0 }:bv[8] && o1[t]:bv[8] != { 0 }:bv[8].

  modular                        ->  o1[0] := 240                (240 * 16 = 3840 wraps to 0)
  widened (--bv-widening)        ->  Tau specification is unsat  (no nonzero 8-bit value has a zero exact product)

The setting is global to the process (--bv-widening/bv-widening) and is read at each normalization, so choose it before a specification is built and keep it for the whole run rather than switching it between steps.

Caveats.

• Subtraction still wraps on underflow: -'s needed width never grows on its own (max(width(a), width(b))), so an underflowing subtraction still wraps, just at W rather than at the base width when it sits above an already-widened operand. Guard it exactly as in the default mode, with a >= b.

• A variable-amount left shift is the one operation the mode cannot bound: accounting for every possible shift amount could need up to w + 2^{w_v} - 1 bits, so a << v for a variable v still executes at W and can still wrap there. A constant-amount shift, a << k, is fully accounted for and exact.

• Complement and the other negating bitwise operators (', !&, !|, !^) act at W, not at the operand's own declared width, because every operator in the atom runs at the atom's computed width. So x' means 2^W - 1 - x, not the base-width complement zero-extended — meaning the saturating idiom min(i2, i1') from the previous section no longer means "clamp against i1's own maximum" once i1' is computed at some wider W:

  sat ex x ((x:bv[8] * { 255 }:bv[8])' <= { 200 }:bv[8]).
  
    modular                        ->  T   (x = 1 gives complement 0 <= 200)
    widened (--bv-widening)        ->  F   (the complement is computed at W = 16, always >= 510)
  

  If a specific width is intended, pin it explicitly with a cast, exactly as in the default mode:

  (bv[8]) i1[t]:bv[8]'          # the base-width (8-bit) complement, regardless of the surrounding computation's width
  

  A cast is always a boundary for this pass: whatever it wraps is left untouched — it computes exactly as it does in the default mode, at its own widths — and its result enters the surrounding widened computation at the cast's declared width, recovering today's exact meaning even with the mode switched on — e.g. adding the cast to the query above, sat ex x ((bv[8]) (x:bv[8] * { 255 }:bv[8])' <= { 200 }:bv[8])., answers T again with --bv-widening still on.

Payoff. With the mode on, the two saturating patterns that need a branch in the default mode — and the checked multiply that needs one no matter what, per the admission above — both collapse to a single min:

always o1[t]:bv[8] = min( i1[t]:bv[8] + i2[t]:bv[8], { 200 }:bv[8] ).   # guard-free saturating +

  200 + 100  ->  200   (exact sum 300 does not fit under {200}, so min clamps to it)
  200 + 100  ->  44    (default mode: the sum itself already wrapped to 44 before min ever ran)

always o1[t]:bv[8] = min( i1[t]:bv[8] * i2[t]:bv[8], { 200 }:bv[8] ).   # guard-free checked *

  16 * 16  ->  200   (exact product 256 does not fit under {200}, so min clamps to it)
  16 * 16  ->  0     (default mode: the product itself already wrapped to 0; no post-hoc min can recover it)

The second pattern is the one this section opened by ruling out: with the mode on, the multiplication itself never wraps, so min sees the real product and the previously-impossible checked multiply becomes an ordinary guard-free expression.

Opaque subterms. An atom containing a subterm the width computation does not understand — a function or predicate call, a capture — is left exactly as written, in modular semantics, with no diagnostic: the mode widens only atoms whose arithmetic it can see through completely. Expand such calls (or rewrite the atom without them) if it must be exact.

Cap. W is bounded by --bv-max-width/bv-max-width (default 1024); a formula that would need a wider computation fails cleanly instead of growing without bound. Exceeding it logs two error lines and the query answers conservatively rather than crashing or hanging, e.g.:

(Error) bv-widening: required width 16 exceeds bv-max-width 8
(Error) is_tau_formula_sat: normalization failed (bv-widening cap exceeded); answering unsat. This is a conservative fallback, not a proof.

A satisfiability check answers unsat (F), a validity check answers "not valid", and constructing or updating a specification that would exceed the cap is rejected the same way — in every case this is a conservative fallback the cap forces, not a proof that the formula is actually unsatisfiable/invalid/unacceptable.

Cost. The mode is inert — identical performance — when off. When on, a ground or lightly-quantified spec runs about as fast as the default mode; widening one atom's arithmetic by a few dozen extra bits is cheap for CVC5. Quantified nonlinear arithmetic is a different story: doubling the width of a product inside a quantifier can turn an instant query into an intractable one, e.g. valid all x all y ((x:bv[64]*y:bv[64])/y = x || y = {0}:bv[64]) answers in well under a second in the default mode but does not finish in five minutes once widened to bv[128]. The mode is at its best for executable specs and ground or lightly-quantified reasoning; deep quantified nonlinear arithmetic may need the cap, or restructuring the specification, to stay tractable.

The guard idioms from the previous section remain the answer in the default mode, and stay available — and correct — with the exact mode switched on too. demos/demo_2.4-exact_bitvector_arithmetic.tau walks through the mode interactively, including the cap and a saturating stream accumulator.

Precedence of term operations

The order of all term operations, bitvector and Boolean alike, is the following (from higher precedence to lower):

(bv[n]) > ' > & > ^ > | > !& > !^ > !| > { %, *, / } > { -, + } > { <<, >> } > fex > fall

The three groups in braces are shared precedence levels: %, * and / sit together at one level, - and + at the next, and << and >> at the last. Operators of one level chain left to right, so a + b - c parses as (a + b) - c and a * b / c as (a * b) / c. Parenthesize whenever the intent is not obvious.

Functions and predicates

Another key concept in the Tau Language are functions and predicates. They are given by the following grammar where function_def defines the syntax for a function and predicate_def defines the syntax for a predicate:

function_def      => function ":=" term
function          => name "[" index+  "]" "(" [ variable ("," variable)* ] ") [":" type]"
predicate_def     => predicate ":=" spec
predícate         => name "[" index+  "]" "(" [ variable [":" type] ("," variable [":" type])* ] ")"

where name is the name of the function or predicate (it has to be a sequence of letters and numbers starting by a letter), typeis the type of the arguments or the function itself (as considered in Type System) and index is a positive integer or a variable or a variable minus a positive integer, i.e.:

index => number | variable | variable "-" number

Simple examples of function definitions are

union(x, y, z) : sbf := x | y | z
intersection(x, y, z) :sbf := x & y & z
bf(a, b, x) : tau := ax | bx'

while sample predicate definitions are

bottom(x) := x = 0
not_atom(x : tau) := ex y y < x && y != 0
chain(x,y,z) := x < y && y < z

Furthermore, it is supported to define a function or a predicate by means of a recurrence relations. Let's see a small example for such a function definition:

rotate[0](x,y,z) : sbf := x & y | z
rotate[n](x,y,z) : sbf := rotate[n-1](y,z,x)

As can be seen rotate[n](x,y,z) is defined in terms of rotate[n-1](y,z,x). Together with the initial condition rotate[0](x,y,z), rotate[k](x,y,z) can be calculated for any positive number k, and essentially rotates the arguments counterclockwise until reaching rotate[0](...).

A similar but more complex example for predicates is

f[0](w,x,y,z) := x & { G o1[t] = 0 } != 0
f[n](w,x,y,z) := f[n-1](x,y,z,w)

h[0](w,x,y,z) := f[0](w,x,y,z)
h[n](w,x,y,z) := h[n-1](w,x,y,z) && f[n](w,x,y,z)

As a result, calling h[3](w,x,y,z) checks that none of the arguments w, x, y, z assumes F o1[t] != 0.

As can be seen, recurrence relations can also refer to other recurrence relations. The rule one must follow is that the index at the right-hand side of := is not bigger than any index on the left. In addition, there must be no circular dependency among the recurrence relation definitions in use.

Furthermore, we support the calculation of a fixpoint of a defined recurrence relation during normalization. The syntax is to call a defined recurrence relation as

name "(" [ variable ("," variable)* ] ")" [":" type] [ "fallback" fp_fallback ]

hence, omitting the index. For example, using the recurrence relation h from above, we can call the fix point by typing into REPL normalize h(x,y,z,w).

Not all recurrence relations have a fixpoint. The enumeration of the successive steps may instead enter a loop, and the optional fallback clause says what to return in that case:

fp_fallback => "first" | "last" | term | local_spec

• first returns the step at which the loop was detected,
• last returns the step just before it, and
• any term or formula returns that value verbatim (it must have the same type as the recurrence relation).

If no fallback clause is given, the default is 0 for functions and F for predicates. For example:

normalize h(x,y,z,w) fallback last

The enumeration of successive steps is unbounded by default. It can be capped with the -E, --max-enum-steps command line option or the max-enum-steps REPL option (see REPL options); if neither a fixpoint nor a loop is found within the cap, the search gives up with an error. Such a cap is a bound on the search, not a proof that no fixpoint exists.

It should be noted that recurrence relations in the Tau language are a conservative extension, meaning that they do not add to the general expressiveness.

Constants

Constants in the Tau Language are elements of some available Boolean algebra, usually different from just 0 and 1. Constants in a particular Boolean algebra come with their own syntax.

In the Tau language, we currently support the following base types. Most are Boolean algebras; qlt is ω-categorical and decidable, and is supported for that reason:

1. the Boolean algebra of Tau specifications (also referred to as Tau Boolean algebra)
2. the Boolean algebra of simple Boolean functions (sbf)
3. the Boolean algebra of bitvectors of fixed bit width (bv)
4. the ω-categorical theory of dense linear order without endpoints (qlt) — rationals under <; ω-categorical and decidable, hence supported
5. the Boolean algebra of rational intervals [x, y) (qint) — left-closed, right-open; accepts both rational (1/4) and decimal (0.25) constants
6. the Natural Language Boolean Algebra (nlang)
7. the Boolean algebra of lex-half-open polyhedra in ℝ^d (hsb) — generalizes qint from 1D to d dimensions using canonical halfspaces

The Boolean algebra of Tau specifications is an extensional Boolean algebra that encodes Tau specifications over arbitrary available other Boolean algebras. As a result, it is possible to have a Tau specification that itself has a Tau specification as a constant, allowing controlled reasoning of Tau specifications over Tau specifications.

Given the available algebras, the general syntax for constants is the following:

constant => "{" (spec | term) "}" [":" base_boolean_algebra_type]

where base_boolean_algebra_type is given by:

base_boolean_algebra_type => "tau" | "sbf" | "bv" '[' bit_width ']'
                           | "qlt" | "qint" | "nlang" | "hsb"

Note that the bit width of a bitvector type is mandatory: bv[8] is a type, while a bare bv is not. Beware that omitting the width is not reported as an error — bv is simply not recognized as a type name, and the expression is reinterpreted as something else (x:bv = 0 parses as xv = 0, a conjunction of two variables).

As mentioned, we can have a Tau specification seen as a Boolean algebra element (you can omit the type, since tau is the default type). For example, the following is a valid constant in the Tau Boolean algebra:

{ ex x ex y ex z (x & y | z) = 0 } : tau

or even a deeper nesting resulting in

{ { ex x ex y ex z (x & y | z) = 0 } : tau = 0 } : tau

where x, y and z are variables.

A constant in the simple Boolean function algebra is for example:

{ (x & y | z) } : sbf

where x, y and z are variables.

Finally, a constant in the bitvector Boolean algebra follows the syntax:

constant => '{' "#b" [0-1]+ | "#x" [0-9a-fA-F]+ | [0-9]+ `}`

For example, the following are valid bitvector constants of width 8:

{ #x1f } : bv[8]

or

{ #b00011111 } : bv[8]

Streams

Streams represent the input and the output of Tau specifications. They are the communication with the outside world, so to speak. We currently have two kinds of them: input streams and output streams. The syntax is given by

stream_variable => name "[" index "]"

where name is a sequence of letters, numbers and _ starting with a letter, and index is defined in subsection Functions and predicates. Hence, o1[t], i1[t], sensor[t] and log_out[t-1] are all valid stream variables.

Whether a stream is an input or an output is determined in one of two ways:

1. by an explicit stream definition (:= in ... / := out ..., see below), or
2. otherwise by its name: a name starting with i (or the special name this) is an input, and a name starting with o (or the special name u) is an output.

A stream that is neither declared nor matches one of those naming conventions cannot be resolved as an input or an output. This is why the conventional names i1, i2, ... and o1, o2, ... used throughout this document work without any declaration.

Both kinds of streams are indexed by time starting at the time step 0. A stream associates to each time step a Boolean algebra element matching the type of the stream.

Which Boolean algebra element is associated, is decided by the Tau specification in which the stream is used. For example, the specification G o1[t] = 0 says that o1 associates 0 to each time step. One can alternatively think about this as the value 0 being written into the stream o1 at each time step.

There are several ways how a stream can refer to a time point. The following list uses an output stream but input streams can be used in these same ways:

1. o1[t] refers to the current time point while executing a specification
2. o1[t-k] refers to the time point k steps ago while executing a specification
3. o1[k] refers to the fixed time point k while executing a specification

There are currently two ways to assign a type to a stream: either explicitly in a stream definition (see below) or implicitly, by type inference from the context in which the stream is used. The inference is performed by the general type system described in section Type system, so constants, variables and other streams occurring in the same atomic formula all contribute to the inferred type. A stream that remains untyped after inference is assigned the default type tau.

In case a type mismatch is detected, the specification is rejected and execution does not start.

The syntax of a stream definition is

stream_definition => stream_name [member_path] [":" type] ":=" ("in" | "out") stream

where stream_name is the name of the stream, type is a supported type (tau, sbf, bv[8], qlt, qint, nlang, hsb, ..., or a user-defined type — see Abstract data types), member_path is an optional tuple-member path (also discussed there), in marks an input stream and out an output stream, and stream is either console (meaning that the stream reads/outputs values from/to the console) or file(file_name) which denotes the file from/into which to read/write (in quotes if needed). For example,

i1 : tau := in console

or

o1 : tau := out console

or

o2 : tau := out file("log.tau")

or, using an arbitrary stream name,

sensor : bv[8] := in file("samples.in")

Stream definitions can be given either as part of a specification's definitions (each terminated by .) or entered directly in the REPL — see subsection Functions, predicates and input/output stream variables.

Special streams

There are two predefined special tau streams called u and this which are discussed in the beginning of section pointwise revision and subsection the this input stream.

Variables and uninterpreted constants

Variables range over Boolean algebra elements. As mentioned in subsection Boolean functions, each variable can only appear as part of a term and has, thus, a unique type.

The syntax for the non-terminal variable depends on whether the charvar option is enabled or not. See REPL options for further details about the option. The option is enabled by default.

If charvar is enabled, a variable is a single letter followed by an arbitrary sequence of numbers.

If charvar is disabled, a variable can be any sequence of letters, numbers and _, must however be started by a letter.

A variable (or stream variable) of a tuple type may additionally be followed by a member path, as in l.tag or s.line.p.a — see Abstract data types.

In the Tau language a variable can appear free or quantified universally or existentially. Since a Tau specification has to be a closed formula, in order to be executable, variables appearing in this context must appear under the scope of a quantifier. In the Tau REPL, however, you can also work with open formulas (i.e. when variables are not quantified).

Uninterpreted constants

Finally, we also have uninterpreted constants. They can be thought of as a variable being implicitly existentially quantified from the outside of the Tau specification. For this reason, from a semantic point of view, they behave more like variables than constants. The syntax is mentioned above in subsection Boolean functions. The appearance of an uninterpreted constant within a Tau specification keeps the specification closed. Note that when executing a specification containing uninterpreted constants they are currently assigned a default value in a suitable way and the specification is then executed with those assignments.

Type system

Available types

The Tau Language currently supports the following base types:

1. tau: the type of Tau specifications,
2. sbf: the type of simple Boolean functions,
3. bv[n]: the type of bitvectors of bit width n,
4. qlt: the ω-categorical theory of the rationals under < (dense linear order, no endpoints) — ω-categorical and decidable, hence supported,
5. qint: the Boolean algebra of left-closed, right-open rational intervals [x, y); accepts both rational (1/4) and decimal (0.25) endpoint constants,
6. nlang: the Natural Language Boolean Algebra (its oracle needs an API key: nlang-api-key, TAU_NLANG_API_KEY, or OPENAI_API_KEY / ANTHROPIC_API_KEY, see Known LTL limitations), and
7. hsb: the Boolean algebra of lex-half-open polyhedra in ℝ^d — generalizes qint from 1D to d dimensions using canonical halfspaces (see hsb).

In addition, user-defined type names — aliases of base types and tuple types — can be introduced with a type definition; see section Abstract data types.

You can type the following elements: variables, streams, recurrence relations, constants and (term) constants. In order to do so, you just add the type information after a colon :. For example,

x : sbf
o1[t] : bv[8]
{ #b00001111 } : bv[16]
{ ex x ex y (x & y) = 0 } : tau
1: tau

are all valid typed elements.

qlt — ω-categorical dense linear order

qlt represents the first-order theory of the rationals under <: a dense linear order without endpoints. This theory is ω-categorical, decidable, and admits quantifier elimination, which is why tau-lang supports it. Every definable set is a finite Boolean combination of open/half-open/closed intervals with rational endpoints.

tau-lang treats qlt specially: its quantifiers are decided by qlt's own elimination (qlt_omcat_qe), not by the Boolean-algebra pipeline (the comparison hooks <, >, ≤, ≥ have their own semantics, and bf_* Boolean-function rewrites do not apply).

Elements are written as interval expressions inside {...}:qlt:

{ (0,1) }:qlt          -- open interval between 0 and 1
{ [0.5,2) }:qlt        -- half-open interval; 0.5 parses as 1/2
{ (-inf,0) }:qlt       -- everything less than 0
{ (0,1) | [3,5) }:qlt  -- union of two intervals
{ 0.45 }:qlt           -- singleton constant (decimal accepted)
{ 1/3 }:qlt            -- singleton constant (rational form)

Endpoints are exact rationals. The special symbols -inf and +inf represent the extended line endpoints. Parentheses (, ) exclude the endpoint; brackets [, ] include it. Both rational (p/q) and decimal (0.d…) literal syntaxes are accepted. A literal whose reduced value does not fit a 64-bit numerator over a positive 64-bit denominator is a parse error.

A qlt variable or stream stands for one point of the order, while a constant {...}:qlt stands for a set of points. Where a term combines a variable x with constants, x reads as the set holding just its point:

• c & x != 0 says that x lies in c, and c & x = 0 that it does not; c & x' != 0 says that c holds a point other than x;
• x = c holds only when c is the single point x, so ex x (x = {[0,1]}:qlt) is F and ex x (x = {1/2}:qlt) is T;
• x = 0 and x = 1 never hold: the typed 0 and 1 are the ends of the order, below and above every point;
• x & y' = 0 says that x is y, and x & y = 0 that it is not;
• <, <=, >, >= compare points.

A quantifier over a qlt variable is decided by cells: the finite endpoints of the constants cut the rationals into the endpoints, the open gaps between them and the two rays beyond them, and every point of one cell satisfies the same atoms. One point per cell therefore decides ex (some cell satisfies the body) and all (every cell does), exactly. So ex x ((({3}:qlt & x) != 0) && (({5}:qlt & x) != 0)) is F (no point is both 3 and 5) and all x ((({(0,1)}:qlt & x) != 0) -> x < {1}:qlt) is T. With one other free variable y the result is the set of the points of y for which the body holds: ex x (x > y && ({[0,1]}:qlt & x) != 0) is y{ (-inf, 1) }:qlt != 0. An order atom between two variables is eliminated by the dense-order rules (ex x (a < x && x < b) is a < b). When none of these applies the binder stays. A decision by cells evaluates at most --qlt-cells-budget instances and ranges over at most --qlt-cells-max-params other free variables or named endpoints; past either it is left open (the binder stays, solve answers UNKNOWN).

solve, run and a program of tau compile give every qlt variable or output one rational, never top, bot or an interval: qlt's own solver picks the values, preferring simple ones, and solve answers no solution when no points satisfy the system (solve {(0, 1)}:qlt x = 0 gives x := { 0 }:qlt; solve x:qlt = {[0, 1]}:qlt has no solution). A system the solver cannot decide (an atom it does not read, a constant with a named endpoint, a spent cell budget, a value past the rationals of 64-bit numerator and denominator, as in solve x:qlt > {9223372036854775807}:qlt) answers UNKNOWN with the reason, never no solution. Points have no least or greatest choice, so --min and --max give a point as well. always o1[t]:qlt != o2[t]:qlt runs as o1 := 1, o2 := 0. When no strategy exists, run says the specification is unrealizable.

A constant may name an endpoint ({c}:qlt, {(c0, c1)}:qlt): the name is an unknown rational. A comparison or a quantifier over such constants is decided only when it has the same truth wherever the names lie among the other endpoints, so {c}:qlt = {c}:qlt is T and ex x (x = {c}:qlt) is T, while {c}:qlt != {0}:qlt and ({c}:qlt & {0}:qlt) = 0 stay as they are (c may be 0). An interval between names is empty when they are out of order, so {(c, d)}:qlt = 0 stays as it is, while {[c, c]}:qlt = 0 is F. An operation whose result would depend on where a name lies is kept as a term instead of being folded into one constant. A formula made of such comparisons alone is decided whole, by the same rule: {c}:qlt < {d}:qlt || {d}:qlt <= {c}:qlt is T, while {c}:qlt < {d}:qlt stays.

An order atom against a constant reads every point of it: x < c holds when x is below every point of c (below inf c, or at it when c does not hold it), x <= c when x is at most every point, and x > c, x >= c dually against sup c; for a constant that is one point this is the usual order. Between two constants every point of the left side is compared with every point of the right, so {[0,1]}:qlt <= {[0,1]}:qlt is F. Such a comparison is not total: x >= c is not the negation of x < c, and core keeps the two apart. An empty constant is the typed 0, which stays the order's lower end.

qint — atomless Boolean algebra of rational intervals

qint represents the atomless Boolean algebra of left-closed, right-open intervals [a, b) over the rationals on the extended real line. Elements are finite unions of such intervals. The sentinels -inf and +inf are supported as endpoints.

Every endpoint is an exact rational with a 64-bit numerator and denominator, so 1/3 and 0.3333333333333333 are different endpoints. Rational (1/4), decimal (0.25, 2e-3) and integer endpoint syntaxes are accepted, plus -inf/+inf; a literal whose exact value does not fit is rejected rather than rounded. An endpoint prints as an integer, a terminating decimal or p/q. Inside {...}:qint, a bare 0 and 1 are the algebraic bottom and top; any other bare number is rejected, because qint has no points -- write an interval such as [n, n+1) instead.

Elements are written as interval expressions inside {...}:qint:

{ [0,1) }:qint           -- unit interval [0, 1)
{ [1/2,+inf) }:qint      -- from 1/2 to +infinity (rational syntax)
{ [0.5,+inf) }:qint      -- identical to above (decimal syntax)
{ [-inf,0) }:qint        -- everything strictly negative
{ [0,1/2) | [1,2) }:qint -- union of two intervals

Each piece is a left-closed, right-open interval, and every Boolean combination is again a finite union of such intervals. qint is atomless: it has no atoms and no points, so a single point cannot be written.

hsb — lex-half-open polyhedra

hsb represents the atomless Boolean algebra of lex-half-open polyhedra in ℝ^d (LP_d^Q). It generalizes qint from 1D to d dimensions using canonical halfspaces.

Mathematical construction. For a normal vector w ∈ ℝ^d \ {0}, define:

• L(w) = min{i : w_i ≠ 0} — the lex-leading index
• s(w) = sign(w_{L(w)}) ∈ {+1, −1} — the lex-leading sign

The canonical halfspace H_{w,b} is:

• { x : ⟨w,x⟩ + b ≤ 0 } if s(w) = −1 (closed — boundary included)
• { x : ⟨w,x⟩ + b < 0 } if s(w) = +1 (open — boundary excluded)

Key properties:

1. Complement: ℝ^d \ H_{w,b} = H_{−w,−b}. Negating the normal flips the lex-leading sign, hence flips open↔closed.
2. No equalities: for any v ≠ 0, exactly one of {⟨v,x⟩ ≤ c} and {⟨v,x⟩ ≥ c} is canonical, so {⟨v,x⟩ = c} is never expressible.
3. Atomless: every non-empty element has non-empty interior (because no equalities → full-dimensional cells). This is the defining property of an atomless Boolean algebra.
4. 1D reduction: when d = 1, H_{w,b} gives exactly the half-open intervals [a, b) of qint.

Elements are formula trees of canonical halfspaces combined with Boolean operations (&, |, ~). Emptiness checking uses Fourier-Motzkin elimination to test LP feasibility of each conjunctive cell in the DNF expansion.

hsb is registered in the dispatcher pack and main.cpp (available as a data-sort alongside sbf, bv, qint, qlt, and nlang).

Parsed constant syntax. The parse_hsb function accepts:

Input	Meaning
top, { top }	Universe (ℝ^d)
bot, bottom, { bot }	Empty set
x[0] < 0	Single open halfspace (x[0] < 0)
0 <= x[0]	Single closed halfspace (x[0] >= 0): read as -x[0] <= 0
x[0] < 1	Constant bound: read as x[0] - 1 < 0
x[1] <= x[0]	Variable bound (x[0] >= x[1]): read as -x[0] + x[1] <= 0
x[0]*0.5 + 0.7 < 0	Halfspace with coefficient and bias
0.5*x[0] + -0.3*x[1] + 0.7 < 0	Multivariate halfspace
2*x[0] < x[1] - 1	Linear expressions on both sides: read as 2*x[0] - x[1] + 1 < 0
(x[0] < 0 & x[1] < 0)	Conjunction of halfspaces (parentheses required)
((x[0] < 0 & x[1] < 0) | ~(x[2] < 0))	Disjunction and negation

Coefficients can appear before (0.5*x[0]) or after (x[0]*0.5) the variable. Both sides of a half-space are linear expressions (linexpr < linexpr or linexpr <= linexpr); the parser moves the right-hand side to the left, so x[0] < 1 is x[0] - 1 < 0, x[1] <= x[0] is -x[0] + x[1] <= 0, and x[0] + x[1] < x[1] + 3 is x[0] - 3 < 0. A comparison whose variables all cancel (x[0] < x[0], 1 < 2) is rejected. Coefficients and biases are unsigned numbers written as integers, decimals (0.5) or fractions (1/2); a leading - negates a term, and a fraction with a zero denominator is rejected.

Strictness is canonical, not chosen by the operator. The algebra is the Boolean algebra of lex-half-open polyhedra: for a normal vector w whose first non-zero coefficient is positive the algebra contains only the open half-space ⟨w,x⟩ + b < 0, and for a negative leading coefficient only the closed one ⟨w,x⟩ + b <= 0; the complement of an element flips both the sign and the strictness, which is what keeps the family closed under the Boolean operations. So x[0] < 1 (open, x[0] < 1) and 1 <= x[0] (closed, x[0] >= 1) are elements, while the closed set x[0] <= 1 and the open set x[0] > 1 are not. A literal whose operator names one of the two missing sets (x[0] <= 1, 1 < x[0]) is rejected with an error that shows the element the algebra does have (x[0] - 1 < 0, -x[0] + 1 <= 0); put the leading variable on the other side of the comparison to name the other bound. The printed form of an element always shows its canonical operator. Inside {...}:hsb, &, | and ~ combine constraints; every &/| combination must be parenthesised. The same combinations are also available through the Boolean algebra operations at the formula level.

The test suite (src/boolean_algebras/hsb/tests/test_hsb.cpp) covers Fourier-Motzkin elimination, complement closure, splitter, Boolean combinations, parser, dispatcher integration, and LTL(hsb) realizability.

nlang — Natural Language Boolean Algebra (experimental)

Note: nlang is experimental. Its semantics depend on an external LLM oracle and results may be non-deterministic or inconsistent across API calls. Use for exploration and prototyping only.

nlang represents a Boolean algebra whose elements are natural language concept descriptions (strings). Boolean operations compose descriptions using English connectives:

• { A }:nlang | { B }:nlang produces "(A) or (B)"
• { A }:nlang & { B }:nlang produces "(A) and (B)"
• ~{ A }:nlang produces "not (A)"

An LLM endpoint serves as the semantic oracle for equality, emptiness, and universality tests. Two providers are supported: openai, any OpenAI-compatible chat completions endpoint (<endpoint>/chat/completions), and anthropic, the Anthropic Messages API (<endpoint>/messages).

Every setting is an option of nlang, with the same name on each surface: the command line (--nlang-model claude-opus-5-5), the REPL (set nlang-model claude-opus-5-5, get nlang-model), the options repository of the C++ API (idni::options().set_text("nlang-model", ...)) and the Python and JavaScript bindings (set_option("nlang-model", ...)). An option takes its environment variable at start, and an empty text option takes its default:

option	kind	environment	default
nlang-provider	text	TAU_NLANG_PROVIDER	detected, else openai
nlang-endpoint	text	TAU_NLANG_ENDPOINT	https://api.openai.com/v1 or https://api.anthropic.com/v1
nlang-model	text	TAU_NLANG_MODEL	openai: none, the endpoint picks its own; anthropic: claude-opus-5-5
nlang-api-key	text	TAU_NLANG_API_KEY	OPENAI_API_KEY or ANTHROPIC_API_KEY by provider
nlang-effort	text	TAU_NLANG_EFFORT	low for the default anthropic model, none otherwise
nlang-max-tokens	count	TAU_NLANG_MAX_TOKENS	16000 (0 = the default)
nlang-http-timeout	count	TAU_NLANG_HTTP_TIMEOUT	15 seconds (0 = no cap)
nlang-fallback	flag	TAU_NLANG_FALLBACK	on

• Provider detection. When nlang-provider is empty, the provider is anthropic when the endpoint names an anthropic host, or when no endpoint is given and ANTHROPIC_API_KEY is the only provider key; otherwise it is openai. A value other than openai or anthropic is an error, also in the variable.
• The key is never read back. nlang-api-key is accepted on every surface, and every read (get nlang-api-key, get_option) answers set or unset. A key given on the command line is visible in the process list and in the shell history, and one typed in the REPL is saved in its history file (.tau_history): prefer the environment variable. Giving a key does not change which provider is detected.
• nlang-effort, nlang-max-tokens and nlang-fallback apply to anthropic only. The effort is one of low, medium, high, xhigh and max. A model the user names gets no effort unless it is set, because not every model accepts it. With the fallback on, the Anthropic API may answer from another model when the named one declines the request.
• A reply that holds no answer (a refusal, a reply cut at nlang-max-tokens, an error object, an HTTP error or a request that fails or times out) is treated as unanswered: the conservative default is used, it is not cached, and a warning is printed once.
• Changing the provider, endpoint, model or effort drops the cached oracle answers, since an answer of one model is not another's.
• The 15 second default of nlang-http-timeout may be short for a model that thinks before it answers; raise it when requests time out.

Without a key every emptiness, universality and equivalence question is answered false (a warning is printed once; the default is not cached), so verdicts over nlang elements are not reliable without the key.

Elements are written as natural language strings inside {...}:nlang:

{ mammals }:nlang
{ large birds }:nlang
{ X | (Y & Z) }:sbf         -- not nlang; use plain strings for nlang

The content inside {} for nlang is a natural language phrase, with a small structural layer: nothing and everything denote bottom and top, and not (φ), (φ) and (ψ), (φ) or (ψ) compose phrases (this is the canonical form the Boolean operations print). Any other text is a single atom.

Requirement: an API key (nlang-api-key, TAU_NLANG_API_KEY, or the provider's OPENAI_API_KEY / ANTHROPIC_API_KEY) must be configured for the oracle to answer.

bv — bit width and unification

The bit width of a bitvector type is mandatory: x : bv[8] is well-formed, while x : bv is not a bitvector annotation at all (see Constants). Each width is a distinct type, so bv[8] and bv[16] never unify — unifying them is a type error, not an implicit widening (use an explicit cast, see Bitvectors).

In the case of functional recurrence relations (as all arguments must have the same type) the syntax is as follows:

f(x) : tau := ...
g[n](x, y) : sbf := ...

In the case of predicate recurrence relations, the syntax is different as each argument can have its own type. The syntax is as follows:

p(x : tau) := ...
q[n](x : sbf, y : tau) := ...

In general, if no type information is present, the default type tau is assumed. Also note that bv actually denotes a family of types, one for each bit width. For example, bv[8] is the type of bitvectors of width 8, while bv[16] is the type of bitvectors of width 16.

Type inference

The Tau Language has a type inference system which infers types of all elements that are not explicitly typed and detect type mismatches.

The inference system is base on a union-find data structure and works by unifying types of elements appearing together in the same context.

Moreover, the inference system is scoped, i.e. types inferred within a certain scope do not leak outside of that scope (unless the element is scoped in an outer scope). For example, argument types inferred within a function definition do not leak outside of that function definition.

Among others, we have the following scopes:

1. global scope: the scoped elements are untyped variables and streams of the formula,
2. recurrence relations definitions: the scoped elements are the arguments of the recurrence relation (everything is resolved taking into account those type arguments): variables, streams and constants,
3. existential and universal quantifications: the scoped elements are the quantified variables, and
4. atomic formulas: the scoped elements are constants appearing in the atomic formula.

Depending on the scope, we also merge the types of the different elements to be typed:

1. untyped variables and streams in the global scope are assigned the default type tau,
2. in a recurrence relation definition:
   • in the functional case: everything is typed acoordingly to the type of the recurrence relation: argument variables, constants, streams,...
   • in the predicate case: everything is typed accordingly to the involved argument types: variables, constants, streams,...
3. in an existential or universal quantification:
   • the quantified variable is typed accordingly to the type inferred in the quantified formula,
4. in an atomic formula:
   • everything is merged together and typed accordingly: variables, streams, constants,...

If we have no type information, the default type tau is assumed.

Examples

Here are some small examples to illustrate the type inference system:

1. x = y && y = z:sbf:

   • ``xis inferred to be of the same type asy`,
   • z is typed as sbf,
   • y is inferred to be of the same type as z, i.e. sbf,
   • no type mismatch occurs.

2. all x:bv[16] x = y:

   • x is typed bv[16],
   • y is inferred to be of the same type as x, i.e. bv[16],
   • no type mismatch occurs.

3. all x x = y:

   • x is inferred to be of the default type tau, as no type information is present,
   • y is inferred to be of the same type as x, i.e. tau,
   • no type mismatch occurs.

4. (all x x = y) && x = y:sbf:

   • x is inferred to be of the same type as y in the first part, i.e. tau, as no type information is present,
   • y is inferred to be of type sbf in the outer formula which is not compatible with the previous type assigned (tau).
   • a type mismatch occurs.

5. all x (all x x = 1:sbf):

   • the inner x is inferred to be of type sbf,
   • the outer x is inferred to be of the default type tau,
   • no type mismatch occurs as both x are in different scopes.

6. ex x x = 1 : bv[8]:

   • the constant 1 is typed as bv[8] (it is the all-ones vector {255}:bv[8], see 0 and 1 in bitvectors),
   • x is inferred to be of the same type as the constant 1, i.e. bv[8],
   • no type mismatch occurs.

7. x:bv[8] = {1}:bv[16]:

   • x is typed as bv[8] and the constant as bv[16],
   • the two bitvector widths are distinct types and do not unify,
   • a type mismatch occurs.

Abstract data types

Besides the base types described in Type system, the Tau Language supports user-defined types, declared with the keyword type. A type definition is a definition like any other (see Tau specifications): as part of a specification it is terminated by ., and it can equally be entered on its own in the REPL, where it persists for the session and is listed by definitions|defs.

The syntax is:

type_def     => "type" name [ ("of" | "/") type_parents ] ("is" | "=") type_body
type_parents => "(" name ("," name)* ")"
type_body    => tuple | type
tuple        => "{" member ("," member)* "}"
member       => name ":" type

The spellings of (...) and / (...) are interchangeable, and so are is and =. Type definitions may reference types declared later in the same specification — resolution is order-independent.

Aliases

The simplest form introduces a new name (an alias) for an existing type:

type byte = bv[8].

Anywhere a type annotation is accepted, byte now means bv[8], so x:byte = x:bv[8] holds. Commands that report values, such as solve, resolve the alias to its underlying type in their output.

Tuples

A tuple type collects several named members, each with its own type:

type Point = {a: sbf, b: sbf}.

An equality between two values of a tuple type expands member-wise, and the expansion happens at parse time, before any normalization: x:Point = y:Point is read as x.a = y.a && x.b = y.b.

An individual member is reached with the . operator: p.a is member a of p. Member types may themselves be tuple types, nesting to arbitrary depth, and a member path then chains accesses: s.line.p.a. Member-wise expansion works at any depth, not only at the leaves, so an equality between two tuple-typed members again expands to all their flattened members. When a member is accessed on a quantified variable, annotate the variable at the binder and parenthesize the body, so that the member access sees the annotation:

ex l:Line (l.tag = 0 && l.p.a = 0)

solve reports one value per flattened member, not a single tuple value.

Inheritance

A tuple type may inherit the members of one or more other tuple types:

type Tagged = {tag: byte}.
type Line of (Tagged) is {p: Point, q: Point}.

The parents' members come first, in declaration order, followed by the type's own members, so Line flattens to tag, p.a, p.b, q.a, q.b.

Errors and re-declaration

A type definition is rejected with an error when it declares a duplicate type name within one specification, a duplicate member (including one introduced via inheritance), a cycle (through members, aliases or parents), or when it inherits from something that is not a tuple type or is not declared. An undeclared name in a member position is not an error — it is treated as a base (non-ADT) type and passed through unchanged.

Re-declaring a type name in a later REPL command replaces the earlier definition: the last definition wins. The same holds for repeated stream definitions (tuple-typed ones included) — note, however, that a stream name keeps the type it was first declared with for the rest of a REPL session.

Tuple-typed streams

A stream may be declared with a tuple type; it then reads and writes all its members together, as one value, in a JSON-like wire format that nests exactly like the type declaration (not like the dotted member paths):

type Point = {a: sbf, b: sbf}.
i : Point := in console.
o : Point := out console.
o[t] = i[t]

with console input (and output) of the form:

{ a: "1", b: "0" }

Unlike a tau-valued stream, the wire literal is complete on its own line — no terminating period is needed. File streams work the same way, one wire literal per line.

A specification may also copy just part of a tuple between streams, e.g. (o[0].a = i[0].a). A member the specification does not copy at some time point is not left dangling: the emitted tuple initializes it to the default value of that member's own Boolean algebra, which is that algebra's 0. Beware, however, that a member the specification never mentions at any time point has no output stream at all, and the tuple, missing one member, is then never written.

Many worked examples can be found in demos/demo_4.1-abstract_data_types.tau.

Constant time constraints

Besides the relations between terms, a formula can also constrain the time point at which it applies. Such a constraint is written in square brackets and compares a time variable against a constant:

time_constraint => "[" ctnvar rel num "]" | "[" num rel ctnvar "]"
rel             => "=" | "!=" | "<" | "<=" | ">" | ">="

where ctnvar is a time variable (typically t) and num a non-negative integer. The constraint evaluates to T at the time points that satisfy it and to F elsewhere, so it acts as a guard on the rest of the formula. For example:

[t <= 3] && o1[t] = 0

is unsatisfiable: a top-level formula holds at every step, and its first conjunct fails from step 4 on. A constraint guards the rest of the formula through an implication instead, so

always ([t < 3] -> o1[t] = 0) && ([t >= 3] -> o1[t] = 1)

writes 0 into o1 for the first three time steps and 1 afterwards.

Note that the operand order matters and is not normalized: [t >= 3] means "the current time point is at least 3", whereas [3 >= t] means "3 is at least the current time point", i.e. at most 3.

A time constraint may also sit under the operators of full LTL, where it reads the absolute step: (o1[t] = 0) until (o1[t] = 1 && [t = 3]) asks o1 to become 1 exactly at step 3, and (always ([t = 0] -> o1[t] = 0)) && (sometimes always o1[t] = 1) is satisfiable.

Pointwise revision

As mentioned in the beginning, pointwise revision refers to the feature to incorporate updates into a currently running specification. To this end, the special output stream u is introduced. A Tau specification written into this stream, will be interpreted as a potential update. If the proposed update is not satisfiable as a stand-alone specification, no update is performed. Otherwise, the pointwise revision procedure is called, updating the currently running specification with the specification written into u.

Minimal example

Let us work with a concrete, minimal example to make the idea more clear. Afterwords, the algorithm for pointwise revision is explained in more detail.

Suppose we execute the specification u[t] = i1[t]. By default, both streams are of type tau. This can be done in the REPL by just entering

run u[t] = i1[t]

u[t] is the special output stream, while i1[t] is an ordinary input stream. Hence, the specification says that the input into i1 is written into u in each step of execution. We now input o1[t] = 1 for i1[0]. This will yield the following output:

u[0] := o1[t] = 1

Since o1[t] = 1 is a satisfiable specification, the update is accepted and in the following step 1, the running Tau specification is

u[t] = i1[t] && o1[t] = 1

If we now input o2[t] = 0 && o2[t] = 1 for i1[1] in the next step, no update is performed, because o2[t] cannot be 0 and 1 at the same time. So this is an example of a very simple unsatisfiable specification.

Finally, in the next step we input o1[t] = 0 for i1[2] as a proposed update. This is a satisfiable specification but contradicts the currently running specification (we required o1[t] = 1). The pointwise revision algorithm will replace the previous specification with the update, yielding just o1[t] = 0, in order to ensure that the new specification is satisfiable.

Running this example in REPL (see The Tau REPL below) yields:

tau> run u[t] = i1[t]

Temporal normalization of G specification reached fixpoint after 0 steps, yielding the result:
i1[t]u[t]' = 0 && i1[t]'u[t] = 0

-----------------------------------------------------------------------------------------------------------
Please provide requested input, or press ENTER to terminate                                               |
If no input is requested, press ENTER to continue to the next execution step, or type q(uit) to terminate |
-----------------------------------------------------------------------------------------------------------

Execution step: 0
i1[0] := o1[t] = 1
u[0] := G o1[t]' = 0

Updated specification:
G o1[t]' = 0 && i1[t]u[t]' = 0 && i1[t]'u[t] = 0

Execution step: 1
i1[1] := o2[t] = 0 && o2[t] = 1
o1[1] := T
u[1] := F

Execution step: 2
i1[2] := o1[t] = 0
o1[2] := T
u[2] := G o1[t] = 0

Updated specification:
G o1[t] = 0

Execution step: 3
o1[3] := F
u[3] := F

Execution step: 4
o1[4] := F
u[4] := F
...

Note, in order to interpret the output, that 1 of type tau is represented as T and O as F. Furthermore, Tau specifications are always displayed normalized during execution. The REPL informs the user whenever an update was done successfully by printing the new, updated specification.

The this input stream

Aside from u there is another special stream which can be utilized in specifications incorporating updates. The special stream is called this and behaves in the same way as an input stream. However, the input is not asked from the user. Instead, the currently running specification is written into the this stream at each point in time. For example the following specification always prints the currently running specification using the output stream o1: u[t] = i1[t] && o1[t] = this[t].

Pointwise revision details

The following is a detailed explanation of the pointwise revision algorithm. Pointwise revision is performed at the end of an execution step in which a Tau specification, let's call it update, is written into the output stream u. First, it is checked if update is satisfiable. This means that for any given input at any given step during execution, there has to exist output satisfying the specification, where in this later case the standard definition of satisfiability for a logical formula is meant. If update is not satisfiable, it normalizes to F and no update is applied.

In case update is satisfiable, the following steps are performed:

1. update can refer to previous memory positions by using negative numbers in a stream index, for example o1[-k]. Let t be the current time point of execution. Then o1[-k] is replaced with the value at o1[t-k]. If no such memory position is present, no update is performed. Furthermore, t-k must not be below 0. After replacing all such streams with the respective value from the memory, it is checked again if update is satisfiable given these memory references. If it is unsatisfiable, no update is performed. Otherwise, we move to the next step:
2. Let us refer to the currently running specification as spec. spec is composed of a single G statement and possibly several F statements. We denote the G part by aw_spec and the collection of F parts by st_spec. In the same way aw_update denotes the G part of update. The next candidate for the updated specification, let's call it U, is given by
   U := update && ( (ex [outputs] aw_update && aw_spec) -> aw_spec), where [outputs] refers to the list of all output streams present in aw_spec and aw_update combined. The meaning is that, whenever possible given the current input at a particular step, update and aw_spec are executed together. The name pointwise revision originates from this behavior. Note that it is possible to refine the definition of the new specification in more advanced ways. We will explore this aspect in the future.
   If update is satisfiable, then U is satisfiable, unless the F part of update prevents it. If it is prevented, update becomes the final updated specification. Otherwise, U becomes the updated specification and the next step is performed.
3. As a final step, it is checked if the previous F statements st_spec are executable along the updated specification U. If this is the case, they are added to the updated specification. Otherwise, U is accepted as the final update.

Note that in the step after an update was successfully applied, the new specification starts running as if it was started at time step 0 shifted to the correct time step to match the overall history. This means, in particular, that streams with lookback k only become solvable once the specification has continued for at least k steps. For example, updating a specification in step s with o1[t] = i1[t-1] means that in the next step o1[s+1] is unspecified. To see this, assume we start at step 0. Then o1[t] = i1[t-1] will leave o1[0] unspecified since i1[-1] is not defined, since we do not allow defining negative time steps in general. The only exception is during pointwise revision in order to allow access to previous stream values, as explained in step 1 above. A specification, unlike an update, cannot read a stream at a fixed position before step 0: sat, run and the other formula commands refuse o1[-1] with "the stream position o1[-1] is before step 0, which no run plays".

The restart applies to the whole revised specification, the parts it keeps from the running one included: an always clause that looks back k steps holds only from k steps after the revision, and its current-time conjuncts are not enforced before. In run always u[t] = i1[t] && o1[t]:bv[1] != o1[t-1]:bv[1], an update always o4[t]:bv[1] = 1 applied at step 3 leaves o1[3] and o4[3] free; from step 4 on, both hold again. A run whose strategy comes from the data game is revised differently: its game starts from the values already played, so its clauses hold from the revision step on (see the data game above).

An update that no clause of a safety run plays, such as a disjunction whose disjunct the system must pick by the inputs or a temporal operator nested in another, is handed to the data game: when the game of the revised specification is won, the run plays its strategy from the revision step on, as a run that started with that specification would.

Reserved symbols

Tau Language has a set of reserved symbols that cannot be used as identifiers. In particular, we require that T and F are reserved for truth values in Tau specifications and 0 and 1 stand for the corresponding Boolean algebra elements. The names min and max are reserved for the builtin bitvector operations (see Bitvectors): a two-argument call min(x, y) or max(x, y) always denotes the builtin, never a user-defined function of the same name.

Command line interface

Tau-lang ships one executable, tau, with two roles:

• interpreter / REPL — runs a specification by solving each time step through the core solver pipeline. Best for REPL use, spec authoring, and executing specifications dynamically.
• tau gen / tau codegen / tau compile — the ahead-of-time compiler. tau gen reads a specification file, invokes the synthesis pipeline once, and writes a standalone CMake project. tau compile does the same and then builds it into an executable that steps the synthesized strategy (see tau gen and tau compile).

Both roles share the same spec format. Use whichever matches your deployment story.

tau — interpreter and REPL

The general form of the tau executable command line is:

tau [ options ] [ <specification file> ]
tau [ options ] gen|codegen|compile [ command options ] <specification file>
tau import-tlsf <spec.tlsf> [ -o, --output <spec.tau> ]

where [ options ] are the global options and [ <specification file> ] is the path to a file containing the Tau specification you want to run. A global option comes before the command: tau -S debug compile spec.tau, not tau compile -S debug spec.tau. Use - to read the specification from standard input. If you omit the file, the Tau REPL will be started.

The general options are the following:

Option	Description
-h, --help	detailed information about options
-l, --license	show the license
-v, --version	show the version of the executable
-V, --charvar	char-as-variable short form (enabled by default)
-B, --preprocessing	master switch for BA-specific preprocessing passes, e.g. bv predicate blasting (disabled by default)
-K, --ba-component-factoring	decide tau-algebra constants per support component (enabled by default)
-S, --severity	severity level (trace/debug/info/error); default info
-I, --indenting	indent formulas in output
-H, --highlighting	syntax highlighting
-b, --benchmarks	print benchmarks (enabled by default)
-J, --json	output in JSON format
-q, --quit	quit when no input is available (scripted runs)

Whereas the REPL specific options are:

Options	Description
-e, --evaluate	REPL command to be evaluated
-s, --status	display status (enabled by default)
-c, --color	use colors (enabled by default)
-X, --legacy-repl	use the legacy terminal REPL instead of the FTXUI one
-x, --experimental	enable transitioning features
-d, --debug	debug mode (Debug builds only)

and the limit options, which bound the engine's iterative searches. The table names each default. The two temporal-normalization caps (--max-fixpoint-steps, --max-flag-search-steps) ship at 500 because those searches have no termination guarantee — unlimited turns a non-converging spec from a loud give-up into a hang (pass 0 to opt in); 0 means unlimited for every cap except where the table says otherwise (--ba-decision-pins, --ltl-mealy-max-* and --compile-max-table-edges read it as none, --spec-size-warn as off); and the two gc knobs keep their tuned defaults. Each is also a REPL option of the same name (see REPL options) and reads its variable TAU_<NAME> at start (see Options and the environment). The flag wins over the variable:

Option	Description
-w, --spec-size-warn	warn when an updated specification exceeds this many characters (default 0; 0 = off)
-a, --max-revision-alts	cap the revision alternatives kept per specification part, dropping middle preference tiers (default 0; 0 = unlimited)
-Z, --pwr-semantic	enable the semantic (winning-region) fallback of the temporal pointwise revision (off by default)
-t, --step-definitional-propagation	propagate the constants a step formula determines before its paths are enumerated, one path instead of 2^k for k guards reading them (on by default)
-p, --block-max-splits	cap per-block Boole-decomposition splits in anti-prenexing (default 0; 0 = unlimited)
-r, --block-max-rounds	cap anti-prenexing quantifier-block driver rounds (default 0; 0 = unlimited)
-N, --ba-decision-pins	decided tau-algebra rows whose key tree is kept alive across the step sweep (default 4096; 0 = none)
-Q, --cqe-max-clauses	cap the DNF clauses complete quantifier elimination may distribute one scope into (default 0; 0 = unlimited)
-g, --lgrs-max-vars	hand a pure-equality bitvector system with more distinct variables than this to the solver instead of squeezing it per width and computing a ground solution algebraically, whose Boole expansion is exponential in them (default 8; 0 = unlimited)
-f, --max-fixpoint-steps	cap temporal-normalization fixpoint steps; a give-up reports an error, not a verdict (default 500; 0 = unlimited)
-F, --max-flag-search-steps	cap the eventual-flag search past the flag boundary; a give-up reports an error, not a verdict (default 500; 0 = unlimited)
-z, --block-squeeze-cap	skip block squeezing above this operand-set size (default 0; 0 = unlimited)
-m, --max-simplify-rounds	cap bitvector simplification rewrite rounds (default 0; 0 = unlimited)
-P, --max-def-passes	cap definition-expansion passes (default 0; 0 = unlimited)
-E, --max-enum-steps	cap recurrence-relation enumeration steps (default 0; 0 = unlimited)
-M, --max-probe-steps	cap the untyped saturation probe over a residual recurrence reference (default 10000; 0 = unlimited)
-R, --max-rewrite-rounds	cap rewrite-to-fixpoint rounds (default 0; 0 = unlimited)
-G, --gc-min-size	tree-node count floor before gc may trigger (default 256)
-W, --gc-growth-factor	gc triggers when node count grows by this factor since last sweep (default 1.5; <= 0 disables the growth-triggered sweeps)
-y, --tref-budget	cap the live interned tree nodes; an api call that starts with the store at or above the cap fails instead of running (default 0; 0 = unlimited)
-C, --tref-budget-soft	percentage of --tref-budget at which a sweep is forced regardless of the gc growth trigger (default 75)
-j, --max-consistency-subsets	cap k-ary consistency subset checks per atom group in LTL(ABA) synthesis (default 4096; 0 = unlimited)
-n, --max-cover-products	cap the ABA oracle's mixed-type coverage expansion (default 256; 0 = unlimited)
-u, --max-constant-size	largest region of fresh values, in tree nodes, a run keeps across steps; past it new values come from the general solver (default 2000; 0 = unlimited)
-A, --cache-bound	bound the string-keyed synthesis caches, FIFO eviction (default 4096; 0 = unbounded)
-T, --ltl-timeout	wall-clock cap in seconds on each ltlsynt call (default 60; 0 = no watchdog)
-L, --ltl-alg	omcat synthesis algorithm: A, B, D or auto (default auto)
-k, --ltl-qe-max-vars	free-variable cap of the omcat QE fast path; above 2 is not sound (default 2; 0 = off)
-Y, --ltl-hoa-max-states	largest state count accepted from an ltlsynt HOA strategy (default 4194304; 0 = unlimited)
-U, --ltl-guard-max-cubes	cap the DNF cubes a HOA guard may expand into in the Algorithm D game (default 512; 0 = unlimited)
-D, --ltl-refinement-rounds	cap the ABA-oracle refinement rounds of a realizability check; the cap answers UNKNOWN (default 64; 0 = unlimited)
--ltl-self-check-steps	steps of the run that checks a realizable verdict of the LTL pipeline; a violated clause answers UNKNOWN (default 64; 0 = no check)
--ltl-strategy-max-states	most states of a strategy; above it ltlsynt is asked again with --simplify=bwoa-sat, and a strategy still above it answers UNKNOWN (default 0; 0 = no bound)
--ltl-compositional	decide and run the parts of a conjunction that share no output each for itself (default off)
--ltl-data-fixpoint-rounds	cap the rounds of one data fixpoint (a strategy checked against the data, a data game over formulas); the cap answers UNKNOWN (default 64; at most 4096, 0 = 4096)
-O, --ltl-window-max-paths	cap the strategy paths the multi-step window oracle examines per check (default 4096; 0 = unlimited)
--ltl-closed-regions-timeout	cap in seconds the data game's attempt on regions that keep their quantifiers, each question at most a quarter of it (default 20; 0 = no such attempt)
--ltl-data-game-max-nodes	cap the live nodes of the BDD of a data game over codes; a full table leaves the game undecided (default 8388608; 0 = unlimited)
--ltl-data-game-max-memo	cap the operation memo entries of the BDD of a data game over codes; a full memo is emptied (default 33554432; 0 = unlimited)
--ltl-data-game-max-combinations	cap the value combinations the data game tabulates for one comparison its circuits do not encode (default 4096; 0 = unlimited)
--ltl-max-observations	cap the observation props whose impossible joint values the synthesis skeleton assumes away (default 8; at most 30, 0 = 30)
--ltl-mealy-max-states	most states of the Mealy view a data-game strategy is played through (default 4096; 0 = no view)
--ltl-mealy-max-edges	most edges of the Mealy view a data-game strategy is played through (default 65536; 0 = no view)
--ltl-ctl-star-tableau-max-states	most states of the tableau that decides a CTL* E asked at several steps (default 64; 0 = unlimited)
--ltl-witness	on UNREALIZABLE, print the environment's winning strategy (HOA) to stderr
--ltl-export-strategy	print the winning strategy to stderr: hoa or dot (empty = off)
--ltl-export-strategy-file	also write the winning strategy (HOA) to this file (empty = off)
--phi-delta-crosscheck	compare the closed form of Phi_Delta against the solver on matching shapes and log a disagreement
--spot-bin	directory searched for ltlsynt, autfilt and ltlfilt after PATH (empty = off)
--ltl-minimize-strategy	merge the bisimilar states of each strategy ltlsynt returns
--ltl-simplification	ltlsynt --simplify: no, bisim, bwoa, sat, bisim-sat or bwoa-sat; none means no (empty = the ltlsynt default)
--ltl-synth-algo	ltlsynt --algo of a verdict: sd, ds, ps, lar, lar.old or acd; the data game tries it first (empty = the ltlsynt default)
--ltl-decompose	ltlsynt --decompose of a verdict: yes or no (empty = the ltlsynt default)
--ltl-semantics	read a temporal formula over infinite traces or over the finite traces of LTLf, whose end the system chooses: infinite or finite (default infinite)
--output-prefer	soft output preferences of each step, stream=value or stream=prev, comma separated, first strongest (empty = none)
--compile-max-table-edges	most edges of a Mealy view gen/compile carries as a table instead of solving as the program runs (default 400; 0 = none)
--compile-build-timeout	seconds the cmake build of tau compile may take before it is stopped and the compile fails (default 3600; 0 = no timeout)
--bf-dependence-max-nodes	cap the BDD nodes built to tell whether a Boolean function depends on a variable (default 65536; 0 = unlimited)
--lean-decide-crosscheck	re-decide the lean constant tests through the full normalization and report a disagreement

Beyond these, each Boolean algebra in the configured pack (-DTAU_BAS=, see "Selecting Boolean algebras" above) may declare CLI options of its own, addressed --<ba>-<option>, and present when that BA is part of the build. bv, for instance, declares --bv-blasting (bv's own predicate-blasting switch, enabled by default), --bv-blastdepth (cap blast-block re-entry nesting in anti-prenexing, 0 = unlimited), --bv-case-split (bitvector case split of quantified variables tested against constants, enabled by default), --bv-case-split-max-tests (cap the constants a quantified bitvector variable may be tested against for the case split, 0 = unlimited), --bv-definitional-elimination (eliminate existentially quantified bitvector variables that a total definition in their scope determines, before the case split; on by default) with its caps --bv-defelim-max-clauses, --bv-defelim-max-atoms, --bv-defelim-max-subset and --bv-defelim-max-rounds (flattened clauses per conjunct, guard atoms per propositional check, clause-subset size and rounds per block; defaults 16, 18, 4 and 256, 0 = unlimited except for the atoms, which stop at 30), --bv-quantifier-free-decision (decide a closed bitvector formula whose binders are all of one kind quantifier-free, off by default), --bv-blasting-max-nodes (the BDD nodes one predicate blasting may build before it declines; 500000 by default, 0 = unlimited), --bv-bitblast-max-width (the widest bitvector a question may hold to be decided on the bits of its values instead of by the solver; 16 by default, 0 leaves every question to the solver), --bv-bitblast-max-nodes (the BDD nodes a question over bitvectors of at most --bv-bitblast-max-width bits may keep in use at once when Tau decides it on the bits of its values, before the solver takes it instead; 1048576 by default, 0 leaves every question to the solver), --bv-solve-timeout (the seconds a bitvector question with quantifiers may take on the bits of its values, and, when it multiplies or divides two values that are not constants, in the solver, which then runs it in a separate process stopped at the limit; a question stopped there has no answer, so the command asking it answers UNKNOWN, naming the limit; 60 by default, 0 runs the solver in the process with no limit), --bv-widening (exact, widened bitvector arithmetic instead of modular wraparound, off by default) and --bv-max-width (cap the width widening may compute at; 1024 by default, and 0 sets the default again); bv blasts only when both --preprocessing/-B and --bv-blasting are on. Each option --bv-<option> reads TAU_BV_<OPTION> at start. In a build without bv, --bv-blasting, --bv-blastdepth, --bv-case-split, --bv-case-split-max-tests, --bv-definitional-elimination, the four --bv-defelim-max-* caps, --bv-quantifier-free-decision, --bv-blasting-max-nodes, --bv-bitblast-max-width, --bv-bitblast-max-nodes, --bv-solve-timeout, --bv-widening and --bv-max-width are not recognized options at all.

tau gen (tau codegen) and tau compile — synthesis-to-executable compiler

tau gen <spec.tau>... [ -o, --output-dir <dir> ] [ --aiger | --machine ]
tau codegen <spec.tau>... [ -o, --output-dir <dir> ] [ --aiger | --machine ]
tau compile <spec.tau> [ -o, --output <exe> ] [ -c, --cxx <c++ compiler> ] [ --preset <name> ] [ -D NAME=VALUE ]... [ -G <generator> ] [ --machine ]

tau gen (also spelled tau codegen) parses each spec file, prepares its execution exactly as the interpreter does, and emits <spec.tau>.build/ (a main.cpp driving the strategy plus a CMakeLists.txt that finds the tau SDK and links TAU::TAU, one preset per platform in CMakePresets.json, and the platforms.json and toolchain that file names). A spec file may be - (stdin, once per list). It emits a.build/. -o (--output-dir) names one output directory. It is an error with several spec files. tau compile runs gen. Then the SDK script cmake/tau-compile.cmake configures and builds the project for this machine by default, or for the --preset platform, and copies the program to -o <exe> (--output) (default: the spec path without its extension, or a.out / a.exe on Windows for stdin). tau compile - writes the artifact to a.build/. --preset names a platform or a ./dev preset name. -D and -G reach the emitted project configure. The program behaves like tau <spec.tau>: it reads inputs, prints outputs, and exits when its input closes. Exit code 0 on success, 1 on every failure, with the reason in the compile failed: message (see Generate and compile a spec). The program makes the moves run makes, because tau compile asks the interpreter what it executes. When run plays the Mealy machine of the data game's strategy, the program carries that machine as a table of up to 400 edges. A larger table would take the C++ compiler longer than the program below, which builds the machine when it starts, as run does. Otherwise run solves as it goes: each step through the safety pipeline, and, for a strategy of the abstraction or of a data game with no such machine, that game or synthesis when it starts. The program then executes the embedded spec the same way, with the same solver, so it needs ltlsynt where run does.

A table (build_program_desc, and make_table_provider in src/table_step_provider.h, which plays one in the interpreter) picks each step's outputs from the edge that step takes. It plays the strategy of the abstraction only when every claim an edge makes about the outputs can be met at that step whatever the inputs and the earlier values are, and the parts of the spec all start at the same step; otherwise a value chosen now could break the spec later, as o1[0] = 1 does for always o2[t] = o1[t-1] && o3[t] = o2[t-1] && o3[t-1] = 0. Such a strategy is refined the way run refines it: the data game is solved on the same abstraction, and the table plays the Mealy machine of its strategy. playable_table_solution returns the strategy a table plays. When the data game has no such machine, these functions return an error saying why, and the spec is executed by run (or tau compile). emit_program also refuses a Mealy machine of the data game that reads values before step 0, which its standalone class cannot carry; drive such a strategy through the table step provider.

tau import-tlsf — TLSF to Tau

tau import-tlsf <spec.tlsf> [ -o, --output <spec.tau> ]

tau import-tlsf writes the Tau specification of a TLSF basic file (the SYNTCOMP format, without parameters) to stdout, or to the -o path. Each input and output becomes a bv[1] console stream of the same name, a proposition a the atom a[t]:bv[1] = 1 (a[0] outside a temporal operator) and X φ the formula read one step later. The sections combine as the Mealy semantics of TLSF says, INITIALLY -> (PRESET && ((G REQUIRE) -> (ASSUME -> ((G ASSERT) && GUARANTEE)))), with an empty section left out. Strict and Moore semantics are refused. The result can be decided with realizable or given to tau gen --aiger.

When to use which

Situation	Use
Interactive spec authoring / debugging	tau REPL
One-off running of a spec against inputs	tau
Checking satisfiability / realizability of a spec	tau
Inspecting or editing the generated C++ project	tau gen / tau codegen
Deploying a realized spec as one binary	tau compile
Integrating the synthesized behaviour into a C++ project	the cpp_codegen.h library API (emit_program)
Specs with data atoms requiring runtime witness search	both: the compiled program solves witnesses per step through libTAU, as the interpreter does

The Tau REPL

The Tau REPL is a command line application that allows you to interact with the Tau Language. It is a simple and easy to use tool that enables you to write and execute Tau specifications on the fly.

By default the REPL uses a full-screen terminal interface based on FTXUI, with command history persisted in .tau_history. Pass -X (--legacy-repl) for the plain line-oriented REPL, which is also what you get if the project was configured with -DTAU_DONT_USE_FTXUI=ON.

Basic REPL commands

An input may span several lines. While it is incomplete, each further line starts with the continuation prompt ...>, aligned with the end of the tau> prompt.

The Tau REPL provides a set of basic commands that allow you to obtain help, version information, exit the REPL and clear the screen. The syntax of the commands is the following:

• help|h [<command>]: shows a general help message or the help message of a specific command.

• help|h example[s]: shows examples of the Tau language syntax.

• version|v: shows the version of the Tau REPL. The version of the Tau REPL corresponds to the repo commit.

• quit|q: exits the Tau REPL.

• clear|c: clears the screen.

• whatis <tau|term|repl_history>: shows the inferred type of an expression.

• reset: returns the session to the state it started in. It stops a run in progress, clears the history, the definitions, the input/output streams and the caches, and frees the memory nothing uses any more. Options keep their values.

• fragment ltl|ctl_star: selects the grammar fragment; ctl_star adds the A, E and - operators (see CTL* fragment).

REPL options

The REPL reads and writes the options of the options repository by name. An option has the name of its command line option, without the dashes in front (see Options and the environment). These commands use the name:

• get: shows every session option and its value.

• get <option>: shows the value of one option.

• set <option> [=] <value>: sets an option to a value. A flag takes on or off (also true/false, yes/no, 1/0). A count takes a number. A text takes letters, digits and . - _ : /, or any characters in double quotes.

• enable <option>: sets a flag to on.

• disable <option>: sets a flag to off.

• toggle <option>: switches a flag between on and off.

get shows a flag as true or false. An unknown name is an error (Unknown option). enable, disable and toggle refuse an option that is not a flag. The session options are the options of the engine, of the output and of the algebras in the pack. The options of the command line alone, such as help, evaluate and output-dir, are not in the list of get.

The flags and the words:

• color: Can be on/off. Controls usage of terminal colors in the output. It is on by default.

• status: Can be on/off. Controls status visibility in the prompt. It is on by default.

• severity: trace, debug, info or error. The value sets how much information the REPL gives. It is info by default, and debug in a build with DEBUG.

• highlighting: Can be on/off. Controls highlighting in the output of commands. It is off by default.

• indenting: Can be on/off. Controls indentation in the output of commands. It is off by default.

• json: Can be on/off. Controls output in JSON format. It is off by default.

• charvar: Can be on/off. Controls usage of character variables in the REPL. It is on by default.

• preprocessing: Can be on/off. Master switch for every BA-specific preprocessing pass, for example the predicate blasting of bv (see below). Off disables all of them, whatever their own setting. It is off by default.

• ba-component-factoring: Can be on/off. Controls support-component factoring of the tau-algebra constant tests: a constant whose clauses share no variables and refer to no absolute time is decided per component, each decision kept across steps, instead of as a whole. It is on by default.

• pwr-semantic: Can be on/off. Enables the semantic (winning-region) fallback of the temporal pointwise revision. This mode solves the revised specification again as an Algorithm D game over the qlt type. It is off by default.

• step-definitional-propagation: Can be on/off. Before the paths of a step are enumerated, normalizes the step formula once, substitutes every top-level o = c with c a constant and repeats until no new constant appears. It carries the values into the solution. A guard that reads a value the same step computes then folds instead of forking the enumeration, so a step with k such guards solves one path instead of up to 2^k. The solution set does not change. It is on by default.

• benchmarks: Can be on/off. Controls printing of timing benchmarks after each command. It is on by default.

• debug: Can be on/off. Controls debug mode. Only a build with DEBUG has it, and there it is on by default.

• ltl-alg: A, B, D or auto, the omcat synthesis algorithm. auto by default.

The other session options are counts. They take a number through set <option> <n>. A count above the largest the option holds is refused, never wrapped. 0 means unlimited, except where the entry below says otherwise: spec-size-warn and ltl-closed-regions-timeout read 0 as off, ba-decision-pins as none, gc-min-size as no floor, ltl-qe-max-vars as off, ltl-max-observations as 30 and ltl-data-fixpoint-rounds as 4096. gc-growth-factor takes a decimal, and a value at or below 0 disables the growth-triggered sweeps. Each count reads its variable TAU_<NAME> at start, and get shows the value in force:

• block-max-splits: per-block Boole-decomposition split budget in anti-prenexing. Unlimited by default.

• block-max-rounds: anti-prenexing quantifier-block driver round cap. Unlimited by default.

• ba-decision-pins: how many decided tau-algebra rows keep their key tree alive across the step sweep of the interpreter, oldest released first. 4096 by default. 0 disables the pinning (a raw count, not "unlimited").

• cqe-max-clauses: cap on the DNF clauses complete quantifier elimination may distribute one scope into. Unlimited by default.

• lgrs-max-vars: above this many distinct variables, a partition of pure bitvector equalities goes to the solver. It is not squeezed per width and given a ground solution algebraically (find_solution, or find_minimal_solution in minimum mode), whose Boole expansion is exponential in the variables. var = constant conjuncts are read off before the count. 8 by default.

• max-fixpoint-steps: temporal-normalization fixpoint step cap. Default

500. The search has no convergence guarantee, so unlimited (0) hangs on a non-converging spec instead of a loud give-up. A give-up is reported as an error ("gave up before reaching a result"), never as a T/F verdict.

• max-flag-search-steps: cap on the eventual-flag search past the flag boundary. Default 500, for the same reason as max-fixpoint-steps. A give-up is an error too, not an unsatisfiable verdict.

• block-squeeze-cap: operand-set size above which block squeezing declines. Unlimited by default.

• max-simplify-rounds: bitvector simplification rewrite round cap. Unlimited by default.

• max-def-passes: definition-expansion pass cap. Unlimited by default.

• max-enum-steps: recurrence-relation enumeration step cap. Unlimited by default.

• max-probe-steps: cap on the untyped saturation probe that calculate_fixed_point runs over a residual recurrence reference. The probe tells a type-blocked rule from a legitimately uninterpreted one. 10000 by default, since a diverging probe never stabilizes. A finite max-enum-steps makes it smaller. 0 = unlimited.

• max-rewrite-rounds: rewrite-to-fixpoint round cap. Unlimited by default.

• gc-min-size: tree-node count floor before the gc of the interpreter can start. 256 by default.

• gc-growth-factor: gc growth-factor trigger. It takes decimals such as 1.5. 1.5 by default. A value at or below 0 disables the growth-triggered sweeps. A store past tref-budget-soft still sweeps.

• tref-budget: cap on the live interned tree nodes. A command that starts with the store at or above the cap fails without running. A command that started finishes, also when it ends above the cap. Unlimited by default.

• tref-budget-soft: percentage of tref-budget at which the interpreter sweeps, whatever its gc growth trigger. 75 by default.

• spec-size-warn: warn when an updated specification exceeds this many printed characters. 0 (off) by default.

• max-revision-alts: cap on revision alternatives kept per specification part. Unlimited by default.

• output-prefer: soft preferences on the outputs of each step, as stream=value entries separated by commas, the first the strongest. A value is written as in an input file, and prev asks for the value the stream took at the step before. A step keeps all of them when it can, otherwise each one in order that still leaves a move. Only the outputs the step solves for are chosen this way; an output the strategy fixes, or a stream the step does not solve, keeps its value. Every move a step can make keeps the spec, so a preference never changes a verdict or whether a step runs. It applies to run and to programs tau gen builds, which read TAU_OUTPUT_PREFER when they run. An entry without =, a name that is not an identifier, or an empty value is an error; a value the stream's type does not parse is an error of the run. Empty by default.

• max-consistency-subsets: cap on the k-ary consistency subset checks per atom group in LTL(ABA) synthesis. 4096 by default. A fired cap is sound but can answer unrealizable.

• max-cover-products: cap on the mixed-type coverage expansion of the ABA oracle. 256 by default.

• max-constant-size: largest region of fresh values, in tree nodes, that a run keeps across steps. Each value a run commits shrinks the region, which grows with it. Past the cap the run stops tracking it, and new values come from the general solver. 2000 by default, 0 = unlimited.

• cache-bound: bound on the string-keyed synthesis caches, with FIFO eviction. 4096 by default. 0 = unbounded.

• ltl-timeout: wall-clock cap in seconds on each ltlsynt call. 60 by default. 0 disables the watchdog.

• ltl-qe-max-vars: free-variable cap of the omcat quantifier-elimination fast path. 2 by default. Values above 2 enable a fast path that is not sound.

• ltl-hoa-max-states: largest state count accepted from an ltlsynt HOA strategy. 4194304 by default. 0 = unlimited.

• ltl-guard-max-cubes: cap on the DNF cubes a HOA guard may expand into in the Algorithm D product game. 512 by default. 0 = unlimited.

• ltl-refinement-rounds: cap on the ABA-oracle refinement rounds of one realizability check. Each round blocks an infeasible strategy edge and runs ltlsynt again. 64 by default. 0 = unlimited. On the cap the verdict is an error (UNKNOWN), never a false answer.

• ltl-self-check-steps: steps of the run that checks a realizable verdict of the LTL pipeline. The specification is run on generated inputs and each top-level clause is read on the trace: a violation, which no correct strategy produces, turns the verdict into UNKNOWN. A clause the trace leaves open (an always it does not break, a sometimes it does not meet) counts as kept. 64 by default. 0 = no check.

• ltl-strategy-max-states: the most states a strategy of ltlsynt may keep, after ltl-minimize-strategy. A larger strategy is asked again with --simplify=bwoa-sat, and one still above the bound answers UNKNOWN. 0 by default, no bound.

• ltl-compositional: Can be on/off. Decides and runs the parts of a conjunction that share no output each for itself (see Compositional synthesis). Off by default.

• ltl-data-fixpoint-rounds: cap on the rounds of one data fixpoint, the check of a strategy against the data and each fixpoint of a data game over formulas. After a losing check, at most that many longer windows are searched for a blocking clause. 64 by default. At most 4096, and 0 means 4096: a fixpoint over formulas need not converge. On the cap the verdict is UNKNOWN.

• ltl-window-max-paths: cap on the strategy paths the multi-step window oracle examines per check. 4096 by default. 0 = unlimited. A hit cap also answers UNKNOWN.

• ltl-closed-regions-timeout: seconds the data game may spend on regions that keep their quantifiers, all their questions together, each question at most a quarter of it. 20 by default. 0 skips the attempt. Past either bound that attempt is undecided, and the other routes continue to decide.

• ltl-data-game-max-nodes: cap on the live nodes of the BDD a data game over codes builds. 8388608 (2^23) by default. 0 = unlimited. A full table leaves the game undecided.

• ltl-data-game-max-memo: cap on the operation memo entries of that BDD. 33554432 (2^25) by default. 0 = unlimited. A memo that reaches the cap is emptied, which costs only recomputation.

• ltl-data-game-max-combinations: cap on the value combinations the data game tabulates for one comparison its circuits do not encode. 4096 by default. 0 = unlimited. Past it the comparison has no code, and the game falls back to formula regions or is undecided.

• ltl-max-observations: cap on the observation props whose impossible joint values the synthesis skeleton assumes away, at 3^n feasibility checks. 8 by default. At most 30, and 0 means 30. Beyond it nothing is assumed, which leaves the environment moves no data produces.

• ltl-mealy-max-states, ltl-mealy-max-edges: the states and edges of the Mealy view a data-game strategy is played through. 4096 and 65536 by default. Past either the moves are played directly, and 0 builds no view.

• ltl-ctl-star-tableau-max-states: the states of the tableau that decides a CTL* E asked at several steps. 64 by default, 0 = unlimited. Past it the witness paths share one set of directions, and an unrealizable answer is UNKNOWN.

• ltl-witness, ltl-export-strategy, ltl-export-strategy-file, spot-bin: the LTL synthesis outputs and the Spot directory, as in the table of LTL synthesis options. Off or empty by default.

• ltl-semantics, ltl-minimize-strategy, ltl-simplification, ltl-synth-algo, ltl-decompose: how a temporal formula is read and how ltlsynt builds a strategy, as in the table of LTL synthesis options. infinite, off and the ltlsynt defaults by default.

• lean-decide-crosscheck, phi-delta-crosscheck: the two diagnostic flags of Options and the environment. Off by default.

• compile-max-table-edges: the edges of a Mealy view tau gen / tau compile carries as a table. 400 by default. A larger strategy is solved as the program runs, and 0 never carries a table.

• compile-build-timeout: seconds the cmake build of tau compile may take before it is stopped and the compile fails. 3600 by default. 0 waits without a bound.

• bf-dependence-max-nodes: cap on the BDD nodes the syntactic variable simplification builds to tell whether a Boolean function depends on a variable. 65536 by default. 0 = unlimited. Past it the question stays open, and the variable goes to the slower simplifications.

A change of a count, of preprocessing or of an option of an algebra between two queries drops the verdict memos. The next sat/realizable is then decided under the new budgets, not answered from the old ones.

Each Boolean algebra in the pack can declare options of its own, named <ba>-<option>. They exist when that BA is part of the build, and set/get/enable/disable/toggle take them like every other option. bv, for example, declares:

• bv-blasting: its own predicate-blasting switch. On by default, but it works only while the master preprocessing above is also on.
• bv-blastdepth: blast-block re-entry nesting cap in anti-prenexing. Unlimited by default.
• bv-case-split: the bitvector case split. A quantified bitvector variable that occurs only in comparisons against constants of its type is eliminated by one witness per cell those constants cut the domain into, before any quantifier block forms. On by default.
• bv-case-split-max-tests: cap on the constants a quantified bitvector variable may be tested against for the case split. Unlimited by default.
• bv-definitional-elimination: substitute an existentially quantified bitvector variable that a total definition in its scope determines -- a bare equation, or clauses D_i || x = c_i whose guards cover every case -- where it is read, and drop its binder, before the case split. On by default.
• bv-defelim-max-clauses, bv-defelim-max-atoms, bv-defelim-max-subset and bv-defelim-max-rounds: the caps of that elimination.
• bv-quantifier-free-decision: decide a closed bitvector formula whose binders are all of one kind without quantifiers. Off by default.
• bv-blasting-max-nodes: the BDD nodes one predicate blasting may build before it declines. 500000 by default, 0 = unlimited.
• bv-bitblast-max-width: the widest bitvector a question may hold to be decided on its bits. 16 by default. 0 leaves every question to the solver.
• bv-bitblast-max-nodes: the BDD budget, in nodes in use at once, of the decision on the bits of values of at most bv-bitblast-max-width bits. 1048576 by default. 0 leaves every question to the solver.
• bv-solve-timeout: the seconds a bitvector question with quantifiers may take, on its bits and, when it multiplies or divides two values that are not constants, in the solver. Past it the command that asks it answers UNKNOWN. 60 by default, 0 = no limit.
• bv-widening: the exact, widened bitvector arithmetic mode. Off by default.
• bv-max-width: cap on the width widening may compute at. 1024 by default. It is a hard ceiling that is never unlimited, so set bv-max-width 0 sets the default 1024 again.

In a session built without bv, set bv-blasting off is an error (Unknown option) and changes nothing.

Functions, predicates and input/output stream variables

As in other programming languages, you can define functions, predicates (both possibly using recurrence relations), types, but also input and output stream variables. The syntax of the commands is the following:

• definitions|defs: shows all the definitions of the current session. That includes the definitions of functions, predicates, types and the input/output stream variables.

• definitions|defs <number>: shows the definition of the given function or predicate.

• predicate_def: defines a predicate, supporting the usage of recurrence relations. See the Tau Language section Functions and predicates for more information.

• function_def: defines a function, supporting the usage of recurrence relations. See the Tau Language section Functions and predicates for more information.

• type_def: defines an abstract data type (an alias or a tuple type). See the Tau Language section Abstract data types for more information.

• <name> [: <type>] := in console | in file(<filename>): defines an input stream variable. The input variable can read values from the console or from a provided file. A value is written bare (3, #x01) or as a specification writes a constant ({ 3 }:qlt, { #x01 }:bv); the type after the braces must be the stream's type or its family.

• <name> [: <type>] := out console | out file(<filename>): defines an output stream variable. The output variable can write values to the console or into a file.

In both cases <name> is any stream name and <type> is tau, sbf or bv[n] (see Streams and Type system). If the type is omitted the stream is left untyped and its type is inferred on use. For example:

i1 : tau := in console
o1 : tau := out console
sensor : bv[8] := in file("samples.in")

Memory related commands

All the results are stored in the REPL memory. You can also store well-formed Tau formulas or Boolean functions for later reference. To do so, you can use the following syntax:

• tau|term: store a tau formula or a Boolean function in the REPL memory.

If you want to consult the REPL memory contents, you can use the following commands:

• history|hist: show all the previously stored Tau expressions.

• history|hist <repl_memory>: show the Tau expression at the specified REPL memory position.

In general, to retrieve a Tau expression from the REPL memory, you can use the following syntax for <repl_memory>:

• %: to retrieve the Tau expression stored at the latest position
• %<number>: to retrieve the Tau expression stored at position <number>
• %-<number>: to retrieve the Tau expression stored at the latest position minus <number>

Expression manipulation

You can substitute expressions into other expressions or instantiate variables in expressions. The syntax of the commands is the following:

• substitute|subst|s <repl_memory|tau|term> [<repl_memory|tau|term>/<repl_memory|tau|term>, ...]: substitutes a memory, well-formed formula or Boolean function by another one in the given expression (this one being a memory position, well-formed formula or Boolean function). Several comma separated match/replace pairs may be given in one command; all pairs are applied simultaneously in a single pass over the input, so every match is found against the original expression and no pair's replacement is ever re-matched by another pair (s x & y [x / y, y / x] swaps x and y). Repeating the same match pattern in two pairs is an error. The result must remain well-typed: a replacement whose type conflicts with the matched context (e.g. s x:sbf & y:sbf = 0 [x:sbf / z:bv[16]], or mismatched bitvector widths) is rejected at substitution time instead of storing an ill-typed expression. Untyped expressions carry the default type (tau) and an unannotated replacement adopts the matched context's type (s x:sbf & y:sbf = 0 [x:sbf / z] yields zy = 0 with z typed sbf). A pair whose match pattern does not occur in the input is reported with a warning instead of silently leaving the input unchanged. An input that cannot be type-inferred at all (e.g. bitvector arithmetic without width annotations) is matched as parsed, so s a + b = c [a / d] substitutes a even though the expression carries no type information. Several bracket groups may follow the input: each group is applied to the result of the previous one, while the pairs inside a group stay simultaneous. So s a | c [a / b] [b / d] chains — the b introduced by the first group is rewritten to d by the second — whereas s a | c [a / b, b / d] yields b | c. The same match pattern may appear in different groups (that is what chaining is for); repeating it inside one group is still an error.

• instantiate|inst|i <repl_memory|tau> [<var>/<repl_memory|term>]: instantiates a variable by a memory position, well-formed formula or Boolean function in the given well-formed or Boolean function expression.

• instantiate|inst|i <repl_memory|term> [<var>/<repl_memory|term>]: instantiates a variable by a memory position or Boolean function in the given expression.

instantiate accepts the same multiple forms as substitute: several comma separated var/value pairs in one bracket are applied simultaneously (i x & y [x / y, y / x] swaps x and y), and several bracket groups compose sequentially. The match side of every pair must be a variable, and the same type safety and no-match reporting apply.

Logical procedures

The Tau REPL also provides a set of logical procedures that allow you to check several aspects of the given specification/well-formed formulas/Boolean functions. The syntax of the commands is the following:

• valid <repl_memory|tau>: checks if the given specification is valid, that is, whether no trace violates it, with every input stream read as an output (see Satisfiability).

• sat <repl_memory|tau>: checks if the given specification is satisfiable.

• unsat <repl_memory|tau>: checks if the given specification is unsatisfiable.

sat, unsat and valid print T or F, or an UNKNOWN error when the formula cannot be decided.

• solve [<options>] <repl_memory|tau>: solves the given system of equations given by the well-formed formula, computing a single satisfying assignment for its free variables. The available options are:

  • --min|--minimum: computes a minimum solution of the system,
  • --max|--maximum: computes a maximum solution of the system,
  • --<type>: uses the given type (sbf, tau, ...) for the solution.

  With an option, put the formula in parentheses: solve --min (x = y). Without them, -- reads as two semantic negations of the formula, and solve reports an error.

  Every value in the assignment is a constant: solve x:bv[2] = y:bv[2] answers x := { 3 }:bv[2] and y := { 3 }:bv[2], where lgrs gives the reproductive solution x := x|y, y := x|y. An ordering system over qlt is solved as a whole, so related variables get distinct values (solve x:qlt < y:qlt gives x a smaller value than y), and its model is checked against every atom before it is printed. A qlt variable always gets one point (see the qlt section).

• lgrs [--<type>] <repl_memory|tau>: computes a least general reproductive solution (LGRS) for the given equation.

• normalize|n <repl_memory|rr|ref|tau|term>: normalizes the given expression. See the TABA book for details.

• qelim <repl_memory|tau>: eliminates the non-temporal quantifiers in the given expression.

• realizable <repl_memory|tau|rr>: checks whether a winning system strategy exists for every input sequence and prints T or F.

• unrealizable <repl_memory|tau|rr>: the complement of realizable.

Normal forms

Also, the Tau REPL includes several transformation procedures to standard forms. The syntax of the commands is as follows:

• dnf <repl_memory|tau|term>: computes the disjunctive normal form of the given expression.

• cnf <repl_memory|tau|term>: computes the conjunctive normal form of the given expression.

• nnf <repl_memory|tau|term>: computes the negation normal form of the given expression.

• mnf <repl_memory|tau|term>: computes the minterm normal form of the given expression.

• onf <var> <repl_memory|tau>: computes the order normal form of the given expression with respect to the given variable.

Specification execution

Finally, you can run a given Tau specification. The syntax for the commands is:

• run|r <repl_memory|tau>: runs the given Tau specification.

• run N steps <repl_memory|tau>: runs the specification for exactly N steps and keeps the session; run N steps continues the stored session for N more steps and a bare run continues it until it ends or needs input. A step that fails, for instance on an output file that cannot be written, ends the run and prints the error.

• stop: discards the stored run session.

• memory: prints the stored run session's current variable-to-value map.

• unrealizable_core <repl_memory|tau>: prints a subset-minimal set of the top-level conjuncts of a specification that is already unrealizable (always (A && B) counts as always A and always B), the REPL form of api::unsat_core; it prints realizable for a realizable specification.

• explain <repl_memory|tau>: says why a specification is unrealizable. It prints the unrealizable core, then the environment's counter-strategy against the core: the Moore machine ltlsynt finds for the negated core, over props it names with their atoms (p0 := i1[t]:bv[1] = 0). A core the data game or the safety pipeline decides has no counter-strategy to print. When ltlsynt decides the core but does not solve the negated game, it prints no counter-strategy: and why: a timeout, or an ltlsynt older than Spot 2.16, which lacks the --semantics=Moore that game runs.

• ltl <repl_memory|tau>: prints the full LTL(ABA) translation pipeline for a formula containing LTL operators (F, G, U, R, W, S, T). Shows the data atom extraction, propositional skeleton (with the temporal testers of S and T), the first ltlsynt round, its HOA strategy automaton and the ABA oracle feasibility checks of its edges, and how run executes the formula: the synthesized safety formula, or the strategy of the data game. It explains the formula realizable decides, with the same always part and warm-ups, and prints the verdict realizable gives. That verdict may come from the data game or from later refinement rounds; the trace says so when it differs from the first round's.

Web IDE

A full-featured browser-based IDE for composing, navigating, debugging, and running Tau programs. It is a Python local webserver that wraps the tau binary and exposes every REPL command through a modern editor UI.

Running the IDE

Quick start (one command)

The launcher script handles everything — builds the tau binary (if needed), creates a Python virtual environment, installs dependencies, and starts the IDE:

# Linux / macOS
./run-ide.sh

# Windows (PowerShell)
.\run-ide.ps1

Then open http://localhost:8080 in your browser.

Options:

Flag	Effect
--port 9090	Use a different port
--jobs 4	Parallel build jobs (default: half your cores)
--skip-build	Skip C++ build (IDE still works for editing, help, grammar, visualization, AI)
--help	Show all options

The IDE works for editing, syntax highlighting, help, grammar browsing, visualization, and AI assistance without the tau binary. Execution features (Run, Eval, REPL) activate once the binary is built.

What the launcher does

1. Locates Python 3.10+ — tries python3, then python
2. Builds the tau binary (unless --skip-build or already built):
   • Initializes git submodules
   • Installs build dependencies on Ubuntu (scripts/setup-ubuntu-ci-deps.sh)
   • Vendors the ankerl/unordered_dense header (avoids network issues)
   • Runs release.sh → produces build-Release/tau
3. Creates a Python venv at .venv/ (skipped if it already exists)
4. Installs Python deps from ide/requirements.txt
5. Starts the IDE server on the specified port

Build variants

If you prefer to build manually:

Script	Binary location	Use case
./release.sh	build-Release/tau	Normal use (fastest)
./debug.sh	build-Debug/tau	Debugging with symbols
./relwithdebinfo.sh	build-RelWithDebInfo/tau	Profiling

The IDE server automatically searches all of these directories for the binary.

Manual setup (if you prefer not to use the launcher)

cd tau-ltl
python3 -m venv .venv
source .venv/bin/activate      # ⬅ MUST activate before pip install
pip install -r ide/requirements.txt
python -m uvicorn ide.server:app --host 0.0.0.0 --port 8080

Troubleshooting

Problem	Fix
unordered_dense clone fails during build	The launcher vendors this automatically; if building manually, run: mkdir -p external/parser/external/ankerl && curl -sL https://raw.githubusercontent.com/martinus/unordered_dense/v4.4.0/include/ankerl/unordered_dense.h -o external/parser/external/ankerl/unordered_dense.h
externally-managed-environment error	You forgot to activate the venv: run source .venv/bin/activate first
pip install fails with permission error	Use the launcher script or create a venv manually (see above)
python3: command not found	Try python instead of python3; ensure Python 3.10+ is installed
No module named 'uvicorn'	Make sure you activated the venv (source .venv/bin/activate) before running
Port 8080 already in use	./run-ide.sh --port 9090

Custom binary location

python -m ide.server --port 8080 --tau-binary /path/to/tau

IDE Features

Area	What you get
Compose	Syntax highlighting (grammar-driven), autocomplete from grammar tokens, 8 starter templates, file tabs
Navigate	Sidebar explorer with test/example files, symbol search, command palette (Ctrl+Shift+P)
Debug	AST viewer panel, whatis type inspection, variable hover tooltips
Run	Execute specs (Shift+Enter), evaluate formulas (Ctrl+Enter), quick actions (SAT / valid / normalize / DNF / CNF / …)
Help	10 searchable help topics, grammar reference derived from parser/tau.tgf, keyboard shortcut reference
Visualize	Timeline diagrams for temporal operators, AST tree view, color-coded operator legend
AI	LLM-powered (DeepSeek, OpenAI or Anthropic) NL ↔ Tau translation, context-aware code assistance, code explanations

Keyboard shortcuts

Shortcut	Action
Ctrl+Enter	Evaluate selection/line
Shift+Enter	Run specification
Ctrl+Space	Autocomplete
Ctrl+/	Toggle comment
Ctrl+Shift+P	Command palette
Ctrl+Shift+V	Visualize formula
Ctrl+N	New file
Ctrl+O	Open file
Ctrl+S	Save file
Ctrl+G	Go to line
F1	Toggle help panel
Escape	Close palette/panels

Fragment switching

Use the dropdown in the top bar or the REPL command to switch between grammar fragments:

fragment ltl         # default — standard LTL operators
fragment ctl_star    # enable CTL* path quantifiers A, E and semantic negation -

Grammar Integration

The IDE parses parser/tau.tgf at server startup and derives:

• Token categories for syntax highlighting (keywords, temporal ops, commands, types, operators — all from the grammar)
• Autocomplete entries with documentation for every command, keyword, and operator
• Grammar reference panel in the help sidebar showing every wff, bf, and CLI production rule with syntax, label, and description
• Hover tooltips — hover a highlighted token in the editor to see its grammar rule and description

If the grammar file changes, restart the server to pick up the new definitions. The highlighter and autocomplete update automatically.

Temporal Formula Visualization

Click the Viz button or press Ctrl+Shift+V to visualize the current formula (or selected text). The visualization panel shows:

• Timeline diagram — SVG rendering showing how temporal operators behave over time steps. G spans all steps, F highlights eventual satisfaction, U shows the handoff point, etc.
• AST tree — interactive parse tree of the formula with color-coded nodes for each operator type
• Operator legend — all temporal operators with their semantics and colors

This is a presentation/teaching aid — useful for understanding what a formula means over time.

AI Assistant

The IDE includes an AI assistant for working with Tau code, answered by one of three providers: deepseek and openai (chat completions) and anthropic (the Messages API, through the anthropic Python package that ide/requirements.txt installs). Click the AI button in the top bar or use the AI tab in the bottom panel.

Setup: Pick a model in the selector; the model names its provider. Click the gear icon to enter the API key of that provider. The IDE keeps one key per provider in browser localStorage only — a key is never written to disk and goes with a request to the IDE server, which passes it to that provider's API and nowhere else.

Server-side defaults: a request names its provider, model and key. For what a request leaves out, the server reads TAU_LLM_PROVIDER (default deepseek), TAU_LLM_MODEL (default: deepseek-reasoner for deepseek, claude-opus-5-5 for anthropic, none for openai, which must be given a model) and the provider's own DEEPSEEK_API_KEY, OPENAI_API_KEY or ANTHROPIC_API_KEY. TAU_LLM_MODEL and TAU_LLM_API_KEY belong to the provider TAU_LLM_PROVIDER names: they apply to a request for that provider only, and not at all when the variable is unset, so a key never reaches another provider. The selector opens on the server's default model. python -m ide.server --llm-provider anthropic --llm-model claude-opus-5-5 gives the first two on the command line. With a key in the server's environment the browser needs none, and anyone who can reach the server's port can spend it: keep the default --host 127.0.0.1 in that case.

Three modes:

1. Ask (context-aware) — "How do I add a liveness property to this?" The assistant sees your entire editor content and provides code snippets that integrate with your existing program.

2. Generate from NL — Describe what you want in plain English and the assistant generates complete Tau code. The generation prompt includes the full grammar, language semantics, 15 worked examples, and common-mistake avoidance rules.

3. Explain code — Select code (or use the full editor content) and get a structured natural-language explanation: one-sentence summary, operator-by- operator breakdown, I/O behavior, required fragment.

Models: Choose between DeepSeek R1 (reasoning, slower, more accurate), DeepSeek V3 (fast chat) and Claude Opus 5.5 (Anthropic).

Generated code can be inserted at cursor or replace the editor content with one click.

Developer infrastructure for ω-categorical synthesis

The following headers (all standalone, header-only, test-covered) implement tau-lang's LTL(ABA) synthesis pipeline over ω-categorical theories.

Core synthesis algorithms

Header	Status	Purpose
src/algorithm_b_skeleton.h	Default for input-bearing qlt formulas over T₃	Algorithm B: build_algorithm_b_skeleton(T1_size, T2_size, K, feasible_set_b, t2_pos_m, phi_star). Adds ⌈log₂|T₂|⌉ input P-bits encoding T₂ = (pos_m, pos_x, rel_mx). Assembles (Φ_I ∧ Ψ_I) → (Φ_O^R ∧ Φ_δ ∧ φ*). Sound for input-variable formulas. Activated by default or TAU_LTL_ALG=B.
src/algorithm_a_skeleton.h	Available for pure-output formulas	Algorithm A: build_algorithm_a_skeleton(T1_size, K, feasible_set, phi_star). Uses ⌈log₂|T₁|⌉ output R-bits for the memory type, no input propositions. Faster for pure-output formulas; bypassed when input variables appear.
src/algorithm_d_game.h	Available for output-only formulas (TAU_LTL_ALG=D)	Algorithm D: direct parity-game construction. HOA guard evaluator (eval_guard); synthesis game parser (parse_synth_game_hoa); build_product_game (synthesis game × T₁, with T₃ feasibility pruning); zielonka_win_player1 (recursive attractor + subgame solver, odd priority = system wins).
Algorithm C (deleted)	Not implemented	Oracle-assisted abstract game with A_{ρ,J} oracle propositions. Deleted 2026-08-25 (D2): Algorithm D provides the T1-product game without the formula blow-up, and C's oracle propositions had no executable strategy; the design write-up is kept outside this repository.

Type enumeration (ω-categorical theories)

Header	Purpose
src/omcat_types.h	rational type (128-bit cross-multiplied comparison). qlt_type1/qlt_type2/qlt_type3 structs for 1-/2-/3-types of (ℚ,<,Σ). enumerate_qlt_T1 (2k+1 types from k constants), enumerate_qlt_T2 (T₂ = (pos_m, pos_x, rel_mx) with forced-relation filtering), enumerate_qlt_T3 (T₃ with transitivity filter). realize() rational witnesses (none when the witness does not fit a long long rational).
src/boolean_algebras/qlt/omcat_constants.h	parse_rat_literal for rational/decimal strings (at most 18 fractional digits); collect_qlt_constants(fm) harvesting named constants from a formula.

Supporting infrastructure

Header	Purpose
src/parse_error_hint.h	classify_parse_error(formula) for actionable parse error messages.
src/tau_lang_api.h	Documentation header for the library entry points (is_tau_formula_sat, get_nso_rr, run); there is no tau_lang_is_realizable symbol.

Algorithm A/B soundness rule

Algorithm A has no input propositions, so it is sound only when the formula has no input variables. If a qlt formula contains input variables, the default routing uses Algorithm B, and TAU_LTL_ALG=A sends it to the default abstraction. Algorithm B adds P-bits for the current T₂ type, making the synthesized strategy type-aware.

The C++ API and language bindings

Besides the executable and the REPL, the framework is usable as a library.

The public C++ API is src/api.h. All operations are exposed as static methods on api<node>, and cover parsing (get_spec, get_formula, get_term, get_definition, ...), printing, substitution and instantiation, the logical procedures, the normal forms and the execution of specifications (get_interpreter, get_inputs_for_step, step). unsat_core returns a subset-minimal set of a specification's top-level conjuncts that is already unrealizable (or unsatisfiable), and reset returns the process to a fresh state, freeing every tree node no htref holds. Global switches such as set_charvar, set_preprocessing, set_ba_component_factoring, set_indenting, set_highlighting, set_json and set_severity mirror the command line options, and every runtime limit has a setter of the same name as its option (set_block_max_splits, set_max_fixpoint_steps, set_ba_decision_pins, ...) and a getter beside it (get_max_fixpoint_steps(), ...) that reads back the value in force, with a cap read as 0 when unlimited. tau_init() declares every option. A program then reads the environment with idni::options().load_env("TAU_"). The tau executable, a compiled program and the bindings do this at start. count_limits() lists every numeric limit as a name, a setter and a getter, which is what the bindings enumerate. Every option, of core and of each Boolean algebra, is in the options repository idni::options() under the name it has on the command line, without the dashes in front: set_text("bv-widening", "on") or set_text("bv-defelim-max-atoms", "5") writes it, get_text(name) reads it back, both answer an error for a name the build does not declare, and names() lists the names the build has. An empty text clears a text option to its default, and nlang-api-key reads set or unset.

The underlying tree representation is documented in docs/tau_tree.md, and docs/adding_base_bas.md describes how to add a new base Boolean algebra. For development conventions, standalone runners and testing notes see DEVELOPMENT.md.

Python bindings are provided via nanobind in bindings/python and built with ./dev binding python. They expose the interpreter part of the API together with a set of stream implementations (console, file, and in-memory vector streams) so that inputs and outputs can be driven from Python. The decision procedures sat, unsat, valid, realizable (alias is_realizable) and unrealizable take a full specification and return a tau.result whose value is the verdict, or None when the spec does not parse or gets no verdict. unsat_core(spec, realizability=True) returns a subset-minimal list of the top-level conjuncts (always (A && B) counts as always A and always B) that is already unrealizable, or unsatisfiable with realizability=False. reset() returns the engine to a fresh state, as the REPL reset command does. See docs/tau_result.md for the result type.

import tau   # the built module lives in <build dir>/bindings/python/nanobind

i_stream = tau.vector_input_stream(["T", "F", "T"])
o_stream = tau.vector_output_stream()

opts = tau.interpreter_options()
opts.input_remaps["i"] = i_stream
opts.output_remaps["o"] = o_stream

interpreter = tau.get_interpreter("o[t] = i[t].", opts)
for _ in range(3):
    tau.step(interpreter)

print(o_stream.get_values())   # ['T', 'F', 'T']

The module also carries the api's runtime budgets and engine switches under the same names (tau.set_max_fixpoint_steps(1000), tau.set_tref_budget(n), tau.set_ltl_timeout_sec(120), tau.set_preprocessing(False), ...), a getter for each budget (tau.get_max_fixpoint_steps(), tau.get_ltl_timeout_sec(), tau.get_gc_growth_factor(), ...) and every option by name (tau.option_names(), tau.set_option("bv-widening", "on"), tau.set_option("nlang-provider", "anthropic"), tau.get_option(name), each returning a tau.result that carries the text the option reads).

Further examples are in tests/bindings/python.

The ctypes binding (bindings/python/ctypes, built with -DTAU_BUILD_BINDING_PYTHON_CTYPE=ON) reaches the same budgets by name through its C ABI (tau_lang_set_limit, tau_lang_get_limit, tau_lang_limit_names, and the tau_lang_set_* / tau_lang_get_* pairs of the gc growth factor, the ltlsynt timeout and the synthesis algorithm). Its tau_lang.py spells them like the nanobind module (tau_lang.set_max_fixpoint_steps(1000), tau_lang.get_limit("ltl_hoa_max_states")). It has no access to the options the algebras declare.

The JavaScript module of the WebAssembly build (bindings/js) carries the same budgets and switches under the same snake_case names (tau.set_max_fixpoint_steps(1000), tau.set_tref_budget(n), tau.set_preprocessing(false), tau.set_max_constant_size(n), tau.set_bf_dependence_max_nodes(n), tau.tref_count(), ...), reads each budget back with the getter of the same name (tau.get_max_constant_size(), tau.get_max_fixpoint_steps(), tau.get_gc_growth_factor(), ...), and carries every option by name (tau.option_names(), tau.set_option("qlt-t3-cap", "5"), tau.set_option("qlt-cells-budget", "0"), tau.get_option(name), which return the text the option reads, or null with the reason in tau.get_last_error() for an unknown name or a bad text). The WebAssembly build cannot run ltlsynt, so the options of that route and of the data game played on its game (set_ltl_timeout_sec, set_ltl_algorithm, set_ltl_hoa_max_states, set_ltl_ctl_star_tableau_max_states, set_ltl_data_fixpoint_rounds, set_ltl_self_check_steps, set_ltl_strategy_max_states, set_ltl_compositional, set_ltl_guard_max_cubes, set_ltl_window_max_paths, set_ltl_closed_regions_timeout, set_ltl_data_game_max_nodes, set_ltl_data_game_max_memo, set_ltl_data_game_max_combinations, set_ltl_max_observations, set_ltl_mealy_max_states, set_ltl_mealy_max_edges, set_compile_max_table_edges and set_compile_build_timeout) have no counterpart there. bindings/js/tests/budgets.js shows each of them in use.

On Linux arm64 the binding builds and tests both natively and by cross compilation with ./dev preset release-arm64-all, which runs its tests under qemu-aarch64. The tau_wheel target packs the same module into a wheel for every package platform: Linux x86_64 and arm64, macOS arm64, and Windows x86_64 (MSVC).

The Theory behind the Tau Language

• GS Paper Guarded Successor: A Novel Temporal Logic by Ohad Asor
• TABA book Theories and Applications of Boolean Algebras by Ohad Asor (In works).
• YouTube lecture series on Atomless Boolean Algebra by Ohad Asor.

Known issues

This is a short list of known issues that will be fixed in a subsequent release:

• Simplification and performance:
  • Normalization can grow exponentially on long chains of ?: with exclusive guards and on flat || conditions with many terms (#203). The answers stay correct; only time and memory grow.
  • Equalities between variables are propagated only through plain conjunctions and disjunctions, not under quantifiers, temporal operators, ->, <->, ^^ or ?:, so such formulas can grow before they simplify.
• Several searches are bounded rather than complete. The satisfiability fixpoint search and the eventual-flag search stop after 500 steps by default and report an error instead of an answer (--max-fixpoint-steps / set max-fixpoint-steps, --max-flag-search-steps / set max-flag-search-steps; 0 = unlimited). Such a bound is a limit on the search, not a proof about the input. The fixpoint enumeration of recurrence relations is unbounded by default: a recurrence whose steps keep growing does not terminate unless a cap is set with --max-enum-steps / set max-enum-steps.
• Fixpoint calculation is not supported for recurrence relations with more than one offset index.
• The anf (algebraic normal form) and pnf (prenex normal form) commands are not implemented and are currently not reachable from the REPL grammar; the library function api::pnf returns an unsupported_operation error.
• REPL: a statement the parser reads as incomplete gives no error and waits for more input, so the next line is appended to it (#16); for example test(n) := (n=0) -> 1 followed by = n becomes test(n) := (n = 0 -> 1 = n).
• LTL-specific:
  • Write the time index on every stream: G(o1[t]:sbf = i1[t]:sbf). Without it o1 and i1 are ordinary variables, not streams: G(o1:sbf = i1:sbf) is accepted, but run refuses it ("the specification contains free variables").
  • An atom at a fixed step, such as o1[0], is not supported under a temporal operator (F (o1[0] = 1)) or in the same conjunct as [t] atoms ((o1[0] = 1) U (o2[t] = 1)); realizability is then reported as UNKNOWN.
• tau gen / tau compile do not cover every specification run executes. They refuse, among others, a data-game strategy that reads values before step 0, outputs that need witness solving at run time, pointwise revision with data-atom outputs and interval comparison atoms. Such specifications still run in the interpreter.
• The WebAssembly build has no bv, hsb or nlang type and cannot run ltlsynt.

Future work

• Performance: faster normalization and satisfiability checking of Tau specifications, including the normalization of Boolean functions and of Boolean equations, and complete procedures where the fixpoint enumeration of recurrence relations and the satisfiability fixpoint search are bounded today.
• General Boolean functions: a Boolean algebra of Boolean functions over an arbitrary base Boolean algebra; today only simple Boolean functions (sbf, functions over {0,1}) are supported.
• Term algebras: support for term algebras (theory of trees) as a concrete domain — decidable ω-categorical theories admitting quantifier elimination.
• qlt and qint: decide the cases qlt leaves open today — constants with named endpoints, order atoms against a constant that is not a single point, and values beyond 64-bit rationals, which answer UNKNOWN — and extend the reactive-synthesis oracle over qint.
• Algorithm D with inputs: Algorithm D solves the qlt product game as a parity game (Zielonka's algorithm over the priorities of the acceptance ltlsynt prints) for output-only formulas; under ltl-alg D a formula with inputs goes to the default abstraction. Extending D to them (the T₂ dimension in the environment states) is open.
• Type encoding for other Boolean algebras: only qlt uses the T₁/T₂ type enumeration of Algorithms B and D. Extending it to sbf, bv and tau needs a BDD-based encoding: the type of an element relative to the formula's named constants is the atom of the subalgebra generated by those constants that the element falls in — equivalently, the element's BDD restricted to the constant variables.
• CTL*: decide valid for formulas with A, E or -, give E an exact encoding when its path formula contains S or T, and encode the placements of A/E that are refused today.
• Boolean-function quantifiers in LTL synthesis: fall and fex inside temporal formulas, not only in always (safety) formulas.
• REPL: interactive work on a selected subformula — convert it to a normal form, eliminate a selected quantifier, substitute a variable or function in it.
• Pointwise revision: more refined ways of building the revised specification.
• Error reporting: report, instead of only logging, the errors that are dropped today, such as malformed tuple-stream input.
• nlang in WebAssembly: an HTTP transport for the nlang oracle in the WebAssembly build, which leaves nlang out because curl has no wasm port.
• Compile times: extend the explicit template instantiations of src/instantiate_pack.cpp and src/instantiate_artifact_pack.cpp to more of the heavy pipeline templates.

Submitting issues

Please submit issues at the following link: Tau Language issues.

License

Tau Language is licensed under the following terms: Tau Language License

The packages also ship libraries and tools of other projects, each under its own license. Every package carries their license texts in a licenses folder: share/doc/tau/licenses in the Linux and Windows packages, licenses beside tau in the macOS one, licenses in the SDK, tau/licenses in the Python wheel and licenses in the JavaScript package. The source of the GPL Spot tools and of the LGPL GMP library is published with each release; licenses/spot/SOURCE.md and licenses/gmp/SOURCE.md say where.

Authors

The Tau Language has been developed by the following authors:

• Ohad Asor
• David Castro Esteban
• Tomáš Klapka
• Lucca Tiemens

Contributors

Thank you to everyone who has improved Tau through a pull request or through code shared in an issue:

• andrei-idni
• David Andel
• Jme-Tau
• LEARNTAU
• m4nki
• Mikolaj Konarski
• pt7k
• Taumorrow
• TheDarkLightX