kernel_objects

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

kernel_waitflags

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

kernel_card_arithmetic

This module contains cardinality arithmetic that also supports the symbol inf and inf_overflow.

inf_arith

This module contains arithmetic that also supports the symbol inf.

chr_integer_inequality

Provide interface to CHR integer reasoning.

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.

bsets_clp

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

delay

Utilities to delay calls until sufficiently instantiated.

kernel_tools

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

avl_tools

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

closures

This module provides various utility functions to analyse ProB closures.

kernel_records

This module contains predicates that operate on the record type.

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.

b_enumerate

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.

b_interpreter_components

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

value_persistance

This module is responsible for caching constants and operations on disk

kernel_reals

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

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.

kernel_equality

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.

fd_utils_clpfd

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

b_interpreter_check

This module provides a reified interpreter for certain predicates.

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.

clpfd_tables

Provide interface to CLP(FD) table constraint.

clpfd_lists

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.

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.

chr_set_membership

Provide interface to CHR set reasoning.

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.

module_information

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

pathes

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

tools_platform

Utilities for getting information about the platform/OS, seperated out from tools.pl to avoid cyclic module dependencies.

tools_portability

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

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.

prob_startup

General startup code required for all versions of ProB.

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.

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

self_check

This module provides predicates to define and run unit tests.

tools_printing

This module contains printing/debug helper predicates.

tools_positions

A few utilities on raw positions as provided by the B Parser.

debug

This module provides predicates to output debugging information when needed.

eventhandling

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

tools_strings

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

xml_prob

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

junit_tests

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

tools_files

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

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.

version

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

preferences

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

pathes_lib

This module checks the contents of the lib folder and can install some missing components

system_call

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

tools_io

This module contains file io helper predicates.

hashing

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

user_signal

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

translate

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

bsyntaxtree

This module provides operations on the type-checked AST.

gensym

Tools for generating fresh symbols and numbers.

typing_tools

This module provides utilities for B types.

kernel_freetypes

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

typechecker

A very basic runtime type checker for Prolog.

random_permutations

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

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.

btypechecker

ProBs type checker and type inference module.

b_ast_cleanup

This module implements transformations/simplifications on the AST.

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.

b_enumeration_order_analysis

This module computes DO_NOT_ENUMERATE variables.

performance_messages

This module allows to generate performance messages.

b_operation_guards

Compute guard predicates of operations.

bmachine_construction

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

bmachine_structure

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

pragmas

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.

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.

tools_timeout

This module contains higher-level timeout helper predicates.

state_packing

This module packs and upacks states and values.

kernel_z

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

solver_interface

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

external_functions

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

runtime_profiler

This module provides a simple runtime profiler.

probhash

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

input_syntax_tree

Utilities on the raw AST.

parsercall

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

tools_fastread

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

dot_graph_generator

This a few tools for generating dot graphs.

succeed_max

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

b_machine_hierarchy

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

bmachine_eventb

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

bsyntaxtree_quantifiers

This module provides operations on the type-checked AST.

external_function_declarations

This module provides utilities to query the available external functions.

softfloat

This module provides software floating point operations via the berkley softfloat library.

table_tools

This module provides utilities to print tables.

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

cbc_path_solver

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

quantifier_instantiation

This module implements transformations to simplify SMT-LIB translations.

ast_optimizer_for_smt

This module implements transformations to simplify SMT-LIB translations.

cdclt_settings

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

cdclt_stats

This module logs statistics of the CDCL(T) solver if the options is set in the CDCL(T) settings module.

well_def_analyser

This module computes WD conditions in AST.

well_def_hyps

This module provides hypotheses stack management.

well_def_tools

This module provides utilities for the WD prover.

well_def_prover

This module proves WD POs.

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.

predicate_handling

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

cdclt_preprocessing

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

cdclt_pred_to_sat

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

unsat_cores

Computation of unsatisfiable cores of predicates.

fibonacci_heap

