Remove outdated copy of wiki main page

src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc

-
-[[the-prob-animator-and-modelchecker]]
-= The ProB Animator and Modelchecker
-
-[width="100%",cols="60%,40%",]
-|=======================================================================
-| ProB is an animator, constraint solver and model checker for the
-https://en.wikipedia.org/wiki/B-Method[B-Method] (see the
-https://www.clearsy.com/en/[B-Method
-site of Clearsy]). It allows fully automatic animation of B
-specifications, and can be used to systematically check a specification
-for a wide range of errors. The constraint-solving capabilities of ProB
-can also be used for model finding,
-<<constraint-based-checking,deadlock checking>> and
-<<test-case-generation,test-case generation>>.
-
-The B language is rooted in predicate logic, arithmetic and set theory
-and provides support for data structures such as (higher-order)
-relations, functions and sequences. In addition to the B language, ProB
-also supports http://www.event-b.org/[Event-B],
-http://en.wikipedia.org/wiki/Communicating_sequential_processes[CSP-M],
-http://lamport.azurewebsites.net/tla/tla.html[TLA+],
-and http://en.wikipedia.org/wiki/Z_notation[Z]. ProB can be installed
-within http://sourceforge.net/projects/rodin-b-sharp/[Rodin], where it
-comes with
-https://www3.hhu.de/stups/prob/index.php/BMotion_Studio[BMotionStudio] to
-easily generate domain specific graphical visualizations. (See
-https://www3.hhu.de/stups/prob/[for an overview of ProB's components]).
-ProB can now also be used as a
- https://gitlab.cs.uni-duesseldorf.de/dgelessus/prob2-jupyter-kernel[Jupyter kernel] to generate interactive notebooks.
-
-ProB is being used within Siemens, Alstom, Thales and several other
-companies for http://www.data-validation.fr[data validation] of
-complicated properties for safety critical systems.
-ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.
-In https://www.youtube.com/watch?v=FjKnugbmrP4[a video from the Deutsche Bahn] you can see ProB animating a formal B model of the ETCS hybrid-level 3 principles in real-time, controlling two trains.
-For commercial
-support contact the spin-off company http://www.formalmind.com[Formal
-Mind] or https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team.html[Michael
-Leuschel].
-
-|*1/10/2018* <<downloads,ProB 1.8.2>> is available. Highlights: improved error feedback, support Jupyter kernel, first support for Alloy models.
-
-*20/3/2018* <<downloads,ProB 1.8.0>> is available. Highlights:
-terminal colour support, performance improvements, improved symmetry breaking.
-
-*5/10/2017* <<downloads,ProB 1.7.1>> is available. Highlights:
-performance, Z support, export history to HTML.
-
-*11/7/2017* <<downloads,ProB 1.7.0>> is available. Highlights:
-improved <<generating-documents-with-prob-and-latex,Latex document
-generation>>, improved XML/CSV data import and export, RULE DSL language,
-improvements in solver.
-
-*20/10/2016* <<downloads,ProB 1.6.1>> is available. Highlights:
-<<generating-documents-with-prob-and-latex,Latex document
-generation>>, <<tips-b-idioms,LET and IF-THEN-ELSE for expressions and
-predicates>>.
-
-*22/4/2016* <<downloads,ProB 1.6.0>> is available. Highlights:
-<<tutorial-directed-model-checking,directed model checking>>,
-<<using-prob-with-z3,Z3 as backend>>, B line comments and unicode
-symbols.
-
-*19/2/2015* <<prior-versions-of-prob,ProB 1.5.0>> is available.
-<<state-space-coverage-analyses,MC/DC coverage>>, improved
-<<tlc,TLC interface>>.
-
-*30/03/2012* <<prob-logic-calulator,ProB Logic Calculator>>
-available.
-
-<<release-history, More in the Release History section>>
-
-|=======================================================================
-
-[[implementation]]
-== Implementation
-
-The core of ProB is implemented in
-http://www.sics.se/isl/sicstuswww/site/index.html[SICStus Prolog] (but
-can be run without a SICStus Prolog license). The ProB constraint solver
-is implemented using co-routining and the CLP(FD) finite domain library
-of SICStus. An alternate <<using-prob-with-kodkod,constraint solver
-based on Kodkod (and thus SAT)>> is also available within ProB, as is
-<<using-prob-with-z3,an integration with the SMT solver Z3>>. An
-alternate <<tlc,model checking engine (using TLC)>> well-suited for
-lower level B specifications is also available. An integration with
-https://github.com/utwente-fmt/ltsmin/releases[LTSmin] is also
-available. The <<prob-licence,ProB Licence can be found here>>.
-Automatically generated test
-https://www3.hhu.de/stups/internal/coverage/html/[coverage reports are
-also available].
-
-[[features]]
-== Features
-
-ProB covers a <<summary-of-b-syntax,large part of B>>, and we are
-striving towards full coverage of Atelier B constructs. ProB supports B
-features such as non-deterministic operations, arbitrary quantification,
-sets, sequences, functions, lambda abstractions, set comprehensions,
-records, and many more. ProB does support multiple machines,
-refinements, and implementations. ProB can also be used for automated
-<<refinement-checking,refinement checking>> and
-<<ltl-model-checking,LTL model checking>>. It also
-<<cps-m,supports almost full CSP-M>> process descriptions, to be used
-on their own or to guide B machines for specification and property
-validation. The state space of the specifications can be
-<<graphical-viewer,graphically visualized>>. ProB also supports Z
-specifications (ProB in this context is sometimes called
-<<proz,ProZ>>) as well as <<tla,TLA+ specifications>>. We now also
-have an online <<prob-logic-calulator,ProB Logic Calculator>>. ProB
-can be used within
-http://www.atelierb.eu/en/2016/02/18/atelier-b-4-3-1-is-available-for-maintenance-holders/[Atelier-B
-as a disprover and prover].