LTSmin - Revision history

Michael Leuschel: /* LTSmin Extension of ProB */

2022-03-24T06:53:13Z

LTSmin Extension of ProB

← Older revision		Revision as of 06:53, 24 March 2022
Line 11:		Line 11:
	In order to set up the LTSmin and ProB integration, do the following:		In order to set up the LTSmin and ProB integration, do the following:

	* Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it		* Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it (as of ProB 1.12.0-beta1 you can also simply type <tt>probcli --install ltsmin</tt>)
	* (Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ		* (Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ
	* In ProB, go to Preferences > All Preferences (alphabetical)…		* In ProB, go to Preferences > All Preferences (alphabetical)…
	* Set the LTSMIN preference to the subfolder called "bin/" of the extracted LTSmin archive (containing the binaries prob2-lts-seq, prob2lts-sym, ...)		* Set the LTSMIN preference to the subfolder called "bin/" of the extracted LTSmin archive (containing the binaries prob2-lts-seq, prob2lts-sym, ...; you do not need to do this step if you have installed ltsmin with <tt>probcli --install ltsmin</tt>)
	* Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)		* Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)

Michael Leuschel: /* LTSmin Extension of ProB */

2022-03-23T07:47:00Z

LTSmin Extension of ProB

← Older revision		Revision as of 07:47, 23 March 2022
Line 14:		Line 14:
	* (Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ		* (Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ
	* In ProB, go to Preferences > All Preferences (alphabetical)…		* In ProB, go to Preferences > All Preferences (alphabetical)…
	* Set the ~~LTSmin~~ preference to the bin/ ~~subfolder~~ of the extracted LTSmin archive (containing the binaries prob2-lts-seq, prob2lts-sym, ...)		* Set the LTSMIN preference to the subfolder called "bin/" of the extracted LTSmin archive (containing the binaries prob2-lts-seq, prob2lts-sym, ...)
	* Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)		* Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-12T10:31:45Z

ProB LTSmin CLI-Commands

@@ Line 79: / Line 79: @@
 /prob2lts-seq with [--trace,/tmp/prob-ltsmin-trace.gcf,-c,-d] exited with status: exit(0)
 LTSMin found no counter example
 </pre>

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-10T08:00:17Z

ProB LTSmin CLI-Commands

← Older revision		Revision as of 08:00, 10 June 2020
Line 54:		Line 54:
	An example run:		An example run:
	<pre>		<pre>
	)$ probcli scheduler.mch -mc_with_lts_seq -noinv -p LTSMIN ~/bin/ltsmin_v3.0.2/bin		$ probcli scheduler.mch -mc_with_lts_seq -noinv -p LTSMIN ~/bin/ltsmin_v3.0.2/bin
	starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[])		starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[])
	prob2lts-seq, 0.001: ProB module initialized		prob2lts-seq, 0.001: ProB module initialized

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-10T08:00:05Z

ProB LTSmin CLI-Commands

← Older revision		Revision as of 08:00, 10 June 2020
Line 50:		Line 50:

	\|}		\|}


			An example run:
			<pre>
			)$ probcli scheduler.mch -mc_with_lts_seq -noinv -p LTSMIN ~/bin/ltsmin_v3.0.2/bin
			starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[])
			prob2lts-seq, 0.001: ProB module initialized
			prob2lts-seq, 0.001: Loading model from /tmp/ltsmin.probz
			prob2lts-seq, 0.001: ProB init
			prob2lts-seq, 0.002: connecting to zocket ipc:///private/tmp/ltsmin.probz
			pl_init_for_lts_min
			vars([active,ready,waiting])
			prob2lts-seq, 0.026: There are 7 state labels and 1 edge labels
			prob2lts-seq, 0.026: State length is 4, there are 6 groups
			prob2lts-seq, 0.026: Running dfs search strategy
			prob2lts-seq, 0.026: Using a tree for state storage
			prob2lts-seq, 0.147: state space 30 levels, 36 states 156 transitions
			prob2lts-seq, 0.147: Deadlocks: >= 0
			prob2lts-seq, 0.147: terminating ProB connection
			get-next-state: 121
			get-next-state (short): 0
			get-next-action: 0
			get-next-action (short): 0
			get-state-label: 0
			get-state-label (short): 0
			get-label-group: 0
			prob2lts-seq, 0.147: disconnecting from zocket ipc:///private/tmp/ltsmin.probz
			/prob2lts-seq with [--trace,/tmp/prob-ltsmin-trace.gcf,-c,-d] exited with status: exit(0)
			LTSMin found no counter example
			</pre>

