math/spot 2.16
Library for omega automata manipulation and model checking
- Repository
- FreeBSD ports
- Maintainer
- [email protected]
- Last update
- Commit
6464c4ca26- License
- GPLv3
- Categories
- math
- Package size
- 3179.6 KiB, 12036.1 KiB installed
Description
Spot is a library for LTL, omega-automata manipulation and model checking.
It has the following notable features: * Support for LTL (several syntaxes supported) and a subset of the linear fragment of PSL. * Support for omega-automata with arbitrary acceptance condition. * Support for transition-based acceptance (state-based acceptance is supported by a reduction to transition-based acceptance). * The automaton parser can read a stream of automata written in any of four syntaxes (HOA, never claims, LBTT, DSTAR). * Several algorithms for formula manipulation including: simplifying formulas, testing implication or equivalence, testing stutter-invariance, removing some operators by rewriting, translation to automata, testing membership to the temporal hierarchy of Manna & Pnueli... * Several algorithms for automata manipulation including: product, emptiness checks, simulation-based reductions, minimization of weak-DBA, removal of useless SCCs, acceptance-condition transformations, determinization, SAT-based minimization of deterministic automata, etc. * In addition to the C++ interface, most of its algorithms are usable via command-line tools, and via Python bindings. * One command-line tool, called ltlcross, is a rewrite of LBTT, but with support for PSL and automata with arbitrary acceptance conditions.
Install
As a binary package — by origin, or by package name:
pkg install math/spot
pkg install spotFrom the ports tree:
cd /usr/ports/math/spot/ && make install cleanTo depend on this port in another port's Makefile:
RUN_DEPENDS= spot>0:math/spot
LIB_DEPENDS= libbddx.so:math/spotPackages
The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.
| Repository | aarch64 | amd64 | armv6 | armv7 | i386 |
|---|---|---|---|---|---|
| FreeBSD:14:latest | 2.16 | 2.16 | 2.11.3 | 2.12.1 | 2.16 |
| FreeBSD:14:quarterly | 2.16 | 2.16 | n/a | 2.12.1 | 2.16 |
| FreeBSD:15:latest | 2.16 | 2.16 | n/a | 2.12.1 | 2.12.1 |
| FreeBSD:15:quarterly | 2.16 | 2.16 | n/a | n/a | n/a |
| FreeBSD:16:latest | 2.16 | 2.16 | n/a | n/a | n/a |
| FreeBSD:16:quarterly | n/a | n/a | n/a | n/a | n/a |
Dependencies
As this port's Makefile names them.
Test 4
${PYTHON_PKGNAMEPREFIX}numpy>=1.16: math/py-numpy${PYTHON_PKGNAMEPREFIX}pandas>0: math/py-pandasgawk: lang/gawkgcut: sysutils/coreutils
The full lists below include those, and their dependencies in turn.
All build dependencies 3
Required by 1
Configuration
Options name: math_spot
| Option | Default | Description |
|---|---|---|
| DOCS | off | Build and/or install documentation |
- USES
- charsetfix compiler:c++17-lang gmake libtool python:test
- Service scripts
- none
Files
Manual pages 20
- autcross(1)
- autdo(1)
- autfilt(1)
- autwords(1)
- dstar2tgba(1)
- genaut(1)
- genltl(1)
- ltl2tgba(1)
- ltlcross(1)
- ltldo(1)
- ltlf2dfa(1)
- ltlfilt(1)
- ltlfsynt(1)
- ltlgrind(1)
- ltlmix(1)
- ltlsynt(1)
- randaut(1)
- randltl(1)
- spot(7)
- spot-x(7)
pkg-plist 242
- bin/autcross
- bin/autdo
- bin/autfilt
- bin/autwords
- bin/dstar2tgba
- bin/genaut
- bin/genltl
- bin/ltl2tgba
- bin/ltlcross
- bin/ltldo
- bin/ltlf2dfa
- bin/ltlfilt
- bin/ltlfsynt
- bin/ltlgrind
- bin/ltlmix
- bin/ltlsynt
- bin/randaut
- bin/randltl
- include/bddx.h
- include/bvecx.h
- include/fddx.h
- include/spot/bricks/brick-assert
- include/spot/bricks/brick-bitlevel
- include/spot/bricks/brick-hash
- include/spot/bricks/brick-hashset
- include/spot/bricks/brick-shmem
- include/spot/bricks/brick-types
- include/spot/gen/automata.hh
- include/spot/gen/formulas.hh
- include/spot/graph/adjlist.hh
- include/spot/graph/graph.hh
- include/spot/graph/ngraph.hh
- include/spot/kripke/fairkripke.hh
- include/spot/kripke/fwd.hh
- include/spot/kripke/kripke.hh
- include/spot/kripke/kripkegraph.hh
- include/spot/ltsmin/ltsmin.hh
- include/spot/ltsmin/spins_interface.hh
- include/spot/ltsmin/spins_kripke.hh
- include/spot/ltsmin/spins_kripke.hxx
- include/spot/mc/bloemen.hh
- include/spot/mc/bloemen_ec.hh
- include/spot/mc/cndfs.hh
- include/spot/mc/deadlock.hh
- include/spot/mc/intersect.hh
- include/spot/mc/lpar13.hh
- include/spot/mc/mc.hh
- include/spot/mc/mc_instanciator.hh
- include/spot/mc/unionfind.hh
- include/spot/mc/utils.hh
- include/spot/misc/_config.h
- include/spot/misc/bareword.hh
- include/spot/misc/bddlt.hh
- include/spot/misc/bitset.hh
- include/spot/misc/bitvect.hh
- include/spot/misc/casts.hh
- include/spot/misc/clz.hh
- include/spot/misc/common.hh
- include/spot/misc/escape.hh
- include/spot/misc/fixpool.hh
- include/spot/misc/formater.hh
- include/spot/misc/hash.hh
- include/spot/misc/hashfunc.hh
- include/spot/misc/intvcmp2.hh
- include/spot/misc/intvcomp.hh
- include/spot/misc/location.hh
- include/spot/misc/ltstr.hh
- include/spot/misc/memusage.hh
- include/spot/misc/minato.hh
- include/spot/misc/mspool.hh
- include/spot/misc/optionmap.hh
- include/spot/misc/permute.hh
- include/spot/misc/position.hh
- include/spot/misc/random.hh
- include/spot/misc/satsolver.hh
- include/spot/misc/timer.hh
- include/spot/misc/tmpfile.hh
- include/spot/misc/trival.hh
- include/spot/misc/version.hh
- include/spot/parseaut/public.hh
- include/spot/tl/apcollect.hh
- include/spot/tl/contain.hh
- include/spot/tl/declenv.hh
- include/spot/tl/defaultenv.hh
- include/spot/tl/delta2.hh
- include/spot/tl/distribute.hh
- include/spot/tl/dot.hh
- include/spot/tl/environment.hh
- include/spot/tl/exclusive.hh
- include/spot/tl/formula.hh
- include/spot/tl/hierarchy.hh
- include/spot/tl/length.hh
- include/spot/tl/ltlf.hh
- include/spot/tl/mutation.hh
- include/spot/tl/nenoform.hh
- include/spot/tl/parse.hh
- include/spot/tl/print.hh
- include/spot/tl/randomltl.hh
- include/spot/tl/relabel.hh
- include/spot/tl/remove_x.hh
The first 100 are listed.
distinfo 1
| File | Size | SHA256 |
|---|---|---|
| spot-2.16.tar.gz | 9.516931e+06 | 688463cb2fa393c51d9cf938fb01a716b91e4c8122aeb52fd116a3bbfddab869 |
Master sites 1
- http://www.lrde.epita.fr/dload/spot/