LTSmin: Difference between revisions

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 (as of ProB 1.12.0-beta1 you can also simply type probcli --install ltsmin)
• (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 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 probcli --install ltsmin)
• 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/

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