alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Update documentation.

Browse source 
* iface/ltsmin/README: here.
This commit is contained in:
Etienne Renault 2015-04-23 19:48:08 +02:00
parent 5f4b7e1f3f
commit 528cc04cca
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
iface/ltsmin/README
View file

@ -121,11 +121,11 @@ Usage with Spot
Examples Examples
======== ========
Using the dve2check program built into this directory, we can verify Using the modelcheck program built into this directory, we can verify
that the critical section is accessed infinitely often by some that the critical section is accessed infinitely often by some
processes using: processes using:
% ./dve2check beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' % ./modelcheck beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
2239039 unique states visited 2239039 unique states visited
0 strongly connected components in search stack 0 strongly connected components in search stack
11449204 transitions explored 11449204 transitions explored
@ -134,7 +134,7 @@ Examples
Process P_0 can starve, waiting to enter in critical section: Process P_0 can starve, waiting to enter in critical section:
% ./dve2check beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)' % ./modelcheck beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
2190 unique states visited 2190 unique states visited
34 strongly connected components in search stack 34 strongly connected components in search stack
4896 transitions explored 4896 transitions explored
@ -144,7 +144,7 @@ Examples
Variable pos[1] is not always < 3 (this formula makes no sense, it Variable pos[1] is not always < 3 (this formula makes no sense, it
is just to demonstrate the use of double quote). is just to demonstrate the use of double quote).
% ./dve2check beem-peterson.4.dve '!G("pos[1] < 3")' % ./modelcheck beem-peterson.4.dve '!G("pos[1] < 3")'
130 unique states visited 130 unique states visited
61 strongly connected components in search stack 61 strongly connected components in search stack
132 transitions explored 132 transitions explored
@ -158,7 +158,7 @@ than 2^28, it is way faster than -z (which will work for all values).
Activating state compression will often reduce runtime. Compare: Activating state compression will often reduce runtime. Compare:
% ./dve2check -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' % ./modelcheck -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
2239039 unique states visited 2239039 unique states visited
0 strongly connected components in search stack 0 strongly connected components in search stack
11449204 transitions explored 11449204 transitions explored
@ -176,7 +176,7 @@ running emptiness chec | 1222 100.0 | 18 100.0 | 1240 100.0 | 1
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 | TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 |
% ./dve2check -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' % ./modelcheck -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
2239039 unique states visited 2239039 unique states visited
0 strongly connected components in search stack 0 strongly connected components in search stack
11449204 transitions explored 11449204 transitions explored