BSD Ports

devel/tla+ 1.7.4 FreeBSD

TLC is a model checker for specifications written in TLA+

System
FreeBSD
Repository
FreeBSD ports
Maintainer
[email protected]
Port added
Last update
Commit
50fc7f3612
License
MIT
Categories
devel, java
Package size
2105.5 KiB, 2223.1 KiB installed

Description

TLA+ is a language for modeling software above the code level and hardware above the circuit level. The tool most commonly used by engineers is the TLC model checker, but there is also a proof checker. TLA+ is based on mathematics and does not resemble any programming language. Most engineers will find PlusCal to be the easiest way to start using TLA+.

This port installs the TLA+ command-line tools packaged as tla2tools.jar, with wrapper scripts for each:

tla-tlc - the TLC model checker, which explores a specification's state space to check safety and liveness properties tla-sany - the SANY syntactic and semantic analyzer (parser) tla-tla2sany - export a parsed TLA+ module as an XML parse tree tla-pcal - the PlusCal-to-TLA+ translator tla-tla2tex - the LaTeX pretty printer for TLA+ specifications

Install

Binary package:

pkg install tla+

From the ports tree:

cd /usr/ports/devel/tla+/ && make install clean

To depend on this port in another port's Makefile:

RUN_DEPENDS=	tla+>0:devel/tla+

Packages

The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.

Repositoryaarch64amd64armv6armv7i386
FreeBSD:14:latest1.7.41.7.4--1.7.4
FreeBSD:14:quarterly1.7.41.7.4n/a-1.7.4
FreeBSD:15:latest1.7.41.7.4n/a--
FreeBSD:15:quarterly1.7.41.7.4n/an/an/a
FreeBSD:16:latest1.7.41.7.4n/an/an/a
FreeBSD:16:quarterlyn/an/an/an/an/a

Dependencies

The Makefile names none itself; they come from USES and USE_*.

The full lists below include those, and their dependencies in turn.

Build dependencies 55
Run dependencies 41

No port depends on this one.

Configuration

No options to configure.

USES
java:ant,run
Service scripts
none

Files

distinfo 1
FileSizeSHA256
tlaplus-tlaplus-v1.7.4_GH0.tar.gz7.2966127e+07eb4e54b6c8dc4945cbd697dbfe55819b6fc3f13fe9561afd7d6523c18ea4c350

Commit history 1

DateCommitCreditsLog message
50fc7f3612 Pat Maddox devel/tla+: new port
TLA+ is a language for modeling software above the code level and hardware above the circuit level. The tool most commonly used by engineers is the TLC model checker, but there is also a proof checker. TLA+ is based on mathematics and does not resemble any programming language. Most engineers will find PlusCal to be the easiest way to start using TLA+. The graphical TLA Toolbox IDE is not included. It is a separate Eclipse RCP application that would be better as its own port. WWW: https://www.tlapl.us Approved by: dch (mentor) Reviewed by: arrowd Pull Request: https://github.com/freebsd/freebsd-ports/pull/554