From a2cc2a3c95b4f0181484ccb609684bdf66616034 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Tue, 9 Jul 2024 11:42:06 +0200 Subject: [PATCH] add intro to readme Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de> --- README.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/README.md b/README.md index ece10b6..6883009 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,17 @@ TLC4B ===== +This project contains a translator from B to TLA+ with the purpose of applying the +TLC model checker on B models within the ProB validation tool. + +TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker + +The following article describes the translation: +Dominik Hansen and Michael Leuschel. +Translating B to TLA+ for validation with TLC. +Sci. Comput. Program. 131, pages 109-125. 2016. +[Link](https://doi.org/10.1016/j.scico.2016.04.014) + +More details about using TLC4B can be found on the [ProB web pages](https://prob.hhu.de/w/index.php?title=TLC). + [](https://gitlab.cs.uni-duesseldorf.de/general/stups/tlc4b/pipelines) -- GitLab