kernel_waitflags

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

clpfd_interface

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

kernel_dif

This module provides a dif which works with reified equality.

kernel_objects

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

avl_tools

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

kernel_records

This module contains predicates that operate on the record type.

kernel_tools

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

delay

Utilities to delay calls until sufficiently instantiated.

store

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

memoization

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

kernel_mappings

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

bsets_clp

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

b_interpreter_check

This module provides a reified interpreter for certain predicates.

b_enumerate

This module takes care of enumerating B variables.

kernel_ordering

This module provides term ordering utilities.

bool_pred

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

kernel_strings

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

value_persistance

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

b_compiler

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

kernel_frozen_info

This module detects information about variables by using frozen.

inf_arith

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.

kernel_equality

This module provides reified equality and membership predicates.

fd_utils_clpfd

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

clpfd_lists

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

closures

This module provides various utility functions to analyse ProB closures.

clpfd_tables

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

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

b_interpreter

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

kernel_propagation

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

kernel_lists

This module provides operations for lists of B objects.

module_information

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_cli

ProB start file in cli mode.

debugging_calls

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

debugging_calls_te

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

pathes

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

tools

This module contains many general helper predicates.

tools_meta

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

self_check

This module provides predicates to define and run unit tests.

tools_printing

This module contains printing/debug helper predicates.

debug

This module provides predicates to output debugging information when needed.

junit_tests

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

tools_strings

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

tools_files

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

eventhandling

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

tools_lists

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

error_manager

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.

preferences

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

typechecker

A very basic runtime type checker for Prolog.

random_permutations

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

gensym

Tools for generating fresh symbols and numbers.

state_space

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.

specfile

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

bsyntaxtree

This module provides operations on the type-checked AST.

translate

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

bmachine_structure

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

btypechecker

ProBs type checker and type inference module.

b_ast_cleanup

This module implements transformations/simplifications on the AST.

tools_timeout

This module contains higher-level timeout helper predicates.

kernel_freetypes

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

external_functions

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

kernel_z

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

probhash

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

hashing

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

succeed_max

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

version

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

state_packing

This module packs and upacks states and values.

b_machine_hierarchy

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

tools_io

This module contains file io helper predicates.

pragmas

This module handles pragmas loaded with a b machine

bmachine_eventb

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

z_tools

This module provides several helper predicates for ProZ.

dot_graph_generator

This a few tools for generating dot graphs.

parsercall

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

system_call

Tools for calling underlying system procedures.

bvisual2

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

haskell_csp

Interpreter for CSP.

haskell_csp_analyzer

Pre-compiler and analyzer for CSP.

csp_sets

Operations on CSP sets.

csp_sequences

Operations on CSP sequences.

csp_basic

Basic operations on CSP values.

csp_tuples

Operations on CSP tuples.

xtl_interface

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

refinement_checker

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

user_interrupts

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

user_signal

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

pref_definitions

Tools for extracting information from DEFINITIONS.

predicate_debugger

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

interval_calc

This module provides methods to calculate with interval expressions.

predicate_analysis

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

kodkod_tools

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

kodkod_translate

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

kodkod_rewrite

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.

kodkod2

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

kodkod_typing

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

kodkod_printer

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

kodkod_process

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

kodkod_annotator

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

kodkod

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

b_read_write_info

ProBs type checker and type inference module.

b_state_model_check

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

solver_interface

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.

model_translation

This module translates the models found by an SMT-solvers to a ProB state.

solver_dispatcher

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

cvc4interface

This is the interface between ProB and the CVC4 SMT solver

z3interface

This is the interface between ProB and the Z3 SMT solver

ast_cleanup_for_smt

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.

seq_rewriter

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

static_ordering

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

unsat_cores

Computation of unsatisfiable cores of predicates.

satsolver

This is the interface between ProB and the Glucose SAT solver

xml2b

This module transforms XML into a B representation.

xml_prob

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_db

Rewrite rules for transformations/simplifications on the AST.

partition_detection

This module detects set partition predicates.

tools_matching

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.

record_detection

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

bmachine

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

translate_keywords

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

b_operation_cache

This module caches B operation results on projected states.

b_trace_checking

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.

eclipse_interface

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

model_checker

The core model checker (does not treat LTL).

static_analysis

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

enabling_predicates

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.

b_simplifier

This module provides predicates for simplifying B predicates

prob2_interface

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

symmetry_marker

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

evalstores

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

enable_graph

This module provides operations of directed enable graphs.

enabling_analysis

This module computes enabling relations for B operations.

pge_algo

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

ample_sets

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

ltl_fairness

This module provides LTL fairness checking on models.

ltl_translate

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

ltl_tools

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

ltl_propositions

This module provides predicates for evaluating atomic and transition prepositions.

ltlc

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

ltl_verification

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

ltl2ba

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.

safety_mc

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

ltl_safety

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

ltl

This module provides LTL model checking on models.

disprover

Rodin Prover / Disprover

graph_canon

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

