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 provides memoization features (for closure expansion, closure1,...).

This module contains predicates that operate on the record type.

This module takes care of enumerating B variables.

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 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.

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

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 translates AST constructs to calls in the ProB kernel.

This module detects information about variables by using frozen.

This module contains arithmetic that also supports the symbol inf.

This module can be used to find optimal (maximal/minimal) solutions to a predicate.

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

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.

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

General startup code required for all versions of ProB.

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.

This module contains file io helper predicates.

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.

b_expression_sharing

Common-Subexpression Elimination.

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

ProBs type checker and type inference module.

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

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.

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

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

This module contains higher-level timeout helper predicates.

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 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 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 contains the current version number of ProB together with automatically updated version control infos.

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

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.

This module provides a more efficient way to parse and read Prolog terms.

Tools for calling underlying system procedures.

This module provides a simple runtime profiler.

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.

A few utilities for fuzzy matching and completion.

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

A few utilities to call external programs/commands.

This module provides a simple profile just counting number of hits.

A module to interface ProB's avl_set relations with the SICStus ugraph library (unweighted graphs).

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).

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.

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 module detects set partition predicates.

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 provides a simple B model source profiler.

This module caches B operation results on projected states.

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

Provide interface to CHR set reasoning.

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

This module computes WD conditions in AST.

This module provides hypotheses stack management.

This module proves WD POs.