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

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 AVL-tree utilities used by the kernel.

This module contains predicates that operate on the record type.

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

Utilities to delay calls until sufficiently instantiated.

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 provides more advanced operations for the basic datatypes of ProB (mainly for relations, functions, sequences).

This module provides a reified interpreter for certain predicates.

This module takes care of enumerating B variables.

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 is responsible for caching constants and operations on disk

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.

This module contains arithmetic that also supports the symbol inf.

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.

This module provides reified equality and membership predicates.

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

kernel_cardinality_attr

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

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

This module provides various utility functions to analyse ProB closures.

Provide interface to CLP(FD) table constraint.

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 support for deferred/enumerated set elements in B.

static_symmetry_reduction

This module provides support for symmetry reduction on deferred sets.

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 contains functionality to store basic documentation and information about all modules in ProB.

coverage_term_expander

This module generates various statistics by expanding and counting terms. Used in the coverage reports.

ProB start file in cli mode.

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 contains code to compute compile-time and runtime-pathes.

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 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 manages the various preferences of ProB. Preferences can be grouped, saved and restored and validated from file.

A very basic runtime type checker for Prolog.

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

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 computes transitions and properties depending on the current animator mode.

This module provides operations on the type-checked AST.

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

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

ProBs type checker and type inference module.

This module implements transformations/simplifications on the AST.

This module contains higher-level timeout helper predicates.

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

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

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

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

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

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

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

This module packs and upacks states and values.

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

This module contains file io helper predicates.

This module handles pragmas loaded with a b machine

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

This module provides several helper predicates for ProZ.

This a few tools for generating dot graphs.

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

Tools for calling underlying system procedures.

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

Interpreter for CSP.

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.

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

Tools for extracting information from DEFINITIONS.

The predicate debugger adds conjuncts one by one until the predicate becomes unsatisfiable.

This module provides methods to calculate with interval expressions.

This is a module and plugin to extract information about expressions (e.g. integer bounds (aka intervals), cardinality) by static analysis. Used by Kodkod.

This module contains helper predicates for the Kodkod translation part of ProB

This module contains the code to translate B expressions and predicates into Kodkod.

This module contains rewriting rules that are applied during tge translation to Kodkod.

kodkod_integer_recalc

This module provides functionality to adapt the outcome of the interval analysis to the needs of the Kodkod translation.

This module contains the several phases of a translation process to Kodkod.

This is a small internal type checker for Kodkod expressions. It's needed for inserting casts between different integer representations.

This module contains code to print the description of a Kodkod problem, used to send it to a seperate process.

This is the inter-process communication with the Java process that contains the Kodkod engine.

Annotate specific constraints within a typed B or Event-B AST with external predicate calls to be solved by Kodkod.

This is the central module of the B to Kodkod translation (still experimental).

ProBs type checker and type inference module.

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

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 translates the models found by an SMT-solvers to a ProB state.

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

This is the interface between ProB and the CVC4 SMT solver

This is the interface between ProB and the Z3 SMT solver

This module implements transformations needed by the SMT-LIB translation.

smt_common_predicates

Shared Predicates used by several Modules belonging to the SMT Solvers Integration.

This module implements transformations of sequences to sets as needed by the SMT-LIB translation.

prob_state_predicates

This module translates ProB's (local) states to predicates understandable for CVC4/Z3

Sort a list of identifiers according to the number of occurences inside conjuncts of a predicate. Mimics the static ordering heursitic of SAT solvers

Computation of unsatisfiable cores of predicates.

This is the interface between ProB and the Glucose SAT solver

This module transforms XML into a B representation.

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

b_ast_cleanup_rewrite_rules

A rewriting engine for transformations/simplifications on the AST.

Rewrite rules for transformations/simplifications on the AST.

This module detects set partition predicates.

A few utilities for fuzzy matching and completion.

bmachine_static_checks

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

bmachine_construction

This module contains the rules for loading, including, seeing, etc. B machines, scope of constants, variables, parameters, etc.

This module detects bijections between deferred sets and cartesian products, and compiles them away.

This module provides access to the various parts of the loaded B machine.

This module is responsible for translating identifiers which happen to be keywords

This module caches B operation results on projected states.

Replay saved traces; raise error if not possible. Used in regression testing.

state_space_exploration_modes

This module groups various techniques for exploring the state space.

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

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

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

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

This module provides methods to construct stores dynamically and evaluate expressions in them, possibly used only by ProB1 for Rodin.

This module provides operations of directed enable graphs.

This module computes enabling relations for B operations.

This module contains predictes for model checking B and Event-B models using the partial guard evaluation optimisastion.

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 LTL3BA tool for LTL ---> NBA.

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

Compute canonical forms of state graphs and store them using nauty C interface.

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

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

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.

before_after_predicates

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

This module generates data to train a neural network that predicts the library components that are necessary to synthesize a program 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 contains the synthesis workflow following the approach by Gulwani et.al. using SMT solving

This module can provide a Tk graphical representation of a B state.

Tools to evaluate B expressions and predicates passed as strings.

This module provides a DPLL(T) based solver for B combining ProB, Z3 and Kodkod.

A finite-state symbolic model checker based on BMC.

Handling and creation of predicates used in the symbolic model checker.

Internal data structures for solver / prover

atelierb_provers_interface

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

A finite-state symbolic model checker based on k-Induction.