This module manages the various choice points and enumerators of ProB, by maintaining the kernel Waitflags store.

chr_integer_inequality

Provide interface to CHR integer reasoning.

Provide interface to CLP(FD), with Prolog fallback in case of errors or when CLP(FD) turned off.

This module provides a dif which works with reified equality.

This module provides operations for the basic datatypes of ProB (equal, not_equal, enumeration).

This module provides more advanced operations for the basic datatypes of ProB (mainly for relations, functions, sequences).

Utilities to delay calls until sufficiently instantiated.

This module provides utilities for term variables for B expressions and values.

This module provides AVL-tree utilities used by the kernel.

custom_explicit_sets

This module provides customised operations for the custom explicit set representations of ProB (closures, avl_sets and global_sets).

This module provides various utility functions to analyse ProB closures.

This module contains predicates that operate on the record type.

This module takes care of storing B values in an environment and normalising values.

This module provides memoization features (for closure expansion, closure1,...).

This module translates AST constructs to calls in the ProB kernel.

This module takes care of enumerating B variables.

This module provides (external) functions to manipulate B reals and floats.

This module provides term ordering utilities.

This module provides reified equality and negation for pred_true/pred_false.

This module provides (external) functions to manipulate B strings.

This module provides a reified interpreter for certain predicates.

This module provides reified equality and membership predicates.

kernel_non_empty_attr

This module provides operations for non-emptyness of sets, storing them as attributes.

Basic checks for SET elements (equality, ...); maps to CLP(FD).

This module is responsible for caching constants and operations on disk

This module contains arithmetic that also supports the symbol inf.

b_interpreter_components

This module can be used to split a predicate into components and solving each component individually (with tracing feedback).

This module compiles set comprehensions into closures; making them independent of the state of the B machine.

This module detects information about variables by using frozen.

b_interpreter_eventb

