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

fd_utils_clpfd

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

kernel_tools

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

delay

Utilities to delay calls until sufficiently instantiated.

kernel_records

This module contains predicates that operate on the record type.

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.

external_functions

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

kernel_ordering

This module provides term ordering utilities.

bool_pred

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

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 componente individually (with tracing feedback).

kernel_equality

This module provides reified equality and membership predicates.

clpfd_lists

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

clpfd_tables

Provide interface to CLP(FD) table constraint.

inf_arith

This module contains arithmetic that also supports the symbol inf.

kernel_mappings

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

b_interpreter

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

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

closures

This module provides various utility functions to analyse ProB closures.

store

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

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.

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

pathes

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

tools

This module contains many general helper predicates.

self_check

This module provides predicates to define and run unit tests.

gensym

Tools for generating fresh symbols and numbers.

tools_strings

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

tools_printing

This module contains printing/debug helper predicates.

debug

This module provides predicates to output debugging information when needed.

typechecker

A very basic runtime type checker for Prolog.

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.

eventhandling

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

tools_meta

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

junit_tests

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

random_permutations

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

translate

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

bsyntaxtree

This module provides operations on the type-checked AST.

kernel_freetypes

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

btypechecker

ProBs type checker and type inference module.

b_ast_cleanup

This module implements transformations/simplifications on the AST.

specfile

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

hashing

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

probhash

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

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_structure

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

bmachine_eventb

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

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.

predicate_debugger

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

xml2b

This module transforms XML into a B representation.

kernel_z

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

interval_calc

This module provides methods to calculate with interval expressions.

predicate_analysis

This is an experimental plugin to extract information about expressions (e.g. integer bounds (aka intervals), cardinality) by static analysis.

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

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.

tools_timeout

This module contains higher-level timeout helper predicates.

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.

plugins

A plugin mechanism for ProB.

xtl_interface

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

h_int

This is the Promela (the Spin model checker language) extension.

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.

refinement_checker

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

user_signal

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

b_operation_cache

This module caches B operation results on projected states.

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.

pref_definitions

Tools for extracting information from DEFINITIONS.

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

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.

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.

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

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

flow

Flow Analysis for Event-B models. Extracts a flow graph from a model.

reduce_graph_state_space

Various minimization/reduction algorithms for the state space.

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.

visualize_graph

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

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.

ltl_fairness

This module provides LTL fairness checking on models.

promela_tools

This module contains helper predicates for the Promela extension.

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.

eclipse_interface

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

evalstores

This module provides methods to construct stores dynamically and evaluate expressions in them.

eval_strings

Tools to evaluate B expressions and predicates passed as strings.

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.

before_after_predicates

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

ltl_prepositions

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.

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

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.

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

sap

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

pge_algo

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

state_custom_dot_graph

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

fdr_csp_generator

Tools for exporting state space in CSP or Promela format.

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.

ltsmin

This is the interface to C code for LTSmin integration.

ctl

This module provides CTL model checking on models.

promela_ncprinter

Promela extension: This module contains predicates to print never claims.

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.

predicate_handling

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

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

user_interrupts

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

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.

log_analyser

A small tool to generate Excel or Gnuplot data and scripts to analyse data generated by probcli when model checking with logging (-l).

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

atelierb_provers_interface

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

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.

ic3

A symbolic model checker based on IC3.

solver_handling

Internal data structures for solver / prover

unsat_core_generalization

Counter example generalization based on unsat cores.

mic_generation

Generation of minimal inductive (sub-)clauses.

ctigar

An infinite-state symbolic model checker based on CTIGAR.

predicate_abstraction

An abstract domain using predicate abstraction.

kinduction

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

bmc

A finite-state symbolic model checker based on BMC.

absint

This is an experimental plugin that applies abstract interpretation on B models.

b_abstract_interpreter

Abstract Interpreter for B.

b_abstract_mappings

Experimental abstract interpretation plugin: this module maps regular operators to the ones in the selected abstract domain.

interval

Integer interval analysis for the experimental abstract interpretation plugin. This domain abstracts integers by intervals and sets by the cardinality.

b_abstract_interpreter_helpers

Abstract Interpreter: Helper Predicates

xtl_program

This module provides just a namespace for a loaded XTL file (experimental plugin).

xtl

This module provides the experimental XTL (LTS definition with a Prolog-like syntax) support.

testaddon

This is an example plugin for the experimental plugin structure.

units_conversions

Units Plugin: This module lists conversion factors for different units.

units_domain

Units Plugin: The abstract Domain.

unit_parser

Units Plugin: Parsing unit expressions inside pragmas to internal representation of units.

units_alias

Units Plugin: Short aliases for commonly used units.

units_interpreter_helpers

Units Plugin: Helper Predicates

units_tools

Units Plugin: Analysis tools used in several places.

units_interpreter

Units Plugin: Abstract Interpreter

units_prettyprint

Units Plugin: Prettyprinter for properties and transitions

units

Units Plugin: This is an experimental plugin that analyses physical units stored in pragmas.

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.