Fibonacci heap to store atoms with a priority.

cdclt_sat_solver

This module provides the SAT solver for CDCL(T) implementing CDCL with backjumping and further improvements.

cdclt_solver

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

enabling_analysis

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.

pge_algo

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

tcltk_interface

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

state_space_exploration_modes

This module groups various techniques for exploring the state space.

xtl_interface

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

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.

state_permuter

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

symmetry_marker

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

graph_iso_nauty

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

state_graph_canon

Compute canonical forms of state as graphs.

graphiso

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

b_trace_checking

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

translate_keywords

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

visualize_graph

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

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.

state_space_reduction

This module computes state space projections for dot visualizations.

prob2_interface

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

pref_definitions

Tools for extracting information from DEFINITIONS.

tools_matching

A few utilities for fuzzy matching and completion.

enable_graph

This module provides operations of directed enable graphs.

ample_sets

This module contains predictes for partial order reduction using the ample sets' theory. It is only applicable in B mode (not CSP||B).

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.

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 LTL2BA tool for LTL to NBA conversion.

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.

ctl

This module provides CTL model checking on models.

bvisual2

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

tools_commands

A few utilities to call external programs/commands.

disprover

Rodin Prover / Disprover

b2setlog

This module provides a translation from B to Setlog

state_as_dot_graph

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

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

z_tools

This module provides several helper predicates for ProZ.

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.

eval_strings

Tools to evaluate B expressions and predicates passed as strings.

cvc4interface

This is the interface between ProB and the CVC4 SMT solver

z3interface

This is the interface between ProB and the Z3 SMT solver

solver_dispatcher

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

logger

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

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_expression_sharing

Common-Subexpression Elimination.

optimizing_solver

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

graphical_state_viewer_images

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

bmc

A finite-state symbolic model checker based on BMC.

solver_handling

Internal data structures for solver / prover

ce_replay

Replay symbolically generated traces.

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.

b2sat

This is the interface for ProB to use various SAT solvers (glucose, Z3)

source_profiler

This module provides a simple B model source profiler.

satsolver

This is the interface between ProB and the Glucose SAT solver

hit_profiler

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

meta_interface

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

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

uml_generator

This module generates UML diagrams for PlantUML.

mcdc_coverage

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

b_operation_cache

This module caches B operation results on projected states. Used when preference try_operation_reuse different from false

visb_visualiser

This module provides VisB visualisation functionality.

mcts_game_play

This module provides Monte Carlo Tree Search for games.

b_intelligent_trace_replay

Replay saved (JSON) traces in a flexible way.

sap

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

b_show_history

Write animator history into a file in B format.

ltsmin

This is the interface to C code for LTSmin integration.

cbc_refinement_checks

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

state_space_dijkstra

Tools for finding shortest paths between visited states.

predicate_evaluator

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

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.

eval_interface

Utilities for evaluating formulas, predicates, expressions.

ltl_propositions

This module provides predicates for evaluating atomic and transition prepositions.

avl_ugraphs

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

xml2b

This module transforms XML into a B representation.

json_freetype

This module provides translation between the internal json_parser representation and the freetype representation used in the stdlib

zmq_rpc

RPC via ZMQ implementation (using JSON-RPC 2.0)

model_translation

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

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.

ast_cleanup_for_smt

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

prob_state_predicates

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

smt_solvers_interface

This module provides an interface to SMT-solvers like CVC4 or 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

record_detection

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

partition_detection

This module detects set partition predicates.

bmachine

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

rule_validation

This module provides functionality for the B Rules DSL.

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.

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.

prob_socketserver

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

predicate_debugger

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

ctigar

An infinite-state symbolic model checker based on CTIGAR.

predicate_abstraction

An abstract domain using predicate abstraction.

trace_generator

This module generates all traces under a certain condition.

compile_time_flags

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

smt_solver_benchmarks

This module provides benchmarks for the integration of Z3 and the different versions of the CDCL(T) based solver.

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.