LTSmin: Difference between revisions

Revision as of 10:31, 12 June 2020

LTSmin is a high-performance language-independent model checker that allows numerous modelling language front-ends to be connected to various analysis algorithms, through a common interface.

LTSmin Extension of ProB

We have implemented an integration of LTSmin with ProB for symbolic reachability and for explicit state model checking:

Symbolic Reachability Analysis of B Through ProB and LTSmin, Proceedings of iFM'2016
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin, Proceedings iFM'2018.

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
(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)…
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)

Note that the LTSmin extension is not available for Windows.

ProB LTSmin CLI-Commands

Note that on Linux, you might prefix the commands with LD_LIBRARY_PATH=lib/

probcli Flag	Example	Description
-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
-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
-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.
-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)

An example run:

$ 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

Here a run that finds a counter example:

probcli public_examples/B/Demo/CarlaTravelAgencyErr.mch -mc_with_lts_seq -nodead -p LTSMIN ~/bin/ltsmin_v3.0.2/bin 
% unused_constants(1,[AGENCY_USER])
prob2lts-seq, 0.000: ProB module initialized
prob2lts-seq, 0.000: Loading model from /tmp/ltsmin.probz
prob2lts-seq, 0.000: ProB init
prob2lts-seq, 0.000: connecting to zocket ipc:///private/tmp/ltsmin.probz
starting prob2lts-sym/seq (flags nodead=true, noinv=false, moreflags=[])
Merging last 9 of 16 invariants (LTSMin POR supports max 8 invariants)
pl_init_for_lts_min
vars([session,session_response,session_card,session_state,session_request,user_hotel_bookings,user_rental_bookings,rooms_hotel,cars_rental,global_room_bookings,global_car_bookings,AGENCY_USER])
prob2lts-seq, 0.024: "!is_init || (inv16 && inv15 && inv14 && inv13 && inv12 && inv11 && inv10 && inv9 && inv8 && inv7 && inv6 && inv5 && inv4 && inv3 && inv2 && inv1)" is not a file, parsing as formula...
prob2lts-seq, 0.024: There are 18 state labels and 1 edge labels
prob2lts-seq, 0.024: State length is 13, there are 11 groups
prob2lts-seq, 0.024: Running dfs search strategy
prob2lts-seq, 0.024: Using a tree for state storage
% Runtime for SOLUTION for SETUP_CONSTANTS: 42 ms (walltime: 44 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 2 ms (walltime: 2 ms)
% Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
% Runtime to FINALISE SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
prob2lts-seq, 0.258:  
prob2lts-seq, 0.258: Invariant violation (!is_init || (inv16 && inv15 && inv14 && inv13 && inv12 && inv11 && inv10 && inv9 && inv8 && inv7 && inv6 && inv5 && inv4 && inv3 && inv2 && inv1)) found at depth 38!
prob2lts-seq, 0.258:  
prob2lts-seq, 0.258: Writing trace to /tmp/prob-ltsmin-trace.gcf
prob2lts-seq, 0.264: terminating ProB connection
get-next-state:          306
get-next-state (short):  0
get-next-action:         0
get-next-action (short): 0
get-state-label:         184
get-state-label (short): 0
get-label-group:         0
prob2lts-seq, 0.265: disconnecting from zocket ipc:///private/tmp/ltsmin.probz
prob2lts-seq, 0.266: exiting now
ltsmin-printtrace: Writing output to '/tmp/prob-ltsmin-trace.csv'
ltsmin-printtrace: realloc
ltsmin-printtrace: action labeled, detecting silent step
ltsmin-printtrace: no silent label
ltsmin-printtrace: length of trace is 37
writing trace to /tmp/prob-ltsmin-trace.csv
/prob2lts-seq with [--trace,/tmp/prob-ltsmin-trace.gcf,-c,--invariant=!is_init || (inv16 && inv15 && inv14 && inv13 && inv12 && inv11 && inv10 && inv9 && inv8 && inv7 && inv6 && inv5 && inv4 && inv3 && inv2 && inv1)] exited with status: exit(1)
! An error occurred (source: ltsmin_counter_example_found) !
! LTSMin found a counter example, written to: /tmp/prob-ltsmin-trace.csv
*** TRACE: 
(37) $init_state login unbookCar enterCard logout login unbookCar enterCard logout login unbookCar enterCard response login logout unbookCar enterCard response login again unbookCar enterCard retryCard response unbookCar again enterCard retryCard response unbookCar enterCard logout login logout unbookCar enterCard response 
! *** error occurred ***
! ltsmin_counter_example_found
! Total Errors: 1, Warnings:0