TLC - Revision history

Jan Gruteser: /* Using TLC in probcli */

2024-07-24T11:27:30Z

Using TLC in probcli

← Older revision		Revision as of 11:27, 24 July 2024
Line 39:		Line 39:
	* -noltl (no checking of LTL assertions)		* -noltl (no checking of LTL assertions)

	~~The preference~~ <tt>TLC_WORKERS</tt> influences the number of workers that will be used by TLC.		ProB Preferences influencing TLC:
	~~So,~~ a call might look like this:		* <tt>TLC_WORKERS</tt>: influences the number of workers that will be used by TLC; a call might look like this:
	probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl		<tt>probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl</tt>
			* <tt>TLC_USE_PROB_CONSTANTS</tt>: setup constants using ProB before applying TLC (can lead to a considerable speed-up); e.g.
			<tt>probcli FILE.mch -mc_with_tlc -p TLC_USE_PROB_CONSTANTS TRUE</tt>

	= When to use TLC =		= When to use TLC =

2024-07-24T11:23:00Z

Limitations

← Older revision		Revision as of 11:23, 24 July 2024
Line 61:		Line 61:
	* Refinement specifications		* Refinement specifications
	* Machine inclusion (SEES, INCLUDES, ..)		* Machine inclusion (SEES, INCLUDES, ..)
	* Sequential composition ~~statement~~ (G;H)		* Sequential composition (G;H) with variables assigned more than once

	= Visited States =		= Visited States =

2024-07-09T09:45:35Z

More Information

← Older revision		Revision as of 09:45, 9 July 2024
Line 83:		Line 83:

	= More Information =		= More Information =
	More information can be found in our [https://~~www3~~.~~hhu~~.de/~~stups/downloads/pdf/HansenLeuschel_ABZ14~~.~~pdf ABZ'14 article~~].		More information can be found in our article which is an extended version of the ABZ'2014 conference paper:
			* Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link].

2024-07-09T09:44:31Z

Translation from B to TLA+

← Older revision		Revision as of 09:44, 9 July 2024
Line 56:		Line 56:
	The following article describes the translation in more detail:		The following article describes the translation in more detail:
	* Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link].		* Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link].

	~~There is also a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.~~

	= Limitations =		= Limitations =

2024-07-09T09:44:08Z

Translation from B to TLA+

← Older revision		Revision as of 09:44, 9 July 2024
Line 54:		Line 54:
	The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.		The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

	There is a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.		The following article describes the translation in more detail:
			* Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link].

			There is also a [http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport technical report] that describes our translation from B to TLA+.

	= Limitations =		= Limitations =

2022-02-04T17:00:47Z

Translation from B to TLA+

← Older revision		Revision as of 17:00, 4 February 2022
Line 50:		Line 50:

	TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].		TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+].
	To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.		To validate B specification with TLC we developed the translator [https://gitlab.cs.uni-duesseldorf.de/general/stups/tlc4b TLC4B] which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B.
	Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.		Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator.
	The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.		The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.

2021-02-03T17:02:29Z

Update article PDF link

← Older revision		Revision as of 17:02, 3 February 2021
Line 82:		Line 82:

	= More Information =		= More Information =
	More information can be found in our [~~http~~://~~www~~.~~stups.uni-duesseldorf~~.de/w/~~Special:Publication~~/HansenLeuschel_ABZ14 ABZ'14 article].		More information can be found in our [https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_ABZ14.pdf ABZ'14 article].

2016-08-11T12:05:41Z

← Older revision		Revision as of 12:05, 11 August 2016
Line 23:		Line 23:
	[[File:Model_Checking_With_TLC_Trace.png\|400px\|center]]		[[File:Model_Checking_With_TLC_Trace.png\|400px\|center]]
	=== Requirements ===		=== Requirements ===
	On Linux the tlc-thread package is required to run TLC from the tcl/tk ui.		On Linux the tlc-thread package is required to run TLC from the tcl/tk ui:
			sudo apt-get install tcl-thread

	~~the sudo apt-get install tcl-thread~~
	== Using TLC in probcli ==		== Using TLC in probcli ==

2016-08-11T12:02:57Z

← Older revision		Revision as of 12:02, 11 August 2016
Line 22:		Line 22:

	[[File:Model_Checking_With_TLC_Trace.png\|400px\|center]]		[[File:Model_Checking_With_TLC_Trace.png\|400px\|center]]
			=== Requirements ===
			On Linux the tlc-thread package is required to run TLC from the tcl/tk ui.

			the sudo apt-get install tcl-thread
	== Using TLC in probcli ==		== Using TLC in probcli ==

2016-01-13T14:10:59Z

How to use TLC

@@ Line 4: / Line 4: @@
 = How to use TLC =
 First you have to open a B specification in the ProB GUI.
 Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.
@@ Line 21: / Line 22: @@
 [[File:Model_Checking_With_TLC_Trace.png|400px|center]]
 = When to use TLC =
 TLC is extremely valuable when it comes to explicit state model checking for large state spaces.