Michael Leuschel: /* LTSmin Extension of ProB */

2020-06-10T07:50:49Z

LTSmin Extension of ProB

← Older revision		Revision as of 07:50, 10 June 2020
Line 14:		Line 14:
	* (Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ		* (Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ
	* In ProB, go to Preferences > All Preferences (alphabetical)…		* In ProB, go to Preferences > All Preferences (alphabetical)…
	* Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive		* Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive (containing the binaries prob2-lts-seq, prob2lts-sym, ...)
	* Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)		* Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)

Line 20:		Line 20:

	[[File:ProBLTSMinTk.png\|\|600px]]		[[File:ProBLTSMinTk.png\|\|600px]]


	== ProB LTSmin CLI-Commands ==		== ProB LTSmin CLI-Commands ==

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-10T07:47:07Z

ProB LTSmin CLI-Commands

← Older revision		Revision as of 07:47, 10 June 2020
Line 26:		Line 26:

	{\| cellpadding="5" cellspacing="1" width="100%" border="1"		{\| cellpadding="5" cellspacing="1" width="100%" border="1"
	!style="background-color:lightgrey;" \| "probcli Flag "		!style="background-color:lightgrey;" \| probcli Flag
	!style="background-color:lightgrey;" \| Example		!style="background-color:lightgrey;" \| Example
	!style="background-color:lightgrey;" \| Description		!style="background-color:lightgrey;" \| Description

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-10T07:46:54Z

ProB LTSmin CLI-Commands

← Older revision		Revision as of 07:46, 10 June 2020
Line 26:		Line 26:

	{\| cellpadding="5" cellspacing="1" width="100%" border="1"		{\| cellpadding="5" cellspacing="1" width="100%" border="1"
	!style="background-color:lightgrey;" \| probcli Flag		!style="background-color:lightgrey;" \| "probcli Flag "
	!style="background-color:lightgrey;" \| Example		!style="background-color:lightgrey;" \| Example
	!style="background-color:lightgrey;" \| Description		!style="background-color:lightgrey;" \| Description

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-10T07:46:26Z

ProB LTSmin CLI-Commands

← Older revision		Revision as of 07:46, 10 June 2020
Line 26:		Line 26:

	{\| cellpadding="5" cellspacing="1" width="100%" border="1"		{\| cellpadding="5" cellspacing="1" width="100%" border="1"
	!style="background-color:lightgrey;" \| Flag		!style="background-color:lightgrey;" \| probcli Flag
	!style="background-color:lightgrey;" \| Example		!style="background-color:lightgrey;" \| Example
	!style="background-color:lightgrey;" \| Description		!style="background-color:lightgrey;" \| Description

Michael Leuschel: /* ProB LTSmin CLI-Commands */

2020-06-10T07:46:04Z

ProB LTSmin CLI-Commands

@@ Line 25: / Line 25: @@
 Note that on Linux, you might prefix the commands with LD_LIBRARY_PATH=lib/
-Flag	Example Usage	Description
+{| cellpadding="5" cellspacing="1" width="100%" border="1"
--ltsmin	./probcli -ltsmin FILE	Start the ProB server for LTSmin at the default endpoint /tmp/ltsmin.probz - it will use the machine FILE in order to provide information to LTSmin
+!style="background-color:lightgrey;" | Flag
--ltsmin2	./probcli -ltsmin2 endpoint.probz FILE	Start the ProB server for LTSmin at the endpoint given by the specific endpoint.probz file. It will use the machine FILE in order to provide information to LTSmin
+!style="background-color:lightgrey;" | Example
--mc-with-lts-seq	./probcli -nodead -mc-with-lts-seq FILE	Start invariant model checking with the sequential backend of LTSmin on FILE. Note that at least one of -nodead or -noinv must be provided.
+!style="background-color:lightgrey;" | Description
--mc-with-lts-sym	./probcli -nodead -mc-with-lts-sym FILE	Start invariant model checking with the symbolic backend of LTSmin on FILE. Note that at least one of -nodead or -noinv must be provided.
+|-
--p LTSMIN	-p LTSMIN /opt/ltsmin/	Use the LTSmin commands in the provided directory (here /opt/ltsmin)
+ | -ltsmin