This is an Event-B specific part of the interpreter. It contains the interpreter rules for events (as opposed to operations in classical B.

Provide interface to CLP(FD) table constraint.

This module provides a way to call the CLPFD clpfd_inlist and clpfd:element predicates for lists of FD values.

kernel_cardinality_attr

This module provides operations for cardinality of sets, storing them as attributes.

This module provides the basic interpreter for expressions, predicates and substitutions.

This module has rules about when and how to propagate in the ProB kernel.

This module provides operations for lists of B objects.

This module provides support for deferred/enumerated set elements in B.

static_symmetry_reduction

This module provides support for symmetry reduction on deferred sets.

Provide interface to CHR set reasoning.

This module contains functionality to store basic documentation and information about all modules in ProB.

ProB start file in cli mode.

General startup code required for all versions of ProB.

This module contains code to compute compile-time and runtime-pathes.

Utilities for inspecting the features of the current Prolog system, to simplify writing portable code that can run on different Prolog systems.

This module contains many general helper predicates.

A utility on timeouts safe_time_out seperated out from tools.pl to avoid cyclic module dependencies.

This module provides functionality to specify meta-calls that (like a must-not-fail call) that are short-circuited when compiling production code.

This sub-module contains the term-expansing code of the debugging call module, to remove ~~ calls

This module provides predicates to define and run unit tests.

This module contains printing/debug helper predicates.

This module provides predicates to output debugging information when needed.

This module provides functionality to output test case results in a format compatible to junit.

A few utilities on strings/atoms seperated out from tools.pl to avoid cyclic module dependencies.

A few utilities on files seperated out from tools.pl to avoid cyclic module dependencies.

The eventhandling module is used to register predicates that are called when certain events (like loading a specification) occurr.

A few utilities on lists seperated out from tools.pl to avoid cyclic module dependencies.

The error_manager controls error messages. Error messages can be added, retrieved, counted,etc. The module also takes care of extracting source spans from error messages.

This module contains the current version number of ProB together with automatically updated version control infos.

This module manages the various preferences of ProB. Preferences can be grouped, saved and restored and validated from file.

This module contains file io helper predicates.

This module computes hash values (mainly for states) for efficient indexing.

This is the interface to C code for interrupting Prolog runs with a UNIX signal.

A very basic runtime type checker for Prolog.

This module provides operations on the type-checked AST.

This module is responsible for pretty-printing B and CSP, source spans, ...

This module computes transitions and properties depending on the current animator mode.

This module contains predicates that cope with the internal freetype. This is currently only used by the Z extension.

This module provides utilities for B types.

ProBs type checker and type inference module.

This module implements transformations/simplifications on the AST.

b_ast_cleanup_rewrite_rules

A rewriting engine for transformations/simplifications on the AST.

Rewrite rules for transformations/simplifications on the AST.

b_enumeration_order_analysis

This module computes DO_NOT_ENUMERATE variables.

performance_messages

This module allows to generate performance messages.

Compute guard predicates of operations.

Here is the data structure defined that holds a complete B machine.

This module handles pragmas loaded with a b machine

bmachine_static_checks

Static checking of B machines upon construction. Detection of name clashes and uninitalised variables.

ProBs type checker and type inference module.

This module provides various tools for constraint-based checking of B machines.

This module contains higher-level timeout helper predicates.

This module provides operations that are special to the Z notation (sequence compaction, items of a bag).

Tools for generating fresh symbols and numbers.

This module keeps track of the visited states by the animator/model checker.

state_space_open_nodes_c

This module keeps track of the unprocessed states queue of the model checker/animator.

This module packs and upacks states and values.

Interpreter for CSP.

Tools for calling underlying system procedures or binaries (java, dot, krt,...).

haskell_csp_analyzer

Pre-compiler and analyzer for CSP.

Operations on CSP sets.

Operations on CSP sequences.

Basic operations on CSP values.

Operations on CSP tuples.

Provides an interface to the non-B animators depending on animation-mode.

A CSP refinement checker, along with determinism, deadlock and livelock checking.

This module allows to call predicates which can be interrupted by cntrl-c.

The core model checker (does not treat LTL).

This module provides predicates for static analysis of Event-B and B models

This module provides predicates computing weakest preconditions without taking the preconditions of the substitutions into account

weakest_preconditions

This module provides weakest precondition calculation for B and Event-B operations.

This module provides predicates for simplifying B predicates

Create paths for Event-B or Classical B via constraint solving

This module computes enabling relations for B operations.

static_enabling_analysis

This module computes static enabling infos for B operations, without using the constraint solver.

This a few tools for generating dot graphs.

This module provides an interface to ProB's constraint solving kernel.

smt_solvers_interface

This module provides an interface to SMT-solvers like CVC4 or Z3.

This module provides a way to call external functions and predicates.

This is the interface to C code for generating good hashes (SHA-1).

This module provides utilities to print tables.

This module provides on-the-fly construction of random permutations of intervals.

Utilities on the raw AST.

This module provides a meta call to retrieve a specified maximum number of solutions.

This module provides functionality to visualize the dependencies of a B machine (include and sees relations, etc.).

This module contains the rules for loading a Event-B machine or context.

bsyntaxtree_quantifiers

This module provides operations on the type-checked AST.

This module takes care of calling the Java B Parser if necessary.

The socket server is used to interface to Java and other languages.

This module provides the Prolog interface to Java and other languages (usually called via socket server).

This module contains functionality to analyse B expressions and predicates by evaluating and decomposing them into substructures.

Tools for extracting information from DEFINITIONS.

A few utilities for fuzzy matching and completion.

A few utilities to call external programs/commands.

This module provides the new ProB2 Prolog interface to Java and other languages (usually called via socket server).

state_space_exploration_modes

This module groups various techniques for exploring the state space.

Computes all permutations of a B state; used by flooding symmetry.

This module computes symmetry hash markers for B states (used for hash symmetry).

Translate a state graph into a form for nauty and insert into internal DB of nauty C-interface.

Compute canonical forms of state as graphs.

This is the interface to the C code for the symmetry reduction with nauty.

This module provides operations of directed enable graphs.

This module contains predictes for partial order reduction using the ample sets' theory.

This module provides LTL fairness checking on models.

This module provides utility predicates for pretty-printing LTL and CTL formulae.

This module provides utility predicates for the LTL and CTL model checkers.

This module provides predicates for evaluating atomic and transition prepositions.

This is the interface to the LTL model checker's C code.

This module provides predicates for checking an LTL formula on a concrete path.

This is the interface to the LTL2BA tool for LTL to NBA conversion.

state_space_explorer

This module provides predicates for state space exploration without performing any checks.

This module provides predicates for automata-based model checking of safety properties.

This module provides predicates for checking whether an LTL formula is a safety property.

This module provides LTL model checking on models.

Rodin Prover / Disprover

Computation of unsatisfiable cores of predicates.

This module computes WD conditions in AST.

This module provides hypotheses stack management.

This module provides utilities for the WD prover.

This module proves WD POs.

This module provides a simple runtime profiler.

atelierb_provers_interface

This module provides an interface to the Atelier-B provers.

before_after_predicates

This module computes before-after-predicates of B and Event-B actions.

state_space_reduction

This module computes state space projections for dot visualizations.

This module transforms XML into a Prolog representation, adaptation of SICStus library module.

This module contains code to generate test cases based on Event-B or Classical B models

Display canonical form of state graph using dot.

b_machine_identifier_normalization

Normalize all identifiers and strings in the currently loaded B machine. Patterns are preserved using specific prefixes: variables (v), constants (c), deferred sets (s), enumerated elements (e), record fields (f), operation parameters (p), operation return ids (r), operation names (o), local ids (l) e.g. in quantifiers or comprehension sets. Intended to be used for deep learning tasks on B/Event-B machines.

operation_data_generator

This module generates data to train a neural network that predicts the library components that are necessary to synthesize a B operation's substitution for given I/O examples.

Symmetry reduction for synthesis

This module defines the constraint for synthesizing invariants, preconditions or complete operations using simple I/O examples.

This module defines the default library configuration and sets up the selected library from the user used for synthesis.

location_vars_to_program

This module defines the translation from a distribution of location variables to a B/Event-B AST.

This module provides several preprocessing steps for the DPLL(T) based solver such as lifting negations from B operators.

This module provides the conversion from B predicates to SAT formulae and vice-versa to be used for DPLL(T).

This module provides settings for the DPLL(T) solver.

This module provides the SAT solver for DPLL(T) implementing CDCL with backjumping.

This module provides a DPLL(T) based solver for B.

ast_optimizer_for_smt

This module implements transformations to simplify SMT-LIB translations.

This module contains the synthesis workflow following the approach by Gulwani et.al. using SMT solving

This module provides several helper predicates for ProZ.

This module includes a parser for files generated by the fuzz type checker for Z specifications.

This module contains predicates to decompose and operate on Z expressions

This module provides predicates to access a type environment for Z specifications.

This module contains code to extract the variables declared and visible in a schema declaration

This module provides functionality to replace a Z schema's parameter by expressions