graph_iso_nauty

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

graphiso

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 like variables, deferred sets, or enumerated elements are preserved using specific prefixes.

before_after_predicates

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

data_generator

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

Symmetry reduction for synthesis

constraints

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

library_setup

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.

b_synthesis

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

state_viewer_images

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

eval_strings

Tools to evaluate B expressions and predicates passed as strings.

bmc

A finite-state symbolic model checker based on BMC.

predicate_handling

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

solver_handling

Internal data structures for solver / prover

atelierb_provers_interface

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

kinduction

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

ic3

A symbolic model checker based on IC3.

unsat_core_generalization

Counter example generalization based on unsat cores.

mic_generation

Generation of minimal inductive (sub-)clauses.

coverage_statistics

This module is responsible for computing state space coverage info.

meta_interface

This module provides access and description to a variety of Prolog commands.

visualize_graph

This module generates various dot graphs (state space, single state, transition diagram,...).

reduce_graph_state_space

Various minimization/reduction algorithms for the state space.

dot_graphs_static_analysis

This module provides predicates for printing out graphs in dot-format calculated by computing some of the static analyses used for partial order reduction

state_custom_dot_graph

This module provides a way to generate custom state graphs (using info from DEFINITIONS).

sap

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

bvisual

Generate a dot visualization of B predicates and expressions.

bvisual_any_maxsolver

Tool for generating dot visualization of B predicates and expressions. Finds a maximally satisfiable subset for predicates.

maxsolver

Finds a maximally satisfiable subset for predicates; used by bvisual_any_maxsolver.

cbc_refinement_checks

This module provides constraint-based checking of B and Event-B refinements.

state_permuter

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

fdr_csp_generator

Tools for exporting state space in CSP or Promela format.

fuzzfile

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

subexpressions

This module contains predicates to decompose and operate on Z expressions

zenvironment

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

schemavars

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

zparameters

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

schemaexpansion

This module includes code for expanding Z schemas, i.e. removing references to other schemas by their content and evaluating schema calculus expressions

dependence

This module provides a predicate to find dependencies between Z schemas

z_typechecker

This module contains a type checker for Z specifications, mainly because the types are needed for the translation to B.

ztransformations

This module provides several transformations on the Z syntax tree in order to prepare the translation to B.

consistencycheck

This module provides functionality to check whether the internal data structures of ProZ are consistent.

proz

This is the central ProZ module for translating Z specification into B.

ltsmin

This is the interface to C code for LTSmin integration.

ctl

This module provides CTL model checking on models.

b_show_history

Write animator history into a file in B format.

mcdc_coverage

A module to construct MC/DC coverage criterion predicates and check them in the state space

prologTasks

This module provides the interface to the Tcl/Tk tree_inspector.

ast_inspector

This module provides the logic behind the AST inspector debugging view in Tcl

tcltk_tree_inspector

This module provides the interface to the Tcl/Tk tree_inspector.

cbc_ba

A constraint-based invariant checker using before-after predicates.

ctigar

An infinite-state symbolic model checker based on CTIGAR.

predicate_abstraction

An abstract domain using predicate abstraction.

tcltk_interface

Interface between the Tcl/Tk GUI, the CLI and the internal modules.

state_space_dijkstra

Tools for finding shortest paths between visited states.

predicate_evaluator

Various tools to analyse conjunctions of predicates textually (along with statistics).

prob_socketserver

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

logger

This module is responsible for (xml and prolog) logging.

zmq

This is the interface to C code for distributed model checking.

master

This is the interface to C code for distributed model checking.

worker

This is the interface to C code for distributed model checking.

kodkod_test

This is a test engine for the Kodkod translation functionality.

smtlib2_cli

Command line interface and REPL for SMT-LIB 2 files.

smtlib2_interpreter

The SMT-LIB 2 Interpreter - Main Interpreter

smtlib2_environment

The SMT-LIB 2 Interpreter - Environment

smtlib2_translation

The SMT-LIB 2 Interpreter - Translation from SMT-LIB 2 to B

smtlib2_parser

The SMT-LIB 2 Interpreter - Parser

disprover_test_runner

Rodin Prover / Disprover

latex_processor

This module processes Latex Files for ProB commands.

compile_time_flags

This module describes the possible compile-time flags of ProB.

pltables_export

This module provides html/latex and codespeed export functionality for the other table modules

pltables_export_tools

Tools used by several of the export modules

pltables_export_html

This module is used to export coverage tables to html.

pltables_export_latex

This module is used to export coverage tables to latex.

pltables_export_xml

This module is used to export coverage tables to xml.

pltables_export_csv

This module is used to export coverage tables to csv.

pltables

This module is used to generate, store and export coverage tables.

coverage_tools

This module automatically generates the SICStus Prolog coverage information reports.

testcases

This module defines the (integration) tests.

test_runner

This module runs the tests stored in testcases.pl.

prob_cov

ProB start file with coverage tests activated. Includes predicates to execute certain tests. Used by Jenkins.