sci-mathematics/atelier-b::eventb-rossi
- Ebuilds: 1, Testing: 24.04.2 Description:
Atelier B Community Edition is an IDE by ClearSy for the B
method: type checking, proof obligation generation, automatic
and interactive provers, and code generation from B models.
Homepage:https://www.atelierb.eu/ License: Atelier-B-Community
sci-mathematics/prob-bin::eventb-rossi
- Ebuilds: 1, Testing: 1.15.1 Description:
ProB is an animator, constraint solver and model checker for the
B method. It supports classical B, Event-B, CSP-M, TLA+ and Z,
and allows the animation and automated/guided model checking of
specifications, including invariant and deadlock checking. This
package installs the prebuilt Tcl/Tk graphical interface (prob)
and the command-line tool (probcli).
Homepage:https://prob.hhu.de/ License: EPL-1.0
sci-mathematics/prob2-ui::eventb-rossi
- Ebuilds: 1, Testing: 1.3.1 Description:
ProB2-UI is a modern JavaFX-based user interface for the ProB
animator, constraint solver and model checker. It supports the
B method, Event-B, CSP-M, TLA+ and Z, offering interactive
animation, model checking, LTL/CTL verification, trace
recording and replay, and visualisation.
Homepage:https://prob.hhu.de/ License: EPL-2.0
sci-mathematics/rodin::eventb-rossi
- Ebuilds: 2, Testing: 3.10.0 Description:
The Rodin Platform is an Eclipse-based IDE for Event-B that
provides effective support for refinement and mathematical
proof. Event-B is a formal method for system-level modelling
and analysis.
Homepage:https://www.event-b.org/ License: EPL-1.0 EPL-2.0
sci-mathematics/rodin-headless::eventb-rossi
- Ebuilds: 1, Testing: 4.0 Description:
rodin-headless drives the Rodin Platform from the command line to build,
model-check, and prove Event-B models without a graphical session. It
takes .zip archives of Event-B projects, runs a full Rodin workspace
build headlessly, and writes the static-checked artifacts back into the
archives. Beyond plain builds it can model-check and validate models with
ProB and discharge proof obligations with the Rodin auto-provers. The
Rodin and ProB runtimes are downloaded on first use by the bundled
rodin-headless-install command rather than shipped with this package.
Homepage:https://github.com/eventb-rossi/rodin-headless License: MIT
sci-mathematics/rossi::eventb-rossi
- Ebuilds: 1, Testing: 0.1.4 Description:
Rossi is a Rust toolchain for Event-B providing a parser, a static
checker, a command-line interface, and a language server. It validates
Event-B models, converts between Event-B text and Rodin archives,
reformats models, and powers editor integration over the Language
Server Protocol.
Homepage:https://github.com/eventb-rossi/rossi License: || ( Apache-2.0 MIT )
Apache-2.0 Apache-2.0-with-LLVM-exceptions MIT Unicode-3.0 ZLIB
BZIP2
|| ( CC0-1.0 MIT-0 )
sci-mathematics/tlc4b::eventb-rossi
- Ebuilds: 1, Testing: 1.2.3 Description:
TLC4B model-checks classical B specifications by translating
them to TLA+ and running the TLC model checker: invariant and
assertion checking, deadlock detection, and counter-example
traces mapped back to B.
Homepage:https://github.com/hhu-stups/tlc4b License: EPL-1.0